feat(model): proved source semantics for nonreentrant(lock) (lane 2.2 step 1)

[Th0rgal]

First step of lane 2.2: Verity.Core.Model.NonReentrantGuard.guarded — executable source semantics of the compiled transient-lock prologue (attachNonReentrantGuard), with the guard laws proved:

• guarded_locked_reverts / guarded_reentry_blocked: lock held ⇒ revert, state untouched; identity as a state transformer.
• guarded_free_runs_body + body_observes_lock + guarded_success_releases: lock free ⇒ body runs under an observably set lock, successful exits release it (same-tx sequential calls stay allowed), reverting exits roll back the acquire.
• runSeq_guarded_locked_id: whole reentry schedules of same-lock guarded entrypoints collapse to the identity on locked states — closes the reentry window at schedule level, composing with CallbackBounded (feat(model): callback-bounded adversaries — reentrancy specs at the call boundary (#1963 slice 6) #2260).

Still open (documented in TRUST_ASSUMPTIONS.md): guarded ↔ emitted-Yul correspondence, and lifting the supported-fragment noNonReentrant restriction.

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

---

Note

Medium Risk
Touches the security-critical reentrancy model, but is additive Lean proof infrastructure with no compiler or runtime emission changes. Correspondence to emitted Yul remains an open trust boundary.

Overview
Adds proved source-level semantics for the compiled nonreentrant(lock) transient-storage guard via new Verity.Core.Model.NonReentrantGuard.guarded.

When the lock is free, the body runs under an observably set lock and successful exits release it (reverts roll back the acquire). When held, same-lock guarded entrypoints revert with state unchanged — so whole reentry schedules collapse to the identity (runSeq_guarded_locked_id), closing the reentry window at the model level and composing with CallbackBounded / ReentrancySpec.

Updates TRUST_ASSUMPTIONS.md accordingly. Still trusted: correspondence of guarded to Yul from attachNonReentrantGuard, and the supported-fragment noNonReentrant restriction.

^{Reviewed by Cursor Bugbot for commit 29211e8. 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 11:56am

[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_eacee24a-539b-4f1f-b866-e04f2b41d0f5)

[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.