make spec infra more ergonomic
Signed-off-by: Onur Özkan <work@onurozkan.dev>
This commit is contained in:
1 parent
b0a7a9bb03
commit
85559bd2d5
20 files changed
+74
-123
No files matched your search
@@ -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.
|
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
|
## 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.
|
- 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 ---`.
|
- 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 `##`.
|
- 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("...")]`.
|
- Each file-backed Rust module requires a same-name `.spec.md` sidecar.
|
||||||
- Missing linked spec files must fail compilation.
|
- 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:
|
Example:
|
||||||
|
|
||||||
```rust
|
```rust
|
||||||
use kaptan_spec::spec;
|
use kaptan_spec::no_spec;
|
||||||
|
|
||||||
#[spec("control_loop.spec.md")]
|
no_spec!("Crate root declares child modules only.");
|
||||||
pub struct ControlLoop;
|
|
||||||
```
|
```
|
||||||
+16
-10
@@ -1,28 +1,34 @@
|
|||||||
# Specifications
|
# 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:
|
Examples:
|
||||||
|
|
||||||
- `kaptan-runtime/src/control_loop.rs`
|
- `kaptan-runtime/src/runtime.rs`
|
||||||
- `kaptan-runtime/src/control_loop.spec.md`
|
- `kaptan-runtime/src/runtime.spec.md`
|
||||||
- `kaptan-runtime/src/scheduler.rs`
|
- `kaptan-runtime/src/scheduler.rs`
|
||||||
- `kaptan-runtime/src/scheduler.spec.md`
|
- `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
|
```rust
|
||||||
use kaptan_spec::spec;
|
use kaptan_spec::no_spec;
|
||||||
|
|
||||||
#[spec("control_loop.spec.md")]
|
no_spec!("Crate root declares child modules only.");
|
||||||
pub struct ControlLoop;
|
|
||||||
```
|
```
|
||||||
|
|
||||||
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
|
## Spec Format
|
||||||
|
|
||||||
|
|||||||
+18
-33
@@ -1,27 +1,26 @@
|
|||||||
use proc_macro::{Literal, TokenStream, TokenTree};
|
use proc_macro::{Literal, TokenStream, TokenTree};
|
||||||
|
|
||||||
#[proc_macro_attribute]
|
#[proc_macro]
|
||||||
pub fn spec(attr: TokenStream, item: TokenStream) -> TokenStream {
|
pub fn no_spec(input: TokenStream) -> TokenStream {
|
||||||
match parse_spec_path(attr) {
|
match parse_no_spec_reason(input) {
|
||||||
Ok(path) if is_module_item(&item) => expand_spec_guard(&path, item),
|
Ok(reason) => expand_no_spec_reason(&reason),
|
||||||
Ok(_) => compile_error("`#[spec]` may only be applied to a module"),
|
|
||||||
Err(message) => compile_error(&message),
|
Err(message) => compile_error(&message),
|
||||||
}
|
}
|
||||||
}
|
}
|
||||||
|
|
||||||
fn parse_spec_path(attr: TokenStream) -> Result<String, String> {
|
fn parse_no_spec_reason(input: TokenStream) -> Result<String, String> {
|
||||||
let tokens: Vec<TokenTree> = attr.into_iter().collect();
|
let tokens: Vec<TokenTree> = input.into_iter().collect();
|
||||||
|
|
||||||
match tokens.as_slice() {
|
match tokens.as_slice() {
|
||||||
[TokenTree::Literal(path)] if is_string_literal(path) => {
|
[TokenTree::Literal(path)] if is_string_literal(path) => {
|
||||||
if has_spec_suffix(path) {
|
if has_non_empty_string(path) {
|
||||||
Ok(path.to_string())
|
Ok(path.to_string())
|
||||||
} else {
|
} 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("missing no-spec explanation; use no_spec!(\"reason\");".into()),
|
||||||
_ => Err("invalid spec attribute; use #[spec(\"file.spec.md\")]".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('"')
|
value.starts_with('"') && value.ends_with('"')
|
||||||
}
|
}
|
||||||
|
|
||||||
fn has_spec_suffix(literal: &Literal) -> bool {
|
fn has_non_empty_string(literal: &Literal) -> bool {
|
||||||
literal
|
let value = literal.to_string();
|
||||||
.to_string()
|
|
||||||
.strip_suffix('"')
|
!value[1..value.len() - 1].trim().is_empty()
|
||||||
.is_some_and(|path| path.ends_with(".spec.md"))
|
|
||||||
}
|
}
|
||||||
|
|
||||||
fn is_module_item(item: &TokenStream) -> bool {
|
fn expand_no_spec_reason(reason: &str) -> TokenStream {
|
||||||
item.clone().into_iter().any(
|
format!("const _: &str = {reason};")
|
||||||
|token| matches!(token, TokenTree::Ident(identifier) if identifier.to_string() == "mod"),
|
.parse::<TokenStream>()
|
||||||
)
|
.expect("no_spec macro must generate valid Rust tokens")
|
||||||
}
|
|
||||||
|
|
||||||
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::<TokenStream>()
|
|
||||||
.expect("spec macro must generate valid Rust tokens"),
|
|
||||||
);
|
|
||||||
output.extend(item);
|
|
||||||
output
|
|
||||||
}
|
}
|
||||||
|
|
||||||
fn compile_error(message: &str) -> TokenStream {
|
fn compile_error(message: &str) -> TokenStream {
|
||||||
|
|||||||
@@ -1,17 +1,14 @@
|
|||||||
#[test]
|
#[test]
|
||||||
fn accepts_existing_sidecar_spec() {
|
fn accepts_no_spec_reason() {
|
||||||
let tests = trybuild::TestCases::new();
|
let tests = trybuild::TestCases::new();
|
||||||
tests.pass("tests/ui/flight_core_contract.rs");
|
tests.pass("tests/ui/no_spec.rs");
|
||||||
}
|
}
|
||||||
|
|
||||||
#[test]
|
#[test]
|
||||||
fn rejects_invalid_spec_uses() {
|
fn rejects_invalid_no_spec_invocations() {
|
||||||
let tests = trybuild::TestCases::new();
|
let tests = trybuild::TestCases::new();
|
||||||
|
|
||||||
tests.compile_fail("tests/ui/fail_missing_argument.rs");
|
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_non_string_argument.rs");
|
||||||
tests.compile_fail("tests/ui/fail_invalid_suffix.rs");
|
tests.compile_fail("tests/ui/fail_empty_explanation.rs");
|
||||||
tests.compile_fail("tests/ui/fail_missing_sidecar.rs");
|
|
||||||
tests.compile_fail("tests/ui/fail_non_module_item.rs");
|
|
||||||
}
|
}
|
||||||
@@ -0,0 +1,5 @@
|
|||||||
|
use kaptan_spec::no_spec;
|
||||||
|
|
||||||
|
no_spec!(" ");
|
||||||
|
|
||||||
|
fn main() {}
|
||||||
@@ -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)
|
||||||
@@ -1,6 +0,0 @@
|
|||||||
use kaptan_spec::spec;
|
|
||||||
|
|
||||||
#[spec("flight_core_contract.md")]
|
|
||||||
struct InvalidSuffix;
|
|
||||||
|
|
||||||
fn main() {}
|
|
||||||
@@ -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)
|
|
||||||
@@ -1,6 +0,0 @@
|
|||||||
use kaptan_spec::spec;
|
|
||||||
|
|
||||||
#[spec(path = "flight_core_contract.spec.md")]
|
|
||||||
struct LegacyNamedArgument;
|
|
||||||
|
|
||||||
fn main() {}
|
|
||||||
@@ -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)
|
|
||||||
@@ -1,6 +1,5 @@
|
|||||||
use kaptan_spec::spec;
|
use kaptan_spec::no_spec;
|
||||||
|
|
||||||
#[spec]
|
no_spec!();
|
||||||
struct MissingArgument;
|
|
||||||
|
|
||||||
fn main() {}
|
fn main() {}
|
||||||
@@ -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
|
--> 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)
|
||||||
@@ -1,7 +0,0 @@
|
|||||||
use kaptan_spec::spec;
|
|
||||||
|
|
||||||
#[spec("fail_missing_sidecar.spec.md")]
|
|
||||||
mod missing_spec {}
|
|
||||||
|
|
||||||
fn main() {
|
|
||||||
}
|
|
||||||
@@ -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")]
|
|
||||||
| ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
|
|
||||||
@@ -1,6 +0,0 @@
|
|||||||
use kaptan_spec::spec;
|
|
||||||
|
|
||||||
#[spec("flight_core_contract.spec.md")]
|
|
||||||
struct FlightCore;
|
|
||||||
|
|
||||||
fn main() {}
|
|
||||||
@@ -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)
|
|
||||||
@@ -1,6 +1,5 @@
|
|||||||
use kaptan_spec::spec;
|
use kaptan_spec::no_spec;
|
||||||
|
|
||||||
#[spec(42)]
|
no_spec!(42);
|
||||||
struct NonStringArgument;
|
|
||||||
|
|
||||||
fn main() {}
|
fn main() {}
|
||||||
@@ -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
|
--> 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)
|
||||||
@@ -1,7 +1,6 @@
|
|||||||
use kaptan_spec::spec;
|
use kaptan_spec::spec;
|
||||||
|
|
||||||
#[spec("flight_core_contract.spec.md")]
|
spec!("flight_core_contract.spec.md");
|
||||||
mod flight_core {}
|
|
||||||
|
|
||||||
fn main() {
|
fn main() {
|
||||||
assert_eq!(core::mem::size_of::<()>(), 0);
|
assert_eq!(core::mem::size_of::<()>(), 0);
|
||||||
|
|||||||
@@ -0,0 +1,5 @@
|
|||||||
|
use kaptan_spec::no_spec;
|
||||||
|
|
||||||
|
no_spec!("This fixture has no governed runtime behavior.");
|
||||||
|
|
||||||
|
fn main() {}
|
||||||
Reference in new issue
Block a user