proof(ir): end-to-end guarded unit (lane 2.2 milestone)

[Th0rgal]

The lane's IR-side capstone: execIRStmts_guardedUnit_fallthrough/_halting compose the prologue laws (#2274/#2275) with both wrapper branches (#2292/#2293), proving the compiled guarded unit mirrors Verity.Core.Model.NonReentrantGuard.guarded exactly over the SpliceSim fragment: locked entry ⇒ revert untouched; free entry ⇒ body runs from the acquired state, successful outcomes released, reverts roll back the acquire.

TRUST_ASSUMPTIONS.md updated — remaining trusted: switch/loop guarded bodies, the invalid/selfdestruct halt-analysis gap, and the compile_preserves_semantics threading for the noNonReentrant lift.

Validation: full lake build OK, make check all passed, no sorry/admit/new axiom.

---

Note

Low Risk
Proof-only additions and documentation; no runtime compiler or auth changes.

Overview
Adds execIRStmts_guardedUnit_fallthrough and execIRStmts_guardedUnit_halting in SpliceSimulation.lean, showing that guardPrologueStmts plus applyLockReleaseOnExits on the IR interpreter matches NonReentrantGuard.guarded: lock held ⇒ revert with unchanged state; lock free ⇒ body runs after acquire and successful exits release the lock.

Each proof is a short case split on lock 0/1, wiring guardedBody_locked_reverts / guardedBody_free_runs_suffix to the existing applyLockReleaseOnExits fall-through and modeled-halt lemmas.

PrintAxioms.lean registers the two new theorems (6237 → 6239 total). TRUST_ASSUMPTIONS.md records that the loop/switch-free guarded unit is now proved end-to-end and narrows what remains trusted (switch/loops, ModeledHalt gap, compile_preserves_semantics / noNonReentrant lift).

^{Reviewed by Cursor Bugbot for commit 0e38d1d. Bugbot is set up for automated code reviews on this repo. Configure here.}

[vercel]

The latest updates on your projects. Learn more about Vercel for GitHub.

Project	Deployment	Actions	Updated (UTC)
verity	Ready	Preview	Aug 12, 2026 4:20pm

[cursor]

Bugbot couldn't run - usage limit reached

Bugbot is counted against Cursor usage for this user or team, and this run hit a usage or spend limit.

A user or team admin can review and increase usage limits in the Cursor dashboard.

(requestId: serverGenReqId_ee37d648-d4d1-45ce-bbe5-3cd219495f49)

[github-actions]

OpenCodeReview first-pass review

⚪ OCR did not run — this diff has no OCR-supported files. Not a review outcome.

No changed files matched OCR include rules.

OCR pilot metrics & packet coverage

OCR pilot metrics

• Routing: no-supported (router-v10)
• Changed files: 0 supported / 0 total; Lean 0, trust docs 0, workflow/scripts 0, contracts 0, docs 0
• Changed lines: 0 supported; thresholds large Lean >=3 files or >800 lines
• OCR: status no-supported; comments 0; files 0; tokens 0; tool calls 0; warnings 0; duration 0s

Pilot mode: advisory only. Codex Review remains the merge gate.