proofs: sorry reduction pass 5 — systematic plan and fixes

.github/actions/setup-lean/action.yml

@@ -100,7 +100,7 @@ runs:
         if [ -x "$HOME/.elan/bin/elan" ]; then
           exit 0
         fi
-        curl -sSfL "https://raw.githubusercontent.com/leanprover/elan/${ELAN_VERSION}/elan-init.sh" -o elan-init.sh
+        curl -sSfL --retry 3 --retry-delay 5 "https://raw.githubusercontent.com/leanprover/elan/${ELAN_VERSION}/elan-init.sh" -o elan-init.sh
         echo "${ELAN_INIT_SHA256}  elan-init.sh" | sha256sum -c -
         bash elan-init.sh -y --default-toolchain none
         rm elan-init.sh

AXIOMS.md

@@ -41,6 +41,33 @@ Instead, Verity treats it as a black box and validates its outputs in CI.
 
 **Risk**: Low.
 
+### 2. `solidityMappingSlot_lt_evmModulus`
+
+**Location**: `Compiler/Proofs/MappingSlot.lean:125`
+
+**Statement**:
+```lean
+axiom solidityMappingSlot_lt_evmModulus (baseSlot key : Nat) :
+    solidityMappingSlot baseSlot key < Compiler.Constants.evmModulus
+```
+
+**Purpose**:
+Asserts that the keccak256 hash used to compute a Solidity mapping slot fits
+in 256 bits (i.e. is less than 2^256). This is mathematically true because
+keccak256 produces exactly 32 bytes, but unprovable in Lean because `ffi.KEC`
+is an opaque FFI call that does not expose the output length.
+
+**Why this is currently an axiom**:
+The FFI boundary hides the byte-length guarantee. Proving it would require
+internalising the keccak256 spec or exposing output-length metadata from the
+FFI layer.
+
+**Soundness controls**:
+- End-to-end regression suites exercise mapping reads/writes.
+- Mapping-slot abstraction boundary checks in CI.
+
+**Risk**: Low.
+
 ## Trusted Cryptographic Primitive (Non-Axiom)
 
 ### `ffi.KEC` (keccak256 via FFI)
@@ -134,7 +161,7 @@ specification.
 
 ## Trust Summary
 
-- Active axioms: 1
+- Active axioms: 2
 - Production blockers from axioms: 0
 - Enforcement: `scripts/check_axioms.py` ensures this file tracks exact source locations.
 - All internal compiler functions are proven to terminate (no axioms involved).
@@ -147,4 +174,4 @@ Any commit that adds, removes, renames, or moves an axiom must update this file
 
 If this file is stale, trust analysis is stale.
 
-**Last Updated**: 2026-03-11
+**Last Updated**: 2026-03-27

Compiler/CompilationModel/StorageWrites.lean

@@ -85,28 +85,33 @@ def compileSetStorage (fields : List Field) (dynamicSource : DynamicDataSource)
               throw s!"Compilation error: field '{field}' is not address-typed; use Stmt.setStorage instead"
         let slots := slot :: f.aliasSlots
         let valueExpr ← compileExpr fields dynamicSource value
+        let storedValueExpr :=
+          if requireAddressField then
+            YulExpr.call "and" [valueExpr, YulExpr.hex Compiler.Constants.addressMask]
+          else
+            valueExpr
         match slots with
         | [] =>
             throw s!"Compilation error: internal invariant failure: no write slots for field '{field}' in setStorage"
         | [singleSlot] =>
             match f.packedBits with
             | none =>
-                pure [YulStmt.expr (YulExpr.call "sstore" [YulExpr.lit singleSlot, valueExpr])]
+                pure [YulStmt.expr (YulExpr.call "sstore" [YulExpr.lit singleSlot, storedValueExpr])]
             | some packed =>
-                pure (compilePackedStorageWrite (YulExpr.lit singleSlot) valueExpr packed)
+                pure (compilePackedStorageWrite (YulExpr.lit singleSlot) storedValueExpr packed)
         | _ =>
             let writeSlots := slots.map YulExpr.lit
             match f.packedBits with
             | none =>
                 pure [
                   YulStmt.block (
-                    [YulStmt.let_ "__compat_value" valueExpr] ++
+                    [YulStmt.let_ "__compat_value" storedValueExpr] ++
                     writeSlots.map (fun writeSlot =>
                       YulStmt.expr (YulExpr.call "sstore" [writeSlot, YulExpr.ident "__compat_value"]))
                   )
                 ]
             | some packed =>
-                pure (compileCompatPackedStorageWrites writeSlots valueExpr packed)
+                pure (compileCompatPackedStorageWrites writeSlots storedValueExpr packed)
     | none => throw s!"Compilation error: unknown storage field '{field}' in setStorage"
 
 def compileStorageArrayPush (fields : List Field) (dynamicSource : DynamicDataSource)

Compiler/CompilationModel/Types.lean

@@ -547,6 +547,25 @@ theorem fieldName_eq_of_findFieldWithResolvedSlot_eq_some
       case isFalse =>
         exact ih (idx + 1) hgo
 
+private theorem find_eq_of_findFieldByName_go
+    {name : String}
+    {f : Field}
+    {slot : Nat}
+    {fields : List Field}
+    {idx : Nat} :
+    findFieldByName.go name (fun f slot => (f, slot)) fields idx = some (f, slot) →
+    fields.find? (·.name == name) = some f := by
+  intro hgo
+  induction fields generalizing idx with
+  | nil => simp [findFieldByName.go] at hgo
+  | cons hd tl ih =>
+    simp only [findFieldByName.go] at hgo
+    by_cases hname : hd.name == name
+    · simp [hname] at hgo ⊢
+      exact hgo.1
+    · simp [hname] at hgo ⊢
+      exact ih hgo
+
 def findFieldWriteSlots (fields : List Field) (name : String) : Option (List Nat) :=
   findFieldByName fields name fun f slot => slot :: f.aliasSlots
 
@@ -674,6 +693,38 @@ def isMapping (fields : List Field) (name : String) : Bool :=
     | FieldType.mappingStruct2 _ _ _ => true
     | _ => false
 
+theorem isMapping_false_of_findFieldWithResolvedSlot_address
+    {fields : List Field}
+    {name : String}
+    {f : Field}
+    {slot : Nat}
+    (hfind : findFieldWithResolvedSlot fields name = some (f, slot))
+    (hty : f.ty = FieldType.address) :
+    isMapping fields name = false := by
+  unfold isMapping
+  have hfound : fields.find? (·.name == name) = some f := by
+    unfold findFieldWithResolvedSlot at hfind
+    unfold findFieldByName at hfind
+    exact find_eq_of_findFieldByName_go hfind
+  rw [hfound]
+  simp [Option.any, hty]
+
+theorem isMapping_false_of_findFieldWithResolvedSlot_uint256
+    {fields : List Field}
+    {name : String}
+    {f : Field}
+    {slot : Nat}
+    (hfind : findFieldWithResolvedSlot fields name = some (f, slot))
+    (hty : f.ty = FieldType.uint256) :
+    isMapping fields name = false := by
+  unfold isMapping
+  have hfound : fields.find? (·.name == name) = some f := by
+    unfold findFieldWithResolvedSlot at hfind
+    unfold findFieldByName at hfind
+    exact find_eq_of_findFieldByName_go hfind
+  rw [hfound]
+  simp [Option.any, hty]
+
 -- Helper: Is field a double mapping?
 def isMapping2 (fields : List Field) (name : String) : Bool :=
   fields.find? (·.name == name) |>.any fun f =>

Compiler/CompilationModel/ValidationHelpers.lean

@@ -132,24 +132,24 @@ mutual
 def collectStmtNames : Stmt → List String
   | Stmt.letVar name value => name :: collectExprNames value
   | Stmt.assignVar name value => name :: collectExprNames value
-  | Stmt.setStorage field value | Stmt.setStorageAddr field value => field :: collectExprNames value
-  | Stmt.storageArrayPush field value => field :: collectExprNames value
-  | Stmt.storageArrayPop field => [field]
-  | Stmt.setStorageArrayElement field index value =>
-      field :: collectExprNames index ++ collectExprNames value
-  | Stmt.setMapping field key value => field :: collectExprNames key ++ collectExprNames value
-  | Stmt.setMappingWord field key _ value => field :: collectExprNames key ++ collectExprNames value
-  | Stmt.setMappingPackedWord field key _ _ value => field :: collectExprNames key ++ collectExprNames value
-  | Stmt.setMapping2 field key1 key2 value =>
-    field :: collectExprNames key1 ++ collectExprNames key2 ++ collectExprNames value
-  | Stmt.setMapping2Word field key1 key2 _ value =>
-    field :: collectExprNames key1 ++ collectExprNames key2 ++ collectExprNames value
-  | Stmt.setMappingUint field key value => field :: collectExprNames key ++ collectExprNames value
-  | Stmt.setMappingChain field keys value =>
-    field :: collectExprListNames keys ++ collectExprNames value
-  | Stmt.setStructMember field key _ value => field :: collectExprNames key ++ collectExprNames value
-  | Stmt.setStructMember2 field key1 key2 _ value =>
-    field :: collectExprNames key1 ++ collectExprNames key2 ++ collectExprNames value
+  | Stmt.setStorage _ value | Stmt.setStorageAddr _ value => collectExprNames value
+  | Stmt.storageArrayPush _ value => collectExprNames value
+  | Stmt.storageArrayPop _ => []
+  | Stmt.setStorageArrayElement _ index value =>
+      collectExprNames index ++ collectExprNames value
+  | Stmt.setMapping _ key value => collectExprNames key ++ collectExprNames value
+  | Stmt.setMappingWord _ key _ value => collectExprNames key ++ collectExprNames value
+  | Stmt.setMappingPackedWord _ key _ _ value => collectExprNames key ++ collectExprNames value
+  | Stmt.setMapping2 _ key1 key2 value =>
+    collectExprNames key1 ++ collectExprNames key2 ++ collectExprNames value
+  | Stmt.setMapping2Word _ key1 key2 _ value =>
+    collectExprNames key1 ++ collectExprNames key2 ++ collectExprNames value
+  | Stmt.setMappingUint _ key value => collectExprNames key ++ collectExprNames value
+  | Stmt.setMappingChain _ keys value =>
+    collectExprListNames keys ++ collectExprNames value
+  | Stmt.setStructMember _ key _ value => collectExprNames key ++ collectExprNames value
+  | Stmt.setStructMember2 _ key1 key2 _ value =>
+    collectExprNames key1 ++ collectExprNames key2 ++ collectExprNames value
   | Stmt.require cond _ => collectExprNames cond
   | Stmt.requireError cond errorName args => errorName :: collectExprNames cond ++ collectExprListNames args
   | Stmt.revertError errorName args => errorName :: collectExprListNames args

Compiler/CompilationModelFeatureTest.lean

@@ -1047,6 +1047,21 @@ def initializeExecutableRunsOnce : Bool :=
 
 example : initializeExecutableRunsOnce = true := by native_decide
 
+def compileSetStorageAddrMasksAddressWrites : Bool :=
+  let fields : List Compiler.CompilationModel.Field :=
+    [{ name := "owner", ty := Compiler.CompilationModel.FieldType.address }]
+  match Compiler.CompilationModel.compileSetStorage fields .calldata "owner" (Expr.literal 42) true with
+  | .ok [Compiler.Yul.YulStmt.expr
+      (Compiler.Yul.YulExpr.call "sstore"
+        [Compiler.Yul.YulExpr.lit 0,
+         Compiler.Yul.YulExpr.call "and"
+           [Compiler.Yul.YulExpr.lit 42,
+            Compiler.Yul.YulExpr.hex mask]])] =>
+      mask == Compiler.Constants.addressMask
+  | _ => false
+
+example : compileSetStorageAddrMasksAddressWrites = true := by native_decide
+
 def initializeExecutableSecondCallReverts : Bool :=
   let seedOwner := wordToAddress 77
   match MacroInitializer.initOwner seedOwner Verity.defaultState with
@@ -2622,6 +2637,9 @@ set_option maxRecDepth 4096 in
   expectTrue
     "macro initializer executable path seeds storage on the first call"
     MacroInitializerSmoke.initializeExecutableRunsOnce
+  expectTrue
+    "setStorageAddr compilation masks stored address words"
+    MacroInitializerSmoke.compileSetStorageAddrMasksAddressWrites
   expectTrue
     "macro initializer executable path rejects a second call"
     MacroInitializerSmoke.initializeExecutableSecondCallReverts

Compiler/Proofs/IRGeneration/Contract.lean

@@ -2885,13 +2885,13 @@ theorem compile_preserves_semantics
 -- SORRY'D:     (hparamsSupported := hparamsSupported)
 -- SORRY'D:     (hfunction := hfunction)
 
--- SORRY'D: /-- Helper-proof-carrying whole-contract Layer 2 theorem.
--- SORRY'D: This theorem family is the intended stable public interface for the helper
--- SORRY'D: composition step tracked by `#1630`: callers can already pass explicit
--- SORRY'D: summary-soundness evidence today, and once the body proof consumes it this
--- TYPESIG_SORRY: theorem can strengthen without another theorem-shape rewrite. The current proof
--- TYPESIG_SORRY: still reduces through the legacy helper-closed path, so the trusted boundary is
--- TYPESIG_SORRY: unchanged. -/
+/-- Helper-proof-carrying whole-contract Layer 2 theorem.
+This theorem family is the intended stable public interface for the helper
+composition step tracked by `#1630`: callers can already pass explicit
+summary-soundness evidence today, and once the body proof consumes it this
+theorem can strengthen without another theorem-shape rewrite. The current proof
+still reduces through the legacy helper-closed path, so the trusted boundary is
+unchanged. -/
 theorem compile_preserves_semantics_with_helper_proofs
     (model : CompilationModel)
     (selectors : List Nat)

Compiler/Proofs/IRGeneration/ExprCore.lean

@@ -111,6 +111,37 @@ inductive ExprCompileCore : Expr → Prop where
       ExprCompileCore lhs → ExprCompileCore rhs → ExprCompileCore (.logicalAnd lhs rhs)
   | logicalOr {lhs rhs : Expr} :
       ExprCompileCore lhs → ExprCompileCore rhs → ExprCompileCore (.logicalOr lhs rhs)
+  | bitAnd {lhs rhs : Expr} :
+      ExprCompileCore lhs → ExprCompileCore rhs → ExprCompileCore (.bitAnd lhs rhs)
+  | bitOr {lhs rhs : Expr} :
+      ExprCompileCore lhs → ExprCompileCore rhs → ExprCompileCore (.bitOr lhs rhs)
+  | bitXor {lhs rhs : Expr} :
+      ExprCompileCore lhs → ExprCompileCore rhs → ExprCompileCore (.bitXor lhs rhs)
+  | bitNot {expr : Expr} :
+      ExprCompileCore expr → ExprCompileCore (.bitNot expr)
+  | shl {shift value : Expr} :
+      ExprCompileCore shift → ExprCompileCore value → ExprCompileCore (.shl shift value)
+  | shr {shift value : Expr} :
+      ExprCompileCore shift → ExprCompileCore value → ExprCompileCore (.shr shift value)
+  | min {lhs rhs : Expr} :
+      ExprCompileCore lhs → ExprCompileCore rhs → ExprCompileCore (.min lhs rhs)
+  | max {lhs rhs : Expr} :
+      ExprCompileCore lhs → ExprCompileCore rhs → ExprCompileCore (.max lhs rhs)
+  | ite {cond thenVal elseVal : Expr} :
+      ExprCompileCore cond → ExprCompileCore thenVal → ExprCompileCore elseVal →
+        ExprCompileCore (.ite cond thenVal elseVal)
+  | ceilDiv {lhs rhs : Expr} :
+      ExprCompileCore lhs → ExprCompileCore rhs → ExprCompileCore (.ceilDiv lhs rhs)
+  | wMulDown {lhs rhs : Expr} :
+      ExprCompileCore lhs → ExprCompileCore rhs → ExprCompileCore (.wMulDown lhs rhs)
+  | wDivUp {lhs rhs : Expr} :
+      ExprCompileCore lhs → ExprCompileCore rhs → ExprCompileCore (.wDivUp lhs rhs)
+  | mulDivDown {a b c : Expr} :
+      ExprCompileCore a → ExprCompileCore b → ExprCompileCore c →
+        ExprCompileCore (.mulDivDown a b c)
+  | mulDivUp {a b c : Expr} :
+      ExprCompileCore a → ExprCompileCore b → ExprCompileCore c →
+        ExprCompileCore (.mulDivUp a b c)
 
 /-! ## Scope analysis -/