feat: bytecode immutables (#1992)

Compiler/CompilationModel/Compile.lean

@@ -139,6 +139,16 @@ def compileStmt (fields : List Field) (events : List EventDef := [])
       pure [YulStmt.let_ name (← compileExpr fields dynamicSource value)]
   | Stmt.assignVar name value => do
       pure [YulStmt.assign name (← compileExpr fields dynamicSource value)]
+  | Stmt.setImmutable name value => do
+      match dynamicSource with
+      | .memory =>
+          pure [YulStmt.expr (YulExpr.call "setimmutable" [
+            YulExpr.call "dataoffset" [YulExpr.str "runtime"],
+            YulExpr.str name,
+            ← compileExpr fields dynamicSource value
+          ])]
+      | .calldata =>
+          throw s!"Compilation error: setImmutable '{name}' is only valid in constructor/deploy code"
   | Stmt.setStorage field value =>
       match adtTypes with
       | [] => compileSetStorage fields dynamicSource field value

Compiler/CompilationModel/Dispatch.lean

@@ -398,13 +398,16 @@ private def validateCompileInputsBeforeFieldWriteConflict
       pure ()
   for fn in spec.functions do
     validateFunctionSpec fn
+    validateSetImmutableRuntimeGuard fn
+    validateImmutableNamesInFunction spec.immutables fn
     validateInteropFunctionSpec fn
     validateSpecialEntrypointSpec fn
     validateEventArgShapesInFunction fn spec.events
     validateCustomErrorArgShapesInFunction fn spec.errors
     validateInternalCallShapesInFunction spec.functions fn
     validateExternalCallTargetsInFunction spec.externals fn
   validateConstructorSpec spec.constructor
+  validateImmutableNamesInConstructor spec.immutables spec.constructor
   validateInteropConstructorSpec spec.constructor
   validateExternalCallTargetsInConstructor spec.externals spec.constructor
   match spec.constructor with
@@ -445,6 +448,12 @@ private def validateCompileInputsBeforeFieldWriteConflict
       throw s!"Compilation error: duplicate field name '{dup}' in {spec.name}"
   | none =>
       pure ()
+  match firstDuplicateName (spec.immutables.map (·.name)) with
+  | some dup =>
+      throw s!"Compilation error: duplicate immutable name '{dup}' in {spec.name}"
+  | none =>
+      pure ()
+  validateImmutableInitialization spec.immutables spec.constructor
   match firstInvalidPackedBits spec.fields with
   | some (fieldName, packed) =>
       throw s!"Compilation error: field '{fieldName}' has invalid packedBits offset={packed.offset} width={packed.width} in {spec.name} ({issue623Ref}). Require 0 < width <= 256, offset < 256, and offset + width <= 256."

Compiler/CompilationModel/ExpressionCompile.lean

@@ -55,6 +55,7 @@ def compileExpr (fields : List Field)
   | Expr.literal n => pure (YulExpr.lit (n % uint256Modulus))
   | Expr.param name => pure (YulExpr.ident name)
   | Expr.constructorArg idx => pure (YulExpr.ident s!"arg{idx}")
+  | Expr.immutable name => pure (YulExpr.call "loadimmutable" [YulExpr.str name])
   | Expr.storage field =>
     if isMapping fields field then
       throw s!"Compilation error: field '{field}' is a mapping; use Expr.mapping, Expr.mappingWord, or Expr.mappingPackedWord"

Compiler/CompilationModel/LayoutReport.lean

@@ -105,6 +105,14 @@ private def fieldJson (declaredField effectiveField : Field) (idx : Nat) : Strin
     ("packedBits", jsonOption packedBitsJson declaredField.packedBits)
   ]
 
+private def immutableJson (imm : ImmutableSpec) : String :=
+  jsonObject [
+    ("name", jsonString imm.name),
+    ("type", jsonString (paramTypeToSolidityString imm.ty)),
+    ("storageFootprint", jsonNat 0),
+    ("kind", jsonString "bytecodeImmutable")
+  ]
+
 /-! ### Storage families and non-alias certificate (#1966)
 
 Each storage field becomes a "family" — the set of storage locations the
@@ -285,6 +293,7 @@ where
       ("contract", jsonString spec.name),
       ("storageNamespace", nsField),
       ("fields", jsonArray fieldsJson),
+      ("immutables", jsonArray (spec.immutables.map immutableJson)),
       ("storageFamilies", jsonArray familiesJson),
       ("nonAliasClaims", jsonArray claimsJson),
       ("reservedSlotRanges", jsonArray (spec.reservedSlotRanges.map reservedSlotRangeJson)),

Compiler/CompilationModel/TrustSurface.lean

@@ -220,6 +220,7 @@ private partial def collectUnguardedLowLevelStmtMechanics : Stmt → List String
   | .assignVar _ value
   | .setStorage _ value
   | .setStorageAddr _ value
+  | .setImmutable _ value
   | .setStorageWord _ _ value
   | .storageArrayPush _ value
   | .return value

Compiler/CompilationModel/UsageAnalysis.lean

@@ -160,7 +160,7 @@ def exprUsesArrayElementKind (includePlain includeWord : Bool) : Expr → Bool
         exprUsesArrayElementKind includePlain includeWord elseVal
   | Expr.adtConstruct _ _ args => exprListUsesArrayElementKind includePlain includeWord args
   | Expr.adtField _ _ _ _ _ => false
-  | Expr.literal _ | Expr.param _ | Expr.constructorArg _ | Expr.storage _ | Expr.storageAddr _
+  | Expr.literal _ | Expr.param _ | Expr.constructorArg _ | Expr.immutable _ | Expr.storage _ | Expr.storageAddr _
   | Expr.caller | Expr.contractAddress | Expr.txOrigin | Expr.chainid | Expr.msgValue | Expr.selfBalance | Expr.blockTimestamp
   | Expr.blockNumber | Expr.blobbasefee
   | Expr.calldatasize | Expr.returndataSize | Expr.localVar _ | Expr.arrayLength _
@@ -186,7 +186,7 @@ termination_by es => sizeOf es
 decreasing_by all_goals simp_wf; all_goals omega
 
 def stmtUsesArrayElementKind (includePlain includeWord : Bool) : Stmt → Bool
-  | Stmt.letVar _ value | Stmt.assignVar _ value | Stmt.setStorage _ value | Stmt.setStorageAddr _ value
+  | Stmt.letVar _ value | Stmt.assignVar _ value | Stmt.setStorage _ value | Stmt.setStorageAddr _ value | Stmt.setImmutable _ value
   | Stmt.setStorageWord _ _ value |
     Stmt.storageArrayPush _ value |
     Stmt.return value | Stmt.require value _ =>
@@ -342,7 +342,7 @@ def exprUsesArrayElement : Expr → Bool
       exprUsesArrayElement a
   | Expr.ite cond thenVal elseVal =>
       exprUsesArrayElement cond || exprUsesArrayElement thenVal || exprUsesArrayElement elseVal
-  | Expr.literal _ | Expr.param _ | Expr.constructorArg _ | Expr.storage _ | Expr.storageAddr _
+  | Expr.literal _ | Expr.param _ | Expr.constructorArg _ | Expr.immutable _ | Expr.storage _ | Expr.storageAddr _
   | Expr.caller | Expr.contractAddress | Expr.txOrigin | Expr.chainid | Expr.msgValue | Expr.selfBalance | Expr.blockTimestamp
   | Expr.blockNumber | Expr.blobbasefee
   | Expr.calldatasize | Expr.returndataSize | Expr.localVar _ | Expr.arrayLength _
@@ -366,7 +366,7 @@ termination_by es => sizeOf es
 decreasing_by all_goals simp_wf; all_goals omega
 
 def stmtUsesArrayElement : Stmt → Bool
-  | Stmt.letVar _ value | Stmt.assignVar _ value | Stmt.setStorage _ value | Stmt.setStorageAddr _ value
+  | Stmt.letVar _ value | Stmt.assignVar _ value | Stmt.setStorage _ value | Stmt.setStorageAddr _ value | Stmt.setImmutable _ value
   | Stmt.setStorageWord _ _ value | Stmt.storageArrayPush _ value
   | Stmt.return value | Stmt.require value _ =>
       exprUsesArrayElement value
@@ -549,7 +549,7 @@ def exprUsesParamDynamicHeadWord : Expr → Bool
   | Expr.ite a b c =>
       exprUsesParamDynamicHeadWord a || exprUsesParamDynamicHeadWord b ||
       exprUsesParamDynamicHeadWord c
-  | Expr.literal _ | Expr.param _ | Expr.constructorArg _
+  | Expr.literal _ | Expr.param _ | Expr.constructorArg _ | Expr.immutable _
   | Expr.storage _ | Expr.storageAddr _
   | Expr.caller | Expr.contractAddress | Expr.txOrigin | Expr.chainid | Expr.msgValue | Expr.selfBalance
   | Expr.blockTimestamp | Expr.blockNumber | Expr.blobbasefee
@@ -572,7 +572,7 @@ end
 mutual
 def stmtUsesParamDynamicHeadWord : Stmt → Bool
   | Stmt.letVar _ value | Stmt.assignVar _ value | Stmt.setStorage _ value
-  | Stmt.setStorageAddr _ value | Stmt.setStorageWord _ _ value
+  | Stmt.setStorageAddr _ value | Stmt.setImmutable _ value | Stmt.setStorageWord _ _ value
   | Stmt.storageArrayPush _ value | Stmt.return value | Stmt.require value _ =>
       exprUsesParamDynamicHeadWord value
   | Stmt.setStorageArrayElement _ index value =>
@@ -693,7 +693,7 @@ def exprUsesMulDiv512 : Expr → Bool
       exprUsesMulDiv512 thenExpr || exprUsesMulDiv512 elseExpr
   | Expr.mulDivDown a b c | Expr.mulDivUp a b c | Expr.ite a b c =>
       exprUsesMulDiv512 a || exprUsesMulDiv512 b || exprUsesMulDiv512 c
-  | Expr.literal _ | Expr.param _ | Expr.constructorArg _
+  | Expr.literal _ | Expr.param _ | Expr.constructorArg _ | Expr.immutable _
   | Expr.storage _ | Expr.storageAddr _
   | Expr.caller | Expr.contractAddress | Expr.txOrigin | Expr.chainid | Expr.msgValue | Expr.selfBalance
   | Expr.blockTimestamp | Expr.blockNumber | Expr.blobbasefee
@@ -722,7 +722,7 @@ end
 mutual
 def stmtUsesMulDiv512 : Stmt → Bool
   | Stmt.letVar _ value | Stmt.assignVar _ value | Stmt.setStorage _ value
-  | Stmt.setStorageAddr _ value | Stmt.setStorageWord _ _ value
+  | Stmt.setStorageAddr _ value | Stmt.setImmutable _ value | Stmt.setStorageWord _ _ value
   | Stmt.storageArrayPush _ value | Stmt.return value | Stmt.require value _ =>
       exprUsesMulDiv512 value
   | Stmt.setStorageArrayElement _ index value =>
@@ -862,7 +862,7 @@ def exprUsesStorageArrayElement : Expr → Bool
       exprUsesStorageArrayElement cond || exprUsesStorageArrayElement thenVal || exprUsesStorageArrayElement elseVal
   | Expr.adtConstruct _ _ args => exprListUsesStorageArrayElement args
   | Expr.adtField _ _ _ _ _ => false
-  | Expr.literal _ | Expr.param _ | Expr.constructorArg _ | Expr.storage _ | Expr.storageAddr _
+  | Expr.literal _ | Expr.param _ | Expr.constructorArg _ | Expr.immutable _ | Expr.storage _ | Expr.storageAddr _
   | Expr.caller | Expr.contractAddress | Expr.txOrigin | Expr.chainid | Expr.msgValue | Expr.selfBalance | Expr.blockTimestamp
   | Expr.blockNumber | Expr.blobbasefee
   | Expr.calldatasize | Expr.returndataSize | Expr.localVar _ | Expr.arrayLength _
@@ -893,7 +893,7 @@ termination_by es => sizeOf es
 decreasing_by all_goals simp_wf; all_goals omega
 
 def stmtUsesStorageArrayElement : Stmt → Bool
-  | Stmt.letVar _ value | Stmt.assignVar _ value | Stmt.setStorage _ value | Stmt.setStorageAddr _ value
+  | Stmt.letVar _ value | Stmt.assignVar _ value | Stmt.setStorage _ value | Stmt.setStorageAddr _ value | Stmt.setImmutable _ value
   | Stmt.setStorageWord _ _ value |
     Stmt.storageArrayPush _ value |
     Stmt.return value | Stmt.require value _ =>
@@ -1029,7 +1029,7 @@ def exprUsesDynamicBytesEq : Expr → Bool
       exprUsesDynamicBytesEq cond || exprUsesDynamicBytesEq thenVal || exprUsesDynamicBytesEq elseVal
   | Expr.adtConstruct _ _ args => exprListUsesDynamicBytesEq args
   | Expr.adtField _ _ _ _ _ => false
-  | Expr.literal _ | Expr.param _ | Expr.constructorArg _ | Expr.storage _ | Expr.storageAddr _
+  | Expr.literal _ | Expr.param _ | Expr.constructorArg _ | Expr.immutable _ | Expr.storage _ | Expr.storageAddr _
   | Expr.caller | Expr.contractAddress | Expr.txOrigin | Expr.chainid | Expr.msgValue | Expr.selfBalance | Expr.blockTimestamp
   | Expr.blockNumber | Expr.blobbasefee
   | Expr.calldatasize | Expr.returndataSize | Expr.localVar _ | Expr.arrayLength _
@@ -1052,7 +1052,7 @@ termination_by es => sizeOf es
 decreasing_by all_goals simp_wf; all_goals omega
 
 def stmtUsesDynamicBytesEq : Stmt → Bool
-  | Stmt.letVar _ value | Stmt.assignVar _ value | Stmt.setStorage _ value | Stmt.setStorageAddr _ value
+  | Stmt.letVar _ value | Stmt.assignVar _ value | Stmt.setStorage _ value | Stmt.setStorageAddr _ value | Stmt.setImmutable _ value
   | Stmt.setStorageWord _ _ value
   | Stmt.storageArrayPush _ value
   | Stmt.return value | Stmt.require value _ =>

Compiler/CompilationModel/Validation.lean

@@ -70,6 +70,76 @@ private def validateAdtPayloadParamNameCollisions
       throw s!"Compilation error: {context} reserves generated ADT payload local '{name}'. Rename the parameter or local binding that conflicts with generated '<param>_f<i>' locals."
   | none => pure ()
 
+private def immutableNames (immutables : List ImmutableSpec) : List String :=
+  immutables.map (·.name)
+
+private def validateModelImmutableExprNameNode (names : List String)
+    (context : String) : Expr → Except String Unit
+  | Expr.immutable name =>
+      if names.contains name then
+        pure ()
+      else
+        throw s!"Compilation error: {context} references unknown immutable '{name}'"
+  | _ => pure ()
+
+private def validateModelImmutableStmtNode (names : List String)
+    (context : String) : Stmt → Except String Unit
+  | stmt => do
+      match stmt with
+      | Stmt.setImmutable name _ =>
+          if names.contains name then
+            pure ()
+          else
+            throw s!"Compilation error: {context} sets unknown immutable '{name}'"
+      | _ => pure ()
+      for expr in stmt.directMetadata.subexpressions do
+        expr.checkRec (validateModelImmutableExprNameNode names context)
+
+private def validateSetImmutableRuntimeGuardNode (fnName : String) : Stmt → Except String Unit
+  | Stmt.setImmutable name _ =>
+      throw s!"Compilation error: function '{fnName}' uses Stmt.setImmutable for immutable '{name}' outside constructor scope"
+  | _ => pure ()
+
+def validateSetImmutableRuntimeGuard (fn : FunctionSpec) : Except String Unit :=
+  Stmt.checkRecList (validateSetImmutableRuntimeGuardNode fn.name) fn.body
+
+def validateImmutableNamesInFunction (immutables : List ImmutableSpec)
+    (fn : FunctionSpec) : Except String Unit :=
+  Stmt.checkRecList (validateModelImmutableStmtNode (immutableNames immutables) s!"function '{fn.name}'") fn.body
+
+def validateImmutableNamesInConstructor (immutables : List ImmutableSpec)
+    (ctor : Option ConstructorSpec) : Except String Unit := do
+  let names := immutableNames immutables
+  match ctor with
+  | none => pure ()
+  | some spec =>
+      for imm in immutables do
+        imm.init.checkRec (validateModelImmutableExprNameNode names s!"immutable '{imm.name}' initializer")
+      Stmt.checkRecList (validateModelImmutableStmtNode names "constructor") spec.body
+
+/-- Each declared immutable must be assigned via `Stmt.setImmutable` in the
+    constructor body; deploy code only emits `setimmutable` from those
+    statements (never from `ImmutableSpec.init`), so an unset immutable would
+    read uninitialized bytecode at runtime. -/
+def validateImmutableInitialization (immutables : List ImmutableSpec)
+    (ctor : Option ConstructorSpec) : Except String Unit := do
+  match immutables with
+  | [] => pure ()
+  | _ =>
+      match ctor with
+      | none =>
+          throw "Compilation error: contract declares immutables but has no constructor to initialize them"
+      | some spec =>
+          for imm in immutables do
+            let isSet := Stmt.foldBoolList
+              (fun s => match s with
+                | Stmt.setImmutable name _ => name == imm.name
+                | _ => false) spec.body
+            if isSet then
+              pure ()
+            else
+              throw s!"Compilation error: immutable '{imm.name}' is declared but never initialized in the constructor"
+
 def isStorageWordArrayParam : ParamType → Bool
   | ty => isWordArrayParam ty
 
@@ -654,7 +724,7 @@ def matchBranchesMayContainExternalCall (branches : List (String × List String
     statement bodies are reached via the canonical `Stmt.anyDeep`. -/
 def stmtReadsStateOrEnvNode : Stmt → Bool
   | Stmt.letVar _ value | Stmt.assignVar _ value | Stmt.setStorage _ value | Stmt.setStorageAddr _ value
-  | Stmt.setStorageWord _ _ value |
+  | Stmt.setImmutable _ value | Stmt.setStorageWord _ _ value |
     Stmt.return value | Stmt.require value _ =>
       exprReadsStateOrEnv value
   | Stmt.storageArrayPush _ _ | Stmt.setStorageArrayElement _ _ _ | Stmt.storageArrayPop _ =>
@@ -824,7 +894,7 @@ def stmtReadsStateOrEnvWithFunctionEffectsNode
       (lookupFunctionEffect effects name).readsStateOrEnv ||
         exprListReadsStateOrEnvWithFunctionEffects effects args
   | Stmt.letVar _ value | Stmt.assignVar _ value | Stmt.setStorage _ value | Stmt.setStorageAddr _ value
-  | Stmt.setStorageWord _ _ value |
+  | Stmt.setImmutable _ value | Stmt.setStorageWord _ _ value |
     Stmt.return value | Stmt.require value _ =>
       exprReadsStateOrEnvWithFunctionEffects effects value
   | Stmt.storageArrayPush _ _ | Stmt.setStorageArrayElement _ _ _ | Stmt.storageArrayPop _ =>
@@ -1104,7 +1174,7 @@ def validateNoUnsupportedAdtConstructNode : Stmt → Except String Unit
       else
         pure ()
   | Stmt.letVar _ value | Stmt.assignVar _ value | Stmt.setStorage _ value
-  | Stmt.setStorageAddr _ value | Stmt.setStorageWord _ _ value | Stmt.storageArrayPush _ value
+  | Stmt.setStorageAddr _ value | Stmt.setImmutable _ value | Stmt.setStorageWord _ _ value | Stmt.storageArrayPush _ value
   | Stmt.setStorageArrayElement _ _ value | Stmt.setMapping _ _ value
   | Stmt.setMappingUint _ _ value | Stmt.setMappingWord _ _ _ value
   | Stmt.setMapping2 _ _ _ value | Stmt.setMapping2Word _ _ _ _ value

Compiler/CompilationModel/ValidationHelpers.lean

@@ -38,6 +38,7 @@ def collectExprNames : Expr → List String
   | Expr.literal _ => []
   | Expr.param name => [name]
   | Expr.constructorArg _ => []
+  | Expr.immutable name => [name]
   | Expr.storage field | Expr.storageAddr field => [field]
   | Expr.mapping field key => field :: collectExprNames key
   | Expr.mappingWord field key _ => field :: collectExprNames key
@@ -155,7 +156,8 @@ mutual
 def collectStmtNames : Stmt → List String
   | Stmt.letVar name value => name :: collectExprNames value
   | Stmt.assignVar name value => name :: collectExprNames value
-  | Stmt.setStorage _ value | Stmt.setStorageAddr _ value | Stmt.setStorageWord _ _ value =>
+  | Stmt.setStorage _ value | Stmt.setStorageAddr _ value | Stmt.setImmutable _ value
+  | Stmt.setStorageWord _ _ value =>
       collectExprNames value
   | Stmt.storageArrayPush _ value => collectExprNames value
   | Stmt.storageArrayPop _ => []

Compiler/CompilationModel/ValidationInterop.lean

@@ -126,7 +126,7 @@ def validateInteropExpr (context : String) : Expr → Except String Unit
   -- not have to enumerate the complement of every pattern above. This avoids
   -- the `_mutual.eq_def` 200 000-heartbeat ceiling when new `Expr`
   -- constructors land (e.g. verity#1832's `paramDynamicHeadWord`).
-  | Expr.literal _ | Expr.param _ | Expr.constructorArg _
+  | Expr.literal _ | Expr.param _ | Expr.constructorArg _ | Expr.immutable _
   | Expr.storage _ | Expr.storageAddr _
   | Expr.caller | Expr.blockTimestamp | Expr.blockNumber
   | Expr.localVar _