fix: add unwind(4) to normalize Kani proofs (CI timeout)#266
Merged
brandon-coproduct merged 3 commits intomainfrom Mar 20, 2026
Merged
fix: add unwind(4) to normalize Kani proofs (CI timeout)#266brandon-coproduct merged 3 commits intomainfrom
brandon-coproduct merged 3 commits intomainfrom
Conversation
… Kani proofs These two harnesses were missing #[kani::unwind(4)], causing unbounded loop unwinding in BTreeSet<Operation> internals (alloc::btree::node:: correct_childrens_parent_links). This led to 339s symex, 61K VCCs, and CI timeout on the Kani (full) tier. The third normalize harness (normalize_monotone) already had unwind(4). Generated with [Claude Code](https://claude.ai/code) via [Happy](https://happy.engineering) Co-Authored-By: Claude <noreply@anthropic.com> Co-Authored-By: Happy <yesreply@happy.engineering>
Constitutional kernel proofs timed out at 20 min because all 11 harnesses run together, and BTreeSet construction in parent_policy() pulls in alloc::btree node machinery even for concrete data. Changes: - Split into fast tier (4 concrete-policy proofs, every PR, 15min) and full tier (all 11 including symbolic_set() proofs, nightly, 60min) - Add #[kani::unwind(5)] to the 4 fast-tier proofs to bound BTreeSet loop unrolling in CBMC Fast tier harnesses: proof_rejected_never_in_lineage proof_budget_escalation_always_rejected proof_constitutional_self_merge_impossible proof_identical_policy_config_patch_admitted Generated with [Claude Code](https://claude.ai/code) via [Happy](https://happy.engineering) Co-Authored-By: Claude <noreply@anthropic.com> Co-Authored-By: Happy <yesreply@happy.engineering>
… nightly Any proof touching admit() pulls in BTreeSet node machinery that takes >15 min in CBMC regardless of unwind bounds. Root cause is concrete BTreeSet construction in parent_policy(), not symbolic traversal. Solution: two-tier architecture. **Fast tier (every PR, <2 min):** 5 pure bitmask proofs that never import BTreeSet. Models set-valued axes as u8 bitmasks where subset is (child & !parent) == 0. Proves: - F1: Budget escalation detected (symbolic u64) - F2: Capability escalation biconditional (symbolic u8×6) - F3: I/O confinement biconditional (symbolic u8×5) - F4: Combined monotonicity = conjunction of axes - F5: Subset transitivity (lattice property) **Full tier (nightly, 60 min):** 11 proofs through admit() with bounded symbolic BTreeSets + unwind(5). Verifies the production code path including check_monotonicity, escalations_over, etc. Generated with [Claude Code](https://claude.ai/code) via [Happy](https://happy.engineering) Co-Authored-By: Claude <noreply@anthropic.com> Co-Authored-By: Happy <yesreply@happy.engineering>
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
1 participant
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
Summary
#[kani::unwind(4)]toproof_normalize_idempotentandproof_normalize_deflationaryproof_normalize_monotonealready had#[kani::unwind(4)]Root Cause
Without unwind bounds, Kani attempts unbounded loop unwinding through
BTreeSet<Operation>internals (alloc::btree::node::correct_childrens_parent_links). This produced:Test plan
feat/witness-enrichmentbranch where it was verifiedworkflow_dispatchof Kani BMC on this branch to verify full tier🤖 Generated with Claude Code
via Happy