formal(P0): mechanize the OCAP two-stream sequencing against the frozen algebra#239
Merged
Merged
Conversation
…en algebra
The two-stream sequencing decision (brush-first / ceremony-in-parallel, L3-gated
brush default, safe-subset fallback) was a prose plan-of-record. This proves it
does not violate the ratified v0.3.1 spec -- by showing it is DERIVABLE INSIDE
the frozen algebra, adding no new law and no fourth axis.
Ceremony/P0/Boundary.lean (imports only Authority.lean; lake build 10 jobs, 0
sorry, formalGate clean):
- boundaryVerdict_is_attenuation: the L3-gated decision is Effect.meet of the
desired allow with the fence's enforceable ceiling -- the frozen meet, not a
bespoke operation.
- fallback_is_forced: the safe-subset fallback under `advisory` IS the honest
(non-overclaiming) brush verdict; it is derived from ADR 0002 I9, not a
separate policy knob.
- minted_le_request / minted_le_enforceable: a minted grant never exceeds the
request or what the fence can enforce (I9 "never overclaim", via meet_le_*).
- advisory_dynamic_grant_is_deny: a containment-needing op under no kernel
fence fails closed on Effect (L3/I5), for any request ceiling.
- proj_effect_meet (+ assurance/scope): projection to the enforced carrier is
a meet-homomorphism -- the ADR 0020 D7 "siblings, not two competing models"
claim, mechanized. Stream A (brush/Caveats) enforces the meet-image of what
Stream B (ceremony/Authority) proves, so layered-parallel CONVERGES.
tla/EnforcementGate.tla (+ two .cfg): the temporal half -- a fence that DROPS
between grant and exec. NoAdvisoryDynamicExec (I9/I5 over time) holds iff the
gate re-checks the fence at exec (spec I4). TLC verified both ways:
- CheckAtExec=TRUE -> "No error has been found" (4 distinct states).
- CheckAtExec=FALSE -> Inv violated; trace AuthorizeDynamic; FenceDown;
ExecDynamic ends advisoryDynamicRan=TRUE. The design Stream A must NOT ship.
Net: the sequencing is spec-faithful, and it is spec-faithful IFF Stream A
re-checks the active fence at exec -- which names the exact obligation the brush
default carries. Records the confirmation next to the proofs; formal/README
updated; TLC scratch artifacts gitignored.
Refs: knowledge/board/2026-07-16_ocap-two-streams-sequencing-DECIDED.md,
ADR 0002 (Caveats I3/I9/I10), ADR 0020 (Authority product lattice, D7).
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.
Confirms the two-stream sequencing does not violate the v0.3.1 spec
The OCAP two-stream sequencing decision (brush-first / ceremony-in-parallel, L3-gated brush default, safe-subset fallback) was a prose plan-of-record. This proves it is derivable inside the frozen algebra — no new law, no fourth axis — rather than merely asserting compatibility.
Lean —
formal/Ceremony/P0/Boundary.leanImports only
Authority.lean.lake build→ 10 jobs, 0sorry;formalGateclean.boundaryVerdict_is_attenuation— the L3-gated decision isEffect.meetof the desiredallowwith the fence's enforceable ceiling. The frozen operation, not a bespoke one. The fence is enforcement strength (ADR 0002 I9sandbox_kind), deliberately not a fourthAuthorityaxis — it lands onEffectvia the existing meet.fallback_is_forced— the safe-subset fallback underadvisoryis the honest (non-overclaiming) brush verdict. Forced by I9, derived, not a separate policy knob.minted_le_request/minted_le_enforceable— a grant never exceeds the request or what the fence can enforce (I9 "never overclaim"), frommeet_le_*.advisory_dynamic_grant_is_deny— containment-needing op with no kernel fence fails closed onEffect(L3/I5), for any ceiling.proj_effect_meet— the convergence proof. Projection to the carrier brush enforces (Caveats) is a meet-homomorphism: Stream A enforces the ⊓-image of what Stream B proves. Layered-parallel converges (ADR 0020 D7 "siblings, not competitors", mechanized), conditional on brush not reinventingCaveats(ADR 0002 I3).TLA+ —
formal/tla/EnforcementGate.tla(+ two.cfg)The one genuinely-new obligation: a fence can drop between grant and exec. TLC-checked both ways:
CheckAtExec = TRUE(re-check at exec, spec I4) → No error found (4 distinct states).CheckAtExec = FALSE(cache grant-time fence) → Inv violated; TOCTOU traceAuthorizeDynamic; FenceDown; ExecDynamic→advisoryDynamicRan = TRUE.Conclusion: the L3-gated brush default is spec-faithful iff enforcement re-checks the active fence at exec — which names the exact obligation for Stream A (newt#1243 Leg 1): the brush gate must not cache grant-time fence state.
Test plan
just check-formal→lake build(10 jobs) +formalGate, exit 0.tla2toolslocally): PASS withcheckAtExec, VIOLATION-with-trace withcacheGrantFence.[pre-push] OK).Risk
Low — additive to
formal/+ one README row; touches no Rust, no CI/build config, deletes nothing. TLC scratch artifacts gitignored.Refs: ADR 0002 (Caveats I3/I9/I10), ADR 0020 (Authority product lattice, D7), the DECIDED board note.