diff --git a/Compiler/CompilationModel/Compile.lean b/Compiler/CompilationModel/Compile.lean index e57d8ce90..bec1c0fc0 100644 --- a/Compiler/CompilationModel/Compile.lean +++ b/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 diff --git a/Compiler/CompilationModel/Dispatch.lean b/Compiler/CompilationModel/Dispatch.lean index 18022ca9c..6ece048ae 100644 --- a/Compiler/CompilationModel/Dispatch.lean +++ b/Compiler/CompilationModel/Dispatch.lean @@ -398,6 +398,8 @@ 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 @@ -405,6 +407,7 @@ private def validateCompileInputsBeforeFieldWriteConflict 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." diff --git a/Compiler/CompilationModel/ExpressionCompile.lean b/Compiler/CompilationModel/ExpressionCompile.lean index 20403a33e..9bd7464d8 100644 --- a/Compiler/CompilationModel/ExpressionCompile.lean +++ b/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" diff --git a/Compiler/CompilationModel/LayoutReport.lean b/Compiler/CompilationModel/LayoutReport.lean index 33785cd22..a9fa33bcd 100644 --- a/Compiler/CompilationModel/LayoutReport.lean +++ b/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)), diff --git a/Compiler/CompilationModel/ScopeValidation.lean b/Compiler/CompilationModel/ScopeValidation.lean index 9755385b5..608ee7794 100644 --- a/Compiler/CompilationModel/ScopeValidation.lean +++ b/Compiler/CompilationModel/ScopeValidation.lean @@ -91,7 +91,7 @@ def dynamicParamBases (params : List Param) : List String := mutual def validateScopedExprIdentifiers (context : String) (params : List Param) (paramScope : List String) (dynamicParams : List String) - (localScope : List String) (constructorArgCount : Option Nat) : Expr → Except String Unit + (immutableNames : List String) (localScope : List String) (constructorArgCount : Option Nat) : Expr → Except String Unit | Expr.param name => if paramScope.contains name then pure () @@ -106,6 +106,11 @@ def validateScopedExprIdentifiers throw s!"Compilation error: constructor Expr.constructorArg {idx} is out of bounds for {count} constructor parameter(s)" | none => throw s!"Compilation error: {context} uses Expr.constructorArg outside constructor scope" + | Expr.immutable name => + if immutableNames.isEmpty || immutableNames.contains name then + pure () + else + throw s!"Compilation error: {context} references unknown immutable '{name}'" | Expr.localVar name => if localScope.contains name then pure () @@ -126,7 +131,7 @@ def validateScopedExprIdentifiers | Expr.storageArrayLength _ => pure () | Expr.storageArrayElement _ index => do - validateScopedExprIdentifiers context params paramScope dynamicParams localScope constructorArgCount index + validateScopedExprIdentifiers context params paramScope dynamicParams immutableNames localScope constructorArgCount index | Expr.arrayElement name index => do match findParamType params name with | some ty@(ParamType.array elemTy) => @@ -138,13 +143,13 @@ def validateScopedExprIdentifiers throw s!"Compilation error: {context} Expr.arrayElement '{name}' requires array parameter, got {repr ty}" | none => throw s!"Compilation error: {context} references unknown parameter '{name}' in Expr.arrayElement" - validateScopedExprIdentifiers context params paramScope dynamicParams localScope constructorArgCount index + validateScopedExprIdentifiers context params paramScope dynamicParams immutableNames localScope constructorArgCount index | Expr.memoryArrayElement name index => do if localScope.contains s!"{name}_data_offset" && localScope.contains s!"{name}_length" then pure () else throw s!"Compilation error: {context} Expr.memoryArrayElement '{name}' requires local bindings '{name}_data_offset' and '{name}_length'" - validateScopedExprIdentifiers context params paramScope dynamicParams localScope constructorArgCount index + validateScopedExprIdentifiers context params paramScope dynamicParams immutableNames localScope constructorArgCount index | Expr.arrayElementWord name index elementWords wordOffset => do if elementWords == 0 then throw s!"Compilation error: {context} Expr.arrayElementWord '{name}' requires elementWords > 0" @@ -164,7 +169,7 @@ def validateScopedExprIdentifiers throw s!"Compilation error: {context} Expr.arrayElementWord '{name}' requires array parameter, got {repr ty}" | none => throw s!"Compilation error: {context} references unknown parameter '{name}' in Expr.arrayElementWord" - validateScopedExprIdentifiers context params paramScope dynamicParams localScope constructorArgCount index + validateScopedExprIdentifiers context params paramScope dynamicParams immutableNames localScope constructorArgCount index | Expr.arrayElementDynamicWord name index wordOffset => do match findParamType params name with | some ty@(ParamType.array elemTy) => @@ -180,7 +185,7 @@ def validateScopedExprIdentifiers throw s!"Compilation error: {context} Expr.arrayElementDynamicWord '{name}' requires array parameter, got {repr ty}" | none => throw s!"Compilation error: {context} references unknown parameter '{name}' in Expr.arrayElementDynamicWord" - validateScopedExprIdentifiers context params paramScope dynamicParams localScope constructorArgCount index + validateScopedExprIdentifiers context params paramScope dynamicParams immutableNames localScope constructorArgCount index | Expr.arrayElementDynamicDataOffset name index => do match findParamType params name with | some ty@(ParamType.array elemTy) => @@ -192,7 +197,7 @@ def validateScopedExprIdentifiers throw s!"Compilation error: {context} Expr.arrayElementDynamicDataOffset '{name}' requires array parameter, got {repr ty}" | none => throw s!"Compilation error: {context} references unknown parameter '{name}' in Expr.arrayElementDynamicDataOffset" - validateScopedExprIdentifiers context params paramScope dynamicParams localScope constructorArgCount index + validateScopedExprIdentifiers context params paramScope dynamicParams immutableNames localScope constructorArgCount index | Expr.arrayElementDynamicMemberLength name index wordOffset => do match findParamType params name with | some ty@(ParamType.array elemTy) => @@ -208,7 +213,7 @@ def validateScopedExprIdentifiers throw s!"Compilation error: {context} Expr.arrayElementDynamicMemberLength '{name}' requires array parameter, got {repr ty}" | none => throw s!"Compilation error: {context} references unknown parameter '{name}' in Expr.arrayElementDynamicMemberLength" - validateScopedExprIdentifiers context params paramScope dynamicParams localScope constructorArgCount index + validateScopedExprIdentifiers context params paramScope dynamicParams immutableNames localScope constructorArgCount index | Expr.arrayElementDynamicMemberDataOffset name index wordOffset => do match findParamType params name with | some ty@(ParamType.array elemTy) => @@ -224,7 +229,7 @@ def validateScopedExprIdentifiers throw s!"Compilation error: {context} Expr.arrayElementDynamicMemberDataOffset '{name}' requires array parameter, got {repr ty}" | none => throw s!"Compilation error: {context} references unknown parameter '{name}' in Expr.arrayElementDynamicMemberDataOffset" - validateScopedExprIdentifiers context params paramScope dynamicParams localScope constructorArgCount index + validateScopedExprIdentifiers context params paramScope dynamicParams immutableNames localScope constructorArgCount index | Expr.arrayElementDynamicMemberElement name index wordOffset innerIndex => do match findParamType params name with | some ty@(ParamType.array elemTy) => @@ -240,8 +245,8 @@ def validateScopedExprIdentifiers throw s!"Compilation error: {context} Expr.arrayElementDynamicMemberElement '{name}' requires array parameter, got {repr ty}" | none => throw s!"Compilation error: {context} references unknown parameter '{name}' in Expr.arrayElementDynamicMemberElement" - validateScopedExprIdentifiers context params paramScope dynamicParams localScope constructorArgCount index - validateScopedExprIdentifiers context params paramScope dynamicParams localScope constructorArgCount innerIndex + validateScopedExprIdentifiers context params paramScope dynamicParams immutableNames localScope constructorArgCount index + validateScopedExprIdentifiers context params paramScope dynamicParams immutableNames localScope constructorArgCount innerIndex | Expr.paramDynamicHeadWord name wordOffset => do match findParamType params name with | some ty@(ParamType.tuple _) => @@ -303,51 +308,51 @@ def validateScopedExprIdentifiers throw s!"Compilation error: {context} Expr.paramDynamicMemberElement '{name}' requires a tuple parameter, got {repr ty}" | none => throw s!"Compilation error: {context} references unknown parameter '{name}' in Expr.paramDynamicMemberElement" - validateScopedExprIdentifiers context params paramScope dynamicParams localScope constructorArgCount innerIndex + validateScopedExprIdentifiers context params paramScope dynamicParams immutableNames localScope constructorArgCount innerIndex | Expr.mapping _ key | Expr.mappingWord _ key _ | Expr.mappingPackedWord _ key _ _ | Expr.mappingUint _ key | Expr.structMember _ key _ => - validateScopedExprIdentifiers context params paramScope dynamicParams localScope constructorArgCount key + validateScopedExprIdentifiers context params paramScope dynamicParams immutableNames localScope constructorArgCount key | Expr.mappingChain _ keys => - validateScopedExprIdentifiersList context params paramScope dynamicParams localScope constructorArgCount keys + validateScopedExprIdentifiersList context params paramScope dynamicParams immutableNames localScope constructorArgCount keys | Expr.mapping2 _ key1 key2 | Expr.mapping2Word _ key1 key2 _ | Expr.structMember2 _ key1 key2 _ => do - validateScopedExprIdentifiers context params paramScope dynamicParams localScope constructorArgCount key1 - validateScopedExprIdentifiers context params paramScope dynamicParams localScope constructorArgCount key2 + validateScopedExprIdentifiers context params paramScope dynamicParams immutableNames localScope constructorArgCount key1 + validateScopedExprIdentifiers context params paramScope dynamicParams immutableNames localScope constructorArgCount key2 | Expr.call gas target value inOffset inSize outOffset outSize => do - validateScopedExprIdentifiers context params paramScope dynamicParams localScope constructorArgCount gas - validateScopedExprIdentifiers context params paramScope dynamicParams localScope constructorArgCount target - validateScopedExprIdentifiers context params paramScope dynamicParams localScope constructorArgCount value - validateScopedExprIdentifiers context params paramScope dynamicParams localScope constructorArgCount inOffset - validateScopedExprIdentifiers context params paramScope dynamicParams localScope constructorArgCount inSize - validateScopedExprIdentifiers context params paramScope dynamicParams localScope constructorArgCount outOffset - validateScopedExprIdentifiers context params paramScope dynamicParams localScope constructorArgCount outSize + validateScopedExprIdentifiers context params paramScope dynamicParams immutableNames localScope constructorArgCount gas + validateScopedExprIdentifiers context params paramScope dynamicParams immutableNames localScope constructorArgCount target + validateScopedExprIdentifiers context params paramScope dynamicParams immutableNames localScope constructorArgCount value + validateScopedExprIdentifiers context params paramScope dynamicParams immutableNames localScope constructorArgCount inOffset + validateScopedExprIdentifiers context params paramScope dynamicParams immutableNames localScope constructorArgCount inSize + validateScopedExprIdentifiers context params paramScope dynamicParams immutableNames localScope constructorArgCount outOffset + validateScopedExprIdentifiers context params paramScope dynamicParams immutableNames localScope constructorArgCount outSize | Expr.staticcall gas target inOffset inSize outOffset outSize => do - validateScopedExprIdentifiers context params paramScope dynamicParams localScope constructorArgCount gas - validateScopedExprIdentifiers context params paramScope dynamicParams localScope constructorArgCount target - validateScopedExprIdentifiers context params paramScope dynamicParams localScope constructorArgCount inOffset - validateScopedExprIdentifiers context params paramScope dynamicParams localScope constructorArgCount inSize - validateScopedExprIdentifiers context params paramScope dynamicParams localScope constructorArgCount outOffset - validateScopedExprIdentifiers context params paramScope dynamicParams localScope constructorArgCount outSize + validateScopedExprIdentifiers context params paramScope dynamicParams immutableNames localScope constructorArgCount gas + validateScopedExprIdentifiers context params paramScope dynamicParams immutableNames localScope constructorArgCount target + validateScopedExprIdentifiers context params paramScope dynamicParams immutableNames localScope constructorArgCount inOffset + validateScopedExprIdentifiers context params paramScope dynamicParams immutableNames localScope constructorArgCount inSize + validateScopedExprIdentifiers context params paramScope dynamicParams immutableNames localScope constructorArgCount outOffset + validateScopedExprIdentifiers context params paramScope dynamicParams immutableNames localScope constructorArgCount outSize | Expr.delegatecall gas target inOffset inSize outOffset outSize => do - validateScopedExprIdentifiers context params paramScope dynamicParams localScope constructorArgCount gas - validateScopedExprIdentifiers context params paramScope dynamicParams localScope constructorArgCount target - validateScopedExprIdentifiers context params paramScope dynamicParams localScope constructorArgCount inOffset - validateScopedExprIdentifiers context params paramScope dynamicParams localScope constructorArgCount inSize - validateScopedExprIdentifiers context params paramScope dynamicParams localScope constructorArgCount outOffset - validateScopedExprIdentifiers context params paramScope dynamicParams localScope constructorArgCount outSize + validateScopedExprIdentifiers context params paramScope dynamicParams immutableNames localScope constructorArgCount gas + validateScopedExprIdentifiers context params paramScope dynamicParams immutableNames localScope constructorArgCount target + validateScopedExprIdentifiers context params paramScope dynamicParams immutableNames localScope constructorArgCount inOffset + validateScopedExprIdentifiers context params paramScope dynamicParams immutableNames localScope constructorArgCount inSize + validateScopedExprIdentifiers context params paramScope dynamicParams immutableNames localScope constructorArgCount outOffset + validateScopedExprIdentifiers context params paramScope dynamicParams immutableNames localScope constructorArgCount outSize | Expr.extcodesize addr => - validateScopedExprIdentifiers context params paramScope dynamicParams localScope constructorArgCount addr + validateScopedExprIdentifiers context params paramScope dynamicParams immutableNames localScope constructorArgCount addr | Expr.mload offset | Expr.tload offset => - validateScopedExprIdentifiers context params paramScope dynamicParams localScope constructorArgCount offset + validateScopedExprIdentifiers context params paramScope dynamicParams immutableNames localScope constructorArgCount offset | Expr.calldataload offset => - validateScopedExprIdentifiers context params paramScope dynamicParams localScope constructorArgCount offset + validateScopedExprIdentifiers context params paramScope dynamicParams immutableNames localScope constructorArgCount offset | Expr.keccak256 offset size => do - validateScopedExprIdentifiers context params paramScope dynamicParams localScope constructorArgCount offset - validateScopedExprIdentifiers context params paramScope dynamicParams localScope constructorArgCount size + validateScopedExprIdentifiers context params paramScope dynamicParams immutableNames localScope constructorArgCount offset + validateScopedExprIdentifiers context params paramScope dynamicParams immutableNames localScope constructorArgCount size | Expr.returndataOptionalBoolAt outOffset => - validateScopedExprIdentifiers context params paramScope dynamicParams localScope constructorArgCount outOffset + validateScopedExprIdentifiers context params paramScope dynamicParams immutableNames localScope constructorArgCount outOffset | Expr.externalCall _ args | Expr.internalCall _ args => - validateScopedExprIdentifiersList context params paramScope dynamicParams localScope constructorArgCount args + validateScopedExprIdentifiersList context params paramScope dynamicParams immutableNames localScope constructorArgCount args | Expr.dynamicBytesEq lhsName rhsName => do let ensureDynamicParam (name : String) : Except String Unit := do match findParamType params name with @@ -363,38 +368,38 @@ def validateScopedExprIdentifiers Expr.sar a b | Expr.signextend a b | Expr.byte a b | Expr.eq a b | Expr.ge a b | Expr.gt a b | Expr.sgt a b | Expr.lt a b | Expr.slt a b | Expr.le a b | Expr.wMulDown a b => do - validateScopedExprIdentifiers context params paramScope dynamicParams localScope constructorArgCount a - validateScopedExprIdentifiers context params paramScope dynamicParams localScope constructorArgCount b + validateScopedExprIdentifiers context params paramScope dynamicParams immutableNames localScope constructorArgCount a + validateScopedExprIdentifiers context params paramScope dynamicParams immutableNames localScope constructorArgCount b | Expr.intrinsic _ _ _ args => - validateScopedExprIdentifiersList context params paramScope dynamicParams localScope constructorArgCount args + validateScopedExprIdentifiersList context params paramScope dynamicParams immutableNames localScope constructorArgCount args | Expr.forkIfAtLeast _ thenExpr elseExpr => do - validateScopedExprIdentifiers context params paramScope dynamicParams localScope constructorArgCount thenExpr - validateScopedExprIdentifiers context params paramScope dynamicParams localScope constructorArgCount elseExpr + validateScopedExprIdentifiers context params paramScope dynamicParams immutableNames localScope constructorArgCount thenExpr + validateScopedExprIdentifiers context params paramScope dynamicParams immutableNames localScope constructorArgCount elseExpr | Expr.wDivUp a b => do validateArithDuplicatedOperandPurity context [b] - validateScopedExprIdentifiers context params paramScope dynamicParams localScope constructorArgCount a - validateScopedExprIdentifiers context params paramScope dynamicParams localScope constructorArgCount b + validateScopedExprIdentifiers context params paramScope dynamicParams immutableNames localScope constructorArgCount a + validateScopedExprIdentifiers context params paramScope dynamicParams immutableNames localScope constructorArgCount b | Expr.min a b | Expr.max a b => do validateArithDuplicatedOperandPurity context [a, b] - validateScopedExprIdentifiers context params paramScope dynamicParams localScope constructorArgCount a - validateScopedExprIdentifiers context params paramScope dynamicParams localScope constructorArgCount b + validateScopedExprIdentifiers context params paramScope dynamicParams immutableNames localScope constructorArgCount a + validateScopedExprIdentifiers context params paramScope dynamicParams immutableNames localScope constructorArgCount b | Expr.ceilDiv a b => do validateArithDuplicatedOperandPurity context [a] - validateScopedExprIdentifiers context params paramScope dynamicParams localScope constructorArgCount a - validateScopedExprIdentifiers context params paramScope dynamicParams localScope constructorArgCount b + validateScopedExprIdentifiers context params paramScope dynamicParams immutableNames localScope constructorArgCount a + validateScopedExprIdentifiers context params paramScope dynamicParams immutableNames localScope constructorArgCount b | Expr.mulDivDown a b c => do - validateScopedExprIdentifiers context params paramScope dynamicParams localScope constructorArgCount a - validateScopedExprIdentifiers context params paramScope dynamicParams localScope constructorArgCount b - validateScopedExprIdentifiers context params paramScope dynamicParams localScope constructorArgCount c + validateScopedExprIdentifiers context params paramScope dynamicParams immutableNames localScope constructorArgCount a + validateScopedExprIdentifiers context params paramScope dynamicParams immutableNames localScope constructorArgCount b + validateScopedExprIdentifiers context params paramScope dynamicParams immutableNames localScope constructorArgCount c | Expr.mulDivUp a b c => do validateArithDuplicatedOperandPurity context [c] - validateScopedExprIdentifiers context params paramScope dynamicParams localScope constructorArgCount a - validateScopedExprIdentifiers context params paramScope dynamicParams localScope constructorArgCount b - validateScopedExprIdentifiers context params paramScope dynamicParams localScope constructorArgCount c + validateScopedExprIdentifiers context params paramScope dynamicParams immutableNames localScope constructorArgCount a + validateScopedExprIdentifiers context params paramScope dynamicParams immutableNames localScope constructorArgCount b + validateScopedExprIdentifiers context params paramScope dynamicParams immutableNames localScope constructorArgCount c | Expr.mulDiv512Down a b c => do - validateScopedExprIdentifiers context params paramScope dynamicParams localScope constructorArgCount a - validateScopedExprIdentifiers context params paramScope dynamicParams localScope constructorArgCount b - validateScopedExprIdentifiers context params paramScope dynamicParams localScope constructorArgCount c + validateScopedExprIdentifiers context params paramScope dynamicParams immutableNames localScope constructorArgCount a + validateScopedExprIdentifiers context params paramScope dynamicParams immutableNames localScope constructorArgCount b + validateScopedExprIdentifiers context params paramScope dynamicParams immutableNames localScope constructorArgCount c | Expr.mulDiv512Up a b c => do -- Unlike `mulDivUp` (which inlines `cc` twice in the emitted Yul), -- `mulDiv512Up` lowers to a single function call @@ -402,23 +407,23 @@ def validateScopedExprIdentifiers -- evaluated exactly once at the call site. The `denominator` -- duplication only exists between the helper's local copies, so we -- do NOT need `validateArithDuplicatedOperandPurity` here. (verity#1761) - validateScopedExprIdentifiers context params paramScope dynamicParams localScope constructorArgCount a - validateScopedExprIdentifiers context params paramScope dynamicParams localScope constructorArgCount b - validateScopedExprIdentifiers context params paramScope dynamicParams localScope constructorArgCount c + validateScopedExprIdentifiers context params paramScope dynamicParams immutableNames localScope constructorArgCount a + validateScopedExprIdentifiers context params paramScope dynamicParams immutableNames localScope constructorArgCount b + validateScopedExprIdentifiers context params paramScope dynamicParams immutableNames localScope constructorArgCount c | Expr.logicalAnd a b | Expr.logicalOr a b => do validateLogicalOperandPurity context a b - validateScopedExprIdentifiers context params paramScope dynamicParams localScope constructorArgCount a - validateScopedExprIdentifiers context params paramScope dynamicParams localScope constructorArgCount b + validateScopedExprIdentifiers context params paramScope dynamicParams immutableNames localScope constructorArgCount a + validateScopedExprIdentifiers context params paramScope dynamicParams immutableNames localScope constructorArgCount b | Expr.bitNot a | Expr.logicalNot a => - validateScopedExprIdentifiers context params paramScope dynamicParams localScope constructorArgCount a + validateScopedExprIdentifiers context params paramScope dynamicParams immutableNames localScope constructorArgCount a | Expr.ite cond thenVal elseVal => do if exprContainsCallLike cond || exprContainsCallLike thenVal || exprContainsCallLike elseVal then throw s!"Compilation error: {context} uses Expr.ite with call-like operand(s), which are eagerly evaluated ({issue748Ref}). Both branches execute regardless of the condition. Move call-like expressions into Stmt.letVar/Stmt.ite before using Expr.ite." - validateScopedExprIdentifiers context params paramScope dynamicParams localScope constructorArgCount cond - validateScopedExprIdentifiers context params paramScope dynamicParams localScope constructorArgCount thenVal - validateScopedExprIdentifiers context params paramScope dynamicParams localScope constructorArgCount elseVal + validateScopedExprIdentifiers context params paramScope dynamicParams immutableNames localScope constructorArgCount cond + validateScopedExprIdentifiers context params paramScope dynamicParams immutableNames localScope constructorArgCount thenVal + validateScopedExprIdentifiers context params paramScope dynamicParams immutableNames localScope constructorArgCount elseVal | Expr.adtConstruct _ _ args => - validateScopedExprIdentifiersList context params paramScope dynamicParams localScope constructorArgCount args + validateScopedExprIdentifiersList context params paramScope dynamicParams immutableNames localScope constructorArgCount args | Expr.adtTag _ _ => pure () | Expr.adtField _ _ _ _ _ => @@ -432,19 +437,19 @@ decreasing_by all_goals simp_wf; all_goals omega def validateScopedExprIdentifiersList (context : String) (params : List Param) (paramScope : List String) (dynamicParams : List String) - (localScope : List String) (constructorArgCount : Option Nat) : List Expr → Except String Unit + (immutableNames : List String) (localScope : List String) (constructorArgCount : Option Nat) : List Expr → Except String Unit | [] => pure () | e :: es => do - validateScopedExprIdentifiers context params paramScope dynamicParams localScope constructorArgCount e - validateScopedExprIdentifiersList context params paramScope dynamicParams localScope constructorArgCount es + validateScopedExprIdentifiers context params paramScope dynamicParams immutableNames localScope constructorArgCount e + validateScopedExprIdentifiersList context params paramScope dynamicParams immutableNames localScope constructorArgCount es termination_by es => sizeOf es decreasing_by all_goals simp_wf; all_goals omega def validateScopedStmtIdentifiers (context : String) (params : List Param) (paramScope : List String) (dynamicParams : List String) - (localScope : List String) (constructorArgCount : Option Nat) : Stmt → Except String (List String) + (immutableNames : List String) (localScope : List String) (constructorArgCount : Option Nat) : Stmt → Except String (List String) | Stmt.letVar name value => do - validateScopedExprIdentifiers context params paramScope dynamicParams localScope constructorArgCount value + validateScopedExprIdentifiers context params paramScope dynamicParams immutableNames localScope constructorArgCount value if paramScope.contains name then throw s!"Compilation error: {context} declares local variable '{name}' that shadows a parameter" if localScope.contains name then @@ -453,98 +458,109 @@ def validateScopedStmtIdentifiers | Stmt.assignVar name value => do if !localScope.contains name then throw s!"Compilation error: {context} assigns to undeclared local variable '{name}'" - validateScopedExprIdentifiers context params paramScope dynamicParams localScope constructorArgCount value + validateScopedExprIdentifiers context params paramScope dynamicParams immutableNames localScope constructorArgCount value pure localScope | Stmt.setStorage _ value | Stmt.setStorageAddr _ value | Stmt.setStorageWord _ _ value | Stmt.return value | Stmt.require value _ => do - validateScopedExprIdentifiers context params paramScope dynamicParams localScope constructorArgCount value + validateScopedExprIdentifiers context params paramScope dynamicParams immutableNames localScope constructorArgCount value + pure localScope + | Stmt.setImmutable name value => do + match constructorArgCount with + | some _ => pure () + | none => + throw s!"Compilation error: {context} uses Stmt.setImmutable '{name}' outside constructor scope" + if immutableNames.isEmpty || immutableNames.contains name then + pure () + else + throw s!"Compilation error: {context} sets unknown immutable '{name}'" + validateScopedExprIdentifiers context params paramScope dynamicParams immutableNames localScope constructorArgCount value pure localScope | Stmt.storageArrayPush _ value => do - validateScopedExprIdentifiers context params paramScope dynamicParams localScope constructorArgCount value + validateScopedExprIdentifiers context params paramScope dynamicParams immutableNames localScope constructorArgCount value pure localScope | Stmt.storageArrayPop _ => pure localScope | Stmt.setStorageArrayElement _ index value => do - validateScopedExprIdentifiers context params paramScope dynamicParams localScope constructorArgCount index - validateScopedExprIdentifiers context params paramScope dynamicParams localScope constructorArgCount value + validateScopedExprIdentifiers context params paramScope dynamicParams immutableNames localScope constructorArgCount index + validateScopedExprIdentifiers context params paramScope dynamicParams immutableNames localScope constructorArgCount value pure localScope | Stmt.setMapping _ key value | Stmt.setMappingWord _ key _ value | Stmt.setMappingPackedWord _ key _ _ value | Stmt.setMappingUint _ key value | Stmt.setStructMember _ key _ value => do - validateScopedExprIdentifiers context params paramScope dynamicParams localScope constructorArgCount key - validateScopedExprIdentifiers context params paramScope dynamicParams localScope constructorArgCount value + validateScopedExprIdentifiers context params paramScope dynamicParams immutableNames localScope constructorArgCount key + validateScopedExprIdentifiers context params paramScope dynamicParams immutableNames localScope constructorArgCount value pure localScope | Stmt.setMappingChain _ keys value => do - validateScopedExprIdentifiersList context params paramScope dynamicParams localScope constructorArgCount keys - validateScopedExprIdentifiers context params paramScope dynamicParams localScope constructorArgCount value + validateScopedExprIdentifiersList context params paramScope dynamicParams immutableNames localScope constructorArgCount keys + validateScopedExprIdentifiers context params paramScope dynamicParams immutableNames localScope constructorArgCount value pure localScope | Stmt.setMapping2 _ key1 key2 value | Stmt.setMapping2Word _ key1 key2 _ value | Stmt.setStructMember2 _ key1 key2 _ value => do - validateScopedExprIdentifiers context params paramScope dynamicParams localScope constructorArgCount key1 - validateScopedExprIdentifiers context params paramScope dynamicParams localScope constructorArgCount key2 - validateScopedExprIdentifiers context params paramScope dynamicParams localScope constructorArgCount value + validateScopedExprIdentifiers context params paramScope dynamicParams immutableNames localScope constructorArgCount key1 + validateScopedExprIdentifiers context params paramScope dynamicParams immutableNames localScope constructorArgCount key2 + validateScopedExprIdentifiers context params paramScope dynamicParams immutableNames localScope constructorArgCount value pure localScope | Stmt.requireError cond _ args => do - validateScopedExprIdentifiers context params paramScope dynamicParams localScope constructorArgCount cond - validateScopedExprIdentifiersList context params paramScope dynamicParams localScope constructorArgCount args + validateScopedExprIdentifiers context params paramScope dynamicParams immutableNames localScope constructorArgCount cond + validateScopedExprIdentifiersList context params paramScope dynamicParams immutableNames localScope constructorArgCount args pure localScope | Stmt.revertError _ args | Stmt.emit _ args | Stmt.returnValues args => do - validateScopedExprIdentifiersList context params paramScope dynamicParams localScope constructorArgCount args + validateScopedExprIdentifiersList context params paramScope dynamicParams immutableNames localScope constructorArgCount args pure localScope | Stmt.mstore offset value => do - validateScopedExprIdentifiers context params paramScope dynamicParams localScope constructorArgCount offset - validateScopedExprIdentifiers context params paramScope dynamicParams localScope constructorArgCount value + validateScopedExprIdentifiers context params paramScope dynamicParams immutableNames localScope constructorArgCount offset + validateScopedExprIdentifiers context params paramScope dynamicParams immutableNames localScope constructorArgCount value pure localScope | Stmt.tstore offset value => do - validateScopedExprIdentifiers context params paramScope dynamicParams localScope constructorArgCount offset - validateScopedExprIdentifiers context params paramScope dynamicParams localScope constructorArgCount value + validateScopedExprIdentifiers context params paramScope dynamicParams immutableNames localScope constructorArgCount offset + validateScopedExprIdentifiers context params paramScope dynamicParams immutableNames localScope constructorArgCount value pure localScope | Stmt.calldatacopy destOffset sourceOffset size => do - validateScopedExprIdentifiers context params paramScope dynamicParams localScope constructorArgCount destOffset - validateScopedExprIdentifiers context params paramScope dynamicParams localScope constructorArgCount sourceOffset - validateScopedExprIdentifiers context params paramScope dynamicParams localScope constructorArgCount size + validateScopedExprIdentifiers context params paramScope dynamicParams immutableNames localScope constructorArgCount destOffset + validateScopedExprIdentifiers context params paramScope dynamicParams immutableNames localScope constructorArgCount sourceOffset + validateScopedExprIdentifiers context params paramScope dynamicParams immutableNames localScope constructorArgCount size pure localScope | Stmt.returndataCopy destOffset sourceOffset size => do - validateScopedExprIdentifiers context params paramScope dynamicParams localScope constructorArgCount destOffset - validateScopedExprIdentifiers context params paramScope dynamicParams localScope constructorArgCount sourceOffset - validateScopedExprIdentifiers context params paramScope dynamicParams localScope constructorArgCount size + validateScopedExprIdentifiers context params paramScope dynamicParams immutableNames localScope constructorArgCount destOffset + validateScopedExprIdentifiers context params paramScope dynamicParams immutableNames localScope constructorArgCount sourceOffset + validateScopedExprIdentifiers context params paramScope dynamicParams immutableNames localScope constructorArgCount size pure localScope | Stmt.ite cond thenBranch elseBranch => do - validateScopedExprIdentifiers context params paramScope dynamicParams localScope constructorArgCount cond - let _ ← validateScopedStmtListIdentifiers context params paramScope dynamicParams localScope constructorArgCount thenBranch - let _ ← validateScopedStmtListIdentifiers context params paramScope dynamicParams localScope constructorArgCount elseBranch + validateScopedExprIdentifiers context params paramScope dynamicParams immutableNames localScope constructorArgCount cond + let _ ← validateScopedStmtListIdentifiers context params paramScope dynamicParams immutableNames localScope constructorArgCount thenBranch + let _ ← validateScopedStmtListIdentifiers context params paramScope dynamicParams immutableNames localScope constructorArgCount elseBranch pure localScope | Stmt.forEach varName count body => do - validateScopedExprIdentifiers context params paramScope dynamicParams localScope constructorArgCount count - let _ ← validateScopedStmtListIdentifiers context params paramScope dynamicParams (varName :: localScope) constructorArgCount body + validateScopedExprIdentifiers context params paramScope dynamicParams immutableNames localScope constructorArgCount count + let _ ← validateScopedStmtListIdentifiers context params paramScope dynamicParams immutableNames (varName :: localScope) constructorArgCount body pure localScope | Stmt.unsafeBlock _ body => do - let _ ← validateScopedStmtListIdentifiers context params paramScope dynamicParams localScope constructorArgCount body + let _ ← validateScopedStmtListIdentifiers context params paramScope dynamicParams immutableNames localScope constructorArgCount body pure localScope | Stmt.matchAdt _ scrutinee branches => do - validateScopedExprIdentifiers context params paramScope dynamicParams localScope constructorArgCount scrutinee - validateScopedMatchBranches context params paramScope dynamicParams localScope constructorArgCount branches + validateScopedExprIdentifiers context params paramScope dynamicParams immutableNames localScope constructorArgCount scrutinee + validateScopedMatchBranches context params paramScope dynamicParams immutableNames localScope constructorArgCount branches pure localScope | Stmt.internalCall _ args => do - validateScopedExprIdentifiersList context params paramScope dynamicParams localScope constructorArgCount args + validateScopedExprIdentifiersList context params paramScope dynamicParams immutableNames localScope constructorArgCount args pure localScope | Stmt.internalCallAssign names _ args => do - validateScopedExprIdentifiersList context params paramScope dynamicParams localScope constructorArgCount args + validateScopedExprIdentifiersList context params paramScope dynamicParams immutableNames localScope constructorArgCount args pure (names.reverse ++ localScope) | Stmt.rawLog topics dataOffset dataSize => do - validateScopedExprIdentifiersList context params paramScope dynamicParams localScope constructorArgCount topics - validateScopedExprIdentifiers context params paramScope dynamicParams localScope constructorArgCount dataOffset - validateScopedExprIdentifiers context params paramScope dynamicParams localScope constructorArgCount dataSize + validateScopedExprIdentifiersList context params paramScope dynamicParams immutableNames localScope constructorArgCount topics + validateScopedExprIdentifiers context params paramScope dynamicParams immutableNames localScope constructorArgCount dataOffset + validateScopedExprIdentifiers context params paramScope dynamicParams immutableNames localScope constructorArgCount dataSize pure localScope | Stmt.externalCallBind resultVars _ args => do - validateScopedExprIdentifiersList context params paramScope dynamicParams localScope constructorArgCount args + validateScopedExprIdentifiersList context params paramScope dynamicParams immutableNames localScope constructorArgCount args pure (resultVars.reverse ++ localScope) | Stmt.tryExternalCallBind successVar resultVars _ args => do - validateScopedExprIdentifiersList context params paramScope dynamicParams localScope constructorArgCount args + validateScopedExprIdentifiersList context params paramScope dynamicParams immutableNames localScope constructorArgCount args pure ((successVar :: resultVars).reverse ++ localScope) | Stmt.ecm mod args => do if args.length != mod.numArgs then throw s!"Compilation error: {context} uses ECM '{mod.name}' with {args.length} arguments but it expects {mod.numArgs}" - validateScopedExprIdentifiersList context params paramScope dynamicParams localScope constructorArgCount args + validateScopedExprIdentifiersList context params paramScope dynamicParams immutableNames localScope constructorArgCount args let mut scope := localScope for rv in mod.resultVars do if paramScope.contains rv then @@ -564,7 +580,7 @@ def validateScopedStmtIdentifiers else throw s!"Compilation error: {context} Stmt.returnArray '{name}' requires parameter '{name}' or local bindings '{name}_data_offset' and '{name}_length'" | Stmt.returnCodeData pointer => do - validateScopedExprIdentifiers context params paramScope dynamicParams localScope constructorArgCount pointer + validateScopedExprIdentifiers context params paramScope dynamicParams immutableNames localScope constructorArgCount pointer pure localScope | Stmt.returnBytes _ | Stmt.returnStorageWords _ | Stmt.revertReturndata | Stmt.stop => @@ -586,55 +602,60 @@ decreasing_by all_goals simp_wf; all_goals omega def validateScopedStmtListIdentifiers (context : String) (params : List Param) (paramScope : List String) (dynamicParams : List String) - (localScope : List String) (constructorArgCount : Option Nat) : List Stmt → Except String (List String) + (immutableNames : List String) (localScope : List String) (constructorArgCount : Option Nat) : List Stmt → Except String (List String) | [] => pure localScope | stmt :: rest => do - let nextScope ← validateScopedStmtIdentifiers context params paramScope dynamicParams localScope constructorArgCount stmt - validateScopedStmtListIdentifiers context params paramScope dynamicParams nextScope constructorArgCount rest + let nextScope ← validateScopedStmtIdentifiers context params paramScope dynamicParams immutableNames localScope constructorArgCount stmt + validateScopedStmtListIdentifiers context params paramScope dynamicParams immutableNames nextScope constructorArgCount rest termination_by ss => sizeOf ss decreasing_by all_goals simp_wf; all_goals omega def validateScopedMatchBranches (context : String) (params : List Param) (paramScope : List String) (dynamicParams : List String) - (localScope : List String) (constructorArgCount : Option Nat) : + (immutableNames : List String) (localScope : List String) (constructorArgCount : Option Nat) : List (String × List String × List Stmt) → Except String Unit | [] => pure () | (_, varNames, body) :: rest => do let branchScope := varNames.reverse ++ localScope - let _ ← validateScopedStmtListIdentifiers context params paramScope dynamicParams branchScope constructorArgCount body - validateScopedMatchBranches context params paramScope dynamicParams localScope constructorArgCount rest + let _ ← validateScopedStmtListIdentifiers context params paramScope dynamicParams immutableNames branchScope constructorArgCount body + validateScopedMatchBranches context params paramScope dynamicParams immutableNames localScope constructorArgCount rest termination_by bs => sizeOf bs decreasing_by all_goals simp_wf; all_goals omega end -def validateFunctionIdentifierReferences (spec : FunctionSpec) : Except String Unit := do +def validateFunctionIdentifierReferencesWithImmutables + (immutableNames : List String) (spec : FunctionSpec) : Except String Unit := do let _ ← validateScopedStmtListIdentifiers s!"function '{spec.name}'" spec.params (paramScopeNames spec.params) (dynamicParamBases spec.params) + immutableNames [] none spec.body pure () +def validateFunctionIdentifierReferences (spec : FunctionSpec) : Except String Unit := + validateFunctionIdentifierReferencesWithImmutables [] spec + theorem validateScopedStmtListIdentifiers_append_ok_inv {context : String} {params : List Param} - {paramScope dynamicParams localScope : List String} + {paramScope dynamicParams immutableNames localScope : List String} {constructorArgCount : Option Nat} {pre post : List Stmt} {finalScope : List String} (hvalidate : validateScopedStmtListIdentifiers - context params paramScope dynamicParams localScope constructorArgCount + context params paramScope dynamicParams immutableNames localScope constructorArgCount (pre ++ post) = Except.ok finalScope) : ∃ midScope, validateScopedStmtListIdentifiers - context params paramScope dynamicParams localScope constructorArgCount + context params paramScope dynamicParams immutableNames localScope constructorArgCount pre = Except.ok midScope ∧ validateScopedStmtListIdentifiers - context params paramScope dynamicParams midScope constructorArgCount + context params paramScope dynamicParams immutableNames midScope constructorArgCount post = Except.ok finalScope := by induction pre generalizing localScope with | nil => @@ -646,7 +667,7 @@ theorem validateScopedStmtListIdentifiers_append_ok_inv simp [validateScopedStmtListIdentifiers] at hvalidate cases hnext : validateScopedStmtIdentifiers - context params paramScope dynamicParams localScope constructorArgCount stmt with + context params paramScope dynamicParams immutableNames localScope constructorArgCount stmt with | error err => simp [hnext] at hvalidate cases hvalidate @@ -660,26 +681,26 @@ theorem validateScopedStmtListIdentifiers_append_ok_inv theorem validateScopedStmtListIdentifiers_cons_ok_inv {context : String} {params : List Param} - {paramScope dynamicParams localScope : List String} + {paramScope dynamicParams immutableNames localScope : List String} {constructorArgCount : Option Nat} {stmt : Stmt} {rest : List Stmt} {finalScope : List String} (hvalidate : validateScopedStmtListIdentifiers - context params paramScope dynamicParams localScope constructorArgCount + context params paramScope dynamicParams immutableNames localScope constructorArgCount (stmt :: rest) = Except.ok finalScope) : ∃ nextScope, validateScopedStmtIdentifiers - context params paramScope dynamicParams localScope constructorArgCount + context params paramScope dynamicParams immutableNames localScope constructorArgCount stmt = Except.ok nextScope ∧ validateScopedStmtListIdentifiers - context params paramScope dynamicParams nextScope constructorArgCount + context params paramScope dynamicParams immutableNames nextScope constructorArgCount rest = Except.ok finalScope := by simp [validateScopedStmtListIdentifiers] at hvalidate cases hnext : validateScopedStmtIdentifiers - context params paramScope dynamicParams localScope constructorArgCount stmt with + context params paramScope dynamicParams immutableNames localScope constructorArgCount stmt with | error err => simp [hnext] at hvalidate cases hvalidate @@ -691,16 +712,16 @@ theorem validateScopedStmtListIdentifiers_cons_ok_inv theorem validateScopedStmtListIdentifiers_singleton_ok_inv {context : String} {params : List Param} - {paramScope dynamicParams localScope : List String} + {paramScope dynamicParams immutableNames localScope : List String} {constructorArgCount : Option Nat} {stmt : Stmt} {finalScope : List String} (hvalidate : validateScopedStmtListIdentifiers - context params paramScope dynamicParams localScope constructorArgCount + context params paramScope dynamicParams immutableNames localScope constructorArgCount [stmt] = Except.ok finalScope) : validateScopedStmtIdentifiers - context params paramScope dynamicParams localScope constructorArgCount + context params paramScope dynamicParams immutableNames localScope constructorArgCount stmt = Except.ok finalScope := by rcases validateScopedStmtListIdentifiers_cons_ok_inv hvalidate with ⟨nextScope, hstmt, hnil⟩ @@ -721,9 +742,10 @@ theorem validateFunctionIdentifierReferences_prefix_ok (paramScopeNames spec.params) (dynamicParamBases spec.params) [] + [] none pre = Except.ok localScope := by - unfold validateFunctionIdentifierReferences at hvalidate + unfold validateFunctionIdentifierReferences validateFunctionIdentifierReferencesWithImmutables at hvalidate rw [hbody] at hvalidate cases hscoped : validateScopedStmtListIdentifiers @@ -732,6 +754,7 @@ theorem validateFunctionIdentifierReferences_prefix_ok (paramScopeNames spec.params) (dynamicParamBases spec.params) [] + [] none (pre ++ post) with | error err => @@ -756,6 +779,7 @@ theorem validateFunctionIdentifierReferences_prefix_stmt_ok (paramScopeNames spec.params) (dynamicParamBases spec.params) [] + [] none pre = Except.ok localScope ∧ validateScopedStmtIdentifiers @@ -763,6 +787,7 @@ theorem validateFunctionIdentifierReferences_prefix_stmt_ok spec.params (paramScopeNames spec.params) (dynamicParamBases spec.params) + [] localScope none stmt = Except.ok nextScope := by @@ -774,6 +799,7 @@ theorem validateFunctionIdentifierReferences_prefix_stmt_ok (paramScopeNames spec.params) (dynamicParamBases spec.params) [] + [] none (pre ++ stmt :: []) = Except.ok midScope := by have hbody' : spec.body = (pre ++ stmt :: []) ++ post := by @@ -791,6 +817,7 @@ theorem validateFunctionIdentifierReferences_prefix_stmt_ok spec.params (paramScopeNames spec.params) (dynamicParamBases spec.params) + [] localScope none stmt with @@ -801,7 +828,8 @@ theorem validateFunctionIdentifierReferences_prefix_stmt_ok refine ⟨localScope, nextScope, hprefixOnly, ?_⟩ simp [hnext] -def validateConstructorIdentifierReferences (ctor : Option ConstructorSpec) : Except String Unit := do +def validateConstructorIdentifierReferencesWithImmutables + (immutableNames : List String) (ctor : Option ConstructorSpec) : Except String Unit := do match ctor with | none => pure () | some spec => @@ -810,9 +838,13 @@ def validateConstructorIdentifierReferences (ctor : Option ConstructorSpec) : Ex spec.params (paramScopeNames spec.params) (dynamicParamBases spec.params) + immutableNames [] (some spec.params.length) spec.body pure () +def validateConstructorIdentifierReferences (ctor : Option ConstructorSpec) : Except String Unit := + validateConstructorIdentifierReferencesWithImmutables [] ctor + end Compiler.CompilationModel diff --git a/Compiler/CompilationModel/TrustSurface.lean b/Compiler/CompilationModel/TrustSurface.lean index 6feef4db6..f6a98c84d 100644 --- a/Compiler/CompilationModel/TrustSurface.lean +++ b/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 diff --git a/Compiler/CompilationModel/UsageAnalysis.lean b/Compiler/CompilationModel/UsageAnalysis.lean index 3c78c9861..f1cba7970 100644 --- a/Compiler/CompilationModel/UsageAnalysis.lean +++ b/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 _ => diff --git a/Compiler/CompilationModel/Validation.lean b/Compiler/CompilationModel/Validation.lean index 8ba9090e5..847f36d72 100644 --- a/Compiler/CompilationModel/Validation.lean +++ b/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 '_f' 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 diff --git a/Compiler/CompilationModel/ValidationHelpers.lean b/Compiler/CompilationModel/ValidationHelpers.lean index bf7a86619..d4587a81d 100644 --- a/Compiler/CompilationModel/ValidationHelpers.lean +++ b/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 _ => [] diff --git a/Compiler/CompilationModel/ValidationInterop.lean b/Compiler/CompilationModel/ValidationInterop.lean index c9c97457c..358f3c53f 100644 --- a/Compiler/CompilationModel/ValidationInterop.lean +++ b/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 _ diff --git a/Compiler/CompilationModelFeatureTest.lean b/Compiler/CompilationModelFeatureTest.lean index ed7a213b0..202ea5ecf 100644 --- a/Compiler/CompilationModelFeatureTest.lean +++ b/Compiler/CompilationModelFeatureTest.lean @@ -1788,33 +1788,28 @@ verity_contract MacroTypedImmutable where function domainSeparator () : Bytes32 := do return domainTag -def specIncludesInternalImmutableFields : Bool := - MacroImmutable.spec.fields.map (·.name) == - ["owner", "__immutable_seededSupply", "__immutable_treasury"] +def specKeepsImmutablesOutOfStorageFields : Bool := + MacroImmutable.spec.fields.map (·.name) == ["owner"] && + MacroImmutable.spec.immutables.map (·.name) == ["seededSupply", "treasury"] -example : specIncludesInternalImmutableFields = true := by native_decide - -def constructorSeedsInternalImmutableSlots : Bool := +def constructorSeedsBytecodeImmutables : Bool := match MacroImmutable.spec.constructor with | some ctor => match ctor.body with - | [Stmt.setStorage "__immutable_seededSupply" + | [Stmt.setImmutable "seededSupply" (Expr.add (Expr.param "seed") (Expr.literal 2)), - Stmt.setStorageAddr "__immutable_treasury" (Expr.param "ownerSeed"), + Stmt.setImmutable "treasury" (Expr.param "ownerSeed"), Stmt.setStorageAddr "owner" (Expr.param "ownerSeed")] => true | _ => false | none => false -example : constructorSeedsInternalImmutableSlots = true := by native_decide - -def runtimeFunctionsLoadImmutableValuesFromState : Bool := - match MacroImmutable.supplyCap Verity.defaultState, MacroImmutable.treasuryAddr Verity.defaultState with - | .success 0 _, .success treasury _ => treasury == zeroAddress +def runtimeFunctionsUseImmutableExpressions : Bool := + match MacroImmutable.supplyCap_modelBody, MacroImmutable.treasuryAddr_modelBody with + | [Stmt.return (Expr.immutable "seededSupply")], + [Stmt.return (Expr.immutable "treasury")] => true | _, _ => false -example : runtimeFunctionsLoadImmutableValuesFromState = true := by native_decide - def functionParamsStillShadowImmutableNames : Bool := match MacroImmutable.shadowed 91 Verity.defaultState with | .success value _ => value == 91 @@ -1827,51 +1822,40 @@ def implicitConstructorCreatedForImmutableInitializers : Bool := | some ctor => ctor.params.isEmpty && match ctor.body with - | [Stmt.setStorage "__immutable_feeScale" (Expr.literal 10000)] => true + | [Stmt.setImmutable "feeScale" (Expr.literal 10000)] => true | _ => false | none => false -example : implicitConstructorCreatedForImmutableInitializers = true := by native_decide - -def implicitImmutableExecutableReadsRuntimeSlot : Bool := - match MacroImplicitImmutable.getFeeScale Verity.defaultState with - | .success value _ => value == 0 +def implicitImmutableFunctionUsesImmutableExpression : Bool := + match MacroImplicitImmutable.getFeeScale_modelBody with + | [Stmt.return (Expr.immutable "feeScale")] => true | _ => false -example : implicitImmutableExecutableReadsRuntimeSlot = true := by native_decide +def typedImmutableSpecUsesImmutableSurface : Bool := + MacroTypedImmutable.spec.fields.isEmpty && + MacroTypedImmutable.spec.immutables.map (fun imm => (imm.name, imm.ty)) == + [("paused", ParamType.bool), ("feeBps", ParamType.uint8), ("domainTag", ParamType.bytes32)] -def typedImmutableSpecUsesWordBackedHiddenSlots : Bool := - match MacroTypedImmutable.spec.fields.map (fun f => (f.name, f.ty)) with - | [("__immutable_paused", FieldType.uint256), - ("__immutable_feeBps", FieldType.uint256), - ("__immutable_domainTag", FieldType.uint256)] => true - | _ => false - -example : typedImmutableSpecUsesWordBackedHiddenSlots = true := by native_decide - -def typedImmutableConstructorSeedsWordSlots : Bool := +def typedImmutableConstructorSeedsBytecodeValues : Bool := match MacroTypedImmutable.spec.constructor with | some ctor => ctor.params.isEmpty && match ctor.body with - | [Stmt.setStorage "__immutable_paused" (Expr.literal 1), - Stmt.setStorage "__immutable_feeBps" (Expr.literal 7), - Stmt.setStorage "__immutable_domainTag" (Expr.literal 42)] => true + | [Stmt.setImmutable "paused" (Expr.literal 1), + Stmt.setImmutable "feeBps" (Expr.literal 7), + Stmt.setImmutable "domainTag" (Expr.literal 42)] => true | _ => false | none => false -example : typedImmutableConstructorSeedsWordSlots = true := by native_decide - -def typedImmutableExecutableReadsConvertedValues : Bool := - match MacroTypedImmutable.isPaused Verity.defaultState, - MacroTypedImmutable.feeScale Verity.defaultState, - MacroTypedImmutable.domainSeparator Verity.defaultState with - | .success paused _, .success feeBps _, .success domainTag _ => - paused = false && feeBps == 0 && domainTag == 0 +def typedImmutableFunctionsUseImmutableExpressions : Bool := + match MacroTypedImmutable.isPaused_modelBody, + MacroTypedImmutable.feeScale_modelBody, + MacroTypedImmutable.domainSeparator_modelBody with + | [Stmt.return (Expr.immutable "paused")], + [Stmt.return (Expr.immutable "feeBps")], + [Stmt.return (Expr.immutable "domainTag")] => true | _, _, _ => false -example : typedImmutableExecutableReadsConvertedValues = true := by native_decide - end MacroImmutableSmoke namespace MacroStructDestructuringSmoke @@ -2594,6 +2578,36 @@ private def duplicateInternalNameSpec : CompilationModel := { ] } +private def duplicateImmutableNameSpec : CompilationModel := { + name := "DuplicateImmutableName" + fields := [] + «immutables» := [ + { name := "cap", ty := ParamType.uint256, init := Expr.literal 1 }, + { name := "cap", ty := ParamType.uint256, init := Expr.literal 2 } + ] + «constructor» := none + functions := [] +} + +private def uninitializedImmutableSpec : CompilationModel := { + name := "UninitializedImmutable" + fields := [] + «immutables» := [ + { name := "cap", ty := ParamType.uint256, init := Expr.literal 1 } + ] + «constructor» := some { + params := [] + body := [Stmt.stop] + } + functions := [ + { name := "load" + params := [] + returnType := some FieldType.uint256 + body := [Stmt.return (Expr.immutable "cap")] + } + ] +} + private def internalExternalNameCollisionSpec : CompilationModel := { name := "InternalExternalNameCollision" fields := [] @@ -5262,6 +5276,14 @@ set_option maxRecDepth 4096 in "same-name internal helpers are rejected before Yul lowering" duplicateInternalNameSpec "duplicate internal function name 'helper'" + expectCompileErrorContains + "same-name immutables are rejected before Yul lowering" + duplicateImmutableNameSpec + "duplicate immutable name 'cap'" + expectCompileErrorContains + "declared immutables left unset by the constructor are rejected" + uninitializedImmutableSpec + "immutable 'cap' is declared but never initialized in the constructor" expectCompileErrorContains "internal helper source names cannot collide with external dispatch names" internalExternalNameCollisionSpec @@ -5367,14 +5389,14 @@ set_option maxRecDepth 4096 in "macro reinitializer executable path advances the tracked version" MacroInitializerSmoke.reinitializerExecutableAdvancesVersion expectTrue - "macro immutable spec includes internal hidden fields" - MacroImmutableSmoke.specIncludesInternalImmutableFields + "macro immutable spec keeps immutables out of storage fields" + MacroImmutableSmoke.specKeepsImmutablesOutOfStorageFields expectTrue - "macro immutable constructor seeds internal slots before user code" - MacroImmutableSmoke.constructorSeedsInternalImmutableSlots + "macro immutable constructor seeds bytecode immutables before user code" + MacroImmutableSmoke.constructorSeedsBytecodeImmutables expectTrue - "macro immutable executable path loads runtime slot values" - MacroImmutableSmoke.runtimeFunctionsLoadImmutableValuesFromState + "macro immutable model path reads immutable expressions" + MacroImmutableSmoke.runtimeFunctionsUseImmutableExpressions expectTrue "macro immutable function parameters still shadow immutable names" MacroImmutableSmoke.functionParamsStillShadowImmutableNames @@ -5382,17 +5404,17 @@ set_option maxRecDepth 4096 in "macro immutables synthesize a constructor when needed" MacroImmutableSmoke.implicitConstructorCreatedForImmutableInitializers expectTrue - "macro synthesized immutable constructor reads runtime storage on the executable path" - MacroImmutableSmoke.implicitImmutableExecutableReadsRuntimeSlot + "macro synthesized immutable function reads immutable expressions" + MacroImmutableSmoke.implicitImmutableFunctionUsesImmutableExpression expectTrue - "macro typed immutables lower to word-backed hidden slots in the spec" - MacroImmutableSmoke.typedImmutableSpecUsesWordBackedHiddenSlots + "macro typed immutables lower to the immutable spec surface" + MacroImmutableSmoke.typedImmutableSpecUsesImmutableSurface expectTrue - "macro typed immutables seed word-backed hidden slots in the constructor" - MacroImmutableSmoke.typedImmutableConstructorSeedsWordSlots + "macro typed immutables seed bytecode immutable values in the constructor" + MacroImmutableSmoke.typedImmutableConstructorSeedsBytecodeValues expectTrue - "macro typed immutables convert executable runtime reads back to source types" - MacroImmutableSmoke.typedImmutableExecutableReadsConvertedValues + "macro typed immutables read immutable expressions" + MacroImmutableSmoke.typedImmutableFunctionsUseImmutableExpressions expectTrue "macro emit lowers to Stmt.emit" MacroEventTraceSmoke.emitNamedModelUsesStmtEmit expectTrue "macro event declarations populate CompilationModel event metadata" diff --git a/Compiler/CompileDriverCommon.lean b/Compiler/CompileDriverCommon.lean index 60e7e53cd..5ab07621b 100644 --- a/Compiler/CompileDriverCommon.lean +++ b/Compiler/CompileDriverCommon.lean @@ -321,7 +321,7 @@ private def specializeForkSpec private partial def collectIntrinsicUsesStmt : Stmt → List IntrinsicUse | .letVar _ value | .assignVar _ value | .setStorage _ value - | .setStorageAddr _ value | .setStorageWord _ _ value + | .setStorageAddr _ value | .setImmutable _ value | .setStorageWord _ _ value | .storageArrayPush _ value | .return value | .require value _ => collectIntrinsicUsesExpr value | .setStorageArrayElement _ index value diff --git a/Compiler/CompileDriverTest.lean b/Compiler/CompileDriverTest.lean index c73f3b52e..f2bf124a7 100644 --- a/Compiler/CompileDriverTest.lean +++ b/Compiler/CompileDriverTest.lean @@ -68,6 +68,43 @@ private def abiSmokeSpec : CompilationModel := { ] } +private def runtimeSetImmutableSpec : CompilationModel := { + name := "RuntimeSetImmutable" + fields := [] + «immutables» := [ + { name := "owner", ty := ParamType.address, init := Expr.literal 0 } + ] + «constructor» := none + functions := [ + { name := "setOwner" + params := [{ name := "next", ty := ParamType.address }] + returnType := none + body := [ + Stmt.setImmutable "owner" (Expr.param "next"), + Stmt.stop + ] + } + ] +} + +private def unknownImmutableReadSpec : CompilationModel := { + name := "UnknownImmutableRead" + fields := [] + «immutables» := [ + { name := "owner", ty := ParamType.address, init := Expr.literal 0 } + ] + «constructor» := none + functions := [ + { name := "owner" + params := [] + returnType := some FieldType.address + body := [ + Stmt.return (Expr.immutable "owenr") + ] + } + ] +} + private def futureForkIntrinsicSpec : CompilationModel := { name := "FutureForkIntrinsicSmoke" fields := [] @@ -1217,6 +1254,20 @@ unsafe def runTests : IO Unit := do try IO.FS.removeFile earlySuccessfulAbi catch _ => pure () + expectFailureContains + "validateCompileInputs rejects setImmutable in runtime function body" + (match validateCompileInputs runtimeSetImmutableSpec [0] with + | Except.ok _ => pure () + | Except.error err => throw (IO.userError err)) + "uses Stmt.setImmutable 'owner' outside constructor scope" + + expectFailureContains + "validateCompileInputs rejects unknown immutable reads" + (match validateCompileInputs unknownImmutableReadSpec [0] with + | Except.ok _ => pure () + | Except.error err => throw (IO.userError err)) + "references unknown immutable 'owenr'" + expectFailureContains "compileSpecsWithOptions reports missing linked library" (compileSpecsWithOptions [abiSmokeSpec, linkedLibrarySpec] outDir false [missingLib] {} none none none (some abiDir)) diff --git a/Compiler/Proofs/EndToEnd/Base.lean b/Compiler/Proofs/EndToEnd/Base.lean index b5f097183..14c93cae9 100644 --- a/Compiler/Proofs/EndToEnd/Base.lean +++ b/Compiler/Proofs/EndToEnd/Base.lean @@ -5252,6 +5252,9 @@ theorem supportedStmtList_safe_of_state_effect_closed | setStorageAddrSingleSlot hValue _ hFind => exact Compiler.Proofs.YulGeneration.Backends.bridgedSafeStmts_setStorageAddrSingleSlot_of_exprCompileCore (errors := errors) (dynamicSource := dynamicSource) hValue hFind + | setImmutableSingle _ _ => + simp [stmtListTouchesUnsupportedEffectSurface, + stmtTouchesUnsupportedEffectSurface] at hEffects | mstoreSingle hOffset _ hValue _ => exact Compiler.Proofs.YulGeneration.Backends.bridgedSafeStmts_mstoreSingle_of_exprCompileCore (fields := fields) (errors := errors) (dynamicSource := dynamicSource) @@ -5413,6 +5416,9 @@ theorem supportedStmtList_safe_of_state_except_mapping_writes_stmt_safety | setStorageAddrSingleSlot hValue _ hFind => exact Compiler.Proofs.YulGeneration.Backends.bridgedSafeStmts_setStorageAddrSingleSlot_of_exprCompileCore (errors := errors) (dynamicSource := dynamicSource) hValue hFind + | setImmutableSingle _ _ => + simp [stmtListTouchesUnsupportedEffectSurface, + stmtTouchesUnsupportedEffectSurface] at hEffects | mstoreSingle hOffset _ hValue _ => exact Compiler.Proofs.YulGeneration.Backends.bridgedSafeStmts_mstoreSingle_of_exprCompileCore (fields := fields) (errors := errors) (dynamicSource := dynamicSource) diff --git a/Compiler/Proofs/GeneratedTransition.lean b/Compiler/Proofs/GeneratedTransition.lean index a382ded47..509652858 100644 --- a/Compiler/Proofs/GeneratedTransition.lean +++ b/Compiler/Proofs/GeneratedTransition.lean @@ -76,6 +76,8 @@ mutual private partial def stmtSummary : Stmt → TransitionSummary | .setStorage field value | .setStorageAddr field value => { reads := dedup (exprReads value), writes := [field] } + | .setImmutable name value => + { reads := dedup (exprReads value), writes := ["immutable:" ++ name] } | .setStorageWord field offset value => { reads := dedup (exprReads value), writes := [field ++ "+" ++ toString offset] } | .storageArrayPush field value => diff --git a/Compiler/Proofs/IRGeneration/DenoteAgreement.lean b/Compiler/Proofs/IRGeneration/DenoteAgreement.lean index 8310ca950..1bb06481d 100644 --- a/Compiler/Proofs/IRGeneration/DenoteAgreement.lean +++ b/Compiler/Proofs/IRGeneration/DenoteAgreement.lean @@ -33,11 +33,14 @@ def sourceOracle : DenoteOracle := /-- The state conversion is field-for-field (the two structures coincide). -/ def toRuntimeState (s : DenoteState) : SourceSemantics.RuntimeState := - { world := s.world, bindings := s.bindings, selector := s.selector } + { world := s.world, immutable := s.immutable, bindings := s.bindings, selector := s.selector } @[simp] theorem toRuntimeState_world (s : DenoteState) : (toRuntimeState s).world = s.world := rfl +@[simp] theorem toRuntimeState_immutable (s : DenoteState) : + (toRuntimeState s).immutable = s.immutable := rfl + @[simp] theorem toRuntimeState_bindings (s : DenoteState) : (toRuntimeState s).bindings = s.bindings := rfl @@ -63,7 +66,7 @@ theorem denote_evalExpr_eq (fields : List Field) (s : DenoteState) : ∀ e : Expr, Denote.evalExpr sourceOracle fields s e = SourceSemantics.evalExpr fields (toRuntimeState s) e - | .literal _ | .param _ | .constructorArg _ | .storage _ | .storageAddr _ + | .literal _ | .param _ | .immutable _ | .constructorArg _ | .storage _ | .storageAddr _ | .mappingChain .. | .localVar _ | .storageArrayLength _ | .dynamicBytesEq .. | .memoryArrayLength _ | .memoryArrayElement .. | .arrayElementDynamicDataOffset .. | .arrayElementDynamicMemberLength .. | .arrayElementDynamicMemberDataOffset .. @@ -321,6 +324,7 @@ theorem execForEachLoop_agree {varName : String} | _, _, 0 => rfl | st, index, remaining + 1 => by have hb := h ⟨st.world, + st.immutable, SourceSemantics.bindValue st.bindings varName (SourceSemantics.wordNormalize index), st.selector⟩ rw [SourceSemantics.execForEachLoop_succ] @@ -328,6 +332,7 @@ theorem execForEachLoop_agree {varName : String} rw [← hb] show toStmtResult (match runBody ⟨st.world, + st.immutable, SourceSemantics.bindValue st.bindings varName (SourceSemantics.wordNormalize index), st.selector⟩ with | .continue next => Denote.execForEachLoop varName runBody next (index + 1) remaining @@ -335,6 +340,7 @@ theorem execForEachLoop_agree {varName : String} | .return value next => .return value next | .revert => .revert) = _ cases runBody ⟨st.world, + st.immutable, SourceSemantics.bindValue st.bindings varName (SourceSemantics.wordNormalize index), st.selector⟩ <;> first @@ -373,7 +379,7 @@ theorem execStmt_eq (fields : List Field) : toStmtResult (Denote.execStmt sourceOracle fields st stmt) = SourceSemantics.execStmt fields (toRuntimeState st) stmt | _, .letVar n v | _, .assignVar n v => by denote_stmt_arm - | _, .setStorage f v | _, .setStorageAddr f v => by denote_stmt_arm + | _, .setStorage f v | _, .setStorageAddr f v | _, .setImmutable f v => by denote_stmt_arm | _, .setStorageWord f w v => by denote_stmt_arm | _, .setMapping f k v | _, .setMappingUint f k v => by denote_stmt_arm | _, .setMappingWord f k w v => by denote_stmt_arm @@ -408,7 +414,7 @@ theorem execStmt_eq (fields : List Field) : exact execForEachLoop_agree (runBody' := fun ls => SourceSemantics.execStmtList fields ls body) (fun ls => execStmtList_eq fields ls body) - ⟨st.world, Denote.bindValue st.bindings v (Denote.wordNormalize 0), st.selector⟩ + ⟨st.world, st.immutable, Denote.bindValue st.bindings v (Denote.wordNormalize 0), st.selector⟩ 0 bound | _, .requireError .. | _, .revertError .. | _, .returnValues .. | _, .returnArray .. | _, .returnBytes .. | _, .returnStorageWords .. diff --git a/Compiler/Proofs/IRGeneration/DenoteFunctionAgreement.lean b/Compiler/Proofs/IRGeneration/DenoteFunctionAgreement.lean index d1b16239e..f3c3952c9 100644 --- a/Compiler/Proofs/IRGeneration/DenoteFunctionAgreement.lean +++ b/Compiler/Proofs/IRGeneration/DenoteFunctionAgreement.lean @@ -200,13 +200,13 @@ theorem denoteFunction_eq | none => simp | some bindings => have hexec := execStmtList_eq (SourceSemantics.effectiveFields spec) - ⟨SourceSemantics.withTransactionContext initialWorld tx, bindings, + ⟨SourceSemantics.withTransactionContext initialWorld tx, fun _ => 0, bindings, tx.functionSelector⟩ fn.body simp only [toRuntimeState] at hexec dsimp only rw [← hexec] cases Denote.execStmtList sourceOracle (SourceSemantics.effectiveFields spec) - ⟨SourceSemantics.withTransactionContext initialWorld tx, bindings, + ⟨SourceSemantics.withTransactionContext initialWorld tx, fun _ => 0, bindings, tx.functionSelector⟩ fn.body <;> simp [toStmtResult, toRuntimeState] diff --git a/Compiler/Proofs/IRGeneration/ExprCore.lean b/Compiler/Proofs/IRGeneration/ExprCore.lean index b53bc2c83..fbd56862b 100644 --- a/Compiler/Proofs/IRGeneration/ExprCore.lean +++ b/Compiler/Proofs/IRGeneration/ExprCore.lean @@ -72,7 +72,7 @@ def exprBoundNames : Expr → List String exprBoundNames thenExpr ++ exprBoundNames elseExpr | .mappingChain _ keys => exprListBoundNames keys | .dynamicBytesEq lhsName rhsName => [lhsName, rhsName] - | .literal _ | .constructorArg _ | .storage _ | .storageAddr _ | .caller + | .literal _ | .constructorArg _ | .immutable _ | .storage _ | .storageAddr _ | .caller | .contractAddress | .chainid | .msgValue | .blockTimestamp | .blockNumber | .selfBalance | .blobbasefee | .calldatasize | .returndataSize | .txOrigin => [] termination_by expr => sizeOf expr diff --git a/Compiler/Proofs/IRGeneration/FunctionBody/Base.lean b/Compiler/Proofs/IRGeneration/FunctionBody/Base.lean index eb09b2030..87d53718a 100644 --- a/Compiler/Proofs/IRGeneration/FunctionBody/Base.lean +++ b/Compiler/Proofs/IRGeneration/FunctionBody/Base.lean @@ -201,7 +201,7 @@ theorem evalIRExpr_ident_of_scope_bindings (hexact : bindingsExactlyMatchIRVarsOnScope scope bindings state) {name : String} (hname : name ∈ scope) : - evalIRExpr state (YulExpr.ident name) = lookupBinding? bindings name := by + evalIRExpr state (YulExpr.ident name) = lookupBinding? bindings name := by simpa [evalIRExpr] using hexact name hname theorem evalIRExpr_caller_of_runtimeStateMatchesIR diff --git a/Compiler/Proofs/IRGeneration/FunctionBody/Stmt.lean b/Compiler/Proofs/IRGeneration/FunctionBody/Stmt.lean index 2f2c1dc96..e817ad5f9 100644 --- a/Compiler/Proofs/IRGeneration/FunctionBody/Stmt.lean +++ b/Compiler/Proofs/IRGeneration/FunctionBody/Stmt.lean @@ -917,7 +917,7 @@ private theorem compileStmt_ok_any_scope_aux rcases hok with ⟨ir, hir⟩ simp [CompilationModel.compileStmt, lookupAdtTypeDef, Except.bind, bind] at hir -- All remaining cases: inScopeNames is unused, so the result is identical - | letVar | assignVar | setStorage | setStorageAddr | setStorageWord | storageArrayPush + | letVar | assignVar | setStorage | setStorageAddr | setImmutable | setStorageWord | storageArrayPush | storageArrayPop | setStorageArrayElement | setMapping | setMappingWord | setMappingPackedWord | setMapping2 | setMapping2Word | setMappingUint | setMappingChain | setStructMember | setStructMember2 | require @@ -1037,7 +1037,7 @@ private theorem compileStmt_ok_any_scope_with_surface_aux | matchAdt adtName scrutinee branches => rcases hok with ⟨ir, hir⟩ simp [CompilationModel.compileStmt, lookupAdtTypeDef, Except.bind, bind] at hir - | letVar | assignVar | setStorage | setStorageAddr | setStorageWord | storageArrayPush + | letVar | assignVar | setStorage | setStorageAddr | setImmutable | setStorageWord | storageArrayPush | storageArrayPop | setStorageArrayElement | setMapping | setMappingWord | setMappingPackedWord | setMapping2 | setMapping2Word | setMappingUint | setMappingChain | setStructMember | setStructMember2 | require diff --git a/Compiler/Proofs/IRGeneration/GenericInduction/Helpers.lean b/Compiler/Proofs/IRGeneration/GenericInduction/Helpers.lean index d3abd55e4..7dcf8c6ee 100644 --- a/Compiler/Proofs/IRGeneration/GenericInduction/Helpers.lean +++ b/Compiler/Proofs/IRGeneration/GenericInduction/Helpers.lean @@ -1567,6 +1567,9 @@ theorem stmtListGenericCore_of_supportedStmtList_of_surface | setStorageAddrSingleSlot hcore hinScope hfind => exact stmtListGenericCore_of_supportedStmtList_setStorageAddrSingleSlot_of_surface (fields := fields) hnoConflict hfind hcore hinScope + | setImmutableSingle _ _ => + simp [stmtListTouchesUnsupportedContractSurface, + stmtTouchesUnsupportedContractSurface] at hsurface | mstoreSingle hcoreOffset hinScopeOffset hcoreValue hinScopeValue => exact stmtListGenericCore_of_supportedStmtList_mstoreSingle_of_surface (fields := fields) hcoreOffset hinScopeOffset hcoreValue hinScopeValue @@ -1668,6 +1671,10 @@ theorem stmtListGenericCore_of_supportedStmtList_of_surface_exceptMappingWrites | setStorageAddrSingleSlot hcore hinScope hfind => exact stmtListGenericCore_of_supportedStmtList_setStorageAddrSingleSlot_of_surface (fields := fields) hnoConflict hfind hcore hinScope + | setImmutableSingle _ _ => + simp [stmtListTouchesUnsupportedContractSurfaceExceptMappingWrites, + stmtTouchesUnsupportedContractSurfaceExceptMappingWrites, + stmtTouchesUnsupportedContractSurface] at hsurface | mstoreSingle hcoreOffset hinScopeOffset hcoreValue hinScopeValue => exact stmtListGenericCore_of_supportedStmtList_mstoreSingle_of_surface (fields := fields) hcoreOffset hinScopeOffset hcoreValue hinScopeValue @@ -1927,6 +1934,10 @@ theorem stmtListGenericCore_of_supportedStmtList_of_surface_exceptMappingWrites_ | setStorageAddrSingleSlot hcore hinScope hfind => exact stmtListGenericCore_of_supportedStmtList_setStorageAddrSingleSlot_of_surface (fields := fields) hnoConflict hfind hcore hinScope + | setImmutableSingle _ _ => + simp [stmtListTouchesUnsupportedContractSurfaceExceptMappingWrites, + stmtTouchesUnsupportedContractSurfaceExceptMappingWrites, + stmtTouchesUnsupportedContractSurface] at hsurface | mstoreSingle hcoreOffset hinScopeOffset hcoreValue hinScopeValue => exact stmtListGenericCore_of_supportedStmtList_mstoreSingle_of_surface (fields := fields) hcoreOffset hinScopeOffset hcoreValue hinScopeValue diff --git a/Compiler/Proofs/IRGeneration/GenericInduction/Scope.lean b/Compiler/Proofs/IRGeneration/GenericInduction/Scope.lean index b248ef071..e32ffa388 100644 --- a/Compiler/Proofs/IRGeneration/GenericInduction/Scope.lean +++ b/Compiler/Proofs/IRGeneration/GenericInduction/Scope.lean @@ -50,6 +50,11 @@ inductive StmtListScopeDiscipline (fieldNames : List String) : List String → L FunctionBody.exprBoundNamesInScope value scope → StmtListScopeDiscipline fieldNames (stmtNextScope scope (.setStorageAddr fieldName value)) rest → StmtListScopeDiscipline fieldNames scope (.setStorageAddr fieldName value :: rest) + | setImmutable {scope : List String} {name : String} {value : Expr} {rest : List Stmt} : + FunctionBody.ExprCompileCore value → + FunctionBody.exprBoundNamesInScope value scope → + StmtListScopeDiscipline fieldNames (stmtNextScope scope (.setImmutable name value)) rest → + StmtListScopeDiscipline fieldNames scope (.setImmutable name value :: rest) | setStorageWord {scope : List String} {fieldName : String} {wordOffset : Nat} {value : Expr} {rest : List Stmt} : fieldName ∈ fieldNames → @@ -121,6 +126,10 @@ inductive StmtListScopeCore (fieldNames : List String) : List Stmt → Prop wher FunctionBody.ExprCompileCore value → StmtListScopeCore fieldNames rest → StmtListScopeCore fieldNames (.setStorageAddr fieldName value :: rest) + | setImmutable {name : String} {value : Expr} {rest : List Stmt} : + FunctionBody.ExprCompileCore value → + StmtListScopeCore fieldNames rest → + StmtListScopeCore fieldNames (.setImmutable name value :: rest) | setStorageWord {fieldName : String} {wordOffset : Nat} {value : Expr} {rest : List Stmt} : fieldName ∈ fieldNames → FunctionBody.ExprCompileCore value → @@ -158,6 +167,7 @@ theorem exprCompileCore_of_exprTouchesUnsupportedContractSurface_eq_false | .literal _, _ => exact .literal _ | .param _, _ => exact .param _ | .localVar _, _ => exact .localVar _ + | .immutable _, hsurface => simp [exprTouchesUnsupportedContractSurface] at hsurface | .caller, _ => exact .caller | .contractAddress, _ => exact .contractAddress | .txOrigin, _ => exact .txOrigin @@ -402,6 +412,10 @@ private theorem stmtListScopeCore_of_unsupportedContractSurface_eq_false exact fieldName_mem_fields_of_compileSetStorage_ok hhead) (exprCompileCore_of_exprTouchesUnsupportedContractSurface_eq_false (by simpa [stmtTouchesUnsupportedContractSurface] using hstmtSurface)) ihRest + | setImmutable name value => + exact .setImmutable + (exprCompileCore_of_exprTouchesUnsupportedContractSurface_eq_false + (by simpa [stmtTouchesUnsupportedContractSurface] using hstmtSurface)) ihRest | setStorageWord fieldName wordOffset value => exact .setStorageWord (by @@ -528,6 +542,11 @@ theorem stmtListScopeCore_prefix_of_compileStmtList_ok_of_stmtListTouchesUnsuppo (exprCompileCore_of_exprTouchesUnsupportedContractSurface_eq_false (by simpa [stmtTouchesUnsupportedContractSurface] using hstmtSurface)) (ih hrestSurface htail) + | setImmutable name value => + exact StmtListScopeCore.setImmutable + (exprCompileCore_of_exprTouchesUnsupportedContractSurface_eq_false + (by simpa [stmtTouchesUnsupportedContractSurface] using hstmtSurface)) + (ih hrestSurface htail) | setStorageWord fieldName wordOffset value => exact StmtListScopeCore.setStorageWord (by @@ -662,22 +681,22 @@ private theorem mem_stmtNextScopeList_of_mem_scope private theorem validateScopedExprIdentifiers_pair_ok_left {context : String} {params : List Param} - {paramScope dynamicParams localScope : List String} + {paramScope dynamicParams immutableNames localScope : List String} {constructorArgCount : Option Nat} {lhs rhs : Expr} (hvalidate : (do validateScopedExprIdentifiers - context params paramScope dynamicParams localScope constructorArgCount lhs + context params paramScope dynamicParams immutableNames localScope constructorArgCount lhs validateScopedExprIdentifiers - context params paramScope dynamicParams localScope constructorArgCount rhs) = + context params paramScope dynamicParams immutableNames localScope constructorArgCount rhs) = Except.ok ()) : validateScopedExprIdentifiers - context params paramScope dynamicParams localScope constructorArgCount lhs = + context params paramScope dynamicParams immutableNames localScope constructorArgCount lhs = Except.ok () := by cases hlhs : validateScopedExprIdentifiers - context params paramScope dynamicParams localScope constructorArgCount lhs with + context params paramScope dynamicParams immutableNames localScope constructorArgCount lhs with | error err => simp [hlhs] at hvalidate cases hvalidate @@ -688,22 +707,22 @@ private theorem validateScopedExprIdentifiers_pair_ok_left private theorem validateScopedExprIdentifiers_pair_ok_right {context : String} {params : List Param} - {paramScope dynamicParams localScope : List String} + {paramScope dynamicParams immutableNames localScope : List String} {constructorArgCount : Option Nat} {lhs rhs : Expr} (hvalidate : (do validateScopedExprIdentifiers - context params paramScope dynamicParams localScope constructorArgCount lhs + context params paramScope dynamicParams immutableNames localScope constructorArgCount lhs validateScopedExprIdentifiers - context params paramScope dynamicParams localScope constructorArgCount rhs) = + context params paramScope dynamicParams immutableNames localScope constructorArgCount rhs) = Except.ok ()) : validateScopedExprIdentifiers - context params paramScope dynamicParams localScope constructorArgCount rhs = + context params paramScope dynamicParams immutableNames localScope constructorArgCount rhs = Except.ok () := by cases hlhs : validateScopedExprIdentifiers - context params paramScope dynamicParams localScope constructorArgCount lhs with + context params paramScope dynamicParams immutableNames localScope constructorArgCount lhs with | error err => simp [hlhs] at hvalidate cases hvalidate @@ -714,13 +733,13 @@ private theorem validateScopedExprIdentifiers_pair_ok_right private theorem exprBoundNamesInScope_of_validateScopedExprIdentifiers_core {context : String} {params : List Param} - {paramScope dynamicParams localScope scope : List String} + {paramScope dynamicParams immutableNames localScope scope : List String} {constructorArgCount : Option Nat} {expr : Expr} (hcore : FunctionBody.ExprCompileCore expr) (hvalidate : validateScopedExprIdentifiers - context params paramScope dynamicParams localScope constructorArgCount expr = + context params paramScope dynamicParams immutableNames localScope constructorArgCount expr = Except.ok ()) (hparamsInScope : ∀ name, name ∈ paramScope → name ∈ scope) (hlocalsInScope : ∀ name, name ∈ localScope → name ∈ scope) : @@ -770,9 +789,9 @@ private theorem exprBoundNamesInScope_of_validateScopedExprIdentifiers_core have hpair : (do validateScopedExprIdentifiers - context params paramScope dynamicParams localScope constructorArgCount lhs + context params paramScope dynamicParams immutableNames localScope constructorArgCount lhs validateScopedExprIdentifiers - context params paramScope dynamicParams localScope constructorArgCount rhs) = + context params paramScope dynamicParams immutableNames localScope constructorArgCount rhs) = Except.ok () := by simpa [validateScopedExprIdentifiers] using hvalidate intro name hmem @@ -797,9 +816,9 @@ private theorem exprBoundNamesInScope_of_validateScopedExprIdentifiers_core have hpair : (do validateScopedExprIdentifiers - context params paramScope dynamicParams localScope constructorArgCount shift + context params paramScope dynamicParams immutableNames localScope constructorArgCount shift validateScopedExprIdentifiers - context params paramScope dynamicParams localScope constructorArgCount value) = + context params paramScope dynamicParams immutableNames localScope constructorArgCount value) = Except.ok () := by simpa [validateScopedExprIdentifiers] using hvalidate intro name hmem @@ -813,9 +832,9 @@ private theorem exprBoundNamesInScope_of_validateScopedExprIdentifiers_core have hpair : (do validateScopedExprIdentifiers - context params paramScope dynamicParams localScope constructorArgCount lhs + context params paramScope dynamicParams immutableNames localScope constructorArgCount lhs validateScopedExprIdentifiers - context params paramScope dynamicParams localScope constructorArgCount rhs) = + context params paramScope dynamicParams immutableNames localScope constructorArgCount rhs) = Except.ok () := by simp only [validateScopedExprIdentifiers] at hvalidate revert hvalidate @@ -833,9 +852,9 @@ private theorem exprBoundNamesInScope_of_validateScopedExprIdentifiers_core have hpair : (do validateScopedExprIdentifiers - context params paramScope dynamicParams localScope constructorArgCount lhs + context params paramScope dynamicParams immutableNames localScope constructorArgCount lhs validateScopedExprIdentifiers - context params paramScope dynamicParams localScope constructorArgCount rhs) = + context params paramScope dynamicParams immutableNames localScope constructorArgCount rhs) = Except.ok () := by simp only [validateScopedExprIdentifiers] at hvalidate revert hvalidate @@ -852,9 +871,9 @@ private theorem exprBoundNamesInScope_of_validateScopedExprIdentifiers_core have hpair : (do validateScopedExprIdentifiers - context params paramScope dynamicParams localScope constructorArgCount lhs + context params paramScope dynamicParams immutableNames localScope constructorArgCount lhs validateScopedExprIdentifiers - context params paramScope dynamicParams localScope constructorArgCount rhs) = + context params paramScope dynamicParams immutableNames localScope constructorArgCount rhs) = Except.ok () := by simpa [validateScopedExprIdentifiers] using hvalidate intro name hmem @@ -867,51 +886,51 @@ private theorem exprBoundNamesInScope_of_validateScopedExprIdentifiers_core have htriple : (do validateScopedExprIdentifiers - context params paramScope dynamicParams localScope constructorArgCount a + context params paramScope dynamicParams immutableNames localScope constructorArgCount a validateScopedExprIdentifiers - context params paramScope dynamicParams localScope constructorArgCount b + context params paramScope dynamicParams immutableNames localScope constructorArgCount b validateScopedExprIdentifiers - context params paramScope dynamicParams localScope constructorArgCount c) = + context params paramScope dynamicParams immutableNames localScope constructorArgCount c) = Except.ok () := by simpa [validateScopedExprIdentifiers] using hvalidate have hA_ok : validateScopedExprIdentifiers - context params paramScope dynamicParams localScope constructorArgCount a = + context params paramScope dynamicParams immutableNames localScope constructorArgCount a = Except.ok () := by revert htriple cases ha : validateScopedExprIdentifiers - context params paramScope dynamicParams localScope constructorArgCount a with + context params paramScope dynamicParams immutableNames localScope constructorArgCount a with | error e => simp [ha, Bind.bind, Except.bind] | ok v => intro; rfl have hB_ok : validateScopedExprIdentifiers - context params paramScope dynamicParams localScope constructorArgCount b = + context params paramScope dynamicParams immutableNames localScope constructorArgCount b = Except.ok () := by revert htriple cases ha : validateScopedExprIdentifiers - context params paramScope dynamicParams localScope constructorArgCount a with + context params paramScope dynamicParams immutableNames localScope constructorArgCount a with | error e => simp [ha, Bind.bind, Except.bind] | ok v => cases hb : validateScopedExprIdentifiers - context params paramScope dynamicParams localScope constructorArgCount b with + context params paramScope dynamicParams immutableNames localScope constructorArgCount b with | error e => simp [ha, hb, Bind.bind, Except.bind] | ok v => intro; rfl have hC_ok : validateScopedExprIdentifiers - context params paramScope dynamicParams localScope constructorArgCount c = + context params paramScope dynamicParams immutableNames localScope constructorArgCount c = Except.ok () := by revert htriple cases ha : validateScopedExprIdentifiers - context params paramScope dynamicParams localScope constructorArgCount a with + context params paramScope dynamicParams immutableNames localScope constructorArgCount a with | error e => simp [ha, Bind.bind, Except.bind] | ok v => cases hb : validateScopedExprIdentifiers - context params paramScope dynamicParams localScope constructorArgCount b with + context params paramScope dynamicParams immutableNames localScope constructorArgCount b with | error e => simp [ha, hb, Bind.bind, Except.bind] | ok v => simp [ha, hb, Bind.bind, Except.bind] @@ -927,11 +946,11 @@ private theorem exprBoundNamesInScope_of_validateScopedExprIdentifiers_core have htriple : (do validateScopedExprIdentifiers - context params paramScope dynamicParams localScope constructorArgCount a + context params paramScope dynamicParams immutableNames localScope constructorArgCount a validateScopedExprIdentifiers - context params paramScope dynamicParams localScope constructorArgCount b + context params paramScope dynamicParams immutableNames localScope constructorArgCount b validateScopedExprIdentifiers - context params paramScope dynamicParams localScope constructorArgCount c) = + context params paramScope dynamicParams immutableNames localScope constructorArgCount c) = Except.ok () := by simp only [validateScopedExprIdentifiers] at hvalidate revert hvalidate @@ -940,42 +959,42 @@ private theorem exprBoundNamesInScope_of_validateScopedExprIdentifiers_core | error e => simp [Bind.bind, Except.bind] have hA_ok : validateScopedExprIdentifiers - context params paramScope dynamicParams localScope constructorArgCount a = + context params paramScope dynamicParams immutableNames localScope constructorArgCount a = Except.ok () := by revert htriple cases ha : validateScopedExprIdentifiers - context params paramScope dynamicParams localScope constructorArgCount a with + context params paramScope dynamicParams immutableNames localScope constructorArgCount a with | error e => simp [ha, Bind.bind, Except.bind] | ok v => intro; rfl have hB_ok : validateScopedExprIdentifiers - context params paramScope dynamicParams localScope constructorArgCount b = + context params paramScope dynamicParams immutableNames localScope constructorArgCount b = Except.ok () := by revert htriple cases ha : validateScopedExprIdentifiers - context params paramScope dynamicParams localScope constructorArgCount a with + context params paramScope dynamicParams immutableNames localScope constructorArgCount a with | error e => simp [ha, Bind.bind, Except.bind] | ok v => cases hb : validateScopedExprIdentifiers - context params paramScope dynamicParams localScope constructorArgCount b with + context params paramScope dynamicParams immutableNames localScope constructorArgCount b with | error e => simp [ha, hb, Bind.bind, Except.bind] | ok v => intro; rfl have hC_ok : validateScopedExprIdentifiers - context params paramScope dynamicParams localScope constructorArgCount c = + context params paramScope dynamicParams immutableNames localScope constructorArgCount c = Except.ok () := by revert htriple cases ha : validateScopedExprIdentifiers - context params paramScope dynamicParams localScope constructorArgCount a with + context params paramScope dynamicParams immutableNames localScope constructorArgCount a with | error e => simp [ha, Bind.bind, Except.bind] | ok v => cases hb : validateScopedExprIdentifiers - context params paramScope dynamicParams localScope constructorArgCount b with + context params paramScope dynamicParams immutableNames localScope constructorArgCount b with | error e => simp [ha, hb, Bind.bind, Except.bind] | ok v => simp [ha, hb, Bind.bind, Except.bind] @@ -990,7 +1009,7 @@ private theorem exprBoundNamesInScope_of_validateScopedExprIdentifiers_core rename_i cond thenVal elseVal have hC_ok : validateScopedExprIdentifiers - context params paramScope dynamicParams localScope constructorArgCount cond = + context params paramScope dynamicParams immutableNames localScope constructorArgCount cond = Except.ok () := by simp only [validateScopedExprIdentifiers] at hvalidate revert hvalidate @@ -1003,12 +1022,12 @@ private theorem exprBoundNamesInScope_of_validateScopedExprIdentifiers_core intro h cases hc : validateScopedExprIdentifiers - context params paramScope dynamicParams localScope constructorArgCount cond with + context params paramScope dynamicParams immutableNames localScope constructorArgCount cond with | error e => simp [hc] at h | ok v => rfl have hT_ok : validateScopedExprIdentifiers - context params paramScope dynamicParams localScope constructorArgCount thenVal = + context params paramScope dynamicParams immutableNames localScope constructorArgCount thenVal = Except.ok () := by simp only [validateScopedExprIdentifiers] at hvalidate revert hvalidate @@ -1021,17 +1040,17 @@ private theorem exprBoundNamesInScope_of_validateScopedExprIdentifiers_core intro h cases hc : validateScopedExprIdentifiers - context params paramScope dynamicParams localScope constructorArgCount cond with + context params paramScope dynamicParams immutableNames localScope constructorArgCount cond with | error e => simp [hc] at h | ok v => cases ht : validateScopedExprIdentifiers - context params paramScope dynamicParams localScope constructorArgCount thenVal with + context params paramScope dynamicParams immutableNames localScope constructorArgCount thenVal with | error e => simp [hc, ht] at h | ok v => rfl have hE_ok : validateScopedExprIdentifiers - context params paramScope dynamicParams localScope constructorArgCount elseVal = + context params paramScope dynamicParams immutableNames localScope constructorArgCount elseVal = Except.ok () := by simp only [validateScopedExprIdentifiers] at hvalidate revert hvalidate @@ -1044,12 +1063,12 @@ private theorem exprBoundNamesInScope_of_validateScopedExprIdentifiers_core intro h cases hc : validateScopedExprIdentifiers - context params paramScope dynamicParams localScope constructorArgCount cond with + context params paramScope dynamicParams immutableNames localScope constructorArgCount cond with | error e => simp [hc] at h | ok v => cases ht : validateScopedExprIdentifiers - context params paramScope dynamicParams localScope constructorArgCount thenVal with + context params paramScope dynamicParams immutableNames localScope constructorArgCount thenVal with | error e => simp [hc, ht] at h | ok v => simpa [hc, ht] using h intro name hmem @@ -1065,9 +1084,9 @@ private theorem exprBoundNamesInScope_of_validateScopedExprIdentifiers_core have hpair : (do validateScopedExprIdentifiers - context params paramScope dynamicParams localScope constructorArgCount lhs + context params paramScope dynamicParams immutableNames localScope constructorArgCount lhs validateScopedExprIdentifiers - context params paramScope dynamicParams localScope constructorArgCount rhs) = + context params paramScope dynamicParams immutableNames localScope constructorArgCount rhs) = Except.ok () := by by_cases hcall : exprContainsCallLike lhs = true ∨ exprContainsCallLike rhs = true · simp [validateScopedExprIdentifiers, validateLogicalOperandPurity, hcall] at hvalidate @@ -1083,14 +1102,14 @@ private theorem stmtListScopeDiscipline_of_validateScopedStmtListIdentifiers {fieldNames : List String} {context : String} {params : List Param} - {paramScope dynamicParams localScope scope : List String} + {paramScope dynamicParams immutableNames localScope scope : List String} {constructorArgCount : Option Nat} {stmts : List Stmt} {finalScope : List String} (hcore : StmtListScopeCore fieldNames stmts) (hvalidate : validateScopedStmtListIdentifiers - context params paramScope dynamicParams localScope constructorArgCount stmts = + context params paramScope dynamicParams immutableNames localScope constructorArgCount stmts = Except.ok finalScope) (hparamsInScope : ∀ name, name ∈ paramScope → name ∈ scope) (hlocalsInScope : ∀ name, name ∈ localScope → name ∈ scope) : @@ -1106,7 +1125,7 @@ private theorem stmtListScopeDiscipline_of_validateScopedStmtListIdentifiers have hstmt' := hstmt unfold validateScopedStmtIdentifiers at hstmt' revert hstmt' - rcases hExprVal : validateScopedExprIdentifiers context params paramScope dynamicParams localScope constructorArgCount _ with _ | _ + rcases hExprVal : validateScopedExprIdentifiers context params paramScope dynamicParams immutableNames localScope constructorArgCount _ with _ | _ · intro h; simp [hExprVal, bind, Except.bind] at h · simp only [hExprVal, bind, Except.bind, pure, Except.pure] intro h @@ -1138,7 +1157,7 @@ private theorem stmtListScopeDiscipline_of_validateScopedStmtListIdentifiers · intro h; simp [bind, Except.bind] at h · intro hstmt' simp only [bind, Except.bind, pure, Except.pure] at hstmt' - rcases hExprVal : validateScopedExprIdentifiers context params paramScope dynamicParams localScope constructorArgCount _ with _ | _ + rcases hExprVal : validateScopedExprIdentifiers context params paramScope dynamicParams immutableNames localScope constructorArgCount _ with _ | _ · rw [hExprVal] at hstmt'; exact absurd hstmt' (by simp) · rw [hExprVal] at hstmt'; simp at hstmt'; cases hstmt' exact StmtListScopeDiscipline.assignVar @@ -1158,7 +1177,7 @@ private theorem stmtListScopeDiscipline_of_validateScopedStmtListIdentifiers have hstmt' := hstmt unfold validateScopedStmtIdentifiers at hstmt' revert hstmt' - rcases hExprVal : validateScopedExprIdentifiers context params paramScope dynamicParams localScope constructorArgCount _ with _ | _ + rcases hExprVal : validateScopedExprIdentifiers context params paramScope dynamicParams immutableNames localScope constructorArgCount _ with _ | _ · intro h; simp [bind, Except.bind] at h · simp only [bind, Except.bind, pure, Except.pure] intro h; cases h @@ -1179,7 +1198,7 @@ private theorem stmtListScopeDiscipline_of_validateScopedStmtListIdentifiers have hstmt' := hstmt unfold validateScopedStmtIdentifiers at hstmt' revert hstmt' - rcases hExprVal : validateScopedExprIdentifiers context params paramScope dynamicParams localScope constructorArgCount _ with _ | _ + rcases hExprVal : validateScopedExprIdentifiers context params paramScope dynamicParams immutableNames localScope constructorArgCount _ with _ | _ · intro h; simp [bind, Except.bind] at h · simp only [bind, Except.bind, pure, Except.pure] intro h; cases h @@ -1209,7 +1228,7 @@ private theorem stmtListScopeDiscipline_of_validateScopedStmtListIdentifiers have hstmt' := hstmt unfold validateScopedStmtIdentifiers at hstmt' revert hstmt' - rcases hExprVal : validateScopedExprIdentifiers context params paramScope dynamicParams localScope constructorArgCount _ with _ | _ + rcases hExprVal : validateScopedExprIdentifiers context params paramScope dynamicParams immutableNames localScope constructorArgCount _ with _ | _ · intro h; simp [bind, Except.bind] at h · simp only [bind, Except.bind, pure, Except.pure] intro h; cases h @@ -1231,7 +1250,7 @@ private theorem stmtListScopeDiscipline_of_validateScopedStmtListIdentifiers have hstmt' := hstmt unfold validateScopedStmtIdentifiers at hstmt' revert hstmt' - rcases hExprVal : validateScopedExprIdentifiers context params paramScope dynamicParams localScope constructorArgCount _ with _ | _ + rcases hExprVal : validateScopedExprIdentifiers context params paramScope dynamicParams immutableNames localScope constructorArgCount _ with _ | _ · intro h; simp [bind, Except.bind] at h · simp only [bind, Except.bind, pure, Except.pure] intro h; cases h @@ -1247,13 +1266,54 @@ private theorem stmtListScopeDiscipline_of_validateScopedStmtListIdentifiers (by intro other hmem exact mem_stmtNextScope_of_mem_scope (hlocalsInScope other hmem))) + | setImmutable hvalueCore hrest ih => + rename_i immName immValue immRest + rcases validateScopedStmtListIdentifiers_cons_ok_inv hvalidate with + ⟨nextLocalScope, hstmt, hrestValidate⟩ + have hstmt' := hstmt + unfold validateScopedStmtIdentifiers at hstmt' + revert hstmt' + rcases hExprVal : + validateScopedExprIdentifiers context params paramScope dynamicParams immutableNames + localScope constructorArgCount _ with _ | _ + · intro h + cases constructorArgCount with + | none => + simp [hExprVal, bind, Except.bind] at h + | some _ => + by_cases himm : immutableNames = [] ∨ immName ∈ immutableNames + · simp [hExprVal, himm, bind, Except.bind] at h + cases h + · simp [hExprVal, himm, bind, Except.bind] at h + cases h + · intro h + cases constructorArgCount with + | none => + simp [hExprVal, bind, Except.bind] at h + | some _ => + by_cases himm : immutableNames = [] ∨ immName ∈ immutableNames + · simp [hExprVal, himm, bind, Except.bind] at h + cases h + exact StmtListScopeDiscipline.setImmutable + hvalueCore + (exprBoundNamesInScope_of_validateScopedExprIdentifiers_core + hvalueCore hExprVal hparamsInScope hlocalsInScope) + (ih hrestValidate + (by + intro other hmem + exact mem_stmtNextScope_of_mem_scope (hparamsInScope other hmem)) + (by + intro other hmem + exact mem_stmtNextScope_of_mem_scope (hlocalsInScope other hmem))) + · simp [hExprVal, himm, bind, Except.bind] at h + cases h | setStorageWord hfield hvalueCore hrest ih => rcases validateScopedStmtListIdentifiers_cons_ok_inv hvalidate with ⟨nextLocalScope, hstmt, hrestValidate⟩ have hstmt' := hstmt unfold validateScopedStmtIdentifiers at hstmt' revert hstmt' - rcases hExprVal : validateScopedExprIdentifiers context params paramScope dynamicParams localScope constructorArgCount _ with _ | _ + rcases hExprVal : validateScopedExprIdentifiers context params paramScope dynamicParams immutableNames localScope constructorArgCount _ with _ | _ · intro h; simp [bind, Except.bind] at h · simp only [bind, Except.bind, pure, Except.pure] intro h; cases h @@ -1276,11 +1336,11 @@ private theorem stmtListScopeDiscipline_of_validateScopedStmtListIdentifiers unfold validateScopedStmtIdentifiers at hstmt' revert hstmt' rcases hOffsetVal : validateScopedExprIdentifiers context params paramScope dynamicParams - localScope constructorArgCount _ with _ | _ + immutableNames localScope constructorArgCount _ with _ | _ · intro h; simp [bind, Except.bind] at h · simp only [hOffsetVal, bind, Except.bind] rcases hValueVal : validateScopedExprIdentifiers context params paramScope dynamicParams - localScope constructorArgCount _ with _ | _ + immutableNames localScope constructorArgCount _ with _ | _ · intro h; simp [hValueVal, bind, Except.bind] at h · simp only [hValueVal, bind, Except.bind, pure, Except.pure] intro h; cases h @@ -1303,11 +1363,11 @@ private theorem stmtListScopeDiscipline_of_validateScopedStmtListIdentifiers unfold validateScopedStmtIdentifiers at hstmt' revert hstmt' rcases hOffsetVal : validateScopedExprIdentifiers context params paramScope dynamicParams - localScope constructorArgCount _ with _ | _ + immutableNames localScope constructorArgCount _ with _ | _ · intro h; simp [bind, Except.bind] at h · simp only [hOffsetVal, bind, Except.bind] rcases hValueVal : validateScopedExprIdentifiers context params paramScope dynamicParams - localScope constructorArgCount _ with _ | _ + immutableNames localScope constructorArgCount _ with _ | _ · intro h; simp [hValueVal, bind, Except.bind] at h · simp only [hValueVal, bind, Except.bind, pure, Except.pure] intro h; cases h @@ -1329,13 +1389,13 @@ private theorem stmtListScopeDiscipline_of_validateScopedStmtListIdentifiers have hstmt' := hstmt unfold validateScopedStmtIdentifiers at hstmt' revert hstmt' - rcases hCondVal : validateScopedExprIdentifiers context params paramScope dynamicParams localScope constructorArgCount _ with _ | _ + rcases hCondVal : validateScopedExprIdentifiers context params paramScope dynamicParams immutableNames localScope constructorArgCount _ with _ | _ · intro h; simp [bind, Except.bind] at h · simp only [bind, Except.bind, pure, Except.pure] - rcases hThenVal : validateScopedStmtListIdentifiers context params paramScope dynamicParams localScope constructorArgCount _ with _ | _ + rcases hThenVal : validateScopedStmtListIdentifiers context params paramScope dynamicParams immutableNames localScope constructorArgCount _ with _ | _ · intro h; simp [hThenVal, bind, Except.bind] at h · simp only [hThenVal, bind, Except.bind] - rcases hElseVal : validateScopedStmtListIdentifiers context params paramScope dynamicParams localScope constructorArgCount _ with _ | _ + rcases hElseVal : validateScopedStmtListIdentifiers context params paramScope dynamicParams immutableNames localScope constructorArgCount _ with _ | _ · intro h; simp [hElseVal, bind, Except.bind] at h · simp only [hElseVal, bind, Except.bind, pure, Except.pure] intro h; cases h @@ -1361,13 +1421,13 @@ private theorem stmtListScopeDiscipline_of_validateScopedStmtListIdentifiers simp only [bind, Except.bind, pure, Except.pure] intro hstmt' rcases hCountVal : - validateScopedExprIdentifiers context params paramScope dynamicParams localScope + validateScopedExprIdentifiers context params paramScope dynamicParams immutableNames localScope constructorArgCount (Expr.literal 0) with _ | _ · rw [hCountVal] at hstmt'; simp at hstmt' · rw [hCountVal] at hstmt' rcases hBodyVal : validateScopedStmtListIdentifiers context params paramScope dynamicParams - (_ :: localScope) constructorArgCount _ with _ | _ + immutableNames (_ :: localScope) constructorArgCount _ with _ | _ · rw [hBodyVal] at hstmt'; simp at hstmt' · rw [hBodyVal] at hstmt'; simp at hstmt'; cases hstmt' exact StmtListScopeDiscipline.forEachLiteralZero @@ -1397,13 +1457,13 @@ private theorem stmtListScopeDiscipline_of_validateScopedStmtListIdentifiers simp only [bind, Except.bind, pure, Except.pure] intro hstmt' rcases hCountVal : - validateScopedExprIdentifiers context params paramScope dynamicParams localScope + validateScopedExprIdentifiers context params paramScope dynamicParams immutableNames localScope constructorArgCount (Expr.literal _) with _ | _ · rw [hCountVal] at hstmt'; simp at hstmt' · rw [hCountVal] at hstmt' rcases hBodyVal : validateScopedStmtListIdentifiers context params paramScope dynamicParams - (_ :: localScope) constructorArgCount [] with _ | _ + immutableNames (_ :: localScope) constructorArgCount [] with _ | _ · rw [hBodyVal] at hstmt'; simp at hstmt' · rw [hBodyVal] at hstmt'; simp at hstmt'; cases hstmt' exact StmtListScopeDiscipline.forEachLiteralEmpty @@ -1442,14 +1502,14 @@ private theorem scopeNamesPresent_foldl_stmtNextScope_of_validateScopedStmtListI {fieldNames : List String} {context : String} {params : List Param} - {paramScope dynamicParams localScope scope : List String} + {paramScope dynamicParams immutableNames localScope scope : List String} {constructorArgCount : Option Nat} {stmts : List Stmt} {finalScope : List String} (hcore : StmtListScopeCore fieldNames stmts) (hvalidate : validateScopedStmtListIdentifiers - context params paramScope dynamicParams localScope constructorArgCount stmts = + context params paramScope dynamicParams immutableNames localScope constructorArgCount stmts = Except.ok finalScope) (hparamsInScope : ∀ name, name ∈ paramScope → name ∈ scope) (hlocalsInScope : ∀ name, name ∈ localScope → name ∈ scope) : @@ -1466,7 +1526,7 @@ private theorem scopeNamesPresent_foldl_stmtNextScope_of_validateScopedStmtListI have hstmt' := hstmt unfold validateScopedStmtIdentifiers at hstmt' revert hstmt' - rcases hExprVal : validateScopedExprIdentifiers context params paramScope dynamicParams localScope constructorArgCount _ with _ | _ + rcases hExprVal : validateScopedExprIdentifiers context params paramScope dynamicParams immutableNames localScope constructorArgCount _ with _ | _ · intro h; simp [bind, Except.bind] at h · simp only [hExprVal, bind, Except.bind, pure, Except.pure] intro h @@ -1495,7 +1555,7 @@ private theorem scopeNamesPresent_foldl_stmtNextScope_of_validateScopedStmtListI · intro h; simp [bind, Except.bind] at h · intro hstmt' simp only [bind, Except.bind, pure, Except.pure] at hstmt' - rcases hExprVal : validateScopedExprIdentifiers context params paramScope dynamicParams localScope constructorArgCount _ with _ | _ + rcases hExprVal : validateScopedExprIdentifiers context params paramScope dynamicParams immutableNames localScope constructorArgCount _ with _ | _ · rw [hExprVal] at hstmt'; exact absurd hstmt' (by simp) · rw [hExprVal] at hstmt'; simp at hstmt'; cases hstmt' intro other hmem @@ -1513,7 +1573,7 @@ private theorem scopeNamesPresent_foldl_stmtNextScope_of_validateScopedStmtListI have hstmt' := hstmt unfold validateScopedStmtIdentifiers at hstmt' revert hstmt' - rcases hExprVal : validateScopedExprIdentifiers context params paramScope dynamicParams localScope constructorArgCount _ with _ | _ + rcases hExprVal : validateScopedExprIdentifiers context params paramScope dynamicParams immutableNames localScope constructorArgCount _ with _ | _ · intro h; simp [bind, Except.bind] at h · simp only [bind, Except.bind, pure, Except.pure] intro h; cases h @@ -1532,7 +1592,7 @@ private theorem scopeNamesPresent_foldl_stmtNextScope_of_validateScopedStmtListI have hstmt' := hstmt unfold validateScopedStmtIdentifiers at hstmt' revert hstmt' - rcases hExprVal : validateScopedExprIdentifiers context params paramScope dynamicParams localScope constructorArgCount _ with _ | _ + rcases hExprVal : validateScopedExprIdentifiers context params paramScope dynamicParams immutableNames localScope constructorArgCount _ with _ | _ · intro h; simp [bind, Except.bind] at h · simp only [bind, Except.bind, pure, Except.pure] intro h; cases h @@ -1561,7 +1621,7 @@ private theorem scopeNamesPresent_foldl_stmtNextScope_of_validateScopedStmtListI have hstmt' := hstmt unfold validateScopedStmtIdentifiers at hstmt' revert hstmt' - rcases hExprVal : validateScopedExprIdentifiers context params paramScope dynamicParams localScope constructorArgCount _ with _ | _ + rcases hExprVal : validateScopedExprIdentifiers context params paramScope dynamicParams immutableNames localScope constructorArgCount _ with _ | _ · intro h; simp [bind, Except.bind] at h · simp only [bind, Except.bind, pure, Except.pure] intro h; cases h @@ -1580,7 +1640,7 @@ private theorem scopeNamesPresent_foldl_stmtNextScope_of_validateScopedStmtListI have hstmt' := hstmt unfold validateScopedStmtIdentifiers at hstmt' revert hstmt' - rcases hExprVal : validateScopedExprIdentifiers context params paramScope dynamicParams localScope constructorArgCount _ with _ | _ + rcases hExprVal : validateScopedExprIdentifiers context params paramScope dynamicParams immutableNames localScope constructorArgCount _ with _ | _ · intro h; simp [bind, Except.bind] at h · simp only [bind, Except.bind, pure, Except.pure] intro h; cases h @@ -1593,13 +1653,52 @@ private theorem scopeNamesPresent_foldl_stmtNextScope_of_validateScopedStmtListI intro name hname exact mem_stmtNextScope_of_mem_scope (hlocalsInScope name hname)) other hmem + | setImmutable hvalueCore hrest ih => + rename_i immName immValue immRest + rcases validateScopedStmtListIdentifiers_cons_ok_inv hvalidate with + ⟨nextLocalScope, hstmt, hrestValidate⟩ + have hstmt' := hstmt + unfold validateScopedStmtIdentifiers at hstmt' + revert hstmt' + rcases hExprVal : + validateScopedExprIdentifiers context params paramScope dynamicParams immutableNames + localScope constructorArgCount _ with _ | _ + · intro h + cases constructorArgCount with + | none => + simp [hExprVal, bind, Except.bind] at h + | some _ => + by_cases himm : immutableNames = [] ∨ immName ∈ immutableNames + · simp [hExprVal, himm, bind, Except.bind] at h + cases h + · simp [hExprVal, himm, bind, Except.bind] at h + cases h + · intro h + cases constructorArgCount with + | none => + simp [hExprVal, bind, Except.bind] at h + | some _ => + by_cases himm : immutableNames = [] ∨ immName ∈ immutableNames + · simp [hExprVal, himm, bind, Except.bind] at h + cases h + intro other hmem + exact ih hrestValidate + (by + intro name hname + exact mem_stmtNextScope_of_mem_scope (hparamsInScope name hname)) + (by + intro name hname + exact mem_stmtNextScope_of_mem_scope (hlocalsInScope name hname)) + other hmem + · simp [hExprVal, himm, bind, Except.bind] at h + cases h | setStorageWord hfield hvalueCore hrest ih => rcases validateScopedStmtListIdentifiers_cons_ok_inv hvalidate with ⟨nextLocalScope, hstmt, hrestValidate⟩ have hstmt' := hstmt unfold validateScopedStmtIdentifiers at hstmt' revert hstmt' - rcases hExprVal : validateScopedExprIdentifiers context params paramScope dynamicParams localScope constructorArgCount _ with _ | _ + rcases hExprVal : validateScopedExprIdentifiers context params paramScope dynamicParams immutableNames localScope constructorArgCount _ with _ | _ · intro h; simp [bind, Except.bind] at h · simp only [bind, Except.bind, pure, Except.pure] intro h; cases h @@ -1619,11 +1718,11 @@ private theorem scopeNamesPresent_foldl_stmtNextScope_of_validateScopedStmtListI unfold validateScopedStmtIdentifiers at hstmt' revert hstmt' rcases hOffsetVal : validateScopedExprIdentifiers context params paramScope dynamicParams - localScope constructorArgCount _ with _ | _ + immutableNames localScope constructorArgCount _ with _ | _ · intro h; simp [bind, Except.bind] at h · simp only [hOffsetVal, bind, Except.bind] rcases hValueVal : validateScopedExprIdentifiers context params paramScope dynamicParams - localScope constructorArgCount _ with _ | _ + immutableNames localScope constructorArgCount _ with _ | _ · intro h; simp [hValueVal, bind, Except.bind] at h · simp only [hValueVal, bind, Except.bind, pure, Except.pure] intro h; cases h @@ -1641,11 +1740,11 @@ private theorem scopeNamesPresent_foldl_stmtNextScope_of_validateScopedStmtListI unfold validateScopedStmtIdentifiers at hstmt' revert hstmt' rcases hOffsetVal : validateScopedExprIdentifiers context params paramScope dynamicParams - localScope constructorArgCount _ with _ | _ + immutableNames localScope constructorArgCount _ with _ | _ · intro h; simp [bind, Except.bind] at h · simp only [hOffsetVal, bind, Except.bind] rcases hValueVal : validateScopedExprIdentifiers context params paramScope dynamicParams - localScope constructorArgCount _ with _ | _ + immutableNames localScope constructorArgCount _ with _ | _ · intro h; simp [hValueVal, bind, Except.bind] at h · simp only [hValueVal, bind, Except.bind, pure, Except.pure] intro h; cases h @@ -1662,13 +1761,13 @@ private theorem scopeNamesPresent_foldl_stmtNextScope_of_validateScopedStmtListI have hstmt' := hstmt unfold validateScopedStmtIdentifiers at hstmt' revert hstmt' - rcases hCondVal : validateScopedExprIdentifiers context params paramScope dynamicParams localScope constructorArgCount _ with _ | _ + rcases hCondVal : validateScopedExprIdentifiers context params paramScope dynamicParams immutableNames localScope constructorArgCount _ with _ | _ · intro h; simp [bind, Except.bind] at h · simp only [bind, Except.bind, pure, Except.pure] - rcases hThenVal : validateScopedStmtListIdentifiers context params paramScope dynamicParams localScope constructorArgCount _ with _ | _ + rcases hThenVal : validateScopedStmtListIdentifiers context params paramScope dynamicParams immutableNames localScope constructorArgCount _ with _ | _ · intro h; simp [hThenVal, bind, Except.bind] at h · simp only [hThenVal, bind, Except.bind] - rcases hElseVal : validateScopedStmtListIdentifiers context params paramScope dynamicParams localScope constructorArgCount _ with _ | _ + rcases hElseVal : validateScopedStmtListIdentifiers context params paramScope dynamicParams immutableNames localScope constructorArgCount _ with _ | _ · intro h; simp [hElseVal, bind, Except.bind] at h · simp only [hElseVal, bind, Except.bind, pure, Except.pure] intro h; cases h @@ -1690,13 +1789,13 @@ private theorem scopeNamesPresent_foldl_stmtNextScope_of_validateScopedStmtListI simp only [bind, Except.bind, pure, Except.pure] intro hstmt' rcases hCountVal : - validateScopedExprIdentifiers context params paramScope dynamicParams localScope + validateScopedExprIdentifiers context params paramScope dynamicParams immutableNames localScope constructorArgCount (Expr.literal 0) with _ | _ · rw [hCountVal] at hstmt'; simp at hstmt' · rw [hCountVal] at hstmt' rcases hBodyVal : validateScopedStmtListIdentifiers context params paramScope dynamicParams - (_ :: localScope) constructorArgCount _ with _ | _ + immutableNames (_ :: localScope) constructorArgCount _ with _ | _ · rw [hBodyVal] at hstmt'; simp at hstmt' · rw [hBodyVal] at hstmt'; simp at hstmt'; cases hstmt' intro other hmem @@ -1717,13 +1816,13 @@ private theorem scopeNamesPresent_foldl_stmtNextScope_of_validateScopedStmtListI simp only [bind, Except.bind, pure, Except.pure] intro hstmt' rcases hCountVal : - validateScopedExprIdentifiers context params paramScope dynamicParams localScope + validateScopedExprIdentifiers context params paramScope dynamicParams immutableNames localScope constructorArgCount (Expr.literal _) with _ | _ · rw [hCountVal] at hstmt'; simp at hstmt' · rw [hCountVal] at hstmt' rcases hBodyVal : validateScopedStmtListIdentifiers context params paramScope dynamicParams - (_ :: localScope) constructorArgCount [] with _ | _ + immutableNames (_ :: localScope) constructorArgCount [] with _ | _ · rw [hBodyVal] at hstmt'; simp at hstmt' · rw [hBodyVal] at hstmt'; simp at hstmt'; cases hstmt' intro other hmem @@ -1755,7 +1854,7 @@ theorem exprBoundNamesInScope_setStorage_of_validateFunctionIdentifierReferences have hstmt' := hstmtValidate unfold validateScopedStmtIdentifiers at hstmt' revert hstmt' - rcases hExprVal : validateScopedExprIdentifiers _ _ _ _ localScope _ value with _ | _ + rcases hExprVal : validateScopedExprIdentifiers _ _ _ _ [] localScope _ value with _ | _ · intro h; simp [bind, Except.bind] at h · simp only [bind, Except.bind, pure, Except.pure] intro h; cases h @@ -1941,6 +2040,18 @@ theorem stmtListScopeDiscipline_scope_names · right; left; exact hbind · right; right; left; exact hassign · right; right; right; exact hfld + | setImmutable hcore hinScope _ ih => + intro other hmem + simp only [List.foldl] at hmem + have htail := ih other hmem + simp [stmtNextScope, collectStmtNames, collectStmtListBindNames, collectStmtBindNames, + collectStmtListAssignedNames, collectStmtAssignedNames] at htail ⊢ + rcases htail with hvalue | hscope | hbind | hassign | hfld + · left; exact hinScope _ (collectExprNames_mem_exprBoundNames_of_core hcore _ hvalue) + · left; exact hscope + · right; left; exact hbind + · right; right; left; exact hassign + · right; right; right; exact hfld | setStorageWord _hfield hcore hinScope _ ih => intro other hmem simp only [List.foldl] at hmem diff --git a/Compiler/Proofs/IRGeneration/SourceSemantics.lean b/Compiler/Proofs/IRGeneration/SourceSemantics.lean index dcf4f1a0d..28a3f10bc 100644 --- a/Compiler/Proofs/IRGeneration/SourceSemantics.lean +++ b/Compiler/Proofs/IRGeneration/SourceSemantics.lean @@ -595,6 +595,7 @@ private def findUniqueInternalFunction? (spec : CompilationModel) (calleeName : structure RuntimeState where world : Verity.ContractState + immutable : String → Verity.Core.Uint256 := fun _ => 0 bindings : List (String × Nat) selector : Nat := 0 @@ -814,14 +815,15 @@ def evalExpr (fields : List Field) (state : RuntimeState) : Expr → Option Nat | .paramDynamicStaticComposite _ _ => none | .literal n => some (wordNormalize n) | .param name => some (lookupValue state.bindings name) - | .storage fieldName => - match findFieldWithResolvedSlot fields fieldName with - | some (_, slot) => some (state.world.storage (wordNormalize slot)).val - | none => none - | .storageAddr fieldName => - match findFieldWithResolvedSlot fields fieldName with - | some (_, slot) => some (state.world.storageAddr (wordNormalize slot)).val - | none => none + | .immutable name => some (state.immutable name).val + | .storage fieldName => + match findFieldWithResolvedSlot fields fieldName with + | some (_, slot) => some (state.world.storage (wordNormalize slot)).val + | none => none + | .storageAddr fieldName => + match findFieldWithResolvedSlot fields fieldName with + | some (_, slot) => some (state.world.storageAddr (wordNormalize slot)).val + | none => none | .storageArrayLength fieldName => match findFieldWithResolvedSlot fields fieldName with | some ({ ty := .dynamicArray _, .. }, slot) => some (state.world.storageArray slot).length @@ -1121,6 +1123,12 @@ private theorem evalExpr_param (name : String) : evalExpr fields state (.param name) = some (lookupValue state.bindings name) := rfl +private theorem evalExpr_immutable + (fields : List Field) + (state : RuntimeState) + (name : String) : + evalExpr fields state (.immutable name) = some (state.immutable name).val := rfl + private theorem evalExpr_localVar (fields : List Field) (state : RuntimeState) @@ -2078,6 +2086,14 @@ mutual | some slots, some resolved => .continue { state with world := writeAddressSlots state.world slots resolved } | _, _ => .revert + | state, .setImmutable name value => + match evalExpr fields state value with + | some resolved => + .continue + { state with + immutable := fun immName => + if immName == name then resolved else state.immutable immName } + | none => .revert | state, .mstore offset value => match evalExpr fields state offset, evalExpr fields state value with | some resolvedOffset, some resolvedValue => @@ -2338,6 +2354,14 @@ mutual | some slots, some resolved => .continue { state with world := writeAddressSlots state.world slots resolved } | _, _ => .revert + | state, .setImmutable name value => + match evalExpr fields state value with + | some resolved => + .continue + { state with + immutable := fun immName => + if immName == name then resolved else state.immutable immName } + | none => .revert | state, .mstore offset value => match evalExpr fields state offset, evalExpr fields state value with | some resolvedOffset, some resolvedValue => @@ -2878,14 +2902,15 @@ mutual (state : RuntimeState) : Expr → Option Nat | .literal n => some (wordNormalize n) | .param name => some (lookupValue state.bindings name) - | .storage fieldName => - match findFieldWithResolvedSlot fields fieldName with - | some (_, slot) => some (state.world.storage (wordNormalize slot)).val - | none => none - | .storageAddr fieldName => - match findFieldWithResolvedSlot fields fieldName with - | some (_, slot) => some (state.world.storageAddr (wordNormalize slot)).val - | none => none + | .immutable name => some (state.immutable name).val + | .storage fieldName => + match findFieldWithResolvedSlot fields fieldName with + | some (_, slot) => some (state.world.storage (wordNormalize slot)).val + | none => none + | .storageAddr fieldName => + match findFieldWithResolvedSlot fields fieldName with + | some (_, slot) => some (state.world.storageAddr (wordNormalize slot)).val + | none => none | .storageArrayLength fieldName => match findFieldWithResolvedSlot fields fieldName with | some ({ ty := .dynamicArray _, .. }, slot) => some (state.world.storageArray slot).length @@ -3393,6 +3418,14 @@ mutual | some slots, some resolved => .continue { state with world := writeAddressSlots state.world slots resolved } | _, _ => .revert + | .setImmutable name value => + match evalExprWithHelpers spec fields fuel state value with + | some resolved => + .continue + { state with + immutable := fun immName => + if immName == name then resolved else state.immutable immName } + | none => .revert | .mstore offset value => match evalExprWithHelpers spec fields fuel state offset, evalExprWithHelpers spec fields fuel state value with @@ -4259,6 +4292,8 @@ mutual simpa [evalExprWithHelpers, evalExpr_literal] | param _ => simpa [evalExprWithHelpers, evalExpr_param] + | immutable _ => + simpa [evalExprWithHelpers, evalExpr_immutable] | localVar _ => simpa [evalExprWithHelpers, evalExpr_localVar] | caller | contractAddress | txOrigin | chainid | msgValue | selfBalance | blockTimestamp | blockNumber | blobbasefee @@ -4783,6 +4818,10 @@ private theorem execStmtWithHelpers_eq_execStmt_of_helperSurfaceClosed_aux simp only [stmtTouchesUnsupportedHelperSurface] at hsurface simp [execStmtWithHelpers, execStmtWithEvents, evalExprWithHelpers_eq_evalExpr_of_helperSurfaceClosed spec fields fuel state value hsurface] + | .setImmutable _ value => + simp only [stmtTouchesUnsupportedHelperSurface] at hsurface + simp [execStmtWithHelpers, execStmtWithEvents, + evalExprWithHelpers_eq_evalExpr_of_helperSurfaceClosed spec fields fuel state value hsurface] | .storageArrayPush _ value => simp only [stmtTouchesUnsupportedHelperSurface] at hsurface simp [execStmtWithHelpers, execStmtWithEvents, diff --git a/Compiler/Proofs/IRGeneration/SupportedFragment.lean b/Compiler/Proofs/IRGeneration/SupportedFragment.lean index 2393fac99..17f4ec31f 100644 --- a/Compiler/Proofs/IRGeneration/SupportedFragment.lean +++ b/Compiler/Proofs/IRGeneration/SupportedFragment.lean @@ -59,6 +59,13 @@ inductive SupportedStmtList (fields : List Field) : List String → List Stmt findFieldWithResolvedSlot fields fieldName = some ({ name := fieldName, ty := FieldType.address }, slot) → SupportedStmtList fields scope [Stmt.setStorageAddr fieldName value] + | setImmutableSingle + {scope : List String} + {name : String} + {value : Expr} : + FunctionBody.ExprCompileCore value → + FunctionBody.exprBoundNamesInScope value scope → + SupportedStmtList fields scope [Stmt.setImmutable name value] | mstoreSingle {scope : List String} {offset value : Expr} : diff --git a/Compiler/Proofs/IRGeneration/SupportedSpec.lean b/Compiler/Proofs/IRGeneration/SupportedSpec.lean index 88c09772c..4d758ddd4 100644 --- a/Compiler/Proofs/IRGeneration/SupportedSpec.lean +++ b/Compiler/Proofs/IRGeneration/SupportedSpec.lean @@ -211,6 +211,7 @@ def exprEventArgAtomic : Expr → Bool | .literal _ | .param _ | .localVar _ | .caller | .contractAddress | .txOrigin | .msgValue | .blockTimestamp | .blockNumber | .chainid | .blobbasefee | .calldatasize => true + | .immutable _ => false | _ => false def eventEmissionProofSupported @@ -653,7 +654,7 @@ mutual decoding. Raw constructor calldata observations therefore remain outside the current body-level support interface until the deploy-wrapper proof exists. -/ def exprTouchesUnsupportedConstructorRawCalldataSurface : Expr → Bool - | .literal _ | .param _ | .localVar _ | .caller | .contractAddress | .txOrigin + | .literal _ | .param _ | .immutable _ | .localVar _ | .caller | .contractAddress | .txOrigin | .chainid | .msgValue | .selfBalance | .blockTimestamp | .blockNumber | .blobbasefee | .constructorArg _ | .returndataSize | .extcodesize _ => false | .calldatasize => true @@ -737,7 +738,7 @@ def exprListTouchesUnsupportedConstructorRawCalldataSurface : List Expr → Bool def stmtTouchesUnsupportedConstructorRawCalldataSurface : Stmt → Bool | .letVar _ value | .assignVar _ value | .setStorage _ value - | .setStorageAddr _ value | .setStorageWord _ _ value + | .setStorageAddr _ value | .setImmutable _ value | .setStorageWord _ _ value | .require value _ | .return value | .storageArrayPush _ value => exprTouchesUnsupportedConstructorRawCalldataSurface value @@ -806,6 +807,7 @@ def exprTouchesUnsupportedCoreSurface : Expr → Bool | .literal _ | .param _ | .caller | .contractAddress | .txOrigin | .chainid | .msgValue | .blockTimestamp | .blockNumber | .blobbasefee | .calldatasize | .localVar _ => false + | .immutable _ => true | .selfBalance => true | .storage _ | .storageAddr _ => false | .add a b | .sub a b | .mul a b | .div a b | .mod a b @@ -859,7 +861,7 @@ def exprTouchesUnsupportedCoreSurface : Expr → Bool /-- Stateful expression surfaces not yet carried by the generic Layer 2 body interface. These are the next storage/layout-style widening targets. -/ def exprTouchesUnsupportedStateSurface : Expr → Bool - | .literal _ | .param _ | .caller | .contractAddress | .txOrigin + | .literal _ | .param _ | .immutable _ | .caller | .contractAddress | .txOrigin | .chainid | .msgValue | .selfBalance | .blockTimestamp | .blockNumber | .localVar _ => false | .storage _ | .storageAddr _ => true @@ -912,7 +914,7 @@ body theorem: internal helper reuse, low-level calls, and foreign call hooks. -/ def exprTouchesUnsupportedCallSurface : Expr → Bool | .internalCall _ _ | .externalCall _ _ => true | .call _ _ _ _ _ _ _ | .staticcall _ _ _ _ _ _ | .delegatecall _ _ _ _ _ _ => true - | .literal _ | .param _ | .caller | .contractAddress | .txOrigin + | .literal _ | .param _ | .immutable _ | .caller | .contractAddress | .txOrigin | .chainid | .msgValue | .selfBalance | .blockTimestamp | .blockNumber | .localVar _ | .storage _ | .storageAddr _ | .constructorArg _ | .blobbasefee @@ -971,7 +973,7 @@ def exprTouchesUnsupportedCallSurface : Expr → Bool generic whole-contract theorem. -/ def exprTouchesUnsupportedHelperSurface : Expr → Bool | .internalCall _ _ => true - | .literal _ | .param _ | .caller | .contractAddress | .txOrigin + | .literal _ | .param _ | .immutable _ | .caller | .contractAddress | .txOrigin | .chainid | .msgValue | .selfBalance | .blockTimestamp | .blockNumber | .localVar _ | .storage _ | .storageAddr _ | .constructorArg _ | .blobbasefee @@ -1039,7 +1041,7 @@ still-unsupported expression shapes that currently share the coarse `exprTouchesUnsupportedHelperSurface` approximation. -/ def exprTouchesInternalHelperSurface : Expr → Bool | .internalCall _ _ => true - | .literal _ | .param _ | .caller | .contractAddress | .txOrigin + | .literal _ | .param _ | .immutable _ | .caller | .contractAddress | .txOrigin | .chainid | .msgValue | .selfBalance | .blockTimestamp | .blockNumber | .localVar _ | .storage _ | .storageAddr _ | .constructorArg _ | .blobbasefee @@ -1102,7 +1104,7 @@ def exprTouchesInternalHelperSurface : Expr → Bool whole-contract theorem. -/ def exprTouchesUnsupportedForeignSurface : Expr → Bool | .externalCall _ _ => true - | .literal _ | .param _ | .caller | .contractAddress | .txOrigin + | .literal _ | .param _ | .immutable _ | .caller | .contractAddress | .txOrigin | .chainid | .msgValue | .selfBalance | .blockTimestamp | .blockNumber | .localVar _ | .storage _ | .storageAddr _ | .constructorArg _ | .blobbasefee @@ -1163,7 +1165,7 @@ def exprTouchesUnsupportedForeignSurface : Expr → Bool whole-contract theorem. -/ def exprTouchesUnsupportedLowLevelSurface : Expr → Bool | .call _ _ _ _ _ _ _ | .staticcall _ _ _ _ _ _ | .delegatecall _ _ _ _ _ _ => true - | .literal _ | .param _ | .caller | .contractAddress | .txOrigin + | .literal _ | .param _ | .immutable _ | .caller | .contractAddress | .txOrigin | .chainid | .msgValue | .selfBalance | .blockTimestamp | .blockNumber | .localVar _ | .storage _ | .storageAddr _ | .constructorArg _ | .blobbasefee @@ -1228,6 +1230,7 @@ def exprTouchesUnsupportedContractSurface (expr : Expr) : Bool := | .literal _ | .param _ | .caller | .contractAddress | .txOrigin | .chainid | .msgValue | .blockTimestamp | .blockNumber | .blobbasefee | .calldatasize | .localVar _ => false + | .immutable _ => true | .selfBalance => true | .storage _ | .storageAddr _ => true | .add a b | .sub a b | .mul a b | .div a b | .mod a b @@ -1278,7 +1281,8 @@ theorem: richer returns, logs, typed errors, and raw external effect hooks. -/ def stmtTouchesUnsupportedEffectSurface : Stmt → Bool | .requireError _ _ _ | .revertError _ _ | .returnValues _ | .returnArray _ | .returnBytes _ | .returnStorageWords _ | .returnCodeData _ | .emit _ _ | .rawLog _ _ _ - | .externalCallBind _ _ _ | .tryExternalCallBind _ _ _ _ | .ecm _ _ => true + | .externalCallBind _ _ _ | .tryExternalCallBind _ _ _ _ | .ecm _ _ + | .setImmutable _ _ => true | .letVar _ _ | .assignVar _ _ | .setStorage _ _ | .setStorageAddr _ _ | .setStorageWord _ _ _ | .require _ _ | .return _ | .mstore _ _ | .tstore _ _ | .stop @@ -1302,7 +1306,7 @@ interfaces of their own. -/ def stmtTouchesUnsupportedCoreSurface : Stmt → Bool | .letVar _ value | .assignVar _ value | .setStorage _ value => exprTouchesUnsupportedCoreSurface value - | .setStorageAddr _ value => + | .setStorageAddr _ value | .setImmutable _ value => exprTouchesUnsupportedCoreSurface value | .setStorageWord _ _ value => exprTouchesUnsupportedCoreSurface value @@ -1350,7 +1354,7 @@ def stmtTouchesUnsupportedStateSurface : Stmt → Bool exprTouchesUnsupportedStateSurface value | .require cond _ | .return cond => exprTouchesUnsupportedStateSurface cond - | .setStorageAddr _ value => + | .setStorageAddr _ value | .setImmutable _ value => exprTouchesUnsupportedStateSurface value | .setStorageWord _ _ _ | .setMapping _ _ _ | .setMappingWord _ _ _ _ | .setMappingPackedWord _ _ _ _ _ | .setMapping2 _ _ _ _ | .setMapping2Word _ _ _ _ _ | .setMappingUint _ _ _ @@ -1388,7 +1392,7 @@ def stmtTouchesUnsupportedStateSurfaceExceptMappingWrites : Stmt → Bool generic theorem. -/ def stmtTouchesUnsupportedCallSurface : Stmt → Bool | .letVar _ value | .assignVar _ value | .setStorage _ value - | .setStorageAddr _ value | .setStorageWord _ _ value | .storageArrayPush _ value => + | .setStorageAddr _ value | .setImmutable _ value | .setStorageWord _ _ value | .storageArrayPush _ value => exprTouchesUnsupportedCallSurface value | .setMapping _ key value | .setMappingWord _ key _ value | .setMappingPackedWord _ key _ _ value | .setMappingUint _ key value @@ -1430,7 +1434,7 @@ def stmtTouchesUnsupportedCallSurface : Stmt → Bool def stmtTouchesUnsupportedHelperSurface : Stmt → Bool | .letVar _ value | .assignVar _ value | .setStorage _ value - | .setStorageAddr _ value | .setStorageWord _ _ value | .storageArrayPush _ value => + | .setStorageAddr _ value | .setImmutable _ value | .setStorageWord _ _ value | .storageArrayPush _ value => exprTouchesUnsupportedHelperSurface value | .setMapping _ key value | .setMappingWord _ key _ value | .setMappingPackedWord _ key _ _ value | .setMappingUint _ key value @@ -1474,7 +1478,7 @@ this isolates heads that genuinely execute internal helpers, leaving residual non-helper unsupported cases to be tracked separately. -/ def stmtTouchesInternalHelperSurface : Stmt → Bool | .letVar _ value | .assignVar _ value | .setStorage _ value - | .setStorageAddr _ value | .setStorageWord _ _ value | .storageArrayPush _ value => + | .setStorageAddr _ value | .setImmutable _ value | .setStorageWord _ _ value | .storageArrayPush _ value => exprTouchesInternalHelperSurface value | .setMapping _ key value | .setMappingWord _ key _ value | .setMappingPackedWord _ key _ _ value | .setMappingUint _ key value @@ -1541,7 +1545,7 @@ soundness and world-preservation lemmas directly, rather than bundling them with direct helper statements or recursive structural transport. -/ def stmtTouchesExprInternalHelperSurface : Stmt → Bool | .letVar _ value | .assignVar _ value | .setStorage _ value - | .setStorageAddr _ value | .setStorageWord _ _ value | .storageArrayPush _ value => + | .setStorageAddr _ value | .setImmutable _ value | .setStorageWord _ _ value | .storageArrayPush _ value => exprTouchesInternalHelperSurface value | .setMapping _ key value | .setMappingWord _ key _ value | .setMappingPackedWord _ key _ _ value | .setMappingUint _ key value @@ -1588,7 +1592,7 @@ def stmtTouchesStructuralInternalHelperSurface : Stmt → Bool stmtListTouchesInternalHelperSurface body | .letVar _ _ | .assignVar _ _ | .setStorage _ _ | .require _ _ | .return _ | .returnCodeData _ | .internalCall _ _ | .internalCallAssign _ _ _ - | .stop | .setStorageAddr _ _ | .setStorageWord _ _ _ | .mstore _ _ | .tstore _ _ + | .stop | .setStorageAddr _ _ | .setImmutable _ _ | .setStorageWord _ _ _ | .mstore _ _ | .tstore _ _ | .calldatacopy _ _ _ | .returndataCopy _ _ _ | .revertReturndata | .externalCallBind _ _ _ | .tryExternalCallBind _ _ _ _ | .ecm _ _ @@ -1606,7 +1610,7 @@ def stmtTouchesStructuralInternalHelperSurface : Stmt → Bool def stmtTouchesUnsupportedForeignSurface : Stmt → Bool | .letVar _ value | .assignVar _ value | .setStorage _ value - | .setStorageAddr _ value | .setStorageWord _ _ value | .storageArrayPush _ value => + | .setStorageAddr _ value | .setImmutable _ value | .setStorageWord _ _ value | .storageArrayPush _ value => exprTouchesUnsupportedForeignSurface value | .setMapping _ key value | .setMappingWord _ key _ value | .setMappingPackedWord _ key _ _ value | .setMappingUint _ key value @@ -1648,7 +1652,7 @@ def stmtTouchesUnsupportedForeignSurface : Stmt → Bool def stmtTouchesUnsupportedLowLevelSurface : Stmt → Bool | .letVar _ value | .assignVar _ value | .setStorage _ value - | .setStorageAddr _ value | .setStorageWord _ _ value | .storageArrayPush _ value => + | .setStorageAddr _ value | .setImmutable _ value | .setStorageWord _ _ value | .storageArrayPush _ value => exprTouchesUnsupportedLowLevelSurface value | .setMapping _ key value | .setMappingWord _ key _ value | .setMappingPackedWord _ key _ _ value | .setMappingUint _ key value @@ -1693,6 +1697,7 @@ def stmtTouchesUnsupportedContractSurface (stmt : Stmt) : Bool := exprTouchesUnsupportedContractSurface value | .setStorageAddr _ value => exprTouchesUnsupportedContractSurface value + | .setImmutable _ _ => true | .setStorageWord _ _ value => exprTouchesUnsupportedContractSurface value | .require cond _ | .return cond => @@ -1921,7 +1926,7 @@ private theorem compileStmt_eventsErrorsAgnostic_aux (by simp [Stmt.forEach.sizeOf_spec] at hlt; omega) (stmtListTouchesUnsupportedContractSurface_of_forEach_surfaceClosed hsurface)] - | letVar | assignVar | setStorage | setStorageAddr | setStorageWord + | letVar | assignVar | setStorage | setStorageAddr | setImmutable | setStorageWord | require | «return» | mstore | tstore | stop => simp only [CompilationModel.compileStmt] | setMapping | setMappingWord | setMappingPackedWord | setMapping2 @@ -2063,7 +2068,7 @@ mutual -- `_mutual.eq_def` 200 000-heartbeat ceiling when new `Expr` constructors -- land (verity#1842 captured the same pitfall for the Expr→Except -- validators). - | .literal _ | .param _ | .constructorArg _ + | .literal _ | .param _ | .immutable _ | .constructorArg _ | .storage _ | .storageAddr _ | .caller | .contractAddress | .txOrigin | .chainid | .msgValue | .selfBalance | .blockTimestamp | .blockNumber | .blobbasefee @@ -2092,6 +2097,7 @@ mutual helper-aware expression semantics returns only a value. -/ def stmtExprHelperCallNames : Stmt → List String | .letVar _ value | .assignVar _ value | .setStorage _ value | .setStorageAddr _ value + | .setImmutable _ value | .setStorageWord _ _ value | .storageArrayPush _ value | .return value | .require value _ => exprInternalHelperCallNames value @@ -2159,6 +2165,7 @@ mutual /-- Collect direct internal-helper callee names mentioned by a statement list. -/ def stmtInternalHelperCallNames : Stmt → List String | .letVar _ value | .assignVar _ value | .setStorage _ value | .setStorageAddr _ value + | .setImmutable _ value | .setStorageWord _ _ value | .storageArrayPush _ value | .return value | .require value _ => exprInternalHelperCallNames value @@ -3336,6 +3343,12 @@ theorem SupportedStmtList.helperSurfaceClosed Bool.or_false, Bool.false_or] | setStorageAddrSingleSlot hvalue _ _ => exact supportedStmtList_setStorageAddrSingleSlot_helperSurfaceClosed hvalue + | setImmutableSingle hvalue _ => + simp only [stmtListTouchesUnsupportedHelperSurface, + stmtTouchesUnsupportedHelperSurface, + exprTouchesUnsupportedHelperSurface, + exprCompileCore_helperSurfaceClosed hvalue, + Bool.or_false, Bool.false_or] | mstoreSingle hoffset _ hvalue _ => exact supportedStmtList_mstoreSingle_helperSurfaceClosed hoffset hvalue | tstoreSingle hoffset _ hvalue _ => @@ -3464,6 +3477,11 @@ theorem SupportedStmtList.internalHelperCallNames_nil stmtInternalHelperCallNames, exprCompileCore_internalHelperCallNames_nil hvalue, List.nil_append, List.append_nil] + | setImmutableSingle hvalue _ => + simp only [stmtListInternalHelperCallNames, + stmtInternalHelperCallNames, + exprCompileCore_internalHelperCallNames_nil hvalue, + List.nil_append, List.append_nil] | mstoreSingle hoffset _ hvalue _ => simp only [stmtListInternalHelperCallNames, stmtInternalHelperCallNames, @@ -3649,7 +3667,7 @@ mutual | internalCall _ _ => simp [exprTouchesUnsupportedHelperSurface] at hsurface | mappingChain _ _ => simp [exprTouchesUnsupportedHelperSurface] at hsurface | intrinsic _ _ _ _ => simp [exprTouchesUnsupportedHelperSurface] at hsurface - | literal _ | param _ | caller | contractAddress | txOrigin + | literal _ | param _ | immutable _ | caller | contractAddress | txOrigin | chainid | msgValue | selfBalance | blockTimestamp | blockNumber | localVar _ | storage _ | storageAddr _ | constructorArg _ | blobbasefee | calldatasize | returndataSize @@ -3771,7 +3789,7 @@ mutual stmtTouchesInternalHelperSurface stmt = false := by cases stmt with | letVar _ value | assignVar _ value | setStorage _ value - | setStorageAddr _ value | setStorageWord _ _ value | storageArrayPush _ value => + | setStorageAddr _ value | setImmutable _ value | setStorageWord _ _ value | storageArrayPush _ value => simp only [stmtTouchesUnsupportedHelperSurface] at hsurface simp [stmtTouchesInternalHelperSurface, exprTouchesInternalHelperSurface_eq_false_of_helperSurfaceClosed hsurface] @@ -4071,7 +4089,7 @@ private theorem exprTouchesUnsupportedCallSurface_eq_featureOr exprTouchesUnsupportedForeignSurface expr || exprTouchesUnsupportedLowLevelSurface expr) := by cases expr with - | literal _ | param _ | caller | contractAddress | txOrigin + | literal _ | param _ | immutable _ | caller | contractAddress | txOrigin | chainid | msgValue | selfBalance | blockTimestamp | blockNumber | localVar _ | storage _ | storageAddr _ | paramDynamicHeadWord _ _ | paramDynamicStaticComposite _ _ @@ -4307,6 +4325,8 @@ private theorem exprTouchesUnsupportedContractSurface_eq_false_of_featureClosed | chainid | msgValue | blockTimestamp | blockNumber | blobbasefee | calldatasize => simp [exprTouchesUnsupportedContractSurface] + | immutable _ => + simp [exprTouchesUnsupportedCoreSurface] at hcore | selfBalance => simp [exprTouchesUnsupportedCoreSurface] at hcore | storage _ | storageAddr _ => @@ -4562,8 +4582,9 @@ private theorem stmtTouchesUnsupportedContractSurface_eq_false_of_featureClosed exact exprTouchesUnsupportedContractSurface_eq_false_of_featureClosed value (by simpa [stmtTouchesUnsupportedCoreSurface] using hcore) (by simpa [stmtTouchesUnsupportedStateSurface] using hstate) - (by exact exprTouchesUnsupportedCallSurface_eq_false_of_coreClosed value - (by simpa [stmtTouchesUnsupportedCoreSurface] using hcore)) + (by simpa [stmtTouchesUnsupportedCallSurface] using hcalls) + | setImmutable _ _ => + simp [stmtTouchesUnsupportedEffectSurface] at heffects | require cond _ | «return» cond => simp only [stmtTouchesUnsupportedContractSurface] exact exprTouchesUnsupportedContractSurface_eq_false_of_featureClosed cond @@ -4696,6 +4717,8 @@ theorem exprTouchesUnsupportedHelperSurface_eq_false_of_contractSurfaceClosed | chainid | msgValue | blockTimestamp | blockNumber | blobbasefee | calldatasize => simp [exprTouchesUnsupportedHelperSurface] + | immutable _ => + simp [exprTouchesUnsupportedContractSurface] at hsurface | selfBalance => simp [exprTouchesUnsupportedContractSurface] at hsurface | adtConstruct _ _ _ | adtTag _ _ | adtField _ _ _ _ _ => @@ -4793,6 +4816,7 @@ theorem stmtTouchesUnsupportedHelperSurface_eq_false_of_contractSurfaceClosed stmtTouchesUnsupportedHelperSurface stmt = false := by cases stmt with | letVar _ value | assignVar _ value | setStorage _ value | setStorageAddr _ value + | setImmutable _ value | setStorageWord _ _ value | storageArrayPush _ value | require value _ | «return» value => simp [stmtTouchesUnsupportedHelperSurface, stmtTouchesUnsupportedContractSurface] at hsurface ⊢ @@ -5463,6 +5487,9 @@ private theorem supportedStmtList_usesArrayElement_false | setStorageAddrSingleSlot hvalue _ _ => simp only [stmtListUsesArrayElement, stmtUsesArrayElement, exprCompileCore_usesArrayElement_false hvalue, Bool.false_or] + | setImmutableSingle hvalue _ => + simp only [stmtListUsesArrayElement, stmtUsesArrayElement, + exprCompileCore_usesArrayElement_false hvalue, Bool.false_or] | mstoreSingle hoffset _ hvalue _ => simp only [stmtListUsesArrayElement, stmtUsesArrayElement, exprCompileCore_usesArrayElement_false hoffset, @@ -5575,6 +5602,9 @@ private theorem supportedStmtList_usesStorageArrayElement_false | setStorageAddrSingleSlot hvalue _ _ => simp only [stmtListUsesStorageArrayElement, stmtUsesStorageArrayElement, exprCompileCore_usesStorageArrayElement_false hvalue, Bool.false_or] + | setImmutableSingle hvalue _ => + simp only [stmtListUsesStorageArrayElement, stmtUsesStorageArrayElement, + exprCompileCore_usesStorageArrayElement_false hvalue, Bool.false_or] | mstoreSingle hoffset _ hvalue _ => simp only [stmtListUsesStorageArrayElement, stmtUsesStorageArrayElement, exprCompileCore_usesStorageArrayElement_false hoffset, @@ -5695,6 +5725,9 @@ private theorem supportedStmtList_usesDynamicBytesEq_false | setStorageAddrSingleSlot hvalue _ _ => simp only [stmtListUsesDynamicBytesEq, stmtUsesDynamicBytesEq, exprCompileCore_usesDynamicBytesEq_false hvalue, Bool.false_or] + | setImmutableSingle hvalue _ => + simp only [stmtListUsesDynamicBytesEq, stmtUsesDynamicBytesEq, + exprCompileCore_usesDynamicBytesEq_false hvalue, Bool.false_or] | mstoreSingle hoffset _ hvalue _ => simp only [stmtListUsesDynamicBytesEq, stmtUsesDynamicBytesEq, exprCompileCore_usesDynamicBytesEq_false hoffset, @@ -6066,6 +6099,9 @@ private theorem supportedStmtList_usesMulDiv512_false | setStorageAddrSingleSlot hvalue _ _ => simp only [stmtListUsesMulDiv512, stmtUsesMulDiv512, exprCompileCore_usesMulDiv512_false hvalue, Bool.false_or] + | setImmutableSingle hvalue _ => + simp only [stmtListUsesMulDiv512, stmtUsesMulDiv512, + exprCompileCore_usesMulDiv512_false hvalue, Bool.false_or] | mstoreSingle hoffset _ hvalue _ => simp only [stmtListUsesMulDiv512, stmtUsesMulDiv512, exprCompileCore_usesMulDiv512_false hoffset, @@ -6178,6 +6214,9 @@ private theorem supportedStmtList_usesParamDynamicHeadWord_false | setStorageAddrSingleSlot hvalue _ _ => simp only [stmtListUsesParamDynamicHeadWord, stmtUsesParamDynamicHeadWord, exprCompileCore_usesParamDynamicHeadWord_false hvalue, Bool.false_or] + | setImmutableSingle hvalue _ => + simp only [stmtListUsesParamDynamicHeadWord, stmtUsesParamDynamicHeadWord, + exprCompileCore_usesParamDynamicHeadWord_false hvalue, Bool.false_or] | mstoreSingle hoffset _ hvalue _ => simp only [stmtListUsesParamDynamicHeadWord, stmtUsesParamDynamicHeadWord, exprCompileCore_usesParamDynamicHeadWord_false hoffset, diff --git a/PrintAxioms.lean b/PrintAxioms.lean index 789596c49..e14c7b53e 100644 --- a/PrintAxioms.lean +++ b/PrintAxioms.lean @@ -1752,6 +1752,7 @@ end Verity.AxiomAudit -- Compiler/Proofs/IRGeneration/DenoteAgreement.lean Compiler.Proofs.IRGeneration.DenoteAgreement.toRuntimeState_world + Compiler.Proofs.IRGeneration.DenoteAgreement.toRuntimeState_immutable Compiler.Proofs.IRGeneration.DenoteAgreement.toRuntimeState_bindings Compiler.Proofs.IRGeneration.DenoteAgreement.toRuntimeState_selector Compiler.Proofs.IRGeneration.DenoteAgreement.sourceOracle_mappingSlot @@ -3134,6 +3135,7 @@ end Verity.AxiomAudit Compiler.Proofs.IRGeneration.SourceSemantics.execForEachLoop_empty_body_positive_bound -- Compiler.Proofs.IRGeneration.SourceSemantics.evalExpr_literal -- private -- Compiler.Proofs.IRGeneration.SourceSemantics.evalExpr_param -- private + -- Compiler.Proofs.IRGeneration.SourceSemantics.evalExpr_immutable -- private -- Compiler.Proofs.IRGeneration.SourceSemantics.evalExpr_localVar -- private -- Compiler.Proofs.IRGeneration.SourceSemantics.evalExpr_caller -- private -- Compiler.Proofs.IRGeneration.SourceSemantics.evalExpr_contractAddress -- private @@ -5583,4 +5585,4 @@ end Verity.AxiomAudit Compiler.Proofs.YulGeneration.YulTransaction.ofIR_args ] --- Total: 5225 theorems/lemmas (3619 public, 1606 private, 0 sorry'd) +-- Total: 5227 theorems/lemmas (3620 public, 1607 private, 0 sorry'd) diff --git a/Verity/Core/Model/Denote.lean b/Verity/Core/Model/Denote.lean index bb0058e12..77ebc3f18 100644 --- a/Verity/Core/Model/Denote.lean +++ b/Verity/Core/Model/Denote.lean @@ -175,6 +175,7 @@ def lookupBinding? (bindings : Env) (name : String) : Option Nat := /-- Mirrors `SourceSemantics.RuntimeState`. -/ structure DenoteState where world : Verity.ContractState + immutable : String → Verity.Core.Uint256 := fun _ => 0 bindings : Env selector : Nat := 0 @@ -463,6 +464,7 @@ def evalExpr (oracle : DenoteOracle) (fields : List Field) (state : DenoteState) | .paramDynamicStaticComposite _ _ => none | .literal n => some (wordNormalize n) | .param name => some (lookupValue state.bindings name) + | .immutable name => some (state.immutable name).val | .storage fieldName => match findFieldWithResolvedSlot fields fieldName with | some (_, slot) => some (state.world.readSlot (wordNormalize slot)).val @@ -962,6 +964,14 @@ mutual | some slots, some resolved => .continue { state with world := writeAddressSlots state.world slots resolved } | _, _ => .revert + | state, .setImmutable name value => + match evalExpr oracle fields state value with + | some resolved => + .continue + { state with + immutable := fun immName => + if immName == name then resolved else state.immutable immName } + | none => .revert | state, .mstore offset value => match evalExpr oracle fields state offset, evalExpr oracle fields state value with | some resolvedOffset, some resolvedValue => diff --git a/Verity/Core/Model/Types.lean b/Verity/Core/Model/Types.lean index ef45583b8..ee0f0ae2f 100644 --- a/Verity/Core/Model/Types.lean +++ b/Verity/Core/Model/Types.lean @@ -695,6 +695,7 @@ inductive Expr | literal (n : Nat) | param (name : String) | constructorArg (index : Nat) -- Access constructor argument (loaded from bytecode) + | immutable (name : String) | storage (field : String) | storageAddr (field : String) | mapping (field : String) (key : Expr) @@ -927,7 +928,7 @@ namespace Expr `Expr` constructor fails to compile here (and in `children_sizeOf_lt`) rather than silently falling through a dozen independent walkers. -/ def children : Expr → List Expr - | .literal _ | .param _ | .constructorArg _ | .storage _ | .storageAddr _ + | .literal _ | .param _ | .constructorArg _ | .immutable _ | .storage _ | .storageAddr _ | .caller | .contractAddress | .txOrigin | .chainid | .msgValue | .selfBalance | .blockTimestamp | .blockNumber | .blobbasefee | .calldatasize | .returndataSize | .localVar _ @@ -1041,11 +1042,18 @@ termination_by sizeOf e end Expr +structure ImmutableSpec where + name : String + ty : ParamType + init : Expr + deriving Repr + inductive Stmt | letVar (name : String) (value : Expr) -- Declare local variable | assignVar (name : String) (value : Expr) -- Reassign existing variable | setStorage (field : String) (value : Expr) | setStorageAddr (field : String) (value : Expr) + | setImmutable (name : String) (value : Expr) /-- Write a full storage word at `field.slot + wordOffset`. Intended for migration-faithful manual packed-word writes where the source constructs the packed word explicitly. -/ @@ -1160,6 +1168,8 @@ def directMetadata : Stmt → StmtMetadata { subexpressions := [value], scopeEffects := { assignNames := [name] } } | .setStorage field value | .setStorageAddr field value => { subexpressions := [value], scopeEffects := { storageWrites := [field] } } + | .setImmutable _ value => + { subexpressions := [value] } | .setStorageWord field _ value => { subexpressions := [value], scopeEffects := { storageWrites := [field] } } | .storageArrayPush field value => @@ -1461,6 +1471,7 @@ structure ConstructorSpec where structure CompilationModel where name : String fields : List Field + immutables : List ImmutableSpec := [] /-- Explicit owner/admin/minter/relayer-style access-control declarations. Functions annotated with `requires(role)` resolve through this list when present; legacy `requires(storageField)` remains accepted for existing diff --git a/Verity/Macro/Translate.lean b/Verity/Macro/Translate.lean index e7a68d83c..4d1b4cc98 100644 --- a/Verity/Macro/Translate.lean +++ b/Verity/Macro/Translate.lean @@ -1562,14 +1562,13 @@ private def immutableInitStmtTerms (constDecls : Array ConstantDecl) (immutableDecls : Array ImmutableDecl) (ctorParams : Array ParamDecl) : CommandElabM (Array Term) := do - immutableDecls.zipIdx.mapM fun (imm, idx) => do - let slotField := immutableStorageFieldDecl fields imm idx + immutableDecls.zipIdx.mapM fun (imm, _idx) => do let valueExpr ← translatePureExpr fields constDecls #[] ctorParams #[] imm.body match imm.ty with | .uint256 | .int256 | .uint8 | .uint16 | .bytes32 | .bool => - `(Compiler.CompilationModel.Stmt.setStorage $(strTerm slotField.name) $valueExpr) + `(Compiler.CompilationModel.Stmt.setImmutable $(strTerm imm.name) $valueExpr) | .address => - `(Compiler.CompilationModel.Stmt.setStorageAddr $(strTerm slotField.name) $valueExpr) + `(Compiler.CompilationModel.Stmt.setImmutable $(strTerm imm.name) $valueExpr) | _ => throwErrorAt imm.ident s!"immutable '{imm.name}' uses unsupported type" @@ -2123,9 +2122,12 @@ private def mkSpecCommand (functions : Array FunctionDecl) (adtDecls : Array AdtDecl) (storageNamespace : Option Nat) : CommandElabM Cmd := do - let immutableFields := immutableDecls.zipIdx.map (fun (imm, idx) => immutableStorageFieldDecl fields imm idx) - let allFields := fields ++ immutableFields - let fieldTerms ← allFields.mapM mkModelFieldTerm + let immutableTerms ← immutableDecls.mapM fun imm => do + let tyTerm ← modelParamTypeTerm imm.ty + let initTerm ← translatePureExpr fields constDecls #[] (ctor.map (·.params) |>.getD #[]) #[] imm.body + `(({ name := $(strTerm imm.name), ty := $tyTerm, init := $initTerm } : + Compiler.CompilationModel.ImmutableSpec)) + let fieldTerms ← fields.mapM mkModelFieldTerm let roleTerms ← roleDecls.mapM fun role => do let kindTerm ← match role.kind with | .scalarAddress => `(Compiler.CompilationModel.RoleKind.scalarAddress) @@ -2264,6 +2266,7 @@ private def mkSpecCommand `(command| def spec : Compiler.CompilationModel.CompilationModel := { name := $(strTerm contractName) fields := [ $[$fieldTerms],* ] + «immutables» := [ $[$immutableTerms],* ] «roles» := [ $[$roleTerms],* ] «errors» := [ $[$errorTerms],* ] «events» := [ $[$eventTerms],* ] diff --git a/Verity/Macro/Translate/Expr.lean b/Verity/Macro/Translate/Expr.lean index 26f3cbe6f..926714611 100644 --- a/Verity/Macro/Translate/Expr.lean +++ b/Verity/Macro/Translate/Expr.lean @@ -3012,8 +3012,8 @@ partial def translatePureExprWithTypes else if let some imm := immutableDecls.find? (fun imm => declaredNameMatches name imm.name) then match imm.ty with | .uint256 | .int256 | .uint8 | .uint16 | .bytes32 | .bool => - `(Compiler.CompilationModel.Expr.storage $(strTerm (immutableHiddenName imm))) - | .address => `(Compiler.CompilationModel.Expr.storageAddr $(strTerm (immutableHiddenName imm))) + `(Compiler.CompilationModel.Expr.immutable $(strTerm imm.name)) + | .address => `(Compiler.CompilationModel.Expr.immutable $(strTerm imm.name)) | _ => throwErrorAt stx s!"immutable '{name}' uses unsupported type" else if let some constant := constDecls.find? (fun constant => declaredNameMatches name constant.name) then translateConstantExpr fields constDecls immutableDecls visitingConstants constant.name diff --git a/artifacts/storage_layout_report.json b/artifacts/storage_layout_report.json index 1cde5e2fe..bedc9d997 100644 --- a/artifacts/storage_layout_report.json +++ b/artifacts/storage_layout_report.json @@ -18,6 +18,7 @@ ] } ], + "immutables": [], "nonAliasClaims": [], "reservedSlotRanges": [], "slotAliasRanges": [], @@ -50,6 +51,7 @@ ] } ], + "immutables": [], "nonAliasClaims": [], "reservedSlotRanges": [], "slotAliasRanges": [], @@ -82,6 +84,7 @@ ] } ], + "immutables": [], "nonAliasClaims": [], "reservedSlotRanges": [], "slotAliasRanges": [], @@ -118,6 +121,7 @@ ] } ], + "immutables": [], "nonAliasClaims": [], "reservedSlotRanges": [], "slotAliasRanges": [], @@ -182,6 +186,7 @@ ] } ], + "immutables": [], "nonAliasClaims": [ { "a": "totalAssetsSlot", @@ -282,6 +287,7 @@ ] } ], + "immutables": [], "nonAliasClaims": [ { "a": "owner", @@ -367,6 +373,7 @@ ] } ], + "immutables": [], "nonAliasClaims": [ { "a": "ownerSlot", @@ -453,6 +460,7 @@ ] } ], + "immutables": [], "nonAliasClaims": [], "reservedSlotRanges": [], "slotAliasRanges": [], @@ -536,6 +544,7 @@ ] } ], + "immutables": [], "nonAliasClaims": [ { "a": "ownerSlot",