From 85559bd2d5ce064ee9be8e1cf4f01f8b61184bd3 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Onur=20=C3=96zkan?= Date: Sat, 18 Jul 2026 13:28:01 +0300 Subject: [PATCH] make spec infra more ergonomic MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Signed-off-by: Onur Özkan --- README.md | 12 ++--- SPECIFICATIONS.md | 26 ++++++---- kaptan-spec/src/lib.rs | 51 +++++++------------ kaptan-spec/tests/spec_macro.rs | 11 ++-- .../tests/ui/fail_empty_explanation.rs | 5 ++ .../tests/ui/fail_empty_explanation.stderr | 7 +++ kaptan-spec/tests/ui/fail_invalid_suffix.rs | 6 --- .../tests/ui/fail_invalid_suffix.stderr | 7 --- .../tests/ui/fail_legacy_named_argument.rs | 6 --- .../ui/fail_legacy_named_argument.stderr | 7 --- kaptan-spec/tests/ui/fail_missing_argument.rs | 5 +- .../tests/ui/fail_missing_argument.stderr | 8 +-- kaptan-spec/tests/ui/fail_missing_sidecar.rs | 7 --- .../tests/ui/fail_missing_sidecar.stderr | 5 -- kaptan-spec/tests/ui/fail_non_module_item.rs | 6 --- .../tests/ui/fail_non_module_item.stderr | 7 --- .../tests/ui/fail_non_string_argument.rs | 5 +- .../tests/ui/fail_non_string_argument.stderr | 8 +-- kaptan-spec/tests/ui/flight_core_contract.rs | 3 +- kaptan-spec/tests/ui/no_spec.rs | 5 ++ 20 files changed, 74 insertions(+), 123 deletions(-) create mode 100644 kaptan-spec/tests/ui/fail_empty_explanation.rs create mode 100644 kaptan-spec/tests/ui/fail_empty_explanation.stderr delete mode 100644 kaptan-spec/tests/ui/fail_invalid_suffix.rs delete mode 100644 kaptan-spec/tests/ui/fail_invalid_suffix.stderr delete mode 100644 kaptan-spec/tests/ui/fail_legacy_named_argument.rs delete mode 100644 kaptan-spec/tests/ui/fail_legacy_named_argument.stderr delete mode 100644 kaptan-spec/tests/ui/fail_missing_sidecar.rs delete mode 100644 kaptan-spec/tests/ui/fail_missing_sidecar.stderr delete mode 100644 kaptan-spec/tests/ui/fail_non_module_item.rs delete mode 100644 kaptan-spec/tests/ui/fail_non_module_item.stderr create mode 100644 kaptan-spec/tests/ui/no_spec.rs diff --git a/README.md b/README.md index e127142..9ebc223 100644 --- a/README.md +++ b/README.md @@ -2,7 +2,7 @@ Kaptan is a modular flight controller platform focused on deterministic bare-metal execution for flight-critical paths and strong verification discipline around the rest of the stack. -The repository is currently in infrastructure setup. Formal project specifications should be linked directly from the code they govern through compile-time attributes. +The repository is currently in infrastructure setup. Formal project specifications are automatically checked beside the file-backed modules they govern. ## Current Direction @@ -32,14 +32,14 @@ Formal specs should be colocated with the code or board package they govern. - Version history should live inside the same spec file as additional spec entries, not in the filename. - Each appended spec entry should begin with version marker such as `# --- version: 0.1.0 ---`. - Inside a spec entry, `#` is reserved for version markers and content headings should start at `##`. -- Rust items should link to those sidecar specs through `#[spec("...")]`. -- Missing linked spec files must fail compilation. +- Each file-backed Rust module requires a same-name `.spec.md` sidecar. +- Modules that intentionally have no formal specification must declare `no_spec!("reason");` at module scope. +- Missing sidecars and modules that have both a sidecar and `no_spec!(...)` fail the build. Example: ```rust -use kaptan_spec::spec; +use kaptan_spec::no_spec; -#[spec("control_loop.spec.md")] -pub struct ControlLoop; +no_spec!("Crate root declares child modules only."); ``` diff --git a/SPECIFICATIONS.md b/SPECIFICATIONS.md index b0f689a..c5db1fe 100644 --- a/SPECIFICATIONS.md +++ b/SPECIFICATIONS.md @@ -1,28 +1,34 @@ # Specifications -Formal Kaptan specifications should normally live next to the code item they govern. +Formal Kaptan specifications live next to the file-backed module they govern. Examples: -- `kaptan-runtime/src/control_loop.rs` -- `kaptan-runtime/src/control_loop.spec.md` +- `kaptan-runtime/src/runtime.rs` +- `kaptan-runtime/src/runtime.spec.md` - `kaptan-runtime/src/scheduler.rs` - `kaptan-runtime/src/scheduler.spec.md` -## Compile-Time Linking +## Automatic Sidecar Checks -Code implementations should link to their governing spec through `#[spec("...")]`. +Kaptan build checks require a same-name `.spec.md` sidecar for every file-backed Rust module under a checked crate's `src/` tree. -Example: +For example, `control_loop.rs` requires `control_loop.spec.md` in the same directory. A checked module must have exactly one of: + +- its sidecar specification; or +- a top-level `no_spec!("reason");` declaration. + +`no_spec!` is only for module files that intentionally have no formal specification, such as a crate root that only declares child modules. It must provide a non-empty reason and must not be used for types, functions, or individual items. + +Example for a crate root without standalone runtime behavior: ```rust -use kaptan_spec::spec; +use kaptan_spec::no_spec; -#[spec("control_loop.spec.md")] -pub struct ControlLoop; +no_spec!("Crate root declares child modules only."); ``` -The attribute expands to a compile-time file inclusion guard. If the linked file does not exist, compilation fails. +The build fails if a required sidecar is missing or a module contains both a sidecar and `no_spec!(...)`. ## Spec Format diff --git a/kaptan-spec/src/lib.rs b/kaptan-spec/src/lib.rs index 0911393..a6f3415 100644 --- a/kaptan-spec/src/lib.rs +++ b/kaptan-spec/src/lib.rs @@ -1,27 +1,26 @@ use proc_macro::{Literal, TokenStream, TokenTree}; -#[proc_macro_attribute] -pub fn spec(attr: TokenStream, item: TokenStream) -> TokenStream { - match parse_spec_path(attr) { - Ok(path) if is_module_item(&item) => expand_spec_guard(&path, item), - Ok(_) => compile_error("`#[spec]` may only be applied to a module"), +#[proc_macro] +pub fn no_spec(input: TokenStream) -> TokenStream { + match parse_no_spec_reason(input) { + Ok(reason) => expand_no_spec_reason(&reason), Err(message) => compile_error(&message), } } -fn parse_spec_path(attr: TokenStream) -> Result { - let tokens: Vec = attr.into_iter().collect(); +fn parse_no_spec_reason(input: TokenStream) -> Result { + let tokens: Vec = input.into_iter().collect(); match tokens.as_slice() { [TokenTree::Literal(path)] if is_string_literal(path) => { - if has_spec_suffix(path) { + if has_non_empty_string(path) { Ok(path.to_string()) } else { - Err("spec path must end in `.spec.md`; use #[spec(\"file.spec.md\")]".into()) + Err("no-spec explanation must not be empty; use no_spec!(\"reason\");".into()) } } - [] => Err("missing spec path; use #[spec(\"file.spec.md\")]".into()), - _ => Err("invalid spec attribute; use #[spec(\"file.spec.md\")]".into()), + [] => Err("missing no-spec explanation; use no_spec!(\"reason\");".into()), + _ => Err("invalid no-spec invocation; use no_spec!(\"reason\");".into()), } } @@ -31,30 +30,16 @@ fn is_string_literal(literal: &Literal) -> bool { value.starts_with('"') && value.ends_with('"') } -fn has_spec_suffix(literal: &Literal) -> bool { - literal - .to_string() - .strip_suffix('"') - .is_some_and(|path| path.ends_with(".spec.md")) +fn has_non_empty_string(literal: &Literal) -> bool { + let value = literal.to_string(); + + !value[1..value.len() - 1].trim().is_empty() } -fn is_module_item(item: &TokenStream) -> bool { - item.clone().into_iter().any( - |token| matches!(token, TokenTree::Ident(identifier) if identifier.to_string() == "mod"), - ) -} - -fn expand_spec_guard(path: &str, item: TokenStream) -> TokenStream { - let guard = format!("const _: &str = include_str!({path});"); - let mut output = TokenStream::new(); - - output.extend( - guard - .parse::() - .expect("spec macro must generate valid Rust tokens"), - ); - output.extend(item); - output +fn expand_no_spec_reason(reason: &str) -> TokenStream { + format!("const _: &str = {reason};") + .parse::() + .expect("no_spec macro must generate valid Rust tokens") } fn compile_error(message: &str) -> TokenStream { diff --git a/kaptan-spec/tests/spec_macro.rs b/kaptan-spec/tests/spec_macro.rs index a62807c..f36d91a 100644 --- a/kaptan-spec/tests/spec_macro.rs +++ b/kaptan-spec/tests/spec_macro.rs @@ -1,17 +1,14 @@ #[test] -fn accepts_existing_sidecar_spec() { +fn accepts_no_spec_reason() { let tests = trybuild::TestCases::new(); - tests.pass("tests/ui/flight_core_contract.rs"); + tests.pass("tests/ui/no_spec.rs"); } #[test] -fn rejects_invalid_spec_uses() { +fn rejects_invalid_no_spec_invocations() { let tests = trybuild::TestCases::new(); tests.compile_fail("tests/ui/fail_missing_argument.rs"); - tests.compile_fail("tests/ui/fail_legacy_named_argument.rs"); tests.compile_fail("tests/ui/fail_non_string_argument.rs"); - tests.compile_fail("tests/ui/fail_invalid_suffix.rs"); - tests.compile_fail("tests/ui/fail_missing_sidecar.rs"); - tests.compile_fail("tests/ui/fail_non_module_item.rs"); + tests.compile_fail("tests/ui/fail_empty_explanation.rs"); } diff --git a/kaptan-spec/tests/ui/fail_empty_explanation.rs b/kaptan-spec/tests/ui/fail_empty_explanation.rs new file mode 100644 index 0000000..9de6eb4 --- /dev/null +++ b/kaptan-spec/tests/ui/fail_empty_explanation.rs @@ -0,0 +1,5 @@ +use kaptan_spec::no_spec; + +no_spec!(" "); + +fn main() {} \ No newline at end of file diff --git a/kaptan-spec/tests/ui/fail_empty_explanation.stderr b/kaptan-spec/tests/ui/fail_empty_explanation.stderr new file mode 100644 index 0000000..f50f814 --- /dev/null +++ b/kaptan-spec/tests/ui/fail_empty_explanation.stderr @@ -0,0 +1,7 @@ +error: no-spec explanation must not be empty; use no_spec!("reason"); + --> tests/ui/fail_empty_explanation.rs:3:1 + | +3 | no_spec!(" "); + | ^^^^^^^^^^^^^^^ + | + = note: this error originates in the macro `no_spec` (in Nightly builds, run with -Z macro-backtrace for more info) diff --git a/kaptan-spec/tests/ui/fail_invalid_suffix.rs b/kaptan-spec/tests/ui/fail_invalid_suffix.rs deleted file mode 100644 index 293e9cd..0000000 --- a/kaptan-spec/tests/ui/fail_invalid_suffix.rs +++ /dev/null @@ -1,6 +0,0 @@ -use kaptan_spec::spec; - -#[spec("flight_core_contract.md")] -struct InvalidSuffix; - -fn main() {} \ No newline at end of file diff --git a/kaptan-spec/tests/ui/fail_invalid_suffix.stderr b/kaptan-spec/tests/ui/fail_invalid_suffix.stderr deleted file mode 100644 index 512489b..0000000 --- a/kaptan-spec/tests/ui/fail_invalid_suffix.stderr +++ /dev/null @@ -1,7 +0,0 @@ -error: spec path must end in `.spec.md`; use #[spec("file.spec.md")] - --> tests/ui/fail_invalid_suffix.rs:3:1 - | -3 | #[spec("flight_core_contract.md")] - | ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ - | - = note: this error originates in the attribute macro `spec` (in Nightly builds, run with -Z macro-backtrace for more info) diff --git a/kaptan-spec/tests/ui/fail_legacy_named_argument.rs b/kaptan-spec/tests/ui/fail_legacy_named_argument.rs deleted file mode 100644 index c5c539c..0000000 --- a/kaptan-spec/tests/ui/fail_legacy_named_argument.rs +++ /dev/null @@ -1,6 +0,0 @@ -use kaptan_spec::spec; - -#[spec(path = "flight_core_contract.spec.md")] -struct LegacyNamedArgument; - -fn main() {} \ No newline at end of file diff --git a/kaptan-spec/tests/ui/fail_legacy_named_argument.stderr b/kaptan-spec/tests/ui/fail_legacy_named_argument.stderr deleted file mode 100644 index 8e45974..0000000 --- a/kaptan-spec/tests/ui/fail_legacy_named_argument.stderr +++ /dev/null @@ -1,7 +0,0 @@ -error: invalid spec attribute; use #[spec("file.spec.md")] - --> tests/ui/fail_legacy_named_argument.rs:3:1 - | -3 | #[spec(path = "flight_core_contract.spec.md")] - | ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ - | - = note: this error originates in the attribute macro `spec` (in Nightly builds, run with -Z macro-backtrace for more info) diff --git a/kaptan-spec/tests/ui/fail_missing_argument.rs b/kaptan-spec/tests/ui/fail_missing_argument.rs index 4b62f4f..dbc02c8 100644 --- a/kaptan-spec/tests/ui/fail_missing_argument.rs +++ b/kaptan-spec/tests/ui/fail_missing_argument.rs @@ -1,6 +1,5 @@ -use kaptan_spec::spec; +use kaptan_spec::no_spec; -#[spec] -struct MissingArgument; +no_spec!(); fn main() {} \ No newline at end of file diff --git a/kaptan-spec/tests/ui/fail_missing_argument.stderr b/kaptan-spec/tests/ui/fail_missing_argument.stderr index d2c56d3..8734b9b 100644 --- a/kaptan-spec/tests/ui/fail_missing_argument.stderr +++ b/kaptan-spec/tests/ui/fail_missing_argument.stderr @@ -1,7 +1,7 @@ -error: missing spec path; use #[spec("file.spec.md")] +error: missing no-spec explanation; use no_spec!("reason"); --> tests/ui/fail_missing_argument.rs:3:1 | -3 | #[spec] - | ^^^^^^^ +3 | no_spec!(); + | ^^^^^^^^^^ | - = note: this error originates in the attribute macro `spec` (in Nightly builds, run with -Z macro-backtrace for more info) + = note: this error originates in the macro `no_spec` (in Nightly builds, run with -Z macro-backtrace for more info) diff --git a/kaptan-spec/tests/ui/fail_missing_sidecar.rs b/kaptan-spec/tests/ui/fail_missing_sidecar.rs deleted file mode 100644 index 9057817..0000000 --- a/kaptan-spec/tests/ui/fail_missing_sidecar.rs +++ /dev/null @@ -1,7 +0,0 @@ -use kaptan_spec::spec; - -#[spec("fail_missing_sidecar.spec.md")] -mod missing_spec {} - -fn main() { -} \ No newline at end of file diff --git a/kaptan-spec/tests/ui/fail_missing_sidecar.stderr b/kaptan-spec/tests/ui/fail_missing_sidecar.stderr deleted file mode 100644 index bd7cd1e..0000000 --- a/kaptan-spec/tests/ui/fail_missing_sidecar.stderr +++ /dev/null @@ -1,5 +0,0 @@ -error: couldn't read `$DIR/tests/ui/fail_missing_sidecar.spec.md`: No such file or directory (os error 2) - --> tests/ui/fail_missing_sidecar.rs:3:1 - | -3 | #[spec("fail_missing_sidecar.spec.md")] - | ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ diff --git a/kaptan-spec/tests/ui/fail_non_module_item.rs b/kaptan-spec/tests/ui/fail_non_module_item.rs deleted file mode 100644 index 16bd7bb..0000000 --- a/kaptan-spec/tests/ui/fail_non_module_item.rs +++ /dev/null @@ -1,6 +0,0 @@ -use kaptan_spec::spec; - -#[spec("flight_core_contract.spec.md")] -struct FlightCore; - -fn main() {} \ No newline at end of file diff --git a/kaptan-spec/tests/ui/fail_non_module_item.stderr b/kaptan-spec/tests/ui/fail_non_module_item.stderr deleted file mode 100644 index 7825be9..0000000 --- a/kaptan-spec/tests/ui/fail_non_module_item.stderr +++ /dev/null @@ -1,7 +0,0 @@ -error: `#[spec]` may only be applied to a module - --> tests/ui/fail_non_module_item.rs:3:1 - | -3 | #[spec("flight_core_contract.spec.md")] - | ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ - | - = note: this error originates in the attribute macro `spec` (in Nightly builds, run with -Z macro-backtrace for more info) diff --git a/kaptan-spec/tests/ui/fail_non_string_argument.rs b/kaptan-spec/tests/ui/fail_non_string_argument.rs index 7a61a0d..ecce319 100644 --- a/kaptan-spec/tests/ui/fail_non_string_argument.rs +++ b/kaptan-spec/tests/ui/fail_non_string_argument.rs @@ -1,6 +1,5 @@ -use kaptan_spec::spec; +use kaptan_spec::no_spec; -#[spec(42)] -struct NonStringArgument; +no_spec!(42); fn main() {} \ No newline at end of file diff --git a/kaptan-spec/tests/ui/fail_non_string_argument.stderr b/kaptan-spec/tests/ui/fail_non_string_argument.stderr index ff595e6..7b5780f 100644 --- a/kaptan-spec/tests/ui/fail_non_string_argument.stderr +++ b/kaptan-spec/tests/ui/fail_non_string_argument.stderr @@ -1,7 +1,7 @@ -error: invalid spec attribute; use #[spec("file.spec.md")] +error: invalid no-spec invocation; use no_spec!("reason"); --> tests/ui/fail_non_string_argument.rs:3:1 | -3 | #[spec(42)] - | ^^^^^^^^^^^ +3 | no_spec!(42); + | ^^^^^^^^^^^^ | - = note: this error originates in the attribute macro `spec` (in Nightly builds, run with -Z macro-backtrace for more info) + = note: this error originates in the macro `no_spec` (in Nightly builds, run with -Z macro-backtrace for more info) diff --git a/kaptan-spec/tests/ui/flight_core_contract.rs b/kaptan-spec/tests/ui/flight_core_contract.rs index 705ebd9..d2b0ca0 100644 --- a/kaptan-spec/tests/ui/flight_core_contract.rs +++ b/kaptan-spec/tests/ui/flight_core_contract.rs @@ -1,7 +1,6 @@ use kaptan_spec::spec; -#[spec("flight_core_contract.spec.md")] -mod flight_core {} +spec!("flight_core_contract.spec.md"); fn main() { assert_eq!(core::mem::size_of::<()>(), 0); diff --git a/kaptan-spec/tests/ui/no_spec.rs b/kaptan-spec/tests/ui/no_spec.rs new file mode 100644 index 0000000..7edfe0f --- /dev/null +++ b/kaptan-spec/tests/ui/no_spec.rs @@ -0,0 +1,5 @@ +use kaptan_spec::no_spec; + +no_spec!("This fixture has no governed runtime behavior."); + +fn main() {} \ No newline at end of file