Macro-emit reentrancy adversary holes and entrypoint registry (single-source rely-guarantee models)

[Th0rgal]

Problem

The rely-guarantee reentrancy framework (Verity/Core/Reentrancy.lean, worked example in Contracts/ReentrancyRelyGuarantee/Contract.lean) is sound, but using it today requires writing the contract twice:

1. the executable EDSL contract (verity_contract), and
2. a hand-written abstract model where every function that opens a reentrancy window is re-expressed with an adversary hole (adv : ContractState → ContractState) placed at the external call site, plus a hand-maintained entrypoints registry in the ReentrancySpec.

This duplication is also the source of two of the three author obligations recorded in TRUST_ASSUMPTIONS.md (§ Reentrancy Rely-Guarantee Framework):

• Registry completeness — entrypoints must list every state-mutating public function; omitting one makes schedule_preserves quantify over the wrong adversary.
• Hole placement fidelity — the adv hole must sit exactly where the real external call happens; today this correspondence is reviewed, not checked.

The hook for fixing this already exists: Env.reenter : ContractState → ContractState := id is declared in Verity/Core/Semantics.lean:24, but it is not wired into the external-call semantics or the elaborator — its declaration is currently its only reference.

Goal: write once

Make the verity_contract macro the single source of truth:

• Wire Env.reenter into the semantics of external calls (externalCallBind / the call lowering path), so that elaborated function bodies are automatically parameterized by the reentry hook at every real call site — i.e. the macro emits the reentrantCall env.reenter form instead of the author writing a parallel model.
• Emit the entrypoints registry automatically from the contract's actual public surface (non-view, state-mutating, externally dispatchable functions), so ReentrancySpec.entrypoints cannot silently under-approximate.
• Keep the default reenter := id so executable behavior and all existing proofs are unchanged when no adversary is instantiated.
• Update TRUST_ASSUMPTIONS.md: registry completeness and hole placement move from author obligations to macro-guaranteed properties (invariant adequacy remains the author's).
• Port Contracts/ReentrancyRelyGuarantee to consume the emitted form and delete the hand-written model.

Why priority

Until this lands, every rely-guarantee proof rests on the honor system for hole placement and registry completeness — precisely the parts a reviewer is worst at checking. Automating both closes the gap between "the theorem is kernel-checked" and "the theorem is about the contract you actually deployed", and removes the double-write cost that makes the framework expensive to adopt.

References

• Verity/Core/Reentrancy.lean — reentrantCall, ReentrancySpec, schedule_preserves
• Verity/Core/Invariant.lean — Preserves, runSeq, runSeq_preserves
• Verity/Core/Semantics.lean:24 — the unwired Env.reenter hook
• TRUST_ASSUMPTIONS.md — § Reentrancy Rely-Guarantee Framework (three author obligations)