formal(P0): mechanize the OCAP two-stream sequencing against the frozen algebra

formal/Ceremony.lean

@@ -1,2 +1,3 @@
 import Ceremony.P0.Authority
+import Ceremony.P0.Boundary
 import Ceremony.P1.SignedObject

formal/Ceremony/P0/Boundary.lean

@@ -0,0 +1,192 @@
+/-
+  Ceremony Suite — Enforcement boundary & the two-stream composition (P0)
+
+  Mechanizes the "OCAP two-stream sequencing" decision
+  (knowledge/board/2026-07-16_ocap-two-streams-sequencing-DECIDED.md) AGAINST
+  the frozen algebra of `Authority.lean`. It exists to answer one question with
+  a proof rather than prose:
+
+    Does deciding "brush-first / ceremony-in-parallel, L3-gated brush default,
+    fall back to safe-subset when no fence" VIOLATE the ratified v0.3.1 spec?
+
+  The load-bearing sub-decision under test (verbatim from the board note):
+
+    "Brush is the confined default WHERE an L3 fence is actively enforcing;
+     fall back to safe-subset's structural refusal when L3 is unavailable."
+
+  RESULT (what the theorems below establish):
+    • The L3-gate is NOT a new law and NOT a fourth Authority axis. It is the
+      existing `Effect` meet, driven by an *enforceable ceiling* the active
+      fence supplies (ADR 0002 I9/I10 "never overclaim"; only L3 sees inside a
+      spawned binary). `boundaryVerdict = attenuate desired (fence ceiling)`.
+    • The safe-subset fallback is FORCED, not a bolt-on policy: it is exactly
+      what the honest (non-overclaiming) brush verdict reduces to under
+      `advisory` (`fallback_is_forced`).
+    • Stream A (brush enforces `Caveats`) and Stream B (ceremony proves
+      `Authority`) COMPOSE: projection to the enforced carrier is a meet-
+      homomorphism (`proj_effect_meet`) — the ADR 0020 D7 "siblings, not two
+      competing models" claim, mechanized. So enforcement can never grant above
+      what the authority algebra permits; layered-parallel converges.
+
+  It imports only `Ceremony.P0.Authority` and introduces no new operation over
+  it. That IS the confirmation: the sequencing is *inside* the frozen system.
+
+  The temporal half — a fence that DROPS between grant and exec must not fail
+  open (spec I4, "checked at the moment it executes") — is modeled separately
+  in `formal/tla/EnforcementGate.tla`.
+-/
+import Ceremony.P0.Authority
+namespace Ceremony.P0
+
+/-! ### The enforcement fence — ADR 0002 I9/I10 `sandbox_kind`, NOT a new axis
+
+`Fence` is *enforcement strength* (is a kernel L3 fence active right now?), a
+distinct concept from the `Assurance` axis (how strongly the human is present).
+It is deliberately NOT lifted into `Authority` as a fourth coordinate: it does
+not decide *what/how-present/how-long*; it bounds only *what the boundary can
+faithfully enforce*, which lands on `Effect` via the meet below. -/
+inductive Fence
+  | advisory   -- NoopSandbox: L1/L2 cannot see inside a spawned binary (I10)
+  | kernel     -- Landlock / seatbelt / AppContainer actively confining
+deriving DecidableEq, Repr
+
+/-- A shell request, abstracted to the one bit the decision turns on: does it
+    use dynamic constructs (`$(…)`, pipes, `eval`) whose containment only a
+    kernel fence can provide? `dynamic = false` is structurally safe. -/
+structure Request where
+  dynamic : Bool
+deriving DecidableEq, Repr
+
+/-! ### The two engines -/
+
+/-- safe-subset engine: STRUCTURAL refusal of dynamic constructs — least
+    authority by construction, fence-independent (it never runs `$(…)`). -/
+def safeSubset (q : Request) : Effect :=
+  if q.dynamic then .deny else .allow
+
+/-- brush engine, stated as its *honest* verdict (ADR 0002 I9: never report an
+    advisory run as confined). Under `kernel` the op is confined ⇒ honest
+    `allow`. Under `advisory` a dynamic op cannot be confined, so running it and
+    calling it confined would OVERCLAIM ⇒ the honest verdict is `deny`
+    (fail-closed, I5/L3); a static op is structurally safe regardless. -/
+def brushHonest (f : Fence) (q : Request) : Effect :=
+  match f, q.dynamic with
+  | .kernel,   _     => .allow
+  | .advisory, true  => .deny
+  | .advisory, false => .allow
+
+/-- The DECIDED rule: brush is the default WHERE a kernel fence enforces; else
+    fall back to safe-subset's structural refusal. -/
+def boundaryVerdict (f : Fence) (q : Request) : Effect :=
+  match f with
+  | .kernel   => brushHonest .kernel q
+  | .advisory => safeSubset q
+
+/-! ### The board decision is exactly the honest brush verdict -/
+
+/-- **The safe-subset fallback is FORCED, not bolted on.** Under `advisory`, the
+    honest brush verdict *is* safe-subset's — so "fall back to safe-subset when
+    L3 is unavailable" is derived from the no-overclaim rule (I9), not an
+    independent policy knob. -/
+theorem fallback_is_forced (q : Request) :
+    brushHonest .advisory q = safeSubset q := by
+  rcases q with ⟨d⟩; cases d <;> rfl
+
+/-- The DECIDED rule and the honest brush verdict are the same function; the
+    "default + fallback" phrasing is one thing, not two. -/
+theorem boundaryVerdict_eq_honest (f : Fence) (q : Request) :
+    boundaryVerdict f q = brushHonest f q := by
+  cases f
+  · exact (fallback_is_forced q).symm   -- advisory: safeSubset = brushHonest advisory
+  · rfl                                  -- kernel: definitional
+
+/-! ### It is an attenuation in the FROZEN algebra — no new operation
+
+The user's desired effect is `allow` (they want to run the command). `allow` is
+the top of `Effect`, so meeting the desired effect with the fence's enforceable
+ceiling recovers exactly the verdict: the decision is `Effect.meet`, nothing
+new. -/
+
+/-- the enforceable-effect ceiling the fence supplies for this request. -/
+def enforceableCeiling (f : Fence) (q : Request) : Effect := boundaryVerdict f q
+
+theorem allow_is_effect_top (e : Effect) : Effect.meet .allow e = e := by
+  cases e <;> rfl
+
+/-- **The boundary decision is a meet.** It attenuates the desired `allow` by
+    the fence's enforceable ceiling — the frozen `Effect.meet`, no bespoke op. -/
+theorem boundaryVerdict_is_attenuation (f : Fence) (q : Request) :
+    boundaryVerdict f q = Effect.meet .allow (enforceableCeiling f q) := by
+  simp only [enforceableCeiling, allow_is_effect_top]
+
+/-! ### Lifted to `Authority`: the fence bounds ONLY `Effect`
+
+The boundary ceiling is `⊤` on Assurance and Scope (the fence says nothing about
+human presence or duration) and the enforceable effect on `Effect`. Minting a
+grant is `attenuate request boundaryCeiling` — the frozen product meet. -/
+
+/-- the fence ceiling as an `Authority`: enforceable on `Effect`, `⊤` elsewhere. -/
+def boundaryCeiling (f : Fence) (q : Request) : Authority :=
+  ⟨boundaryVerdict f q, .hardware, .durable⟩
+
+/-- what the gate actually mints: the request attenuated by the fence ceiling. -/
+def mintedGrant (req : Authority) (f : Fence) (q : Request) : Authority :=
+  attenuate req (boundaryCeiling f q)
+
+/-- **Never more than requested** — a direct corollary of `meet_le_left`. -/
+theorem minted_le_request (req : Authority) (f : Fence) (q : Request) :
+    mintedGrant req f q ≤ᴬ req :=
+  meet_le_left req (boundaryCeiling f q)
+
+/-- **Never above what the fence can enforce (I9, in the product).** The minted
+    authority is ⊑ the boundary ceiling on every axis — a corollary of
+    `meet_le_right`. An advisory boundary therefore cannot mint an
+    effect its fence would only *advise*. -/
+theorem minted_le_enforceable (req : Authority) (f : Fence) (q : Request) :
+    mintedGrant req f q ≤ᴬ boundaryCeiling f q :=
+  meet_le_right req (boundaryCeiling f q)
+
+/-- **Fail-closed on the unenforceable case (L3/I5).** A containment-needing
+    request under no kernel fence mints `deny` on the effect axis — the exact
+    structural refusal safe-subset gives, reached here through the meet, for
+    ANY request ceiling. This is the honesty guarantee the L3-gate rests on. -/
+theorem advisory_dynamic_grant_is_deny (req : Authority) (q : Request)
+    (h : q.dynamic = true) :
+    (mintedGrant req .advisory q).effect = Effect.deny := by
+  rcases req with ⟨e, a, s⟩
+  simp only [mintedGrant, attenuate, boundaryCeiling, boundaryVerdict, safeSubset,
+             h, Authority.meet, Effect.meet]
+  cases e <;> rfl
+
+/-! ### The two streams compose — projection is a meet-homomorphism (ADR 0020 D7)
+
+Stream A enforces the effect carrier (`Caveats`, ADR 0002 — bridle *depends on*
+it and MUST NOT reinvent it, I3). Stream B proves `Authority`. The projection
+`Authority.effect` carries the product meet to the axis meet definitionally, so
+whenever ceremony attenuates authority, the effect brush enforces attenuates in
+lockstep. Layered-parallel converges: enforcement is the ⊓-image of the proof,
+never a divergent second model. -/
+
+/-- **The convergence theorem.** Projection to the enforced carrier commutes
+    with the meet: `(a ⊓ b).effect = a.effect ⊓ b.effect`. Stream B's
+    attenuation, projected onto what Stream A enforces, *is* Stream A's
+    attenuation. -/
+theorem proj_effect_meet (a b : Authority) :
+    (a ⊓ b).effect = Effect.meet a.effect b.effect := rfl
+
+/-- Same homomorphism on the other two axes — the product really is
+    coordinatewise, so no axis can smuggle in amplification. -/
+theorem proj_assurance_meet (a b : Authority) :
+    (a ⊓ b).assurance = Assurance.meet a.assurance b.assurance := rfl
+theorem proj_scope_meet (a b : Authority) :
+    (a ⊓ b).scope = Scope.meet a.scope b.scope := rfl
+
+/-! ### Summary the gate can quote
+
+`boundaryVerdict = attenuate allow (fence ceiling)` (frozen meet), the fallback
+is forced by I9, minting never exceeds request or enforceable ceiling, dynamic-
+under-advisory fails closed, and enforcement is the meet-homomorphic image of
+the proven authority. No new law; no fourth axis. The sequencing lives INSIDE
+the v0.3.1 freeze. -/
+
+end Ceremony.P0

formal/README.md

@@ -17,10 +17,12 @@ it builds in seconds.
 | Path | Covers | Origin |
 |---|---|---|
 | `Ceremony/P0/Authority.lean` | **P0 authority algebra** — the product meet-lattice `Effect × Assurance × Scope`, attenuation (L4), no-fail-open (OB-9/OB-12), order-independence (L1). 25 theorems, 0 `sorry`. | P0 (this suite) |
+| `Ceremony/P0/Boundary.lean` | **the OCAP two-stream sequencing, mechanized** — the L3-gated brush default proven to be an `Effect` attenuation in the frozen algebra (no new law/axis); safe-subset fallback *forced* by I9; enforcement = meet-homomorphic image of authority (streams converge). Confirms the [DECIDED board note](../../../knowledge/board/2026-07-16_ocap-two-streams-sequencing-DECIDED.md). | P0 (this suite) |
 | `Ceremony/P1/SignedObject.lean` | **P1 signed-object contracts** — profile/algorithm allowlist (`TrustedProfile`), canonical encoding injectivity, the universal `SignaturePreimage` binding profile/codec/domain/store/thread/body/cid/signer (OB-13), genesis. | PR #233 (GPT-5/Codex) |
 | `Gate.lean` + `formalGate` exe | the proof-escape gate: rejects `sorry` / omitted modules. | PR #233 |
 | `Tests/P1Counterexamples.lean`, `Tests/SignedObjectContracts.lean` | negative + contract tests (Lean-level conformance). | PR #233 |
 | `tla/CeremonyStore.tla` | **P2 store** — CAS append + anti-rollback state machine; invariants map to PO-2/2a/2c + OB-15/16. Check with TLC. | P2 (this suite) |
+| `tla/EnforcementGate.tla` | **the L3-gate under a fence that DROPS over time** — temporal half of `Boundary.lean`. `NoAdvisoryDynamicExec` holds iff the fence is re-checked at exec (I4). TLC PASSES with `CheckAtExec=TRUE`, exhibits the TOCTOU trace with `FALSE` (two `.cfg`s next to it). | P0 (this suite) |
 
 ## Why this shape
 

formal/tla/.gitignore

@@ -0,0 +1,5 @@
+# TLC model-checker run artifacts (scratch)
+states/
+*_TTrace_*.tla
+*_TTrace_*.bin
+*.st

formal/tla/EnforcementGate.tla

@@ -0,0 +1,98 @@
+-------------------------- MODULE EnforcementGate --------------------------
+(*
+  Ceremony Suite — the L3-gate under a fence that CHANGES over time (P0).
+  Temporal companion to formal/Ceremony/P0/Boundary.lean, which proves the
+  *static* case (the L3-gated brush default is an attenuation in the frozen
+  algebra, no new law/axis). This module discharges the one genuinely-new
+  obligation the sequencing decision introduces:
+
+    the "OCAP two-stream sequencing" board note makes brush the confined
+    default WHERE a kernel fence is active. But a fence can DROP between the
+    moment a dynamic op is authorized and the moment it executes (kernel
+    module unload, container reconfig, policy change). Spec I4 requires the
+    check "at the moment it executes" — NOT cached from grant time.
+
+  The model makes that requirement falsifiable. `CheckAtExec` toggles the two
+  designs:
+
+    CheckAtExec = TRUE   -> re-check the CURRENT fence at exec (I4-faithful).
+    CheckAtExec = FALSE  -> trust the fence observed at grant time (the bug).
+
+  Invariant NoAdvisoryDynamicExec: no containment-needing op ever actually runs
+  while the fence is advisory (I9 "never overclaim" / I5 fail-closed, over
+  time). TLC result:
+
+    CheckAtExec = TRUE   -> []Inv holds (the sequencing is safe).
+    CheckAtExec = FALSE  -> TLC exhibits the fence-drop TOCTOU counterexample
+                            (authorize under kernel -> FenceDown -> Exec runs
+                            advisory). This is the design the gate must NOT use.
+
+  So: the L3-gated brush default is spec-faithful IFF enforcement re-checks the
+  fence at exec. That conditional IS the confirmation — and names the exact
+  thing Stream A must implement.
+*)
+EXTENDS Naturals
+
+CONSTANT CheckAtExec           \* TRUE = I4-faithful (re-check at exec); FALSE = cache grant-time fence
+
+VARIABLES
+  fence,                       \* "advisory" | "kernel" : the CURRENT enforcement strength
+  grantFence,                  \* "none" | "advisory" | "kernel" : fence seen when the pending dynamic op was authorized
+  advisoryDynamicRan           \* BOOLEAN : did a containment-needing op ever actually run under an advisory fence?
+
+vars == << fence, grantFence, advisoryDynamicRan >>
+
+Fences == { "advisory", "kernel" }
+
+TypeOK ==
+  /\ fence \in Fences
+  /\ grantFence \in (Fences \cup { "none" })
+  /\ advisoryDynamicRan \in BOOLEAN
+
+Init ==
+  /\ fence \in Fences
+  /\ grantFence = "none"
+  /\ advisoryDynamicRan = FALSE
+
+\* The fence strength can change under our feet at any time.
+FenceDown == fence = "kernel"   /\ fence' = "advisory" /\ UNCHANGED << grantFence, advisoryDynamicRan >>
+FenceUp   == fence = "advisory" /\ fence' = "kernel"   /\ UNCHANGED << grantFence, advisoryDynamicRan >>
+
+\* Authorize a containment-needing (dynamic) op. Per the L3-gate, a dynamic op
+\* is authorized only where a kernel fence is currently active; we record the
+\* fence observed at grant time.
+AuthorizeDynamic ==
+  /\ grantFence = "none"
+  /\ fence = "kernel"
+  /\ grantFence' = fence
+  /\ UNCHANGED << fence, advisoryDynamicRan >>
+
+\* Execute the pending dynamic op. The gate consults either the current fence
+\* (I4-faithful) or the cached grant-time fence (the bug), per CheckAtExec. It
+\* proceeds only if that fence reads "kernel". `advisoryDynamicRan` records what
+\* ACTUALLY happened at the kernel — which depends on the CURRENT fence, not the
+\* one the gate consulted.
+ExecDynamic ==
+  /\ grantFence # "none"
+  /\ LET checked == IF CheckAtExec THEN fence ELSE grantFence
+     IN  checked = "kernel"                               \* the gate lets it through
+  /\ advisoryDynamicRan' = (advisoryDynamicRan \/ (fence = "advisory"))
+  /\ grantFence' = "none"
+  /\ UNCHANGED fence
+
+Next == FenceDown \/ FenceUp \/ AuthorizeDynamic \/ ExecDynamic
+
+Spec == Init /\ [][Next]_vars
+
+------------------------------------------------------------------------------
+\* Invariant: a containment-needing op never actually runs advisory (I9/I5 over
+\* time). Holds under CheckAtExec = TRUE; TLC finds a counterexample under FALSE.
+NoAdvisoryDynamicExec == advisoryDynamicRan = FALSE
+
+Inv == TypeOK /\ NoAdvisoryDynamicExec
+
+\* Config: to see it PASS, run with CheckAtExec <- TRUE and check Inv.
+\* To see the TOCTOU bug, run with CheckAtExec <- FALSE (Inv will fail with a
+\* trace: AuthorizeDynamic; FenceDown; ExecDynamic).
+THEOREM SafeWhenCheckedAtExec == (CheckAtExec = TRUE) => (Spec => []Inv)
+=============================================================================

formal/tla/EnforcementGate_cacheGrantFence.cfg

@@ -0,0 +1,7 @@
+\* THE BUG: trust the fence observed at grant time. TLC MUST report a violation
+\* of NoAdvisoryDynamicExec (trace: AuthorizeDynamic; FenceDown; ExecDynamic).
+\* This is the design Stream A must NOT ship; it documents the obligation.
+\* Run:  java -cp tla2tools.jar tlc2.TLC -config EnforcementGate_cacheGrantFence.cfg EnforcementGate.tla
+SPECIFICATION Spec
+CONSTANT CheckAtExec = FALSE
+INVARIANT Inv

formal/tla/EnforcementGate_checkAtExec.cfg

@@ -0,0 +1,5 @@
+\* I4-FAITHFUL: re-check the current fence at exec time. Inv MUST hold.
+\* Run:  java -cp tla2tools.jar tlc2.TLC -config EnforcementGate_checkAtExec.cfg EnforcementGate.tla
+SPECIFICATION Spec
+CONSTANT CheckAtExec = TRUE
+INVARIANT Inv