feat(ceremony): re-land P0 enforcement-boundary module (Boundary.lean mirror)#245
Merged
Conversation
…ary.lean
Completes the P0 Rust kernel: alongside the authority algebra, the enforcement
boundary that carries the OCAP two-stream sequencing result into Rust. Mirrors
formal/Ceremony/P0/Boundary.lean:
- Fence { Advisory | Kernel } (ADR 0002 I9/I10 sandbox_kind — enforcement
strength, NOT a fourth Authority axis), Request { dynamic: bool }
- safe_subset / brush_honest / boundary_verdict: the L3-gated brush default
- boundary_ceiling / minted_grant: the fence bounds only Effect via the
frozen product meet — no new operation
Same discharge discipline as authority.rs: exhaustive over the finite domain.
7 tests, all green, mirroring the Lean theorems:
- fallback_is_forced (advisory brush verdict = safe_subset)
- boundary_verdict = honest brush verdict
- boundary_verdict = Effect::meet(Allow, ceiling) (attenuation, no new op)
- minted grant ≤ request and ≤ enforceable ceiling (I9 never-overclaim)
- advisory + dynamic ⇒ Deny on effect (fail closed, L3/I5)
- projection to Effect is a meet-homomorphism (proj_effect_meet — convergence)
The temporal half (fence dropping between grant and exec ⇒ re-check at exec,
spec I4) is not a pure-function property and stays in EnforcementGate.tla.
fmt + clippy (-D warnings) clean; 19 tests + doctest pass.
Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>
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.
Re-lands
boundary.rs— stranded when #241 merged early#241 was merged at the authority-kernel commit before the boundary push landed on its branch — so
agent-bridle-ceremony/src/boundary.rsnever reachedmain, even though #241's title says "+ enforcement-boundary". This restores it (cherry-pick of the originalc743a48).What it adds
The Rust mirror of
formal/Ceremony/P0/Boundary.lean— the OCAP two-stream sequencing result in the kernel crate:Fence { Advisory | Kernel }(ADR 0002 I9/I10sandbox_kind; enforcement strength, not a fourthAuthorityaxis),Request { dynamic }safe_subset/brush_honest/boundary_verdict— the L3-gated brush defaultboundary_ceiling/minted_grant— the fence bounds onlyEffectvia the frozen product meet7 exhaustive tests mirroring the Lean theorems:
fallback_is_forced, attenuation-is-not-a-new-op,minted ≤ request/≤ enforceable ceiling, advisory+dynamic ⇒Deny, and theproj_effect_meetconvergence check. (Crate now 19 tests + doctest.)Test plan
cargo test -p agent-bridle-ceremony→ 19 + doctest pass.Risk
Low — additive
boundary.rs+ 5-line re-export; already passed the gate on the #241 branch. Makes the merged #241 title accurate.Pairs with #244 (the refinement tier was extracted from a crate including this module).