From a5ca06acd3a9d2d2f12da4aba60624a017e14f3a Mon Sep 17 00:00:00 2001
From: Thomas Marchand <thomas@lfglabs.dev>
Date: Sun, 6 Sep 2026 23:51:50 +0000
Subject: [PATCH 01/27] feat(macro): generate adversary-indexed entrypoint
 registry

---
 .../ReentrancyRelyGuarantee/Contract.lean     |  4 +-
 Verity/Core/Model/CallbackBridge.lean         | 26 +++++++--
 Verity/Macro/Elaborate.lean                   |  2 +
 Verity/Macro/Translate.lean                   | 55 ++++++++++++++++++-
 4 files changed, 78 insertions(+), 9 deletions(-)

diff --git a/Contracts/ReentrancyRelyGuarantee/Contract.lean b/Contracts/ReentrancyRelyGuarantee/Contract.lean
index 1ca9273517..9871914cc8 100644
--- a/Contracts/ReentrancyRelyGuarantee/Contract.lean
+++ b/Contracts/ReentrancyRelyGuarantee/Contract.lean
@@ -203,7 +203,7 @@ any `CallProgram`, and through the transaction commit/revert boundary. -/
 open Compiler.CompilationModel.DenoteExternalCalls in
 theorem callback_bounded_program_preserves_I
     {adversary : AdversaryModel}
-    (hbound : CallbackBounded spec.entrypoints adversary)
+    (hbound : CallbackBounded (EntrypointRegistry.ofList spec.entrypoints) adversary)
     (prog : CallProgram α) (state : CallState) (hInv : I state.world) :
     I (denote prog adversary state).2.world :=
   hbound.denote_preserves spec prog state hInv
@@ -211,7 +211,7 @@ theorem callback_bounded_program_preserves_I
 open Compiler.CompilationModel.DenoteExternalCalls in
 theorem callback_bounded_transaction_preserves_I
     {adversary : AdversaryModel} {α : Type}
-    (hbound : CallbackBounded spec.entrypoints adversary)
+    (hbound : CallbackBounded (EntrypointRegistry.ofList spec.entrypoints) adversary)
     (prog : CallProgram (TransactionResult α)) (state : CallState)
     (hInv : I state.world) :
     I (denoteTransaction prog adversary state).state.world :=
diff --git a/Verity/Core/Model/CallbackBridge.lean b/Verity/Core/Model/CallbackBridge.lean
index a262ca2533..40f2ba0c09 100644
--- a/Verity/Core/Model/CallbackBridge.lean
+++ b/Verity/Core/Model/CallbackBridge.lean
@@ -22,15 +22,31 @@ 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
+
+end EntrypointRegistry
+
 /-- 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
 
 /-- One external call under a callback-bounded adversary preserves the spec
@@ -38,7 +54,7 @@ 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 +94,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 +110,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/Macro/Elaborate.lean b/Verity/Macro/Elaborate.lean
index 1a521eadeb..723755bd4e 100644
--- a/Verity/Macro/Elaborate.lean
+++ b/Verity/Macro/Elaborate.lean
@@ -176,6 +176,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..031ff08a5f 100644
--- a/Verity/Macro/Translate.lean
+++ b/Verity/Macro/Translate.lean
@@ -16,6 +16,8 @@ import Verity.Macro.Internal
 import Verity.Macro.Storage
 import Verity.Macro.Types
 import Verity.Macro.Syntax
+import Verity.Core.Model.CallbackBridge
+import Verity.Core.Model.NonReentrantGuard
 
 namespace Verity.Macro
 
@@ -4960,7 +4962,7 @@ def validateGeneratedDefNamesPublic
     (constDecls : Array ConstantDecl)
     (immutableDecls : Array ImmutableDecl)
     (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"
@@ -5542,6 +5544,13 @@ def mkFunctionCommandsPublic
       mkContractFnType fn.params fn.returnTy
   let fnExecutableBody := ⟨← threadAdversaryThroughExecutableSyntax externalDecls
     adversarialHelpers fn.params advTerm fnExecutableBody.raw⟩
+  let fnExecutableBody ← 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) $fnExecutableBody)
+    | none => pure fnExecutableBody
   let fnValue ← if opensReentrancyWindow then
       mkContractFnValueWithAdversary advIdent fn.params fnExecutableBody
     else
@@ -5566,6 +5575,32 @@ 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 mut applied : Term := fn.ident
+  if opensReentrancyWindow then
+    applied ← `($applied (ExecutableCallContext.ofAdversary $(⟨registryAdvIdent.raw⟩)))
+  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
+    registryParams := registryParams.push (⟨paramIdent.raw⟩, paramTy)
+    applied ← `($applied $(⟨paramIdent.raw⟩))
+  let mut registryBody : Term ←
+    `(($(⟨transitionIdent.raw⟩) : Verity.ContractState → Verity.ContractState) =
+      ($applied).runState)
+  for (paramIdent, paramTy) in registryParams.reverse do
+    registryBody ← `(∃ $paramIdent : $paramTy, $registryBody)
+  let entrypointCmd : Cmd ← `(command|
+    def $entrypointPredicateName
+        ($(⟨registryAdvIdent.raw⟩) :
+          Compiler.CompilationModel.DenoteExternalCalls.AdversaryModel)
+        ($(⟨transitionIdent.raw⟩) : 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 +5627,23 @@ def mkFunctionCommandsPublic
     body := $modelBodyName
     isInternal := $internalTerm
   })
-  pure #[fnCmd, bodyCmd, modelCmd]
+  pure #[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 mut body : Term ← `(False)
+  for fn in functions.reverse do
+    unless fn.isInternal do
+      let predicateName ← mkSuffixedIdent fn.ident "_entrypoint"
+      body ← `($predicateName $(⟨advIdent.raw⟩) $(⟨transitionIdent.raw⟩) ∨ $body)
+  let id := mkIdent (Name.mkSimple "entrypointRegistry")
+  `(command|
+    def $id : Compiler.CompilationModel.DenoteExternalCalls.EntrypointRegistry :=
+      fun $(⟨advIdent.raw⟩) $(⟨transitionIdent.raw⟩) => $body)
 
 def mkSpecCommandPublic
     (contractName : String)

From b688deed98287bb38164e3d39b1a656cc63a1352 Mon Sep 17 00:00:00 2001
From: Thomas Marchand <thomas@lfglabs.dev>
Date: Sun, 6 Sep 2026 23:56:32 +0000
Subject: [PATCH 02/27] fix(macro): load registry semantics at elaboration
 boundary

---
 Verity/Macro/Elaborate.lean | 2 ++
 Verity/Macro/Translate.lean | 2 --
 2 files changed, 2 insertions(+), 2 deletions(-)

diff --git a/Verity/Macro/Elaborate.lean b/Verity/Macro/Elaborate.lean
index 723755bd4e..ac684bb208 100644
--- a/Verity/Macro/Elaborate.lean
+++ b/Verity/Macro/Elaborate.lean
@@ -5,6 +5,8 @@ import Verity.Macro.Translate
 import Verity.Macro.Bridge
 import Verity.Core.Intrinsics
 import Verity.Core.Uint256
+import Verity.Core.Model.CallbackBridge
+import Verity.Core.Model.NonReentrantGuard
 
 namespace Verity.Macro
 
diff --git a/Verity/Macro/Translate.lean b/Verity/Macro/Translate.lean
index 031ff08a5f..a4f6a26dd9 100644
--- a/Verity/Macro/Translate.lean
+++ b/Verity/Macro/Translate.lean
@@ -16,8 +16,6 @@ import Verity.Macro.Internal
 import Verity.Macro.Storage
 import Verity.Macro.Types
 import Verity.Macro.Syntax
-import Verity.Core.Model.CallbackBridge
-import Verity.Core.Model.NonReentrantGuard
 
 namespace Verity.Macro
 

From 8a1d59008774114c47fd956a18df27c7b2d11df5 Mon Sep 17 00:00:00 2001
From: Thomas Marchand <thomas@lfglabs.dev>
Date: Mon, 7 Sep 2026 00:01:53 +0000
Subject: [PATCH 03/27] fix(macro): construct registry binders hygienically

---
 Verity/Macro/Translate.lean | 23 ++++++++++++++---------
 1 file changed, 14 insertions(+), 9 deletions(-)

diff --git a/Verity/Macro/Translate.lean b/Verity/Macro/Translate.lean
index a4f6a26dd9..c8808d8023 100644
--- a/Verity/Macro/Translate.lean
+++ b/Verity/Macro/Translate.lean
@@ -5578,26 +5578,29 @@ def mkFunctionCommandsPublic
     (mkIdentFrom fn.ident `_registryAdv).raw
   let transitionIdent ← Lean.Elab.Term.mkFreshIdent
     (mkIdentFrom fn.ident `_transition).raw
+  let registryAdv : Ident := ⟨registryAdvIdent.raw⟩
+  let transition : Ident := ⟨transitionIdent.raw⟩
   let mut applied : Term := fn.ident
   if opensReentrancyWindow then
-    applied ← `($applied (ExecutableCallContext.ofAdversary $(⟨registryAdvIdent.raw⟩)))
+    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
-    registryParams := registryParams.push (⟨paramIdent.raw⟩, paramTy)
-    applied ← `($applied $(⟨paramIdent.raw⟩))
+    let registryParam : Ident := ⟨paramIdent.raw⟩
+    registryParams := registryParams.push (registryParam, paramTy)
+    applied ← `($applied $registryParam:ident)
   let mut registryBody : Term ←
-    `(($(⟨transitionIdent.raw⟩) : Verity.ContractState → Verity.ContractState) =
+    `(($transition:ident : Verity.ContractState → Verity.ContractState) =
       ($applied).runState)
   for (paramIdent, paramTy) in registryParams.reverse do
-    registryBody ← `(∃ $paramIdent : $paramTy, $registryBody)
+    registryBody ← `(∃ $paramIdent:ident : $paramTy, $registryBody)
   let entrypointCmd : Cmd ← `(command|
     def $entrypointPredicateName
-        ($(⟨registryAdvIdent.raw⟩) :
+        ($registryAdv:ident :
           Compiler.CompilationModel.DenoteExternalCalls.AdversaryModel)
-        ($(⟨transitionIdent.raw⟩) : Verity.ContractState → Verity.ContractState) : Prop :=
+        ($transition:ident : Verity.ContractState → Verity.ContractState) : Prop :=
       $registryBody)
   let bodyCmd : Cmd ← `(command| def $modelBodyName : List Compiler.CompilationModel.Stmt := [ $[$stmtTerms],* ])
   let modelNameTerm :=
@@ -5633,15 +5636,17 @@ 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 $(⟨advIdent.raw⟩) $(⟨transitionIdent.raw⟩) ∨ $body)
+      body ← `($predicateName $registryAdv:ident $transition:ident ∨ $body)
   let id := mkIdent (Name.mkSimple "entrypointRegistry")
   `(command|
     def $id : Compiler.CompilationModel.DenoteExternalCalls.EntrypointRegistry :=
-      fun $(⟨advIdent.raw⟩) $(⟨transitionIdent.raw⟩) => $body)
+      fun $registryAdv:ident $transition:ident => $body)
 
 def mkSpecCommandPublic
     (contractName : String)

From 54c7273996b935a2811c67cea04973b9a8cedbfb Mon Sep 17 00:00:00 2001
From: Thomas Marchand <thomas@lfglabs.dev>
Date: Mon, 7 Sep 2026 00:39:45 +0000
Subject: [PATCH 04/27] proof(reentrancy): consume generated callback registry

---
 .../ReentrancyRelyGuarantee/Contract.lean     | 18 +++++++
 .../GeneratedRegistry.lean                    | 48 ++++++++++++++++++
 Verity/Core/Model/CallbackBridge.lean         | 49 +++++++++++++++++++
 Verity/Macro.lean                             |  2 +
 Verity/Macro/Elaborate.lean                   |  2 -
 5 files changed, 117 insertions(+), 2 deletions(-)
 create mode 100644 Contracts/ReentrancyRelyGuarantee/GeneratedRegistry.lean

diff --git a/Contracts/ReentrancyRelyGuarantee/Contract.lean b/Contracts/ReentrancyRelyGuarantee/Contract.lean
index 9871914cc8..f30dc7cf84 100644
--- a/Contracts/ReentrancyRelyGuarantee/Contract.lean
+++ b/Contracts/ReentrancyRelyGuarantee/Contract.lean
@@ -22,6 +22,7 @@ import Verity.Core
 import Verity.Core.Semantics
 import Verity.Core.Reentrancy
 import Verity.Core.Model.CallbackBridge
+import Contracts.ReentrancyRelyGuarantee.GeneratedRegistry
 
 namespace Contracts.ReentrancyRelyGuarantee
 
@@ -217,4 +218,21 @@ theorem callback_bounded_transaction_preserves_I
     I (denoteTransaction prog adversary state).state.world :=
   hbound.transaction_preserves spec prog state hInv
 
+/-! ## Generated-registry consumer boundary -/
+
+/- `ReentrancyRelyGuarantee` consumes the macro-emitted registry directly at
+the callback boundary.  This deliberately small invariant isolates the PR4
+connection; contract-specific preservation obligations remain with authors. -/
+open Compiler.CompilationModel.DenoteExternalCalls in
+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/Contracts/ReentrancyRelyGuarantee/GeneratedRegistry.lean b/Contracts/ReentrancyRelyGuarantee/GeneratedRegistry.lean
new file mode 100644
index 0000000000..de24734ff8
--- /dev/null
+++ b/Contracts/ReentrancyRelyGuarantee/GeneratedRegistry.lean
@@ -0,0 +1,48 @@
+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) (value : Uint256) :
+    entrypointRegistry adv
+      (guardedPing (ExecutableCallContext.ofAdversary adv) value).runState := by
+  left
+  exact ⟨value, 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
+end Contracts.ReentrancyRelyGuarantee
diff --git a/Verity/Core/Model/CallbackBridge.lean b/Verity/Core/Model/CallbackBridge.lean
index 40f2ba0c09..f2dae8866a 100644
--- a/Verity/Core/Model/CallbackBridge.lean
+++ b/Verity/Core/Model/CallbackBridge.lean
@@ -49,6 +49,55 @@ def CallbackBounded
       (∀ 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. -/
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 ac684bb208..723755bd4e 100644
--- a/Verity/Macro/Elaborate.lean
+++ b/Verity/Macro/Elaborate.lean
@@ -5,8 +5,6 @@ import Verity.Macro.Translate
 import Verity.Macro.Bridge
 import Verity.Core.Intrinsics
 import Verity.Core.Uint256
-import Verity.Core.Model.CallbackBridge
-import Verity.Core.Model.NonReentrantGuard
 
 namespace Verity.Macro
 

From 4af7eaf829f585491aea8c3b8dacb03319667744 Mon Sep 17 00:00:00 2001
From: Thomas Marchand <thomas@lfglabs.dev>
Date: Mon, 7 Sep 2026 00:47:39 +0000
Subject: [PATCH 05/27] chore(audit): sync registry consumer artifacts

---
 Contracts/ReentrancyRelyGuarantee/Contract.lean    |  2 +-
 .../Proofs/Model/GeneratedEntrypointRegistry.lean  |  0
 artifacts/verification_status.json                 | 12 ++++++------
 docs/VERIFICATION_STATUS.md                        | 14 +++++++-------
 test/property_exclusions.json                      |  1 +
 test/property_manifest.json                        |  1 +
 6 files changed, 16 insertions(+), 14 deletions(-)
 rename Contracts/ReentrancyRelyGuarantee/GeneratedRegistry.lean => Verity/Proofs/Model/GeneratedEntrypointRegistry.lean (100%)

diff --git a/Contracts/ReentrancyRelyGuarantee/Contract.lean b/Contracts/ReentrancyRelyGuarantee/Contract.lean
index f30dc7cf84..1a26cdd81b 100644
--- a/Contracts/ReentrancyRelyGuarantee/Contract.lean
+++ b/Contracts/ReentrancyRelyGuarantee/Contract.lean
@@ -22,7 +22,7 @@ import Verity.Core
 import Verity.Core.Semantics
 import Verity.Core.Reentrancy
 import Verity.Core.Model.CallbackBridge
-import Contracts.ReentrancyRelyGuarantee.GeneratedRegistry
+import Verity.Proofs.Model.GeneratedEntrypointRegistry
 
 namespace Contracts.ReentrancyRelyGuarantee
 
diff --git a/Contracts/ReentrancyRelyGuarantee/GeneratedRegistry.lean b/Verity/Proofs/Model/GeneratedEntrypointRegistry.lean
similarity index 100%
rename from Contracts/ReentrancyRelyGuarantee/GeneratedRegistry.lean
rename to Verity/Proofs/Model/GeneratedEntrypointRegistry.lean
diff --git a/artifacts/verification_status.json b/artifacts/verification_status.json
index 3ed6aeae48..401522c405 100644
--- a/artifacts/verification_status.json
+++ b/artifacts/verification_status.json
@@ -16,10 +16,10 @@
   },
   "theorems": {
     "categories": 15,
-    "coverage_percent": 78,
+    "coverage_percent": 77,
     "covered": 255,
-    "excluded": 74,
-    "non_stdlib_total": 329,
+    "excluded": 75,
+    "non_stdlib_total": 330,
     "per_contract": {
       "Counter": 31,
       "ERC20": 22,
@@ -31,15 +31,15 @@
       "OwnedCounter": 63,
       "OwnedCounterComposed": 6,
       "ReentrancyExample": 5,
-      "ReentrancyRelyGuarantee": 10,
+      "ReentrancyRelyGuarantee": 11,
       "SafeCounter": 25,
       "SimpleStorage": 20,
       "SimpleToken": 61,
       "Vault": 9
     },
-    "proven": 329,
+    "proven": 330,
     "stdlib": 0,
-    "total": 329
+    "total": 330
   },
   "toolchain": {
     "lean": "leanprover/lean4:v4.31.0",
diff --git a/docs/VERIFICATION_STATUS.md b/docs/VERIFICATION_STATUS.md
index 08f4684387..87a3166381 100644
--- a/docs/VERIFICATION_STATUS.md
+++ b/docs/VERIFICATION_STATUS.md
@@ -40,11 +40,11 @@ EVM Bytecode
 | ERC721 | 11 | Baseline | `Contracts/ERC721/Proofs/` |
 | Vault | 9 | Baseline | `Contracts/Vault/Proofs/` |
 | ReentrancyExample | 5 | Complete | `Contracts/ReentrancyExample/Contract.lean` |
-| ReentrancyRelyGuarantee | 10 | Semantic | `Contracts/ReentrancyRelyGuarantee/Contract.lean` |
+| ReentrancyRelyGuarantee | 11 | Semantic | `Contracts/ReentrancyRelyGuarantee/Contract.lean` |
 | CryptoHash | 0 | No specs | `Contracts/CryptoHash/Contract.lean` |
-| **Total** | **329** | **✅ 100%** | — |
+| **Total** | **330** | **✅ 100%** | — |
 
-> **Note**: Stdlib (0 internal proof-automation properties) is excluded from the contract-spec theorem table above but included in overall coverage statistics (329 total properties).
+> **Note**: Stdlib (0 internal proof-automation properties) is excluded from the contract-spec theorem table above but included in overall coverage statistics (330 total properties).
 
 Layer 1 uses macro-generated EDSL-to-`CompilationModel` bridge theorems backed by a generic typed-IR compilation-correctness theorem ([`TypedIRCompilerCorrectness.lean`](../Compiler/TypedIRCompilerCorrectness.lean)). Tuple/bytes/fixed-array/dynamic-array/string parameters now stay inside that proof path when they are carried as ABI head words/offsets. Advanced constructs beyond that typed-IR head-word surface (linked libraries, ECMs, fully custom ABI behavior) are still expressed directly in `CompilationModel` and trusted at that boundary. Higher-order internal helpers (function-pointer parameters, [#1747](https://github.com/lfglabs-dev/verity/issues/1747)) are eliminated by a compile-time monomorphization pre-pass that runs before any lowering, so the `CompilationModel` only ever contains first-order helpers: these calls are covered by the existing first-order proof path and introduce no new boundary trust.
 
@@ -205,7 +205,7 @@ Also note that the macro-generated `*_semantic_preservation` theorems are not co
 | ERC721 | 100% (11/11) | 0 |
 | SafeCounter | 100% (25/25) | 0 |
 | ReentrancyExample | 100% (5/5) | 0 |
-| ReentrancyRelyGuarantee | 0% (0/10) | 10 proof-only |
+| ReentrancyRelyGuarantee | 0% (0/11) | 11 proof-only |
 | Ledger | 100% (33/33) | 0 |
 | LocalObligationMacroSmoke | 100% (4/4) | 0 |
 | SimpleStorage | 95% (19/20) | 1 proof-only |
@@ -217,11 +217,11 @@ Also note that the macro-generated `*_semantic_preservation` theorems are not co
 | Counter | 74% (23/31) | 8 proof-only |
 | Stdlib | 0% (0/0) | 0 proof-only |
 
-**Status**: 78% coverage (255/329), 74 remaining exclusions all proof-only
+**Status**: 77% coverage (255/330), 75 remaining exclusions all proof-only
 
-- **Total Properties**: 329
+- **Total Properties**: 330
 - **Covered**: 255
-- **Excluded**: 74 (all proof-only)
+- **Excluded**: 75 (all proof-only)
 
 **Proof-Only Properties (59 exclusions)**: Internal proof machinery that cannot be tested in Foundry.
 
diff --git a/test/property_exclusions.json b/test/property_exclusions.json
index b02ea2d277..788bff1dbf 100644
--- a/test/property_exclusions.json
+++ b/test/property_exclusions.json
@@ -87,6 +87,7 @@
   "buggy_admits_permanent_bad_debt",
   "callback_bounded_program_preserves_I",
   "callback_bounded_transaction_preserves_I",
+  "generated_registry_callback_preserves",
   "liquidate_preserves_I",
   "liquidate_respects_lock",
   "locked_blocks_concrete_liquidation",
diff --git a/test/property_manifest.json b/test/property_manifest.json
index b43566798a..45b508baf6 100644
--- a/test/property_manifest.json
+++ b/test/property_manifest.json
@@ -229,6 +229,7 @@
     "buggy_admits_permanent_bad_debt",
     "callback_bounded_program_preserves_I",
     "callback_bounded_transaction_preserves_I",
+    "generated_registry_callback_preserves",
     "liquidate_preserves_I",
     "liquidate_respects_lock",
     "locked_blocks_concrete_liquidation",

From c98bcbc8b6568a67ffbd828a330128d48e6937b2 Mon Sep 17 00:00:00 2001
From: Thomas Marchand <thomas@lfglabs.dev>
Date: Mon, 7 Sep 2026 00:48:20 +0000
Subject: [PATCH 06/27] chore(audit): register generated registry proofs

---
 PrintAxioms.lean | 7 ++++++-
 1 file changed, 6 insertions(+), 1 deletion(-)

diff --git a/PrintAxioms.lean b/PrintAxioms.lean
index bbf05cfad6..0fb2c66d76 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,10 @@ 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
+
   -- Verity/Proofs/Stdlib/Automation.lean
   Verity.Proofs.Stdlib.Automation.isSuccess_success
   Verity.Proofs.Stdlib.Automation.isSuccess_revert
@@ -7515,4 +7520,4 @@ end Verity.AxiomAudit
   Compiler.Proofs.YulGeneration.YulTransaction.ofIR_args
 ]
 
--- Total: 6953 theorems/lemmas (4963 public, 1990 private, 0 sorry'd)
+-- Total: 6955 theorems/lemmas (4965 public, 1990 private, 0 sorry'd)

From ccf79f911a10433b2503fd1aa7b358da5c9472bc Mon Sep 17 00:00:00 2001
From: Thomas Marchand <thomas@lfglabs.dev>
Date: Mon, 7 Sep 2026 00:50:56 +0000
Subject: [PATCH 07/27] chore(docs): sync proof counts

---
 docs-site/public/llms.txt | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

diff --git a/docs-site/public/llms.txt b/docs-site/public/llms.txt
index b4b89b6647..6cb26e71ad 100644
--- a/docs-site/public/llms.txt
+++ b/docs-site/public/llms.txt
@@ -31,9 +31,9 @@ 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
+- **Theorems**: 330 across 15 categories, 330 fully proven
 - **Axioms**: 1 documented Lean axioms (see AXIOMS.md)
 - **Tests**: 528 Foundry tests, 239 property tests
 - **Build**: `lake build` verifies all proofs

From ed2b7c089e3b2dca7d425dac5af82c587b5b5cd4 Mon Sep 17 00:00:00 2001
From: Thomas Marchand <thomas@lfglabs.dev>
Date: Mon, 7 Sep 2026 09:26:33 +0000
Subject: [PATCH 08/27] fix(reentrancy): preserve no-call contract surface

---
 .../ReentrancyRelyGuarantee/Contract.lean     | 22 ++-----------------
 Verity/Core/Model/CallbackBridge.lean         |  4 ++++
 .../Model/GeneratedEntrypointRegistry.lean    | 15 +++++++++++++
 3 files changed, 21 insertions(+), 20 deletions(-)

diff --git a/Contracts/ReentrancyRelyGuarantee/Contract.lean b/Contracts/ReentrancyRelyGuarantee/Contract.lean
index 1a26cdd81b..1ca9273517 100644
--- a/Contracts/ReentrancyRelyGuarantee/Contract.lean
+++ b/Contracts/ReentrancyRelyGuarantee/Contract.lean
@@ -22,7 +22,6 @@ import Verity.Core
 import Verity.Core.Semantics
 import Verity.Core.Reentrancy
 import Verity.Core.Model.CallbackBridge
-import Verity.Proofs.Model.GeneratedEntrypointRegistry
 
 namespace Contracts.ReentrancyRelyGuarantee
 
@@ -204,7 +203,7 @@ any `CallProgram`, and through the transaction commit/revert boundary. -/
 open Compiler.CompilationModel.DenoteExternalCalls in
 theorem callback_bounded_program_preserves_I
     {adversary : AdversaryModel}
-    (hbound : CallbackBounded (EntrypointRegistry.ofList spec.entrypoints) adversary)
+    (hbound : CallbackBounded spec.entrypoints adversary)
     (prog : CallProgram α) (state : CallState) (hInv : I state.world) :
     I (denote prog adversary state).2.world :=
   hbound.denote_preserves spec prog state hInv
@@ -212,27 +211,10 @@ theorem callback_bounded_program_preserves_I
 open Compiler.CompilationModel.DenoteExternalCalls in
 theorem callback_bounded_transaction_preserves_I
     {adversary : AdversaryModel} {α : Type}
-    (hbound : CallbackBounded (EntrypointRegistry.ofList spec.entrypoints) adversary)
+    (hbound : CallbackBounded spec.entrypoints adversary)
     (prog : CallProgram (TransactionResult α)) (state : CallState)
     (hInv : I state.world) :
     I (denoteTransaction prog adversary state).state.world :=
   hbound.transaction_preserves spec prog state hInv
 
-/-! ## Generated-registry consumer boundary -/
-
-/- `ReentrancyRelyGuarantee` consumes the macro-emitted registry directly at
-the callback boundary.  This deliberately small invariant isolates the PR4
-connection; contract-specific preservation obligations remain with authors. -/
-open Compiler.CompilationModel.DenoteExternalCalls in
-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/Verity/Core/Model/CallbackBridge.lean b/Verity/Core/Model/CallbackBridge.lean
index f2dae8866a..782c64e645 100644
--- a/Verity/Core/Model/CallbackBridge.lean
+++ b/Verity/Core/Model/CallbackBridge.lean
@@ -36,6 +36,10 @@ 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
 
 /-- Each mutable transition is some finite reentry schedule drawn from the
diff --git a/Verity/Proofs/Model/GeneratedEntrypointRegistry.lean b/Verity/Proofs/Model/GeneratedEntrypointRegistry.lean
index de24734ff8..709ee00208 100644
--- a/Verity/Proofs/Model/GeneratedEntrypointRegistry.lean
+++ b/Verity/Proofs/Model/GeneratedEntrypointRegistry.lean
@@ -45,4 +45,19 @@ theorem guardedPing_reentry_blocked (adv : AdversaryModel) (value : Uint256)
   exact hlock
 
 end GeneratedRegistry
+
+/-- `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

From 0411dfa04d83249df05b79527d10c04ab1f57ee3 Mon Sep 17 00:00:00 2001
From: "github-actions[bot]" <github-actions[bot]@users.noreply.github.com>
Date: Mon, 7 Sep 2026 10:30:27 +0100
Subject: [PATCH 09/27] chore: auto-refresh derived artifacts

---
 PrintAxioms.lean | 3 ++-
 1 file changed, 2 insertions(+), 1 deletion(-)

diff --git a/PrintAxioms.lean b/PrintAxioms.lean
index 0fb2c66d76..298c511985 100644
--- a/PrintAxioms.lean
+++ b/PrintAxioms.lean
@@ -722,6 +722,7 @@ end Verity.AxiomAudit
   -- 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
@@ -7520,4 +7521,4 @@ end Verity.AxiomAudit
   Compiler.Proofs.YulGeneration.YulTransaction.ofIR_args
 ]
 
--- Total: 6955 theorems/lemmas (4965 public, 1990 private, 0 sorry'd)
+-- Total: 6956 theorems/lemmas (4966 public, 1990 private, 0 sorry'd)

From c6a4a973b7d4e41e01dc51aa73ce87a99609ae20 Mon Sep 17 00:00:00 2001
From: Thomas Marchand <thomas@lfglabs.dev>
Date: Mon, 7 Sep 2026 09:37:57 +0000
Subject: [PATCH 10/27] chore(audit): sync registry proof manifest

---
 test/property_manifest.json | 1 -
 1 file changed, 1 deletion(-)

diff --git a/test/property_manifest.json b/test/property_manifest.json
index 45b508baf6..b43566798a 100644
--- a/test/property_manifest.json
+++ b/test/property_manifest.json
@@ -229,7 +229,6 @@
     "buggy_admits_permanent_bad_debt",
     "callback_bounded_program_preserves_I",
     "callback_bounded_transaction_preserves_I",
-    "generated_registry_callback_preserves",
     "liquidate_preserves_I",
     "liquidate_respects_lock",
     "locked_blocks_concrete_liquidation",

From d51100ab7acac7040483203efd97f335942c083a Mon Sep 17 00:00:00 2001
From: Thomas Marchand <thomas@lfglabs.dev>
Date: Mon, 7 Sep 2026 09:38:27 +0000
Subject: [PATCH 11/27] chore(audit): sync registry proof exclusions

---
 test/property_exclusions.json | 1 -
 1 file changed, 1 deletion(-)

diff --git a/test/property_exclusions.json b/test/property_exclusions.json
index 788bff1dbf..b02ea2d277 100644
--- a/test/property_exclusions.json
+++ b/test/property_exclusions.json
@@ -87,7 +87,6 @@
   "buggy_admits_permanent_bad_debt",
   "callback_bounded_program_preserves_I",
   "callback_bounded_transaction_preserves_I",
-  "generated_registry_callback_preserves",
   "liquidate_preserves_I",
   "liquidate_respects_lock",
   "locked_blocks_concrete_liquidation",

From 2e53a639fa33366ab4684bc510418b26f31f6fba Mon Sep 17 00:00:00 2001
From: "github-actions[bot]" <github-actions[bot]@users.noreply.github.com>
Date: Mon, 7 Sep 2026 11:42:37 +0200
Subject: [PATCH 12/27] chore: auto-refresh derived artifacts

---
 artifacts/verification_status.json | 12 ++++++------
 1 file changed, 6 insertions(+), 6 deletions(-)

diff --git a/artifacts/verification_status.json b/artifacts/verification_status.json
index 401522c405..3ed6aeae48 100644
--- a/artifacts/verification_status.json
+++ b/artifacts/verification_status.json
@@ -16,10 +16,10 @@
   },
   "theorems": {
     "categories": 15,
-    "coverage_percent": 77,
+    "coverage_percent": 78,
     "covered": 255,
-    "excluded": 75,
-    "non_stdlib_total": 330,
+    "excluded": 74,
+    "non_stdlib_total": 329,
     "per_contract": {
       "Counter": 31,
       "ERC20": 22,
@@ -31,15 +31,15 @@
       "OwnedCounter": 63,
       "OwnedCounterComposed": 6,
       "ReentrancyExample": 5,
-      "ReentrancyRelyGuarantee": 11,
+      "ReentrancyRelyGuarantee": 10,
       "SafeCounter": 25,
       "SimpleStorage": 20,
       "SimpleToken": 61,
       "Vault": 9
     },
-    "proven": 330,
+    "proven": 329,
     "stdlib": 0,
-    "total": 330
+    "total": 329
   },
   "toolchain": {
     "lean": "leanprover/lean4:v4.31.0",

From d946bdf1451e2520adb2e91aa920ccdca5617e4d Mon Sep 17 00:00:00 2001
From: Thomas Marchand <thomas@lfglabs.dev>
Date: Mon, 7 Sep 2026 13:00:47 +0200
Subject: [PATCH 13/27] fix(reentrancy): align guarded registry semantics

---
 Compiler/CompilationModel/Dispatch.lean       |  4 +--
 .../IRGeneration/NonReentrantGuardIR.lean     | 26 +++++++--------
 Verity/Macro/Translate.lean                   | 32 +++++++++++++++++--
 docs-site/public/llms.txt                     |  2 +-
 docs/VERIFICATION_STATUS.md                   | 14 ++++----
 5 files changed, 51 insertions(+), 27 deletions(-)

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/Verity/Macro/Translate.lean b/Verity/Macro/Translate.lean
index c8808d8023..5d9bb4299d 100644
--- a/Verity/Macro/Translate.lean
+++ b/Verity/Macro/Translate.lean
@@ -2402,7 +2402,13 @@ private def threadHelperApp?
       (toString name.getId).endsWith ("." ++ fn.name)) &&
       fn.params.size == args.size
   match helper? with
-  | some _ => some <$> helperCallWithAdv name args adv
+  | some helper =>
+      let target ←
+        if helper.nonReentrantLock.isSome && helper.reentrancyTrusted then
+          mkSuffixedIdent name "_unguarded"
+        else
+          pure name
+      some <$> helperCallWithAdv target args adv
   | none => pure none
 
 private def rewriteTypedInterfaceCall?
@@ -5044,6 +5050,7 @@ def validateGeneratedDefNamesPublic
 
     let helperNames :=
       #[ s!"{generatedFnName}_modelBody"
+       , s!"{generatedFnName}_entrypoint"
        , s!"{generatedFnName}_model"
        , s!"{generatedFnName}_bridge"
        , s!"{generatedFnName}_semantic_preservation"
@@ -5059,6 +5066,11 @@ def validateGeneratedDefNamesPublic
        , s!"{generatedFnName}_requires_role"
        , s!"{generatedFnName}_access_control"
        ]
+    let helperNames :=
+      if fn.nonReentrantLock.isSome && fn.reentrancyTrusted then
+        helperNames.push s!"{generatedFnName}_unguarded"
+      else
+        helperNames
     for helperName in helperNames do
       if storageNames.contains helperName then
         throwErrorAt fn.ident
@@ -5423,6 +5435,13 @@ 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))
+            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))
         for modDecl in mixin.modifiers do
           unless modifierContainsExternalCallSyntaxPublic modDecl do
             let tgt := mkIdent (mixinName ++ modDecl.ident.getId)
@@ -5542,6 +5561,15 @@ def mkFunctionCommandsPublic
       mkContractFnType fn.params fn.returnTy
   let fnExecutableBody := ⟨← threadAdversaryThroughExecutableSyntax externalDecls
     adversarialHelpers fn.params advTerm 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 fnExecutableBody
+      else
+        mkContractFnValue fn.params fnExecutableBody
+    extraExecutableCmds := extraExecutableCmds.push
+      (← `(command| def $unguardedId : $fnType := $unguardedValue))
   let fnExecutableBody ← match fn.nonReentrantLock with
     | some lockIdent =>
         let lockName := toString lockIdent.getId
@@ -5628,7 +5656,7 @@ def mkFunctionCommandsPublic
     body := $modelBodyName
     isInternal := $internalTerm
   })
-  pure #[fnCmd, entrypointCmd, 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
diff --git a/docs-site/public/llms.txt b/docs-site/public/llms.txt
index 6cb26e71ad..5aef189f7a 100644
--- a/docs-site/public/llms.txt
+++ b/docs-site/public/llms.txt
@@ -33,7 +33,7 @@ Every transition inside the proof envelope is either fully verified or recorded
 - **Language**: Lean 4.31.0
 - **Core Size**: 2040 lines
 - **Verified Contracts**: 15 (Counter, ERC20, ERC721, Ledger, LocalObligationMacroSmoke, Ownable, Owned, OwnedCounter, OwnedCounterComposed, ReentrancyExample, ReentrancyRelyGuarantee, SafeCounter, SimpleStorage, SimpleToken, Vault)
-- **Theorems**: 330 across 15 categories, 330 fully proven
+- **Theorems**: 329 across 15 categories, 329 fully proven
 - **Axioms**: 1 documented Lean axioms (see AXIOMS.md)
 - **Tests**: 528 Foundry tests, 239 property tests
 - **Build**: `lake build` verifies all proofs
diff --git a/docs/VERIFICATION_STATUS.md b/docs/VERIFICATION_STATUS.md
index 87a3166381..08f4684387 100644
--- a/docs/VERIFICATION_STATUS.md
+++ b/docs/VERIFICATION_STATUS.md
@@ -40,11 +40,11 @@ EVM Bytecode
 | ERC721 | 11 | Baseline | `Contracts/ERC721/Proofs/` |
 | Vault | 9 | Baseline | `Contracts/Vault/Proofs/` |
 | ReentrancyExample | 5 | Complete | `Contracts/ReentrancyExample/Contract.lean` |
-| ReentrancyRelyGuarantee | 11 | Semantic | `Contracts/ReentrancyRelyGuarantee/Contract.lean` |
+| ReentrancyRelyGuarantee | 10 | Semantic | `Contracts/ReentrancyRelyGuarantee/Contract.lean` |
 | CryptoHash | 0 | No specs | `Contracts/CryptoHash/Contract.lean` |
-| **Total** | **330** | **✅ 100%** | — |
+| **Total** | **329** | **✅ 100%** | — |
 
-> **Note**: Stdlib (0 internal proof-automation properties) is excluded from the contract-spec theorem table above but included in overall coverage statistics (330 total properties).
+> **Note**: Stdlib (0 internal proof-automation properties) is excluded from the contract-spec theorem table above but included in overall coverage statistics (329 total properties).
 
 Layer 1 uses macro-generated EDSL-to-`CompilationModel` bridge theorems backed by a generic typed-IR compilation-correctness theorem ([`TypedIRCompilerCorrectness.lean`](../Compiler/TypedIRCompilerCorrectness.lean)). Tuple/bytes/fixed-array/dynamic-array/string parameters now stay inside that proof path when they are carried as ABI head words/offsets. Advanced constructs beyond that typed-IR head-word surface (linked libraries, ECMs, fully custom ABI behavior) are still expressed directly in `CompilationModel` and trusted at that boundary. Higher-order internal helpers (function-pointer parameters, [#1747](https://github.com/lfglabs-dev/verity/issues/1747)) are eliminated by a compile-time monomorphization pre-pass that runs before any lowering, so the `CompilationModel` only ever contains first-order helpers: these calls are covered by the existing first-order proof path and introduce no new boundary trust.
 
@@ -205,7 +205,7 @@ Also note that the macro-generated `*_semantic_preservation` theorems are not co
 | ERC721 | 100% (11/11) | 0 |
 | SafeCounter | 100% (25/25) | 0 |
 | ReentrancyExample | 100% (5/5) | 0 |
-| ReentrancyRelyGuarantee | 0% (0/11) | 11 proof-only |
+| ReentrancyRelyGuarantee | 0% (0/10) | 10 proof-only |
 | Ledger | 100% (33/33) | 0 |
 | LocalObligationMacroSmoke | 100% (4/4) | 0 |
 | SimpleStorage | 95% (19/20) | 1 proof-only |
@@ -217,11 +217,11 @@ Also note that the macro-generated `*_semantic_preservation` theorems are not co
 | Counter | 74% (23/31) | 8 proof-only |
 | Stdlib | 0% (0/0) | 0 proof-only |
 
-**Status**: 77% coverage (255/330), 75 remaining exclusions all proof-only
+**Status**: 78% coverage (255/329), 74 remaining exclusions all proof-only
 
-- **Total Properties**: 330
+- **Total Properties**: 329
 - **Covered**: 255
-- **Excluded**: 75 (all proof-only)
+- **Excluded**: 74 (all proof-only)
 
 **Proof-Only Properties (59 exclusions)**: Internal proof machinery that cannot be tested in Foundry.
 

From d7cd60058b08874f179b2eaca8aeaa13368e8072 Mon Sep 17 00:00:00 2001
From: Thomas Marchand <thomas@lfglabs.dev>
Date: Mon, 7 Sep 2026 15:26:35 +0200
Subject: [PATCH 14/27] fix(proofs): open callback bridge namespace

---
 Verity/Proofs/Model/GeneratedEntrypointRegistry.lean | 2 ++
 1 file changed, 2 insertions(+)

diff --git a/Verity/Proofs/Model/GeneratedEntrypointRegistry.lean b/Verity/Proofs/Model/GeneratedEntrypointRegistry.lean
index 709ee00208..29df6ddaf1 100644
--- a/Verity/Proofs/Model/GeneratedEntrypointRegistry.lean
+++ b/Verity/Proofs/Model/GeneratedEntrypointRegistry.lean
@@ -46,6 +46,8 @@ theorem guardedPing_reentry_blocked (adv : AdversaryModel) (value : Uint256)
 
 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. -/

From f036c9b3dd1016c1bd547224ae1bd98c53980212 Mon Sep 17 00:00:00 2001
From: Thomas Marchand <thomas@lfglabs.dev>
Date: Mon, 7 Sep 2026 16:54:30 +0200
Subject: [PATCH 15/27] fix(reentrancy): close helper routing gaps

---
 Verity/Macro/Elaborate.lean |  3 ++-
 Verity/Macro/Translate.lean | 49 ++++++++++++++++++++++++++++---------
 2 files changed, 39 insertions(+), 13 deletions(-)

diff --git a/Verity/Macro/Elaborate.lean b/Verity/Macro/Elaborate.lean
index 723755bd4e..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
diff --git a/Verity/Macro/Translate.lean b/Verity/Macro/Translate.lean
index 5d9bb4299d..72fbb8d291 100644
--- a/Verity/Macro/Translate.lean
+++ b/Verity/Macro/Translate.lean
@@ -2394,13 +2394,21 @@ 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)
+    (helpers : Array FunctionDecl) (adversarialHelpers : Array FunctionDecl)
+    (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 helper? := helpers.find? matchesHelper
   match helper? with
   | some helper =>
       let target ←
@@ -2408,7 +2416,12 @@ private def threadHelperApp?
           mkSuffixedIdent name "_unguarded"
         else
           pure name
-      some <$> helperCallWithAdv target args adv
+      if adversarialHelpers.any matchesHelper 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?
@@ -2723,10 +2736,11 @@ private def adaptHoistedWordContext (stx : Term) : CommandElabM Term := do
 
 private partial def threadAdversaryThroughExecutableSyntax
     (externalDecls : Array ExternalDecl)
+    (helpers : Array FunctionDecl)
     (adversarialHelpers : Array FunctionDecl)
     (params : Array ParamDecl)
     (adv : Term) (stx : Syntax) : CommandElabM Syntax := do
-  let go := threadAdversaryThroughExecutableSyntax externalDecls adversarialHelpers params adv
+  let go := threadAdversaryThroughExecutableSyntax externalDecls helpers adversarialHelpers params adv
   let recurseChildren : CommandElabM Syntax := do
     match stx with
     | .node info kind args =>
@@ -2762,7 +2776,7 @@ 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
+        match ← threadHelperApp? helpers adversarialHelpers name args adv with
         | some app => pure (#[], app)
         | none =>
             let mut binds : Array (Ident × Term) := #[]
@@ -2899,7 +2913,7 @@ 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? helpers adversarialHelpers fn args adv with
       | some app => `(doElem| let $name ← $app:term)
       | none => recurseChildren
   | `(doElem| let $name:ident ← $fn:ident $args:term*) =>
@@ -2924,7 +2938,7 @@ private partial def threadAdversaryThroughExecutableSyntax
         wrapBinds binds
           (← `(doElem| let $name ← (totalSupply (externalArgAddress $token) $adv)))
       else
-        match ← threadHelperApp? adversarialHelpers fn original adv with
+        match ← threadHelperApp? helpers adversarialHelpers fn original adv with
         | some app =>
             hoistLive false app fun rewritten => `(doElem| let $name ← $rewritten:term)
         | none =>
@@ -3051,7 +3065,7 @@ private partial def threadAdversaryThroughExecutableSyntax
             let rewritten ← rewriteLinkedCallTerm externalDecls params adv rhs
             `(doElem| $rewritten:term)
         | _ => recurseChildren
-      else match ← threadHelperApp? adversarialHelpers fn original adv with
+      else match ← threadHelperApp? helpers adversarialHelpers fn original adv with
       | some app =>
           hoistLive false app fun rewritten => `(doElem| $rewritten:term)
       | none =>
@@ -3063,7 +3077,7 @@ private partial def threadAdversaryThroughExecutableSyntax
       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? helpers adversarialHelpers name original adv with
       | some app => pure app.raw
       | none =>
           if isLiveStateExternalCall ⟨stx⟩ then
@@ -4962,9 +4976,11 @@ 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", "entrypointRegistry"]
   let mut generatedHelperNames : Array String := reservedGeneratedNames
@@ -5089,6 +5105,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)
@@ -5338,7 +5363,7 @@ def mkConstructorDefCommandPublic
       pure ⟨advIdent.raw⟩
     else
       `(Compiler.CompilationModel.DenoteExternalCalls.AdversaryModel.stub)
-  let executableBody := ⟨← threadAdversaryThroughExecutableSyntax externalDecls adversarialHelpers
+  let executableBody := ⟨← threadAdversaryThroughExecutableSyntax externalDecls functions adversarialHelpers
     ctor.params advTerm executableBody.raw⟩
   let fnType ← if opensReentrancyWindow then
       mkContractFnTypeWithAdversary ctor.params .unit
@@ -5408,7 +5433,7 @@ 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
+      let executableBody := ⟨← threadAdversaryThroughExecutableSyntax externalDecls functions ownAdversarialHelpers
         ctor.params advTerm executableBody.raw⟩
       let fnValue ← if containsExternalCall then
           mkContractFnValueWithAdversary advIdent ctor.params executableBody
@@ -5559,7 +5584,7 @@ def mkFunctionCommandsPublic
       mkContractFnTypeWithAdversary fn.params fn.returnTy
     else
       mkContractFnType fn.params fn.returnTy
-  let fnExecutableBody := ⟨← threadAdversaryThroughExecutableSyntax externalDecls
+  let fnExecutableBody := ⟨← threadAdversaryThroughExecutableSyntax externalDecls functions
     adversarialHelpers fn.params advTerm fnExecutableBody.raw⟩
   let mut extraExecutableCmds : Array Cmd := #[]
   if fn.nonReentrantLock.isSome && fn.reentrancyTrusted then

From bb856e42a3ff92ad4209524d7616e74a931b6288 Mon Sep 17 00:00:00 2001
From: Thomas Marchand <thomas@lfglabs.dev>
Date: Mon, 7 Sep 2026 18:49:50 +0200
Subject: [PATCH 16/27] fix(macro): preserve qualified guarded helper calls

---
 Contracts/Smoke/SecurityCombos.lean | 32 +++++++++++++++++++++++++++++
 Verity/Macro/Translate.lean         |  6 +++++-
 2 files changed, 37 insertions(+), 1 deletion(-)

diff --git a/Contracts/Smoke/SecurityCombos.lean b/Contracts/Smoke/SecurityCombos.lean
index bd42e62e68..2ae3b2d58f 100644
--- a/Contracts/Smoke/SecurityCombos.lean
+++ b/Contracts/Smoke/SecurityCombos.lean
@@ -175,6 +175,38 @@ 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)
+
+verity_contract NonreentrantQualifiedHelperResolution where
+  storage
+    lock : Uint256 := slot 0
+
+  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 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)
+
+#check_contract NonreentrantQualifiedHelperResolution
+
 -- ════════════════════════════════════════════════════════════════════════════
 -- Stress-test contracts: edge-case coverage for Language Design Axes (#1731)
 -- ════════════════════════════════════════════════════════════════════════════
diff --git a/Verity/Macro/Translate.lean b/Verity/Macro/Translate.lean
index 72fbb8d291..47761c94a8 100644
--- a/Verity/Macro/Translate.lean
+++ b/Verity/Macro/Translate.lean
@@ -2408,11 +2408,15 @@ private def threadHelperApp?
     (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 helper? := helpers.find? matchesHelper
   match helper? with
   | some helper =>
       let target ←
-        if helper.nonReentrantLock.isSome && helper.reentrancyTrusted then
+        if helper.nonReentrantLock.isSome && helper.reentrancyTrusted &&
+            matchesExactHelper helper then
           mkSuffixedIdent name "_unguarded"
         else
           pure name

From 8ec2b67b2b5e2af5fe0e7cc83950b9bff7786b5e Mon Sep 17 00:00:00 2001
From: Thomas Marchand <thomas@lfglabs.dev>
Date: Mon, 7 Sep 2026 19:53:51 +0200
Subject: [PATCH 17/27] test(macro): add qualified helper artifacts

---
 ...onreentrantQualifiedHelperResolution.t.sol | 57 +++++++++++++++++++
 .../PropertyQualifiedHelperLibrary.t.sol      | 39 +++++++++++++
 2 files changed, 96 insertions(+)
 create mode 100644 artifacts/macro_property_tests/PropertyNonreentrantQualifiedHelperResolution.t.sol
 create mode 100644 artifacts/macro_property_tests/PropertyQualifiedHelperLibrary.t.sol

diff --git a/artifacts/macro_property_tests/PropertyNonreentrantQualifiedHelperResolution.t.sol b/artifacts/macro_property_tests/PropertyNonreentrantQualifiedHelperResolution.t.sol
new file mode 100644
index 0000000000..655341526e
--- /dev/null
+++ b/artifacts/macro_property_tests/PropertyNonreentrantQualifiedHelperResolution.t.sol
@@ -0,0 +1,57 @@
+// 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 `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 4: 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;
+    }
+}
diff --git a/artifacts/macro_property_tests/PropertyQualifiedHelperLibrary.t.sol b/artifacts/macro_property_tests/PropertyQualifiedHelperLibrary.t.sol
new file mode 100644
index 0000000000..ddd9e72e63
--- /dev/null
+++ b/artifacts/macro_property_tests/PropertyQualifiedHelperLibrary.t.sol
@@ -0,0 +1,39 @@
+// 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");
+    }
+}

From 89703cc3053c837eb0f38ec73b553c7379a905f5 Mon Sep 17 00:00:00 2001
From: Thomas Marchand <thomas@lfglabs.dev>
Date: Mon, 7 Sep 2026 21:38:34 +0200
Subject: [PATCH 18/27] fix(macro): keep adversary threading namespace-local

---
 Contracts/Smoke/SecurityCombos.lean           | 25 ++++++++++++
 Verity/Macro/Translate.lean                   |  2 +-
 ...onreentrantQualifiedHelperResolution.t.sol | 40 ++++++++++++++++++-
 .../PropertyQualifiedHelperLibrary.t.sol      | 19 +++++++++
 4 files changed, 83 insertions(+), 3 deletions(-)

diff --git a/Contracts/Smoke/SecurityCombos.lean b/Contracts/Smoke/SecurityCombos.lean
index 2ae3b2d58f..dab2a49251 100644
--- a/Contracts/Smoke/SecurityCombos.lean
+++ b/Contracts/Smoke/SecurityCombos.lean
@@ -187,16 +187,33 @@ verity_contract QualifiedHelperLibrary where
   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
 
+  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 qualifiedSpace (x : Uint256) : Uint256 := do
     let y ← QualifiedHelperLibrary.trustedEntry x
     return y
@@ -205,6 +222,14 @@ verity_contract NonreentrantQualifiedHelperResolution where
     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)
+
 #check_contract NonreentrantQualifiedHelperResolution
 
 -- ════════════════════════════════════════════════════════════════════════════
diff --git a/Verity/Macro/Translate.lean b/Verity/Macro/Translate.lean
index 47761c94a8..63863f3b82 100644
--- a/Verity/Macro/Translate.lean
+++ b/Verity/Macro/Translate.lean
@@ -2420,7 +2420,7 @@ private def threadHelperApp?
           mkSuffixedIdent name "_unguarded"
         else
           pure name
-      if adversarialHelpers.any matchesHelper then
+      if adversarialHelpers.any matchesExactHelper then
         some <$> helperCallWithAdv target args adv
       else if helper.nonReentrantLock.isSome && helper.reentrancyTrusted then
         some <$> helperCall target args
diff --git a/artifacts/macro_property_tests/PropertyNonreentrantQualifiedHelperResolution.t.sol b/artifacts/macro_property_tests/PropertyNonreentrantQualifiedHelperResolution.t.sol
index 655341526e..a4e1791d86 100644
--- a/artifacts/macro_property_tests/PropertyNonreentrantQualifiedHelperResolution.t.sol
+++ b/artifacts/macro_property_tests/PropertyNonreentrantQualifiedHelperResolution.t.sol
@@ -36,7 +36,25 @@ contract PropertyNonreentrantQualifiedHelperResolutionTest is YulTestBase {
         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 `qualifiedSpace` 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: 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)));
@@ -45,7 +63,7 @@ contract PropertyNonreentrantQualifiedHelperResolutionTest is YulTestBase {
         // TODO(#1011): decode `ret` and assert the concrete postcondition from Lean theorem.
         ret;
     }
-    // Property 4: TODO decode and assert `qualifiedDestructure` result
+    // Property 6: 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)));
@@ -54,4 +72,22 @@ contract PropertyNonreentrantQualifiedHelperResolutionTest is YulTestBase {
         // TODO(#1011): decode `ret` and assert the concrete postcondition from Lean theorem.
         ret;
     }
+    // Property 7: 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 8: 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;
+    }
 }
diff --git a/artifacts/macro_property_tests/PropertyQualifiedHelperLibrary.t.sol b/artifacts/macro_property_tests/PropertyQualifiedHelperLibrary.t.sol
index ddd9e72e63..b4ae08718c 100644
--- a/artifacts/macro_property_tests/PropertyQualifiedHelperLibrary.t.sol
+++ b/artifacts/macro_property_tests/PropertyQualifiedHelperLibrary.t.sol
@@ -36,4 +36,23 @@ contract PropertyQualifiedHelperLibraryTest is YulTestBase {
         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");
+    }
 }

From 3f6dbc78eb83f594b642d94d0f4ff0243654e786 Mon Sep 17 00:00:00 2001
From: Thomas Marchand <thomas@lfglabs.dev>
Date: Mon, 7 Sep 2026 23:23:19 +0200
Subject: [PATCH 19/27] fix(macro): resolve guarded helper overloads

---
 Contracts/Smoke/SecurityCombos.lean           | 21 ++++++
 Verity/Macro/Translate.lean                   | 71 +++++++++++++------
 ...onreentrantQualifiedHelperResolution.t.sol | 56 +++++++++++++--
 3 files changed, 122 insertions(+), 26 deletions(-)

diff --git a/Contracts/Smoke/SecurityCombos.lean b/Contracts/Smoke/SecurityCombos.lean
index dab2a49251..d35b0e0c3b 100644
--- a/Contracts/Smoke/SecurityCombos.lean
+++ b/Contracts/Smoke/SecurityCombos.lean
@@ -214,6 +214,19 @@ verity_contract NonreentrantQualifiedHelperResolution where
     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 qualifiedSpace (x : Uint256) : Uint256 := do
     let y ← QualifiedHelperLibrary.trustedEntry x
     return y
@@ -230,6 +243,14 @@ verity_contract NonreentrantQualifiedHelperResolution where
     let (left, right) ← QualifiedHelperLibrary.adversarialPair x
     return (add left right)
 
+  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"
+
 #check_contract NonreentrantQualifiedHelperResolution
 
 -- ════════════════════════════════════════════════════════════════════════════
diff --git a/Verity/Macro/Translate.lean b/Verity/Macro/Translate.lean
index 63863f3b82..37af4e28de 100644
--- a/Verity/Macro/Translate.lean
+++ b/Verity/Macro/Translate.lean
@@ -2401,7 +2401,11 @@ private def helperCall (name : Ident) (args : Array Term) : CommandElabM Term :=
   pure app
 
 private def threadHelperApp?
+    (fields : Array StorageFieldDecl)
+    (constDecls : Array ConstantDecl) (immutableDecls : Array ImmutableDecl)
+    (externalDecls : Array ExternalDecl)
     (helpers : Array FunctionDecl) (adversarialHelpers : Array FunctionDecl)
+    (params : Array ParamDecl)
     (name : Ident) (args : Array Term)
     (adv : Term) : CommandElabM (Option Term) := do
   let matchesHelper := fun (fn : FunctionDecl) =>
@@ -2411,16 +2415,30 @@ private def threadHelperApp?
   let matchesExactHelper := fun (fn : FunctionDecl) =>
     (fn.name == toString name.getId || fn.ident.getId == name.getId) &&
       fn.params.size == args.size
-  let helper? := helpers.find? matchesHelper
+  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 #[] 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 helper =>
       let target ←
         if helper.nonReentrantLock.isSome && helper.reentrancyTrusted &&
             matchesExactHelper helper then
-          mkSuffixedIdent name "_unguarded"
+          mkSuffixedIdent helper.ident "_unguarded"
         else
           pure name
-      if adversarialHelpers.any matchesExactHelper then
+      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
@@ -2739,12 +2757,15 @@ 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)
     (params : Array ParamDecl)
     (adv : Term) (stx : Syntax) : CommandElabM Syntax := do
-  let go := threadAdversaryThroughExecutableSyntax externalDecls helpers adversarialHelpers params adv
+  let go := threadAdversaryThroughExecutableSyntax fields constDecls immutableDecls
+    externalDecls helpers adversarialHelpers params adv
   let recurseChildren : CommandElabM Syntax := do
     match stx with
     | .node info kind args =>
@@ -2780,7 +2801,8 @@ private partial def threadAdversaryThroughExecutableSyntax
         let rewrittenBody : TSyntax ``Lean.Parser.Term.doSeq := ⟨bodyRaw⟩
         pure (#[], ← `(term| do $rewrittenBody))
     | `(term| $name:ident($[$args:term],*)) =>
-        match ← threadHelperApp? helpers adversarialHelpers name args adv with
+        match ← threadHelperApp? fields constDecls immutableDecls externalDecls
+            helpers adversarialHelpers params name args adv with
         | some app => pure (#[], app)
         | none =>
             let mut binds : Array (Ident × Term) := #[]
@@ -2917,7 +2939,8 @@ private partial def threadAdversaryThroughExecutableSyntax
         (← `(doElem| let $pat:term ← (totalSupply
           (externalArgAddress $rewrittenToken) $adv)))
   | `(doElem| let $name:ident ← $fn:ident($[$args:term],*)) =>
-      match ← threadHelperApp? helpers adversarialHelpers fn args adv with
+      match ← threadHelperApp? fields constDecls immutableDecls externalDecls
+          helpers adversarialHelpers params fn args adv with
       | some app => `(doElem| let $name ← $app:term)
       | none => recurseChildren
   | `(doElem| let $name:ident ← $fn:ident $args:term*) =>
@@ -2942,7 +2965,8 @@ private partial def threadAdversaryThroughExecutableSyntax
         wrapBinds binds
           (← `(doElem| let $name ← (totalSupply (externalArgAddress $token) $adv)))
       else
-        match ← threadHelperApp? helpers adversarialHelpers fn original adv with
+        match ← threadHelperApp? fields constDecls immutableDecls externalDecls
+            helpers adversarialHelpers params fn original adv with
         | some app =>
             hoistLive false app fun rewritten => `(doElem| let $name ← $rewritten:term)
         | none =>
@@ -3069,19 +3093,22 @@ private partial def threadAdversaryThroughExecutableSyntax
             let rewritten ← rewriteLinkedCallTerm externalDecls params adv rhs
             `(doElem| $rewritten:term)
         | _ => recurseChildren
-      else match ← threadHelperApp? helpers 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 params 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? helpers adversarialHelpers name original adv with
+      match ← threadHelperApp? fields constDecls immutableDecls externalDecls
+          helpers adversarialHelpers params name original adv with
       | some app => pure app.raw
       | none =>
           if isLiveStateExternalCall ⟨stx⟩ then
@@ -5367,8 +5394,8 @@ def mkConstructorDefCommandPublic
       pure ⟨advIdent.raw⟩
     else
       `(Compiler.CompilationModel.DenoteExternalCalls.AdversaryModel.stub)
-  let executableBody := ⟨← threadAdversaryThroughExecutableSyntax externalDecls functions 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
@@ -5437,8 +5464,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 functions 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
@@ -5588,8 +5615,8 @@ def mkFunctionCommandsPublic
       mkContractFnTypeWithAdversary fn.params fn.returnTy
     else
       mkContractFnType fn.params fn.returnTy
-  let fnExecutableBody := ⟨← threadAdversaryThroughExecutableSyntax externalDecls functions
-    adversarialHelpers fn.params advTerm fnExecutableBody.raw⟩
+  let fnExecutableBody := ⟨← threadAdversaryThroughExecutableSyntax fields constDecls immutableDecls
+    externalDecls functions adversarialHelpers fn.params advTerm fnExecutableBody.raw⟩
   let mut extraExecutableCmds : Array Cmd := #[]
   if fn.nonReentrantLock.isSome && fn.reentrancyTrusted then
     let unguardedId ← mkSuffixedIdent fn.ident "_unguarded"
diff --git a/artifacts/macro_property_tests/PropertyNonreentrantQualifiedHelperResolution.t.sol b/artifacts/macro_property_tests/PropertyNonreentrantQualifiedHelperResolution.t.sol
index a4e1791d86..e9ced0f2e4 100644
--- a/artifacts/macro_property_tests/PropertyNonreentrantQualifiedHelperResolution.t.sol
+++ b/artifacts/macro_property_tests/PropertyNonreentrantQualifiedHelperResolution.t.sol
@@ -54,7 +54,43 @@ contract PropertyNonreentrantQualifiedHelperResolutionTest is YulTestBase {
         // TODO(#1011): decode `ret` and assert the concrete postcondition from Lean theorem.
         ret;
     }
-    // Property 5: TODO decode and assert `qualifiedSpace` result
+    // 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: 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)));
@@ -63,7 +99,7 @@ contract PropertyNonreentrantQualifiedHelperResolutionTest is YulTestBase {
         // TODO(#1011): decode `ret` and assert the concrete postcondition from Lean theorem.
         ret;
     }
-    // Property 6: TODO decode and assert `qualifiedDestructure` result
+    // Property 10: 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)));
@@ -72,7 +108,7 @@ contract PropertyNonreentrantQualifiedHelperResolutionTest is YulTestBase {
         // TODO(#1011): decode `ret` and assert the concrete postcondition from Lean theorem.
         ret;
     }
-    // Property 7: TODO decode and assert `qualifiedAdversarialSpace` result
+    // Property 11: 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)));
@@ -81,7 +117,7 @@ contract PropertyNonreentrantQualifiedHelperResolutionTest is YulTestBase {
         // TODO(#1011): decode `ret` and assert the concrete postcondition from Lean theorem.
         ret;
     }
-    // Property 8: TODO decode and assert `qualifiedAdversarialDestructure` result
+    // Property 12: 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)));
@@ -90,4 +126,16 @@ contract PropertyNonreentrantQualifiedHelperResolutionTest is YulTestBase {
         // TODO(#1011): decode `ret` and assert the concrete postcondition from Lean theorem.
         ret;
     }
+    // Property 13: 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 14: 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");
+    }
 }

From e55fba5f8a42935818130037ae4d9eed39014ce0 Mon Sep 17 00:00:00 2001
From: Thomas Marchand <thomas@lfglabs.dev>
Date: Tue, 8 Sep 2026 01:33:20 +0200
Subject: [PATCH 20/27] fix(macro): resolve helper calls through typed locals

---
 Contracts/Smoke/SecurityCombos.lean           | 11 ++++
 Verity/Macro/Translate.lean                   | 52 +++++++++++++++----
 ...onreentrantQualifiedHelperResolution.t.sol | 12 +++++
 3 files changed, 64 insertions(+), 11 deletions(-)

diff --git a/Contracts/Smoke/SecurityCombos.lean b/Contracts/Smoke/SecurityCombos.lean
index d35b0e0c3b..f6be31170f 100644
--- a/Contracts/Smoke/SecurityCombos.lean
+++ b/Contracts/Smoke/SecurityCombos.lean
@@ -196,6 +196,7 @@ verity_contract QualifiedHelperLibrary where
 verity_contract NonreentrantQualifiedHelperResolution where
   storage
     lock : Uint256 := slot 0
+    value : Uint256 := slot 1
 
   linked_externals
     external echo(Uint256) -> (Uint256)
@@ -251,6 +252,16 @@ verity_contract NonreentrantQualifiedHelperResolution where
     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"
+
 #check_contract NonreentrantQualifiedHelperResolution
 
 -- ════════════════════════════════════════════════════════════════════════════
diff --git a/Verity/Macro/Translate.lean b/Verity/Macro/Translate.lean
index 37af4e28de..f9103f2a50 100644
--- a/Verity/Macro/Translate.lean
+++ b/Verity/Macro/Translate.lean
@@ -2405,7 +2405,7 @@ private def threadHelperApp?
     (constDecls : Array ConstantDecl) (immutableDecls : Array ImmutableDecl)
     (externalDecls : Array ExternalDecl)
     (helpers : Array FunctionDecl) (adversarialHelpers : Array FunctionDecl)
-    (params : Array ParamDecl)
+    (params : Array ParamDecl) (locals : Array TypedLocal)
     (name : Ident) (args : Array Term)
     (adv : Term) : CommandElabM (Option Term) := do
   let matchesHelper := fun (fn : FunctionDecl) =>
@@ -2423,7 +2423,7 @@ private def threadHelperApp?
       let app ← helperCall name args
       try
         pure ((← resolveLocalFunctionApp? fields constDecls immutableDecls externalDecls
-          helpers params #[] app).map (·.1))
+          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
@@ -2763,9 +2763,10 @@ private partial def threadAdversaryThroughExecutableSyntax
     (helpers : Array FunctionDecl)
     (adversarialHelpers : Array FunctionDecl)
     (params : Array ParamDecl)
+    (locals : Array TypedLocal)
     (adv : Term) (stx : Syntax) : CommandElabM Syntax := do
   let go := threadAdversaryThroughExecutableSyntax fields constDecls immutableDecls
-    externalDecls helpers adversarialHelpers params adv
+    externalDecls helpers adversarialHelpers params locals adv
   let recurseChildren : CommandElabM Syntax := do
     match stx with
     | .node info kind args =>
@@ -2776,6 +2777,26 @@ 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
+    match elem with
+    | `(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) :
@@ -2802,7 +2823,7 @@ private partial def threadAdversaryThroughExecutableSyntax
         pure (#[], ← `(term| do $rewrittenBody))
     | `(term| $name:ident($[$args:term],*)) =>
         match ← threadHelperApp? fields constDecls immutableDecls externalDecls
-            helpers adversarialHelpers params name args adv with
+            helpers adversarialHelpers params locals name args adv with
         | some app => pure (#[], app)
         | none =>
             let mut binds : Array (Ident × Term) := #[]
@@ -2889,6 +2910,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 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 := #[]
@@ -2940,7 +2970,7 @@ private partial def threadAdversaryThroughExecutableSyntax
           (externalArgAddress $rewrittenToken) $adv)))
   | `(doElem| let $name:ident ← $fn:ident($[$args:term],*)) =>
       match ← threadHelperApp? fields constDecls immutableDecls externalDecls
-          helpers adversarialHelpers params fn args adv with
+          helpers adversarialHelpers params locals fn args adv with
       | some app => `(doElem| let $name ← $app:term)
       | none => recurseChildren
   | `(doElem| let $name:ident ← $fn:ident $args:term*) =>
@@ -2966,7 +2996,7 @@ private partial def threadAdversaryThroughExecutableSyntax
           (← `(doElem| let $name ← (totalSupply (externalArgAddress $token) $adv)))
       else
         match ← threadHelperApp? fields constDecls immutableDecls externalDecls
-            helpers adversarialHelpers params fn original adv with
+            helpers adversarialHelpers params locals fn original adv with
         | some app =>
             hoistLive false app fun rewritten => `(doElem| let $name ← $rewritten:term)
         | none =>
@@ -3095,7 +3125,7 @@ private partial def threadAdversaryThroughExecutableSyntax
         | _ => recurseChildren
       else
         match ← threadHelperApp? fields constDecls immutableDecls externalDecls
-            helpers adversarialHelpers params fn original adv with
+          helpers adversarialHelpers params locals fn original adv with
         | some app =>
             hoistLive false app fun rewritten => `(doElem| $rewritten:term)
         | none =>
@@ -3108,7 +3138,7 @@ private partial def threadAdversaryThroughExecutableSyntax
   | `(term| $name:ident $args:term*) =>
       let original := args.map fun arg => (⟨arg.raw⟩ : Term)
       match ← threadHelperApp? fields constDecls immutableDecls externalDecls
-          helpers adversarialHelpers params name original adv with
+          helpers adversarialHelpers params locals name original adv with
       | some app => pure app.raw
       | none =>
           if isLiveStateExternalCall ⟨stx⟩ then
@@ -5395,7 +5425,7 @@ def mkConstructorDefCommandPublic
     else
       `(Compiler.CompilationModel.DenoteExternalCalls.AdversaryModel.stub)
   let executableBody := ⟨← threadAdversaryThroughExecutableSyntax fields constDecls immutableDecls
-    externalDecls functions adversarialHelpers ctor.params advTerm executableBody.raw⟩
+    externalDecls functions adversarialHelpers ctor.params #[] advTerm executableBody.raw⟩
   let fnType ← if opensReentrancyWindow then
       mkContractFnTypeWithAdversary ctor.params .unit
     else
@@ -5465,7 +5495,7 @@ def mkHostConstructorDefCommandPublic
       let body ← `(term| do $[$preludes:doElem]* $[$elems:doElem]*)
       let executableBody ← rewriteForEachExecutableBody fields externalDecls ctor.params body
       let executableBody := ⟨← threadAdversaryThroughExecutableSyntax fields constDecls immutableDecls
-        externalDecls functions ownAdversarialHelpers ctor.params advTerm executableBody.raw⟩
+        externalDecls functions ownAdversarialHelpers ctor.params #[] advTerm executableBody.raw⟩
       let fnValue ← if containsExternalCall then
           mkContractFnValueWithAdversary advIdent ctor.params executableBody
         else
@@ -5616,7 +5646,7 @@ def mkFunctionCommandsPublic
     else
       mkContractFnType fn.params fn.returnTy
   let fnExecutableBody := ⟨← threadAdversaryThroughExecutableSyntax fields constDecls immutableDecls
-    externalDecls functions adversarialHelpers fn.params advTerm fnExecutableBody.raw⟩
+    externalDecls functions adversarialHelpers fn.params #[] advTerm fnExecutableBody.raw⟩
   let mut extraExecutableCmds : Array Cmd := #[]
   if fn.nonReentrantLock.isSome && fn.reentrancyTrusted then
     let unguardedId ← mkSuffixedIdent fn.ident "_unguarded"
diff --git a/artifacts/macro_property_tests/PropertyNonreentrantQualifiedHelperResolution.t.sol b/artifacts/macro_property_tests/PropertyNonreentrantQualifiedHelperResolution.t.sol
index e9ced0f2e4..a6a3beee60 100644
--- a/artifacts/macro_property_tests/PropertyNonreentrantQualifiedHelperResolution.t.sol
+++ b/artifacts/macro_property_tests/PropertyNonreentrantQualifiedHelperResolution.t.sol
@@ -138,4 +138,16 @@ contract PropertyNonreentrantQualifiedHelperResolutionTest is YulTestBase {
         (bool ok,) = target.call(abi.encodeWithSignature("overloadedAdversarialCaller(uint256)", uint256(1)));
         require(ok, "overloadedAdversarialCaller reverted unexpectedly");
     }
+    // Property 15: 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 16: 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");
+    }
 }

From 22ee53c7bf7aca52e2ec1e009151a1895abd0db6 Mon Sep 17 00:00:00 2001
From: Thomas Marchand <thomas@lfglabs.dev>
Date: Tue, 8 Sep 2026 04:09:58 +0200
Subject: [PATCH 21/27] fix(macro): track tuple locals for helper overloads

---
 Contracts/Smoke/SecurityCombos.lean           | 13 +++++
 Verity/Macro/Translate.lean                   | 49 +++++++++++++++----
 ...onreentrantQualifiedHelperResolution.t.sol | 38 +++++++++++---
 3 files changed, 82 insertions(+), 18 deletions(-)

diff --git a/Contracts/Smoke/SecurityCombos.lean b/Contracts/Smoke/SecurityCombos.lean
index f6be31170f..2f2c95ace7 100644
--- a/Contracts/Smoke/SecurityCombos.lean
+++ b/Contracts/Smoke/SecurityCombos.lean
@@ -228,6 +228,9 @@ verity_contract NonreentrantQualifiedHelperResolution where
     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
@@ -262,6 +265,16 @@ verity_contract NonreentrantQualifiedHelperResolution where
     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"
+
 #check_contract NonreentrantQualifiedHelperResolution
 
 -- ════════════════════════════════════════════════════════════════════════════
diff --git a/Verity/Macro/Translate.lean b/Verity/Macro/Translate.lean
index f9103f2a50..5bc7c234d5 100644
--- a/Verity/Macro/Translate.lean
+++ b/Verity/Macro/Translate.lean
@@ -2787,16 +2787,45 @@ private partial def threadAdversaryThroughExecutableSyntax
           | none => inferPureExprType fields constDecls immutableDecls externalDecls params scope rhs
         pure (scope.push (mkTypedLocal (toString name.getId) ty))
       catch _ => pure scope
-    match elem with
-    | `(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 inferTuple (names : Array (Option String)) (rhs : Term) := do
+      try
+        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 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 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 := $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) :
diff --git a/artifacts/macro_property_tests/PropertyNonreentrantQualifiedHelperResolution.t.sol b/artifacts/macro_property_tests/PropertyNonreentrantQualifiedHelperResolution.t.sol
index a6a3beee60..d66bee46d6 100644
--- a/artifacts/macro_property_tests/PropertyNonreentrantQualifiedHelperResolution.t.sol
+++ b/artifacts/macro_property_tests/PropertyNonreentrantQualifiedHelperResolution.t.sol
@@ -90,7 +90,17 @@ contract PropertyNonreentrantQualifiedHelperResolutionTest is YulTestBase {
         // TODO(#1011): decode `ret` and assert the concrete postcondition from Lean theorem.
         ret;
     }
-    // Property 9: TODO decode and assert `qualifiedSpace` result
+    // 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)));
@@ -99,7 +109,7 @@ contract PropertyNonreentrantQualifiedHelperResolutionTest is YulTestBase {
         // TODO(#1011): decode `ret` and assert the concrete postcondition from Lean theorem.
         ret;
     }
-    // Property 10: TODO decode and assert `qualifiedDestructure` result
+    // 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)));
@@ -108,7 +118,7 @@ contract PropertyNonreentrantQualifiedHelperResolutionTest is YulTestBase {
         // TODO(#1011): decode `ret` and assert the concrete postcondition from Lean theorem.
         ret;
     }
-    // Property 11: TODO decode and assert `qualifiedAdversarialSpace` result
+    // 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)));
@@ -117,7 +127,7 @@ contract PropertyNonreentrantQualifiedHelperResolutionTest is YulTestBase {
         // TODO(#1011): decode `ret` and assert the concrete postcondition from Lean theorem.
         ret;
     }
-    // Property 12: TODO decode and assert `qualifiedAdversarialDestructure` result
+    // 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)));
@@ -126,28 +136,40 @@ contract PropertyNonreentrantQualifiedHelperResolutionTest is YulTestBase {
         // TODO(#1011): decode `ret` and assert the concrete postcondition from Lean theorem.
         ret;
     }
-    // Property 13: overloadedTrustedCaller has no unexpected revert
+    // Property 14: 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 14: overloadedAdversarialCaller has no unexpected revert
+    // Property 15: 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 15: overloadedTrustedLocalCaller has no unexpected revert
+    // Property 16: 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 16: overloadedAdversarialLocalCaller has no unexpected revert
+    // Property 17: 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 18: 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 19: 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");
+    }
 }

From aa806ce13fbf2f4b7c21b4a5d3d73325e5ebd420 Mon Sep 17 00:00:00 2001
From: Thomas Marchand <thomas@lfglabs.dev>
Date: Tue, 8 Sep 2026 07:22:29 +0200
Subject: [PATCH 22/27] fix(macro): recurse qualified calls and track loop
 locals

---
 Contracts/Smoke/SecurityCombos.lean           | 14 ++++++++
 Verity/Macro/Translate.lean                   |  7 ++++
 ...onreentrantQualifiedHelperResolution.t.sol | 33 +++++++++++++++----
 3 files changed, 48 insertions(+), 6 deletions(-)

diff --git a/Contracts/Smoke/SecurityCombos.lean b/Contracts/Smoke/SecurityCombos.lean
index 2f2c95ace7..c1c45dd686 100644
--- a/Contracts/Smoke/SecurityCombos.lean
+++ b/Contracts/Smoke/SecurityCombos.lean
@@ -247,6 +247,10 @@ verity_contract NonreentrantQualifiedHelperResolution where
     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 overloadedTrustedCaller (x : Uint256) : Unit := do
     let y ← overloadedTrusted x
     require (y == x) "wrong trusted overload"
@@ -275,6 +279,16 @@ verity_contract NonreentrantQualifiedHelperResolution where
     let y ← overloadedAdversarial right
     require (y == x) "wrong adversarial tuple-local overload"
 
+  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
 
 -- ════════════════════════════════════════════════════════════════════════════
diff --git a/Verity/Macro/Translate.lean b/Verity/Macro/Translate.lean
index 5bc7c234d5..7c2b6080b9 100644
--- a/Verity/Macro/Translate.lean
+++ b/Verity/Macro/Translate.lean
@@ -2431,6 +2431,11 @@ private def threadHelperApp?
         pure none
   match helper? with
   | 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 target ←
         if helper.nonReentrantLock.isSome && helper.reentrancyTrusted &&
             matchesExactHelper helper then
@@ -2817,6 +2822,8 @@ private partial def threadAdversaryThroughExecutableSyntax
     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) =>
diff --git a/artifacts/macro_property_tests/PropertyNonreentrantQualifiedHelperResolution.t.sol b/artifacts/macro_property_tests/PropertyNonreentrantQualifiedHelperResolution.t.sol
index d66bee46d6..94cd69b9d2 100644
--- a/artifacts/macro_property_tests/PropertyNonreentrantQualifiedHelperResolution.t.sol
+++ b/artifacts/macro_property_tests/PropertyNonreentrantQualifiedHelperResolution.t.sol
@@ -136,40 +136,61 @@ contract PropertyNonreentrantQualifiedHelperResolutionTest is YulTestBase {
         // TODO(#1011): decode `ret` and assert the concrete postcondition from Lean theorem.
         ret;
     }
-    // Property 14: overloadedTrustedCaller has no unexpected revert
+    // 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: 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 15: overloadedAdversarialCaller has no unexpected revert
+    // Property 16: 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 16: overloadedTrustedLocalCaller has no unexpected revert
+    // Property 17: 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 17: overloadedAdversarialLocalCaller has no unexpected revert
+    // Property 18: 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 18: overloadedTrustedTupleLocalCaller has no unexpected revert
+    // Property 19: 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 19: overloadedAdversarialTupleLocalCaller has no unexpected revert
+    // Property 20: 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 21: 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 22: 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");
+    }
 }

From e5c550598c3aa5f325e8107df98e347377ed5467 Mon Sep 17 00:00:00 2001
From: Thomas Marchand <thomas@lfglabs.dev>
Date: Tue, 8 Sep 2026 08:41:02 +0200
Subject: [PATCH 23/27] fix(reentrancy): complete registry executable semantics

---
 Contracts/Smoke/SecurityCombos.lean           |  18 ++
 Verity/Core/Model/CallbackBridge.lean         |  70 +++++++
 Verity/Core/Model/NonReentrantGuard.lean      |  19 +-
 Verity/Macro/Translate.lean                   | 184 +++++++++++++-----
 .../Model/GeneratedEntrypointRegistry.lean    |  10 +-
 5 files changed, 239 insertions(+), 62 deletions(-)

diff --git a/Contracts/Smoke/SecurityCombos.lean b/Contracts/Smoke/SecurityCombos.lean
index c1c45dd686..3a08251794 100644
--- a/Contracts/Smoke/SecurityCombos.lean
+++ b/Contracts/Smoke/SecurityCombos.lean
@@ -251,6 +251,10 @@ verity_contract NonreentrantQualifiedHelperResolution where
     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"
@@ -279,6 +283,20 @@ verity_contract NonreentrantQualifiedHelperResolution where
     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
diff --git a/Verity/Core/Model/CallbackBridge.lean b/Verity/Core/Model/CallbackBridge.lean
index 782c64e645..e39c305af9 100644
--- a/Verity/Core/Model/CallbackBridge.lean
+++ b/Verity/Core/Model/CallbackBridge.lean
@@ -42,6 +42,76 @@ instance : Coe (List (Verity.ContractState → Verity.ContractState))
 
 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
+    calldataSize := ctx.calldataSize
+    calldata := ctx.calldata }
+
+def restoreCallbackContext (outer callbackResult : Verity.ContractState) :
+    Verity.ContractState :=
+  { callbackResult with
+    sender := outer.sender
+    msgValue := outer.msgValue
+    calldataSize := outer.calldataSize
+    calldata := outer.calldata }
+
+def callbackTransition (ctx : CallbackContext)
+    (entrypoint : Verity.ContractState → Verity.ContractState) :
+    Verity.ContractState → Verity.ContractState :=
+  fun outer => restoreCallbackContext outer (entrypoint (withCallbackContext ctx outer))
+
+@[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 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
+
 /-- 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. -/
diff --git a/Verity/Core/Model/NonReentrantGuard.lean b/Verity/Core/Model/NonReentrantGuard.lean
index 0ca472b680..5e1aff6b6d 100644
--- a/Verity/Core/Model/NonReentrantGuard.lean
+++ b/Verity/Core/Model/NonReentrantGuard.lean
@@ -47,23 +47,24 @@ def setLock (slot : Nat) (value : Uint256) (s : ContractState) : ContractState :
 /-- Executable semantics of a `nonreentrant(slot)` entrypoint. -/
 def guarded (slot : Nat) (body : Contract α) : Contract α :=
   fun s =>
-    if s.transientStorage slot = 0 then
+    if s.transientStorage slot ≠ 1 then
       match body.run (setLock slot 1 s) with
       | .success a s' => .success a (setLock slot 0 s')
       | .revert msg _ => .revert msg s
     else
       ContractResult.revert "reentrant call blocked" s
 
-/-- Lock held → the guarded entrypoint reverts without touching the state. -/
+/-- The compiler's sentinel value is held → the guarded entrypoint reverts
+without touching the state. Other transient values are not treated as held. -/
 theorem guarded_locked_reverts (slot : Nat) (body : Contract α)
-    (s : ContractState) (hlock : s.transientStorage slot ≠ 0) :
+    (s : ContractState) (hlock : s.transientStorage slot = 1) :
     guarded slot body s = ContractResult.revert "reentrant call blocked" s := by
   simp [guarded, hlock]
 
 /-- Lock free → the body runs from the locked state; successful exits release
 the lock, reverting exits roll back to the pre-call state. -/
 theorem guarded_free_runs_body (slot : Nat) (body : Contract α)
-    (s : ContractState) (hfree : s.transientStorage slot = 0) :
+    (s : ContractState) (hfree : s.transientStorage slot ≠ 1) :
     guarded slot body s =
       match body.run (setLock slot 1 s) with
       | .success a s' => .success a (setLock slot 0 s')
@@ -81,18 +82,18 @@ theorem guarded_success_releases (slot : Nat) (body : Contract α)
     (s s' : ContractState) (a : α)
     (hrun : guarded slot body s = ContractResult.success a s') :
     s'.transientStorage slot = 0 := by
-  by_cases hfree : s.transientStorage slot = 0
+  by_cases hfree : s.transientStorage slot ≠ 1
   · rw [guarded_free_runs_body slot body s hfree] at hrun
     cases hbody : body.run (setLock slot 1 s) with
     | success b sb => rw [hbody] at hrun; injection hrun with _ hs; rw [← hs]; simp
     | revert msg sr => rw [hbody] at hrun; cases hrun
-  · rw [guarded_locked_reverts slot body s hfree] at hrun
+  · rw [guarded_locked_reverts slot body s (by simpa using hfree)] at hrun
     cases hrun
 
 /-- The reentry-window theorem: while the lock is held, a callback into any
 same-lock guarded entrypoint is the identity as a state transformer. -/
 theorem guarded_reentry_blocked (slot : Nat) (body : Contract α)
-    (s : ContractState) (hlock : s.transientStorage slot ≠ 0) :
+    (s : ContractState) (hlock : s.transientStorage slot = 1) :
     (guarded slot body).runState s = s := by
   unfold Contract.runState
   rw [guarded_locked_reverts slot body s hlock]
@@ -101,7 +102,7 @@ theorem guarded_reentry_blocked (slot : Nat) (body : Contract α)
 identity on locked states: no interleaving of guarded entrypoints can act
 inside the window.  This is the schedule-level closure of the guard. -/
 theorem runSeq_guarded_locked_id (slot : Nat) (entries : List (Contract Unit))
-    (s : ContractState) (hlock : s.transientStorage slot ≠ 0) :
+    (s : ContractState) (hlock : s.transientStorage slot = 1) :
     runSeq (entries.map (fun entry => (guarded slot entry).runState)) s = s := by
   induction entries with
   | nil => rfl
@@ -114,7 +115,7 @@ theorem runSeq_guarded_locked_id (slot : Nat) (entries : List (Contract Unit))
 packaged in the `Preserves` shape used by `ReentrancySpec` registries. -/
 theorem guarded_preserves_on_locked (slot : Nat) (body : Contract Unit)
     (Inv : ContractState → Prop) :
-    ∀ s, s.transientStorage slot ≠ 0 → Inv s →
+    ∀ s, s.transientStorage slot = 1 → Inv s →
       Inv ((guarded slot body).runState s) := by
   intro s hlock hInv
   rw [guarded_reentry_blocked slot body s hlock]
diff --git a/Verity/Macro/Translate.lean b/Verity/Macro/Translate.lean
index 7c2b6080b9..81dfa8c785 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
@@ -2405,6 +2418,7 @@ private def threadHelperApp?
     (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
@@ -2436,8 +2450,14 @@ private def threadHelperApp?
         -- 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 helper.nonReentrantLock.isSome && helper.reentrancyTrusted &&
+        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
@@ -2767,11 +2787,12 @@ private partial def threadAdversaryThroughExecutableSyntax
     (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 fields constDecls immutableDecls
-    externalDecls helpers adversarialHelpers params locals adv
+    externalDecls helpers adversarialHelpers registryOnlyHelpers params locals adv
   let recurseChildren : CommandElabM Syntax := do
     match stx with
     | .node info kind args =>
@@ -2792,30 +2813,36 @@ private partial def threadAdversaryThroughExecutableSyntax
           | none => inferPureExprType fields constDecls immutableDecls externalDecls params scope rhs
         pure (scope.push (mkTypedLocal (toString name.getId) ty))
       catch _ => pure scope
-    let inferTuple (names : Array (Option String)) (rhs : Term) := do
+    let inferTuple (origin : Syntax) (names : Array (Option String)) (rhs : Term) := do
       try
-        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
+        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 names ⟨patDecl[4]⟩))
+        | 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 names ⟨patDecl[3][0]⟩))
+        | some names => pure (some (← inferTuple patDecl names ⟨patDecl[3][0]⟩))
         | none => pure none
       else
         pure none
@@ -2858,16 +2885,16 @@ private partial def threadAdversaryThroughExecutableSyntax
         let rewrittenBody : TSyntax ``Lean.Parser.Term.doSeq := ⟨bodyRaw⟩
         pure (#[], ← `(term| do $rewrittenBody))
     | `(term| $name:ident($[$args:term],*)) =>
+        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 params locals name args adv with
-        | some app => pure (#[], app)
+            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)
@@ -2951,7 +2978,7 @@ private partial def threadAdversaryThroughExecutableSyntax
       let mut rewritten : Array (TSyntax `doElem) := #[]
       for elem in elems do
         let raw ← threadAdversaryThroughExecutableSyntax fields constDecls immutableDecls
-          externalDecls helpers adversarialHelpers params scope adv elem.raw
+          externalDecls helpers adversarialHelpers registryOnlyHelpers params scope adv elem.raw
         rewritten := rewritten.push ⟨raw⟩
         scope ← extendLocals scope elem
       `(doSeq| $[$rewritten:doElem]*)
@@ -3006,7 +3033,7 @@ private partial def threadAdversaryThroughExecutableSyntax
           (externalArgAddress $rewrittenToken) $adv)))
   | `(doElem| let $name:ident ← $fn:ident($[$args:term],*)) =>
       match ← threadHelperApp? fields constDecls immutableDecls externalDecls
-          helpers adversarialHelpers params locals fn args adv with
+          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*) =>
@@ -3032,7 +3059,7 @@ private partial def threadAdversaryThroughExecutableSyntax
           (← `(doElem| let $name ← (totalSupply (externalArgAddress $token) $adv)))
       else
         match ← threadHelperApp? fields constDecls immutableDecls externalDecls
-            helpers adversarialHelpers params locals fn original adv with
+            helpers adversarialHelpers registryOnlyHelpers params locals fn original adv with
         | some app =>
             hoistLive false app fun rewritten => `(doElem| let $name ← $rewritten:term)
         | none =>
@@ -3161,7 +3188,7 @@ private partial def threadAdversaryThroughExecutableSyntax
         | _ => recurseChildren
       else
         match ← threadHelperApp? fields constDecls immutableDecls externalDecls
-          helpers adversarialHelpers params locals fn original adv with
+          helpers adversarialHelpers registryOnlyHelpers params locals fn original adv with
         | some app =>
             hoistLive false app fun rewritten => `(doElem| $rewritten:term)
         | none =>
@@ -3174,7 +3201,7 @@ private partial def threadAdversaryThroughExecutableSyntax
   | `(term| $name:ident $args:term*) =>
       let original := args.map fun arg => (⟨arg.raw⟩ : Term)
       match ← threadHelperApp? fields constDecls immutableDecls externalDecls
-          helpers adversarialHelpers params locals name original adv with
+          helpers adversarialHelpers registryOnlyHelpers params locals name original adv with
       | some app => pure app.raw
       | none =>
           if isLiveStateExternalCall ⟨stx⟩ then
@@ -5164,6 +5191,7 @@ def validateGeneratedDefNamesPublic
     let helperNames :=
       #[ s!"{generatedFnName}_modelBody"
        , s!"{generatedFnName}_entrypoint"
+       , s!"{generatedFnName}_registry"
        , s!"{generatedFnName}_model"
        , s!"{generatedFnName}_bridge"
        , s!"{generatedFnName}_semantic_preservation"
@@ -5181,7 +5209,8 @@ def validateGeneratedDefNamesPublic
        ]
     let helperNames :=
       if fn.nonReentrantLock.isSome && fn.reentrancyTrusted then
-        helperNames.push s!"{generatedFnName}_unguarded"
+        (helperNames.push s!"{generatedFnName}_unguarded").push
+          s!"{generatedFnName}_registry_unguarded"
       else
         helperNames
     for helperName in helperNames do
@@ -5461,7 +5490,7 @@ def mkConstructorDefCommandPublic
     else
       `(Compiler.CompilationModel.DenoteExternalCalls.AdversaryModel.stub)
   let executableBody := ⟨← threadAdversaryThroughExecutableSyntax fields constDecls immutableDecls
-    externalDecls functions adversarialHelpers ctor.params #[] advTerm executableBody.raw⟩
+    externalDecls functions adversarialHelpers #[] ctor.params #[] advTerm executableBody.raw⟩
   let fnType ← if opensReentrancyWindow then
       mkContractFnTypeWithAdversary ctor.params .unit
     else
@@ -5531,7 +5560,7 @@ def mkHostConstructorDefCommandPublic
       let body ← `(term| do $[$preludes:doElem]* $[$elems:doElem]*)
       let executableBody ← rewriteForEachExecutableBody fields externalDecls ctor.params body
       let executableBody := ⟨← threadAdversaryThroughExecutableSyntax fields constDecls immutableDecls
-        externalDecls functions ownAdversarialHelpers ctor.params #[] advTerm executableBody.raw⟩
+        externalDecls functions ownAdversarialHelpers #[] ctor.params #[] advTerm executableBody.raw⟩
       let fnValue ← if containsExternalCall then
           mkContractFnValueWithAdversary advIdent ctor.params executableBody
         else
@@ -5560,10 +5589,17 @@ def mkIncludeAliasCommandsPublic
             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)
@@ -5635,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 ←
@@ -5650,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.
@@ -5666,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
@@ -5681,28 +5737,51 @@ def mkFunctionCommandsPublic
       mkContractFnTypeWithAdversary fn.params fn.returnTy
     else
       mkContractFnType fn.params fn.returnTy
-  let fnExecutableBody := ⟨← threadAdversaryThroughExecutableSyntax fields constDecls immutableDecls
-    externalDecls functions 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 fnExecutableBody
+        mkContractFnValueWithAdversary advIdent fn.params publicExecutableBody
       else
-        mkContractFnValue fn.params fnExecutableBody
+        mkContractFnValue fn.params publicExecutableBody
     extraExecutableCmds := extraExecutableCmds.push
       (← `(command| def $unguardedId : $fnType := $unguardedValue))
-  let fnExecutableBody ← match fn.nonReentrantLock with
+  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) $fnExecutableBody)
-    | none => pure fnExecutableBody
+        `(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)
@@ -5728,11 +5807,13 @@ def mkFunctionCommandsPublic
     (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 mut applied : Term := fn.ident
-  if opensReentrancyWindow then
-    applied ← `($applied (ExecutableCallContext.ofAdversary $registryAdv:ident))
+  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
@@ -5743,9 +5824,14 @@ def mkFunctionCommandsPublic
     applied ← `($applied $registryParam:ident)
   let mut registryBody : Term ←
     `(($transition:ident : Verity.ContractState → Verity.ContractState) =
-      ($applied).runState)
+      Compiler.CompilationModel.DenoteExternalCalls.callbackTransition
+        $context:ident ($applied).runState)
   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 :
diff --git a/Verity/Proofs/Model/GeneratedEntrypointRegistry.lean b/Verity/Proofs/Model/GeneratedEntrypointRegistry.lean
index 29df6ddaf1..0a8d0a449d 100644
--- a/Verity/Proofs/Model/GeneratedEntrypointRegistry.lean
+++ b/Verity/Proofs/Model/GeneratedEntrypointRegistry.lean
@@ -30,16 +30,18 @@ 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) (value : Uint256) :
+theorem guardedPing_registered (adv : AdversaryModel) (ctx : CallbackContext)
+    (value : Uint256) :
     entrypointRegistry adv
-      (guardedPing (ExecutableCallContext.ofAdversary adv) value).runState := by
+      (callbackTransition ctx
+        (guardedPing_registry (ExecutableCallContext.ofAdversary adv) value).runState) := by
   left
-  exact ⟨value, rfl⟩
+  exact ⟨ctx, value, 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) :
+    (state : ContractState) (hlock : state.transientStorage 0 = 1) :
     (guardedPing (ExecutableCallContext.ofAdversary adv) value).runState state = state := by
   apply Verity.Core.NonReentrantGuard.guarded_reentry_blocked
   exact hlock

From 9cf62cb5846e830c4444e0d6a044ec555a915c45 Mon Sep 17 00:00:00 2001
From: Thomas Marchand <thomas@lfglabs.dev>
Date: Tue, 8 Sep 2026 08:47:42 +0200
Subject: [PATCH 24/27] test(reentrancy): refresh registry macro fixture

---
 ...onreentrantQualifiedHelperResolution.t.sol | 31 ++++++++++++++-----
 1 file changed, 23 insertions(+), 8 deletions(-)

diff --git a/artifacts/macro_property_tests/PropertyNonreentrantQualifiedHelperResolution.t.sol b/artifacts/macro_property_tests/PropertyNonreentrantQualifiedHelperResolution.t.sol
index 94cd69b9d2..9a290db10c 100644
--- a/artifacts/macro_property_tests/PropertyNonreentrantQualifiedHelperResolution.t.sol
+++ b/artifacts/macro_property_tests/PropertyNonreentrantQualifiedHelperResolution.t.sol
@@ -145,49 +145,64 @@ contract PropertyNonreentrantQualifiedHelperResolutionTest is YulTestBase {
         // TODO(#1011): decode `ret` and assert the concrete postcondition from Lean theorem.
         ret;
     }
-    // Property 15: overloadedTrustedCaller has no unexpected revert
+    // 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 16: overloadedAdversarialCaller has no unexpected revert
+    // 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 17: overloadedTrustedLocalCaller has no unexpected revert
+    // 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 18: overloadedAdversarialLocalCaller has no unexpected revert
+    // 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 19: overloadedTrustedTupleLocalCaller has no unexpected revert
+    // 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 20: overloadedAdversarialTupleLocalCaller has no unexpected revert
+    // 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 21: overloadedTrustedForEachCaller has no unexpected revert
+    // 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 22: overloadedAdversarialForEachSetBitCaller has no unexpected revert
+    // Property 24: overloadedAdversarialForEachSetBitCaller has no unexpected revert
     function testAuto_OverloadedAdversarialForEachSetBitCaller_NoUnexpectedRevert() public {
         vm.prank(alice);
         (bool ok,) = target.call(abi.encodeWithSignature("overloadedAdversarialForEachSetBitCaller()"));

From 01b17a9f34b3beb7e7af391ce279a04bb30a6086 Mon Sep 17 00:00:00 2001
From: Thomas Marchand <thomas@lfglabs.dev>
Date: Tue, 8 Sep 2026 10:39:28 +0200
Subject: [PATCH 25/27] fix(reentrancy): align callback frame and guard

---
 Verity/Core/Model/CallbackBridge.lean         | 12 +++++++++++-
 Verity/Core/Model/NonReentrantGuard.lean      | 19 +++++++++----------
 .../Model/GeneratedEntrypointRegistry.lean    |  2 +-
 3 files changed, 21 insertions(+), 12 deletions(-)

diff --git a/Verity/Core/Model/CallbackBridge.lean b/Verity/Core/Model/CallbackBridge.lean
index e39c305af9..8c9063d2ab 100644
--- a/Verity/Core/Model/CallbackBridge.lean
+++ b/Verity/Core/Model/CallbackBridge.lean
@@ -60,8 +60,10 @@ def withCallbackContext (ctx : CallbackContext) (world : Verity.ContractState) :
   { world with
     sender := ctx.sender
     msgValue := ctx.msgValue
+    selfBalance := world.selfBalance + ctx.msgValue
     calldataSize := ctx.calldataSize
-    calldata := ctx.calldata }
+    calldata := ctx.calldata
+    returndata := [] }
 
 def restoreCallbackContext (outer callbackResult : Verity.ContractState) :
     Verity.ContractState :=
@@ -92,6 +94,14 @@ def callbackTransition (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 callbackTransition_restores_sender (ctx : CallbackContext)
     (entrypoint : Verity.ContractState → Verity.ContractState)
     (outer : Verity.ContractState) :
diff --git a/Verity/Core/Model/NonReentrantGuard.lean b/Verity/Core/Model/NonReentrantGuard.lean
index 5e1aff6b6d..86ffc25f48 100644
--- a/Verity/Core/Model/NonReentrantGuard.lean
+++ b/Verity/Core/Model/NonReentrantGuard.lean
@@ -47,24 +47,23 @@ def setLock (slot : Nat) (value : Uint256) (s : ContractState) : ContractState :
 /-- Executable semantics of a `nonreentrant(slot)` entrypoint. -/
 def guarded (slot : Nat) (body : Contract α) : Contract α :=
   fun s =>
-    if s.transientStorage slot ≠ 1 then
+    if s.transientStorage slot = 0 then
       match body.run (setLock slot 1 s) with
       | .success a s' => .success a (setLock slot 0 s')
       | .revert msg _ => .revert msg s
     else
       ContractResult.revert "reentrant call blocked" s
 
-/-- The compiler's sentinel value is held → the guarded entrypoint reverts
-without touching the state. Other transient values are not treated as held. -/
+/-- 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 = 1) :
+    (s : ContractState) (hlock : s.transientStorage slot ≠ 0) :
     guarded slot body s = ContractResult.revert "reentrant call blocked" s := by
   simp [guarded, hlock]
 
 /-- Lock free → the body runs from the locked state; successful exits release
 the lock, reverting exits roll back to the pre-call state. -/
 theorem guarded_free_runs_body (slot : Nat) (body : Contract α)
-    (s : ContractState) (hfree : s.transientStorage slot ≠ 1) :
+    (s : ContractState) (hfree : s.transientStorage slot = 0) :
     guarded slot body s =
       match body.run (setLock slot 1 s) with
       | .success a s' => .success a (setLock slot 0 s')
@@ -82,18 +81,18 @@ theorem guarded_success_releases (slot : Nat) (body : Contract α)
     (s s' : ContractState) (a : α)
     (hrun : guarded slot body s = ContractResult.success a s') :
     s'.transientStorage slot = 0 := by
-  by_cases hfree : s.transientStorage slot ≠ 1
+  by_cases hfree : s.transientStorage slot = 0
   · rw [guarded_free_runs_body slot body s hfree] at hrun
     cases hbody : body.run (setLock slot 1 s) with
     | success b sb => rw [hbody] at hrun; injection hrun with _ hs; rw [← hs]; simp
     | revert msg sr => rw [hbody] at hrun; cases hrun
-  · rw [guarded_locked_reverts slot body s (by simpa using hfree)] at hrun
+  · rw [guarded_locked_reverts slot body s hfree] at hrun
     cases hrun
 
 /-- The reentry-window theorem: while the lock is held, a callback into any
 same-lock guarded entrypoint is the identity as a state transformer. -/
 theorem guarded_reentry_blocked (slot : Nat) (body : Contract α)
-    (s : ContractState) (hlock : s.transientStorage slot = 1) :
+    (s : ContractState) (hlock : s.transientStorage slot ≠ 0) :
     (guarded slot body).runState s = s := by
   unfold Contract.runState
   rw [guarded_locked_reverts slot body s hlock]
@@ -102,7 +101,7 @@ theorem guarded_reentry_blocked (slot : Nat) (body : Contract α)
 identity on locked states: no interleaving of guarded entrypoints can act
 inside the window.  This is the schedule-level closure of the guard. -/
 theorem runSeq_guarded_locked_id (slot : Nat) (entries : List (Contract Unit))
-    (s : ContractState) (hlock : s.transientStorage slot = 1) :
+    (s : ContractState) (hlock : s.transientStorage slot ≠ 0) :
     runSeq (entries.map (fun entry => (guarded slot entry).runState)) s = s := by
   induction entries with
   | nil => rfl
@@ -115,7 +114,7 @@ theorem runSeq_guarded_locked_id (slot : Nat) (entries : List (Contract Unit))
 packaged in the `Preserves` shape used by `ReentrancySpec` registries. -/
 theorem guarded_preserves_on_locked (slot : Nat) (body : Contract Unit)
     (Inv : ContractState → Prop) :
-    ∀ s, s.transientStorage slot = 1 → Inv s →
+    ∀ s, s.transientStorage slot ≠ 0 → Inv s →
       Inv ((guarded slot body).runState s) := by
   intro s hlock hInv
   rw [guarded_reentry_blocked slot body s hlock]
diff --git a/Verity/Proofs/Model/GeneratedEntrypointRegistry.lean b/Verity/Proofs/Model/GeneratedEntrypointRegistry.lean
index 0a8d0a449d..49e5256e4a 100644
--- a/Verity/Proofs/Model/GeneratedEntrypointRegistry.lean
+++ b/Verity/Proofs/Model/GeneratedEntrypointRegistry.lean
@@ -41,7 +41,7 @@ theorem guardedPing_registered (adv : AdversaryModel) (ctx : CallbackContext)
 /-- 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 = 1) :
+    (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

From ded1d3155be30db45fb8c2196b623bb40a8f9b32 Mon Sep 17 00:00:00 2001
From: Thomas Marchand <thomas@lfglabs.dev>
Date: Tue, 8 Sep 2026 10:53:27 +0200
Subject: [PATCH 26/27] fix(reentrancy): isolate callback frame memory

---
 Verity/Core/Model/CallbackBridge.lean | 19 ++++++++++++++++++-
 1 file changed, 18 insertions(+), 1 deletion(-)

diff --git a/Verity/Core/Model/CallbackBridge.lean b/Verity/Core/Model/CallbackBridge.lean
index 8c9063d2ab..d37e618e5a 100644
--- a/Verity/Core/Model/CallbackBridge.lean
+++ b/Verity/Core/Model/CallbackBridge.lean
@@ -63,6 +63,7 @@ def withCallbackContext (ctx : CallbackContext) (world : Verity.ContractState) :
     selfBalance := world.selfBalance + ctx.msgValue
     calldataSize := ctx.calldataSize
     calldata := ctx.calldata
+    memory := fun _ => 0
     returndata := [] }
 
 def restoreCallbackContext (outer callbackResult : Verity.ContractState) :
@@ -71,7 +72,9 @@ def restoreCallbackContext (outer callbackResult : Verity.ContractState) :
     sender := outer.sender
     msgValue := outer.msgValue
     calldataSize := outer.calldataSize
-    calldata := outer.calldata }
+    calldata := outer.calldata
+    memory := outer.memory
+    returndata := outer.returndata }
 
 def callbackTransition (ctx : CallbackContext)
     (entrypoint : Verity.ContractState → Verity.ContractState) :
@@ -102,6 +105,10 @@ def callbackTransition (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) :
@@ -122,6 +129,16 @@ def callbackTransition (ctx : CallbackContext)
     (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. -/

From c7e0fa6d097fc4d76b24d66b4a108b221ae03295 Mon Sep 17 00:00:00 2001
From: Thomas Marchand <thomas@lfglabs.dev>
Date: Tue, 8 Sep 2026 11:27:52 +0200
Subject: [PATCH 27/27] fix(registry): preserve callback rollback semantics

---
 Verity/Core/Model/CallbackBridge.lean         | 28 +++++++++++++++++++
 Verity/Macro/Translate.lean                   |  6 ++--
 .../Model/GeneratedEntrypointRegistry.lean    |  8 +++---
 3 files changed, 36 insertions(+), 6 deletions(-)

diff --git a/Verity/Core/Model/CallbackBridge.lean b/Verity/Core/Model/CallbackBridge.lean
index d37e618e5a..b83306ae39 100644
--- a/Verity/Core/Model/CallbackBridge.lean
+++ b/Verity/Core/Model/CallbackBridge.lean
@@ -81,6 +81,34 @@ def callbackTransition (ctx : CallbackContext)
     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
diff --git a/Verity/Macro/Translate.lean b/Verity/Macro/Translate.lean
index 81dfa8c785..79a77a7699 100644
--- a/Verity/Macro/Translate.lean
+++ b/Verity/Macro/Translate.lean
@@ -5824,8 +5824,10 @@ def mkFunctionCommandsPublic
     applied ← `($applied $registryParam:ident)
   let mut registryBody : Term ←
     `(($transition:ident : Verity.ContractState → Verity.ContractState) =
-      Compiler.CompilationModel.DenoteExternalCalls.callbackTransition
-        $context:ident ($applied).runState)
+      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 ←
diff --git a/Verity/Proofs/Model/GeneratedEntrypointRegistry.lean b/Verity/Proofs/Model/GeneratedEntrypointRegistry.lean
index 49e5256e4a..c320aed0cc 100644
--- a/Verity/Proofs/Model/GeneratedEntrypointRegistry.lean
+++ b/Verity/Proofs/Model/GeneratedEntrypointRegistry.lean
@@ -31,12 +31,12 @@ 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) :
+    (value : Uint256) (hvalue : ctx.msgValue = 0) :
     entrypointRegistry adv
-      (callbackTransition ctx
-        (guardedPing_registry (ExecutableCallContext.ofAdversary adv) value).runState) := by
+      (callbackContractTransition ctx
+        (guardedPing_registry (ExecutableCallContext.ofAdversary adv) value)) := by
   left
-  exact ⟨ctx, value, rfl⟩
+  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. -/