proof(reentrancy): generate guarded entrypoint registry

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])

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. -/

Contracts/Smoke/SecurityCombos.lean

@@ -175,6 +175,140 @@ verity_contract NonreentrantTrustedInternalHelperAccepted where
 
 #check_contract NonreentrantTrustedInternalHelperAccepted
 
+-- Regression for Codex's PR #2406 qualified-helper finding.  Qualified Lean
+-- helpers that merely share a guarded local function's final name must retain
+-- their qualifier; they do not resolve to the generated lock-free shadow.
+verity_contract QualifiedHelperLibrary where
+  storage
+
+  function trustedEntry (x : Uint256) : Uint256 := do
+    return x
+
+  function trustedPair (x : Uint256) : Tuple [Uint256, Uint256] := do
+    return (x, x)
+
+  function adversarialEntry (x : Uint256) : Uint256 := do
+    return x
+
+  function adversarialPair (x : Uint256) : Tuple [Uint256, Uint256] := do
+    return (x, x)
+
+verity_contract NonreentrantQualifiedHelperResolution where
+  storage
+    lock : Uint256 := slot 0
+    value : Uint256 := slot 1
+
+  linked_externals
+    external echo(Uint256) -> (Uint256)
+
+  function nonreentrant(lock) reentrancy_trusted trustedEntry (x : Uint256) : Uint256 := do
+    return x
+
+  function nonreentrant(lock) reentrancy_trusted trustedPair (x : Uint256) : Tuple [Uint256, Uint256] := do
+    return (x, x)
+
+  function nonreentrant(lock) reentrancy_trusted adversarialEntry (x : Uint256) : Uint256 := do
+    let echoed := externalCall "echo" [x]
+    return echoed
+
+  function nonreentrant(lock) reentrancy_trusted adversarialPair (x : Uint256) : Tuple [Uint256, Uint256] := do
+    let echoed := externalCall "echo" [x]
+    return (echoed, echoed)
+
+  function overloadedTrusted (_who : Address) : Uint256 := do
+    return 0
+
+  function nonreentrant(lock) reentrancy_trusted overloadedTrusted (x : Uint256) : Uint256 := do
+    return x
+
+  function overloadedAdversarial (_who : Address) : Uint256 := do
+    return 0
+
+  function nonreentrant(lock) reentrancy_trusted overloadedAdversarial (x : Uint256) : Uint256 := do
+    let echoed := externalCall "echo" [x]
+    return echoed
+
+  function makePair (x : Uint256) : Tuple [Uint256, Uint256] := do
+    return (x, x)
+
+  function qualifiedSpace (x : Uint256) : Uint256 := do
+    let y ← QualifiedHelperLibrary.trustedEntry x
+    return y
+
+  function qualifiedDestructure (x : Uint256) : Uint256 := do
+    let (left, right) ← QualifiedHelperLibrary.trustedPair x
+    return (add left right)
+
+  function qualifiedAdversarialSpace (x : Uint256) : Uint256 := do
+    let y ← QualifiedHelperLibrary.adversarialEntry x
+    return y
+
+  function qualifiedAdversarialDestructure (x : Uint256) : Uint256 := do
+    let (left, right) ← QualifiedHelperLibrary.adversarialPair x
+    return (add left right)
+
+  function reentrancy_trusted qualifiedNestedExternal (x : Uint256) : Uint256 := do
+    let y ← QualifiedHelperLibrary.trustedEntry (externalCall "echo" [x])
+    return y
+
+  function reentrancy_trusted trustedNestedExternal (x : Uint256) : Uint256 := do
+    let y ← trustedEntry(externalCall "echo" [x])
+    return y
+
+  function overloadedTrustedCaller (x : Uint256) : Unit := do
+    let y ← overloadedTrusted x
+    require (y == x) "wrong trusted overload"
+
+  function overloadedAdversarialCaller (x : Uint256) : Unit := do
+    let y ← overloadedAdversarial x
+    require (y == x) "wrong adversarial overload"
+
+  function overloadedTrustedLocalCaller () : Unit := do
+    let x ← getStorage value
+    let y ← overloadedTrusted x
+    require (y == x) "wrong trusted local overload"
+
+  function overloadedAdversarialLocalCaller () : Unit := do
+    let x ← getStorage value
+    let y ← overloadedAdversarial x
+    require (y == x) "wrong adversarial local overload"
+
+  function overloadedTrustedTupleLocalCaller (x : Uint256) : Unit := do
+    let (left, _right) ← makePair x
+    let y ← overloadedTrusted left
+    require (y == x) "wrong trusted tuple-local overload"
+
+  function overloadedAdversarialTupleLocalCaller (x : Uint256) : Unit := do
+    let (_left, right) ← makePair x
+    let y ← overloadedAdversarial right
+    require (y == x) "wrong adversarial tuple-local overload"
+
+  function overloadedTrustedQualifiedTupleCaller (x : Uint256) : Unit := do
+    let (left, _right) ← QualifiedHelperLibrary.trustedPair x
+    let y ← overloadedTrusted left
+    require (y == x) "wrong qualified tuple-local overload"
+
+  function nonreentrant(lock) reentrancy_trusted staticResultControlsStorage
+      (target : Uint256, x : Uint256)
+      local_obligations [manual_low_level_refinement := assumed "Static-call result threading is the explicit low-level boundary under test."] : Unit := do
+    let observed ← evmStaticCall(50000, target, 0, 0, 0, 0)
+    if observed == x then
+      setStorage value observed
+    else
+      pure ()
+
+  function overloadedTrustedForEachCaller () : Unit := do
+    forEach "i" 1 (do
+      let y ← overloadedTrusted i
+      require (y == i) "wrong trusted loop-local overload")
+
+  function overloadedAdversarialForEachSetBitCaller () : Unit := do
+    forEachSetBit "i" 1 (do
+      let y ← overloadedAdversarial i
+      require (y == i) "wrong adversarial loop-local overload")
+
+#check_contract NonreentrantQualifiedHelperResolution
+
 -- ════════════════════════════════════════════════════════════════════════════
 -- Stress-test contracts: edge-case coverage for Language Design Axes (#1731)
 -- ════════════════════════════════════════════════════════════════════════════

PrintAxioms.lean

@@ -38,6 +38,7 @@ import Contracts.Vault.Proofs.Native
 import Verity.Proofs.CheckedExternalCallConsumer
 import Verity.Proofs.LoopSimulationResultAware
 import Verity.Proofs.Model.CommonExternalCallEquivalence
+import Verity.Proofs.Model.GeneratedEntrypointRegistry
 import Verity.Proofs.Stdlib.Automation
 import Verity.Proofs.Stdlib.ListSum
 import Verity.Proofs.Stdlib.MappingAutomation
@@ -718,6 +719,11 @@ end Verity.AxiomAudit
   Contracts.legacyStringSafeTransfer_eq_stub
   Contracts.legacyStringSafeTransferFrom_eq_stub
 
+  -- Verity/Proofs/Model/GeneratedEntrypointRegistry.lean
+  Contracts.ReentrancyRelyGuarantee.GeneratedRegistry.guardedPing_registered
+  Contracts.ReentrancyRelyGuarantee.GeneratedRegistry.guardedPing_reentry_blocked
+  Contracts.ReentrancyRelyGuarantee.generated_registry_callback_preserves
+
   -- Verity/Proofs/Stdlib/Automation.lean
   Verity.Proofs.Stdlib.Automation.isSuccess_success
   Verity.Proofs.Stdlib.Automation.isSuccess_revert
@@ -7515,4 +7521,4 @@ end Verity.AxiomAudit
   Compiler.Proofs.YulGeneration.YulTransaction.ofIR_args
 ]
 
--- Total: 6953 theorems/lemmas (4963 public, 1990 private, 0 sorry'd)
+-- Total: 6956 theorems/lemmas (4966 public, 1990 private, 0 sorry'd)