From 85ca3167d2ac105b9f9f04f2499743a559729c89 Mon Sep 17 00:00:00 2001 From: Peter Krenesky Date: Sun, 25 Oct 2026 08:05:36 -0700 Subject: [PATCH 1/3] IR-329: enumerate remaining Kani module owners --- spec/spec.md | 4 ++++ 1 file changed, 4 insertions(+) diff --git a/spec/spec.md b/spec/spec.md index 39841c9aa..b87a57563 100644 --- a/spec/spec.md +++ b/spec/spec.md @@ -128,12 +128,16 @@ 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, validated `HarnessSpec`, and renderer are live for scalar and admitted V2 clause paths; collection and remaining families still need their AD-004 ports. | +| `kani/generate/{collection,clause/v2}` | FR-015, including V2 clause and symbolic collection criteria | V2 clause and collection lowerers are live; collection still renders its own template pending AD-004 step 4h and FR-015-AC-96/99 completion. | | `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 and corpus module entry remain until their last callers retire under AD-004 steps 4f/4g and FR-015-AC-110/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`, `kani/test_support`, and the `kani`, `generate`, `lower`, `run`, and `output` module roots | The FR-014/FR-015 criteria traced by the tests and the normative owners of each child module above | Test-only support and module declarations; they create no separate generation or run API. | | `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 From 64db98d6149c81b67829ca47e465ee10cb8fe4a0 Mon Sep 17 00:00:00 2001 From: Peter Krenesky Date: Sun, 25 Oct 2026 08:25:18 -0700 Subject: [PATCH 2/3] IR-329: disposition Kani ownership map review --- .../SR-57701-ir-329-pr577-spec-review-base.md | 45 +++++++++++++++++ ...7702-ir-329-pr577-spec-review-integrity.md | 48 +++++++++++++++++++ .../SR-57703-ir-329-pr577-spec-review-ears.md | 31 ++++++++++++ spec/spec.md | 11 +++-- 4 files changed, 131 insertions(+), 4 deletions(-) create mode 100644 reviews/SR-57701-ir-329-pr577-spec-review-base.md create mode 100644 reviews/SR-57702-ir-329-pr577-spec-review-integrity.md create mode 100644 reviews/SR-57703-ir-329-pr577-spec-review-ears.md diff --git a/reviews/SR-57701-ir-329-pr577-spec-review-base.md b/reviews/SR-57701-ir-329-pr577-spec-review-base.md new file mode 100644 index 000000000..5b3d5a81c --- /dev/null +++ b/reviews/SR-57701-ir-329-pr577-spec-review-base.md @@ -0,0 +1,45 @@ +--- +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 | diff --git a/reviews/SR-57702-ir-329-pr577-spec-review-integrity.md b/reviews/SR-57702-ir-329-pr577-spec-review-integrity.md new file mode 100644 index 000000000..b70d06953 --- /dev/null +++ b/reviews/SR-57702-ir-329-pr577-spec-review-integrity.md @@ -0,0 +1,48 @@ +--- +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 | diff --git a/reviews/SR-57703-ir-329-pr577-spec-review-ears.md b/reviews/SR-57703-ir-329-pr577-spec-review-ears.md new file mode 100644 index 000000000..80750930a --- /dev/null +++ b/reviews/SR-57703-ir-329-pr577-spec-review-ears.md @@ -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) | - | diff --git a/spec/spec.md b/spec/spec.md index b87a57563..2a9d62f3a 100644 --- a/spec/spec.md +++ b/spec/spec.md @@ -128,16 +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, validated `HarnessSpec`, and renderer are live for scalar and admitted V2 clause paths; collection and remaining families still need their AD-004 ports. | -| `kani/generate/{collection,clause/v2}` | FR-015, including V2 clause and symbolic collection criteria | V2 clause and collection lowerers are live; collection still renders its own template pending AD-004 step 4h and FR-015-AC-96/99 completion. | +| `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 and corpus module entry remain until their last callers retire under AD-004 steps 4f/4g and FR-015-AC-110/111. | +| `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`, `kani/test_support`, and the `kani`, `generate`, `lower`, `run`, and `output` module roots | The FR-014/FR-015 criteria traced by the tests and the normative owners of each child module above | Test-only support and module declarations; they create no separate generation or run API. | +| `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 From 1bc9d1d68c7558f35356e0d6cf998f4a706f4221 Mon Sep 17 00:00:00 2001 From: Peter Krenesky Date: Sun, 25 Oct 2026 08:33:18 -0700 Subject: [PATCH 3/3] IR-329: record clean spec review dispositions --- reviews/SR-57701-ir-329-pr577-spec-review-base.md | 9 +++++++++ .../SR-57702-ir-329-pr577-spec-review-integrity.md | 11 +++++++++++ 2 files changed, 20 insertions(+) diff --git a/reviews/SR-57701-ir-329-pr577-spec-review-base.md b/reviews/SR-57701-ir-329-pr577-spec-review-base.md index 5b3d5a81c..d02c0b9bf 100644 --- a/reviews/SR-57701-ir-329-pr577-spec-review-base.md +++ b/reviews/SR-57701-ir-329-pr577-spec-review-base.md @@ -43,3 +43,12 @@ changed. The diff adds no pin or SHA. `quire validate --scope . spec/spec.md` an | --- | --- | --- | --- | | 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`. | diff --git a/reviews/SR-57702-ir-329-pr577-spec-review-integrity.md b/reviews/SR-57702-ir-329-pr577-spec-review-integrity.md index b70d06953..b98762a1a 100644 --- a/reviews/SR-57702-ir-329-pr577-spec-review-integrity.md +++ b/reviews/SR-57702-ir-329-pr577-spec-review-integrity.md @@ -46,3 +46,14 @@ imprecise. | 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. |