diff --git a/.github/workflows/verify.yml b/.github/workflows/verify.yml
index 6c5a830a3..da133dca1 100644
--- a/.github/workflows/verify.yml
+++ b/.github/workflows/verify.yml
@@ -11,6 +11,7 @@ on:
       - '.github/workflows/**'
       - '.github/workflows/verify.yml'
       - 'artifacts/**'
+      - 'artifacts/*'
       - 'Verity/**'
       - 'Verity.lean'
       - 'Compiler/**'
@@ -28,6 +29,7 @@ on:
       - 'lean-toolchain'
       - 'foundry.toml'
       - 'Makefile'
+      - 'PrintAxioms.lean'
       - 'README.md'
   pull_request:
     types: [opened, synchronize, reopened, closed]
@@ -37,6 +39,7 @@ on:
       - '.github/workflows/**'
       - '.github/workflows/verify.yml'
       - 'artifacts/**'
+      - 'artifacts/*'
       - 'Verity/**'
       - 'Verity.lean'
       - 'Compiler/**'
@@ -54,6 +57,7 @@ on:
       - 'lean-toolchain'
       - 'foundry.toml'
       - 'Makefile'
+      - 'PrintAxioms.lean'
       - 'README.md'
   workflow_dispatch:
     inputs:
@@ -324,6 +328,7 @@ jobs:
           python3 scripts/generate_evmyullean_capability_report.py
           python3 scripts/generate_evmyullean_native_lowering_report.py
           python3 scripts/generate_print_axioms.py
+          python3 scripts/generate_trust_surface_report.py
           python3 scripts/sync_verification_status_doc.py
 
       - name: Auto-commit refreshed artifacts
diff --git a/Compiler/CompilationModel/Dispatch.lean b/Compiler/CompilationModel/Dispatch.lean
index 8bd89a6bd..370bf0958 100644
--- a/Compiler/CompilationModel/Dispatch.lean
+++ b/Compiler/CompilationModel/Dispatch.lean
@@ -205,7 +205,7 @@ def compileFunctionSpec (fields : List Field) (events : List EventDef) (errors :
 
     The emitted Yul is:
     ```yul
-    if eq(tload(<lockSlot>), 1) { revert(0, 0) }
+    if tload(<lockSlot>) { revert(0, 0) }
     tstore(<lockSlot>, 1)
     ```
 
@@ -224,7 +224,7 @@ def nonReentrantGuardPrologue (fields : List Field) (lockField : String) :
       let lockSlot := YulExpr.lit slot
       let revertOnReentry :=
         YulStmt.if_
-          (YulExpr.call "eq" [YulExpr.call "tload" [lockSlot], YulExpr.lit 1])
+          (YulExpr.call "tload" [lockSlot])
           [YulStmt.exprStmt (YulExpr.call "revert" [YulExpr.lit 0, YulExpr.lit 0])]
       let acquire :=
         YulStmt.exprStmt (YulExpr.call "tstore" [lockSlot, YulExpr.lit 1])
diff --git a/Compiler/Proofs/IRGeneration/NonReentrantGuardIR.lean b/Compiler/Proofs/IRGeneration/NonReentrantGuardIR.lean
index 3a5729f4f..a3ff24130 100644
--- a/Compiler/Proofs/IRGeneration/NonReentrantGuardIR.lean
+++ b/Compiler/Proofs/IRGeneration/NonReentrantGuardIR.lean
@@ -9,12 +9,12 @@ First machine-checked brick of the `guarded` ↔ emitted-Yul correspondence
 `Compiler.CompilationModel.nonReentrantGuardPrologue` are evaluated under the
 IR interpreter used by the IR-generation proofs.
 
-- lock slot reads `1` → the frame reverts with the state untouched;
+- lock slot reads nonzero → the frame reverts with the state untouched;
 - lock slot reads `0` → execution falls through with the lock set to `1` and
   nothing else changed;
 - the release statement spliced by `applyLockReleaseOnExits` resets the slot;
-- on the reachable (binary) lock values, the Yul decision `eq(tload(slot), 1)`
-  agrees with the source-model decision `lock ≠ 0` of
+- the Yul decision on `tload(slot)` agrees with the source-model decision
+  `lock ≠ 0` of
   `Verity.Core.Model.NonReentrantGuard.guarded`.
 
 Still open: pushing these statement-level facts through
@@ -29,7 +29,7 @@ open Compiler.CompilationModel
 
 /-- The exact prologue shape emitted for a resolved lock slot. -/
 def guardPrologueStmts (slot : Nat) : List YulStmt :=
-  [ .if_ (.call "eq" [.call "tload" [.lit slot], .lit 1])
+  [ .if_ (.call "tload" [.lit slot])
       [.exprStmt (.call "revert" [.lit 0, .lit 0])],
     .exprStmt (.call "tstore" [.lit slot, .lit 1]) ]
 
@@ -45,22 +45,20 @@ theorem nonReentrantGuardPrologue_eq (fields : List Field) (lockField : String)
     nonReentrantGuardPrologue fields lockField = .ok (guardPrologueStmts slot) := by
   simp [nonReentrantGuardPrologue, h, guardPrologueStmts, pure, Except.pure]
 
-/-- Lock held (`tload = 1`) → the prologue reverts and the state is untouched. -/
+/-- Lock held (`tload ≠ 0`) → the prologue reverts and the state is untouched. -/
 theorem execIRStmts_guardPrologue_locked (fuel : Nat) (state : IRState) (slot : Nat)
     (hslot : slot < Compiler.Constants.evmModulus)
-    (hlock : state.transientStorage slot = 1) :
+    (hlock : state.transientStorage slot ≠ 0) :
     execIRStmts (fuel + 3) state (guardPrologueStmts slot) = .revert state := by
   have hmod : slot % Compiler.Constants.evmModulus = slot := Nat.mod_eq_of_lt hslot
-  have hone : (1 : Nat) < Compiler.Constants.evmModulus := by
-    simp [Compiler.Constants.evmModulus]
   cases fuel with
   | zero =>
       simp [guardPrologueStmts, execIRStmts, execIRStmt, evalIRExpr, evalIRCall,
-        evalIRExprs, hmod, hlock, Nat.mod_eq_of_lt hone,
+        evalIRExprs, hmod, hlock,
         YulGeneration.Backends.evalBuiltinCallWithEvmYulLeanContext]
   | succ n =>
       simp [guardPrologueStmts, execIRStmts, execIRStmt, evalIRExpr, evalIRCall,
-        evalIRExprs, hmod, hlock, Nat.mod_eq_of_lt hone,
+        evalIRExprs, hmod, hlock,
         YulGeneration.Backends.evalBuiltinCallWithEvmYulLeanContext]
 
 /-- Lock free (`tload = 0`) → the prologue acquires the lock and changes
@@ -87,11 +85,15 @@ theorem execIRStmt_lockRelease (fuel : Nat) (state : IRState) (slot : Nat)
   have hmod : slot % Compiler.Constants.evmModulus = slot := Nat.mod_eq_of_lt hslot
   simp [lockReleaseStmt, execIRStmt, evalIRExpr, hmod]
 
-/-- On the reachable (binary) lock values, the Yul decision `eq(lock, 1)`
-agrees with the source model's `lock ≠ 0` (`NonReentrantGuard.guarded`). -/
-theorem guard_decision_agrees (v : Nat) (hv : v = 0 ∨ v = 1) :
-    (v = 1) ↔ v ≠ 0 := by
-  rcases hv with h | h <;> simp [h]
+/-- Yul `if tload(slot)` sees the slot's transient value, so its nonzero
+decision is the source model's lock-held predicate `lock ≠ 0` for every
+stored value, not only the binary `{0,1}` acquire/release cycle. -/
+theorem guard_decision_agrees (state : IRState) (slot : Nat)
+    (hslot : slot < Compiler.Constants.evmModulus) :
+    evalIRExpr state (.call "tload" [.lit slot]) =
+      some (state.transientStorage slot) := by
+  have hmod : slot % Compiler.Constants.evmModulus = slot := Nat.mod_eq_of_lt hslot
+  simp [evalIRExpr, evalIRCall_tload_singleton, hmod]
 
 /-- Acquire-then-release round-trips the lock slot: the transient storage
 function is extensionally the initial one when the slot started free. -/
diff --git a/Contracts/Common.lean b/Contracts/Common.lean
index 22b02153c..526bb80c6 100644
--- a/Contracts/Common.lean
+++ b/Contracts/Common.lean
@@ -393,6 +393,20 @@ def tryCatchWord (attempt : Uint256) (handler : String → Contract Unit) : Cont
 def calldatasize : Uint256 := 0
 def returndataSize : Uint256 := 0
 def calldataload (offset : Uint256) : Uint256 := offset
+/-- Registry-mode executable calldata. Public `calldatasize`/`calldataload`
+remain deterministic stubs; generated `*_registry` bodies use these so a
+callback that branches on live calldata is registered. Byte offset 0 of the
+word-list data region is `calldataload 4`, matching compiled dispatch.
+`calldataload 0` (and unaligned loads overlapping the first four bytes)
+observe `state.selector`, not a hard-coded 0. -/
+def calldatasizeLive : Contract Uint256 := fun state =>
+  ContractResult.success state.calldataSize state
+def calldataloadLive (offset : Uint256) : Contract Uint256 := fun state =>
+  ContractResult.success
+    (Verity.Core.Uint256.ofNat
+      (Compiler.CompilationModel.Denote.calldataloadWord
+        state.selector state.calldata offset.val))
+    state
 def mload (offset : Uint256) : Uint256 := offset
 def tload (offset : Uint256) : Contract Uint256 := fun state =>
   ContractResult.success (state.transientStorage (offset : Nat)) state
@@ -687,6 +701,11 @@ structure ExecutableCallContext where
   adversary : AdversaryModel
   resolve : String → Nat → Option Compiler.CompilationModel.DenoteFunctionCalls.LinkedExternal
 
+/-- Bind an explicit adversary while pinning every resolved linked call to
+`target = 0` and `value = 0`. This is the registry/executable convenience
+boundary: the adversary is live, but link-time callee address and ETH value
+are the zero defaults. Callers that need a real target or nonzero value must
+supply `resolve` themselves (`ofCallEnv` or a custom context). -/
 def ExecutableCallContext.ofAdversary (adv : AdversaryModel) : ExecutableCallContext :=
   { adversary := adv
     resolve := fun _ fallbackSiteId =>
diff --git a/Contracts/Smoke/SecurityCombos.lean b/Contracts/Smoke/SecurityCombos.lean
index bd42e62e6..7ce3f9291 100644
--- a/Contracts/Smoke/SecurityCombos.lean
+++ b/Contracts/Smoke/SecurityCombos.lean
@@ -175,6 +175,144 @@ verity_contract NonreentrantTrustedInternalHelperAccepted where
 
 #check_contract NonreentrantTrustedInternalHelperAccepted
 
+-- Regression for Codex's PR #2406 qualified-helper finding.  Qualified Lean
+-- helpers that merely share a guarded local function's final name must retain
+-- their qualifier; they do not resolve to the generated lock-free shadow.
+verity_contract QualifiedHelperLibrary where
+  storage
+
+  function trustedEntry (x : Uint256) : Uint256 := do
+    return x
+
+  function trustedPair (x : Uint256) : Tuple [Uint256, Uint256] := do
+    return (x, x)
+
+  function adversarialEntry (x : Uint256) : Uint256 := do
+    return x
+
+  function adversarialPair (x : Uint256) : Tuple [Uint256, Uint256] := do
+    return (x, x)
+
+verity_contract NonreentrantQualifiedHelperResolution where
+  storage
+    lock : Uint256 := slot 0
+    value : Uint256 := slot 1
+
+  linked_externals
+    external echo(Uint256) -> (Uint256)
+
+  function nonreentrant(lock) reentrancy_trusted trustedEntry (x : Uint256) : Uint256 := do
+    return x
+
+  function nonreentrant(lock) reentrancy_trusted trustedPair (x : Uint256) : Tuple [Uint256, Uint256] := do
+    return (x, x)
+
+  function nonreentrant(lock) reentrancy_trusted adversarialEntry (x : Uint256) : Uint256 := do
+    let echoed := externalCall "echo" [x]
+    return echoed
+
+  function nonreentrant(lock) reentrancy_trusted adversarialPair (x : Uint256) : Tuple [Uint256, Uint256] := do
+    let echoed := externalCall "echo" [x]
+    return (echoed, echoed)
+
+  function overloadedTrusted (_who : Address) : Uint256 := do
+    return 0
+
+  function nonreentrant(lock) reentrancy_trusted overloadedTrusted (x : Uint256) : Uint256 := do
+    return x
+
+  function overloadedAdversarial (_who : Address) : Uint256 := do
+    return 0
+
+  function nonreentrant(lock) reentrancy_trusted overloadedAdversarial (x : Uint256) : Uint256 := do
+    let echoed := externalCall "echo" [x]
+    return echoed
+
+  function makePair (x : Uint256) : Tuple [Uint256, Uint256] := do
+    return (x, x)
+
+  function qualifiedSpace (x : Uint256) : Uint256 := do
+    let y ← QualifiedHelperLibrary.trustedEntry x
+    return y
+
+  function qualifiedDestructure (x : Uint256) : Uint256 := do
+    let (left, right) ← QualifiedHelperLibrary.trustedPair x
+    return (add left right)
+
+  function qualifiedAdversarialSpace (x : Uint256) : Uint256 := do
+    let y ← QualifiedHelperLibrary.adversarialEntry x
+    return y
+
+  function qualifiedAdversarialDestructure (x : Uint256) : Uint256 := do
+    let (left, right) ← QualifiedHelperLibrary.adversarialPair x
+    return (add left right)
+
+  function reentrancy_trusted qualifiedNestedExternal (x : Uint256) : Uint256 := do
+    let y ← QualifiedHelperLibrary.trustedEntry (externalCall "echo" [x])
+    return y
+
+  function reentrancy_trusted trustedNestedExternal (x : Uint256) : Uint256 := do
+    let y ← trustedEntry(externalCall "echo" [x])
+    return y
+
+  function reentrancy_trusted overloadedNestedExternal (x : Uint256) : Uint256 := do
+    let y ← overloadedAdversarial(externalCall "echo" [x])
+    return y
+
+  function overloadedTrustedCaller (x : Uint256) : Unit := do
+    let y ← overloadedTrusted x
+    require (y == x) "wrong trusted overload"
+
+  function overloadedAdversarialCaller (x : Uint256) : Unit := do
+    let y ← overloadedAdversarial x
+    require (y == x) "wrong adversarial overload"
+
+  function overloadedTrustedLocalCaller () : Unit := do
+    let x ← getStorage value
+    let y ← overloadedTrusted x
+    require (y == x) "wrong trusted local overload"
+
+  function overloadedAdversarialLocalCaller () : Unit := do
+    let x ← getStorage value
+    let y ← overloadedAdversarial x
+    require (y == x) "wrong adversarial local overload"
+
+  function overloadedTrustedTupleLocalCaller (x : Uint256) : Unit := do
+    let (left, _right) ← makePair x
+    let y ← overloadedTrusted left
+    require (y == x) "wrong trusted tuple-local overload"
+
+  function overloadedAdversarialTupleLocalCaller (x : Uint256) : Unit := do
+    let (_left, right) ← makePair x
+    let y ← overloadedAdversarial right
+    require (y == x) "wrong adversarial tuple-local overload"
+
+  function overloadedTrustedQualifiedTupleCaller (x : Uint256) : Unit := do
+    let (left, _right) ← QualifiedHelperLibrary.trustedPair x
+    let y ← overloadedTrusted left
+    require (y == x) "wrong qualified tuple-local overload"
+
+  function nonreentrant(lock) reentrancy_trusted staticResultControlsStorage
+      (target : Uint256, x : Uint256)
+      local_obligations [manual_low_level_refinement := assumed "Static-call result threading is the explicit low-level boundary under test."] : Unit := do
+    let observed ← evmStaticCall(50000, target, 0, 0, 0, 0)
+    if observed == x then
+      setStorage value observed
+    else
+      pure ()
+
+  function overloadedTrustedForEachCaller () : Unit := do
+    forEach "i" 1 (do
+      let y ← overloadedTrusted i
+      require (y == i) "wrong trusted loop-local overload")
+
+  function overloadedAdversarialForEachSetBitCaller () : Unit := do
+    forEachSetBit "i" 1 (do
+      let y ← overloadedAdversarial i
+      require (y == i) "wrong adversarial loop-local overload")
+
+#check_contract NonreentrantQualifiedHelperResolution
+
 -- ════════════════════════════════════════════════════════════════════════════
 -- Stress-test contracts: edge-case coverage for Language Design Axes (#1731)
 -- ════════════════════════════════════════════════════════════════════════════
diff --git a/PrintAxioms.lean b/PrintAxioms.lean
index cc799558a..28d1c4283 100644
--- a/PrintAxioms.lean
+++ b/PrintAxioms.lean
@@ -41,6 +41,7 @@ import Contracts.Vault.Proofs.Native
 import Verity.Proofs.CheckedExternalCallConsumer
 import Verity.Proofs.LoopSimulationResultAware
 import Verity.Proofs.Model.CommonExternalCallEquivalence
+import Verity.Proofs.Model.GeneratedEntrypointRegistry
 import Verity.Proofs.Stdlib.Automation
 import Verity.Proofs.Stdlib.Int256
 import Verity.Proofs.Stdlib.ListSum
@@ -739,6 +740,17 @@ end Verity.AxiomAudit
   Contracts.legacyStringSafeTransfer_eq_stub
   Contracts.legacyStringSafeTransferFrom_eq_stub
 
+  -- Verity/Proofs/Model/GeneratedEntrypointRegistry.lean
+  Contracts.ReentrancyRelyGuarantee.GeneratedRegistry.guardedPing_registered
+  Contracts.ReentrancyRelyGuarantee.GeneratedRegistry.guardedPing_registered_ofAdversary
+  Contracts.ReentrancyRelyGuarantee.GeneratedRegistry.guardedPing_reentry_blocked
+  Contracts.ReentrancyRelyGuarantee.RegistryDispatchCalldata.setLast_registered_matching
+  Contracts.ReentrancyRelyGuarantee.RegistryDispatchCalldata.setLast_entrypoint_requires_dispatch
+  Contracts.ReentrancyRelyGuarantee.RegistryDispatchCalldata.receive_registered_empty
+  Contracts.ReentrancyRelyGuarantee.RegistryDispatchCalldata.receive_entrypoint_requires_empty
+  Contracts.ReentrancyRelyGuarantee.RegistryLiveCalldata.setFromCalldata_registered_live
+  Contracts.ReentrancyRelyGuarantee.generated_registry_callback_preserves
+
   -- Verity/Proofs/Stdlib/Automation.lean
   Verity.Proofs.Stdlib.Automation.isSuccess_success
   Verity.Proofs.Stdlib.Automation.isSuccess_revert
@@ -7619,4 +7631,4 @@ end Verity.AxiomAudit
   Compiler.Proofs.YulGeneration.YulTransaction.ofIR_args
 ]
 
--- Total: 7036 theorems/lemmas (5023 public, 2013 private, 0 sorry'd)
+-- Total: 7045 theorems/lemmas (5032 public, 2013 private, 0 sorry'd)
diff --git a/Verity/Core.lean b/Verity/Core.lean
index 7a071d4d6..a746468c4 100644
--- a/Verity/Core.lean
+++ b/Verity/Core.lean
@@ -400,6 +400,9 @@ structure ContractState where
   blobBaseFee : Uint256 := 0
   calldataSize : Uint256 := 0
   calldata : List Nat := []                 -- Immutable calldata words used by ABI expression semantics
+  /-- 4-byte function selector for live `calldataload 0` in registry mode.
+      Compiled dispatch packs it in the high 4 bytes of the first word. -/
+  selector : Nat := 0
   memory : Nat → Uint256 := fun _ => 0     -- EVM memory (word-addressed, zero-initialized)
   knownAddresses : Nat → FiniteAddressSet  -- Tracked addresses per storage slot (for sum properties)
   events : List Event := []  -- Emitted events, append-only log (#153)
diff --git a/Verity/Core/Model/CallbackBridge.lean b/Verity/Core/Model/CallbackBridge.lean
index a262ca253..a07565794 100644
--- a/Verity/Core/Model/CallbackBridge.lean
+++ b/Verity/Core/Model/CallbackBridge.lean
@@ -22,23 +22,482 @@ namespace Compiler.CompilationModel.DenoteExternalCalls
 open Verity.Core.Invariant (Preserves runSeq)
 open Verity.Core.Reentrancy (ReentrancySpec)
 
+/-- The macro-emitted registry is a predicate rather than a list of already
+applied functions.  Entrypoint arguments stay existential, but they are
+tied to the same calldata the compiled dispatcher ABI-decodes, and every
+transition is indexed by the explicit adversary used at the call boundary. -/
+abbrev EntrypointRegistry :=
+  AdversaryModel → (Verity.ContractState → Verity.ContractState) → Prop
+
+namespace EntrypointRegistry
+
+/-- Compatibility adapter for the original, argument-free worked examples. -/
+def ofList (entrypoints : List (Verity.ContractState → Verity.ContractState)) :
+    EntrypointRegistry :=
+  fun _ entrypoint => entrypoint ∈ entrypoints
+
+instance : Coe (List (Verity.ContractState → Verity.ContractState))
+    EntrypointRegistry where
+  coe := ofList
+
+end EntrypointRegistry
+
+/-- EVM frame data chosen by a callee when it calls back into the current
+contract.  Entrypoint arguments remain existential in the generated
+registry; this record covers the ambient values observable through
+`msg.sender`, `msg.value`, and raw calldata intrinsics. -/
+structure CallbackContext where
+  sender : Verity.Address
+  msgValue : Verity.Uint256
+  calldataSize : Verity.Uint256
+  calldata : List Nat
+  /-- 4-byte selector of the selected entrypoint. Live `calldataload 0`
+  observes this via `ContractState.selector`. Defaults to 0 so existing
+  fixtures that omit it stay well-typed. -/
+  selector : Nat := 0
+
+/-- Packed ABI bytes/string data: 32-byte big-endian words, right-zero-padded.
+Not `ExternalArg.toWords`, which journals one word per byte. Fuel is
+`bytes.length`, so this is structurally recursive on `Nat` and reduces
+under `decide`. -/
+def packAbiBytes (bytes : List Nat) : List Nat :=
+  packAbiBytesFuel bytes.length bytes
+where
+  packAbiBytesFuel : Nat → List Nat → List Nat
+    | 0, _ => []
+    | _n+1, [] => []
+    | n+1, x :: xs =>
+        let rest := x :: xs
+        let chunk := rest.take 32
+        let padded := chunk ++ List.replicate (32 - chunk.length) 0
+        let word := padded.foldl (fun acc b => acc * 256 + b % 256) 0
+        word :: packAbiBytesFuel n (rest.drop 32)
+
+/-- One ABI argument as consumed by `genParamLoads` / compiled dispatch. -/
+inductive DispatchVal where
+  | word : Nat → DispatchVal
+  | bytes : List Nat → DispatchVal
+  | array : List DispatchVal → DispatchVal
+  | tuple : List DispatchVal → DispatchVal
+
+mutual
+  def DispatchVal.isDynamic : DispatchVal → Bool
+    | .word _ => false
+    | .bytes _ => true
+    | .array _ => true
+    | .tuple vs => dispatchValAnyDynamic vs
+
+  def dispatchValAnyDynamic : List DispatchVal → Bool
+    | [] => false
+    | v :: vs => v.isDynamic || dispatchValAnyDynamic vs
+
+  def DispatchVal.headBytes : DispatchVal → Nat
+    | .word _ => 32
+    | .bytes _ => 32
+    | .array _ => 32
+    | .tuple vs =>
+        if dispatchValAnyDynamic vs then 32
+        else dispatchValHeadBytesList vs
+
+  def dispatchValHeadBytesList : List DispatchVal → Nat
+    | [] => 0
+    | v :: vs => v.headBytes + dispatchValHeadBytesList vs
+
+  /-- Payload words of a value (no parent offset). Dynamic arrays of dynamic
+  elements use offsets relative to the start of the post-length head. -/
+  def DispatchVal.payloadWords : DispatchVal → List Nat
+    | .word w => [w]
+    | .bytes bs => bs.length :: packAbiBytes bs
+    | .array vs =>
+        if dispatchValAnyDynamic vs then
+          let (offs, tails) := encodeDynamicList vs (32 * vs.length)
+          vs.length :: offs ++ tails
+        else
+          vs.length :: dispatchValFlatPayload vs
+    | .tuple vs =>
+        if dispatchValAnyDynamic vs then
+          let (heads, tails) := encodeArgBlock vs (dispatchValHeadBytesList vs)
+          heads ++ tails
+        else
+          dispatchValFlatPayload vs
+
+  def dispatchValFlatPayload : List DispatchVal → List Nat
+    | [] => []
+    | v :: vs => v.payloadWords ++ dispatchValFlatPayload vs
+
+  def encodeDynamicList : List DispatchVal → Nat → List Nat × List Nat
+    | [], _ => ([], [])
+    | v :: vs, tailOff =>
+        let pay := v.payloadWords
+        let (offs, tails) := encodeDynamicList vs (tailOff + pay.length * 32)
+        (tailOff :: offs, pay ++ tails)
+
+  def encodeArgBlock : List DispatchVal → Nat → List Nat × List Nat
+    | [], _ => ([], [])
+    | v :: vs, tailOff =>
+        if v.isDynamic then
+          let pay := v.payloadWords
+          let (heads, tails) := encodeArgBlock vs (tailOff + pay.length * 32)
+          (tailOff :: heads, pay ++ tails)
+        else
+          let (heads, tails) := encodeArgBlock vs tailOff
+          (v.payloadWords ++ heads, tails)
+end
+
+/-- True when every argument is a static ABI word. Kept outside the mutual
+block so `decide` unfolds it. Static tuples/fixed arrays use `payloadWords`
+via the mutual encoder (not this fast path). -/
+def dispatchArgsAllWords : List DispatchVal → Bool
+  | [] => true
+  | .word _ :: rest => dispatchArgsAllWords rest
+  | _ => false
+
+def dispatchArgWordVals : List DispatchVal → List Nat
+  | [] => []
+  | .word w :: rest => w :: dispatchArgWordVals rest
+  | _ :: rest => 0 :: dispatchArgWordVals rest
+
+/-- ABI argument-block encoding matching `genParamLoads`: static values occupy
+head words; dynamic values contribute a head offset then a tail of
+`[length, packed data…]` (bytes/string) or `[length, elements…]` (arrays).
+All-static-word argument lists skip the mutual encoder so kernel `decide`
+reduces generated scalar `*_entrypoint` tests. -/
+def abiEncodeDispatchArgs (args : List DispatchVal) : List Nat :=
+  if dispatchArgsAllWords args then
+    dispatchArgWordVals args
+  else
+    let (heads, tails) := encodeArgBlock args (dispatchValHeadBytesList args)
+    heads ++ tails
+
+@[simp] theorem abiEncodeDispatchArgs_nil :
+    abiEncodeDispatchArgs [] = [] := rfl
+
+@[simp] theorem abiEncodeDispatchArgs_singleton_word (w : Nat) :
+    abiEncodeDispatchArgs [.word w] = [w] := rfl
+
+class ToDispatchVal (α : Type) where
+  toDispatchVal : α → DispatchVal
+
+instance : ToDispatchVal Verity.Uint256 where
+  toDispatchVal v := .word v.val
+
+instance : ToDispatchVal Verity.Uint16 where
+  toDispatchVal v := .word v.toUint256.val
+
+instance : ToDispatchVal (Verity.UIntN bits) where
+  toDispatchVal v := .word v.toUint256.val
+
+instance : ToDispatchVal (Verity.IntN bits) where
+  toDispatchVal v := .word v.toUint256.val
+
+instance : ToDispatchVal (Verity.BytesN bytes) where
+  toDispatchVal v := .word v.toUint256.val
+
+instance : ToDispatchVal Verity.Int256 where
+  toDispatchVal v := .word v.word.val
+
+instance : ToDispatchVal Verity.Address where
+  toDispatchVal v := .word v.val
+
+instance : ToDispatchVal Bool where
+  toDispatchVal v := .word (if v then 1 else 0)
+
+instance : ToDispatchVal Nat where
+  toDispatchVal v := .word v
+
+instance : ToDispatchVal ByteArray where
+  toDispatchVal b := .bytes (b.data.toList.map (fun x => x.toNat))
+
+instance : ToDispatchVal String where
+  toDispatchVal s := ToDispatchVal.toDispatchVal s.toUTF8
+
+instance [ToDispatchVal α] : ToDispatchVal (Array α) where
+  toDispatchVal vs := .array (vs.toList.map ToDispatchVal.toDispatchVal)
+
+/-- Right-nested Lean products (`α × (β × γ)`) encode as a nested ABI tuple
+unless flattened. Compiled `Tuple [α, β, γ]` is a single flat tuple. -/
+def flattenDispatchTuple : DispatchVal → List DispatchVal
+  | .tuple vs => vs.flatMap flattenDispatchTuple
+  | v => [v]
+
+/-- Compiled `T[n]` is a static/dynamic composite with no `T[]` length word.
+Encode as a tuple of n members (inlined if static; offset-only if dynamic). -/
+def dispatchFixedArray (elems : List DispatchVal) : DispatchVal :=
+  .tuple elems
+
+/-- Flatten a right-nested product encoding into one ABI tuple. -/
+def dispatchFlatTuple (v : DispatchVal) : DispatchVal :=
+  .tuple (flattenDispatchTuple v)
+
+instance [ToDispatchVal α] [ToDispatchVal β] : ToDispatchVal (α × β) where
+  toDispatchVal p :=
+    .tuple (flattenDispatchTuple (ToDispatchVal.toDispatchVal p.1) ++
+      flattenDispatchTuple (ToDispatchVal.toDispatchVal p.2))
+
+/-- How `genScalarLoad` normalizes a loaded word before the body sees it. -/
+inductive ScalarLoadKind where
+  | identity
+  | bool
+  | uint8
+  | uint16
+  | uintN (bits : Nat)
+  | address
+  | bytesN (bytes : Nat)
+  deriving Repr, DecidableEq
+
+def normalizeLoadedWord (kind : ScalarLoadKind) (loaded : Nat) : Nat :=
+  let w := loaded % Compiler.Constants.evmModulus
+  match kind with
+  | .identity => w
+  | .bool => if w == 0 then 0 else 1
+  | .uint8 => w % 256
+  | .uint16 => w % 65536
+  | .uintN bits => w % (2 ^ bits)
+  | .address => w &&& Compiler.Constants.addressMask
+  | .bytesN bytes =>
+      w &&& ((2 ^ (8 * bytes) - 1) * 2 ^ (8 * (32 - bytes)))
+
+def scalarWordMatches (kind : ScalarLoadKind) (canonical loaded : Nat) : Bool :=
+  normalizeLoadedWord kind loaded == canonical % Compiler.Constants.evmModulus
+
+def dispatchWordsMatch : List ScalarLoadKind → List Nat → List Nat → Bool
+  | [], _, _ => true
+  | _ :: _, [], _ => false
+  | _ :: _, _ :: _, [] => false
+  | k :: ks, c :: cs, l :: ls =>
+      scalarWordMatches k c l && dispatchWordsMatch ks cs ls
+
+/-- Compiled dispatch ABI-decodes arguments from the same calldata that
+selected the function (`calldataload` at 4 + 32*i, `calldatasize` at
+least 4 + 32 * n). Extra trailing words are allowed, matching Yul
+`calldatasizeGuard`. `argWords` is the ABI data region (no 4-byte selector),
+from `abiEncodeDispatchArgs`, not `ExternalArg.toWords`. Scalar prefixes
+compare after `genScalarLoad` normalization so noncanonical Bool/uintN/
+address words still register. -/
+def dispatchCalldataMatches (ctx : CallbackContext) (argWords : List Nat) : Prop :=
+  dispatchWordsMatch
+      (List.replicate argWords.length ScalarLoadKind.identity)
+      argWords (ctx.calldata.take argWords.length) = true ∧
+    Verity.Core.Uint256.ofNat (4 + 32 * argWords.length) ≤ ctx.calldataSize
+
+/-- Like `dispatchCalldataMatches`, but scalar words compare after the compiled
+`genScalarLoad` normalization for each argument. -/
+def dispatchCalldataMatchesKinds (ctx : CallbackContext)
+    (kinds : List ScalarLoadKind) (argWords : List Nat) : Prop :=
+  dispatchWordsMatch kinds argWords (ctx.calldata.take argWords.length) = true ∧
+    Verity.Core.Uint256.ofNat (4 + 32 * argWords.length) ≤ ctx.calldataSize
+
+instance (ctx : CallbackContext) (kinds : List ScalarLoadKind) (argWords : List Nat) :
+    Decidable (dispatchCalldataMatchesKinds ctx kinds argWords) := by
+  dsimp [dispatchCalldataMatchesKinds]
+  infer_instance
+
+instance (ctx : CallbackContext) (argWords : List Nat) :
+    Decidable (dispatchCalldataMatches ctx argWords) := by
+  dsimp [dispatchCalldataMatches]
+  infer_instance
+
+/-- Compiled `receive()` runs only when `calldatasize == 0`. -/
+def receiveCalldataMatches (ctx : CallbackContext) : Prop :=
+  ctx.calldata = [] ∧ ctx.calldataSize = 0
+
+instance (ctx : CallbackContext) :
+    Decidable (receiveCalldataMatches ctx) := by
+  dsimp [receiveCalldataMatches]
+  infer_instance
+
+/-- Execute a registered callback in its own call frame, then restore the
+outer frame's ambient context while retaining the callback's contract-state
+effects. -/
+def withCallbackContext (ctx : CallbackContext) (world : Verity.ContractState) :
+    Verity.ContractState :=
+  { world with
+    sender := ctx.sender
+    msgValue := ctx.msgValue
+    selfBalance := world.selfBalance + ctx.msgValue
+    calldataSize := ctx.calldataSize
+    calldata := ctx.calldata
+    selector := ctx.selector
+    memory := fun _ => 0
+    returndata := [] }
+
+def restoreCallbackContext (outer callbackResult : Verity.ContractState) :
+    Verity.ContractState :=
+  { callbackResult with
+    sender := outer.sender
+    msgValue := outer.msgValue
+    calldataSize := outer.calldataSize
+    calldata := outer.calldata
+    selector := outer.selector
+    memory := outer.memory
+    returndata := outer.returndata }
+
+def callbackTransition (ctx : CallbackContext)
+    (entrypoint : Verity.ContractState → Verity.ContractState) :
+    Verity.ContractState → Verity.ContractState :=
+  fun outer => restoreCallbackContext outer (entrypoint (withCallbackContext ctx outer))
+
+/-- Run an executable callback while retaining its success/revert outcome.
+Successful callbacks commit their state after restoring the caller's ambient
+frame; reverting callbacks roll back the entire callback, including the value
+credit installed on entry. -/
+def callbackContractTransition (ctx : CallbackContext)
+    (entrypoint : Verity.Contract α) :
+    Verity.ContractState → Verity.ContractState :=
+  fun outer =>
+    match entrypoint.run (withCallbackContext ctx outer) with
+    | .success _ callbackResult => restoreCallbackContext outer callbackResult
+    | .revert _ _ => outer
+
+@[simp] theorem callbackContractTransition_success (ctx : CallbackContext)
+    (entrypoint : Verity.Contract α) (outer callbackResult : Verity.ContractState)
+    (value : α)
+    (hrun : entrypoint.run (withCallbackContext ctx outer) =
+      Verity.ContractResult.success value callbackResult) :
+    callbackContractTransition ctx entrypoint outer =
+      restoreCallbackContext outer callbackResult := by
+  simp [callbackContractTransition, hrun]
+
+@[simp] theorem callbackContractTransition_revert (ctx : CallbackContext)
+    (entrypoint : Verity.Contract α) (outer : Verity.ContractState) (message : String)
+    (hrun : entrypoint.run (withCallbackContext ctx outer) =
+      Verity.ContractResult.revert message (withCallbackContext ctx outer)) :
+    callbackContractTransition ctx entrypoint outer = outer := by
+  simp [callbackContractTransition, hrun]
+
+@[simp] theorem withCallbackContext_sender (ctx : CallbackContext)
+    (world : Verity.ContractState) :
+    (withCallbackContext ctx world).sender = ctx.sender := rfl
+
+@[simp] theorem withCallbackContext_msgValue (ctx : CallbackContext)
+    (world : Verity.ContractState) :
+    (withCallbackContext ctx world).msgValue = ctx.msgValue := rfl
+
+@[simp] theorem withCallbackContext_calldata (ctx : CallbackContext)
+    (world : Verity.ContractState) :
+    (withCallbackContext ctx world).calldata = ctx.calldata := rfl
+
+@[simp] theorem withCallbackContext_calldataSize (ctx : CallbackContext)
+    (world : Verity.ContractState) :
+    (withCallbackContext ctx world).calldataSize = ctx.calldataSize := rfl
+
+@[simp] theorem withCallbackContext_selector (ctx : CallbackContext)
+    (world : Verity.ContractState) :
+    (withCallbackContext ctx world).selector = ctx.selector := rfl
+
+@[simp] theorem withCallbackContext_selfBalance (ctx : CallbackContext)
+    (world : Verity.ContractState) :
+    (withCallbackContext ctx world).selfBalance = world.selfBalance + ctx.msgValue := rfl
+
+@[simp] theorem withCallbackContext_returndata (ctx : CallbackContext)
+    (world : Verity.ContractState) :
+    (withCallbackContext ctx world).returndata = [] := rfl
+
+@[simp] theorem withCallbackContext_memory (ctx : CallbackContext)
+    (world : Verity.ContractState) :
+    (withCallbackContext ctx world).memory = (fun _ => 0) := rfl
+
+@[simp] theorem callbackTransition_restores_sender (ctx : CallbackContext)
+    (entrypoint : Verity.ContractState → Verity.ContractState)
+    (outer : Verity.ContractState) :
+    (callbackTransition ctx entrypoint outer).sender = outer.sender := rfl
+
+@[simp] theorem callbackTransition_restores_msgValue (ctx : CallbackContext)
+    (entrypoint : Verity.ContractState → Verity.ContractState)
+    (outer : Verity.ContractState) :
+    (callbackTransition ctx entrypoint outer).msgValue = outer.msgValue := rfl
+
+@[simp] theorem callbackTransition_restores_calldata (ctx : CallbackContext)
+    (entrypoint : Verity.ContractState → Verity.ContractState)
+    (outer : Verity.ContractState) :
+    (callbackTransition ctx entrypoint outer).calldata = outer.calldata := rfl
+
+@[simp] theorem callbackTransition_restores_calldataSize (ctx : CallbackContext)
+    (entrypoint : Verity.ContractState → Verity.ContractState)
+    (outer : Verity.ContractState) :
+    (callbackTransition ctx entrypoint outer).calldataSize = outer.calldataSize := rfl
+
+@[simp] theorem callbackTransition_restores_selector (ctx : CallbackContext)
+    (entrypoint : Verity.ContractState → Verity.ContractState)
+    (outer : Verity.ContractState) :
+    (callbackTransition ctx entrypoint outer).selector = outer.selector := rfl
+
+@[simp] theorem callbackTransition_restores_memory (ctx : CallbackContext)
+    (entrypoint : Verity.ContractState → Verity.ContractState)
+    (outer : Verity.ContractState) :
+    (callbackTransition ctx entrypoint outer).memory = outer.memory := rfl
+
+@[simp] theorem callbackTransition_restores_returndata (ctx : CallbackContext)
+    (entrypoint : Verity.ContractState → Verity.ContractState)
+    (outer : Verity.ContractState) :
+    (callbackTransition ctx entrypoint outer).returndata = outer.returndata := rfl
+
 /-- Each mutable transition is some finite reentry schedule drawn from the
 registry.  Static sites are unrestricted: `denoteCall` never commits their
 transitions, and `Conforms` separately pins them externally. -/
 def CallbackBounded
-    (entrypoints : List (Verity.ContractState → Verity.ContractState))
+    (entrypoints : EntrypointRegistry)
     (adversary : AdversaryModel) : Prop :=
   ∀ site world, site.kind ≠ .staticcall →
     ∃ sched : List (Verity.ContractState → Verity.ContractState),
-      (∀ f ∈ sched, f ∈ entrypoints) ∧
+      (∀ f ∈ sched, entrypoints adversary f) ∧
         adversary.stateTransition site world = runSeq sched world
 
+/-- The sole proof obligation at the generated-registry boundary: every
+transition admitted by the registry for this adversary preserves the caller's
+invariant. -/
+def RegistryPreserves (Inv : Verity.ContractState → Prop)
+    (entrypoints : EntrypointRegistry) (adversary : AdversaryModel) : Prop :=
+  ∀ f, entrypoints adversary f → Preserves Inv f
+
+/-- A call through the restricted generated-registry boundary preserves any
+invariant discharged for every registered, fully-applied entrypoint. -/
+theorem CallbackBounded.denoteCall_preserves_registry
+    (Inv : Verity.ContractState → Prop) (entrypoints : EntrypointRegistry)
+    {adversary : AdversaryModel}
+    (hbound : CallbackBounded entrypoints adversary)
+    (hregistry : RegistryPreserves Inv entrypoints adversary)
+    (site : CallSite) (state : CallState) (hInv : Inv state.world) :
+    Inv (denoteCall adversary site state).state.world := by
+  cases hkind : site.kind with
+  | staticcall =>
+      rw [denoteCall_staticcall_world adversary site state hkind]
+      exact hInv
+  | call =>
+      cases hres : adversary.result site state.world with
+      | success data =>
+          rw [denoteCall_call_success_world adversary site state data hkind hres]
+          obtain ⟨sched, hmem, htrans⟩ := hbound site state.world (by simp [hkind])
+          rw [htrans]
+          exact Verity.Core.Invariant.runSeq_preserves sched
+            (fun f hf => hregistry f (hmem f hf)) state.world hInv
+      | failure data =>
+          rw [denoteCall_failure_world adversary site state data (Or.inl hkind) hres]
+          exact hInv
+      | revert data =>
+          rw [denoteCall_revert_world adversary site state data (Or.inl hkind) hres]
+          exact hInv
+  | delegatecall =>
+      cases hres : adversary.result site state.world with
+      | success data =>
+          rw [denoteCall_delegatecall_success_world adversary site state data hkind hres]
+          obtain ⟨sched, hmem, htrans⟩ := hbound site state.world (by simp [hkind])
+          rw [htrans]
+          exact Verity.Core.Invariant.runSeq_preserves sched
+            (fun f hf => hregistry f (hmem f hf)) state.world hInv
+      | failure data =>
+          rw [denoteCall_failure_world adversary site state data (Or.inr hkind) hres]
+          exact hInv
+      | revert data =>
+          rw [denoteCall_revert_world adversary site state data (Or.inr hkind) hres]
+          exact hInv
+
 /-- One external call under a callback-bounded adversary preserves the spec
 invariant: rollback outcomes keep the pre-call world, and committed outcomes
 are reentry schedules, covered by the per-entrypoint obligations. -/
 theorem CallbackBounded.denoteCall_preserves (spec : ReentrancySpec)
     {adversary : AdversaryModel}
-    (h : CallbackBounded spec.entrypoints adversary)
+    (h : CallbackBounded (EntrypointRegistry.ofList spec.entrypoints) adversary)
     (site : CallSite) (state : CallState)
     (hInv : spec.Inv state.world) :
     spec.Inv (denoteCall adversary site state).state.world := by
@@ -78,7 +537,7 @@ sequence of externally opened windows — each free to reenter through any
 registered schedule — can break it. -/
 theorem CallbackBounded.denote_preserves (spec : ReentrancySpec)
     {adversary : AdversaryModel}
-    (h : CallbackBounded spec.entrypoints adversary)
+    (h : CallbackBounded (EntrypointRegistry.ofList spec.entrypoints) adversary)
     (prog : CallProgram α) (state : CallState)
     (hInv : spec.Inv state.world) :
     spec.Inv (denote prog adversary state).2.world := by
@@ -94,7 +553,7 @@ invariant state by the program law, and a reverted one by rollback to the
 initial state. -/
 theorem CallbackBounded.transaction_preserves (spec : ReentrancySpec)
     {adversary : AdversaryModel}
-    (h : CallbackBounded spec.entrypoints adversary)
+    (h : CallbackBounded (EntrypointRegistry.ofList spec.entrypoints) adversary)
     (prog : CallProgram (TransactionResult α)) (state : CallState)
     (hInv : spec.Inv state.world) :
     spec.Inv (denoteTransaction prog adversary state).state.world := by
diff --git a/Verity/Core/Model/NonReentrantGuard.lean b/Verity/Core/Model/NonReentrantGuard.lean
index 0ca472b68..86ffc25f4 100644
--- a/Verity/Core/Model/NonReentrantGuard.lean
+++ b/Verity/Core/Model/NonReentrantGuard.lean
@@ -54,7 +54,7 @@ def guarded (slot : Nat) (body : Contract α) : Contract α :=
     else
       ContractResult.revert "reentrant call blocked" s
 
-/-- Lock held → the guarded entrypoint reverts without touching the state. -/
+/-- Any nonzero lock value is held, matching the compiled `tload` guard. -/
 theorem guarded_locked_reverts (slot : Nat) (body : Contract α)
     (s : ContractState) (hlock : s.transientStorage slot ≠ 0) :
     guarded slot body s = ContractResult.revert "reentrant call blocked" s := by
diff --git a/Verity/Macro.lean b/Verity/Macro.lean
index 876e5efd2..ba5feda44 100644
--- a/Verity/Macro.lean
+++ b/Verity/Macro.lean
@@ -2,6 +2,8 @@ import Verity.Macro.Syntax
 import Verity.Macro.Translate
 import Verity.Macro.Bridge
 import Verity.Macro.Elaborate
+import Verity.Core.Model.CallbackBridge
+import Verity.Core.Model.NonReentrantGuard
 import Verity.Macro.SpecGen
 import Verity.Macro.KeccakLit
 import Verity.Macro.KeccakString
diff --git a/Verity/Macro/Elaborate.lean b/Verity/Macro/Elaborate.lean
index 0678abb27..62c913b12 100644
--- a/Verity/Macro/Elaborate.lean
+++ b/Verity/Macro/Elaborate.lean
@@ -85,7 +85,6 @@ private def elabVerityContractOrMixin (stx : Syntax) : CommandElabM Unit := do
   let isMixin := parsed.isMixin
   let resolvedIncludes := parsed.resolvedIncludes
 
-  validateGeneratedDefNamesPublic fields constDecls immutableDecls functions
   validateConstantDeclsPublic constDecls
   validateImmutableDeclsPublic fields constDecls immutableDecls ctor
   validateExternalDeclsPublic externalDecls
@@ -121,6 +120,8 @@ private def elabVerityContractOrMixin (stx : Syntax) : CommandElabM Unit := do
   let translationExternalDecls := mixinExternalDecls ++ externalDecls
   let translationFunctions := mixinFunctions ++ functions
   let translationRoleDecls := mixinRoleDecls ++ roleDecls
+  validateGeneratedDefNamesPublic structDecls translationFields translationConstDecls
+    translationImmutableDecls (mixinModifiers ++ modifiers) translationFunctions
   validateFunctionDeclsPublic translationFields translationErrorDecls translationEventDecls
     translationConstDecls translationImmutableDecls translationExternalDecls ctor
     (mixinModifiers ++ modifiers) translationFunctions
@@ -135,6 +136,7 @@ private def elabVerityContractOrMixin (stx : Syntax) : CommandElabM Unit := do
       elabCommand (← mkStructDefCommandPublic structDecl)
       elabCommand (← mkStructEventArgInstanceCommandPublic structDecl)
       elabCommand (← mkStructExternalArgInstanceCommandPublic structDecl)
+      elabCommand (← mkStructToDispatchValInstanceCommandPublic structDecl)
       elabCommand (← mkStructExternalResultInstanceCommandPublic structDecl)
 
     let aliasCmds ← mkIncludeAliasCommandsPublic resolvedIncludes
@@ -177,6 +179,8 @@ private def elabVerityContractOrMixin (stx : Syntax) : CommandElabM Unit := do
         elabCommand cmd
       elabCommand (← mkBridgeCommand fn.ident)
 
+    elabCommand (← mkEntrypointRegistryCommandPublic translationFunctions)
+
     -- Constructors may call internal helpers, so emit them only after the
     -- executable helper definitions are available in the namespace.
     if isMixin then
diff --git a/Verity/Macro/Translate.lean b/Verity/Macro/Translate.lean
index 7e3561a72..785f7a495 100644
--- a/Verity/Macro/Translate.lean
+++ b/Verity/Macro/Translate.lean
@@ -2035,7 +2035,7 @@ private def adversaryModelTypeTerm : CommandElabM Term :=
   `(Compiler.CompilationModel.DenoteExternalCalls.AdversaryModel)
 
 private def executableCallContextTypeTerm : CommandElabM Term :=
-  `(ExecutableCallContext)
+  `(Contracts.ExecutableCallContext)
 
 private def mkContractFnTypeWithAdversary
     (params : Array ParamDecl) (retTy : ValueType) : CommandElabM Term := do
@@ -2498,6 +2498,55 @@ def translatedBodyOpensReentrancyWindow
     | _ => throwErrorAt bodyTerm
         "failed to reduce the translated reentrancy-window predicate"
 
+def translatedBodyContainsExternalCall
+    (stmtTerms : Array Term) : CommandElabM Bool := do
+  let bodyTerm : Term ← `([ $[$stmtTerms],* ])
+  liftTermElabM do
+    let predicate : Term ←
+      `($(bodyTerm).any Compiler.CompilationModel.stmtContainsExternalCall)
+    let expr ← Lean.Elab.Term.elabTermEnsuringType predicate (mkConst ``Bool)
+    match ← Lean.Meta.withTransparency .all (Lean.Meta.whnf expr) with
+    | .const ``Bool.true _ => pure true
+    | .const ``Bool.false _ => pure false
+    | _ => throwErrorAt bodyTerm
+        "failed to reduce the translated external-call predicate"
+
+private partial def syntaxContainsCalldataRead (stx : Syntax) : Bool :=
+  match stx with
+  | `(term| calldatasize) | `(term| calldataload $_) => true
+  | _ => stx.getArgs.any syntaxContainsCalldataRead
+
+def translatedBodyContainsCalldataRead
+    (stmtTerms : Array Term) : CommandElabM Bool := do
+  if stmtTerms.any (fun t => syntaxContainsCalldataRead t.raw) then
+    return true
+  let bodyTerm : Term ← `([ $[$stmtTerms],* ])
+  liftTermElabM do
+    let predicate : Term ←
+      `($(bodyTerm).any (fun s =>
+        Compiler.CompilationModel.Stmt.anyDeep
+          (fun
+            | .letVar _ (.calldatasize) => true
+            | .letVar _ (.calldataload _) => true
+            | .assignVar _ (.calldatasize) => true
+            | .assignVar _ (.calldataload _) => true
+            | .setStorage _ (.calldatasize) => true
+            | .setStorage _ (.calldataload _) => true
+            | .ite (.calldatasize) _ _ => true
+            | .ite (.calldataload _) _ _ => true
+            | .return (.calldatasize) => true
+            | .return (.calldataload _) => true
+            | _ => false)
+          s))
+    let expr ← Lean.Elab.Term.elabTermEnsuringType predicate (mkConst ``Bool)
+    match ← Lean.Meta.withTransparency .all (Lean.Meta.whnf expr) with
+    | .const ``Bool.true _ => pure true
+    | .const ``Bool.false _ => pure false
+    | _ =>
+        -- Syntax walk already ran; if the model predicate does not reduce,
+        -- keep the conservative syntax result (false here).
+        pure false
+
 private partial def syntaxCallsAnyHelper
     (helperNames : Array String) (stx : Syntax) : CommandElabM Bool := do
   match stx with
@@ -2629,15 +2678,135 @@ private def helperCallWithAdv (name : Ident) (args : Array Term) (adv : Term) :
     app ← `(term| $app $arg)
   pure app
 
+private def helperCall (name : Ident) (args : Array Term) : CommandElabM Term := do
+  let mut app : Term := ⟨name.raw⟩
+  for arg in args do
+    app ← `(term| $app $arg)
+  pure app
+
+private def identEndsWithSuffix (name : Name) (suffix : String) : Bool :=
+  let s := toString name
+  s == suffix || s.endsWith ("." ++ suffix)
+
+private partial def syntaxEndsWithSuffix (stx : Syntax) (suffix : String) : Bool :=
+  match stx with
+  | .ident _ _ name _ => identEndsWithSuffix name suffix
+  | .node _ kind args =>
+      if kind == ``Lean.Parser.Term.proj && args.size >= 3 then
+        syntaxEndsWithSuffix args[2]! suffix
+      else if args.isEmpty then
+        false
+      else
+        syntaxEndsWithSuffix args.back! suffix
+  | _ => false
+
+private def selfCallCallee? (t : Term) : CommandElabM (Option (Ident × Array Term)) := do
+  let calleeFrom (inner : Term) : CommandElabM (Option (Ident × Array Term)) := do
+    match stripParens inner with
+    | `(term| $fn:ident) => pure (some (fn, #[]))
+    | `(term| $fn:ident()) => pure (some (fn, #[]))
+    | `(term| $fn:ident($[$args:term],*)) => pure (some (fn, args))
+    | `(term| $fn:ident $args:term*) => pure (some (fn, args))
+    | _ => pure none
+  match t with
+  | `(term| selfCall $fn:ident) => pure (some (fn, #[]))
+  | `(term| selfCall $fn:ident($[$args:term],*)) => pure (some (fn, args))
+  | `(term| _root_.Verity.Contract.selfCall $inner:term) => calleeFrom inner
+  | `(term| Verity.Contract.selfCall $inner:term) => calleeFrom inner
+  | `(term| Contract.selfCall $inner:term) => calleeFrom inner
+  | `(term| $name:ident $inner:term) =>
+      if identEndsWithSuffix name.getId "selfCall" then
+        calleeFrom inner
+      else
+        pure none
+  | `(term| $name:ident($[$args:term],*)) =>
+      if identEndsWithSuffix name.getId "selfCall" && args.size == 1 then
+        calleeFrom ⟨args[0]!.raw⟩
+      else
+        pure none
+  | _ =>
+      match t.raw with
+      | .node _ kind args =>
+          if kind == ``Lean.Parser.Term.app && args.size >= 2 &&
+              syntaxEndsWithSuffix args[0]! "selfCall" then
+            calleeFrom ⟨args[1]!⟩
+          else
+            pure none
+      | _ => pure none
+
 private def threadHelperApp?
-    (adversarialHelpers : Array FunctionDecl) (name : Ident) (args : Array Term)
-    (adv : Term) : CommandElabM (Option Term) := do
-  let helper? := adversarialHelpers.find? fun fn =>
+    (fields : Array StorageFieldDecl)
+    (constDecls : Array ConstantDecl) (immutableDecls : Array ImmutableDecl)
+    (externalDecls : Array ExternalDecl)
+    (helpers : Array FunctionDecl) (adversarialHelpers : Array FunctionDecl)
+    (registryOnlyHelpers : Array FunctionDecl)
+    (params : Array ParamDecl) (locals : Array TypedLocal)
+    (name : Ident) (args : Array Term)
+    (adv : Term)
+    (originalArgsForOverload : Option (Array Term) := none)
+    (keepPublicGuard : Bool := false) : CommandElabM (Option Term) := do
+  let matchesHelper := fun (fn : FunctionDecl) =>
     (fn.name == toString name.getId || fn.ident.getId == name.getId ||
       (toString name.getId).endsWith ("." ++ fn.name)) &&
       fn.params.size == args.size
+  let matchesExactHelper := fun (fn : FunctionDecl) =>
+    (fn.name == toString name.getId || fn.ident.getId == name.getId) &&
+      fn.params.size == args.size
+  let exactCandidates := helpers.filter matchesExactHelper
+  let helper? ←
+    if exactCandidates.size <= 1 then
+      pure (exactCandidates[0]? <|> helpers.find? matchesHelper)
+    else
+      let resolveArgs := originalArgsForOverload.getD args
+      let app ← helperCall name resolveArgs
+      try
+        pure ((← resolveLocalFunctionApp? fields constDecls immutableDecls externalDecls
+          helpers params locals app).map (·.1))
+      catch _ =>
+        -- Validation reports ill-typed or ambiguous calls. If local binders keep
+        -- the argument types unavailable here, leave the original call intact
+        -- instead of selecting an overload by declaration order.
+        pure none
   match helper? with
-  | some _ => some <$> helperCallWithAdv name args adv
+  | some helper =>
+      if !matchesExactHelper helper then
+        -- A qualified application whose suffix happens to match a local helper
+        -- is not a local helper call.  Leave it to the recursive traversal so
+        -- linked calls nested in its arguments still receive the adversary.
+        return none
+      -- `registryOnlyHelpers` is the set that must be called as `_registry`
+      -- / `_registry_unguarded`. Public bodies pass `#[]`; registry bodies pass
+      -- every adversarial helper, including window-opening ones, so a nested
+      -- `hop` cannot drop into the stub-only public helper.
+      -- Same-contract `selfCall` is a public CALL: compiled dispatch still
+      -- runs the nonReentrant tload prologue, so hops keep the guarded
+      -- `*_registry` / public path rather than `*_unguarded`.
+      let registryOnly := registryOnlyHelpers.any (fun candidate =>
+        functionSignatureKey candidate == functionSignatureKey helper)
+      let target ←
+        if keepPublicGuard then
+          if registryOnly then
+            mkSuffixedIdent helper.ident "_registry"
+          else
+            pure helper.ident
+        else if registryOnly && helper.nonReentrantLock.isSome && helper.reentrancyTrusted then
+          mkSuffixedIdent helper.ident "_registry_unguarded"
+        else if registryOnly then
+          mkSuffixedIdent helper.ident "_registry"
+        else if helper.nonReentrantLock.isSome && helper.reentrancyTrusted &&
+            matchesExactHelper helper then
+          mkSuffixedIdent helper.ident "_unguarded"
+        else
+          pure helper.ident
+      if matchesExactHelper helper &&
+          (adversarialHelpers.any (fun candidate =>
+              functionSignatureKey candidate == functionSignatureKey helper) ||
+            registryOnly) then
+        some <$> helperCallWithAdv target args adv
+      else if helper.nonReentrantLock.isSome && helper.reentrancyTrusted then
+        some <$> helperCall target args
+      else
+        pure none
   | none => pure none
 
 /-- Resolve a `linked_contracts` binding for an executable typed call.
@@ -2821,21 +2990,31 @@ private def boundCalleeConstName (binding : LinkedContractDecl) (extName : Strin
 /-- Hop body for a bound typed call, and whether it must run as a view hop
     (storage-field getters are always view). -/
 private def boundCalleeBodyTerm (binding : LinkedContractDecl) (extName : String)
-    (args : Array Term) (adv : Term) (returnTys : Array ValueType := #[]) :
-    CommandElabM (Term × Bool) := do
+    (args : Array Term) (adv : Term) (returnTys : Array ValueType := #[])
+    (registryMode : Bool := false) : CommandElabM (Term × Bool) := do
   let method := typedExternalMethodName extName
-  let fnName := boundCalleeConstName binding extName
-  let fnIdent := mkIdent fnName
+  let publicName := boundCalleeConstName binding extName
+  let publicIdent := mkIdent publicName
   -- G23: a Solidity `public` state variable's getter is a storage field
   -- constant (`StorageSlot α`) in the callee, not a `Contract` function.
-  if let some (shape?, innerTy) ← storageSlotGetterShape? fnName then
-    let body ← storageGetterBodyTerm binding method fnIdent shape? innerTy args returnTys
+  -- Getters have no `*_registry` variant; they are pure storage reads.
+  if let some (shape?, innerTy) ← storageSlotGetterShape? publicName then
+    let body ← storageGetterBodyTerm binding method publicIdent shape? innerTy args returnTys
     return (body, true)
+  let registryIdent ← mkSuffixedIdent publicIdent "_registry"
+  -- Every generated `*_registry` executable takes `ExecutableCallContext`.
+  -- Do not gate on env lookup: the callee may live in another namespace, and
+  -- a missed lookup would silently keep the ctx-free public stub path.
+  let useRegistry := registryMode
+  let fnName := if useRegistry then registryIdent.getId else publicName
+  let fnIdent := mkIdent fnName
   let mut app : Term ← `(term| $fnIdent)
   -- Thread the caller's ExecutableCallContext into a bound callee that opens a
-  -- reentrancy window. Ctx-free callees (ModeledCallee.get/set) stay unchanged
-  -- so existing hopCall definitional theorems keep holding.
-  if ← constantTakesExecutableCallContext fnName then
+  -- reentrancy window, and in registry mode also into `*_registry` executables
+  -- of view/static callees (those take the context even when the public def
+  -- does not). Ctx-free public callees stay unchanged so existing hopCall
+  -- definitional theorems keep holding.
+  if useRegistry || (← constantTakesExecutableCallContext fnName) then
     app ← `(term| $app $adv)
   for arg in args do
     app ← `(term| $app $arg)
@@ -2848,7 +3027,7 @@ private def advTermIsFixedStub (adv : Term) : Bool :=
 private def hopBoundCallTerm?
     (linked : Array LinkedContractDecl) (target : Term) (targetName : String)
     (extName : String) (args : Array Term) (isView : Bool) (adv : Term)
-    (returnTys : Array ValueType := #[]) :
+    (returnTys : Array ValueType := #[]) (registryMode : Bool := false) :
     CommandElabM (Option Term) := do
   let some binding ← lookupLinkedBinding? linked targetName extName | return none
   if binding.isDeferred then
@@ -2859,6 +3038,7 @@ private def hopBoundCallTerm?
       throwError s!"internal error: deferred linked_contracts '{binding.name}' call '{extName}' reached a context-free body; the enclosing function must take the ExecutableCallContext"
     return none
   let (body, forceView) ← boundCalleeBodyTerm binding extName args adv returnTys
+    (registryMode := registryMode)
   if isView || forceView then
     some <$> `(term| _root_.Verity.Contract.hopCallView $target $body)
   else
@@ -2922,7 +3102,8 @@ private def rewriteTypedInterfaceCall?
     (externalDecls : Array ExternalDecl)
     (params : Array ParamDecl)
     (adv : Term) (stx : Term)
-    (linkedContracts : Array LinkedContractDecl := #[]) : CommandElabM (Option Term) := do
+    (linkedContracts : Array LinkedContractDecl := #[])
+    (registryMode : Bool := false) : CommandElabM (Option Term) := do
   let some (target, methodName, argTerms) := typedDotCallSyntax? stx | pure none
   let targetName ←
     match stripParens target with
@@ -2933,7 +3114,7 @@ private def rewriteTypedInterfaceCall?
   let some ext := externalDecls.find? (fun ext => ext.name == extName) | pure none
   let isView := externalDecls.any (fun candidate => candidate.name == extName && candidate.isView)
   match ← hopBoundCallTerm? linkedContracts target targetName extName argTerms isView adv
-      (returnTys := ext.returnTys) with
+      (returnTys := ext.returnTys) (registryMode := registryMode) with
   | some hop => return some hop
   | none => pure ()
   let siteId := natTerm (linkedExternalSiteId externalDecls extName)
@@ -2961,7 +3142,8 @@ private def rewriteTypedInterfaceCall?
 private def rewriteLinkedCallTerm
     (externalDecls : Array ExternalDecl) (params : Array ParamDecl)
     (adv : Term) (stx : Term)
-    (linkedContracts : Array LinkedContractDecl := #[]) : CommandElabM Term := do
+    (linkedContracts : Array LinkedContractDecl := #[])
+    (registryMode : Bool := false) : CommandElabM Term := do
   match stx with
   | `(term| __verityTypedCall $target:term $name:term [ $[$args:term],* ]) =>
       let extName ← expectStringOrIdent name
@@ -2973,7 +3155,7 @@ private def rewriteLinkedCallTerm
         | `(term| $targetIdent:ident) => pure (toString targetIdent.getId)
         | _ => pure ""
       match ← hopBoundCallTerm? linkedContracts target targetName extName args ext.isView adv
-          (returnTys := ext.returnTys) with
+          (returnTys := ext.returnTys) (registryMode := registryMode) with
       | some hop => return hop
       | none => pure ()
       let rewritten ← args.zip ext.params |>.mapM fun (arg, ty) => do
@@ -2999,7 +3181,7 @@ private def rewriteLinkedCallTerm
         | `(term| $targetIdent:ident) => pure (toString targetIdent.getId)
         | _ => pure ""
       match ← hopBoundCallTerm? linkedContracts target targetName extName args ext.isView adv
-          (returnTys := ext.returnTys) with
+          (returnTys := ext.returnTys) (registryMode := registryMode) with
       | some hop => return hop
       | none => pure ()
       let rewritten ← args.zip ext.params |>.mapM fun (arg, ty) => do
@@ -3127,6 +3309,16 @@ private def rewriteLinkedCallTerm
       `(term| evmDelegateCallWords $adv $gas $target $inOffset $inSize $outOffset $outSize)
   | `(term| returnDataSize()) | `(term| returndataSize) =>
       `(term| returndataSizeLive)
+  | `(term| calldatasize) =>
+      if registryMode then
+        `(term| calldatasizeLive)
+      else
+        pure stx
+  | `(term| calldataload $offset:term) =>
+      if registryMode then
+        `(term| calldataloadLive $offset)
+      else
+        pure stx
   | `(term| returnDataCopy($destOffset, $sourceOffset, $size))
     | `(term| returndataCopy $destOffset $sourceOffset $size) =>
       `(term| returndataCopyLive $destOffset $sourceOffset $size)
@@ -3188,11 +3380,12 @@ private def rewriteLinkedCallTerm
   | `(term| legacyStringSafeTransferFrom $token:term $fromAddr:term $toAddr:term $amount:term) =>
       `(term| legacyStringSafeTransferFrom $token $fromAddr $toAddr $amount $adv)
   | other =>
-      match ← rewriteTypedInterfaceCall? externalDecls params adv (linkedContracts := linkedContracts) ⟨other.raw⟩ with
+      match ← rewriteTypedInterfaceCall? externalDecls params adv
+          (linkedContracts := linkedContracts) (registryMode := registryMode) ⟨other.raw⟩ with
       | some rewritten => pure rewritten
       | none => pure other
 
-private def isLiveStateExternalCall (stx : Term) : Bool :=
+private def isLiveStateExternalCall (stx : Term) (registryMode : Bool := false) : Bool :=
   match stx with
   | `(term| __verityTypedCall $_ $_ [ $[$_],* ])
   | `(term| __verityTypedEffect $_ $_ [ $[$_],* ])
@@ -3222,6 +3415,7 @@ private def isLiveStateExternalCall (stx : Term) : Bool :=
   | `(term| safeApprove $_ $_ $_)
   | `(term| legacyStringSafeTransfer $_ $_ $_)
   | `(term| legacyStringSafeTransferFrom $_ $_ $_ $_) => true
+  | `(term| calldatasize) | `(term| calldataload $_) => registryMode
   | _ => false
 
 /-- Restore the source language's word-like coercions after a live external
@@ -3251,23 +3445,88 @@ private def adaptHoistedWordContext (stx : Term) : CommandElabM Term := do
   | _ => pure stx
 
 private partial def threadAdversaryThroughExecutableSyntax
+    (fields : Array StorageFieldDecl)
+    (constDecls : Array ConstantDecl) (immutableDecls : Array ImmutableDecl)
     (externalDecls : Array ExternalDecl)
+    (helpers : Array FunctionDecl)
     (adversarialHelpers : Array FunctionDecl)
+    (registryOnlyHelpers : Array FunctionDecl)
     (params : Array ParamDecl)
+    (locals : Array TypedLocal)
     (adv : Term) (stx : Syntax)
-    (linkedContracts : Array LinkedContractDecl := #[]) : CommandElabM Syntax := do
-  let go := threadAdversaryThroughExecutableSyntax externalDecls adversarialHelpers params adv
-    (linkedContracts := linkedContracts)
+    (linkedContracts : Array LinkedContractDecl := #[])
+    (registryMode : Bool := false) : CommandElabM Syntax := do
+  let go := threadAdversaryThroughExecutableSyntax fields constDecls immutableDecls
+    externalDecls helpers adversarialHelpers registryOnlyHelpers params locals adv
+    (linkedContracts := linkedContracts) (registryMode := registryMode)
   let recurseChildren : CommandElabM Syntax := do
     match stx with
     | .node info kind args =>
         pure (.node info kind (← args.mapM go))
     | _ => pure stx
   let rewriteTerm (t : Term) : CommandElabM Term := do
-    rewriteLinkedCallTerm externalDecls params adv t (linkedContracts := linkedContracts)
+    rewriteLinkedCallTerm externalDecls params adv t
+      (linkedContracts := linkedContracts) (registryMode := registryMode)
   let freshExternalIdent (origin : Term) : CommandElabM Ident :=
     Lean.Elab.Term.mkFreshIdent
       (mkIdentFrom origin.raw (Name.mkSimple "__verity_ext")).raw
+  let extendLocals (scope : Array TypedLocal) (elem : TSyntax `doElem) : CommandElabM (Array TypedLocal) := do
+    let infer (name : Ident) (rhs : Term) := do
+      try
+        let ty ←
+          match ← resolveLocalFunctionApp? fields constDecls immutableDecls externalDecls
+              helpers params scope rhs with
+          | some (helper, _) => pure helper.returnTy
+          | none => inferPureExprType fields constDecls immutableDecls externalDecls params scope rhs
+        pure (scope.push (mkTypedLocal (toString name.getId) ty))
+      catch _ => pure scope
+    let inferTuple (origin : Syntax) (names : Array (Option String)) (rhs : Term) := do
+      try
+        match ← resolveQualifiedFunctionApp? fields constDecls immutableDecls externalDecls
+            params scope rhs with
+        | some (qualifiedName, _) =>
+            let typedNames ← unsafe qualifiedTupleBindTypedLocals origin qualifiedName names
+            pure (scope ++ typedNames)
+        | none =>
+            match ← inferTupleSourceTypes? fields constDecls immutableDecls externalDecls
+                helpers params scope rhs with
+            | some valueTys =>
+                if names.size != valueTys.size then
+                  pure scope
+                else
+                  let typedNames := (names.zip valueTys).filterMap fun (name?, ty) =>
+                    name?.map (fun name => mkTypedLocal name ty)
+                  pure (scope ++ typedNames)
+            | none => pure scope
+      catch _ => pure scope
+    let tupleScope? ← do
+      let stx := elem.raw
+      if stx.getKind == `Lean.Parser.Term.doLet then
+        let patDecl := stx[3][0]
+        match tupleBinderNames? patDecl[0] with
+        | some names => pure (some (← inferTuple patDecl names ⟨patDecl[4]⟩))
+        | none => pure none
+      else if stx.getKind == `Lean.Parser.Term.doLetArrow then
+        let patDecl := stx[3]
+        match tupleBinderNames? patDecl[0] with
+        | some names => pure (some (← inferTuple patDecl names ⟨patDecl[3][0]⟩))
+        | none => pure none
+      else
+        pure none
+    match tupleScope? with
+    | some tupleScope => pure tupleScope
+    | none => match elem with
+      | `(doElem| let $name:ident : Uint256 := $_rhs:term) =>
+          pure (scope.push (mkTypedLocal (toString name.getId) .uint256))
+      | `(doElem| let $name:ident := $rhs:term) => infer name rhs
+      | `(doElem| let mut $name:ident := $rhs:term) => infer name rhs
+      | `(doElem| let $name:ident ← $rhs:term) =>
+          try
+            let ty ← inferBindSourceType fields constDecls immutableDecls externalDecls
+              helpers params scope rhs
+            pure (scope.push (mkTypedLocal (toString name.getId) ty))
+          catch _ => pure scope
+      | _ => pure scope
   let rec hoistNested (bindSelf : Bool) (t : Term) :
       CommandElabM (Array (Ident × Term) × Term) := do
     let bindCall (binds : Array (Ident × Term)) (call : Term) :
@@ -3283,6 +3542,26 @@ private partial def threadAdversaryThroughExecutableSyntax
       for (tmp, call) in binds.reverse do
         body ← `(term| _root_.Verity.bind $call (fun $tmp => $body))
       pure body
+    if let some (fn, args) := (← selfCallCallee? t) then
+      let original := args
+      let mut binds : Array (Ident × Term) := #[]
+      let mut hoisted : Array Term := #[]
+      for arg in args do
+        let (inner, rewritten) ← hoistNested true arg
+        binds := binds ++ inner
+        hoisted := hoisted.push rewritten
+      match ← threadHelperApp? fields constDecls immutableDecls externalDecls
+          helpers adversarialHelpers registryOnlyHelpers params locals fn hoisted adv
+          (originalArgsForOverload := original) (keepPublicGuard := true) with
+      | some app =>
+          return (binds, ← `(term| _root_.Verity.Contract.selfCall $app))
+      | none =>
+          let inner ←
+            if hoisted.isEmpty then
+              `(term| $fn:ident())
+            else
+              helperCall fn hoisted
+          return (binds, ← `(term| _root_.Verity.Contract.selfCall $inner))
     match t with
     | `(term| fun $name:ident => $body:term) =>
         let bodyRaw : Syntax ← go body.raw
@@ -3293,18 +3572,39 @@ private partial def threadAdversaryThroughExecutableSyntax
         let rewrittenBody : TSyntax ``Lean.Parser.Term.doSeq := ⟨bodyRaw⟩
         pure (#[], ← `(term| do $rewrittenBody))
     | `(term| $name:ident($[$args:term],*)) =>
-        match ← threadHelperApp? adversarialHelpers name args adv with
-        | some app => pure (#[], app)
+        let original := args.map fun a => (⟨a.raw⟩ : Term)
+        -- Resolve overloads using original source arguments so mangled helper.idents
+        -- for non-guarded adversarial overloads are selected before hoisting rewrites the args.
+        match ← threadHelperApp? fields constDecls immutableDecls externalDecls
+            helpers adversarialHelpers registryOnlyHelpers params locals name original adv with
+        | some _selectedApp =>
+            -- Now hoist nested external-call arguments (or type generated locals soundly),
+            -- then thread the selected helper using the hoisted arguments.
+            let mut binds : Array (Ident × Term) := #[]
+            let mut hoisted : Array Term := #[]
+            for arg in args do
+              let (inner, rewritten) ← hoistNested true arg
+              binds := binds ++ inner
+              hoisted := hoisted.push rewritten
+            match ← threadHelperApp? fields constDecls immutableDecls externalDecls
+                helpers adversarialHelpers registryOnlyHelpers params locals name hoisted adv
+                (originalArgsForOverload := original) with
+            | some app => pure (binds, app)
+            | none =>
+                let mut app : Term := ⟨name.raw⟩
+                for h in hoisted do
+                  app ← `(term| $app $h)
+                pure (binds, app)
         | none =>
             let mut binds : Array (Ident × Term) := #[]
-            let mut rewrittenArgs : Array Term := #[]
+            let mut hoisted : Array Term := #[]
             for arg in args do
               let (inner, rewritten) ← hoistNested true arg
               binds := binds ++ inner
-              rewrittenArgs := rewrittenArgs.push rewritten
+              hoisted := hoisted.push rewritten
             let mut app : Term := ⟨name.raw⟩
-            for arg in rewrittenArgs do
-              app ← `(term| $app $arg)
+            for h in hoisted do
+              app ← `(term| $app $h)
             pure (binds, app)
     | `(term| if $cond:term then $thenValue:term else $elseValue:term) =>
         let (condBinds, rewrittenCond) ← hoistNested true cond
@@ -3327,10 +3627,11 @@ private partial def threadAdversaryThroughExecutableSyntax
           binds := binds ++ inner
           newArgs := newArgs.set! i nt.raw
         let rebuilt ← adaptHoistedWordContext ⟨Syntax.node info kind newArgs⟩
-        if isLiveStateExternalCall rebuilt then
+        if isLiveStateExternalCall rebuilt registryMode then
           bindCall binds rebuilt
         else
-          match ← rewriteTypedInterfaceCall? externalDecls params adv (linkedContracts := linkedContracts) rebuilt with
+          match ← rewriteTypedInterfaceCall? externalDecls params adv
+              (linkedContracts := linkedContracts) (registryMode := registryMode) rebuilt with
           | some rewritten =>
               if bindSelf then
                 let tmp ← freshExternalIdent t
@@ -3339,10 +3640,11 @@ private partial def threadAdversaryThroughExecutableSyntax
                 pure (binds, rewritten)
           | none => pure (binds, rebuilt)
       | _ =>
-        if isLiveStateExternalCall t then
+        if isLiveStateExternalCall t registryMode then
           bindCall #[] t
         else
-          match ← rewriteTypedInterfaceCall? externalDecls params adv (linkedContracts := linkedContracts) t with
+          match ← rewriteTypedInterfaceCall? externalDecls params adv
+              (linkedContracts := linkedContracts) (registryMode := registryMode) t with
           | some rewritten =>
               if bindSelf then
                 let tmp ← freshExternalIdent t
@@ -3379,7 +3681,37 @@ private partial def threadAdversaryThroughExecutableSyntax
       | stripped => stripped
     let rest ← if outerWasBound then pureBinding pureValue else monadic rewritten
     wrapBinds binds rest
+  if let some (fn, args) := (← selfCallCallee? ⟨stx⟩) then
+    let original := args
+    let mut binds : Array (Ident × Term) := #[]
+    let mut hoisted : Array Term := #[]
+    for arg in args do
+      let (inner, rewritten) ← hoistNested true arg
+      binds := binds ++ inner
+      hoisted := hoisted.push rewritten
+    match ← threadHelperApp? fields constDecls immutableDecls externalDecls
+        helpers adversarialHelpers registryOnlyHelpers params locals fn hoisted adv
+        (originalArgsForOverload := original) (keepPublicGuard := true) with
+    | some app =>
+        return (← wrapBinds binds (← `(doElem| _root_.Verity.Contract.selfCall $app))).raw
+    | none =>
+        let inner ←
+          if hoisted.isEmpty then
+            `(term| $fn:ident())
+          else
+            helperCall fn hoisted
+        return (← wrapBinds binds (← `(doElem| _root_.Verity.Contract.selfCall $inner))).raw
   match stx with
+  | `(doSeq| $[$elems:doElem]*) =>
+      let mut scope := locals
+      let mut rewritten : Array (TSyntax `doElem) := #[]
+      for elem in elems do
+        let raw ← threadAdversaryThroughExecutableSyntax fields constDecls immutableDecls
+          externalDecls helpers adversarialHelpers registryOnlyHelpers params scope adv elem.raw
+          (linkedContracts := linkedContracts) (registryMode := registryMode)
+        rewritten := rewritten.push ⟨raw⟩
+        scope ← extendLocals scope elem
+      `(doSeq| $[$rewritten:doElem]*)
   | `(doElem| let $pat:term ← tryExternalCall $name:term [ $[$args:term],* ]) =>
       let mut binds : Array (Ident × Term) := #[]
       let mut rewrittenArgs : Array Term := #[]
@@ -3388,7 +3720,7 @@ private partial def threadAdversaryThroughExecutableSyntax
         binds := binds ++ inner
         rewrittenArgs := rewrittenArgs.push rewritten
       let call ← `(term| tryExternalCall $name [ $[$rewrittenArgs],* ])
-      let rewritten ← rewriteLinkedCallTerm externalDecls params adv (linkedContracts := linkedContracts) call
+      let rewritten ← rewriteLinkedCallTerm externalDecls params adv (linkedContracts := linkedContracts) (registryMode := registryMode) call
       wrapBinds binds (← `(doElem| let $pat:term ← $rewritten:term))
   | `(doElem| let $pat:term ← callResult $name:term [ $[$args:term],* ]) =>
       let mut binds : Array (Ident × Term) := #[]
@@ -3398,7 +3730,7 @@ private partial def threadAdversaryThroughExecutableSyntax
         binds := binds ++ inner
         rewrittenArgs := rewrittenArgs.push rewritten
       let call ← `(term| callResult $name [ $[$rewrittenArgs],* ])
-      let rewritten ← rewriteLinkedCallTerm externalDecls params adv (linkedContracts := linkedContracts) call
+      let rewritten ← rewriteLinkedCallTerm externalDecls params adv (linkedContracts := linkedContracts) (registryMode := registryMode) call
       wrapBinds binds (← `(doElem| let $pat:term ← $rewritten:term))
   | `(doElem| let $pat:term ← callExternal $name:ident ($[$args:term],*)) =>
       let mut binds : Array (Ident × Term) := #[]
@@ -3408,7 +3740,7 @@ private partial def threadAdversaryThroughExecutableSyntax
         binds := binds ++ inner
         rewrittenArgs := rewrittenArgs.push rewritten
       let call ← `(term| callExternal $name ($[$rewrittenArgs],*))
-      let rewritten ← rewriteLinkedCallTerm externalDecls params adv (linkedContracts := linkedContracts) call
+      let rewritten ← rewriteLinkedCallTerm externalDecls params adv (linkedContracts := linkedContracts) (registryMode := registryMode) call
       wrapBinds binds (← `(doElem| let $pat:term ← $rewritten:term))
   | `(doElem| let $pat:term ← balanceOf $token:term $owner:term) =>
       let (tokenBinds, rewrittenToken) ← hoistNested true token
@@ -3430,8 +3762,22 @@ private partial def threadAdversaryThroughExecutableSyntax
         (← `(doElem| let $pat:term ← (totalSupply
           (externalArgAddress $rewrittenToken) $adv)))
   | `(doElem| let $name:ident ← $fn:ident($[$args:term],*)) =>
-      match ← threadHelperApp? adversarialHelpers fn args adv with
-      | some app => `(doElem| let $name ← $app:term)
+      let original := args.map fun a => (⟨a.raw⟩ : Term)
+      -- Resolve overload using original source args (r3956459377), hoist after selection (r3956459383)
+      match ← threadHelperApp? fields constDecls immutableDecls externalDecls
+          helpers adversarialHelpers registryOnlyHelpers params locals fn original adv with
+      | some _ =>
+          let mut binds : Array (Ident × Term) := #[]
+          let mut hoisted : Array Term := #[]
+          for a in args do
+            let (inner, h) ← hoistNested true a
+            binds := binds ++ inner
+            hoisted := hoisted.push h
+          match ← threadHelperApp? fields constDecls immutableDecls externalDecls
+              helpers adversarialHelpers registryOnlyHelpers params locals fn hoisted adv
+              (originalArgsForOverload := original) with
+          | some app => wrapBinds binds (← `(doElem| let $name ← $app:term))
+          | none => recurseChildren
       | none => recurseChildren
   | `(doElem| let $name:ident ← $fn:ident $args:term*) =>
       let original := args.map fun arg => (⟨arg.raw⟩ : Term)
@@ -3455,14 +3801,15 @@ private partial def threadAdversaryThroughExecutableSyntax
         wrapBinds binds
           (← `(doElem| let $name ← (totalSupply (externalArgAddress $token) $adv)))
       else
-        match ← threadHelperApp? adversarialHelpers fn original adv with
+        match ← threadHelperApp? fields constDecls immutableDecls externalDecls
+            helpers adversarialHelpers registryOnlyHelpers params locals fn original adv with
         | some app =>
             hoistLive false app fun rewritten => `(doElem| let $name ← $rewritten:term)
         | none =>
           if fnName == "__verityTypedCall" then
             match stx with
             | `(doElem| let $_ ← $rhs:term) =>
-                let rewritten ← rewriteLinkedCallTerm externalDecls params adv (linkedContracts := linkedContracts) rhs
+                let rewritten ← rewriteLinkedCallTerm externalDecls params adv (linkedContracts := linkedContracts) (registryMode := registryMode) rhs
                 `(doElem| let $name ← $rewritten:term)
             | _ => recurseChildren
           else if fnName == "tryExternalCall" || fnName == "callResult" || fnName == "callExternal"
@@ -3488,9 +3835,12 @@ private partial def threadAdversaryThroughExecutableSyntax
       -- form above; everything else keeps the generic hoisting path.
       let helperApp? ← match rhs with
         | `(term| $fn:ident $args:term*) =>
-            threadHelperApp? adversarialHelpers fn (args.map fun arg => (⟨arg.raw⟩ : Term)) adv
+            threadHelperApp? fields constDecls immutableDecls externalDecls
+              helpers adversarialHelpers registryOnlyHelpers params locals fn
+              (args.map fun arg => (⟨arg.raw⟩ : Term)) adv
         | `(term| $fn:ident($[$args:term],*)) =>
-            threadHelperApp? adversarialHelpers fn args adv
+            threadHelperApp? fields constDecls immutableDecls externalDecls
+              helpers adversarialHelpers registryOnlyHelpers params locals fn args adv
         | _ => pure none
       match helperApp? with
       | some app =>
@@ -3607,32 +3957,35 @@ private partial def threadAdversaryThroughExecutableSyntax
       if toString fn.getId == "__verityTypedEffect" then
         match stx with
         | `(doElem| $rhs:term) =>
-            let rewritten ← rewriteLinkedCallTerm externalDecls params adv (linkedContracts := linkedContracts) rhs
+            let rewritten ← rewriteLinkedCallTerm externalDecls params adv (linkedContracts := linkedContracts) (registryMode := registryMode) rhs
             `(doElem| $rewritten:term)
         | _ => recurseChildren
-      else match ← threadHelperApp? adversarialHelpers fn original adv with
-      | some app =>
-          hoistLive false app fun rewritten => `(doElem| $rewritten:term)
-      | none =>
-          match stx with
-          | `(doElem| $stmt:term) =>
-              hoistLive false stmt fun rewritten => `(doElem| $rewritten:term)
-          | _ => recurseChildren
+      else
+        match ← threadHelperApp? fields constDecls immutableDecls externalDecls
+          helpers adversarialHelpers registryOnlyHelpers params locals fn original adv with
+        | some app =>
+            hoistLive false app fun rewritten => `(doElem| $rewritten:term)
+        | none =>
+            match stx with
+            | `(doElem| $stmt:term) =>
+                hoistLive false stmt fun rewritten => `(doElem| $rewritten:term)
+            | _ => recurseChildren
   | `(doElem| $stmt:term) =>
       hoistLive false stmt fun rewritten => `(doElem| $rewritten:term)
   | `(term| $name:ident $args:term*) =>
       let original := args.map fun arg => (⟨arg.raw⟩ : Term)
-      match ← threadHelperApp? adversarialHelpers name original adv with
+      match ← threadHelperApp? fields constDecls immutableDecls externalDecls
+          helpers adversarialHelpers registryOnlyHelpers params locals name original adv with
       | some app => pure app.raw
       | none =>
-          if isLiveStateExternalCall ⟨stx⟩ then
-            (·.raw) <$> rewriteLinkedCallTerm externalDecls params adv (linkedContracts := linkedContracts) ⟨stx⟩
+          if isLiveStateExternalCall ⟨stx⟩ registryMode then
+            (·.raw) <$> rewriteLinkedCallTerm externalDecls params adv (linkedContracts := linkedContracts) (registryMode := registryMode) ⟨stx⟩
           else
             recurseChildren
   | _ =>
       let asTerm : Term := ⟨stx⟩
-      if isLiveStateExternalCall asTerm then
-        (·.raw) <$> rewriteLinkedCallTerm externalDecls params adv (linkedContracts := linkedContracts) asTerm
+      if isLiveStateExternalCall asTerm registryMode then
+        (·.raw) <$> rewriteLinkedCallTerm externalDecls params adv (linkedContracts := linkedContracts) (registryMode := registryMode) asTerm
       else
         recurseChildren
 
@@ -5898,6 +6251,74 @@ def mkStructExternalArgInstanceCommandPublic (decl : StructDecl) : CommandElabM
         ([ $[$encodedFields],* ] :
           List (List _root_.Verity.Uint256)))
 
+/-- Compile-time DispatchVal from a declared `ValueType`, so `FixedArray`
+encodes as a tuple (no `T[]` length) and `Tuple` flattens rather than
+following the right-nested Lean product instance. -/
+private def scalarLoadKindTerm : ValueType → CommandElabM Term
+  | .bool => `(Compiler.CompilationModel.DenoteExternalCalls.ScalarLoadKind.bool)
+  | .uint8 => `(Compiler.CompilationModel.DenoteExternalCalls.ScalarLoadKind.uint8)
+  | .uint16 => `(Compiler.CompilationModel.DenoteExternalCalls.ScalarLoadKind.uint16)
+  | .uintN bits =>
+      `(Compiler.CompilationModel.DenoteExternalCalls.ScalarLoadKind.uintN $(natTerm bits))
+  | .address => `(Compiler.CompilationModel.DenoteExternalCalls.ScalarLoadKind.address)
+  | .bytesN bytes =>
+      `(Compiler.CompilationModel.DenoteExternalCalls.ScalarLoadKind.bytesN $(natTerm bytes))
+  | _ => `(Compiler.CompilationModel.DenoteExternalCalls.ScalarLoadKind.identity)
+
+private partial def dispatchValTermForType (ty : ValueType) (value : Term) : CommandElabM Term :=
+  match ty with
+  | .fixedArray elemTy size => do
+      let mut elems : Array Term := #[]
+      for i in [:size] do
+        let elem ← `(term| Array.getD $value $(natTerm i) default)
+        elems := elems.push (← dispatchValTermForType elemTy elem)
+      if elems.isEmpty then
+        `(term| Compiler.CompilationModel.DenoteExternalCalls.dispatchFixedArray
+            ([] : List Compiler.CompilationModel.DenoteExternalCalls.DispatchVal))
+      else
+        `(term| Compiler.CompilationModel.DenoteExternalCalls.dispatchFixedArray
+            ([ $[$elems],* ] : List Compiler.CompilationModel.DenoteExternalCalls.DispatchVal))
+  | .tuple elemTys => do
+      let mut elems : Array Term := #[]
+      let mut rest : Term := value
+      let mut idx : Nat := 0
+      for elemTy in elemTys do
+        let elem ←
+          if idx + 1 == elemTys.length then
+            pure rest
+          else do
+            let head ← `(term| Prod.fst $rest)
+            rest ← `(term| Prod.snd $rest)
+            pure head
+        elems := elems.push (← dispatchValTermForType elemTy elem)
+        idx := idx + 1
+      `(term| Compiler.CompilationModel.DenoteExternalCalls.dispatchFlatTuple
+          (Compiler.CompilationModel.DenoteExternalCalls.DispatchVal.tuple
+            ([ $[$elems],* ] : List Compiler.CompilationModel.DenoteExternalCalls.DispatchVal)))
+  | .array elemTy => do
+      `(term| Compiler.CompilationModel.DenoteExternalCalls.DispatchVal.array
+          (($value).toList.map (fun x =>
+            Compiler.CompilationModel.DenoteExternalCalls.ToDispatchVal.toDispatchVal
+              (x : $(← contractValueTypeTerm elemTy)))))
+  | _ =>
+      `(term| Compiler.CompilationModel.DenoteExternalCalls.ToDispatchVal.toDispatchVal
+        $value)
+
+/-- Compiled-dispatch ABI encoding of a named struct: the tuple of its
+fields, matching `genParamLoads` / `abiEncodeDispatchArgs`. -/
+def mkStructToDispatchValInstanceCommandPublic (decl : StructDecl) : CommandElabM Cmd := do
+  let structId := decl.ident
+  let valueId := mkIdent (Name.mkSimple "value")
+  let fieldIds := decl.fields.map (·.ident)
+  let encodedFields ← fieldIds.mapM fun fieldId =>
+    `(term| Compiler.CompilationModel.DenoteExternalCalls.ToDispatchVal.toDispatchVal
+      $valueId.$fieldId)
+  `(command| instance : Compiler.CompilationModel.DenoteExternalCalls.ToDispatchVal $structId where
+      toDispatchVal := fun $valueId =>
+        Compiler.CompilationModel.DenoteExternalCalls.DispatchVal.tuple
+          ([ $[$encodedFields],* ] :
+            List Compiler.CompilationModel.DenoteExternalCalls.DispatchVal))
+
 def mkStructExternalResultInstanceCommandPublic (decl : StructDecl) : CommandElabM Cmd := do
   let structId := decl.ident
   let fieldIds := decl.fields.map (·.ident)
@@ -5935,11 +6356,13 @@ def validateConstantDeclsPublic (constDecls : Array ConstantDecl) : CommandElabM
   validateConstantExprTypes constDecls
 
 def validateGeneratedDefNamesPublic
+    (structDecls : Array StructDecl)
     (fields : Array StorageFieldDecl)
     (constDecls : Array ConstantDecl)
     (immutableDecls : Array ImmutableDecl)
+    (modifiers : Array ModifierDecl)
     (functions : Array FunctionDecl) : CommandElabM Unit := do
-  let reservedGeneratedNames : Array String := #["spec", "storageNamespace"]
+  let reservedGeneratedNames : Array String := #["spec", "storageNamespace", "entrypointRegistry"]
   let mut generatedHelperNames : Array String := reservedGeneratedNames
   if hasStructMapping fields then
     generatedHelperNames := generatedHelperNames.push "structMember"
@@ -6023,6 +6446,8 @@ def validateGeneratedDefNamesPublic
 
     let helperNames :=
       #[ s!"{generatedFnName}_modelBody"
+       , s!"{generatedFnName}_entrypoint"
+       , s!"{generatedFnName}_registry"
        , s!"{generatedFnName}_model"
        , s!"{generatedFnName}_bridge"
        , s!"{generatedFnName}_semantic_preservation"
@@ -6038,6 +6463,12 @@ def validateGeneratedDefNamesPublic
        , s!"{generatedFnName}_requires_role"
        , s!"{generatedFnName}_access_control"
        ]
+    let helperNames :=
+      if fn.nonReentrantLock.isSome && fn.reentrancyTrusted then
+        (helperNames.push s!"{generatedFnName}_unguarded").push
+          s!"{generatedFnName}_registry_unguarded"
+      else
+        helperNames
     for helperName in helperNames do
       if storageNames.contains helperName then
         throwErrorAt fn.ident
@@ -6056,6 +6487,15 @@ def validateGeneratedDefNamesPublic
           s!"function '{fn.name}' generates duplicate helper declaration '{helperName}'"
       generatedHelperNames := generatedHelperNames.push helperName
 
+  for structDecl in structDecls do
+    if generatedHelperNames.contains structDecl.name then
+      throwErrorAt structDecl.ident
+        s!"struct '{structDecl.name}' conflicts with generated declaration '{structDecl.name}'"
+  for modifierDecl in modifiers do
+    if generatedHelperNames.contains modifierDecl.name then
+      throwErrorAt modifierDecl.ident
+        s!"modifier '{modifierDecl.name}' conflicts with generated declaration '{modifierDecl.name}'"
+
 def validateImmutableDeclsPublic
     (fields : Array StorageFieldDecl)
     (constDecls : Array ConstantDecl)
@@ -6285,7 +6725,8 @@ private def constructorAdversarialHelpers
     let mut grew := false
     for helper in functions do
       let callsAdversarial ← syntaxCallsAnyHelper names helper.body.raw
-      if !adversarial.any (fun candidate => candidate.name == helper.name) &&
+      if !adversarial.any (fun candidate =>
+            functionSignatureKey candidate == functionSignatureKey helper) &&
           callsAdversarial then
         adversarial := adversarial.push helper
         grew := true
@@ -6312,8 +6753,9 @@ def mkConstructorDefCommandPublic
       pure ⟨advIdent.raw⟩
     else
       `(Compiler.CompilationModel.DenoteExternalCalls.AdversaryModel.stub)
-  let executableBody := ⟨← threadAdversaryThroughExecutableSyntax externalDecls adversarialHelpers
-    ctor.params advTerm executableBody.raw (linkedContracts := linkedContracts)⟩
+  let executableBody := ⟨← threadAdversaryThroughExecutableSyntax fields constDecls immutableDecls
+    externalDecls functions adversarialHelpers #[] ctor.params #[] advTerm executableBody.raw
+    (linkedContracts := linkedContracts)⟩
   let fnType ← if opensReentrancyWindow then
       mkContractFnTypeWithAdversary ctor.params .unit
     else
@@ -6383,8 +6825,9 @@ def mkHostConstructorDefCommandPublic
             preludes := preludes.push (← `(doElem| $tgt:ident $args*))
       let body ← `(term| do $[$preludes:doElem]* $[$elems:doElem]*)
       let executableBody ← rewriteForEachExecutableBody fields externalDecls ctor.params body
-      let executableBody := ⟨← threadAdversaryThroughExecutableSyntax externalDecls ownAdversarialHelpers
-        ctor.params advTerm executableBody.raw (linkedContracts := linkedContracts)⟩
+      let executableBody := ⟨← threadAdversaryThroughExecutableSyntax fields constDecls immutableDecls
+        externalDecls functions ownAdversarialHelpers #[] ctor.params #[] advTerm executableBody.raw
+        (linkedContracts := linkedContracts)⟩
       let fnValue ← if containsExternalCall then
           mkContractFnValueWithAdversary advIdent ctor.params executableBody
         else
@@ -6410,6 +6853,20 @@ def mkIncludeAliasCommandsPublic
           unless fn.isInternal do
             let tgt := mkIdent (mixinName ++ fn.ident.getId)
             cmds := cmds.push (← `(command| abbrev $(fn.ident) := $tgt))
+            let predicateId ← mkSuffixedIdent fn.ident "_entrypoint"
+            let predicateTgt ← mkSuffixedIdent tgt "_entrypoint"
+            cmds := cmds.push (← `(command| abbrev $predicateId := $predicateTgt))
+            let registryId ← mkSuffixedIdent fn.ident "_registry"
+            let registryTgt ← mkSuffixedIdent tgt "_registry"
+            cmds := cmds.push (← `(command| abbrev $registryId := $registryTgt))
+            if fn.nonReentrantLock.isSome && fn.reentrancyTrusted then
+              let unguardedId ← mkSuffixedIdent fn.ident "_unguarded"
+              let unguardedTgt ← mkSuffixedIdent tgt "_unguarded"
+              cmds := cmds.push (← `(command| abbrev $unguardedId := $unguardedTgt))
+              let registryUnguardedId ← mkSuffixedIdent fn.ident "_registry_unguarded"
+              let registryUnguardedTgt ← mkSuffixedIdent tgt "_registry_unguarded"
+              cmds := cmds.push
+                (← `(command| abbrev $registryUnguardedId := $registryUnguardedTgt))
         for modDecl in mixin.modifiers do
           unless modifierContainsExternalCallSyntaxPublic modDecl do
             let tgt := mkIdent (mixinName ++ modDecl.ident.getId)
@@ -6482,13 +6939,19 @@ def mkFunctionCommandsPublic
       | some inlined => pure inlined
       | none => pure fn
   let stmtTerms ← translateBodyToStmtTerms fields roleDecls errorDecls constDecls immutableDecls externalDecls functions modelFn
-  -- "Takes the ExecutableCallContext" = opens a reentrancy window (model
-  -- plane) OR issues a typed call on a `deferred` binding (G15, executable
-  -- plane only); both are propagated through the helper fixed point below.
+  -- "Takes the ExecutableCallContext" on the public path = opens a reentrancy
+  -- window (model plane) OR issues a typed call on a `deferred` binding (G15,
+  -- executable plane only); both are propagated through the helper fixed point
+  -- below. Executable registry transitions (`*_registry`) additionally use the
+  -- explicit adversary for every external-call-dependent result, including
+  -- static calls whose returndata can influence a later storage write; that
+  -- wider set is `adversarialHelpers`.
   let directlyOpensReentrancyWindow ←
     pure ((← translatedBodyOpensReentrancyWindow stmtTerms) ||
       (← bodyNeedsLinkedCallContext externalDecls fn.params linkedContracts fnExecutableBody.raw))
   let mut adversarialHelpers : Array FunctionDecl := #[]
+  let mut windowHelpers : Array FunctionDecl := #[]
+  let mut calldataHelpers : Array FunctionDecl := #[]
   let mut translatedHelpers : Array (FunctionDecl × FunctionDecl) := #[]
   for helper in functions do
     let helperModel ←
@@ -6503,9 +6966,15 @@ def mkFunctionCommandsPublic
       immutableDecls externalDecls functions helperModel
     translatedHelpers := translatedHelpers.push (helper, helperModel)
     let helperExecutableBody ← rewriteForEachExecutableBody fields externalDecls helper.params helper.body
-    if (← translatedBodyOpensReentrancyWindow helperStmtTerms) ||
-        (← bodyNeedsLinkedCallContext externalDecls helper.params linkedContracts helperExecutableBody.raw) then
+    let helperNeedsLinkedCtx ←
+      bodyNeedsLinkedCallContext externalDecls helper.params linkedContracts helperExecutableBody.raw
+    if (← translatedBodyContainsExternalCall helperStmtTerms) || helperNeedsLinkedCtx then
       adversarialHelpers := adversarialHelpers.push helper
+    if (← translatedBodyOpensReentrancyWindow helperStmtTerms) || helperNeedsLinkedCtx then
+      windowHelpers := windowHelpers.push helper
+    if syntaxContainsCalldataRead helperModel.body.raw ||
+        (← translatedBodyContainsCalldataRead helperStmtTerms) then
+      calldataHelpers := calldataHelpers.push helper
   -- Reentrancy-window capability is transitive across internal helpers. Iterate to a
   -- fixed point so every caller in a multi-hop helper chain receives and forwards
   -- the same adversary instead of silently falling back to the stub.
@@ -6514,16 +6983,45 @@ def mkFunctionCommandsPublic
     let mut grew := false
     for (helper, helperModel) in translatedHelpers do
       let callsAdversarial ← syntaxCallsAnyHelper adversarialNames helperModel.body.raw
-      if !adversarialHelpers.any (fun candidate => candidate.name == helper.name) &&
+      if !adversarialHelpers.any (fun candidate =>
+            functionSignatureKey candidate == functionSignatureKey helper) &&
           callsAdversarial then
         adversarialHelpers := adversarialHelpers.push helper
         grew := true
     if !grew then
       break
-  let adversarialNames := adversarialHelpers.map (·.name)
-  let callsAdversarial ← syntaxCallsAnyHelper adversarialNames modelFn.body.raw
-  let opensReentrancyWindow := directlyOpensReentrancyWindow ||
-    callsAdversarial
+  for _ in [:functions.size] do
+    let windowNames := windowHelpers.map (·.name)
+    let mut grew := false
+    for (helper, helperModel) in translatedHelpers do
+      let callsWindow ← syntaxCallsAnyHelper windowNames helperModel.body.raw
+      if !windowHelpers.any (fun candidate =>
+            functionSignatureKey candidate == functionSignatureKey helper) &&
+          callsWindow then
+        windowHelpers := windowHelpers.push helper
+        grew := true
+    if !grew then
+      break
+  for _ in [:functions.size] do
+    let calldataNames := calldataHelpers.map (·.name)
+    let mut grew := false
+    for (helper, helperModel) in translatedHelpers do
+      let callsCalldata ← syntaxCallsAnyHelper calldataNames helperModel.body.raw
+      if !calldataHelpers.any (fun candidate =>
+            functionSignatureKey candidate == functionSignatureKey helper) &&
+          callsCalldata then
+        calldataHelpers := calldataHelpers.push helper
+        grew := true
+    if !grew then
+      break
+  let mut registryOnlyHelpers : Array FunctionDecl := adversarialHelpers
+  for helper in calldataHelpers do
+    if !registryOnlyHelpers.any (fun candidate =>
+          functionSignatureKey candidate == functionSignatureKey helper) then
+      registryOnlyHelpers := registryOnlyHelpers.push helper
+  let windowNames := windowHelpers.map (·.name)
+  let callsWindow ← syntaxCallsAnyHelper windowNames modelFn.body.raw
+  let opensReentrancyWindow := directlyOpensReentrancyWindow || callsWindow
   -- Keep the generated binder hygienic: source parameters and locals are allowed
   -- to use `_adv` without capturing the adversary threaded into rewritten calls.
   let advIdent ← Lean.Elab.Term.mkFreshIdent (mkIdentFrom fn.ident `_adv).raw
@@ -6535,13 +7033,59 @@ def mkFunctionCommandsPublic
       mkContractFnTypeWithAdversary fn.params fn.returnTy
     else
       mkContractFnType fn.params fn.returnTy
-  let fnExecutableBody := ⟨← threadAdversaryThroughExecutableSyntax externalDecls
-    adversarialHelpers fn.params advTerm fnExecutableBody.raw
+  let publicExecutableBody := ⟨← threadAdversaryThroughExecutableSyntax fields constDecls immutableDecls
+    externalDecls functions windowHelpers #[] fn.params #[] advTerm fnExecutableBody.raw
     (linkedContracts := linkedContracts)⟩
+  -- Registry executables must route every adversarial helper, including
+  -- window-opening helpers, to `_registry` / `_registry_unguarded`. Restricting
+  -- the suffix to non-window helpers let `entry_registry` call public `hop`,
+  -- which then used stub-only nested view helpers and under-approximated the
+  -- compiled callee-controlled ECM. Calldata-reading helpers are also
+  -- registry-only so they observe `calldataloadLive` rather than the stub.
+  let registryExecutableBody := ⟨← threadAdversaryThroughExecutableSyntax fields constDecls immutableDecls
+    externalDecls functions adversarialHelpers functions fn.params #[]
+      (⟨advIdent.raw⟩ : Term) fnExecutableBody.raw (linkedContracts := linkedContracts)
+      (registryMode := true)⟩
+  let mut extraExecutableCmds : Array Cmd := #[]
+  if fn.nonReentrantLock.isSome && fn.reentrancyTrusted then
+    let unguardedId ← mkSuffixedIdent fn.ident "_unguarded"
+    let unguardedValue ← if opensReentrancyWindow then
+        mkContractFnValueWithAdversary advIdent fn.params publicExecutableBody
+      else
+        mkContractFnValue fn.params publicExecutableBody
+    extraExecutableCmds := extraExecutableCmds.push
+      (← `(command| def $unguardedId : $fnType := $unguardedValue))
+  let publicExecutableBody ← match fn.nonReentrantLock with
+    | some lockIdent =>
+        let lockName := toString lockIdent.getId
+        let some lockField := fields.find? (fun field => field.name == lockName)
+          | throwErrorAt lockIdent s!"unknown nonreentrant lock field '{lockName}'"
+        `(Verity.Core.NonReentrantGuard.guarded $(natTerm lockField.slotNum) $publicExecutableBody)
+    | none => pure publicExecutableBody
   let fnValue ← if opensReentrancyWindow then
-      mkContractFnValueWithAdversary advIdent fn.params fnExecutableBody
+      mkContractFnValueWithAdversary advIdent fn.params publicExecutableBody
     else
-      mkContractFnValue fn.params fnExecutableBody
+      mkContractFnValue fn.params publicExecutableBody
+  let registryId ← mkSuffixedIdent fn.ident "_registry"
+  let registryType ← mkContractFnTypeWithAdversary fn.params fn.returnTy
+  if fn.nonReentrantLock.isSome && fn.reentrancyTrusted then
+    let registryUnguardedId ← mkSuffixedIdent fn.ident "_registry_unguarded"
+    let registryUnguardedValue ←
+      mkContractFnValueWithAdversary advIdent fn.params registryExecutableBody
+    extraExecutableCmds := extraExecutableCmds.push
+      (← `(command| def $registryUnguardedId : $registryType := $registryUnguardedValue))
+  let registryGuardedBody ← match fn.nonReentrantLock with
+    | some lockIdent =>
+        let lockName := toString lockIdent.getId
+        let some lockField := fields.find? (fun field => field.name == lockName)
+          | throwErrorAt lockIdent s!"unknown nonreentrant lock field '{lockName}'"
+        `(Verity.Core.NonReentrantGuard.guarded
+          $(natTerm lockField.slotNum) $registryExecutableBody)
+    | none => pure registryExecutableBody
+  let registryValue ←
+    mkContractFnValueWithAdversary advIdent fn.params registryGuardedBody
+  extraExecutableCmds := extraExecutableCmds.push
+    (← `(command| def $registryId : $registryType := $registryValue))
   let modelParams ← mkModelParamsTerm fn.params
   let localObligationTerms ← (functionLocalObligationsWithArithmetic fn).mapM mkModelLocalObligationTerm
   let payableTerm ← if fn.isPayable then `(true) else `(false)
@@ -6562,6 +7106,95 @@ def mkFunctionCommandsPublic
   let returnsTerm ← modelReturnsTerm fn.returnTy
 
   let fnCmd : Cmd ← `(command| def $fn.ident : $fnType := $fnValue)
+  let entrypointPredicateName ← mkSuffixedIdent fn.ident "_entrypoint"
+  let registryAdvIdent ← Lean.Elab.Term.mkFreshIdent
+    (mkIdentFrom fn.ident `_registryAdv).raw
+  let transitionIdent ← Lean.Elab.Term.mkFreshIdent
+    (mkIdentFrom fn.ident `_transition).raw
+  let contextIdent ← Lean.Elab.Term.mkFreshIdent
+    (mkIdentFrom fn.ident `_callbackContext).raw
+  let registryAdv : Ident := ⟨registryAdvIdent.raw⟩
+  let transition : Ident := ⟨transitionIdent.raw⟩
+  let context : Ident := ⟨contextIdent.raw⟩
+  -- The executable resolver is existentially quantified: a registered
+  -- transition may come from any `ExecutableCallContext` carrying the
+  -- registry adversary (e.g. `ofCallEnv`), not only from `ofAdversary`,
+  -- whose resolver fixes target/value to 0 (Codex P1 on #2406).
+  let resolveIdent ← Lean.Elab.Term.mkFreshIdent
+    (mkIdentFrom fn.ident `_registryResolve).raw
+  let resolve : Ident := ⟨resolveIdent.raw⟩
+  let mut applied : Term := registryId
+  applied ← `($applied ({ adversary := $registryAdv:ident, resolve := $resolve:ident } :
+    Contracts.ExecutableCallContext))
+  let mut registryParams : Array (Ident × Term) := #[]
+  for param in fn.params do
+    let paramTy ← contractValueTypeTerm param.ty
+    let paramIdent ← Lean.Elab.Term.mkFreshIdent
+      (mkIdentFrom param.ident `_registryArg).raw
+    let registryParam : Ident := ⟨paramIdent.raw⟩
+    registryParams := registryParams.push (registryParam, paramTy)
+    applied ← `($applied $registryParam:ident)
+  let mut registryBody : Term ←
+    `(($transition:ident : Verity.ContractState → Verity.ContractState) =
+      Compiler.CompilationModel.DenoteExternalCalls.callbackContractTransition
+        $context:ident $applied)
+  if !fn.isPayable then
+    registryBody ← `(($context:ident).msgValue = 0 ∧ $registryBody)
+  -- Tie Lean arguments to the same ABI calldata the compiled dispatcher
+  -- ABI-decodes (`calldatasizeGuard` + `calldataload`). `receive` is
+  -- compiled only when `calldatasize == 0`. Dynamic types use
+  -- `abiEncodeDispatchArgs`, not `ExternalArg.toWords`.
+  if fn.name == "receive" then
+    registryBody ←
+      `(Compiler.CompilationModel.DenoteExternalCalls.receiveCalldataMatches
+          $context:ident ∧ $registryBody)
+  else if fn.name != "fallback" then
+    let mut dispatchValTerms : Array Term := #[]
+    let mut kindTerms : Array Term := #[]
+    for (param, (paramIdent, _)) in fn.params.zip registryParams do
+      dispatchValTerms := dispatchValTerms.push
+        (← dispatchValTermForType param.ty ⟨paramIdent.raw⟩)
+      kindTerms := kindTerms.push (← scalarLoadKindTerm param.ty)
+    let argWordsTerm ←
+      if dispatchValTerms.isEmpty then
+        `( ([] : List Nat) )
+      else
+        `(Compiler.CompilationModel.DenoteExternalCalls.abiEncodeDispatchArgs
+            ([ $[$dispatchValTerms],* ] : List Compiler.CompilationModel.DenoteExternalCalls.DispatchVal))
+    let usesScalarNorm := fn.params.any fun p =>
+      match p.ty with
+      | .bool | .uint8 | .uint16 | .uintN _ | .address | .bytesN _ => true
+      | _ => false
+    if usesScalarNorm then
+      let kindsTerm ←
+        if kindTerms.isEmpty then
+          `( ([] : List Compiler.CompilationModel.DenoteExternalCalls.ScalarLoadKind) )
+        else
+          `( ([ $[$kindTerms],* ] :
+              List Compiler.CompilationModel.DenoteExternalCalls.ScalarLoadKind) )
+      registryBody ←
+        `(Compiler.CompilationModel.DenoteExternalCalls.dispatchCalldataMatchesKinds
+            $context:ident $kindsTerm $argWordsTerm ∧ $registryBody)
+    else
+      registryBody ←
+        `(Compiler.CompilationModel.DenoteExternalCalls.dispatchCalldataMatches
+            $context:ident $argWordsTerm ∧ $registryBody)
+  for (paramIdent, paramTy) in registryParams.reverse do
+    registryBody ← `(∃ $paramIdent:ident : $paramTy, $registryBody)
+  registryBody ←
+    `(∃ $resolve:ident :
+        String → Nat → Option Compiler.CompilationModel.DenoteFunctionCalls.LinkedExternal,
+      $registryBody)
+  registryBody ←
+    `(∃ $context:ident :
+        Compiler.CompilationModel.DenoteExternalCalls.CallbackContext,
+      $registryBody)
+  let entrypointCmd : Cmd ← `(command|
+    def $entrypointPredicateName
+        ($registryAdv:ident :
+          Compiler.CompilationModel.DenoteExternalCalls.AdversaryModel)
+        ($transition:ident : Verity.ContractState → Verity.ContractState) : Prop :=
+      $registryBody)
   let bodyCmd : Cmd ← `(command| def $modelBodyName : List Compiler.CompilationModel.Stmt := [ $[$stmtTerms],* ])
   let modelNameTerm :=
     if fn.isInternal then
@@ -6588,7 +7221,26 @@ def mkFunctionCommandsPublic
     body := $modelBodyName
     isInternal := $internalTerm
   })
-  pure #[fnCmd, bodyCmd, modelCmd]
+  pure (extraExecutableCmds ++ #[fnCmd, entrypointCmd, bodyCmd, modelCmd])
+
+/-- Emit the contract-wide union of all externally callable entrypoint
+predicates.  Each per-function predicate keeps arguments existential, ties
+them to compiled-dispatch ABI calldata (`abiEncodeDispatchArgs`), and uses the
+registry's explicit adversary when the function opens a reentrancy window. -/
+def mkEntrypointRegistryCommandPublic (functions : Array FunctionDecl) : CommandElabM Cmd := do
+  let advIdent ← Lean.Elab.Term.mkFreshIdent (mkIdent `_registryAdv).raw
+  let transitionIdent ← Lean.Elab.Term.mkFreshIdent (mkIdent `_transition).raw
+  let registryAdv : Ident := ⟨advIdent.raw⟩
+  let transition : Ident := ⟨transitionIdent.raw⟩
+  let mut body : Term ← `(False)
+  for fn in functions.reverse do
+    unless fn.isInternal do
+      let predicateName ← mkSuffixedIdent fn.ident "_entrypoint"
+      body ← `($predicateName $registryAdv:ident $transition:ident ∨ $body)
+  let id := mkIdent (Name.mkSimple "entrypointRegistry")
+  `(command|
+    def $id : Compiler.CompilationModel.DenoteExternalCalls.EntrypointRegistry :=
+      fun $registryAdv:ident $transition:ident => $body)
 
 def mkSpecCommandPublic
     (contractName : String)
diff --git a/Verity/Proofs/Model/GeneratedEntrypointRegistry.lean b/Verity/Proofs/Model/GeneratedEntrypointRegistry.lean
new file mode 100644
index 000000000..7ab367c40
--- /dev/null
+++ b/Verity/Proofs/Model/GeneratedEntrypointRegistry.lean
@@ -0,0 +1,616 @@
+import Contracts.Common
+import Verity.Core.Model.CallbackBridge
+import Verity.Core.Model.NonReentrantGuard
+
+namespace Contracts.ReentrancyRelyGuarantee
+
+open Contracts
+open Verity hiding pure bind
+open Verity.EVM.Uint256
+open Compiler.CompilationModel.DenoteExternalCalls
+
+/-! Focused generated consumer for the registry/guard boundary.  It contains
+an actual mutable external-call window, so the executable entrypoint must take
+an explicit adversary and the nonreentrant annotation must guard that same
+generated function. -/
+verity_contract GeneratedRegistry where
+  storage
+    lock : Uint256 := slot 0
+  linked_externals
+    external ping(Uint256) -> (Uint256)
+
+  function nonreentrant(lock) guardedPing (value : Uint256) : Unit := do
+    let _response := externalCall "ping" [value]
+    return ()
+
+  function noop (value : Uint256) : Uint256 := do
+    return value
+
+namespace GeneratedRegistry
+
+/-- The generated registry uses its explicit adversary at the external-call
+entrypoint; there is no `.stub` compatibility path in this theorem surface.
+The registry quantifies over the executable resolver, so any
+`ExecutableCallContext` carrying the adversary is covered, not only
+`ofAdversary` (whose resolver fixes target/value to 0). -/
+theorem guardedPing_registered (ectx : Contracts.ExecutableCallContext) (ctx : CallbackContext)
+    (value : Uint256) (hvalue : ctx.msgValue = 0)
+    (hcalldata : dispatchCalldataMatches ctx
+      (abiEncodeDispatchArgs [ToDispatchVal.toDispatchVal value])) :
+    entrypointRegistry ectx.adversary
+      (callbackContractTransition ctx (guardedPing_registry ectx value)) := by
+  left
+  exact ⟨ctx, ectx.resolve, value, hcalldata, hvalue, rfl⟩
+
+/-- The `ofAdversary` instance of the general registration theorem. -/
+theorem guardedPing_registered_ofAdversary (adv : AdversaryModel) (ctx : CallbackContext)
+    (value : Uint256) (hvalue : ctx.msgValue = 0)
+    (hcalldata : dispatchCalldataMatches ctx
+      (abiEncodeDispatchArgs [ToDispatchVal.toDispatchVal value])) :
+    entrypointRegistry adv
+      (callbackContractTransition ctx
+        (guardedPing_registry (Contracts.ExecutableCallContext.ofAdversary adv) value)) :=
+  guardedPing_registered (Contracts.ExecutableCallContext.ofAdversary adv) ctx value hvalue
+    hcalldata
+
+/-- The executable generated entrypoint is definitionally protected by the
+canonical source guard at the same slot used by the compiled dispatch guard. -/
+theorem guardedPing_reentry_blocked (adv : AdversaryModel) (value : Uint256)
+    (state : ContractState) (hlock : state.transientStorage 0 ≠ 0) :
+    (guardedPing (Contracts.ExecutableCallContext.ofAdversary adv) value).runState state = state := by
+  apply Verity.Core.NonReentrantGuard.guarded_reentry_blocked
+  exact hlock
+
+end GeneratedRegistry
+
+/-! Regression for registry window-helper routing: `readBal` is adversarial
+(view/staticcall ECM) but does not open a reentrancy window, while `hop`
+opens a window and then calls `readBal`. `entry_registry` must call
+`hop_registry` (which calls `readBal_registry`) rather than public `hop`
+(which uses stub-only `readBal` and under-approximates a callee-controlled
+view ECM). -/
+verity_contract RegistryWindowHelperRouting where
+  storage
+    last : Uint256 := slot 0
+  interfaces
+    interface IToken where
+      function balanceOf(Address) view returns (Uint256)
+    end
+  linked_externals
+    external ping(Uint256) -> (Uint256)
+
+  function view readBal (token : IToken, who : Address) : Uint256 := do
+    let observed ← token.balanceOf who
+    return observed
+
+  function reentrancy_trusted hop (token : IToken, who : Address) : Uint256 := do
+    let _ack := externalCall "ping" [0]
+    let observed ← readBal token who
+    return observed
+
+  function allow_post_interaction_writes reentrancy_trusted entry
+      (token : IToken, who : Address) : Uint256 := do
+    let observed ← hop token who
+    setStorage last observed
+    return observed
+
+namespace RegistryWindowHelperRouting
+
+/-- Distinctive view-call adversary: staticcall sites return 42 instead of the
+deterministic stub word. Public `hop` ignores this because it calls stub-only
+`readBal`; `hop_registry` / `entry_registry` must observe 42. -/
+def distinctiveViewAdv : AdversaryModel where
+  stateTransition := fun _ state => state
+  result := fun site world =>
+    if site.kind = .staticcall then .success [42]
+    else AdversaryModel.stub.result site world
+  gasUsed := fun _ _ => 0
+
+def distinctiveCtx : Contracts.ExecutableCallContext :=
+  Contracts.ExecutableCallContext.ofAdversary distinctiveViewAdv
+
+/-- Public `hop` still uses stub-only `readBal` (no adversary). -/
+def hopPublicSeesStub : Bool :=
+  match (hop distinctiveCtx 0 0).run Verity.defaultState with
+  | .success value _ => !(value == 42)
+  | _ => false
+
+example : hopPublicSeesStub = true := by decide
+
+/-- `hop_registry` routes the nested view helper through `readBal_registry`. -/
+def hopRegistrySeesAdversary : Bool :=
+  match (hop_registry distinctiveCtx 0 0).run Verity.defaultState with
+  | .success value _ => value == 42
+  | _ => false
+
+example : hopRegistrySeesAdversary = true := by decide
+
+/-- `entry_registry` must call `hop_registry`, not public `hop`. -/
+def entryRegistrySeesAdversary : Bool :=
+  match (entry_registry distinctiveCtx 0 0).run Verity.defaultState with
+  | .success value _ => value == 42
+  | _ => false
+
+example : entryRegistrySeesAdversary = true := by decide
+
+end RegistryWindowHelperRouting
+
+/-! Regression: parenthesized overloaded helper + nested `externalCall`.
+Second-pass `threadHelperApp?` must resolve the overload from the original
+source arguments (`originalArgsForOverload`), not the hoisted temps. Otherwise
+the registry body falls through to the public helper and observes stub
+returndata. The parenthesized `let observed ← overloadedHop(externalCall ...)`
+form is the let-bind second-pass site; `hoistNested` rewrites the nested
+`externalCall` argument of that same application. -/
+verity_contract RegistryOverloadedNestedExternal where
+  storage
+    last : Uint256 := slot 0
+  linked_externals
+    external ping(Uint256) -> (Uint256)
+
+  function overloadedHop (_who : Address) : Uint256 := do
+    return 0
+
+  function reentrancy_trusted overloadedHop (x : Uint256) : Uint256 := do
+    let observed := externalCall "ping" [x]
+    return observed
+
+  function allow_post_interaction_writes reentrancy_trusted entryLet (x : Uint256) : Uint256 := do
+    let observed ← overloadedHop(externalCall "ping" [x])
+    setStorage last observed
+    return observed
+
+namespace RegistryOverloadedNestedExternal
+
+def distinctivePingAdv : AdversaryModel where
+  stateTransition := fun _ state => state
+  result := fun site world =>
+    if site.name = "ping" then .success [42]
+    else AdversaryModel.stub.result site world
+  gasUsed := fun _ _ => 0
+
+def distinctivePingCtx : Contracts.ExecutableCallContext :=
+  Contracts.ExecutableCallContext.ofAdversary distinctivePingAdv
+
+/-- `entryLet_registry` must call `overloadedHop_registry`, not public `overloadedHop`. -/
+def entryLetRegistrySeesAdversary : Bool :=
+  match (entryLet_registry distinctivePingCtx 0).run Verity.defaultState with
+  | .success value _ => value == 42
+  | _ => false
+
+example : entryLetRegistrySeesAdversary = true := by decide
+
+end RegistryOverloadedNestedExternal
+
+/-! Regression: `linked_contracts` hop to a view/static-only bound callee.
+Public `helper.get` uses `.stub`; `entry_registry` must hop through
+`BoundViewCallee.get_registry` so a distinctive staticcall adversary is
+observed (Codex P1 on #2406). -/
+verity_contract BoundViewCallee where
+  storage
+    unused : Uint256 := slot 0
+  interfaces
+    interface IToken where
+      function balanceOf(Address) view returns (Uint256)
+    end
+
+  function view get (token : IToken, who : Address) : Uint256 := do
+    let observed ← token.balanceOf who
+    return observed
+
+verity_contract BoundViewCaller where
+  storage
+    last : Uint256 := slot 0
+  interfaces
+    interface IViewCallee where
+      function get(Address, Address) view returns (Uint256)
+    end
+  linked_contracts
+    helper : IViewCallee := BoundViewCallee
+
+  function allow_post_interaction_writes reentrancy_trusted entry
+      (helper : IViewCallee, token : Address, who : Address) : Uint256 := do
+    let observed ← helper.get token who
+    setStorage last observed
+    return observed
+
+namespace BoundViewCaller
+
+def distinctiveViewAdv : AdversaryModel where
+  stateTransition := fun _ state => state
+  result := fun site world =>
+    if site.kind = .staticcall then .success [42]
+    else AdversaryModel.stub.result site world
+  gasUsed := fun _ _ => 0
+
+def distinctiveCtx : Contracts.ExecutableCallContext :=
+  Contracts.ExecutableCallContext.ofAdversary distinctiveViewAdv
+
+/-- Public `entry` is ctx-free and hops to stub-backed `BoundViewCallee.get`. -/
+def entryPublicSeesStub : Bool :=
+  match (entry 0 0 0).run Verity.defaultState with
+  | .success value _ => !(value == 42)
+  | _ => false
+
+example : entryPublicSeesStub = true := by decide
+
+/-- `entry_registry` hops through `BoundViewCallee.get_registry`. -/
+def entryRegistrySeesAdversary : Bool :=
+  match (entry_registry distinctiveCtx 0 0 0).run Verity.defaultState with
+  | .success value _ => value == 42
+  | _ => false
+
+example : entryRegistrySeesAdversary = true := by decide
+
+end BoundViewCaller
+
+/-! Regression: registered transitions cannot pair Lean arguments with
+unrelated calldata, and `receive` is only registered for empty calldata. -/
+verity_contract RegistryDispatchCalldata where
+  storage
+    last : Uint256 := slot 0
+
+  receive := do
+    setStorage last 7
+
+  function setLast (value : Uint256) : Unit := do
+    setStorage last value
+    return ()
+
+namespace RegistryDispatchCalldata
+
+def matchingCtx (value : Uint256) : CallbackContext where
+  sender := 0
+  msgValue := 0
+  calldataSize := Verity.Core.Uint256.ofNat 36
+  calldata := [value.val]
+
+def mismatchedCtx : CallbackContext where
+  sender := 0
+  msgValue := 0
+  calldataSize := Verity.Core.Uint256.ofNat 36
+  calldata := [99]
+
+def emptyReceiveCtx : CallbackContext where
+  sender := 0
+  msgValue := 0
+  calldataSize := 0
+  calldata := []
+
+def nonemptyReceiveCtx : CallbackContext where
+  sender := 0
+  msgValue := 0
+  calldataSize := Verity.Core.Uint256.ofNat 4
+  calldata := [1]
+
+def argWords (value : Uint256) : List Nat :=
+  abiEncodeDispatchArgs [ToDispatchVal.toDispatchVal value]
+
+example : dispatchCalldataMatches (matchingCtx 7) (argWords 7) := by decide
+
+example : ¬ dispatchCalldataMatches mismatchedCtx (argWords 7) := by decide
+
+example : receiveCalldataMatches emptyReceiveCtx := by decide
+
+example : ¬ receiveCalldataMatches nonemptyReceiveCtx := by decide
+
+theorem setLast_registered_matching (value : Uint256)
+    (h : dispatchCalldataMatches (matchingCtx value) (argWords value)) :
+    setLast_entrypoint AdversaryModel.stub
+      (callbackContractTransition (matchingCtx value)
+        (setLast_registry (Contracts.ExecutableCallContext.ofAdversary AdversaryModel.stub) value)) :=
+  ⟨matchingCtx value, (Contracts.ExecutableCallContext.ofAdversary AdversaryModel.stub).resolve,
+    value, h, rfl, rfl⟩
+
+theorem setLast_entrypoint_requires_dispatch
+    {adv : AdversaryModel} {transition : ContractState → ContractState}
+    (h : setLast_entrypoint adv transition) :
+    ∃ ctx resolve value,
+      dispatchCalldataMatches ctx (argWords value) ∧
+        ctx.msgValue = 0 ∧
+        transition =
+          callbackContractTransition ctx
+            (setLast_registry { adversary := adv, resolve := resolve } value) :=
+  h
+
+theorem receive_registered_empty :
+    __verity_receive_entrypoint AdversaryModel.stub
+      (callbackContractTransition emptyReceiveCtx
+        (__verity_receive_registry
+          (Contracts.ExecutableCallContext.ofAdversary AdversaryModel.stub))) :=
+  ⟨emptyReceiveCtx, (Contracts.ExecutableCallContext.ofAdversary AdversaryModel.stub).resolve,
+    by decide, rfl⟩
+
+theorem receive_entrypoint_requires_empty
+    {adv : AdversaryModel} {transition : ContractState → ContractState}
+    (h : __verity_receive_entrypoint adv transition) :
+    ∃ ctx resolve,
+      receiveCalldataMatches ctx ∧
+        transition =
+          callbackContractTransition ctx
+            (__verity_receive_registry { adversary := adv, resolve := resolve }) :=
+  h
+
+/-- Journal encoding of `Bytes` is one word per byte (`[len, b0, b1, …]`).
+Compiled dispatch marks bytes as dynamic (`DispatchVal.bytes`) and packs
+them as `[length, packed data…]` via `abiEncodeDispatchArgs`. -/
+example : dispatchArgsAllWords
+    [ToDispatchVal.toDispatchVal (ByteArray.mk #[0x61, 0x62])] = false :=
+  rfl
+
+example :
+    List.map (fun w => (w : Nat))
+        (Contracts.ExternalArg.toWords (ByteArray.mk #[0x61, 0x62])) =
+      [2, 0x61, 0x62] := by
+  decide
+
+end RegistryDispatchCalldata
+
+/-! Regression: registry executables observe live callback calldata, not the
+public `calldatasize = 0` / `calldataload offset = offset` stubs. -/
+verity_contract RegistryLiveCalldata where
+  storage
+    last : Uint256 := slot 0
+
+  function setFromCalldata (_value : Uint256)
+      local_obligations [manual_low_level_refinement := assumed
+        "Fixture reads compiled-dispatch calldata via calldataload 4."]
+      : Unit := do
+    let cds := calldatasize
+    let loaded := calldataload 4
+    if cds == 36 then
+      setStorage last loaded
+    else
+      setStorage last 0
+    return ()
+
+namespace RegistryLiveCalldata
+
+def liveCtx (value : Uint256) : CallbackContext where
+  sender := 0
+  msgValue := 0
+  calldataSize := Verity.Core.Uint256.ofNat 36
+  calldata := [value.val]
+
+def publicWritesStub : Bool :=
+  match (setFromCalldata (7 : Uint256)).run Verity.defaultState with
+  | .success _ s => s.storage 0 == 0
+  | _ => false
+
+example : publicWritesStub = true := by decide
+
+def liveWritesLoaded : Bool :=
+  let s := callbackContractTransition (liveCtx 7)
+    (setFromCalldata_registry
+      (Contracts.ExecutableCallContext.ofAdversary AdversaryModel.stub) 7)
+    Verity.defaultState
+  s.storage 0 == 7
+
+example : liveWritesLoaded = true := by decide
+
+def liveArgWords (value : Uint256) : List Nat :=
+  abiEncodeDispatchArgs [ToDispatchVal.toDispatchVal value]
+
+theorem setFromCalldata_registered_live
+    (h : dispatchCalldataMatches (liveCtx 7) (liveArgWords 7)) :
+    setFromCalldata_entrypoint AdversaryModel.stub
+      (callbackContractTransition (liveCtx 7)
+        (setFromCalldata_registry
+          (Contracts.ExecutableCallContext.ofAdversary AdversaryModel.stub) 7)) :=
+  ⟨liveCtx 7, (Contracts.ExecutableCallContext.ofAdversary AdversaryModel.stub).resolve,
+    7, h, rfl, rfl⟩
+
+end RegistryLiveCalldata
+
+verity_contract RegistryLiveSelector where
+  storage
+    last : Uint256 := slot 0
+
+  function setFromSelector (_unused : Uint256)
+      local_obligations [manual_low_level_refinement := assumed
+        "Fixture reads compiled-dispatch selector via calldataload 0."]
+      : Unit := do
+    let loaded := calldataload 0
+    setStorage last loaded
+    return ()
+
+namespace RegistryLiveSelector
+
+def selCtx : CallbackContext where
+  sender := 0
+  msgValue := 0
+  calldataSize := Verity.Core.Uint256.ofNat 4
+  calldata := []
+  selector := 0xa9059cbb
+
+def publicWritesOffset : Bool :=
+  match (setFromSelector (0 : Uint256)).run Verity.defaultState with
+  | .success _ s => s.storage 0 == 0
+  | _ => false
+
+example : publicWritesOffset = true := by decide
+
+def liveWritesSelectorWord : Bool :=
+  let s := callbackContractTransition selCtx
+    (setFromSelector_registry
+      (Contracts.ExecutableCallContext.ofAdversary AdversaryModel.stub) 0)
+    Verity.defaultState
+  s.storage 0 == Compiler.CompilationModel.Denote.selectorWord 0xa9059cbb
+
+example : liveWritesSelectorWord = true := by decide
+
+end RegistryLiveSelector
+
+/-! P1: FixedArray vs Array encoding; flattened 3-member tuples. -/
+example :
+    DispatchVal.isDynamic
+      (dispatchFixedArray
+        [ToDispatchVal.toDispatchVal (1 : Uint256),
+         ToDispatchVal.toDispatchVal (2 : Uint256)]) = false :=
+  rfl
+
+example :
+    (dispatchFixedArray
+      [ToDispatchVal.toDispatchVal (1 : Uint256),
+       ToDispatchVal.toDispatchVal (2 : Uint256)]).payloadWords = [1, 2] :=
+  rfl
+
+example :
+    dispatchArgsAllWords
+      [ToDispatchVal.toDispatchVal (#[(1 : Uint256), (2 : Uint256)] : Array Uint256)] = false :=
+  rfl
+
+example :
+    (abiEncodeDispatchArgs
+      [ToDispatchVal.toDispatchVal (#[(1 : Uint256), (2 : Uint256)] : Array Uint256)]).head? =
+      some 32 :=
+  rfl
+
+example :
+    dispatchArgsAllWords
+      [ToDispatchVal.toDispatchVal
+        ((1 : Uint256), ("ab", (3 : Uint256)))] = false :=
+  rfl
+
+example :
+    dispatchArgsAllWords
+      [dispatchFlatTuple
+        (DispatchVal.tuple
+          [ToDispatchVal.toDispatchVal (1 : Uint256),
+           ToDispatchVal.toDispatchVal ("ab" : String),
+           ToDispatchVal.toDispatchVal (3 : Uint256)])] = false :=
+  rfl
+
+/-! P1: genScalarLoad-normalized noncanonical scalar words still match. -/
+example : dispatchCalldataMatchesKinds
+    { sender := 0, msgValue := 0,
+      calldataSize := Verity.Core.Uint256.ofNat 36, calldata := [2] }
+    [.bool]
+    (abiEncodeDispatchArgs [ToDispatchVal.toDispatchVal true]) := by decide
+
+example : dispatchCalldataMatchesKinds
+    { sender := 0, msgValue := 0,
+      calldataSize := Verity.Core.Uint256.ofNat 36, calldata := [256] }
+    [.uint8]
+    (abiEncodeDispatchArgs [ToDispatchVal.toDispatchVal (0 : Verity.Core.UIntN 8)]) := by decide
+
+example : dispatchCalldataMatchesKinds
+    { sender := 0, msgValue := 0,
+      calldataSize := Verity.Core.Uint256.ofNat 36,
+      calldata := [Compiler.Constants.addressMask + 1 + 7] }
+    [.address]
+    (abiEncodeDispatchArgs [ToDispatchVal.toDispatchVal (7 : Address)]) := by decide
+
+/-! P1: calldata-reading helpers are routed through *_registry. -/
+verity_contract RegistryCalldataHelperRouting where
+  storage
+    last : Uint256 := slot 0
+
+  function loadArg (_unused : Uint256)
+      local_obligations [manual_low_level_refinement := assumed
+        "Helper reads compiled-dispatch calldata via calldataload 4."]
+      : Uint256 := do
+    return calldataload 4
+
+  function setFromHelper (_value : Uint256)
+      local_obligations [manual_low_level_refinement := assumed
+        "Entrypoint delegates calldata load to an internal helper."]
+      : Unit := do
+    let loaded ← loadArg 0
+    setStorage last loaded
+    return ()
+
+namespace RegistryCalldataHelperRouting
+
+def helperCtx (value : Uint256) : CallbackContext where
+  sender := 0
+  msgValue := 0
+  calldataSize := Verity.Core.Uint256.ofNat 36
+  calldata := [value.val]
+
+def publicHelperWritesStub : Bool :=
+  match (setFromHelper (7 : Uint256)).run Verity.defaultState with
+  | .success _ s => s.storage 0 == 4
+  | _ => false
+
+example : publicHelperWritesStub = true := by decide
+
+def registryHelperWritesLive : Bool :=
+  let s := callbackContractTransition (helperCtx 7)
+    (setFromHelper_registry
+      (Contracts.ExecutableCallContext.ofAdversary AdversaryModel.stub) 7)
+    Verity.defaultState
+  s.storage 0 == 7
+
+example : registryHelperWritesLive = true := by decide
+
+end RegistryCalldataHelperRouting
+
+/-! Regression: public Solidity self-calls still hit the nonReentrant tload
+prologue. Bound hops must keep the guarded registry path, not `*_unguarded`. -/
+verity_contract RegistrySelfCallGuard where
+  storage
+    lock : Uint256 := slot 0
+    last : Uint256 := slot 1
+  linked_externals
+    external ping(Uint256) -> (Uint256)
+
+  function nonreentrant(lock) reentrancy_trusted hop (value : Uint256) : Unit := do
+    let _ack := externalCall "ping" [value]
+    setStorage last value
+    return ()
+
+  function reentrancy_trusted allow_post_interaction_writes entry
+      (value : Uint256)
+      local_obligations [manual_low_level_refinement := assumed
+        "tryCall/selfCall compilation model is CALL-with-status to this; selector and argument encoding are a documented gap."]
+      : Unit := do
+    tryCall (selfCall hop(value)) then
+      (do setStorage last value)
+    catch
+      (do setStorage last 99)
+    return ()
+
+namespace RegistrySelfCallGuard
+
+def lockedState : ContractState :=
+  Verity.defaultState.writeTransient 0 1
+
+def hopBlockedWhenLocked : Bool :=
+  match (hop (Contracts.ExecutableCallContext.ofAdversary AdversaryModel.stub) (7 : Uint256)).run lockedState with
+  | .revert _ s => s.storage 1 == 0
+  | _ => false
+
+example : hopBlockedWhenLocked = true := by decide
+
+def selfCallHopBlockedWhenLocked : Bool :=
+  match (entry (Contracts.ExecutableCallContext.ofAdversary AdversaryModel.stub) (7 : Uint256)).run lockedState with
+  | .success _ s => s.storage 1 == 99
+  | _ => false
+
+example : selfCallHopBlockedWhenLocked = true := by decide
+
+def selfCallHopRegistryBlockedWhenLocked : Bool :=
+  match (entry_registry (Contracts.ExecutableCallContext.ofAdversary AdversaryModel.stub) (7 : Uint256)).run lockedState with
+  | .success _ s => s.storage 1 == 99
+  | _ => false
+
+example : selfCallHopRegistryBlockedWhenLocked = true := by decide
+
+end RegistrySelfCallGuard
+
+/-- `ReentrancyRelyGuarantee` consumes the emitted registry at the restricted
+callback boundary.  Contract-specific preservation obligations remain with
+authors; this PR establishes only the generated registry/guard connection. -/
+theorem generated_registry_callback_preserves
+    {adversary : AdversaryModel}
+    (hbound : CallbackBounded GeneratedRegistry.entrypointRegistry adversary)
+    (hregistry : RegistryPreserves (fun _ => True)
+      GeneratedRegistry.entrypointRegistry adversary)
+    (site : CallSite) (state : CallState) :
+    (fun _ : ContractState => True)
+      (denoteCall adversary site state).state.world :=
+  hbound.denoteCall_preserves_registry (fun _ => True)
+    GeneratedRegistry.entrypointRegistry hregistry site state trivial
+
+end Contracts.ReentrancyRelyGuarantee
diff --git a/artifacts/macro_property_tests/PropertyNonreentrantQualifiedHelperResolution.t.sol b/artifacts/macro_property_tests/PropertyNonreentrantQualifiedHelperResolution.t.sol
new file mode 100644
index 000000000..f382a5ab7
--- /dev/null
+++ b/artifacts/macro_property_tests/PropertyNonreentrantQualifiedHelperResolution.t.sol
@@ -0,0 +1,220 @@
+// SPDX-License-Identifier: MIT
+pragma solidity ^0.8.33;
+
+import "./yul/YulTestBase.sol";
+
+/**
+ * @title PropertyNonreentrantQualifiedHelperResolutionTest
+ * @notice Auto-generated baseline property stubs from `verity_contract` declarations.
+ * @dev Source: Contracts/Smoke/SecurityCombos.lean
+ */
+contract PropertyNonreentrantQualifiedHelperResolutionTest is YulTestBase {
+    address target;
+    address alice = address(0x1111);
+
+    function setUp() public {
+        target = deployYul("NonreentrantQualifiedHelperResolution");
+        require(target != address(0), "Deploy failed");
+    }
+
+    // Property 1: trustedEntry returns the direct parameter value
+    function testAuto_TrustedEntry_ReturnsDirectParam() public {
+        vm.prank(alice);
+        (bool ok, bytes memory ret) = target.call(abi.encodeWithSignature("trustedEntry(uint256)", uint256(1)));
+        require(ok, "trustedEntry reverted unexpectedly");
+        assertEq(ret.length, 32, "trustedEntry ABI return length mismatch (expected 32 bytes)");
+        uint256 actual = abi.decode(ret, (uint256));
+        assertEq(actual, uint256(1), "trustedEntry should preserve the expected value");
+    }
+    // Property 2: trustedPair decodes and matches the inferred tuple result
+    function testAuto_TrustedPair_ReturnsInferredTupleResult() public {
+        vm.prank(alice);
+        (bool ok, bytes memory ret) = target.call(abi.encodeWithSignature("trustedPair(uint256)", uint256(1)));
+        require(ok, "trustedPair reverted unexpectedly");
+        require(ret.length >= 64, "trustedPair ABI tuple return payload unexpectedly short");
+        (uint256 actual0, uint256 actual1) = abi.decode(ret, (uint256, uint256));
+        assertEq(actual0, uint256(1), "trustedPair tuple element 0 should preserve the inferred result");
+        assertEq(actual1, uint256(1), "trustedPair tuple element 1 should preserve the inferred result");
+    }
+    // Property 3: TODO decode and assert `adversarialEntry` result
+    function testTODO_AdversarialEntry_DecodeAndAssert() public {
+        vm.prank(alice);
+        (bool ok, bytes memory ret) = target.call(abi.encodeWithSignature("adversarialEntry(uint256)", uint256(1)));
+        require(ok, "adversarialEntry reverted unexpectedly");
+        assertEq(ret.length, 32, "adversarialEntry ABI return length mismatch (expected 32 bytes)");
+        // TODO(#1011): decode `ret` and assert the concrete postcondition from Lean theorem.
+        ret;
+    }
+    // Property 4: TODO decode and assert `adversarialPair` result
+    function testTODO_AdversarialPair_DecodeAndAssert() public {
+        vm.prank(alice);
+        (bool ok, bytes memory ret) = target.call(abi.encodeWithSignature("adversarialPair(uint256)", uint256(1)));
+        require(ok, "adversarialPair reverted unexpectedly");
+        require(ret.length >= 64, "adversarialPair ABI tuple return payload unexpectedly short");
+        // TODO(#1011): decode `ret` and assert the concrete postcondition from Lean theorem.
+        ret;
+    }
+    // Property 5: overloadedTrusted returns the declared constant result
+    function testAuto_OverloadedTrusted_ReturnsDeclaredConstant() public {
+        vm.prank(alice);
+        (bool ok, bytes memory ret) = target.call(abi.encodeWithSignature("overloadedTrusted(address)", alice));
+        require(ok, "overloadedTrusted reverted unexpectedly");
+        assertEq(ret.length, 32, "overloadedTrusted ABI return length mismatch (expected 32 bytes)");
+        uint256 actual = abi.decode(ret, (uint256));
+        assertEq(actual, 0, "overloadedTrusted should return the declared constant");
+    }
+    // Property 6: overloadedTrusted returns the direct parameter value
+    function testAuto_OverloadedTrusted_ReturnsDirectParam() public {
+        vm.prank(alice);
+        (bool ok, bytes memory ret) = target.call(abi.encodeWithSignature("overloadedTrusted(uint256)", uint256(1)));
+        require(ok, "overloadedTrusted reverted unexpectedly");
+        assertEq(ret.length, 32, "overloadedTrusted ABI return length mismatch (expected 32 bytes)");
+        uint256 actual = abi.decode(ret, (uint256));
+        assertEq(actual, uint256(1), "overloadedTrusted should preserve the expected value");
+    }
+    // Property 7: overloadedAdversarial returns the declared constant result
+    function testAuto_OverloadedAdversarial_ReturnsDeclaredConstant() public {
+        vm.prank(alice);
+        (bool ok, bytes memory ret) = target.call(abi.encodeWithSignature("overloadedAdversarial(address)", alice));
+        require(ok, "overloadedAdversarial reverted unexpectedly");
+        assertEq(ret.length, 32, "overloadedAdversarial ABI return length mismatch (expected 32 bytes)");
+        uint256 actual = abi.decode(ret, (uint256));
+        assertEq(actual, 0, "overloadedAdversarial should return the declared constant");
+    }
+    // Property 8: TODO decode and assert `overloadedAdversarial` result
+    function testTODO_OverloadedAdversarial_DecodeAndAssert() public {
+        vm.prank(alice);
+        (bool ok, bytes memory ret) = target.call(abi.encodeWithSignature("overloadedAdversarial(uint256)", uint256(1)));
+        require(ok, "overloadedAdversarial reverted unexpectedly");
+        assertEq(ret.length, 32, "overloadedAdversarial ABI return length mismatch (expected 32 bytes)");
+        // TODO(#1011): decode `ret` and assert the concrete postcondition from Lean theorem.
+        ret;
+    }
+    // Property 9: makePair decodes and matches the inferred tuple result
+    function testAuto_MakePair_ReturnsInferredTupleResult() public {
+        vm.prank(alice);
+        (bool ok, bytes memory ret) = target.call(abi.encodeWithSignature("makePair(uint256)", uint256(1)));
+        require(ok, "makePair reverted unexpectedly");
+        require(ret.length >= 64, "makePair ABI tuple return payload unexpectedly short");
+        (uint256 actual0, uint256 actual1) = abi.decode(ret, (uint256, uint256));
+        assertEq(actual0, uint256(1), "makePair tuple element 0 should preserve the inferred result");
+        assertEq(actual1, uint256(1), "makePair tuple element 1 should preserve the inferred result");
+    }
+    // Property 10: TODO decode and assert `qualifiedSpace` result
+    function testTODO_QualifiedSpace_DecodeAndAssert() public {
+        vm.prank(alice);
+        (bool ok, bytes memory ret) = target.call(abi.encodeWithSignature("qualifiedSpace(uint256)", uint256(1)));
+        require(ok, "qualifiedSpace reverted unexpectedly");
+        assertEq(ret.length, 32, "qualifiedSpace ABI return length mismatch (expected 32 bytes)");
+        // TODO(#1011): decode `ret` and assert the concrete postcondition from Lean theorem.
+        ret;
+    }
+    // Property 11: TODO decode and assert `qualifiedDestructure` result
+    function testTODO_QualifiedDestructure_DecodeAndAssert() public {
+        vm.prank(alice);
+        (bool ok, bytes memory ret) = target.call(abi.encodeWithSignature("qualifiedDestructure(uint256)", uint256(1)));
+        require(ok, "qualifiedDestructure reverted unexpectedly");
+        assertEq(ret.length, 32, "qualifiedDestructure ABI return length mismatch (expected 32 bytes)");
+        // TODO(#1011): decode `ret` and assert the concrete postcondition from Lean theorem.
+        ret;
+    }
+    // Property 12: TODO decode and assert `qualifiedAdversarialSpace` result
+    function testTODO_QualifiedAdversarialSpace_DecodeAndAssert() public {
+        vm.prank(alice);
+        (bool ok, bytes memory ret) = target.call(abi.encodeWithSignature("qualifiedAdversarialSpace(uint256)", uint256(1)));
+        require(ok, "qualifiedAdversarialSpace reverted unexpectedly");
+        assertEq(ret.length, 32, "qualifiedAdversarialSpace ABI return length mismatch (expected 32 bytes)");
+        // TODO(#1011): decode `ret` and assert the concrete postcondition from Lean theorem.
+        ret;
+    }
+    // Property 13: TODO decode and assert `qualifiedAdversarialDestructure` result
+    function testTODO_QualifiedAdversarialDestructure_DecodeAndAssert() public {
+        vm.prank(alice);
+        (bool ok, bytes memory ret) = target.call(abi.encodeWithSignature("qualifiedAdversarialDestructure(uint256)", uint256(1)));
+        require(ok, "qualifiedAdversarialDestructure reverted unexpectedly");
+        assertEq(ret.length, 32, "qualifiedAdversarialDestructure ABI return length mismatch (expected 32 bytes)");
+        // TODO(#1011): decode `ret` and assert the concrete postcondition from Lean theorem.
+        ret;
+    }
+    // Property 14: TODO decode and assert `qualifiedNestedExternal` result
+    function testTODO_QualifiedNestedExternal_DecodeAndAssert() public {
+        vm.prank(alice);
+        (bool ok, bytes memory ret) = target.call(abi.encodeWithSignature("qualifiedNestedExternal(uint256)", uint256(1)));
+        require(ok, "qualifiedNestedExternal reverted unexpectedly");
+        assertEq(ret.length, 32, "qualifiedNestedExternal ABI return length mismatch (expected 32 bytes)");
+        // TODO(#1011): decode `ret` and assert the concrete postcondition from Lean theorem.
+        ret;
+    }
+    // Property 15: TODO decode and assert `trustedNestedExternal` result
+    function testTODO_TrustedNestedExternal_DecodeAndAssert() public {
+        vm.prank(alice);
+        (bool ok, bytes memory ret) = target.call(abi.encodeWithSignature("trustedNestedExternal(uint256)", uint256(1)));
+        require(ok, "trustedNestedExternal reverted unexpectedly");
+        assertEq(ret.length, 32, "trustedNestedExternal ABI return length mismatch (expected 32 bytes)");
+        // TODO(#1011): decode `ret` and assert the concrete postcondition from Lean theorem.
+        ret;
+    }
+    // Property 16: TODO decode and assert `overloadedNestedExternal` result
+    function testTODO_OverloadedNestedExternal_DecodeAndAssert() public {
+        vm.prank(alice);
+        (bool ok, bytes memory ret) = target.call(abi.encodeWithSignature("overloadedNestedExternal(uint256)", uint256(1)));
+        require(ok, "overloadedNestedExternal reverted unexpectedly");
+        assertEq(ret.length, 32, "overloadedNestedExternal ABI return length mismatch (expected 32 bytes)");
+        // TODO(#1011): decode `ret` and assert the concrete postcondition from Lean theorem.
+        ret;
+    }
+    // Property 17: overloadedTrustedCaller has no unexpected revert
+    function testAuto_OverloadedTrustedCaller_NoUnexpectedRevert() public {
+        vm.prank(alice);
+        (bool ok,) = target.call(abi.encodeWithSignature("overloadedTrustedCaller(uint256)", uint256(1)));
+        require(ok, "overloadedTrustedCaller reverted unexpectedly");
+    }
+    // Property 18: overloadedAdversarialCaller has no unexpected revert
+    function testAuto_OverloadedAdversarialCaller_NoUnexpectedRevert() public {
+        vm.prank(alice);
+        (bool ok,) = target.call(abi.encodeWithSignature("overloadedAdversarialCaller(uint256)", uint256(1)));
+        require(ok, "overloadedAdversarialCaller reverted unexpectedly");
+    }
+    // Property 19: overloadedTrustedLocalCaller has no unexpected revert
+    function testAuto_OverloadedTrustedLocalCaller_NoUnexpectedRevert() public {
+        vm.prank(alice);
+        (bool ok,) = target.call(abi.encodeWithSignature("overloadedTrustedLocalCaller()"));
+        require(ok, "overloadedTrustedLocalCaller reverted unexpectedly");
+    }
+    // Property 20: overloadedAdversarialLocalCaller has no unexpected revert
+    function testAuto_OverloadedAdversarialLocalCaller_NoUnexpectedRevert() public {
+        vm.prank(alice);
+        (bool ok,) = target.call(abi.encodeWithSignature("overloadedAdversarialLocalCaller()"));
+        require(ok, "overloadedAdversarialLocalCaller reverted unexpectedly");
+    }
+    // Property 21: overloadedTrustedTupleLocalCaller has no unexpected revert
+    function testAuto_OverloadedTrustedTupleLocalCaller_NoUnexpectedRevert() public {
+        vm.prank(alice);
+        (bool ok,) = target.call(abi.encodeWithSignature("overloadedTrustedTupleLocalCaller(uint256)", uint256(1)));
+        require(ok, "overloadedTrustedTupleLocalCaller reverted unexpectedly");
+    }
+    // Property 22: overloadedAdversarialTupleLocalCaller has no unexpected revert
+    function testAuto_OverloadedAdversarialTupleLocalCaller_NoUnexpectedRevert() public {
+        vm.prank(alice);
+        (bool ok,) = target.call(abi.encodeWithSignature("overloadedAdversarialTupleLocalCaller(uint256)", uint256(1)));
+        require(ok, "overloadedAdversarialTupleLocalCaller reverted unexpectedly");
+    }
+    // Property 23: overloadedTrustedQualifiedTupleCaller has no unexpected revert
+    function testAuto_OverloadedTrustedQualifiedTupleCaller_NoUnexpectedRevert() public {
+        vm.prank(alice);
+        (bool ok,) = target.call(abi.encodeWithSignature("overloadedTrustedQualifiedTupleCaller(uint256)", uint256(1)));
+        require(ok, "overloadedTrustedQualifiedTupleCaller reverted unexpectedly");
+    }
+    // Property 24: overloadedTrustedForEachCaller has no unexpected revert
+    function testAuto_OverloadedTrustedForEachCaller_NoUnexpectedRevert() public {
+        vm.prank(alice);
+        (bool ok,) = target.call(abi.encodeWithSignature("overloadedTrustedForEachCaller()"));
+        require(ok, "overloadedTrustedForEachCaller reverted unexpectedly");
+    }
+    // Property 25: overloadedAdversarialForEachSetBitCaller has no unexpected revert
+    function testAuto_OverloadedAdversarialForEachSetBitCaller_NoUnexpectedRevert() public {
+        vm.prank(alice);
+        (bool ok,) = target.call(abi.encodeWithSignature("overloadedAdversarialForEachSetBitCaller()"));
+        require(ok, "overloadedAdversarialForEachSetBitCaller reverted unexpectedly");
+    }
+}
diff --git a/artifacts/macro_property_tests/PropertyQualifiedHelperLibrary.t.sol b/artifacts/macro_property_tests/PropertyQualifiedHelperLibrary.t.sol
new file mode 100644
index 000000000..b4ae08718
--- /dev/null
+++ b/artifacts/macro_property_tests/PropertyQualifiedHelperLibrary.t.sol
@@ -0,0 +1,58 @@
+// SPDX-License-Identifier: MIT
+pragma solidity ^0.8.33;
+
+import "./yul/YulTestBase.sol";
+
+/**
+ * @title PropertyQualifiedHelperLibraryTest
+ * @notice Auto-generated baseline property stubs from `verity_contract` declarations.
+ * @dev Source: Contracts/Smoke/SecurityCombos.lean
+ */
+contract PropertyQualifiedHelperLibraryTest is YulTestBase {
+    address target;
+    address alice = address(0x1111);
+
+    function setUp() public {
+        target = deployYul("QualifiedHelperLibrary");
+        require(target != address(0), "Deploy failed");
+    }
+
+    // Property 1: trustedEntry returns the direct parameter value
+    function testAuto_TrustedEntry_ReturnsDirectParam() public {
+        vm.prank(alice);
+        (bool ok, bytes memory ret) = target.call(abi.encodeWithSignature("trustedEntry(uint256)", uint256(1)));
+        require(ok, "trustedEntry reverted unexpectedly");
+        assertEq(ret.length, 32, "trustedEntry ABI return length mismatch (expected 32 bytes)");
+        uint256 actual = abi.decode(ret, (uint256));
+        assertEq(actual, uint256(1), "trustedEntry should preserve the expected value");
+    }
+    // Property 2: trustedPair decodes and matches the inferred tuple result
+    function testAuto_TrustedPair_ReturnsInferredTupleResult() public {
+        vm.prank(alice);
+        (bool ok, bytes memory ret) = target.call(abi.encodeWithSignature("trustedPair(uint256)", uint256(1)));
+        require(ok, "trustedPair reverted unexpectedly");
+        require(ret.length >= 64, "trustedPair ABI tuple return payload unexpectedly short");
+        (uint256 actual0, uint256 actual1) = abi.decode(ret, (uint256, uint256));
+        assertEq(actual0, uint256(1), "trustedPair tuple element 0 should preserve the inferred result");
+        assertEq(actual1, uint256(1), "trustedPair tuple element 1 should preserve the inferred result");
+    }
+    // Property 3: adversarialEntry returns the direct parameter value
+    function testAuto_AdversarialEntry_ReturnsDirectParam() public {
+        vm.prank(alice);
+        (bool ok, bytes memory ret) = target.call(abi.encodeWithSignature("adversarialEntry(uint256)", uint256(1)));
+        require(ok, "adversarialEntry reverted unexpectedly");
+        assertEq(ret.length, 32, "adversarialEntry ABI return length mismatch (expected 32 bytes)");
+        uint256 actual = abi.decode(ret, (uint256));
+        assertEq(actual, uint256(1), "adversarialEntry should preserve the expected value");
+    }
+    // Property 4: adversarialPair decodes and matches the inferred tuple result
+    function testAuto_AdversarialPair_ReturnsInferredTupleResult() public {
+        vm.prank(alice);
+        (bool ok, bytes memory ret) = target.call(abi.encodeWithSignature("adversarialPair(uint256)", uint256(1)));
+        require(ok, "adversarialPair reverted unexpectedly");
+        require(ret.length >= 64, "adversarialPair ABI tuple return payload unexpectedly short");
+        (uint256 actual0, uint256 actual1) = abi.decode(ret, (uint256, uint256));
+        assertEq(actual0, uint256(1), "adversarialPair tuple element 0 should preserve the inferred result");
+        assertEq(actual1, uint256(1), "adversarialPair tuple element 1 should preserve the inferred result");
+    }
+}
diff --git a/artifacts/trust_surface_report.json b/artifacts/trust_surface_report.json
index e4341d80c..71da346cf 100644
--- a/artifacts/trust_surface_report.json
+++ b/artifacts/trust_surface_report.json
@@ -169,7 +169,7 @@
   "mechanisms": {
     "@[implemented_by": 4,
     "native_decide": 479,
-    "partial def": 197
+    "partial def": 200
   },
   "notes": "native_decide trusts Lean.ofReduceBool or Lean 4.31 generated per-proof native_decide axioms + Lean.trustCompiler. Prose registry: docs/AXIOMS.md, docs/TRUST_ASSUMPTIONS.md (enforced by scripts/check_trust_surface_registry.py).",
   "schema_version": 1
diff --git a/artifacts/verification_status.json b/artifacts/verification_status.json
index 015a9839c..0032bfd16 100644
--- a/artifacts/verification_status.json
+++ b/artifacts/verification_status.json
@@ -1,6 +1,6 @@
 {
   "codebase": {
-    "core_lines": 2810,
+    "core_lines": 2813,
     "example_contracts": 19
   },
   "proofs": {
diff --git a/docs/ROADMAP.md b/docs/ROADMAP.md
index 73ddbb3e0..fe691d47f 100644
--- a/docs/ROADMAP.md
+++ b/docs/ROADMAP.md
@@ -257,7 +257,7 @@ Priority work for Verity core:
 | P1 | `sha256` / `sha256Packed` helper | Avoid hand-rolled SHA-256 precompile calls in public-signal construction. | `Compiler.Modules.Precompiles.sha256Memory` covers existing memory slices, with `sha256` as a short alias; `Compiler.Modules.Hashing.sha256PackedWords` covers static-word packed preimages, with `sha256Packed` as a short alias; `Compiler.Modules.Hashing.sha256PackedStaticSegments` covers static 1- to 32-byte segments. SHA-256 helpers route through precompile 0x02 with failure reverts and generated-Yul/trust-report tests. |
 | P1 | BN254 curve precompile ECMs | Avoid hand-rolled assembly for Groth16-style verifiers and other zkSNARK postcondition checks at the EVM boundary. | `Compiler.Modules.Precompiles.bn256Add` (0x06), `bn256ScalarMul` (0x07), and `bn256Pairing` (0x08) lower to staticcall against the EIP-196/EIP-197 precompiles, bind output coordinates / boolean word from scratch memory, revert on precompile failure, and surface a single `evm_bn256_*_precompile` trust assumption each; generated-Yul + trust-report smoke tests live in `Compiler/CompilationModelFeatureTest.lean`. |
 | P1 | `keccak256_lit` compile-time literal sugar | Make ERC-7201 namespaces and other Keccak-of-string constants safe and reviewable inside `verity_contract` bodies without ad-hoc Lean. | `Verity.Macro.KeccakLit` exposes `keccak256_nat` / `keccak256_lit` backed by the in-tree pure Keccak engine (`Compiler.Keccak.Sponge`) so authors can write `constants STORAGE_NAMESPACE : Uint256 := keccak256_lit "MyContract.storage.v0"`; the helpers are pure Lean definitions (no new trust assumption) with `native_decide`-checked test vectors against the official Keccak-256 empty-string digest. The follow-on `keccakString "<literal>"` term form (`Verity.Macro.KeccakString`, #1973) computes the digest at macro-expansion time and emits a `Uint256` numeric literal directly; it is parser-restricted to string literals (non-literal arguments are rejected at parse time) and is pattern-matched by the `verity_contract` translator, so EIP-712 type hashes, ERC-7201 namespaces, and event topic constants can be expressed without storage reads, without runtime hashing, and without per-author copies of the digest. |
-| P2 | Real `nonreentrant` guard semantics (#1893) | Upgrade the `nonreentrant(lockField)` annotation from a metadata/proof hook to a synthesised runtime guard so contracts can safely write state after external calls within reentrancy-protected entry points. | `Compiler.CompilationModel.Dispatch.attachNonReentrantGuard` (#1893) prepends a **transient-storage** acquire prologue — `if eq(tload(lockSlot), 1) { revert(0, 0) }; tstore(lockSlot, 1)` — immediately after parameter loading for any `nonreentrant(lockField)` external. Transient storage (TLOAD / TSTORE, EIP-1153, Cancun+) auto-clears at end-of-transaction, so no exit-path cleanup is needed and early `return` / `revert` / panic cannot leak the lock across transactions. CEI enforcement in `Compiler.CompilationModel.Validation.validateFunctionSpec` is now lifted for `nonReentrantLock.isSome` functions because the synthesised guard closes the post-interaction-write reentry window at runtime. The `validateNonReentrantForkCompatibility` pre-check (#1968) rejects any contract carrying a `nonreentrant(<lock>)` annotation when the targeted EVM fork predates Cancun, so the synthesised TLOAD/TSTORE opcodes cannot be silently emitted against a chain that does not expose them. Kept as a post-`compileFunctionSpec` transformation so the IR-generation proof modules continue to characterise the underlying body shape without a nonReentrantLock case split; the first version sits outside `SupportedSpec` (proof obligations for guarded specs are deferred). |
+| P2 | Real `nonreentrant` guard semantics (#1893) | Upgrade the `nonreentrant(lockField)` annotation from a metadata/proof hook to a synthesised runtime guard so contracts can safely write state after external calls within reentrancy-protected entry points. | `Compiler.CompilationModel.Dispatch.attachNonReentrantGuard` (#1893) prepends a **transient-storage** acquire prologue — `if tload(lockSlot) { revert(0, 0) }; tstore(lockSlot, 1)` — immediately after parameter loading for any `nonreentrant(lockField)` external. Transient storage (TLOAD / TSTORE, EIP-1153, Cancun+) auto-clears at end-of-transaction, so no exit-path cleanup is needed and early `return` / `revert` / panic cannot leak the lock across transactions. CEI enforcement in `Compiler.CompilationModel.Validation.validateFunctionSpec` is now lifted for `nonReentrantLock.isSome` functions because the synthesised guard closes the post-interaction-write reentry window at runtime. The `validateNonReentrantForkCompatibility` pre-check (#1968) rejects any contract carrying a `nonreentrant(<lock>)` annotation when the targeted EVM fork predates Cancun, so the synthesised TLOAD/TSTORE opcodes cannot be silently emitted against a chain that does not expose them. Kept as a post-`compileFunctionSpec` transformation so the IR-generation proof modules continue to characterise the underlying body shape without a nonReentrantLock case split; the first version sits outside `SupportedSpec` (proof obligations for guarded specs are deferred). |
 | P2 | BN254 scalar field helper | Improve readability of circuit-facing reductions. | `Verity.Stdlib.Math` exposes documented `SNARK_SCALAR_FIELD` and `modField` helpers with basic simp lemmas. |
 
 Already-supported items that should not become new roadmap work:
diff --git a/docs/TRUST_ASSUMPTIONS.md b/docs/TRUST_ASSUMPTIONS.md
index 75e2737fa..954f9a753 100644
--- a/docs/TRUST_ASSUMPTIONS.md
+++ b/docs/TRUST_ASSUMPTIONS.md
@@ -603,10 +603,29 @@ of byte-for-byte EVM ABI layout. Trust boundaries of that plane:
 - **Return values are deterministic stubs, not adversary models.** In-band
   words come from `externalCallStubWord`; the success bit is
   `externalCallStubSuccess` (`false` only for the reserved callee name
-  `"fail"`). Supported single-word results decode that same word; aggregate
-  and no-result stubs use their inhabited default. Executable-plane theorems
-  about call *outcomes* are therefore claims about the stub, not about a real
-  callee; adversarial reasoning lives in the model plane (`DenoteExternalCalls`).
+  `"fail"`). These are closed Lean definitions, not feature-flag, env-var, or
+  backend overrides. Supported single-word results decode that same word;
+  aggregate and no-result stubs use their inhabited default. Executable-plane
+  theorems about call *outcomes* are therefore claims about the stub, not about
+  a real callee; adversarial reasoning lives in the model plane
+  (`DenoteExternalCalls`).
+- **`ExecutableCallContext.ofAdversary` pins `target = 0` and `value = 0`.**
+  It is a convenience context, not a general linker: a nonzero target or value
+  requires `ofCallEnv` or a custom `resolve`. The generated registry predicate
+  does not depend on it: each `*_entrypoint` existentially quantifies the
+  executable resolver, so a transition produced by any `ExecutableCallContext`
+  carrying the registry adversary (including `ofCallEnv`) is a registered
+  transition. `CallbackBounded` therefore covers executable linked calls that
+  resolve a nonzero target/value, not only the zero boundary.
+- **Registry callback calldata is compiled-dispatch ABI, not the journal
+  encoder.** Generated `*_entrypoint` predicates constrain
+  `CallbackContext.calldata` with `abiEncodeDispatchArgs` /
+  `ToDispatchVal` (offset/length/packed-bytes layout matching
+  `genParamLoads`). `ExternalArg.toWords` remains the executable journal
+  encoding and is not an ABI decoder. Public `calldatasize`/`calldataload`
+  stay deterministic stubs (`0` and the offset); generated `*_registry`
+  bodies rewrite those intrinsics to `calldatasizeLive`/`calldataloadLive`,
+  which read `ContractState.calldata` installed by `withCallbackContext`.
 - **`externalCallWords` (pure expression form) does not journal.** It is not
   monadic, so `externalCall name [args]` used as a pure expression remains
   observationally silent; only the monadic forms journal. Specs that need
@@ -672,7 +691,7 @@ of byte-for-byte EVM ABI layout. Trust boundaries of that plane:
 ### Reentrancy Guard (`nonreentrant(lockField)`)
 Functions annotated `nonreentrant(lockField)` are compiled with a
 **transient-storage** reentrancy guard prologue (#1893): an
-`if eq(tload(lockSlot), 1) { revert(0, 0) }; tstore(lockSlot, 1)` pair runs
+`if tload(lockSlot) { revert(0, 0) }; tstore(lockSlot, 1)` pair runs
 before any user-authored Yul. Transient storage (EIP-1153, Cancun+) auto-clears
 at end-of-transaction, so the guard does not need an explicit release path —
 early `return`, `revert`, or panic cannot leak the lock across transactions.
@@ -689,8 +708,8 @@ reentry window is closed at the model level. On the compiled side,
 prologue/release statements under the IR interpreter: locked entry reverts
 untouched, free entry acquires the lock and changes nothing else, the spliced
 release resets it (acquire/release round-trips the transient store), and the
-Yul decision `eq(lock,1)` agrees with the model's `lock ≠ 0` on reachable
-binary lock values. `Compiler.Proofs.IRGeneration.SpliceSimulation` now proves the full guarded
+Yul decision `if tload(slot)` (nonzero is true) agrees with the model's `lock ≠ 0` for every
+stored lock value, not only the binary `{0,1}` acquire/release cycle. `Compiler.Proofs.IRGeneration.SpliceSimulation` now proves the full guarded
 unit end to end for the loop/switch-free fragment with compiler-emitted
 exits: the general splice simulation (`execIRStmts_spliced`), both
 `applyLockReleaseOnExits` branches, and
@@ -757,8 +776,37 @@ global invariant `I : ContractState → Prop`.
      externally reachable state transformer an adversary can invoke during a
      reentry window. Omitting a reachable entrypoint voids the guarantee
      (analogous to declaring the lock field for `nonreentrant`). The
-     macro-emitted entrypoint registry is the intended source of this list; until
-     that emission lands, the list is author-supplied.
+     macro-emitted entrypoint registry (`entrypointRegistry` and per-function
+      `*_registry` / `*_registry_unguarded` executables generated by
+      `verity_contract`) is the source of this list on the macro path.
+      Registry-mode `linked_contracts` hops use the bound callee's `*_registry`
+      executable (and thread the current `ExecutableCallContext`) when that
+      definition takes the context, including view/static callees whose public
+      bodies do not open a reentrancy window. Public hopCall bodies keep the
+      ctx-free public definition. Generated `*_entrypoint` predicates require
+      Lean arguments to match compiled-dispatch ABI words of
+      `CallbackContext.calldata` (`abiEncodeDispatchArgs` into
+      `dispatchCalldataMatches`); `receive` is registered only for empty
+      calldata. Registry-mode executables observe that same calldata through
+      `calldatasizeLive`/`calldataloadLive`, including the selected
+      entrypoint selector at `calldataload 0` (`CallbackContext.selector` /
+      `ContractState.selector`). `dispatchCalldataMatches` accepts
+      `genScalarLoad`-normalized noncanonical Bool / uintN / address words.
+      `FixedArray` encodes as a length-free composite (tuple of members);
+      source `Tuple` encodings are flattened before `abiEncodeDispatchArgs`.
+      Helpers whose bodies (transitively) read `calldatasize`/`calldataload`
+      are routed through `*_registry` so they observe live calldata.
+      Completeness of the generated
+      list is still an author obligation: the kernel checks consumers of
+      `entrypointRegistry`, it does not independently re-enumerate compiled
+      dispatcher cases. Same-contract `selfCall` hops keep the guarded public
+      / `*_registry` path so they still observe the nonReentrant tload
+      prologue. The Lean toolchain is pinned by `lean-toolchain`;
+      `threadAdversaryThroughExecutableSyntax` consults no IO or env vars.
+      Existing `unsafe qualifiedTupleBindTypedLocals` is elaborator-only
+      typed-local inference, not a kernel skip.
+     Author-supplied lists remain only for hand-written `ReentrancySpec`
+     consumers.
   2. **Adversary-model fidelity** — reentry is modeled as an arbitrary
      `ContractState → ContractState` over *this* contract's persistent channels
      (`adv` in `reentrantCall`). This captures self- and cross-contract reentry
diff --git a/scripts/measure.sh b/scripts/measure.sh
new file mode 100755
index 000000000..d3236afe7
--- /dev/null
+++ b/scripts/measure.sh
@@ -0,0 +1,18 @@
+#!/bin/sh
+# Time a full `lake build` and propagate its exit status (the previous
+# `lake build | tail` form returned tail's status, so a failed build exited 0).
+set -eu
+START=$(date +%s)
+echo "START: $(date -Iseconds)"
+LOG=$(mktemp)
+set +e
+lake build >"$LOG" 2>&1
+STATUS=$?
+set -e
+tail -20 "$LOG"
+rm -f "$LOG"
+END=$(date +%s)
+echo "DURATION: $((END-START))s"
+echo "END: $(date -Iseconds)"
+echo "BUILD_STATUS: $STATUS"
+exit "$STATUS"
diff --git a/scripts/refresh_verification_artifacts.sh b/scripts/refresh_verification_artifacts.sh
index 1b6ffa2eb..532ab6d27 100755
--- a/scripts/refresh_verification_artifacts.sh
+++ b/scripts/refresh_verification_artifacts.sh
@@ -11,6 +11,7 @@ python3 scripts/generate_verify_sync_spec.py
 python3 scripts/generate_evmyullean_capability_report.py
 python3 scripts/generate_evmyullean_native_lowering_report.py
 python3 scripts/generate_print_axioms.py
+python3 scripts/generate_trust_surface_report.py
 python3 scripts/sync_verification_status_doc.py
 
 echo "[refresh] Validating refreshed artifacts"
@@ -20,6 +21,7 @@ python3 scripts/generate_verify_sync_spec.py --check
 python3 scripts/generate_evmyullean_capability_report.py --check
 python3 scripts/generate_evmyullean_native_lowering_report.py --check
 python3 scripts/generate_print_axioms.py --check
+python3 scripts/generate_trust_surface_report.py --check
 python3 scripts/check_verification_status_doc.py
 python3 scripts/check_layer2_boundary_catalog_sync.py
 
diff --git a/scripts/verify_sync_spec.json b/scripts/verify_sync_spec.json
index 8f7daf79f..861a77678 100644
--- a/scripts/verify_sync_spec.json
+++ b/scripts/verify_sync_spec.json
@@ -3,9 +3,11 @@
     ".github/workflows/**",
     ".github/ISSUE_TEMPLATE/**",
     "artifacts/**",
+    "artifacts/*",
     "docs/**",
     "docs-site/**",
     "Makefile",
+    "PrintAxioms.lean",
     "README.md"
   ],
   "build_paths": [
@@ -833,6 +835,7 @@
     "python3 scripts/generate_evmyullean_capability_report.py --check",
     "python3 scripts/generate_evmyullean_native_lowering_report.py --check",
     "python3 scripts/generate_print_axioms.py --check",
+    "python3 scripts/generate_trust_surface_report.py --check",
     "python3 scripts/lean_lint.py --only proof_length",
     "python3 scripts/check_issue_1060_integrity.py",
     "python3 -m unittest discover -s scripts -p 'test_*.py' -v"
diff --git a/scripts/verify_sync_spec_source.py b/scripts/verify_sync_spec_source.py
index 912eabdfb..dd0c435b1 100644
--- a/scripts/verify_sync_spec_source.py
+++ b/scripts/verify_sync_spec_source.py
@@ -12,9 +12,11 @@
 SPEC = {'check_only_paths': ['.github/workflows/**',
                       '.github/ISSUE_TEMPLATE/**',
                       'artifacts/**',
+                      'artifacts/*',
                       'docs/**',
                       'docs-site/**',
                       'Makefile',
+                      'PrintAxioms.lean',
                       'README.md'],
  'build_paths': ['.github/actions/**',
                  '.github/workflows/verify.yml',
@@ -699,6 +701,7 @@
                                       'python3 scripts/generate_evmyullean_native_lowering_report.py '
                                       '--check',
                                       'python3 scripts/generate_print_axioms.py --check',
+                                      'python3 scripts/generate_trust_surface_report.py --check',
                                       'python3 scripts/lean_lint.py --only proof_length',
                                       'python3 scripts/check_issue_1060_integrity.py',
                                       "python3 -m unittest discover -s scripts -p 'test_*.py' -v"],