proof(reentrancy): generate guarded entrypoint registry

.github/workflows/verify.yml

@@ -11,6 +11,7 @@ on:
       - '.github/workflows/**'
       - '.github/workflows/verify.yml'
       - 'artifacts/**'
+      - 'artifacts/*'
       - 'Verity/**'
       - 'Verity.lean'
       - 'Compiler/**'
@@ -28,6 +29,7 @@ on:
       - 'lean-toolchain'
       - 'foundry.toml'
       - 'Makefile'
+      - 'PrintAxioms.lean'
       - 'README.md'
   pull_request:
     types: [opened, synchronize, reopened, closed]
@@ -37,6 +39,7 @@ on:
       - '.github/workflows/**'
       - '.github/workflows/verify.yml'
       - 'artifacts/**'
+      - 'artifacts/*'
       - 'Verity/**'
       - 'Verity.lean'
       - 'Compiler/**'
@@ -54,6 +57,7 @@ on:
       - 'lean-toolchain'
       - 'foundry.toml'
       - 'Makefile'
+      - 'PrintAxioms.lean'
       - 'README.md'
   workflow_dispatch:
     inputs:
@@ -324,6 +328,7 @@ jobs:
           python3 scripts/generate_evmyullean_capability_report.py
           python3 scripts/generate_evmyullean_native_lowering_report.py
           python3 scripts/generate_print_axioms.py
+          python3 scripts/generate_trust_surface_report.py
           python3 scripts/sync_verification_status_doc.py
 
       - name: Auto-commit refreshed artifacts

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,15 @@ theorem execIRStmt_lockRelease (fuel : Nat) (state : IRState) (slot : Nat)
   have hmod : slot % Compiler.Constants.evmModulus = slot := Nat.mod_eq_of_lt hslot
   simp [lockReleaseStmt, execIRStmt, evalIRExpr, hmod]
 
-/-- On the reachable (binary) lock values, the Yul decision `eq(lock, 1)`
-agrees with the source model's `lock ≠ 0` (`NonReentrantGuard.guarded`). -/
-theorem guard_decision_agrees (v : Nat) (hv : v = 0 ∨ v = 1) :
-    (v = 1) ↔ v ≠ 0 := by
-  rcases hv with h | h <;> simp [h]
+/-- Yul `if tload(slot)` sees the slot's transient value, so its nonzero
+decision is the source model's lock-held predicate `lock ≠ 0` for every
+stored value, not only the binary `{0,1}` acquire/release cycle. -/
+theorem guard_decision_agrees (state : IRState) (slot : Nat)
+    (hslot : slot < Compiler.Constants.evmModulus) :
+    evalIRExpr state (.call "tload" [.lit slot]) =
+      some (state.transientStorage slot) := by
+  have hmod : slot % Compiler.Constants.evmModulus = slot := Nat.mod_eq_of_lt hslot
+  simp [evalIRExpr, evalIRCall_tload_singleton, hmod]
 
 /-- Acquire-then-release round-trips the lock slot: the transient storage
 function is extensionally the initial one when the slot started free. -/

Contracts/Common.lean

@@ -393,6 +393,20 @@ def tryCatchWord (attempt : Uint256) (handler : String → Contract Unit) : Cont
 def calldatasize : Uint256 := 0
 def returndataSize : Uint256 := 0
 def calldataload (offset : Uint256) : Uint256 := offset
+/-- Registry-mode executable calldata. Public `calldatasize`/`calldataload`
+remain deterministic stubs; generated `*_registry` bodies use these so a
+callback that branches on live calldata is registered. Byte offset 0 of the
+word-list data region is `calldataload 4`, matching compiled dispatch.
+`calldataload 0` (and unaligned loads overlapping the first four bytes)
+observe `state.selector`, not a hard-coded 0. -/
+def calldatasizeLive : Contract Uint256 := fun state =>
+  ContractResult.success state.calldataSize state
+def calldataloadLive (offset : Uint256) : Contract Uint256 := fun state =>
+  ContractResult.success
+    (Verity.Core.Uint256.ofNat
+      (Compiler.CompilationModel.Denote.calldataloadWord
+        state.selector state.calldata offset.val))
+    state
 def mload (offset : Uint256) : Uint256 := offset
 def tload (offset : Uint256) : Contract Uint256 := fun state =>
   ContractResult.success (state.transientStorage (offset : Nat)) state
@@ -687,6 +701,11 @@ structure ExecutableCallContext where
   adversary : AdversaryModel
   resolve : String → Nat → Option Compiler.CompilationModel.DenoteFunctionCalls.LinkedExternal
 
+/-- Bind an explicit adversary while pinning every resolved linked call to
+`target = 0` and `value = 0`. This is the registry/executable convenience
+boundary: the adversary is live, but link-time callee address and ETH value
+are the zero defaults. Callers that need a real target or nonzero value must
+supply `resolve` themselves (`ofCallEnv` or a custom context). -/
 def ExecutableCallContext.ofAdversary (adv : AdversaryModel) : ExecutableCallContext :=
   { adversary := adv
     resolve := fun _ fallbackSiteId =>

Contracts/Smoke/SecurityCombos.lean

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

PrintAxioms.lean

@@ -41,6 +41,7 @@ import Contracts.Vault.Proofs.Native
 import Verity.Proofs.CheckedExternalCallConsumer
 import Verity.Proofs.LoopSimulationResultAware
 import Verity.Proofs.Model.CommonExternalCallEquivalence
+import Verity.Proofs.Model.GeneratedEntrypointRegistry
 import Verity.Proofs.Stdlib.Automation
 import Verity.Proofs.Stdlib.Int256
 import Verity.Proofs.Stdlib.ListSum
@@ -739,6 +740,17 @@ end Verity.AxiomAudit
   Contracts.legacyStringSafeTransfer_eq_stub
   Contracts.legacyStringSafeTransferFrom_eq_stub
 
+  -- Verity/Proofs/Model/GeneratedEntrypointRegistry.lean
+  Contracts.ReentrancyRelyGuarantee.GeneratedRegistry.guardedPing_registered
+  Contracts.ReentrancyRelyGuarantee.GeneratedRegistry.guardedPing_registered_ofAdversary
+  Contracts.ReentrancyRelyGuarantee.GeneratedRegistry.guardedPing_reentry_blocked
+  Contracts.ReentrancyRelyGuarantee.RegistryDispatchCalldata.setLast_registered_matching
+  Contracts.ReentrancyRelyGuarantee.RegistryDispatchCalldata.setLast_entrypoint_requires_dispatch
+  Contracts.ReentrancyRelyGuarantee.RegistryDispatchCalldata.receive_registered_empty
+  Contracts.ReentrancyRelyGuarantee.RegistryDispatchCalldata.receive_entrypoint_requires_empty
+  Contracts.ReentrancyRelyGuarantee.RegistryLiveCalldata.setFromCalldata_registered_live
+  Contracts.ReentrancyRelyGuarantee.generated_registry_callback_preserves
+
   -- Verity/Proofs/Stdlib/Automation.lean
   Verity.Proofs.Stdlib.Automation.isSuccess_success
   Verity.Proofs.Stdlib.Automation.isSuccess_revert
@@ -7619,4 +7631,4 @@ end Verity.AxiomAudit
   Compiler.Proofs.YulGeneration.YulTransaction.ofIR_args
 ]
 
--- Total: 7036 theorems/lemmas (5023 public, 2013 private, 0 sorry'd)
+-- Total: 7045 theorems/lemmas (5032 public, 2013 private, 0 sorry'd)

Verity/Core.lean

@@ -400,6 +400,9 @@ structure ContractState where
   blobBaseFee : Uint256 := 0
   calldataSize : Uint256 := 0
   calldata : List Nat := []                 -- Immutable calldata words used by ABI expression semantics
+  /-- 4-byte function selector for live `calldataload 0` in registry mode.
+      Compiled dispatch packs it in the high 4 bytes of the first word. -/
+  selector : Nat := 0
   memory : Nat → Uint256 := fun _ => 0     -- EVM memory (word-addressed, zero-initialized)
   knownAddresses : Nat → FiniteAddressSet  -- Tracked addresses per storage slot (for sum properties)
   events : List Event := []  -- Emitted events, append-only log (#153)