kreneskyp · Oct 25, 2026 · Oct 25, 2026 · Oct 25, 2026 · Oct 25, 2026
@@ -0,0 +1,54 @@
+---
+id: SR-57701
+title: "IR-329 PR 577 Kani module ownership map base spec review"
+type: SpecReview
+analysis: base
+review_set: subset
+scope: "agent-ix/quire-contract-codegen@21f28b1bec5df6471dd6735214ce3145545d21a4; spec/spec.md (Kani module and public-surface ownership map, four added rows)"
+---
+
+## Summary
+
+Ticket: IR-329. PR: quire-contract-codegen#577, frozen head 21f28b1b over base b60b18ef (CG
+main at review time). The diff adds four rows, and changes no existing row, to the Kani
+module and public-surface ownership map in `spec/spec.md`. This base review checks each added
+row's owner and status against the code on main, FR-015 and AD-004.
+
+## Examined scope
+
+- Row `kani/generate/{record,spec,render}`: examined. The files exist. AD-004 places
+  `record.rs`, and places `spec.rs` and `render.rs` at step 4b. FR-015-AC-112 to AC-117 are
+  Implemented (IR-858). `scalar.rs` and `clause/v2.rs` call `render::render`. `collection.rs`
+  already imports `record`.
+- Row `kani/generate/{collection,clause/v2}`: examined. Both files exist. `clause/v2.rs` is
+  only the "bounded cover harness for an admitted V2 parameter precondition", which
+  `negotiate.rs` wires in. FR-015-AC-38 to AC-49 are all PLANNED (IR-489).
+- Row `kani/generate/census_validation` and `kani/generate/corpus/mod.rs`: examined.
+  Checked against AD-004's `census_validation.rs` entry and the FR-015-AC-109 to AC-111
+  slices.
+- Row `role_parity_tests`, `test_support` and module roots: examined. See SR-57702.
+- Existing rows 1 and 3 (`{negotiate,...}`, `{clause,v1_bundle}`): context only, compared
+  for contradiction.
+- FR-015 "Planned (IR-489)" paragraph and "Partly implemented (IR-268)" paragraph: context only.
+
+## Verdict
+
+CHANGES REQUESTED. Every path named exists on main. No existing row or acceptance criterion
+changed. The diff adds no pin or SHA. `quire validate --scope . spec/spec.md` and
+`quire matrix` both pass. Two status cells say more than the code and FR-015 support.
+
+## Findings
+
+| ID | Severity | Summary | Refs |
+| --- | --- | --- | --- |
+| FND-001 | medium | The `{collection,clause/v2}` row says "V2 clause and collection lowerers are live". `clause/v2.rs` only lowers the V2 parameter-precondition cover. FR-015-AC-38 to AC-49 are all PLANNED (IR-489), and the existing `{negotiate,...}` row still says "V2 contract-clause items planned". The cell should say that only the V2 parameter-precondition cover is live and that AC-38 to AC-49 remain planned. | spec/spec.md:132 |
+| FND-002 | low | The `{record,spec,render}` row groups `record` with the unported pieces: "live for scalar and admitted V2 clause paths; collection and remaining families still need their AD-004 ports". `collection.rs` already uses `record`. Only `HarnessSpec` and `render` are still unported for collection (step 4h). | spec/spec.md:131 |
+
+## Dispositions
+
+Round 1, checked against fix-round head 59b9b4e031340a6642cdb160408c12f0f1b11d71.
+
+| FND | outcome | reason |
+| --- | --- | --- |
+| FND-001 | fixed | `{collection,clause/v2}` is split into two rows. The `clause/v2` row now says only the parameter-precondition cover harness is live and that FR-015-AC-38 to AC-49 remain PLANNED (IR-489). This matches `clause/v2.rs` and FR-015. |
+| FND-002 | fixed | The `{record,spec,render}` row now says the shared record is already used by collection and that only the step 4h rendering port remains. This matches the `record::` import in `collection.rs`. |
@@ -0,0 +1,59 @@
+---
+id: SR-57702
+title: "IR-329 PR 577 Kani module ownership map integrity analysis"
+type: SpecReview
+analysis: integrity
+review_set: subset
+scope: "agent-ix/quire-contract-codegen@21f28b1bec5df6471dd6735214ce3145545d21a4; spec/spec.md (Kani module and public-surface ownership map, four added rows)"
+---
+
+## Summary
+
+Ticket: IR-329. PR: quire-contract-codegen#577 at 21f28b1b. This integrity pass checks the
+map's coverage, single ownership per concept, consistency with AD-004's layout, and the
+precision of the retirement citations.
+
+## Examined scope
+
+- Completeness: examined. Every file under `src/kani/` on main now falls under some row.
+- `kani/generate/lower/mod.rs`: examined. It holds the non-test function `admit_family` and
+  tests traced to FR-015-AC-82, AC-86 and AC-88. Existing row 6 already owns it and retires
+  it at AC-111.
+- `kani/mod.rs`: examined. It holds module declarations and a `#[cfg(test)]` macro, with no
+  `pub use` re-exports. The crate root's re-exports are in `lib.rs`, so the row's
+  "module declarations" claim holds for `kani/mod.rs`.
+- `generate/mod.rs`, `run/mod.rs` and `output/mod.rs`: examined. They hold module
+  declarations and `#[cfg(test)]` helpers only.
+- `kani/test_support.rs`: examined. Its users include `run/{execute,harness,launch,memory,namespace,report_file,scalar,tool}.rs`,
+  `classify.rs`, `render.rs`, `scalar.rs`, `negotiate.rs` and the corpus.
+- `role_parity_tests.rs`: examined. It is traced to FR-014-AC-38, FR-015-AC-60 and
+  FR-015-AC-68, plus TC-024 and TC-025.
+- AD-004 source layout and step 2f item map: context only. It lists `clause.rs` as "the V1
+  clause lowering ... interim, reshaped by step 4c". It names neither `clause/v2.rs` nor
+  `role_parity_tests.rs`.
+
+## Verdict
+
+CHANGES REQUESTED. The map is now complete, and no row of the base file was changed or
+narrowed. Two new rows break single ownership or AD-004 consistency. Two citations are
+imprecise.
+
+## Findings
+
+| ID | Severity | Summary | Refs |
+| --- | --- | --- | --- |
+| FND-001 | medium | The module-roots row claims the `lower` module root as "test-only support and module declarations" with no API. `lower/mod.rs` holds the non-test profile-admission function `admit_family`. Existing row 6 already owns `lower/mod.rs` (FR-015-AC-82 to AC-89, retiring at AC-111). That is double ownership with contradictory descriptions. Drop `lower` from the roots list. | spec/spec.md:140; spec/spec.md:135; src/kani/generate/lower/mod.rs:14 |
+| FND-002 | medium | The map gives `kani/generate/clause/v2` its own V2 owner row, but AD-004's layout has no `clause/v2.rs` (nor `role_parity_tests.rs`). The module is declared inside `clause.rs`, which AD-004 and existing row 4 treat as V1-interim "pending AD-004 steps 4c to 4f". It is now unclear whether `clause/v2` retires or moves with its parent. Give it an AD-004 home, or note in the row that AD-004 does not yet place it. | spec/spec.md:132; spec/spec.md:133; src/kani/generate/clause.rs:4; spec/assurance/AD-004-cg-crate-layout.md:227 |
+| FND-003 | low | The final row's owner cell is one compound phrase for three different things. Read literally, "the FR-014/FR-015 criteria traced by the tests" covers `kani/test_support`, which mostly serves FR-017 run, report and classify tests. Give each item its own owner: `role_parity_tests` → its traced FR-014/FR-015 criteria; `test_support` → the criteria of the tests that use it (FR-015, FR-017); module roots → each child module's owner. | spec/spec.md:140; src/kani/test_support.rs |
+| FND-004 | low | The census row says `census_validation` and `corpus/mod.rs` retire under "FR-015-AC-110/111". AC-110, the collection slice, retires neither. `corpus/mod.rs` goes only with AC-111. AD-004 also lets the V2 census input replace `census_validation` instead. | spec/spec.md:134; spec/assurance/AD-004-cg-crate-layout.md:234 |
+
+## Dispositions
+
+Round 1, checked against fix-round head 59b9b4e031340a6642cdb160408c12f0f1b11d71.
+
+| FND | outcome | reason |
+| --- | --- | --- |
+| FND-001 | fixed | The module-roots row now names only `kani/mod.rs` and `kani/{generate,run,output}/mod.rs`. It states that `lower/mod.rs` is owned by the finite-input auxiliary row, which keeps a single owner. |
+| FND-002 | fixed | The `clause/v2` row states that AD-004 does not yet place this child of interim `clause.rs` and that its placement or retirement must be resolved with steps 4c to 4f. The `role_parity_tests` row states the same gap. |
+| FND-003 | fixed | Each item now has its own row. `role_parity_tests` is owned by FR-014-AC-38 and FR-015-AC-60/68, which matches its trace tags. `test_support` is owned by the FR-015 and FR-017 criteria of its users; its users in run, output, classify and generate were verified. Module roots are owned by their children's owners. |
+| FND-004 | fixed | The census row now ties `census_validation` to steps 4f/4g or replacement by the V2 census input. It ties `corpus/mod.rs` to FR-015-AC-111 only. |
@@ -0,0 +1,31 @@
+---
+id: SR-57703
+title: "IR-329 PR 577 Kani module ownership map EARS analysis"
+type: SpecReview
+analysis: ears-conformance
+review_set: subset
+scope: "agent-ix/quire-contract-codegen@21f28b1bec5df6471dd6735214ce3145545d21a4; spec/spec.md (Kani module and public-surface ownership map, four added rows)"
+---
+
+## Summary
+
+Ticket: IR-329. PR: quire-contract-codegen#577 at 21f28b1b. This pass checks the EARS
+requirement grammar of any requirement statement the diff adds or edits.
+
+## Examined scope
+
+- The four added map rows (spec/spec.md lines 131, 132, 134 and 140): examined. They are
+  descriptive ownership and status rows, not FR, NFR or StR statements.
+- No FR, NFR or StR statement and no acceptance criterion is added or edited
+  (`git diff origin/main...HEAD` touches only `spec/spec.md`, +4/-0).
+
+## Verdict
+
+PASS. No requirement statement is in scope, so there is no EARS defect. The status-wording
+issues in these rows are recorded in SR-57701 and SR-57702.
+
+## Findings
+
+| ID | Severity | Summary | Refs |
+| --- | --- | --- | --- |
+| FND-001 | low | No findings (placeholder) | - |
@@ -128,12 +128,19 @@ The current Kani module and public-surface ownership map is:
 | Current source or public operation | Normative owner | State |
 | --- | --- | --- |
 | `kani/generate/{negotiate,outcome,scalar,precondition,contract,frame}` and `negotiate_kani_obligations` | FR-015; FR-025 for argument/subject ABI | V2 scalar and state/frame items live; V2 contract-clause items planned (FR-015-AC-38 to AC-49). |
+| `kani/generate/{record,spec,render}` | FR-015; FR-025 for the recorded harness identity and ABI | The shared record is already used by collection; validated `HarnessSpec` and the shared renderer are live for scalar and the V2 parameter-precondition cover, while collection still needs its AD-004 step 4h rendering port. |
+| `kani/generate/collection` | FR-015 symbolic collection criteria | Collection lowering is live, but it still renders its own template pending AD-004 step 4h and FR-015-AC-96/99 completion. |
+| `kani/generate/clause/v2` | FR-015 V2 parameter-precondition cover | Only the parameter-precondition cover harness is live; V2 contract-clause FR-015-AC-38 to AC-49 remain PLANNED (IR-489). AD-004 does not yet place this child of interim `clause.rs`; its placement or retirement must be resolved with steps 4c to 4f. |
 | `kani/generate/{clause,v1_bundle}` and `generate_kani_bundle` | FR-015 interim bundle criteria; FR-025 ABI | V1 input and bundle live pending AD-004 steps 4c to 4f; no second enduring Kani generator is authorized by ADR-001 Q1. |
+| `kani/generate/census_validation` and `kani/generate/corpus/mod.rs` | FR-015 interim census and bounded-corpus criteria | V1 validation helpers remain until their last callers retire under AD-004 steps 4f/4g or the V2 census input replaces them; the corpus module entry retires with the final graph/API slice FR-015-AC-111. |
 | `kani/generate/lower/{bounded_kani_profile,finite_reference_graphs,bounded_collections}` and their three public classifier/lowering operations | FR-015-AC-82 to AC-89 | Arithmetic auxiliary retired by AC-109; remaining live finite-input auxiliaries retire per slice: `bounded_collections` at AC-110, `finite_reference_graphs`, `bounded_kani_profile` and `lower/mod.rs` at AC-111. |
 | `kani/generate/corpus/bounded_kani_corpus` and `generate_bounded_kani_corpus_case` | FR-015-AC-51 to AC-58 and AC-90 to AC-95 and AC-109 to AC-111 | Live graph/collection finite-input corpus; arithmetic retired at AC-109, with collection AC-110 and graph/the whole API AC-111 still pending under AD-004 step 4g (end state AC-95), each slice gated on IR-858, and the graph slice on IR-805; its generated-case classification ends with the last slice, and its replay is dropped with the final slice (AC-111), not planned. |
 | `kani/{abi,census,identity}` | FR-015 proof census and identity; FR-025 symbolic argument and subject ABI | Live support vocabulary; composite leaf ABI remains planned. |
 | `kani/{run,output,classify}` and the execution operations | FR-017, with FR-028 proof ceilings and NFR-006's real-Kani lane | Live run and report processing. |
 | `kani/terminal` | FR-029 and FR-030 | Live terminal maps; the backend adapter trait remains planned. |
+| `kani/generate/role_parity_tests` | FR-014-AC-38 and FR-015-AC-60/68 | Test-only role parity controls. AD-004 does not separately place this test module. |
+| `kani/test_support` | FR-015 and FR-017 criteria of the tests that use these shared helpers | Test-only fixtures shared across generation, run, output, and classification tests. |
+| `kani/mod.rs` and `kani/{generate,run,output}/mod.rs` | The normative owners of their child modules above | Module declarations and test-only helpers; no separate generation or run API. `kani/generate/lower/mod.rs` is owned by the finite-input auxiliary row above. |
 | `replay/{witness,function,frame,state_clause}` and Kani playback scanning in `kani/output/playback` | FR-016 witness decode/native replay and FR-024 QSL envelope intake | Live function/frame paths; common typed intake remains planned. Corpus replay is live until FR-015-AC-111 drops it. |
 
 FR-003, FR-007 and FR-023 have no active CG requirement artifacts or generator