docs: add module-level rustdoc to ck-policy#267
Closed
brandon-coproduct wants to merge 10 commits intomainfrom
Closed
docs: add module-level rustdoc to ck-policy#267brandon-coproduct wants to merge 10 commits intomainfrom
brandon-coproduct wants to merge 10 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>
Defines the invariant rules that AI-generated changes must preserve: Classification: Config — docs, tests, examples (auto-admittable) Controller — ck-kernel, portcullis, nucleus (requires Kani) Evaluator — ck-policy, ck-types (requires build + tests) Constitutional — this file, kani.rs proofs, LICENSE (human sigs) Invariants: - Capabilities cannot escalate (monotone) - I/O surface cannot widen (monotone) - Proof requirements cannot weaken (monotone) - Constitutional files require 1 human signature Protected paths (may_not_modify without constitutional amendment): - PolicyManifest.toml - crates/ck-kernel/src/kani.rs (48 Kani proofs) - crates/portcullis/src/kani.rs - LICENSE, SECURITY.md Co-Authored-By: Claude Opus 4.6 (1M context) <noreply@anthropic.com>
Constitutional Gate: RejectedPatch class: Config Reasons:
|
Constitutional Gate: RejectedPatch class: Config Reasons:
|
This PR needs changes before it can be mergedThis PR was classified as a Config change but couldn't be admitted.
What is this? Your repo has a Constitutional Gate · What is this? · Edit policy |
This PR needs changes before it can be mergedThis PR was classified as a Config change but couldn't be admitted. Bounded Termination
What is this? Your repo has a Constitutional Gate · What is this? · Edit policy |
Contributor
Author
|
Superseded by #269 (clean PolicyManifest bootstrap). |
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.
Add module-level documentation to
ck-policy/src/lib.rsexplainingthe monotonicity checker and the four constitutional invariants.
This is a Config-class change (documentation only) — the constitutional
gate should admit it automatically.
Testing the constitutional merge gate.