feat(codegen): Kani harnesses for generated-code AADL contract preservation

Add three #[kani::proof] harnesses in crates/spar-codegen/tests/kani_contracts.rs
that prove each codegen pass preserves the AADL source contract (spar's
Logika-equivalent strategy: machine-checked proofs on the generated-code path).

- prove_thread_period_preserved: for any Period p in (0, 1_000_000_000] ns,
  the emitted dispatch-metadata string round-trips back to exactly p (no
  truncation, no off-by-one)
- prove_port_direction_preserved: Out→In connections produce complementary
  WIT setter+getter pairs; same-direction connections never produce a
  complementary pair (AADL §9 directionality contract)
- prove_access_right_preserved: Access_Rights = Read_Only never produces
  &mut in the generated access shim; Read_Write always does (type-level
  read-only enforcement)

Wire-up: add kani-harnesses feature flag to spar-codegen/Cargo.toml; extend
CI Kani job to run each harness explicitly; add REQ-KANI-CODEGEN-001 +
TEST-KANI-CODEGEN to artifacts YAML.

Co-Authored-By: Claude Opus 4.7 <noreply@anthropic.com>

Author: avrabe

.github/workflows/ci.yml

@@ -323,5 +323,13 @@ jobs:
           cargo kani setup
       - name: Run Kani on spar-solver
         run: cargo kani --tests -p spar-solver
-      - name: Run Kani on spar-codegen
-        run: cargo kani --tests -p spar-codegen
+      - name: Run Kani on spar-codegen (schedule harness)
+        run: cargo kani --tests -p spar-codegen --harness kani_emit_preserves_schedule
+      - name: Run Kani on spar-codegen (AADL contract harnesses)
+        # prove_thread_period_preserved  — period round-trip (no truncation)
+        # prove_port_direction_preserved — WIT direction token mapping
+        # prove_access_right_preserved   — Read_Only never widens to &mut
+        run: >-
+          cargo kani --tests -p spar-codegen --harness prove_thread_period_preserved &&
+          cargo kani --tests -p spar-codegen --harness prove_port_direction_preserved &&
+          cargo kani --tests -p spar-codegen --harness prove_access_right_preserved

artifacts/requirements.yaml

@@ -855,6 +855,27 @@ artifacts:
       - type: traces-to
         target: REQ-CODEGEN-001
 
+  - id: REQ-KANI-CODEGEN-001
+    type: requirement
+    title: Kani harnesses for generated-code AADL contract preservation
+    description: >
+      Three Kani bounded model-checking harnesses in crates/spar-codegen/tests/
+      kani_contracts.rs prove that each codegen pass preserves the AADL source
+      contract: (1) thread Period is emitted without truncation or off-by-one
+      (prove_thread_period_preserved), (2) port direction is faithfully mapped
+      to the WIT interface token (prove_port_direction_preserved), (3) a
+      bus-access feature with Access_Rights = Read_Only never generates a &mut
+      reference (prove_access_right_preserved).  This is spar's
+      Logika-equivalent strategy: machine-checked proofs on the codegen output
+      path rather than importing a new prover language.
+    status: implemented
+    tags: [codegen, kani, verification, v0100, safety]
+    links:
+      - type: traces-to
+        target: REQ-CODEGEN-VERIFY-PROOF
+      - type: traces-to
+        target: REQ-CODEGEN-001
+
   - id: REQ-SYSML2-PARSE
     type: requirement
     title: Parse SysML v2 textual notation (KerML grammar)

artifacts/verification.yaml

@@ -914,6 +914,39 @@ artifacts:
       - type: verifies
         target: REQ-CODEGEN-VERIFY-PROOF
 
+  - id: TEST-KANI-CODEGEN
+    type: feature
+    status: passing
+    title: Kani — AADL contract preservation harnesses for codegen
+    description: >
+      Three #[kani::proof] harnesses in crates/spar-codegen/tests/kani_contracts.rs
+      constitute spar's Logika-equivalent strategy for generated-code correctness.
+      Each harness uses kani::any() + kani::assume() for symbolic inputs and
+      asserts the postcondition that the codegen pass must satisfy:
+        prove_thread_period_preserved — for any Period p in (0, 1_000_000_000] ns,
+          the emitted dispatch-metadata string round-trips back to exactly p ns
+          (no truncation, no off-by-one);
+        prove_port_direction_preserved — Out source maps exclusively to a WIT setter
+          and In sink to a WIT getter; a well-formed Out→In connection always produces
+          a complementary setter+getter pair; same-direction features never produce a
+          complementary pair;
+        prove_access_right_preserved — Access_Rights = Read_Only never produces
+          &mut in the generated access shim (read-only enforcement at the type level),
+          and Read_Write always does.
+    fields:
+      method: formal-bounded
+      steps:
+        - run: cargo kani --tests -p spar-codegen --harness prove_thread_period_preserved
+        - run: cargo kani --tests -p spar-codegen --harness prove_port_direction_preserved
+        - run: cargo kani --tests -p spar-codegen --harness prove_access_right_preserved
+    links:
+      - type: satisfies
+        target: REQ-KANI-CODEGEN-001
+      - type: satisfies
+        target: REQ-CODEGEN-VERIFY-PROOF
+      - type: satisfies
+        target: REQ-CODEGEN-001
+
   - id: VAL-MUTATION-001
     type: feature
     status: pass

crates/spar-codegen/Cargo.toml

@@ -31,6 +31,16 @@ harness = false
 [target.'cfg(kani)'.dev-dependencies]
 # `kani` is injected by cargo-kani; no version pin needed.
 
+[features]
+# Enable the AADL-contract Kani harnesses in tests/kani_contracts.rs.
+# Under `cargo kani --tests`, the harnesses are compiled via the `#[cfg(kani)]`
+# cfg-guard (injected by the cargo-kani driver).  This feature flag is a
+# no-op at runtime; it exists so `cargo build -p spar-codegen --features
+# kani-harnesses` can verify the harness module compiles under a normal
+# Rust toolchain without requiring the Kani driver.
+kani-harnesses = []
+
 [lints.rust]
-# Permit the `#[cfg(kani)]` gates used by `tests/kani_codegen.rs`.
+# Permit the `#[cfg(kani)]` gates used by `tests/kani_codegen.rs` and
+# `tests/kani_contracts.rs`.
 unexpected_cfgs = { level = "warn", check-cfg = ['cfg(kani)'] }