diff --git a/Compiler/CompilationModel/Dispatch.lean b/Compiler/CompilationModel/Dispatch.lean
index 8bd89a6bd2..370bf0958d 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 3a5729f4f1..2d95c80b13 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,9 @@ 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]
+/-- The emitted Yul and source model use the same nonzero lock decision. -/
+theorem guard_decision_agrees (v : Nat) : (v ≠ 0) ↔ v ≠ 0 := by
+  rfl
 
 /-- 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/Smoke/SecurityCombos.lean b/Contracts/Smoke/SecurityCombos.lean
index bd42e62e68..3a08251794 100644
--- a/Contracts/Smoke/SecurityCombos.lean
+++ b/Contracts/Smoke/SecurityCombos.lean
@@ -175,6 +175,140 @@ 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 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 bbf05cfad6..298c511985 100644
--- a/PrintAxioms.lean
+++ b/PrintAxioms.lean
@@ -38,6 +38,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.ListSum
 import Verity.Proofs.Stdlib.MappingAutomation
@@ -718,6 +719,11 @@ 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_reentry_blocked
+  Contracts.ReentrancyRelyGuarantee.generated_registry_callback_preserves
+
   -- Verity/Proofs/Stdlib/Automation.lean
   Verity.Proofs.Stdlib.Automation.isSuccess_success
   Verity.Proofs.Stdlib.Automation.isSuccess_revert
@@ -7515,4 +7521,4 @@ end Verity.AxiomAudit
   Compiler.Proofs.YulGeneration.YulTransaction.ofIR_args
 ]
 
--- Total: 6953 theorems/lemmas (4963 public, 1990 private, 0 sorry'd)
+-- Total: 6956 theorems/lemmas (4966 public, 1990 private, 0 sorry'd)
diff --git a/Verity/Core/Model/CallbackBridge.lean b/Verity/Core/Model/CallbackBridge.lean
index a262ca2533..b83306ae39 100644
--- a/Verity/Core/Model/CallbackBridge.lean
+++ b/Verity/Core/Model/CallbackBridge.lean
@@ -22,23 +22,217 @@ 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.  This keeps entrypoint arguments existential and, crucially,
+indexes every executable transition by the same 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
+
+/-- 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
+    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
+    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_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_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 +272,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 +288,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 0ca472b680..86ffc25f48 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 876e5efd2f..ba5feda449 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 1a521eadeb..51a20f56f5 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
@@ -176,6 +177,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 9e6a4cc966..79a77a7699 100644
--- a/Verity/Macro/Translate.lean
+++ b/Verity/Macro/Translate.lean
@@ -2265,6 +2265,19 @@ 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 syntaxCallsAnyHelper
     (helperNames : Array String) (stx : Syntax) : CommandElabM Bool := do
   match stx with
@@ -2394,15 +2407,68 @@ 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 threadHelperApp?
-    (adversarialHelpers : Array FunctionDecl) (name : Ident) (args : Array Term)
+    (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) : CommandElabM (Option Term) := do
-  let helper? := adversarialHelpers.find? fun fn =>
+  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 app ← helperCall name args
+      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
+      let registryOnly := registryOnlyHelpers.any (fun candidate =>
+        functionSignatureKey candidate == functionSignatureKey helper)
+      let target ←
+        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 name
+      if matchesExactHelper helper && adversarialHelpers.any (fun candidate =>
+          functionSignatureKey candidate == functionSignatureKey helper) then
+        some <$> helperCallWithAdv target args adv
+      else if helper.nonReentrantLock.isSome && helper.reentrancyTrusted then
+        some <$> helperCall target args
+      else
+        pure none
   | none => pure none
 
 private def rewriteTypedInterfaceCall?
@@ -2716,11 +2782,17 @@ 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) : CommandElabM Syntax := do
-  let go := threadAdversaryThroughExecutableSyntax externalDecls adversarialHelpers params adv
+  let go := threadAdversaryThroughExecutableSyntax fields constDecls immutableDecls
+    externalDecls helpers adversarialHelpers registryOnlyHelpers params locals adv
   let recurseChildren : CommandElabM Syntax := do
     match stx with
     | .node info kind args =>
@@ -2731,6 +2803,63 @@ private partial def threadAdversaryThroughExecutableSyntax
   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) :
@@ -2756,15 +2885,16 @@ 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 mut binds : Array (Ident × Term) := #[]
+        let mut rewrittenArgs : Array Term := #[]
+        for arg in args do
+          let (inner, rewritten) ← hoistNested true arg
+          binds := binds ++ inner
+          rewrittenArgs := rewrittenArgs.push rewritten
+        match ← threadHelperApp? fields constDecls immutableDecls externalDecls
+            helpers adversarialHelpers registryOnlyHelpers params locals name rewrittenArgs adv with
+        | some app => pure (binds, app)
         | none =>
-            let mut binds : Array (Ident × Term) := #[]
-            let mut rewrittenArgs : Array Term := #[]
-            for arg in args do
-              let (inner, rewritten) ← hoistNested true arg
-              binds := binds ++ inner
-              rewrittenArgs := rewrittenArgs.push rewritten
             let mut app : Term := ⟨name.raw⟩
             for arg in rewrittenArgs do
               app ← `(term| $app $arg)
@@ -2843,6 +2973,15 @@ private partial def threadAdversaryThroughExecutableSyntax
     let rest ← if outerWasBound then pureBinding pureValue else monadic rewritten
     wrapBinds binds rest
   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
+        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 := #[]
@@ -2893,7 +3032,8 @@ 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
+      match ← threadHelperApp? fields constDecls immutableDecls externalDecls
+          helpers adversarialHelpers registryOnlyHelpers params locals fn args adv with
       | some app => `(doElem| let $name ← $app:term)
       | none => recurseChildren
   | `(doElem| let $name:ident ← $fn:ident $args:term*) =>
@@ -2918,7 +3058,8 @@ 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 =>
@@ -3045,19 +3186,22 @@ private partial def threadAdversaryThroughExecutableSyntax
             let rewritten ← rewriteLinkedCallTerm externalDecls params adv 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
@@ -4956,11 +5100,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"
@@ -5044,6 +5190,8 @@ def validateGeneratedDefNamesPublic
 
     let helperNames :=
       #[ s!"{generatedFnName}_modelBody"
+       , s!"{generatedFnName}_entrypoint"
+       , s!"{generatedFnName}_registry"
        , s!"{generatedFnName}_model"
        , s!"{generatedFnName}_bridge"
        , s!"{generatedFnName}_semantic_preservation"
@@ -5059,6 +5207,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
@@ -5077,6 +5231,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)
@@ -5326,8 +5489,8 @@ def mkConstructorDefCommandPublic
       pure ⟨advIdent.raw⟩
     else
       `(Compiler.CompilationModel.DenoteExternalCalls.AdversaryModel.stub)
-  let executableBody := ⟨← threadAdversaryThroughExecutableSyntax externalDecls adversarialHelpers
-    ctor.params advTerm executableBody.raw⟩
+  let executableBody := ⟨← threadAdversaryThroughExecutableSyntax fields constDecls immutableDecls
+    externalDecls functions adversarialHelpers #[] ctor.params #[] advTerm executableBody.raw⟩
   let fnType ← if opensReentrancyWindow then
       mkContractFnTypeWithAdversary ctor.params .unit
     else
@@ -5396,8 +5559,8 @@ 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⟩
+      let executableBody := ⟨← threadAdversaryThroughExecutableSyntax fields constDecls immutableDecls
+        externalDecls functions ownAdversarialHelpers #[] ctor.params #[] advTerm executableBody.raw⟩
       let fnValue ← if containsExternalCall then
           mkContractFnValueWithAdversary advIdent ctor.params executableBody
         else
@@ -5423,6 +5586,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)
@@ -5494,8 +5671,13 @@ def mkFunctionCommandsPublic
       | some inlined => pure inlined
       | none => pure fn
   let stmtTerms ← translateBodyToStmtTerms fields roleDecls errorDecls constDecls immutableDecls externalDecls functions modelFn
+  -- Executable registry transitions must use the explicit adversary for every
+  -- external-call-dependent result, including static calls whose returndata
+  -- can influence a later storage write.  Reentrancy-window classification is
+  -- intentionally narrower and is therefore not sufficient for this path.
   let directlyOpensReentrancyWindow ← translatedBodyOpensReentrancyWindow stmtTerms
   let mut adversarialHelpers : Array FunctionDecl := #[]
+  let mut windowHelpers : Array FunctionDecl := #[]
   let mut translatedHelpers : Array (FunctionDecl × FunctionDecl) := #[]
   for helper in functions do
     let helperModel ←
@@ -5509,8 +5691,10 @@ def mkFunctionCommandsPublic
     let helperStmtTerms ← translateBodyToStmtTerms fields roleDecls errorDecls constDecls
       immutableDecls externalDecls functions helperModel
     translatedHelpers := translatedHelpers.push (helper, helperModel)
-    if ← translatedBodyOpensReentrancyWindow helperStmtTerms then
+    if ← translatedBodyContainsExternalCall helperStmtTerms then
       adversarialHelpers := adversarialHelpers.push helper
+    if ← translatedBodyOpensReentrancyWindow helperStmtTerms then
+      windowHelpers := windowHelpers.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.
@@ -5525,10 +5709,23 @@ def mkFunctionCommandsPublic
         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 => candidate.name == helper.name) &&
+          callsWindow then
+        windowHelpers := windowHelpers.push helper
+        grew := true
+    if !grew then
+      break
+  let windowNames := windowHelpers.map (·.name)
+  let callsWindow ← syntaxCallsAnyHelper windowNames modelFn.body.raw
+  let opensReentrancyWindow := directlyOpensReentrancyWindow || callsWindow
+  let registryOnlyHelpers := adversarialHelpers.filter fun helper =>
+    !windowHelpers.any (fun candidate =>
+      functionSignatureKey candidate == functionSignatureKey helper)
   -- 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
@@ -5540,12 +5737,51 @@ 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⟩
+  let registryExecutableBody := ⟨← threadAdversaryThroughExecutableSyntax fields constDecls immutableDecls
+    externalDecls functions adversarialHelpers registryOnlyHelpers fn.params #[]
+      (⟨advIdent.raw⟩ : Term) fnExecutableBody.raw⟩
+  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)
@@ -5566,6 +5802,44 @@ 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⟩
+  let mut applied : Term := registryId
+  applied ← `($applied (ExecutableCallContext.ofAdversary $registryAdv:ident))
+  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)
+  for (paramIdent, paramTy) in registryParams.reverse do
+    registryBody ← `(∃ $paramIdent:ident : $paramTy, $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
@@ -5592,7 +5866,25 @@ 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 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 0000000000..c320aed0cc
--- /dev/null
+++ b/Verity/Proofs/Model/GeneratedEntrypointRegistry.lean
@@ -0,0 +1,67 @@
+import Contracts.Common
+import Verity.Core.Model.CallbackBridge
+import Verity.Core.Model.NonReentrantGuard
+
+namespace Contracts.ReentrancyRelyGuarantee
+
+open Contracts
+open Verity hiding pure bind
+
+/-! 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
+
+open Compiler.CompilationModel.DenoteExternalCalls
+
+/-- The generated registry uses its explicit adversary at the external-call
+entrypoint; there is no `.stub` compatibility path in this theorem surface. -/
+theorem guardedPing_registered (adv : AdversaryModel) (ctx : CallbackContext)
+    (value : Uint256) (hvalue : ctx.msgValue = 0) :
+    entrypointRegistry adv
+      (callbackContractTransition ctx
+        (guardedPing_registry (ExecutableCallContext.ofAdversary adv) value)) := by
+  left
+  exact ⟨ctx, value, hvalue, rfl⟩
+
+/-- 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 (ExecutableCallContext.ofAdversary adv) value).runState state = state := by
+  apply Verity.Core.NonReentrantGuard.guarded_reentry_blocked
+  exact hlock
+
+end GeneratedRegistry
+
+open Compiler.CompilationModel.DenoteExternalCalls
+
+/-- `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 0000000000..9a290db10c
--- /dev/null
+++ b/artifacts/macro_property_tests/PropertyNonreentrantQualifiedHelperResolution.t.sol
@@ -0,0 +1,211 @@
+// 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: 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 17: 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 18: 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 19: 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 20: 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 21: 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 22: 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 23: 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 24: 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 0000000000..b4ae08718c
--- /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/docs-site/public/llms.txt b/docs-site/public/llms.txt
index b4b89b6647..5aef189f7a 100644
--- a/docs-site/public/llms.txt
+++ b/docs-site/public/llms.txt
@@ -31,7 +31,7 @@ Every transition inside the proof envelope is either fully verified or recorded
 
 <!-- BEGIN GENERATED QUICK FACTS -->
 - **Language**: Lean 4.31.0
-- **Core Size**: 1991 lines
+- **Core Size**: 2040 lines
 - **Verified Contracts**: 15 (Counter, ERC20, ERC721, Ledger, LocalObligationMacroSmoke, Ownable, Owned, OwnedCounter, OwnedCounterComposed, ReentrancyExample, ReentrancyRelyGuarantee, SafeCounter, SimpleStorage, SimpleToken, Vault)
 - **Theorems**: 329 across 15 categories, 329 fully proven
 - **Axioms**: 1 documented Lean axioms (see AXIOMS.md)