Skip to content

IR-881: consume Kani checker absence code - #484

Merged
kreneskyp merged 7 commits into
mainfrom
code/ir881-cg-checker-absent
Oct 21, 2026
Merged

kreneskyp merged 7 commits into
mainfrom
code/ir881-cg-checker-absent

Conversation

@kreneskyp

@kreneskyp kreneskyp commented Oct 21, 2026 •

Copy link
Copy Markdown
Contributor

IR-881 CG consumer

Contract IR merged the STD-001 rename to kani_checker_absent. This PR updates CG's terminal map and owning spec to consume that name without an alias. UnavailabilityCause::SolverAbsent remains CG's distinct terminal settlement; the registered IR code and every reference to its former spelling are replaced.

The lockfile changes only quire-contract-ir and quire-contract-model to the same merged source revision. The selective Cargo update initially refreshed four unrelated transitive Git crates; each was restored through cargo update --precise. The RT revision remains 3cc88c48, and filament-core-data is unchanged.

Verification

  • Spec-first, then red-test commits: the focused TC-041 test failed compilation because the old IR lock lacked KANI_CHECKER_ABSENT.
  • Implementation commit: focused TC-041 test passed against the selectively updated IR lock.
  • Mutation control: temporarily mapped KANI_BACKEND_ABSENT in the checker arm. TC-041 failed with Unsupported(BackendAbsent) instead of Unsupported(SolverAbsent); source restored and the worktree is clean.
  • Pre-PR RUST_TEST_THREADS=1 QSPEC_DIR=/home/peter/dev/quire-specification make ci passed on exact head 3f06f98f: both MSRV and regular passes completed 378 unit, 665 integration and 16 doc tests. The real Kani gate passed 37/37 with a clean tree, and make cargo-audit passed with one allowed yanked-crate warning. The serial setting avoids a separately tracked stand-in startup ceiling flake observed under parallel full-suite load; its isolated test also passed.

Independent code/Rust, gap and spec review is required before merge. Final full gates will run again on the reviewed head.

@kreneskyp
kreneskyp force-pushed the code/ir881-cg-checker-absent branch from 3f06f98 to ab01e5e Compare October 21, 2026 05:55
kreneskyp and others added 2 commits October 20, 2026 23:03
@kreneskyp
kreneskyp merged commit 8ac09bc into main Oct 21, 2026
3 checks passed
@kreneskyp
kreneskyp deleted the code/ir881-cg-checker-absent branch October 21, 2026 13:13
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

None yet

Projects

None yet

Development

Successfully merging this pull request may close these issues.

1 participant