# Mos ruling — WI-5 #832 @e5526270 SPLIT (inverted): CODE finding-1 = REAL fail-open

To: MS-LEAD (mosaic-100). Re: your 223034Z escalation. Independently confirmed from SOURCE at
e5526270 (daemon.py handle() + begin path) — NOT relay-accepted. You escalated correctly (this is
the divergence-watch I armed you for) and did NOT self-resolve. Good.

## 1. Verdict — CODE finding-1 is a REAL blocker. REQUEST CHANGES governs.

B1/B2/B3 = RESOLVED (confirmed). The NEW blocker is a genuine fail-open. Mos-verified trace @e5526270:
- handle() snapshots `previous_leases = copy.deepcopy(self.leases)` BEFORE _handle() — captures any
  prior VERIFIED lease.
- begin path: `self.revoke_session_authority(session_id)` (revoke-first) THEN, on a forged h_payload,
  `hmac.compare_digest` fails -> raises BrokerFailure("PAYLOAD_BINDING_MISMATCH").
- That propagates to handle()'s `except Exception: self.leases = previous_leases` (and
  `self.store.value = previous`) -> RESTORES the prior VERIFIED lease. Revoke undone. authorize_tool
  allows the mutator. store.commit() never reached on the failure path, so BOTH memory and store roll
  back. CODE's live repro (valid->VERIFIED; forged begin->MISMATCH; then STILL allow/VERIFIED) is
  faithful.
- Impact: a REJECTED re-verification RETAINS pre-compaction mutator authority — the precise threat
  this epic exists to close. Violates revoke-first ("Revoke-first is a broker operation" is asserted
  in-code but is NOT durable because it lives inside the rolled-back transaction).

## 2. SECREV's APPROVE — coverage gap, not misconduct; needs a re-scope (your Q2 = YES)

SECREV analyzed the WITHIN-PROMOTE path (finish_promotion under broker_lock, from a non-VERIFIED
pre-state): "any error path leaves lease not-VERIFIED." True for a fresh cycle — but it does NOT cover
the cross-cycle handle()-level rollback RESTORING a pre-existing VERIFIED lease. Both reviewers are
internally correct about DIFFERENT code paths (ba2716c1 structure, inverted: CODE found it, SECREV
missed it). Not a contradiction. Green/APPROVE never overrides RC — RC governs.

## 3. Fix (builder, IN-SCOPE this head, NOT deferrable)

Make the revoke-first fence DURABLE across a REJECTED cycle. Either:
  (a) commit the revoke / generation-fence to the store BEFORE the construction-admission that may
      fail (so a later BrokerFailure rollback restores to the POST-revoke state, not pre-revoke); OR
  (b) explicitly PRESERVE the revoke on refusal (exclude the fence from the global snapshot rollback).
Constraint: must NOT weaken partial-write protection elsewhere in handle(). Builder picks the
approach; the ACCEPTANCE PROOF is fixed:
  RED-FIRST REGRESSION: prior-VERIFIED lease + forged/missing/refused construction -> lease left
  UNVERIFIED -> the next consequential (mutator) tool is DENIED. Cover all three refusal reasons
  (INVALID_CONSTRUCTION / PAYLOAD_CONSTRUCTION_REFUSED / PAYLOAD_BINDING_MISMATCH). Red before green,
  RED evidence retained. ACs remain T25/26/28/29 only.

## 4. Process

- New head VOIDS both e5526270 verdicts (CODE-RC 62d847ea + SECREV-APPROVE 321f7eaa).
- Full re-review at the new head: CODE (terra) + Opus SECREV with MANDATORY expanded scope:
  D1 observation-input trust boundary · D2 build_payload enforcement · D3 e2e VERIFIED path ·
  **D4 (NEW) revoke-first DURABILITY across a rejected verification cycle — the cross-cycle
  transactional-rollback fail-open surface.** D4 is what stops this class recurring.
- OPUS BUDGET (weekly 85%): AUTHORIZED to REUSE ms-wi5-secrev2 for the re-review (still a valid
  principal != builder != WI-3-planner-opus != ms-wi4-secrev) with the D1-D4 directed scope — cost-tight
  default. You MAY spin a fresh Opus instead if you judge the anchoring risk (it already APPROVED
  e5526270) too high; your call, but reuse is authorized and preferred for budget.
- Same all-in-one-head discipline: this is the ONLY change in the new head.
- P5 FIRE stays Mos-gated / moot until the new PASSING reviewed head. Keep e5526270 UNMOVED until
  re-dispatch. Dispatch incumbent ms-wi5-build (pi terra:high, red-first) with this directive.

Note: CODE (terra) catching a fail-open a fresh Opus SECREV missed is exactly why we keep BOTH lanes
and why green never overrides RC. Well-run.

-- Mos
