docs: add Reentrancy Model explanation page (rely-guarantee framework)

[Th0rgal]

Summary

• New Explanation page docs-site/content/reentrancy.mdx documenting all four reentrancy mechanisms in one place: the fail-closed disposition gate, the nonreentrant(lock) runtime guard, reentrancy_trusted, and the ReentrancySpec rely-guarantee proof framework (adversary holes, schedule_preserves, nested reentry, the lock-as-disjunct strong/weak invariant layering, and the honest trust limits from TRUST_ASSUMPTIONS.md).
• Cross-links and touch-ups: _meta.js (new Explanation entry), edsl/functions.mdx (link from the disposition section), proof-techniques.mdx (fixes the outdated "reentrancy is not modeled via cross-call semantics" limitation note), trust-model.mdx (new bullet for the three rely-guarantee author obligations), glossary.mdx (new entries: Reentry schedule, Rely-guarantee (ReentrancySpec), Strong vs weak invariant).
• Docs-only change: no semantic/trust/CI boundary moves, so AUDIT.md / TRUST_ASSUMPTIONS.md / AXIOMS.md are untouched; the page links to them as the authoritative sources.

Related: #2094 (macro-emitted adversary holes + entrypoint registry), which the page and trust-model bullet reference as the planned mitigation for the registry-completeness and hole-placement obligations.

Validation

• make check — All checks passed (607 Python tests OK in 443.9s, docsync/macro-health/selector/path checks passed).
• cd docs-site && npm ci && npm run build — Next.js production build succeeded; Pagefind indexed 27 pages including the new /reentrancy page.

Test plan

• Preview the Vercel deploy: check /reentrancy renders, sidebar shows "Reentrancy Model" first under Explanation, and internal links (/edsl/functions#reentrancy-disposition, /trust-model, /glossary) resolve.
• Verify the GitHub source links (Reentrancy.lean, Invariant.lean, ReentrancyRelyGuarantee example, TRUST_ASSUMPTIONS.md) point at existing paths on main.

---

Note

Low Risk
Documentation-only changes with no runtime, compiler, or proof boundary impact.

Overview
Adds a new Explanation page at /reentrancy that documents Verity’s reentrancy story end-to-end: the fail-closed disposition gate, nonreentrant(lock), reentrancy_trusted, and the ReentrancySpec rely-guarantee proof path (adversary holes, schedule_preserves, lock-as-disjunct strong/weak layering, multi-contract schedules, and documented trust limits).

Navigation and cross-links: _meta.js lists Reentrancy Model under Explanation; edsl/functions, proof-techniques, trust-model, and glossary now point at the new page and refresh wording (e.g. proof-techniques no longer says reentrancy is unmodeled; trust-model adds rely-guarantee author obligations; glossary adds reentry schedule, rely-guarantee, strong vs weak invariant).

Docs-only — no compiler, proof, or trust-artifact changes.

^{Reviewed by Cursor Bugbot for commit c91952c. 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, Comment	Jul 4, 2026 6:24am

[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_c981255e-85a3-4665-87db-a651a7c06e5f)