diff --git a/Compiler/CompilationModel.lean b/Compiler/CompilationModel.lean index 0da1f3367..5f1aa9d4a 100644 --- a/Compiler/CompilationModel.lean +++ b/Compiler/CompilationModel.lean @@ -22,6 +22,7 @@ import Compiler.CompilationModel.MappingWrites import Compiler.CompilationModel.ScopeValidation import Compiler.CompilationModel.StorageWrites import Compiler.CompilationModel.TrustSurface +import Compiler.CompilationModel.YulImporter import Compiler.CompilationModel.UsageAnalysis import Compiler.CompilationModel.ValidationCalls import Compiler.CompilationModel.ValidationEvents diff --git a/Compiler/CompilationModel/Compile.lean b/Compiler/CompilationModel/Compile.lean index efb916144..2153a3259 100644 --- a/Compiler/CompilationModel/Compile.lean +++ b/Compiler/CompilationModel/Compile.lean @@ -42,6 +42,16 @@ namespace Compiler.CompilationModel open Compiler open Compiler.Yul +/-- Single bridge from typed unsafe/raw Yul fragments into the EVMYul AST. + Proof obligations and trust metadata live on `UnsafeYulFragment`; this + function is intentionally the only compiler lowering point for that escape + hatch. -/ +def unsafeYulToEVMYul (fragment : UnsafeYulFragment) : List YulStmt := + fragment.stmts + +theorem unsafeYulToEVMYul_eq (fragment : UnsafeYulFragment) : + unsafeYulToEVMYul fragment = fragment.stmts := rfl + private def compileAdtStorageWrite (fields : List Field) (dynamicSource : DynamicDataSource) (adtTypes : List AdtTypeDef) (storageField adtName variantName : String) (args : List Expr) : @@ -270,6 +280,9 @@ def compileStmt (fields : List Field) (events : List EventDef := []) -- Unsafe block: transparent wrapper, compile inner body directly (#1728, Axis 6 Step 6a) compileStmtList fields events errors dynamicSource internalRetNames isInternal inScopeNames adtTypes body + | Stmt.unsafeYul fragment => + pure (unsafeYulToEVMYul fragment) + | Stmt.emit eventName args => do compileEmit fields events dynamicSource eventName args @@ -467,4 +480,17 @@ def compileMatchAdtBranches (fields : List Field) (events : List EventDef) pure ((variant.tag, fieldBindings ++ bodyStmts) :: restCases) end +theorem compileStmt_unsafeYul + (fields : List Field) (events : List EventDef := []) + (errors : List ErrorDef := []) + (dynamicSource : DynamicDataSource := .calldata) + (internalRetNames : List String := []) + (isInternal : Bool := false) + (inScopeNames : List String := []) + (adtTypes : List AdtTypeDef := []) + (fragment : UnsafeYulFragment) : + compileStmt fields events errors dynamicSource internalRetNames isInternal inScopeNames adtTypes + (Stmt.unsafeYul fragment) = pure fragment.stmts := by + simp [compileStmt, unsafeYulToEVMYul] + end Compiler.CompilationModel diff --git a/Compiler/CompilationModel/LogicalPurity.lean b/Compiler/CompilationModel/LogicalPurity.lean index 428a5e2df..1b05572d9 100644 --- a/Compiler/CompilationModel/LogicalPurity.lean +++ b/Compiler/CompilationModel/LogicalPurity.lean @@ -258,6 +258,8 @@ def stmtContainsUnsafeLogicalCallLike : Stmt → Bool exprListAnyUnsafeLogicalCallLike args | Stmt.ecm _ args => exprListAnyUnsafeLogicalCallLike args + | Stmt.unsafeYul _ => + false termination_by s => sizeOf s decreasing_by all_goals simp_wf; all_goals omega diff --git a/Compiler/CompilationModel/ScopeValidation.lean b/Compiler/CompilationModel/ScopeValidation.lean index aa0f11533..56a21b785 100644 --- a/Compiler/CompilationModel/ScopeValidation.lean +++ b/Compiler/CompilationModel/ScopeValidation.lean @@ -566,6 +566,18 @@ def validateScopedStmtIdentifiers | Stmt.returnBytes _ | Stmt.returnStorageWords _ | Stmt.revertReturndata | Stmt.stop => pure localScope + | Stmt.unsafeYul fragment => do + let mut scope := localScope + for name in fragment.scopeEffects.bindNames do + if paramScope.contains name then + throw s!"Compilation error: {context} unsafe Yul fragment '{fragment.label}' result '{name}' shadows a parameter" + if scope.contains name then + throw s!"Compilation error: {context} unsafe Yul fragment '{fragment.label}' redeclares result '{name}' in the same scope" + scope := name :: scope + for name in fragment.scopeEffects.assignNames do + if !scope.contains name then + throw s!"Compilation error: {context} unsafe Yul fragment '{fragment.label}' assigns to undeclared local variable '{name}'" + pure scope termination_by s => sizeOf s decreasing_by all_goals simp_wf; all_goals omega diff --git a/Compiler/CompilationModel/TrustSurface.lean b/Compiler/CompilationModel/TrustSurface.lean index 0f8c2e16c..a8219991e 100644 --- a/Compiler/CompilationModel/TrustSurface.lean +++ b/Compiler/CompilationModel/TrustSurface.lean @@ -156,142 +156,21 @@ private partial def collectAxiomatizedExprPrimitives : Expr → List String | _ => [] -private partial def collectLowLevelStmtMechanics : Stmt → List String - | .letVar _ value - | .assignVar _ value - | .setStorage _ value - | .setStorageAddr _ value - | .setStorageWord _ _ value - | .storageArrayPush _ value - | .return value - | .require value _ => - collectLowLevelExprMechanics value - | .setStorageArrayElement _ index value => - collectLowLevelExprMechanics index ++ collectLowLevelExprMechanics value - | .storageArrayPop _ => - [] - | .requireError cond _ args => - collectLowLevelExprMechanics cond ++ args.flatMap collectLowLevelExprMechanics - | .revertError _ args => - args.flatMap collectLowLevelExprMechanics - | .mstore offset value => - ["mstore"] ++ collectLowLevelExprMechanics offset ++ collectLowLevelExprMechanics value - | .tstore offset value => - ["tstore"] ++ collectLowLevelExprMechanics offset ++ collectLowLevelExprMechanics value - | .calldatacopy destOffset sourceOffset size => - ["calldatacopy"] ++ collectLowLevelExprMechanics destOffset ++ - collectLowLevelExprMechanics sourceOffset ++ collectLowLevelExprMechanics size - | .returndataCopy destOffset sourceOffset size => - ["returndataCopy"] ++ collectLowLevelExprMechanics destOffset ++ collectLowLevelExprMechanics sourceOffset ++ collectLowLevelExprMechanics size - | .revertReturndata => - ["revertReturndata"] - | .setMapping _ key value - | .setMappingWord _ key _ value - | .setMappingPackedWord _ key _ _ value - | .setMappingUint _ key value - | .setStructMember _ key _ value => - collectLowLevelExprMechanics key ++ collectLowLevelExprMechanics value - | .setMappingChain _ keys value => - keys.flatMap collectLowLevelExprMechanics ++ collectLowLevelExprMechanics value - | .setMapping2 _ key1 key2 value - | .setMapping2Word _ key1 key2 _ value - | .setStructMember2 _ key1 key2 _ value => - collectLowLevelExprMechanics key1 ++ collectLowLevelExprMechanics key2 ++ collectLowLevelExprMechanics value - | .ite cond thenBr elseBr => - collectLowLevelExprMechanics cond ++ thenBr.flatMap collectLowLevelStmtMechanics ++ elseBr.flatMap collectLowLevelStmtMechanics - | .forEach _ count body => - collectLowLevelExprMechanics count ++ body.flatMap collectLowLevelStmtMechanics - | .unsafeBlock _ body => - body.flatMap collectLowLevelStmtMechanics - | .matchAdt _ scrutinee branches => - collectLowLevelExprMechanics scrutinee ++ - branches.flatMap fun (_, _, body) => body.flatMap collectLowLevelStmtMechanics - | .emit _ args - | .internalCall _ args - | .externalCallBind _ _ args | .tryExternalCallBind _ _ _ args - | .returnValues args - | .ecm _ args - | .internalCallAssign _ _ args => - args.flatMap collectLowLevelExprMechanics - | .rawLog topics dataOffset dataSize => - topics.flatMap collectLowLevelExprMechanics ++ collectLowLevelExprMechanics dataOffset ++ collectLowLevelExprMechanics dataSize - | .returnArray _ - | .returnBytes _ - | .returnStorageWords _ - | .stop => - [] - -private partial def collectAxiomatizedStmtPrimitives : Stmt → List String - | .letVar _ value - | .assignVar _ value - | .setStorage _ value - | .setStorageAddr _ value - | .setStorageWord _ _ value - | .storageArrayPush _ value - | .return value - | .require value _ => - collectAxiomatizedExprPrimitives value - | .setStorageArrayElement _ index value => - collectAxiomatizedExprPrimitives index ++ collectAxiomatizedExprPrimitives value - | .storageArrayPop _ => - [] - | .requireError cond _ args => - collectAxiomatizedExprPrimitives cond ++ args.flatMap collectAxiomatizedExprPrimitives - | .revertError _ args => - args.flatMap collectAxiomatizedExprPrimitives - | .mstore offset value => - collectAxiomatizedExprPrimitives offset ++ collectAxiomatizedExprPrimitives value - | .tstore offset value => - collectAxiomatizedExprPrimitives offset ++ collectAxiomatizedExprPrimitives value - | .calldatacopy destOffset sourceOffset size - | .returndataCopy destOffset sourceOffset size => - collectAxiomatizedExprPrimitives destOffset ++ collectAxiomatizedExprPrimitives sourceOffset ++ - collectAxiomatizedExprPrimitives size - | .setMapping _ key value - | .setMappingWord _ key _ value - | .setMappingPackedWord _ key _ _ value - | .setMappingUint _ key value - | .setStructMember _ key _ value => - collectAxiomatizedExprPrimitives key ++ collectAxiomatizedExprPrimitives value - | .setMappingChain _ keys value => - keys.flatMap collectAxiomatizedExprPrimitives ++ collectAxiomatizedExprPrimitives value - | .setMapping2 _ key1 key2 value - | .setMapping2Word _ key1 key2 _ value - | .setStructMember2 _ key1 key2 _ value => - collectAxiomatizedExprPrimitives key1 ++ collectAxiomatizedExprPrimitives key2 ++ - collectAxiomatizedExprPrimitives value - | .ite cond thenBr elseBr => - collectAxiomatizedExprPrimitives cond ++ thenBr.flatMap collectAxiomatizedStmtPrimitives ++ - elseBr.flatMap collectAxiomatizedStmtPrimitives - | .forEach _ count body => - collectAxiomatizedExprPrimitives count ++ body.flatMap collectAxiomatizedStmtPrimitives - | .unsafeBlock _ body => - body.flatMap collectAxiomatizedStmtPrimitives - | .matchAdt _ scrutinee branches => - collectAxiomatizedExprPrimitives scrutinee ++ - branches.flatMap fun (_, _, body) => body.flatMap collectAxiomatizedStmtPrimitives - | .emit _ args - | .internalCall _ args - | .externalCallBind _ _ args | .tryExternalCallBind _ _ _ args - | .returnValues args - | .ecm _ args - | .internalCallAssign _ _ args => - args.flatMap collectAxiomatizedExprPrimitives - | .rawLog topics dataOffset dataSize => - topics.flatMap collectAxiomatizedExprPrimitives ++ collectAxiomatizedExprPrimitives dataOffset ++ - collectAxiomatizedExprPrimitives dataSize - | .returnArray _ - | .returnBytes _ - | .returnStorageWords _ - | .revertReturndata - | .stop => - [] - private def collectLowLevelMechanicsFromStmts (stmts : List Stmt) : List String := - dedupPreserve (stmts.flatMap collectLowLevelStmtMechanics) + dedupPreserve <| + Stmt.foldList + (fun acc _ md => + acc ++ md.lowLevelMechanics.map LowLevelMechanic.toReportString ++ + md.subexpressions.flatMap collectLowLevelExprMechanics) + [] + stmts private def collectAxiomatizedPrimitivesFromStmts (stmts : List Stmt) : List String := - dedupPreserve (stmts.flatMap collectAxiomatizedStmtPrimitives) + dedupPreserve <| + Stmt.foldList + (fun acc _ md => acc ++ md.subexpressions.flatMap collectAxiomatizedExprPrimitives) + [] + stmts private def isUnsafeBoundaryMechanic (mechanic : String) : Bool := match mechanic with @@ -305,7 +184,7 @@ private def isUnsafeBoundaryMechanic (mechanic : String) : Bool := def collectUnsafeBoundaryMechanicsFromStmts (stmts : List Stmt) : List String := dedupPreserve ((collectLowLevelMechanicsFromStmts stmts).filter isUnsafeBoundaryMechanic) -/-- Like `collectLowLevelStmtMechanics` but skips `unsafeBlock` bodies — +/-- Like `collectLowLevelMechanicsFromStmts` but skips `unsafeBlock` bodies — returns only mechanics that appear *outside* any `unsafe` wrapper. -/ private partial def collectUnguardedLowLevelStmtMechanics : Stmt → List String | .letVar _ value @@ -366,6 +245,8 @@ private partial def collectUnguardedLowLevelStmtMechanics : Stmt → List String args.flatMap collectLowLevelExprMechanics | .rawLog topics dataOffset dataSize => topics.flatMap collectLowLevelExprMechanics ++ collectLowLevelExprMechanics dataOffset ++ collectLowLevelExprMechanics dataSize + | .unsafeYul _ => + [] | .returnArray _ | .returnBytes _ | .returnStorageWords _ @@ -381,20 +262,8 @@ private def collectUnguardedLowLevelMechanicsFromStmts (stmts : List Stmt) : Lis def collectUnguardedUnsafeBoundaryMechanicsFromStmts (stmts : List Stmt) : List String := dedupPreserve ((collectUnguardedLowLevelMechanicsFromStmts stmts).filter isUnsafeBoundaryMechanic) -/-- Collect `unsafe "reason" do` block reason strings from a statement, recursing into branches. -/ -private partial def collectUnsafeBlockReasonsInStmt : Stmt → List String - | .unsafeBlock reason body => - [reason] ++ body.flatMap collectUnsafeBlockReasonsInStmt - | .ite _ thenBr elseBr => - thenBr.flatMap collectUnsafeBlockReasonsInStmt ++ elseBr.flatMap collectUnsafeBlockReasonsInStmt - | .forEach _ _ body => - body.flatMap collectUnsafeBlockReasonsInStmt - | .matchAdt _ _ branches => - branches.flatMap fun (_, _, body) => body.flatMap collectUnsafeBlockReasonsInStmt - | _ => [] - private def collectUnsafeBlockReasonsFromStmts (stmts : List Stmt) : List String := - stmts.flatMap collectUnsafeBlockReasonsInStmt + Stmt.foldList (fun acc _ md => acc ++ md.unsafeReasons) [] stmts /-- Collect all `unsafe "reason" do` block reasons used by a spec. -/ def collectUnsafeBlockReasons (spec : CompilationModel) : List String := @@ -481,74 +350,18 @@ private partial def collectEventEmissionExprMechanics : Expr → List String | _ => [] -private partial def collectEventEmissionStmtMechanics : Stmt → List String - | .letVar _ value - | .assignVar _ value - | .setStorage _ value - | .setStorageAddr _ value - | .setStorageWord _ _ value - | .storageArrayPush _ value - | .return value - | .require value _ => - collectEventEmissionExprMechanics value - | .setStorageArrayElement _ index value => - collectEventEmissionExprMechanics index ++ collectEventEmissionExprMechanics value - | .storageArrayPop _ => - [] - | .requireError cond _ args => - collectEventEmissionExprMechanics cond ++ args.flatMap collectEventEmissionExprMechanics - | .revertError _ args => - args.flatMap collectEventEmissionExprMechanics - | .mstore offset value - | .tstore offset value => - collectEventEmissionExprMechanics offset ++ collectEventEmissionExprMechanics value - | .calldatacopy destOffset sourceOffset size - | .returndataCopy destOffset sourceOffset size => - collectEventEmissionExprMechanics destOffset ++ collectEventEmissionExprMechanics sourceOffset ++ - collectEventEmissionExprMechanics size - | .setMapping _ key value - | .setMappingWord _ key _ value - | .setMappingPackedWord _ key _ _ value - | .setMappingUint _ key value - | .setStructMember _ key _ value => - collectEventEmissionExprMechanics key ++ collectEventEmissionExprMechanics value - | .setMappingChain _ keys value => - keys.flatMap collectEventEmissionExprMechanics ++ collectEventEmissionExprMechanics value - | .setMapping2 _ key1 key2 value - | .setMapping2Word _ key1 key2 _ value - | .setStructMember2 _ key1 key2 _ value => - collectEventEmissionExprMechanics key1 ++ collectEventEmissionExprMechanics key2 ++ - collectEventEmissionExprMechanics value - | .ite cond thenBr elseBr => - collectEventEmissionExprMechanics cond ++ - thenBr.flatMap collectEventEmissionStmtMechanics ++ - elseBr.flatMap collectEventEmissionStmtMechanics - | .forEach _ count body => - collectEventEmissionExprMechanics count ++ body.flatMap collectEventEmissionStmtMechanics - | .unsafeBlock _ body => - body.flatMap collectEventEmissionStmtMechanics - | .matchAdt _ scrutinee branches => - collectEventEmissionExprMechanics scrutinee ++ - branches.flatMap fun (_, _, body) => body.flatMap collectEventEmissionStmtMechanics - | .emit _ args - | .internalCall _ args - | .externalCallBind _ _ args | .tryExternalCallBind _ _ _ args - | .returnValues args - | .ecm _ args - | .internalCallAssign _ _ args => - args.flatMap collectEventEmissionExprMechanics - | .rawLog topics dataOffset dataSize => - ["rawLog"] ++ topics.flatMap collectEventEmissionExprMechanics ++ - collectEventEmissionExprMechanics dataOffset ++ collectEventEmissionExprMechanics dataSize - | .returnArray _ - | .returnBytes _ - | .returnStorageWords _ - | .revertReturndata - | .stop => - [] - private def collectEventEmissionMechanicsFromStmts (stmts : List Stmt) : List String := - dedupPreserve (stmts.flatMap collectEventEmissionStmtMechanics) + dedupPreserve <| + Stmt.foldList + (fun acc stmt md => + let direct := + match stmt with + | .rawLog _ _ _ => ["rawLog"] + | .unsafeYul fragment => if fragment.mechanics.contains .rawLog then ["rawLog"] else [] + | _ => [] + acc ++ direct ++ md.subexpressions.flatMap collectEventEmissionExprMechanics) + [] + stmts /-- Collect not-modeled raw event-emission mechanics used by a spec. -/ def collectEventEmissionMechanics (spec : CompilationModel) : List String := @@ -562,7 +375,7 @@ def collectEventEmissionMechanics (spec : CompilationModel) : List String := private def isDeniedLowLevelMechanic (mechanic : String) : Bool := match mechanic with | "call" | "staticcall" | "delegatecall" | "returndataSize" | "returndataCopy" - | "revertReturndata" | "returndataOptionalBoolAt" | "blobbasefee" => true + | "revertReturndata" | "rawRevert" | "returndataOptionalBoolAt" | "blobbasefee" => true | _ => false private def collectDeniedLowLevelMechanicsFromMechanics (mechanics : List String) : List String := @@ -650,77 +463,24 @@ private partial def collectRuntimeIntrospectionExprMechanics : Expr → List Str | _ => [] -private partial def collectRuntimeIntrospectionStmtMechanics : Stmt → List String - | .letVar _ value - | .assignVar _ value - | .setStorage _ value - | .setStorageAddr _ value - | .setStorageWord _ _ value - | .storageArrayPush _ value - | .return value - | .require value _ => - collectRuntimeIntrospectionExprMechanics value - | .setStorageArrayElement _ index value => - collectRuntimeIntrospectionExprMechanics index ++ collectRuntimeIntrospectionExprMechanics value - | .storageArrayPop _ => - [] - | .requireError cond _ args => - collectRuntimeIntrospectionExprMechanics cond ++ args.flatMap collectRuntimeIntrospectionExprMechanics - | .revertError _ args => - args.flatMap collectRuntimeIntrospectionExprMechanics - | .mstore offset value - | .tstore offset value => - collectRuntimeIntrospectionExprMechanics offset ++ collectRuntimeIntrospectionExprMechanics value - | .calldatacopy destOffset sourceOffset size - | .returndataCopy destOffset sourceOffset size => - collectRuntimeIntrospectionExprMechanics destOffset ++ - collectRuntimeIntrospectionExprMechanics sourceOffset ++ - collectRuntimeIntrospectionExprMechanics size - | .setMapping _ key value - | .setMappingWord _ key _ value - | .setMappingPackedWord _ key _ _ value - | .setMappingUint _ key value - | .setStructMember _ key _ value => - collectRuntimeIntrospectionExprMechanics key ++ collectRuntimeIntrospectionExprMechanics value - | .setMappingChain _ keys value => - keys.flatMap collectRuntimeIntrospectionExprMechanics ++ collectRuntimeIntrospectionExprMechanics value - | .setMapping2 _ key1 key2 value - | .setMapping2Word _ key1 key2 _ value - | .setStructMember2 _ key1 key2 _ value => - collectRuntimeIntrospectionExprMechanics key1 ++ collectRuntimeIntrospectionExprMechanics key2 ++ - collectRuntimeIntrospectionExprMechanics value - | .ite cond thenBr elseBr => - collectRuntimeIntrospectionExprMechanics cond ++ - thenBr.flatMap collectRuntimeIntrospectionStmtMechanics ++ - elseBr.flatMap collectRuntimeIntrospectionStmtMechanics - | .forEach _ count body => - collectRuntimeIntrospectionExprMechanics count ++ body.flatMap collectRuntimeIntrospectionStmtMechanics - | .unsafeBlock _ body => - body.flatMap collectRuntimeIntrospectionStmtMechanics - | .matchAdt _ scrutinee branches => - collectRuntimeIntrospectionExprMechanics scrutinee ++ - branches.flatMap fun (_, _, body) => body.flatMap collectRuntimeIntrospectionStmtMechanics - | .emit _ args - | .internalCall _ args - | .returnValues args - | .ecm _ args - | .internalCallAssign _ _ args => - args.flatMap collectRuntimeIntrospectionExprMechanics - | .externalCallBind _ _ args | .tryExternalCallBind _ _ _ args => - args.flatMap collectRuntimeIntrospectionExprMechanics - | .rawLog topics dataOffset dataSize => - topics.flatMap collectRuntimeIntrospectionExprMechanics ++ - collectRuntimeIntrospectionExprMechanics dataOffset ++ - collectRuntimeIntrospectionExprMechanics dataSize - | .returnArray _ - | .returnBytes _ - | .returnStorageWords _ - | .revertReturndata - | .stop => - [] - private def collectRuntimeIntrospectionMechanicsFromStmts (stmts : List Stmt) : List String := - dedupPreserve (stmts.flatMap collectRuntimeIntrospectionStmtMechanics) + dedupPreserve <| + Stmt.foldList + (fun acc stmt md => + let direct := + match stmt with + | .unsafeYul fragment => + fragment.mechanics.filterMap (fun mechanic => + if mechanic == .contractAddress || mechanic == .chainid || + mechanic == .selfBalance || mechanic == .blockNumber || + mechanic == .blobbasefee then + some mechanic.toReportString + else + none) + | _ => [] + acc ++ direct ++ md.subexpressions.flatMap collectRuntimeIntrospectionExprMechanics) + [] + stmts /-- Collect partially modeled runtime-introspection mechanics used by a spec. -/ def collectRuntimeIntrospectionMechanics (spec : CompilationModel) : List String := @@ -835,73 +595,33 @@ example : collectRuntimeIntrospectionExprMechanics arrayElementWordRuntimeIndexS example : collectExternalExprNames arrayElementWordExternalIndexSmoke = ["oracle"] := by native_decide -private partial def collectExternalStmtNames : Stmt → List String - | .letVar _ value - | .assignVar _ value - | .setStorage _ value - | .setStorageAddr _ value - | .setStorageWord _ _ value - | .storageArrayPush _ value - | .return value - | .require value _ => - collectExternalExprNames value - | .setStorageArrayElement _ index value => - collectExternalExprNames index ++ collectExternalExprNames value - | .storageArrayPop _ => - [] - | .requireError cond _ args => - collectExternalExprNames cond ++ args.flatMap collectExternalExprNames - | .revertError _ args => - args.flatMap collectExternalExprNames - | .mstore offset value => - collectExternalExprNames offset ++ collectExternalExprNames value - | .tstore offset value => - collectExternalExprNames offset ++ collectExternalExprNames value - | .calldatacopy destOffset sourceOffset size - | .returndataCopy destOffset sourceOffset size => - collectExternalExprNames destOffset ++ collectExternalExprNames sourceOffset ++ collectExternalExprNames size - | .setMapping _ key value - | .setMappingWord _ key _ value - | .setMappingPackedWord _ key _ _ value - | .setMappingUint _ key value - | .setStructMember _ key _ value => - collectExternalExprNames key ++ collectExternalExprNames value - | .setMappingChain _ keys value => - keys.flatMap collectExternalExprNames ++ collectExternalExprNames value - | .setMapping2 _ key1 key2 value - | .setMapping2Word _ key1 key2 _ value - | .setStructMember2 _ key1 key2 _ value => - collectExternalExprNames key1 ++ collectExternalExprNames key2 ++ collectExternalExprNames value - | .ite cond thenBr elseBr => - collectExternalExprNames cond ++ thenBr.flatMap collectExternalStmtNames ++ elseBr.flatMap collectExternalStmtNames - | .forEach _ count body => - collectExternalExprNames count ++ body.flatMap collectExternalStmtNames - | .unsafeBlock _ body => - body.flatMap collectExternalStmtNames - | .matchAdt _ scrutinee branches => - collectExternalExprNames scrutinee ++ - branches.flatMap fun (_, _, body) => body.flatMap collectExternalStmtNames - | .emit _ args - | .internalCall _ args - | .returnValues args - | .ecm _ args - | .internalCallAssign _ _ args => - args.flatMap collectExternalExprNames - | .externalCallBind _ externalName args => - externalName :: args.flatMap collectExternalExprNames - | .tryExternalCallBind _ _ externalName args => - externalName :: args.flatMap collectExternalExprNames - | .rawLog topics dataOffset dataSize => - topics.flatMap collectExternalExprNames ++ collectExternalExprNames dataOffset ++ collectExternalExprNames dataSize - | .returnArray _ - | .returnBytes _ - | .returnStorageWords _ - | .revertReturndata - | .stop => - [] +private def stmtAxiomatizedArgSmoke : Stmt := + Stmt.mstore (Expr.keccak256 (Expr.literal 0) (Expr.literal 64)) (Expr.literal 32) + +private def stmtRuntimeArgSmoke : Stmt := + Stmt.mstore Expr.blockNumber (Expr.literal 32) + +private def stmtExternalArgSmoke : Stmt := + Stmt.mstore (Expr.externalCall "oracle" []) (Expr.literal 32) + +example : collectAxiomatizedPrimitivesFromStmts [stmtAxiomatizedArgSmoke] = ["keccak256"] := by + native_decide + +example : collectRuntimeIntrospectionMechanicsFromStmts [stmtRuntimeArgSmoke] = ["blockNumber"] := by + native_decide private def collectUsedExternalNamesFromStmts (stmts : List Stmt) : List String := - dedupPreserve (stmts.flatMap collectExternalStmtNames) + dedupPreserve <| + Stmt.foldList + (fun acc stmt md => + let direct := + match stmt with + | .externalCallBind _ externalName _ => [externalName] + | .tryExternalCallBind _ _ externalName _ => [externalName] + | _ => [] + acc ++ direct ++ md.subexpressions.flatMap collectExternalExprNames) + [] + stmts private def collectUsedExternalAssumptionsFromStmts (externals : List ExternalFunction) @@ -933,21 +653,18 @@ private def collectUsedExternalNamesByStatus (fun acc ext => if ext.proofStatus == status then acc ++ [ext.name] else acc) [] -private partial def collectUsedEcmModulesInStmt : Stmt → List ECM.ExternalCallModule - | .ecm mod _ => [mod] - | .ite _ thenBr elseBr => - thenBr.flatMap collectUsedEcmModulesInStmt ++ elseBr.flatMap collectUsedEcmModulesInStmt - | .forEach _ _ body => - body.flatMap collectUsedEcmModulesInStmt - | .unsafeBlock _ body => - body.flatMap collectUsedEcmModulesInStmt - | .matchAdt _ _ branches => - branches.flatMap fun (_, _, body) => body.flatMap collectUsedEcmModulesInStmt - | _ => - [] +example : collectUsedExternalNamesFromStmts [stmtExternalArgSmoke] = ["oracle"] := by + native_decide private def collectUsedEcmModulesFromStmts (stmts : List Stmt) : List ECM.ExternalCallModule := - dedupEcmModules (stmts.flatMap collectUsedEcmModulesInStmt) + dedupEcmModules <| + Stmt.foldList + (fun acc stmt _ => + match stmt with + | .ecm mod _ => acc ++ [mod] + | _ => acc) + [] + stmts /-- Collect ECM modules that are actually referenced by the spec, including constructor bodies. This shared view keeps machine-readable reports and @@ -969,8 +686,9 @@ private def collectUsedEcmModuleNamesByStatus private def collectLocalObligationsFromStmts (obligations : List LocalObligation) - (_stmts : List Stmt) : List LocalObligation := - obligations + (stmts : List Stmt) : List LocalObligation := + dedupLocalObligations + (obligations ++ Stmt.foldList (fun acc _ md => acc ++ md.localObligations) [] stmts) private def collectConstructorLocalObligations (spec : CompilationModel) : List LocalObligation := match spec.constructor with @@ -979,8 +697,16 @@ private def collectConstructorLocalObligations (spec : CompilationModel) : List /-- Collect local proof obligations attached to functions/constructors. -/ def collectLocalObligations (spec : CompilationModel) : List LocalObligation := - let functionObligations := spec.functions.flatMap (·.localObligations) - dedupLocalObligations (collectConstructorLocalObligations spec ++ functionObligations) + let ctorObligations := + match spec.constructor with + | some ctor => collectLocalObligationsFromStmts ctor.localObligations ctor.body + | none => [] + let functionObligations := + spec.functions.flatMap fun fn => collectLocalObligationsFromStmts fn.localObligations fn.body + dedupLocalObligations (ctorObligations ++ functionObligations) + +private def collectUnsafeYulContractsFromStmts (stmts : List Stmt) : List UnsafeYulContract := + Stmt.foldList (fun acc _ md => acc ++ md.unsafeYulContracts) [] stmts private def collectLocalObligationNamesByStatus (spec : CompilationModel) @@ -1027,6 +753,25 @@ private def ecmModuleJson (entry : ECM.ExternalCallModule) : String := ("axioms", jsonArray (entry.axioms.map jsonString)) ] +private def frameSpecJson (frame : FrameSpec) : String := + jsonObject [ + ("localReads", jsonArray (frame.localReads.map jsonString)), + ("localWrites", jsonArray (frame.localWrites.map jsonString)), + ("memoryReads", jsonArray (frame.memoryReads.map jsonString)), + ("memoryWrites", jsonArray (frame.memoryWrites.map jsonString)), + ("storageReads", jsonArray (frame.storageReads.map jsonString)), + ("storageWrites", jsonArray (frame.storageWrites.map jsonString)), + ("transientReads", jsonArray (frame.transientReads.map jsonString)), + ("transientWrites", jsonArray (frame.transientWrites.map jsonString)) + ] + +private def unsafeYulContractJson (contract : UnsafeYulContract) : String := + jsonObject [ + ("name", jsonString contract.name), + ("summary", jsonString contract.summary), + ("frame", frameSpecJson contract.frame) + ] + private def localObligationJson (entry : LocalObligation) : String := jsonObject [ ("name", jsonString entry.name), @@ -1140,6 +885,7 @@ private structure UsageSiteSummary where externals : List ExternalFunction modules : List ECM.ExternalCallModule localObligations : List LocalObligation + unsafeYulContracts : List UnsafeYulContract unsafeBlocks : List String private def ecmAxiomsFromModules (modules : List ECM.ExternalCallModule) : List (String × String) := @@ -1157,6 +903,7 @@ private def siteHasTrustSurface !(collectUsedExternalAssumptionsFromStmts externals stmts).isEmpty || !(collectUsedEcmModulesFromStmts stmts).isEmpty || !(collectLocalObligationsFromStmts localObligations stmts).isEmpty || + !(collectUnsafeYulContractsFromStmts stmts).isEmpty || !(collectUnsafeBlockReasonsFromStmts stmts).isEmpty private def usageSiteSummary @@ -1173,6 +920,7 @@ private def usageSiteSummary let siteExternals := collectUsedExternalAssumptionsFromStmts spec.externals stmts let siteModules := collectUsedEcmModulesFromStmts stmts let siteLocalObligations := collectLocalObligationsFromStmts localObligations stmts + let siteUnsafeYulContracts := collectUnsafeYulContractsFromStmts stmts let siteUnsafeBlocks := collectUnsafeBlockReasonsFromStmts stmts { kind := kind name := name @@ -1184,6 +932,7 @@ private def usageSiteSummary externals := siteExternals modules := siteModules localObligations := siteLocalObligations + unsafeYulContracts := siteUnsafeYulContracts unsafeBlocks := siteUnsafeBlocks } private def collectUsageSiteSummaries (spec : CompilationModel) : List UsageSiteSummary := @@ -1219,6 +968,7 @@ private def usageSitesJson (spec : CompilationModel) : String := ("axiomatizedPrimitives", jsonArray (site.primitives.map jsonString)), ("proofStatus", proofStatusJsonForSite site.primitives site.externals site.modules site.localObligations), ("localObligations", jsonArray (site.localObligations.map localObligationJson)), + ("unsafeYulContracts", jsonArray (site.unsafeYulContracts.map unsafeYulContractJson)), ("unsafeBlocks", jsonArray (site.unsafeBlocks.map jsonString)), ("hasUncheckedDependencies", if hasUncheckedDependenciesForSite site.externals site.modules then "true" else "false"), diff --git a/Compiler/CompilationModel/Types.lean b/Compiler/CompilationModel/Types.lean index ae39fcab8..0f730f1db 100644 --- a/Compiler/CompilationModel/Types.lean +++ b/Compiler/CompilationModel/Types.lean @@ -291,6 +291,50 @@ structure ExternalFunction where linkMode : ForeignLinkMode := .objectLinked deriving Repr +structure YulState where + vars : List (String × Nat) := [] + memory : Nat → Nat := fun _ => 0 + storage : Nat → Nat := fun _ => 0 + transientStorage : Nat → Nat := fun _ => 0 + returndata : List Nat := [] + reverted : Bool := false + +structure FrameSpec where + localReads : List String := [] + localWrites : List String := [] + memoryReads : List String := [] + memoryWrites : List String := [] + storageReads : List String := [] + storageWrites : List String := [] + transientReads : List String := [] + transientWrites : List String := [] + deriving Repr, BEq, Inhabited + +/-- Structured refinement contract for localized unsafe Yul boundaries. + The predicates give proof code a real target while `summary` remains the + stable human-readable report text. -/ +structure UnsafeYulContract where + name : String + summary : String + pre : YulState → Prop + post : YulState → YulState → Prop + frame : FrameSpec := {} + +instance : Repr UnsafeYulContract where + reprPrec contract prec := + reprPrec (contract.name, contract.summary, contract.frame) prec + +namespace UnsafeYulContract + +def rawRevert (name summary : String) : UnsafeYulContract := + { name := name + summary := summary + pre := fun _ => True + post := fun _ after => after.reverted = true + frame := { memoryReads := ["revertPayload"] } } + +end UnsafeYulContract + structure LocalObligation where name : String /-- User-supplied summary of the local refinement contract that must hold @@ -300,6 +344,271 @@ structure LocalObligation where proofStatus : Compiler.ProofStatus := .assumed deriving Repr +/-- Coarse statement termination classification used by generic statement + metadata. `mayTerminate` covers handwritten/raw Yul fragments unless a + caller supplies a more precise contract. -/ +inductive StmtTermination where + | fallsThrough + | alwaysTerminates + | mayTerminate + deriving Repr, BEq + +/-- Finer control-flow summary for statements and statement lists. + This intentionally coexists with `StmtTermination` while callers migrate: + the old field answers the coarse "can execution continue?" question, while + this summary records which terminal behaviors may occur. -/ +structure ControlFlowSummary where + mayFallThrough : Bool := true + mayRevert : Bool := false + mayReturn : Bool := false + mayStop : Bool := false + deriving Repr, BEq, Inhabited + +namespace ControlFlowSummary + +def fallsThrough : ControlFlowSummary := {} + +/-- Empty control-flow set, used as the identity when unioning alternatives. -/ +def noPaths : ControlFlowSummary := + { mayFallThrough := false, mayRevert := false, mayReturn := false, mayStop := false } + +def mayReverting : ControlFlowSummary := + { mayFallThrough := true, mayRevert := true } + +def reverts : ControlFlowSummary := + { mayFallThrough := false, mayRevert := true } + +def returns : ControlFlowSummary := + { mayFallThrough := false, mayReturn := true } + +def stops : ControlFlowSummary := + { mayFallThrough := false, mayStop := true } + +def unknown : ControlFlowSummary := + { mayFallThrough := true, mayRevert := true, mayReturn := true, mayStop := true } + +def union (a b : ControlFlowSummary) : ControlFlowSummary := + { mayFallThrough := a.mayFallThrough || b.mayFallThrough + mayRevert := a.mayRevert || b.mayRevert + mayReturn := a.mayReturn || b.mayReturn + mayStop := a.mayStop || b.mayStop } + +/-- Sequential composition: `b` is reachable only along fall-through paths of `a`. -/ +def seq (a b : ControlFlowSummary) : ControlFlowSummary := + { mayFallThrough := a.mayFallThrough && b.mayFallThrough + mayRevert := a.mayRevert || (a.mayFallThrough && b.mayRevert) + mayReturn := a.mayReturn || (a.mayFallThrough && b.mayReturn) + mayStop := a.mayStop || (a.mayFallThrough && b.mayStop) } + +/-- True when every path terminates specifically through a Solidity-style +return or revert. A raw `stop` also halts execution, but it does not produce the +return data required by functions that declare return values. -/ +def alwaysReturnsOrReverts (cf : ControlFlowSummary) : Bool := + !cf.mayFallThrough && !cf.mayStop && (cf.mayReturn || cf.mayRevert) + +def fromTermination : StmtTermination → ControlFlowSummary + | .fallsThrough => fallsThrough + | .alwaysTerminates => unknown + | .mayTerminate => unknown + +end ControlFlowSummary + +/-- Scope effects exposed by the generic statement metadata layer. -/ +structure StmtScopeEffects where + bindNames : List String := [] + assignNames : List String := [] + storageWrites : List String := [] + deriving Repr, Inhabited + +namespace StmtScopeEffects + +def merge (a b : StmtScopeEffects) : StmtScopeEffects := + { bindNames := a.bindNames ++ b.bindNames + assignNames := a.assignNames ++ b.assignNames + storageWrites := a.storageWrites ++ b.storageWrites } + +end StmtScopeEffects + +mutual +/-- Conservative scan for storage-like writes inside raw Yul expressions. + Transient `tstore` is intentionally classified as a storage write for + effect validation because it mutates EVM transaction-local state. -/ +partial def yulExprWritesStorage : YulExpr → Bool + | .call func args => + func == "sstore" || func == "tstore" || yulExprListWritesStorage args + | _ => false + +partial def yulExprListWritesStorage : List YulExpr → Bool + | [] => false + | expr :: rest => + yulExprWritesStorage expr || yulExprListWritesStorage rest +end + +mutual +/-- Conservative scope/effect derivation for embedded Yul AST fragments. + This is the single source of truth used by both imported-Yul construction + and unsafe-Yul validation, so generated declarations and validation checks + cannot drift apart. -/ +partial def yulStmtScopeEffects : YulStmt → StmtScopeEffects + | .comment _ | .leave => + {} + | .let_ name value => + { bindNames := [name] + storageWrites := if yulExprWritesStorage value then [""] else [] } + | .letMany names value => + { bindNames := names + storageWrites := if yulExprWritesStorage value then [""] else [] } + | .assign name value => + { assignNames := [name] + storageWrites := if yulExprWritesStorage value then [""] else [] } + | .expr expr => + { storageWrites := if yulExprWritesStorage expr then [""] else [] } + | .if_ cond body => + let bodyEffects := yulStmtListScopeEffects body + { bodyEffects with + storageWrites := + (if yulExprWritesStorage cond then [""] else []) ++ + bodyEffects.storageWrites } + | .for_ init cond post body => + let initEffects := yulStmtListScopeEffects init + let postEffects := yulStmtListScopeEffects post + let bodyEffects := yulStmtListScopeEffects body + { bindNames := initEffects.bindNames ++ postEffects.bindNames ++ bodyEffects.bindNames + assignNames := initEffects.assignNames ++ postEffects.assignNames ++ bodyEffects.assignNames + storageWrites := + initEffects.storageWrites ++ + (if yulExprWritesStorage cond then [""] else []) ++ + postEffects.storageWrites ++ bodyEffects.storageWrites } + | .switch expr cases default => + let casesEffects := + cases.foldl + (fun acc (_, body) => StmtScopeEffects.merge acc (yulStmtListScopeEffects body)) + ({} : StmtScopeEffects) + let defaultEffects := + match default with + | none => ({} : StmtScopeEffects) + | some body => yulStmtListScopeEffects body + { bindNames := casesEffects.bindNames ++ defaultEffects.bindNames + assignNames := casesEffects.assignNames ++ defaultEffects.assignNames + storageWrites := + (if yulExprWritesStorage expr then [""] else []) ++ + casesEffects.storageWrites ++ defaultEffects.storageWrites } + | .block stmts => + yulStmtListScopeEffects stmts + | .funcDef name _params _rets body => + let bodyEffects := yulStmtListScopeEffects body + { bindNames := [name] + assignNames := [] + storageWrites := bodyEffects.storageWrites } + +partial def yulStmtListScopeEffects : List YulStmt → StmtScopeEffects + | [] => {} + | stmt :: rest => + StmtScopeEffects.merge (yulStmtScopeEffects stmt) (yulStmtListScopeEffects rest) +end + +/-- Typed trust-report mechanics emitted by low-level statements and raw Yul fragments. + JSON and human-readable reports still render these through `toReportString`, + preserving the existing public report format while keeping the model boundary + from depending on ad-hoc string literals. -/ +inductive LowLevelMechanic where + | call + | staticcall + | delegatecall + | returndataSize + | returndataCopy + | revertReturndata + | rawRevert + | returndataOptionalBoolAt + | blobbasefee + | mload + | mstore + | calldataload + | calldatacopy + | extcodesize + | tload + | tstore + | rawLog + | contractAddress + | chainid + | selfBalance + | blockNumber + | storageWrite + deriving Repr, BEq, Inhabited + +namespace LowLevelMechanic + +def toReportString : LowLevelMechanic → String + | .call => "call" + | .staticcall => "staticcall" + | .delegatecall => "delegatecall" + | .returndataSize => "returndataSize" + | .returndataCopy => "returndataCopy" + | .revertReturndata => "revertReturndata" + | .rawRevert => "rawRevert" + | .returndataOptionalBoolAt => "returndataOptionalBoolAt" + | .blobbasefee => "blobbasefee" + | .mload => "mload" + | .mstore => "mstore" + | .calldataload => "calldataload" + | .calldatacopy => "calldatacopy" + | .extcodesize => "extcodesize" + | .tload => "tload" + | .tstore => "tstore" + | .rawLog => "rawLog" + | .contractAddress => "contractAddress" + | .chainid => "chainid" + | .selfBalance => "selfBalance" + | .blockNumber => "blockNumber" + | .storageWrite => "storageWrite" + +instance : ToString LowLevelMechanic where + toString := toReportString + +end LowLevelMechanic + +/-- Typed handwritten Yul fragment. This is intentionally not just a string: + callers provide an EVMYul AST payload plus explicit proof obligations and + trust-surface metadata at the same boundary where the raw fragment enters + the compilation model. -/ +structure UnsafeYulFragment where + label : String + stmts : List YulStmt + obligations : List LocalObligation + contracts : List UnsafeYulContract := [] + mechanics : List LowLevelMechanic := [] + scopeEffects : StmtScopeEffects := {} + termination : StmtTermination := .mayTerminate + controlFlow : ControlFlowSummary := .unknown + deriving Repr + +/-- Backwards-friendly name for explicitly trusted raw Yul fragments. -/ +abbrev RawYul := UnsafeYulFragment + +namespace UnsafeYulFragment + +/-- Helper constructor for the single Yul `revert(offset, size)` instruction. + + Prefer this through `Stmt.unsafeYul` for one-off raw instruction escapes. + Stable typed primitives such as `Stmt.mstore` and `Stmt.calldatacopy` + remain first-class statements because Verity has explicit semantics and + proof/audit surfaces for them; ad-hoc raw instructions should carry their + trust metadata at the `UnsafeYulFragment` boundary instead of growing `Stmt`. + Raw memory reverts are intentionally modeled as unsafe Yul fragments rather + than first-class `Stmt` constructors. -/ +def rawRevert (offset size : YulExpr) (obligation : LocalObligation) + (label : String := obligation.name) : UnsafeYulFragment := { + label := label + stmts := [YulStmt.expr (YulExpr.call "revert" [offset, size])] + obligations := [obligation] + contracts := [UnsafeYulContract.rawRevert obligation.name obligation.obligation] + mechanics := [.rawRevert] + termination := .alwaysTerminates + controlFlow := .reverts +} + +end UnsafeYulFragment + /-! ### ADT Type Definitions (#1727, Phase 5 Step 5b) @@ -630,6 +939,10 @@ inductive Stmt Marks a region where restricted operations (Step 6b) are permitted. The reason string is preserved for trust reporting (Step 6c). -/ | unsafeBlock (reason : String) (body : List Stmt) + /-- Typed handwritten Yul fragment with localized proof obligations and + trust-surface metadata. Lowering to EVMYul AST is centralized in + `CompilationModel.unsafeYulToEVMYul`. -/ + | unsafeYul (fragment : UnsafeYulFragment) /-- Pattern match on an ADT value: `matchAdt adtName scrutinee branches`. Each branch is `(variantName, boundVarNames, body)`. Compiles to `YulStmt.switch` on the tag byte. (#1727 Step 5b) -/ @@ -637,6 +950,198 @@ inductive Stmt (branches : List (String × List String × List Stmt)) deriving Repr +/-- Common statement metadata. New `Stmt` constructors should be represented + here once, then generic traversals and collectors can consume this surface + instead of duplicating constructor-by-constructor walks. -/ +structure StmtMetadata where + subexpressions : List Expr := [] + termination : StmtTermination := .fallsThrough + controlFlow : ControlFlowSummary := {} + lowLevelMechanics : List LowLevelMechanic := [] + scopeEffects : StmtScopeEffects := {} + localObligations : List LocalObligation := [] + unsafeYulContracts : List UnsafeYulContract := [] + unsafeReasons : List String := [] + deriving Repr + +namespace Stmt + +def childLists : Stmt → List (List Stmt) + | .ite _ thenBranch elseBranch => [thenBranch, elseBranch] + | .forEach _ _ body => [body] + | .unsafeBlock _ body => [body] + | .matchAdt _ _ branches => branches.map (fun (_, _, body) => body) + | _ => [] + +def directMetadata : Stmt → StmtMetadata + | .letVar name value => + { subexpressions := [value], scopeEffects := { bindNames := [name] } } + | .assignVar name value => + { subexpressions := [value], scopeEffects := { assignNames := [name] } } + | .setStorage field value | .setStorageAddr field value => + { subexpressions := [value], scopeEffects := { storageWrites := [field] } } + | .setStorageWord field _ value => + { subexpressions := [value], scopeEffects := { storageWrites := [field] } } + | .storageArrayPush field value => + { subexpressions := [value], scopeEffects := { storageWrites := [field] } } + | .storageArrayPop field => + { scopeEffects := { storageWrites := [field] } } + | .setStorageArrayElement field index value => + { subexpressions := [index, value], scopeEffects := { storageWrites := [field] } } + | .setMapping field key value | .setMappingWord field key _ value + | .setMappingPackedWord field key _ _ value | .setMappingUint field key value + | .setStructMember field key _ value => + { subexpressions := [key, value], scopeEffects := { storageWrites := [field] } } + | .setMappingChain field keys value => + { subexpressions := keys ++ [value], scopeEffects := { storageWrites := [field] } } + | .setMapping2 field key1 key2 value | .setMapping2Word field key1 key2 _ value + | .setStructMember2 field key1 key2 _ value => + { subexpressions := [key1, key2, value], scopeEffects := { storageWrites := [field] } } + | .require cond _ => + { subexpressions := [cond], termination := .mayTerminate, controlFlow := .mayReverting } + | .requireError cond _ args => + { subexpressions := cond :: args, termination := .mayTerminate, controlFlow := .mayReverting } + | .revertError _ args => + { subexpressions := args, termination := .alwaysTerminates, controlFlow := .reverts } + | .return value => + { subexpressions := [value], termination := .alwaysTerminates, controlFlow := .returns } + | .returnValues values => + { subexpressions := values, termination := .alwaysTerminates, controlFlow := .returns } + | .returnArray _ | .returnBytes _ | .returnStorageWords _ => + { termination := .alwaysTerminates, controlFlow := .returns } + | .mstore offset value => + { subexpressions := [offset, value], lowLevelMechanics := [.mstore] } + | .tstore offset value => + { subexpressions := [offset, value], lowLevelMechanics := [.tstore] } + | .calldatacopy destOffset sourceOffset size => + { subexpressions := [destOffset, sourceOffset, size], lowLevelMechanics := [.calldatacopy] } + | .returndataCopy destOffset sourceOffset size => + { subexpressions := [destOffset, sourceOffset, size], lowLevelMechanics := [.returndataCopy] } + | .revertReturndata => + { termination := .alwaysTerminates, controlFlow := .reverts, lowLevelMechanics := [.revertReturndata] } + | .stop => + { termination := .alwaysTerminates, controlFlow := .stops } + | .ite cond _ _ => + { subexpressions := [cond], termination := .mayTerminate, controlFlow := .unknown } + | .forEach varName count _ => + { subexpressions := [count], scopeEffects := { bindNames := [varName] } } + | .emit _ args => + { subexpressions := args } + | .internalCall _ args => + { subexpressions := args } + | .internalCallAssign names _ args => + { subexpressions := args, scopeEffects := { bindNames := names } } + | .rawLog topics dataOffset dataSize => + { subexpressions := topics ++ [dataOffset, dataSize] } + | .externalCallBind resultVars _ args => + { subexpressions := args, scopeEffects := { bindNames := resultVars } } + | .tryExternalCallBind successVar resultVars _ args => + { subexpressions := args, scopeEffects := { bindNames := successVar :: resultVars } } + | .ecm mod args => + { subexpressions := args, scopeEffects := { bindNames := mod.resultVars } } + | .unsafeBlock reason _ => + { unsafeReasons := [reason] } + | .unsafeYul fragment => + { termination := fragment.termination + controlFlow := fragment.controlFlow + lowLevelMechanics := fragment.mechanics + scopeEffects := fragment.scopeEffects + localObligations := fragment.obligations + unsafeYulContracts := fragment.contracts + unsafeReasons := [fragment.label] } + | .matchAdt _ scrutinee branches => + { subexpressions := [scrutinee] + termination := .mayTerminate + controlFlow := .unknown + scopeEffects := { bindNames := branches.flatMap (fun (_, names, _) => names) } } + +partial def fold (f : α → Stmt → StmtMetadata → α) (init : α) (stmt : Stmt) : α := + let md := stmt.directMetadata + let acc := f init stmt md + stmt.childLists.foldl + (fun acc childList => childList.foldl (fun inner child => child.fold f inner) acc) + acc + +partial def foldList (f : α → Stmt → StmtMetadata → α) (init : α) (stmts : List Stmt) : α := + stmts.foldl (fun acc stmt => stmt.fold f acc) init + +mutual +partial def controlFlow : Stmt → ControlFlowSummary + | .require _ _ | .requireError _ _ _ => + .mayReverting + | .revertError _ _ | .revertReturndata => + .reverts + | .return _ | .returnValues _ | .returnArray _ | .returnBytes _ | .returnStorageWords _ => + .returns + | .stop => + .stops + | .ite _ thenBranch elseBranch => + ControlFlowSummary.union (controlFlowList thenBranch) (controlFlowList elseBranch) + | .forEach _ _ body => + -- Loops are bounded and may execute zero times, so the loop itself can fall through + -- even if some body path returns or reverts. + ControlFlowSummary.union .fallsThrough (controlFlowList body) + | .unsafeBlock _ body => + controlFlowList body + | .matchAdt _ _ branches => + controlFlowBranches branches + | .unsafeYul fragment => + fragment.controlFlow + | _ => + .fallsThrough + +partial def controlFlowList : List Stmt → ControlFlowSummary + | [] => .fallsThrough + | stmt :: rest => + ControlFlowSummary.seq (controlFlow stmt) (controlFlowList rest) + +partial def controlFlowBranches : List (String × List String × List Stmt) → ControlFlowSummary + | [] => .noPaths + | (_, _, body) :: rest => + ControlFlowSummary.union (controlFlowList body) (controlFlowBranches rest) +end + +example : (controlFlowList [Stmt.return (Expr.literal 1), Stmt.stop]).mayStop = false := by + native_decide + +example : (controlFlow (Stmt.require (Expr.literal 1) "ok")).mayRevert = true := by + native_decide + +partial def metadataDeep (stmt : Stmt) : StmtMetadata := + stmt.fold + (fun acc _ md => + { subexpressions := acc.subexpressions ++ md.subexpressions + termination := if acc.termination == .alwaysTerminates then .alwaysTerminates else md.termination + controlFlow := ControlFlowSummary.union acc.controlFlow md.controlFlow + lowLevelMechanics := acc.lowLevelMechanics ++ md.lowLevelMechanics + scopeEffects := + { bindNames := acc.scopeEffects.bindNames ++ md.scopeEffects.bindNames + assignNames := acc.scopeEffects.assignNames ++ md.scopeEffects.assignNames + storageWrites := acc.scopeEffects.storageWrites ++ md.scopeEffects.storageWrites } + localObligations := acc.localObligations ++ md.localObligations + unsafeYulContracts := acc.unsafeYulContracts ++ md.unsafeYulContracts + unsafeReasons := acc.unsafeReasons ++ md.unsafeReasons }) + {} + +def metadataListDeep (stmts : List Stmt) : StmtMetadata := + foldList + (fun acc _ md => + { subexpressions := acc.subexpressions ++ md.subexpressions + termination := if acc.termination == .alwaysTerminates then .alwaysTerminates else md.termination + controlFlow := ControlFlowSummary.union acc.controlFlow md.controlFlow + lowLevelMechanics := acc.lowLevelMechanics ++ md.lowLevelMechanics + scopeEffects := + { bindNames := acc.scopeEffects.bindNames ++ md.scopeEffects.bindNames + assignNames := acc.scopeEffects.assignNames ++ md.scopeEffects.assignNames + storageWrites := acc.scopeEffects.storageWrites ++ md.scopeEffects.storageWrites } + localObligations := acc.localObligations ++ md.localObligations + unsafeYulContracts := acc.unsafeYulContracts ++ md.unsafeYulContracts + unsafeReasons := acc.unsafeReasons ++ md.unsafeReasons }) + {} + stmts + +end Stmt + structure FunctionSpec where name : String params : List Param diff --git a/Compiler/CompilationModel/UsageAnalysis.lean b/Compiler/CompilationModel/UsageAnalysis.lean index 4e68848ff..39a98ed76 100644 --- a/Compiler/CompilationModel/UsageAnalysis.lean +++ b/Compiler/CompilationModel/UsageAnalysis.lean @@ -4,33 +4,19 @@ namespace Compiler.CompilationModel mutual def collectStmtBindNames : Stmt → List String - | Stmt.letVar name _ => [name] - | Stmt.ite _ thenBranch elseBranch => + | .letVar name _ => [name] + | .internalCallAssign names _ _ => names + | .externalCallBind resultVars _ _ => resultVars + | .tryExternalCallBind successVar resultVars _ _ => successVar :: resultVars + | .ecm mod _ => mod.resultVars + | .ite _ thenBranch elseBranch => collectStmtListBindNames thenBranch ++ collectStmtListBindNames elseBranch - | Stmt.forEach varName _ body => - varName :: collectStmtListBindNames body - | Stmt.unsafeBlock _ body => - collectStmtListBindNames body - | Stmt.matchAdt _ _ branches => - collectMatchBranchBindNames branches - | Stmt.internalCallAssign names _ _ => names - | Stmt.externalCallBind resultVars _ _ => resultVars - | Stmt.tryExternalCallBind successVar resultVars _ _ => successVar :: resultVars - | Stmt.ecm mod _ => mod.resultVars - -- Statements that never bind new names. - | Stmt.assignVar _ _ | Stmt.setStorage _ _ | Stmt.setStorageAddr _ _ | Stmt.setStorageWord _ _ _ - | Stmt.storageArrayPush _ _ | Stmt.storageArrayPop _ | Stmt.setStorageArrayElement _ _ _ - | Stmt.return _ - | Stmt.setMapping _ _ _ | Stmt.setMappingWord _ _ _ _ | Stmt.setMappingPackedWord _ _ _ _ _ | Stmt.setMappingUint _ _ _ - | Stmt.setMappingChain _ _ _ - | Stmt.setMapping2 _ _ _ _ | Stmt.setMapping2Word _ _ _ _ _ - | Stmt.setStructMember _ _ _ _ | Stmt.setStructMember2 _ _ _ _ _ - | Stmt.require _ _ | Stmt.requireError _ _ _ | Stmt.revertError _ _ - | Stmt.returnValues _ | Stmt.returnArray _ | Stmt.returnBytes _ | Stmt.returnStorageWords _ - | Stmt.mstore _ _ | Stmt.tstore _ _ | Stmt.calldatacopy _ _ _ | Stmt.returndataCopy _ _ _ | Stmt.revertReturndata | Stmt.stop - | Stmt.emit _ _ | Stmt.internalCall _ _ | Stmt.rawLog _ _ _ => - [] -termination_by s => sizeOf s + | .forEach varName _ body => varName :: collectStmtListBindNames body + | .unsafeBlock _ body => collectStmtListBindNames body + | .matchAdt _ _ branches => collectMatchBranchBindNames branches + | .unsafeYul fragment => fragment.scopeEffects.bindNames + | _ => [] +termination_by stmt => sizeOf stmt decreasing_by all_goals simp_wf; all_goals omega def collectStmtListBindNames : List Stmt → List String @@ -50,29 +36,15 @@ end mutual def collectStmtAssignedNames : Stmt → List String - | Stmt.assignVar name _ => [name] - | Stmt.ite _ thenBranch elseBranch => + | .assignVar name _ => [name] + | .unsafeBlock _ body => collectStmtListAssignedNames body + | .ite _ thenBranch elseBranch => collectStmtListAssignedNames thenBranch ++ collectStmtListAssignedNames elseBranch - | Stmt.forEach _ _ body => - collectStmtListAssignedNames body - | Stmt.unsafeBlock _ body => - collectStmtListAssignedNames body - | Stmt.matchAdt _ _ branches => - collectMatchBranchAssignedNames branches - | Stmt.letVar _ _ | Stmt.setStorage _ _ | Stmt.setStorageAddr _ _ | Stmt.setStorageWord _ _ _ - | Stmt.storageArrayPush _ _ | Stmt.storageArrayPop _ | Stmt.setStorageArrayElement _ _ _ - | Stmt.return _ - | Stmt.setMapping _ _ _ | Stmt.setMappingWord _ _ _ _ | Stmt.setMappingPackedWord _ _ _ _ _ | Stmt.setMappingUint _ _ _ - | Stmt.setMappingChain _ _ _ - | Stmt.setMapping2 _ _ _ _ | Stmt.setMapping2Word _ _ _ _ _ - | Stmt.setStructMember _ _ _ _ | Stmt.setStructMember2 _ _ _ _ _ - | Stmt.require _ _ | Stmt.requireError _ _ _ | Stmt.revertError _ _ - | Stmt.returnValues _ | Stmt.returnArray _ | Stmt.returnBytes _ | Stmt.returnStorageWords _ - | Stmt.mstore _ _ | Stmt.tstore _ _ | Stmt.calldatacopy _ _ _ | Stmt.returndataCopy _ _ _ | Stmt.revertReturndata | Stmt.stop - | Stmt.emit _ _ | Stmt.internalCall _ _ | Stmt.internalCallAssign _ _ _ - | Stmt.rawLog _ _ _ | Stmt.externalCallBind _ _ _ | Stmt.tryExternalCallBind _ _ _ _ | Stmt.ecm _ _ => - [] -termination_by s => sizeOf s + | .forEach _ _ body => collectStmtListAssignedNames body + | .matchAdt _ _ branches => collectMatchBranchAssignedNames branches + | .unsafeYul fragment => fragment.scopeEffects.assignNames + | _ => [] +termination_by stmt => sizeOf stmt decreasing_by all_goals simp_wf; all_goals omega def collectStmtListAssignedNames : List Stmt → List String @@ -277,9 +249,12 @@ def stmtUsesArrayElementKind (includePlain includeWord : Bool) : Stmt → Bool exprListUsesArrayElementKind includePlain includeWord args | Stmt.ecm _ args => exprListUsesArrayElementKind includePlain includeWord args - | Stmt.returnArray _ | Stmt.returnBytes _ | Stmt.returnStorageWords _ + | Stmt.returnArray _ | Stmt.returnBytes _ | Stmt.returnStorageWords _ => + false | Stmt.revertReturndata | Stmt.stop => false + | Stmt.unsafeYul _ => + false termination_by s => sizeOf s decreasing_by all_goals simp_wf; all_goals omega @@ -432,9 +407,12 @@ def stmtUsesArrayElement : Stmt → Bool exprListUsesArrayElement topics || exprUsesArrayElement dataOffset || exprUsesArrayElement dataSize | Stmt.externalCallBind _ _ args | Stmt.tryExternalCallBind _ _ _ args | Stmt.ecm _ args => exprListUsesArrayElement args - | Stmt.returnArray _ | Stmt.returnBytes _ | Stmt.returnStorageWords _ + | Stmt.returnArray _ | Stmt.returnBytes _ | Stmt.returnStorageWords _ => + false | Stmt.revertReturndata | Stmt.stop => false + | Stmt.unsafeYul _ => + false termination_by s => sizeOf s decreasing_by all_goals simp_wf; all_goals omega @@ -637,9 +615,12 @@ def stmtUsesParamDynamicHeadWord : Stmt → Bool exprListUsesParamDynamicHeadWord topics || exprUsesParamDynamicHeadWord dataOffset || exprUsesParamDynamicHeadWord dataSize - | Stmt.returnArray _ | Stmt.returnBytes _ | Stmt.returnStorageWords _ + | Stmt.returnArray _ | Stmt.returnBytes _ | Stmt.returnStorageWords _ => + false | Stmt.revertReturndata | Stmt.stop => false + | Stmt.unsafeYul _ => + false termination_by s => sizeOf s decreasing_by all_goals simp_wf; all_goals omega @@ -781,9 +762,12 @@ def stmtUsesMulDiv512 : Stmt → Bool | Stmt.rawLog topics dataOffset dataSize => exprListUsesMulDiv512 topics || exprUsesMulDiv512 dataOffset || exprUsesMulDiv512 dataSize - | Stmt.returnArray _ | Stmt.returnBytes _ | Stmt.returnStorageWords _ + | Stmt.returnArray _ | Stmt.returnBytes _ | Stmt.returnStorageWords _ => + false | Stmt.revertReturndata | Stmt.stop => false + | Stmt.unsafeYul _ => + false termination_by s => sizeOf s decreasing_by all_goals simp_wf; all_goals omega @@ -954,9 +938,12 @@ def stmtUsesStorageArrayElement : Stmt → Bool exprListUsesStorageArrayElement topics || exprUsesStorageArrayElement dataOffset || exprUsesStorageArrayElement dataSize | Stmt.ecm _ args => exprListUsesStorageArrayElement args - | Stmt.returnArray _ | Stmt.returnBytes _ | Stmt.returnStorageWords _ + | Stmt.returnArray _ | Stmt.returnBytes _ | Stmt.returnStorageWords _ => + false | Stmt.revertReturndata | Stmt.stop => false + | Stmt.unsafeYul _ => + false termination_by s => sizeOf s decreasing_by all_goals simp_wf; all_goals omega @@ -1107,9 +1094,12 @@ def stmtUsesDynamicBytesEq : Stmt → Bool exprListUsesDynamicBytesEq args | Stmt.rawLog topics dataOffset dataSize => exprListUsesDynamicBytesEq topics || exprUsesDynamicBytesEq dataOffset || exprUsesDynamicBytesEq dataSize - | Stmt.returnArray _ | Stmt.returnBytes _ | Stmt.returnStorageWords _ + | Stmt.returnArray _ | Stmt.returnBytes _ | Stmt.returnStorageWords _ => + false | Stmt.revertReturndata | Stmt.stop => false + | Stmt.unsafeYul _ => + false termination_by s => sizeOf s decreasing_by all_goals simp_wf; all_goals omega diff --git a/Compiler/CompilationModel/Validation.lean b/Compiler/CompilationModel/Validation.lean index 3df3a4928..242d8ba09 100644 --- a/Compiler/CompilationModel/Validation.lean +++ b/Compiler/CompilationModel/Validation.lean @@ -32,6 +32,24 @@ private def firstDuplicateString : List String → Option String | name :: rest => if rest.contains name then some name else firstDuplicateString rest +private def missingDeclaredNames (actual declared : List String) : List String := + actual.foldl + (fun acc name => + if declared.contains name || acc.contains name then acc else acc ++ [name]) + [] + +private def validateUnsafeYulDeclaredScopeEffects (fragment : UnsafeYulFragment) : + Except String Unit := do + let actual := yulStmtListScopeEffects fragment.stmts + let missingBinds := missingDeclaredNames actual.bindNames fragment.scopeEffects.bindNames + if !missingBinds.isEmpty then + throw s!"Compilation error: unsafe Yul fragment '{fragment.label}' under-declares bound local(s): {String.intercalate ", " missingBinds}" + let missingAssigns := missingDeclaredNames actual.assignNames fragment.scopeEffects.assignNames + if !missingAssigns.isEmpty then + throw s!"Compilation error: unsafe Yul fragment '{fragment.label}' under-declares assigned local(s): {String.intercalate ", " missingAssigns}" + if !actual.storageWrites.isEmpty && fragment.scopeEffects.storageWrites.isEmpty then + throw s!"Compilation error: unsafe Yul fragment '{fragment.label}' under-declares storage effects for raw Yul storage write(s)." + private def adtPayloadParamNames (params : List Param) : List String := params.flatMap fun param => match param.ty with @@ -209,40 +227,8 @@ termination_by bs => sizeOf bs decreasing_by all_goals simp_wf; all_goals omega end -mutual - private def stmtListAlwaysReturnsOrReverts : List Stmt → Bool - | [] => false - | stmt :: rest => - if stmtAlwaysReturnsOrReverts stmt then - true - else - stmtListAlwaysReturnsOrReverts rest - termination_by ss => sizeOf ss - decreasing_by all_goals simp_wf; all_goals omega - - private def stmtAlwaysReturnsOrReverts : Stmt → Bool - | Stmt.return _ | Stmt.returnValues _ | Stmt.returnArray _ - | Stmt.returnBytes _ | Stmt.returnStorageWords _ - | Stmt.revertError _ _ | Stmt.revertReturndata => - true - | Stmt.ite _ thenBranch elseBranch => - stmtListAlwaysReturnsOrReverts thenBranch && stmtListAlwaysReturnsOrReverts elseBranch - | Stmt.unsafeBlock _ body => - stmtListAlwaysReturnsOrReverts body - | Stmt.matchAdt _ _ branches => - matchBranchesAllReturnOrRevert branches - | _ => - false - termination_by s => sizeOf s - decreasing_by all_goals simp_wf; all_goals omega - - private def matchBranchesAllReturnOrRevert : List (String × List String × List Stmt) → Bool - | [] => true - | (_, _, body) :: rest => - stmtListAlwaysReturnsOrReverts body && matchBranchesAllReturnOrRevert rest - termination_by bs => sizeOf bs - decreasing_by all_goals simp_wf; all_goals omega -end +private def stmtListAlwaysReturnsOrReverts (stmts : List Stmt) : Bool := + ControlFlowSummary.alwaysReturnsOrReverts (Stmt.controlFlowList stmts) def exprReadsStateOrEnv : Expr → Bool | Expr.literal _ => false @@ -428,6 +414,8 @@ def stmtWritesState : Stmt → Bool false | Stmt.returnBytes _ => false + | Stmt.unsafeYul fragment => + !fragment.scopeEffects.storageWrites.isEmpty || fragment.mechanics.contains .tstore | Stmt.returnStorageWords _ => false | Stmt.mstore offset value => @@ -492,6 +480,8 @@ def stmtWrittenFields : Stmt → List String stmtListWrittenFields body | Stmt.unsafeBlock _ body => stmtListWrittenFields body + | Stmt.unsafeYul fragment => + fragment.scopeEffects.storageWrites | Stmt.matchAdt _ _ branches => matchBranchesWrittenFields branches | _ => [] @@ -643,6 +633,10 @@ def stmtHasUntrackableWrites : Stmt → Bool exprHasUntrackableWrites count || stmtListHasUntrackableWrites body | Stmt.unsafeBlock _ body => stmtListHasUntrackableWrites body + | Stmt.unsafeYul fragment => + -- Raw Yul storage writes target computed slots that cannot be tied back to + -- declared storage fields, so any storage-writing fragment is untrackable. + !fragment.scopeEffects.storageWrites.isEmpty || fragment.mechanics.contains .storageWrite | Stmt.matchAdt _ scrutinee branches => exprHasUntrackableWrites scrutinee || matchBranchesHasUntrackableWrites branches | _ => false @@ -887,6 +881,10 @@ def stmtContainsExternalCall : Stmt → Bool matchBranchesContainExternalCall branches | Stmt.internalCall _ args | Stmt.internalCallAssign _ _ args => args.any exprContainsExternalCall + | Stmt.unsafeYul fragment => + fragment.mechanics.contains .call || + fragment.mechanics.contains .staticcall || + fragment.mechanics.contains .delegatecall | _ => false termination_by s => sizeOf s decreasing_by all_goals simp_wf; all_goals omega @@ -1030,6 +1028,8 @@ def stmtReadsStateOrEnv : Stmt → Bool | Stmt.matchAdt _ scrutinee branches => exprReadsStateOrEnv scrutinee || matchBranchesReadStateOrEnv branches + | Stmt.unsafeYul fragment => + !fragment.mechanics.isEmpty || !fragment.scopeEffects.storageWrites.isEmpty termination_by s => sizeOf s decreasing_by all_goals simp_wf; all_goals omega @@ -1231,6 +1231,8 @@ def stmtWritesStateWithFunctionEffects | Stmt.matchAdt _ scrutinee branches => exprWritesStateWithFunctionEffects effects scrutinee || matchBranchesWriteStateWithFunctionEffects effects branches + | Stmt.unsafeYul fragment => + !fragment.scopeEffects.storageWrites.isEmpty || fragment.mechanics.contains .tstore termination_by s => sizeOf s decreasing_by all_goals simp_wf; all_goals omega @@ -1414,6 +1416,8 @@ def stmtReadsStateOrEnvWithFunctionEffects | Stmt.matchAdt _ scrutinee branches => exprReadsStateOrEnvWithFunctionEffects effects scrutinee || matchBranchesReadStateOrEnvWithFunctionEffects effects branches + | Stmt.unsafeYul fragment => + !fragment.mechanics.isEmpty || !fragment.scopeEffects.storageWrites.isEmpty termination_by s => sizeOf s decreasing_by all_goals simp_wf; all_goals omega @@ -1494,6 +1498,8 @@ def stmtIsPersistentWrite : Stmt → Bool stmtListContainsPersistentWrite body | Stmt.matchAdt _ _ branches => matchBranchesPersistentWrite branches + | Stmt.unsafeYul fragment => + !fragment.scopeEffects.storageWrites.isEmpty || fragment.mechanics.contains .tstore | _ => false termination_by s => sizeOf s decreasing_by all_goals simp_wf; all_goals omega @@ -1529,6 +1535,8 @@ def stmtMayPersistentlyWrite : Stmt → Bool stmtListMayPersistentlyWrite body | Stmt.matchAdt _ _ branches => matchBranchesMayPersistentlyWrite branches + | Stmt.unsafeYul fragment => + !fragment.scopeEffects.storageWrites.isEmpty || fragment.mechanics.contains .tstore | s => stmtIsPersistentWrite s termination_by s => sizeOf s decreasing_by all_goals simp_wf; all_goals omega @@ -1626,6 +1634,23 @@ def stmtInternalCEIViolation : Stmt → Bool → Option String -- `match adtTag (externalCall ...) { ... setStorage ... }` is correctly flagged let scrutineeSeenCall := seenCall || exprMayContainExternalCall scrutinee matchBranchesCEIViolation branches scrutineeSeenCall + | Stmt.unsafeYul fragment, seenCall => + -- A raw Yul fragment whose mechanics include an external interaction must be + -- treated like a call for CEI purposes. Flag a violation when a storage write + -- happens after a prior external call, or within a fragment that both calls + -- out and writes storage. + let fragmentCalls := + fragment.mechanics.contains .call || + fragment.mechanics.contains .staticcall || + fragment.mechanics.contains .delegatecall + let fragmentWrites := + !fragment.scopeEffects.storageWrites.isEmpty || + fragment.mechanics.contains .storageWrite || + fragment.mechanics.contains .tstore + if (seenCall || fragmentCalls) && fragmentWrites then + some "raw Yul fragment writes state after an external call" + else + none | _, _ => none termination_by s => sizeOf s decreasing_by all_goals simp_wf; all_goals omega @@ -1793,6 +1818,11 @@ def validateNoUnsupportedAdtConstructInStmt : Stmt → Except String Unit | Stmt.storageArrayPop _ | Stmt.returnArray _ | Stmt.returnBytes _ | Stmt.returnStorageWords _ | Stmt.revertReturndata | Stmt.stop => pure () + | Stmt.unsafeYul fragment => + if fragment.obligations.isEmpty then + throw s!"Compilation error: unsafe Yul fragment '{fragment.label}' must declare at least one local proof obligation." + else + validateUnsafeYulDeclaredScopeEffects fragment termination_by s => sizeOf s decreasing_by all_goals simp_wf; all_goals omega @@ -1815,11 +1845,22 @@ decreasing_by all_goals simp_wf; all_goals omega end def validateFunctionSpec (spec : FunctionSpec) : Except String Unit := do + let rawYulObligations := + Stmt.foldList + (fun acc _ md => acc ++ md.localObligations) + [] + spec.body + if spec.body.any (fun stmt => + stmt.fold (fun acc s _ => + match s with + | Stmt.unsafeYul fragment => acc || fragment.obligations.isEmpty + | _ => acc) false) then + throw s!"Compilation error: function '{spec.name}' contains an unsafe Yul fragment without explicit local proof obligations." -- Check for unsafe boundary mechanics outside `unsafe "reason" do` blocks. -- Mechanics inside `unsafe` blocks are documented by the reason string and -- do not independently require `local_obligations` (#1728, Phase 6 Step 6b). let unguardedMechanics := collectUnguardedUnsafeBoundaryMechanicsFromStmts spec.body - if !unguardedMechanics.isEmpty && spec.localObligations.isEmpty then + if !unguardedMechanics.isEmpty && spec.localObligations.isEmpty && rawYulObligations.isEmpty then throw s!"Compilation error: function '{spec.name}' uses low-level/assembly mechanic(s) {String.intercalate ", " unguardedMechanics} outside an unsafe block without any local_obligations entry ({issue1424Ref}). Wrap the low-level code in `unsafe \"reason\" do` or add local_obligations [...] to make the trust boundary explicit." if spec.isPayable && (spec.isView || spec.isPure) then throw s!"Compilation error: function '{spec.name}' cannot be both payable and view/pure ({issue586Ref})" @@ -1901,8 +1942,19 @@ def validateConstructorSpec (ctor : Option ConstructorSpec) : Except String Unit match ctor with | none => pure () | some spec => + let rawYulObligations := + Stmt.foldList + (fun acc _ md => acc ++ md.localObligations) + [] + spec.body + if spec.body.any (fun stmt => + stmt.fold (fun acc s _ => + match s with + | Stmt.unsafeYul fragment => acc || fragment.obligations.isEmpty + | _ => acc) false) then + throw "Compilation error: constructor contains an unsafe Yul fragment without explicit local proof obligations." let unguardedMechanics := collectUnguardedUnsafeBoundaryMechanicsFromStmts spec.body - if !unguardedMechanics.isEmpty && spec.localObligations.isEmpty then + if !unguardedMechanics.isEmpty && spec.localObligations.isEmpty && rawYulObligations.isEmpty then throw s!"Compilation error: constructor uses low-level/assembly mechanic(s) {String.intercalate ", " unguardedMechanics} outside an unsafe block without any local_obligations entry ({issue1424Ref}). Wrap the low-level code in `unsafe \"reason\" do` or add local_obligations [...] to make the trust boundary explicit." if spec.body.any stmtContainsUnsafeLogicalCallLike then throw s!"Compilation error: constructor uses Expr.logicalAnd/Expr.logicalOr/Expr.ite or arithmetic helpers (mulDivUp/wDivUp/min/max) with call-like operand(s) that would be duplicated in Yul output ({issue748Ref}). Move call-like expressions into Stmt.letVar before combining." diff --git a/Compiler/CompilationModel/ValidationHelpers.lean b/Compiler/CompilationModel/ValidationHelpers.lean index ee80dcc02..dbde7e080 100644 --- a/Compiler/CompilationModel/ValidationHelpers.lean +++ b/Compiler/CompilationModel/ValidationHelpers.lean @@ -209,6 +209,8 @@ def collectStmtNames : Stmt → List String successVar :: resultVars ++ externalName :: collectExprListNames args | Stmt.ecm mod args => mod.resultVars ++ collectExprListNames args + | Stmt.unsafeYul fragment => + fragment.scopeEffects.bindNames ++ fragment.scopeEffects.assignNames termination_by stmt => sizeOf stmt decreasing_by all_goals simp_wf diff --git a/Compiler/CompilationModel/YulImporter.lean b/Compiler/CompilationModel/YulImporter.lean new file mode 100644 index 000000000..0c4ff3903 --- /dev/null +++ b/Compiler/CompilationModel/YulImporter.lean @@ -0,0 +1,168 @@ +import Compiler.CompilationModel.Types + +namespace Compiler.CompilationModel + +open Compiler.Yul + +/-- Source location supplied by an external Solidity/Yul AST importer. -/ +structure YulSourceSpan where + sourceName : String + startLine : Nat + startColumn : Nat + endLine : Nat + endColumn : Nat + deriving Repr, BEq, Inhabited + +namespace YulSourceSpan + +def toReportString (span : YulSourceSpan) : String := + s!"{span.sourceName}:{span.startLine}:{span.startColumn}-{span.endLine}:{span.endColumn}" + +end YulSourceSpan + +/-- Provenance for Yul entering the compilation model from outside Verity. -/ +inductive ImportedYulDialect where + | solidityInlineAssembly + | yul + | generatedYul + deriving Repr, BEq, Inhabited + +namespace ImportedYulDialect + +def toReportString : ImportedYulDialect → String + | .solidityInlineAssembly => "Solidity inline assembly" + | .yul => "Yul" + | .generatedYul => "generated Yul" + +end ImportedYulDialect + +/-- Typed boundary for importing already-parsed Solidity inline assembly/Yul AST. + Parsing remains outside this module; this boundary converts `Compiler.Yul.YulStmt` + into the localized unsafe-Yul statement surface with derived metadata. -/ +structure ImportedYulBlock where + label : String + dialect : ImportedYulDialect := .solidityInlineAssembly + sourceSpan : Option YulSourceSpan := none + stmts : List YulStmt + obligation : Option String := none + proofStatus : Compiler.ProofStatus := .assumed + extraMechanics : List LowLevelMechanic := [] + extraContracts : List UnsafeYulContract := [] + termination : StmtTermination := .mayTerminate + controlFlow : ControlFlowSummary := .unknown + deriving Repr + +namespace YulImporter + +private def uniqueMechanics (xs : List LowLevelMechanic) : List LowLevelMechanic := + xs.eraseDups + +private partial def mechanicsOfExpr : YulExpr → List LowLevelMechanic + | .call name args => + let here := + match name with + | "call" => [.call] + | "staticcall" => [.staticcall] + | "delegatecall" => [.delegatecall] + | "returndatasize" => [.returndataSize] + | "returndatacopy" => [.returndataCopy] + | "revert" => [.rawRevert] + | "mload" => [.mload] + | "mstore" => [.mstore] + | "calldataload" => [.calldataload] + | "calldatacopy" => [.calldatacopy] + | "extcodesize" => [.extcodesize] + | "tload" => [.tload] + | "tstore" => [.tstore, .storageWrite] + | "sstore" => [.storageWrite] + | "log0" | "log1" | "log2" | "log3" | "log4" => [.rawLog] + | "address" => [.contractAddress] + | "chainid" => [.chainid] + | "selfbalance" => [.selfBalance] + | "number" => [.blockNumber] + | _ => [] + here ++ args.flatMap mechanicsOfExpr + | _ => [] + +mutual +private partial def mechanicsOfStmt : YulStmt → List LowLevelMechanic + | .comment _ | .leave => [] + | .let_ _ value | .letMany _ value | .assign _ value | .expr value => + mechanicsOfExpr value + | .if_ cond body => + mechanicsOfExpr cond ++ mechanicsOfStmts body + | .for_ init cond post body => + mechanicsOfStmts init ++ mechanicsOfExpr cond ++ mechanicsOfStmts post ++ mechanicsOfStmts body + | .switch expr cases default => + mechanicsOfExpr expr ++ + cases.flatMap (fun (_, body) => mechanicsOfStmts body) ++ + default.toList.flatMap mechanicsOfStmts + | .block stmts => + mechanicsOfStmts stmts + | .funcDef _ _ _ body => + mechanicsOfStmts body + +private partial def mechanicsOfStmts : List YulStmt → List LowLevelMechanic + | [] => [] + | stmt :: rest => mechanicsOfStmt stmt ++ mechanicsOfStmts rest +end + +private def controlFlowOfExpr : YulExpr → ControlFlowSummary + | .call "revert" _ => .reverts + | .call "return" _ => .returns + | .call "stop" _ => .stops + | _ => .fallsThrough + +mutual +private partial def controlFlowOfStmt : YulStmt → ControlFlowSummary + | .comment _ | .let_ _ _ | .letMany _ _ | .assign _ _ | .funcDef _ _ _ _ => + .fallsThrough + | .leave => + .returns + | .expr expr => + controlFlowOfExpr expr + | .if_ cond body => + (controlFlowOfExpr cond).union { (controlFlowOfStmts body) with mayFallThrough := true } + | .for_ _ _ _ _ | .switch _ _ _ => + .unknown + | .block stmts => + controlFlowOfStmts stmts + +private partial def controlFlowOfStmts : List YulStmt → ControlFlowSummary + | [] => .fallsThrough + | stmt :: rest => + (controlFlowOfStmt stmt).seq (controlFlowOfStmts rest) +end + +private def defaultObligationText (block : ImportedYulBlock) : String := + let source := + match block.sourceSpan with + | none => block.dialect.toReportString + | some span => s!"{block.dialect.toReportString} at {span.toReportString}" + s!"Imported {source} block '{block.label}' must refine the declared Verity state transition." + +/-- Convert imported Solidity inline assembly/Yul AST into a localized unsafe-Yul statement. -/ +def importBlock (block : ImportedYulBlock) : Stmt := + let obligationText := block.obligation.getD (defaultObligationText block) + let obligation : LocalObligation := + { name := block.label + obligation := obligationText + proofStatus := block.proofStatus } + Stmt.unsafeYul { + label := block.label + stmts := block.stmts + obligations := [obligation] + contracts := block.extraContracts + mechanics := uniqueMechanics (mechanicsOfStmts block.stmts ++ block.extraMechanics) + scopeEffects := yulStmtListScopeEffects block.stmts + termination := block.termination + controlFlow := + if block.controlFlow == .unknown then + controlFlowOfStmts block.stmts + else + block.controlFlow + } + +end YulImporter + +end Compiler.CompilationModel diff --git a/Compiler/CompilationModelFeatureTest.lean b/Compiler/CompilationModelFeatureTest.lean index a5b4c3be2..04c0db652 100644 --- a/Compiler/CompilationModelFeatureTest.lean +++ b/Compiler/CompilationModelFeatureTest.lean @@ -75,6 +75,65 @@ example : dischargedEdgeExecutableStillRuns = true := by native_decide end MacroLocalObligationSmoke +namespace YulImporterSmoke + +open Compiler.Yul + +private def importedAssemblyStmt : Stmt := + YulImporter.importBlock { + label := "sol_inline_assembly" + sourceSpan := some { + sourceName := "Contract.sol" + startLine := 12 + startColumn := 8 + endLine := 18 + endColumn := 5 + } + stmts := [ + YulStmt.let_ "ptr" (YulExpr.call "mload" [YulExpr.lit 64]), + YulStmt.assign "ptr" (YulExpr.call "add" [YulExpr.ident "ptr", YulExpr.lit 32]), + YulStmt.expr (YulExpr.call "mstore" [YulExpr.ident "ptr", YulExpr.lit 1]), + YulStmt.expr (YulExpr.call "sstore" [YulExpr.lit 0, YulExpr.lit 1]), + YulStmt.expr (YulExpr.call "revert" [YulExpr.ident "ptr", YulExpr.lit 32]) + ] + } + +def importedAssemblyCarriesDerivedMetadata : Bool := + match importedAssemblyStmt with + | Stmt.unsafeYul fragment => + fragment.label == "sol_inline_assembly" && + (match fragment.obligations with + | [{ name := "sol_inline_assembly" + obligation := "Imported Solidity inline assembly at Contract.sol:12:8-18:5 block 'sol_inline_assembly' must refine the declared Verity state transition." + proofStatus := .assumed }] => true + | _ => false) && + fragment.mechanics.contains .mload && + fragment.mechanics.contains .mstore && + fragment.mechanics.contains .storageWrite && + fragment.mechanics.contains .rawRevert && + fragment.scopeEffects.bindNames == ["ptr"] && + fragment.scopeEffects.assignNames == ["ptr"] && + !fragment.scopeEffects.storageWrites.isEmpty && + fragment.controlFlow == .reverts + | _ => false + +example : importedAssemblyCarriesDerivedMetadata = true := by native_decide + +def importedAssemblyPassesUnsafeYulValidation : Bool := + let spec : FunctionSpec := { + name := "usesImportedAssembly" + params := [] + returnType := none + body := [importedAssemblyStmt, Stmt.stop] + } + match validateFunctionSpec spec with + | .ok _ => true + | .error _ => false + +example : importedAssemblyPassesUnsafeYulValidation = true := by native_decide + +end YulImporterSmoke + namespace MacroProxyUpgradeabilitySmoke open Contracts @@ -2726,6 +2785,156 @@ private def rawLogTooManyTopicsSpec : CompilationModel := { ] } +private def rawRevertSmokeSpec : CompilationModel := { + name := "RawRevertSmoke" + fields := [] + «constructor» := none + functions := [ + { name := "fail" + params := [ + { name := "offset", ty := ParamType.uint256 }, + { name := "size", ty := ParamType.uint256 } + ] + returnType := none + body := [ + Stmt.unsafeYul + (UnsafeYulFragment.rawRevert + (Compiler.Yul.YulExpr.ident "offset") + (Compiler.Yul.YulExpr.ident "size") + { name := "raw_revert_memory_slice_refinement" + obligation := "Caller-provided raw revert memory slice must refine the intended failure payload." + proofStatus := .assumed }) + ] + } + ] +} + +private def unsafeYulScopeObligation (name : String) : LocalObligation := + { name := name + obligation := "Raw Yul scope effects must conservatively describe the Yul payload." + proofStatus := .assumed } + +private def unsafeYulUnderDeclaredBindSpec : CompilationModel := { + name := "UnsafeYulUnderDeclaredBind" + fields := [] + «constructor» := none + functions := [ + { name := "bad" + params := [] + returnType := none + body := [ + Stmt.unsafeYul { + label := "under_declared_bind" + stmts := [Compiler.Yul.YulStmt.let_ "tmp" (Compiler.Yul.YulExpr.lit 1)] + obligations := [unsafeYulScopeObligation "under_declared_bind_obligation"] + } + ] + } + ] +} + +private def unsafeYulUnderDeclaredAssignSpec : CompilationModel := { + name := "UnsafeYulUnderDeclaredAssign" + fields := [] + «constructor» := none + functions := [ + { name := "bad" + params := [] + returnType := none + body := [ + Stmt.letVar "tmp" (Expr.literal 0), + Stmt.unsafeYul { + label := "under_declared_assign" + stmts := [Compiler.Yul.YulStmt.assign "tmp" (Compiler.Yul.YulExpr.lit 1)] + obligations := [unsafeYulScopeObligation "under_declared_assign_obligation"] + } + ] + } + ] +} + +private def unsafeYulUnderDeclaredStorageSpec : CompilationModel := { + name := "UnsafeYulUnderDeclaredStorage" + fields := [{ name := "value", ty := FieldType.uint256 }] + «constructor» := none + functions := [ + { name := "bad" + params := [] + returnType := none + body := [ + Stmt.unsafeYul { + label := "under_declared_storage" + stmts := [ + Compiler.Yul.YulStmt.expr + (Compiler.Yul.YulExpr.call "sstore" [Compiler.Yul.YulExpr.lit 0, Compiler.Yul.YulExpr.lit 1]) + ] + obligations := [unsafeYulScopeObligation "under_declared_storage_obligation"] + } + ] + } + ] +} + +private def unsafeYulTstoreMechanicViewRejectedSpec : CompilationModel := { + name := "UnsafeYulTstoreMechanicViewRejected" + fields := [] + «constructor» := none + functions := [ + { name := "bad" + params := [] + returnType := none + isView := true + body := [ + Stmt.unsafeYul { + label := "declared_tstore_mechanic" + stmts := [Compiler.Yul.YulStmt.comment "mechanic-only tstore boundary"] + obligations := [unsafeYulScopeObligation "declared_tstore_mechanic_obligation"] + mechanics := [.tstore] + } + ] + } + ] +} + +private def matchAdtAllBranchesTerminateSpec : CompilationModel := { + name := "MatchAdtAllBranchesTerminate" + fields := [{ name := "choice", ty := FieldType.adt "Choice" 1 }] + «constructor» := none + functions := [ + { name := "pick" + params := [] + returnType := some FieldType.uint256 + body := [ + Stmt.matchAdt "Choice" (Expr.adtTag "Choice" "choice") [ + ("None", [], [Stmt.return (Expr.literal 0)]), + ("Some", ["amount"], [Stmt.return (Expr.localVar "amount")]) + ] + ] + } + ] + adtTypes := [ + { name := "Choice" + variants := [ + { name := "None", tag := 0, fields := [] }, + { name := "Some", tag := 1, fields := [{ name := "amount", ty := ParamType.uint256 }] } + ] + } + ] +} + +private def returnValueStopRejectedSpec : CompilationModel := { + name := "ReturnValueStopRejected" + fields := [] + «constructor» := none + functions := [ + { name := "bad" + params := [] + returnType := some FieldType.uint256 + body := [Stmt.stop] + } + ] +} + private def reservedEcmResultVarSpec : CompilationModel := { name := "ReservedEcmResultVar" fields := [{ name := "value", ty := FieldType.uint256 }] @@ -5053,6 +5262,43 @@ set_option maxRecDepth 4096 in "compiler rawLog rejects more than four topics" rawLogTooManyTopicsSpec "rawLog supports at most 4 topics" + let rawRevertYul ← expectCompileToYul + "rawRevert smoke spec" + rawRevertSmokeSpec + expectTrue "rawRevert preserves the modeled memory slice in rendered Yul" + (contains rawRevertYul "revert(offset, size)") + let rawRevertTrustReport := emitTrustReportJson [rawRevertSmokeSpec] + let rawRevertLowLevelLines := emitLowLevelMechanicsUsageSiteLines [rawRevertSmokeSpec] + expectTrue "rawRevert trust report classifies raw memory reverts as denied low-level mechanics" + (contains rawRevertTrustReport "\"modeledLowLevelMechanics\"" && + contains rawRevertTrustReport "\"rawRevert\"" && + rawRevertLowLevelLines.any (fun line => contains line "RawRevertSmoke [function:fail]: rawRevert")) + expectTrue "rawRevert trust report includes structured unsafe Yul contract" + (contains rawRevertTrustReport "\"unsafeYulContracts\":[{\"name\":\"raw_revert_memory_slice_refinement\"" && + contains rawRevertTrustReport "\"memoryReads\":[\"revertPayload\"]") + expectCompileErrorContains + "unsafeYul validation rejects under-declared Yul let bindings" + unsafeYulUnderDeclaredBindSpec + "under-declares bound local(s): tmp" + expectCompileErrorContains + "unsafeYul validation rejects under-declared Yul assignments" + unsafeYulUnderDeclaredAssignSpec + "under-declares assigned local(s): tmp" + expectCompileErrorContains + "unsafeYul validation rejects under-declared Yul storage writes" + unsafeYulUnderDeclaredStorageSpec + "under-declares storage effects" + expectCompileErrorContains + "unsafeYul tstore mechanic is rejected from view functions" + unsafeYulTstoreMechanicViewRejectedSpec + "function 'bad' is marked view but writes state" + discard <| expectCompile + "matchAdt with terminating branches" + matchAdtAllBranchesTerminateSpec + expectCompileErrorContains + "function with return value rejects stop-only termination" + returnValueStopRejectedSpec + "not all control-flow paths end in return/revert" let envRuntimeYul ← expectCompileToYul "env runtime smoke compiles" envRuntimeSmokeSpec expectTrue "env runtime smoke lowers block.number" (contains envRuntimeYul "number()") let stringCompiled := diff --git a/Compiler/CompileDriverCommon.lean b/Compiler/CompileDriverCommon.lean index 97b992bf2..619da3dde 100644 --- a/Compiler/CompileDriverCommon.lean +++ b/Compiler/CompileDriverCommon.lean @@ -360,6 +360,8 @@ private partial def collectIntrinsicUsesStmt : Stmt → List IntrinsicUse | .storageArrayPop _ | .returnArray _ | .returnBytes _ | .returnStorageWords _ | .revertReturndata | .stop => [] + | .unsafeYul _ => + [] private def collectIntrinsicUsesSpec (spec : CompilationModel) : List IntrinsicUse := let ctorUses := diff --git a/Compiler/CompileDriverTest.lean b/Compiler/CompileDriverTest.lean index 5a849116c..841716ca8 100644 --- a/Compiler/CompileDriverTest.lean +++ b/Compiler/CompileDriverTest.lean @@ -612,6 +612,35 @@ private def localObligationTrustSurfaceSpec : CompilationModel := { ] } +private def rawYulTrustSurfaceSpec : CompilationModel := { + name := "RawYulTrustSurface" + fields := [] + «constructor» := none + functions := [ + { name := "unsafeMemory" + params := [] + returnType := none + body := [ + Stmt.unsafeYul { + label := "manual_memory_refinement" + stmts := [ + Compiler.Yul.YulStmt.expr + (Compiler.Yul.YulExpr.call "mstore" [Compiler.Yul.YulExpr.lit 0, Compiler.Yul.YulExpr.lit 1]) + ] + obligations := [ + { name := "manual_memory_refinement" + obligation := "Handwritten Yul memory write must refine the high-level memory contract." + proofStatus := .assumed } + ] + mechanics := [.mstore] + termination := .fallsThrough + }, + Stmt.stop + ] + } + ] +} + private def unsafeBlockTrustSurfaceSpec : CompilationModel := { name := "UnsafeBlockTrustSurface" fields := [] @@ -1497,6 +1526,24 @@ unsafe def runTests : IO Unit := do throw (IO.userError "✗ local-obligation diagnostics localize usage sites") IO.println "✓ trust report surfaces local unsafe/refinement obligations" + let rawYulTrustReport := emitTrustReportJson [rawYulTrustSurfaceSpec] + if !contains rawYulTrustReport "\"contract\":\"RawYulTrustSurface\"" then + throw (IO.userError "✗ raw Yul trust report emits contract name") + if !contains rawYulTrustReport "\"modeledLowLevelMechanics\":[\"mstore\"]" then + throw (IO.userError "✗ raw Yul trust report emits fragment low-level mechanics") + if !contains rawYulTrustReport "\"localObligations\":[{\"name\":\"manual_memory_refinement\",\"status\":\"assumed\",\"obligation\":\"Handwritten Yul memory write must refine the high-level memory contract.\"}]" then + throw (IO.userError "✗ raw Yul trust report emits fragment local obligations") + if !contains rawYulTrustReport "\"usageSites\":[{\"kind\":\"function\",\"name\":\"unsafeMemory\"" || + !contains rawYulTrustReport "\"unsafeBlocks\":[\"manual_memory_refinement\"]" then + throw (IO.userError "✗ raw Yul trust report localizes fragment usage site") + let rawYulOutDir := s!"/tmp/verity-compile-driver-test-{nonce}-raw-yul-out" + IO.FS.createDirAll rawYulOutDir + compileSpecsWithOptions [rawYulTrustSurfaceSpec] rawYulOutDir false [] {} none none none none + let rawYulArtifact ← IO.FS.readFile s!"{rawYulOutDir}/RawYulTrustSurface.yul" + if !contains rawYulArtifact "mstore(0, 1)" then + throw (IO.userError "✗ raw Yul fragment lowers through the central EVMYul bridge") + IO.println "✓ raw Yul fragments lower and surface trust obligations" + let assumptionReport := emitAssumptionReportJson [trustSurfaceSpec, localObligationTrustSurfaceSpec] if !contains assumptionReport "\"contract\":\"TrustSurfaceSmoke\"" then throw (IO.userError "✗ assumption report emits contract name") diff --git a/Compiler/Proofs/IRGeneration/FunctionBody.lean b/Compiler/Proofs/IRGeneration/FunctionBody.lean index 22c7f86b4..9eb8c6f7a 100644 --- a/Compiler/Proofs/IRGeneration/FunctionBody.lean +++ b/Compiler/Proofs/IRGeneration/FunctionBody.lean @@ -8161,7 +8161,8 @@ private theorem compileStmt_ok_any_scope_aux | requireError | revertError | «return» | returnValues | returnArray | returnBytes | returnStorageWords | mstore | tstore | calldatacopy | returndataCopy | revertReturndata | stop | emit | internalCall - | internalCallAssign | externalCallBind | tryExternalCallBind | ecm | rawLog => + | internalCallAssign | externalCallBind | tryExternalCallBind | ecm | rawLog + | unsafeYul => simp only [CompilationModel.compileStmt] at hok ⊢; exact hok · -- compileStmtList part intro stmts scope1 scope2 hlt hok @@ -8279,7 +8280,7 @@ private theorem compileStmt_ok_any_scope_with_surface_aux | returnBytes | returnStorageWords | mstore | tstore | calldatacopy | returndataCopy | revertReturndata | stop | emit | internalCall | internalCallAssign | externalCallBind | tryExternalCallBind - | ecm | rawLog => + | ecm | rawLog | unsafeYul => simp only [CompilationModel.compileStmt] at hok ⊢; exact hok · intro stmts scope1 scope2 hlt hok cases stmts with diff --git a/Compiler/Proofs/IRGeneration/GenericInduction.lean b/Compiler/Proofs/IRGeneration/GenericInduction.lean index 2712beee4..39db20fb6 100644 --- a/Compiler/Proofs/IRGeneration/GenericInduction.lean +++ b/Compiler/Proofs/IRGeneration/GenericInduction.lean @@ -1834,7 +1834,7 @@ theorem legacyCompatibleExternalStmtList_of_compileStmt_ok_on_supportedContractS | ite _ _ _ | forEach _ _ _ | emit _ _ | internalCall _ _ | internalCallAssign _ _ _ | rawLog _ _ _ | externalCallBind _ _ _ | tryExternalCallBind _ _ _ _ | ecm _ _ - | unsafeBlock _ _ | matchAdt _ _ _ => + | unsafeBlock _ _ | unsafeYul _ | matchAdt _ _ _ => exact legacyCompatibleExternalStmtList_of_compileStmt_ok_on_supportedContractSurface hnoPacked (by simpa [stmtTouchesUnsupportedContractSurfaceExceptMappingWrites] using hsurface) @@ -3781,7 +3781,7 @@ theorem stmtListScopeCore_prefix_of_compileStmtList_ok_of_stmtListTouchesUnsuppo | returndataCopy _ _ _ | revertReturndata | emit _ _ | internalCall _ _ | internalCallAssign _ _ _ | rawLog _ _ _ | externalCallBind _ _ _ | tryExternalCallBind _ _ _ _ | ecm _ _ - | unsafeBlock _ _ | matchAdt _ _ _ => + | unsafeBlock _ _ | unsafeYul _ | matchAdt _ _ _ => simp [stmtTouchesUnsupportedContractSurface] at hstmtSurface private theorem stmtTouchesUnsupportedContractSurface_of_stmtListTouchesUnsupportedContractSurface_append_cons diff --git a/Compiler/Proofs/IRGeneration/SourceSemantics.lean b/Compiler/Proofs/IRGeneration/SourceSemantics.lean index 8b50cf938..df4a25f9a 100644 --- a/Compiler/Proofs/IRGeneration/SourceSemantics.lean +++ b/Compiler/Proofs/IRGeneration/SourceSemantics.lean @@ -4561,6 +4561,7 @@ private theorem execStmtWithHelpers_eq_execStmt_of_helperSurfaceClosed_aux evalExprListWithHelpers_eq_evalExprList_of_helperSurfaceClosed spec fields fuel state args hall, evalExprList_eq_mapM] | .rawLog _ _ _ => simp [execStmtWithHelpers, execStmtWithEvents] + | .unsafeYul _ => cases hsurface | .externalCallBind _ _ _ => simp [execStmtWithHelpers, execStmtWithEvents] | .tryExternalCallBind _ _ _ _ => simp [execStmtWithHelpers, execStmtWithEvents] | .ecm _ _ => simp [execStmtWithHelpers, execStmtWithEvents] diff --git a/Compiler/Proofs/IRGeneration/SupportedSpec.lean b/Compiler/Proofs/IRGeneration/SupportedSpec.lean index 8c88c6bd9..64f3bc533 100644 --- a/Compiler/Proofs/IRGeneration/SupportedSpec.lean +++ b/Compiler/Proofs/IRGeneration/SupportedSpec.lean @@ -644,7 +644,7 @@ def stmtTouchesUnsupportedConstructorRawCalldataSurface : Stmt → Bool | .setMapping _ key value | .setMappingWord _ key _ value | .setMappingPackedWord _ key _ _ value | .setMappingUint _ key value | .setStructMember _ key _ value | .setStorageArrayElement _ key value - | .mstore key value | .tstore key value => + | .mstore key value | .tstore key value => exprTouchesUnsupportedConstructorRawCalldataSurface key || exprTouchesUnsupportedConstructorRawCalldataSurface value | .setMappingChain _ keys value => @@ -669,7 +669,7 @@ def stmtTouchesUnsupportedConstructorRawCalldataSurface : Stmt → Bool | .returnValues _ | .returnArray _ | .returnBytes _ | .returnStorageWords _ | .calldatacopy _ _ _ | .returndataCopy _ _ _ | .revertReturndata | .rawLog _ _ _ | .ecm _ _ => false - | .unsafeBlock _ _ | .matchAdt _ _ _ => true + | .unsafeBlock _ _ | .unsafeYul _ | .matchAdt _ _ _ => true def stmtListTouchesUnsupportedConstructorRawCalldataSurface : List Stmt → Bool | [] => false @@ -1177,7 +1177,7 @@ def stmtTouchesUnsupportedEffectSurface : Stmt → Bool | .storageArrayPush _ _ | .storageArrayPop _ | .setStorageArrayElement _ _ _ | .calldatacopy _ _ _ | .returndataCopy _ _ _ | .revertReturndata | .internalCall _ _ | .internalCallAssign _ _ _ => false - | .unsafeBlock _ _ | .matchAdt _ _ _ => true + | .unsafeBlock _ _ | .unsafeYul _ | .matchAdt _ _ _ => true | .ite _ thenBranch elseBranch => stmtListTouchesUnsupportedEffectSurface thenBranch || stmtListTouchesUnsupportedEffectSurface elseBranch @@ -1212,7 +1212,7 @@ def stmtTouchesUnsupportedCoreSurface : Stmt → Bool | .setStorageArrayElement _ index value => exprTouchesUnsupportedCoreSurface index || exprTouchesUnsupportedCoreSurface value - | .mstore offset value | .tstore offset value => + | .mstore offset value | .tstore offset value => exprTouchesUnsupportedCoreSurface offset || exprTouchesUnsupportedCoreSurface value | .require cond _ | .return cond => @@ -1229,7 +1229,7 @@ def stmtTouchesUnsupportedCoreSurface : Stmt → Bool | .returndataCopy _ _ _ | .revertReturndata | .emit _ _ | .internalCall _ _ | .internalCallAssign _ _ _ | .rawLog _ _ _ | .externalCallBind _ _ _ | .tryExternalCallBind _ _ _ _ | .ecm _ _ => false - | .unsafeBlock _ _ | .matchAdt _ _ _ => true + | .unsafeBlock _ _ | .unsafeYul _ | .matchAdt _ _ _ => true /-- State/layout-rich statement surfaces still outside the current whole-contract theorem. -/ @@ -1245,7 +1245,7 @@ def stmtTouchesUnsupportedStateSurface : Stmt → Bool | .setMappingChain _ _ _ | .setStructMember _ _ _ _ | .setStructMember2 _ _ _ _ _ | .storageArrayPush _ _ | .storageArrayPop _ | .setStorageArrayElement _ _ _ => true - | .mstore offset value | .tstore offset value => + | .mstore offset value | .tstore offset value => exprTouchesUnsupportedStateSurface offset || exprTouchesUnsupportedStateSurface value | .stop @@ -1254,7 +1254,7 @@ def stmtTouchesUnsupportedStateSurface : Stmt → Bool | .returndataCopy _ _ _ | .revertReturndata | .emit _ _ | .internalCall _ _ | .internalCallAssign _ _ _ | .rawLog _ _ _ | .externalCallBind _ _ _ | .tryExternalCallBind _ _ _ _ | .ecm _ _ => false - | .unsafeBlock _ _ | .matchAdt _ _ _ => true + | .unsafeBlock _ _ | .unsafeYul _ | .matchAdt _ _ _ => true | .ite cond thenBranch elseBranch => exprTouchesUnsupportedStateSurface cond || stmtListTouchesUnsupportedStateSurface thenBranch || @@ -1299,13 +1299,14 @@ def stmtTouchesUnsupportedCallSurface : Stmt → Bool exprTouchesUnsupportedCallSurface cond | .internalCall _ _ | .internalCallAssign _ _ _ => true | .calldatacopy _ _ _ - | .returndataCopy _ _ _ | .revertReturndata | .externalCallBind _ _ _ | .tryExternalCallBind _ _ _ _ + | .returndataCopy _ _ _ | .revertReturndata + | .externalCallBind _ _ _ | .tryExternalCallBind _ _ _ _ | .ecm _ _ => true | .stop | .storageArrayPop _ | .requireError _ _ _ | .revertError _ _ | .returnValues _ | .returnArray _ | .returnBytes _ | .returnStorageWords _ | .rawLog _ _ _ => false | .emit _ args => args.any exprTouchesUnsupportedCallSurface - | .unsafeBlock _ _ | .matchAdt _ _ _ => true + | .unsafeBlock _ _ | .unsafeYul _ | .matchAdt _ _ _ => true | .ite cond thenBranch elseBranch => exprTouchesUnsupportedCallSurface cond || stmtListTouchesUnsupportedCallSurface thenBranch || @@ -1332,7 +1333,7 @@ def stmtTouchesUnsupportedHelperSurface : Stmt → Bool exprTouchesUnsupportedHelperSurface key2 || exprTouchesUnsupportedHelperSurface value | .setStorageArrayElement _ index value - | .mstore index value | .tstore index value => + | .mstore index value | .tstore index value => exprTouchesUnsupportedHelperSurface index || exprTouchesUnsupportedHelperSurface value | .require cond _ | .return cond => @@ -1344,7 +1345,7 @@ def stmtTouchesUnsupportedHelperSurface : Stmt → Bool | .requireError _ _ _ | .revertError _ _ | .returnValues _ | .returnArray _ | .returnBytes _ | .returnStorageWords _ | .rawLog _ _ _ => false | .emit _ args => exprListTouchesUnsupportedHelperSurface args - | .unsafeBlock _ _ | .matchAdt _ _ _ => true + | .unsafeBlock _ _ | .unsafeYul _ | .matchAdt _ _ _ => true | .ite cond thenBranch elseBranch => exprTouchesUnsupportedHelperSurface cond || stmtListTouchesUnsupportedHelperSurface thenBranch || @@ -1374,7 +1375,7 @@ def stmtTouchesInternalHelperSurface : Stmt → Bool exprTouchesInternalHelperSurface key2 || exprTouchesInternalHelperSurface value | .setStorageArrayElement _ index value - | .mstore index value | .tstore index value => + | .mstore index value | .tstore index value => exprTouchesInternalHelperSurface index || exprTouchesInternalHelperSurface value | .require cond _ | .return cond => @@ -1386,7 +1387,7 @@ def stmtTouchesInternalHelperSurface : Stmt → Bool | .revertError _ _ | .returnValues _ | .returnArray _ | .returnBytes _ | .returnStorageWords _ | .emit _ _ | .rawLog _ _ _ => false - | .unsafeBlock _ _ | .matchAdt _ _ _ => true + | .unsafeBlock _ _ | .unsafeYul _ | .matchAdt _ _ _ => true | .ite cond thenBranch elseBranch => exprTouchesInternalHelperSurface cond || stmtListTouchesInternalHelperSurface thenBranch || @@ -1439,7 +1440,7 @@ def stmtTouchesExprInternalHelperSurface : Stmt → Bool exprTouchesInternalHelperSurface key2 || exprTouchesInternalHelperSurface value | .setStorageArrayElement _ index value - | .mstore index value | .tstore index value => + | .mstore index value | .tstore index value => exprTouchesInternalHelperSurface index || exprTouchesInternalHelperSurface value | .require cond _ | .return cond => @@ -1455,7 +1456,7 @@ def stmtTouchesExprInternalHelperSurface : Stmt → Bool | .revertError _ _ | .returnValues _ | .returnArray _ | .returnBytes _ | .returnStorageWords _ | .emit _ _ | .rawLog _ _ _ => false - | .unsafeBlock _ _ | .matchAdt _ _ _ => true + | .unsafeBlock _ _ | .unsafeYul _ | .matchAdt _ _ _ => true /-- Recursive structural internal-helper transport at the current statement head. This isolates `ite` / `forEach` obligations whose proof burden is mainly @@ -1469,6 +1470,7 @@ def stmtTouchesStructuralInternalHelperSurface : Stmt → Bool | .letVar _ _ | .assignVar _ _ | .setStorage _ _ | .require _ _ | .return _ | .internalCall _ _ | .internalCallAssign _ _ _ | .stop | .setStorageAddr _ _ | .setStorageWord _ _ _ | .mstore _ _ | .tstore _ _ + | .calldatacopy _ _ _ | .returndataCopy _ _ _ | .revertReturndata | .externalCallBind _ _ _ | .tryExternalCallBind _ _ _ _ | .ecm _ _ | .setMapping _ _ _ | .setMappingWord _ _ _ _ @@ -1481,7 +1483,7 @@ def stmtTouchesStructuralInternalHelperSurface : Stmt → Bool | .revertError _ _ | .returnValues _ | .returnArray _ | .returnBytes _ | .returnStorageWords _ | .emit _ _ | .rawLog _ _ _ => false - | .unsafeBlock _ _ | .matchAdt _ _ _ => true + | .unsafeBlock _ _ | .unsafeYul _ | .matchAdt _ _ _ => true def stmtTouchesUnsupportedForeignSurface : Stmt → Bool | .letVar _ value | .assignVar _ value | .setStorage _ value @@ -1501,7 +1503,7 @@ def stmtTouchesUnsupportedForeignSurface : Stmt → Bool exprTouchesUnsupportedForeignSurface key2 || exprTouchesUnsupportedForeignSurface value | .setStorageArrayElement _ index value - | .mstore index value | .tstore index value => + | .mstore index value | .tstore index value => exprTouchesUnsupportedForeignSurface index || exprTouchesUnsupportedForeignSurface value | .require cond _ | .return cond => @@ -1514,7 +1516,7 @@ def stmtTouchesUnsupportedForeignSurface : Stmt → Bool | .requireError _ _ _ | .revertError _ _ | .returnValues _ | .returnArray _ | .returnBytes _ | .returnStorageWords _ | .rawLog _ _ _ => false | .emit _ args => args.any exprTouchesUnsupportedForeignSurface - | .unsafeBlock _ _ | .matchAdt _ _ _ => true + | .unsafeBlock _ _ | .unsafeYul _ | .matchAdt _ _ _ => true | .ite cond thenBranch elseBranch => exprTouchesUnsupportedForeignSurface cond || stmtListTouchesUnsupportedForeignSurface thenBranch || @@ -1554,7 +1556,7 @@ def stmtTouchesUnsupportedLowLevelSurface : Stmt → Bool | .requireError _ _ _ | .revertError _ _ | .returnValues _ | .returnArray _ | .returnBytes _ | .returnStorageWords _ | .rawLog _ _ _ => false | .emit _ args => args.any exprTouchesUnsupportedLowLevelSurface - | .unsafeBlock _ _ | .matchAdt _ _ _ => true + | .unsafeBlock _ _ | .unsafeYul _ | .matchAdt _ _ _ => true | .ite cond thenBranch elseBranch => exprTouchesUnsupportedLowLevelSurface cond || stmtListTouchesUnsupportedLowLevelSurface thenBranch || @@ -1591,7 +1593,7 @@ def stmtTouchesUnsupportedContractSurface (stmt : Stmt) : Bool := | .returndataCopy _ _ _ | .revertReturndata | .emit _ _ | .internalCall _ _ | .internalCallAssign _ _ _ | .rawLog _ _ _ | .externalCallBind _ _ _ | .ecm _ _ - | .tryExternalCallBind _ _ _ _ | .unsafeBlock _ _ | .matchAdt _ _ _ => true + | .tryExternalCallBind _ _ _ _ | .unsafeBlock _ _ | .unsafeYul _ | .matchAdt _ _ _ => true | .forEach _ (.literal 0) body => stmtListTouchesUnsupportedContractSurface body | .forEach _ (.literal _) [] => false @@ -1887,6 +1889,7 @@ mutual | .revertReturndata | .stop => [] | .unsafeBlock _ body => stmtListExprHelperCallNames body + | .unsafeYul _ => [] | .matchAdt _ _ branches => matchAdtBranchesExprHelperCallNames branches termination_by s => sizeOf s @@ -1953,6 +1956,7 @@ mutual | .revertReturndata | .stop => [] | .unsafeBlock _ body => stmtListInternalHelperCallNames body + | .unsafeYul _ => [] | .matchAdt _ _ branches => matchAdtBranchesInternalHelperCallNames branches termination_by s => sizeOf s @@ -3457,7 +3461,7 @@ mutual simp [stmtTouchesInternalHelperSurface, exprTouchesInternalHelperSurface_eq_false_of_helperSurfaceClosed hsurface.1, stmtListTouchesInternalHelperSurface_eq_false_of_helperSurfaceClosed hsurface.2] - | unsafeBlock _ _ | matchAdt _ _ _ => + | unsafeBlock _ _ | unsafeYul _ | matchAdt _ _ _ => simp [stmtTouchesUnsupportedHelperSurface] at hsurface | stop | calldatacopy _ _ _ | returndataCopy _ _ _ | revertReturndata | externalCallBind _ _ _ | tryExternalCallBind _ _ _ _ | ecm _ _ | storageArrayPop _ | requireError _ _ _ @@ -4436,7 +4440,7 @@ theorem stmtTouchesUnsupportedHelperSurface_eq_false_of_contractSurfaceClosed exact ⟨⟨exprTouchesUnsupportedHelperSurface_eq_false_of_contractSurfaceClosed hsurface.1.1, stmtListTouchesUnsupportedHelperSurface_eq_false_of_contractSurfaceClosed hsurface.1.2⟩, stmtListTouchesUnsupportedHelperSurface_eq_false_of_contractSurfaceClosed hsurface.2⟩ - | tryExternalCallBind _ _ _ _ | unsafeBlock _ _ | matchAdt _ _ _ + | tryExternalCallBind _ _ _ _ | unsafeBlock _ _ | unsafeYul _ | matchAdt _ _ _ | setMapping _ _ _ | setMappingWord _ _ _ _ | setMappingPackedWord _ _ _ _ _ | setMapping2 _ _ _ _ | setMapping2Word _ _ _ _ _ | setMappingUint _ _ _ diff --git a/README.md b/README.md index d49511036..5ac81c858 100644 --- a/README.md +++ b/README.md @@ -95,6 +95,7 @@ Verity is complementary to these tools. It is for cases where you need mathemati | [Production Solidity Patterns](https://veritylang.com/guides/production-solidity-patterns) | Agent guidance for production ports, reusable Verity features, and oracle/spec boundaries | | [docs/VERIFICATION_STATUS.md](docs/VERIFICATION_STATUS.md) | Theorem counts, proof status, test coverage | | [docs/INTRINSICS.md](docs/INTRINSICS.md) | Consumer-owned opcode bindings and their trust model | +| [docs/LOW_LEVEL_YUL.md](docs/LOW_LEVEL_YUL.md) | Policy for typed low-level primitives vs. raw Yul escape hatches | | [TRUST_ASSUMPTIONS.md](TRUST_ASSUMPTIONS.md) | What is verified vs. what is trusted | | [AXIOMS.md](AXIOMS.md) | Documented axioms (currently 0) | | [AUDIT.md](AUDIT.md) | Trust-boundary audit evidence and CI guards | diff --git a/TRUST_ASSUMPTIONS.md b/TRUST_ASSUMPTIONS.md index 3d3fe8fd9..24ec9590c 100644 --- a/TRUST_ASSUMPTIONS.md +++ b/TRUST_ASSUMPTIONS.md @@ -84,6 +84,20 @@ Current theorem totals, property-test coverage, and proof status live in [docs/V - **Status**: Surfaced explicitly in `--trust-report`, `--verbose`, and `proofStatus.*.localObligations`. - **Mitigation**: `verity-compiler --deny-local-obligations` fails closed on any obligation that remains `assumed` or `unchecked`. +### 10a. Raw Yul Escape Hatch +- **Role**: Model ad-hoc handwritten Yul through `Stmt.unsafeYul` and + `UnsafeYulFragment` when the surface is only a single instruction or otherwise + too local to justify a first-class `Stmt` constructor. +- **Status**: Raw Yul fragments lower through the single + `unsafeYulToEVMYul` bridge and carry their own mechanics, termination + metadata, and local obligations. Raw memory reverts use + `UnsafeYulFragment.rawRevert` through `Stmt.unsafeYul`. +- **Mitigation**: Keep common typed primitives such as `mstore` and + `calldatacopy` first-class only when Verity has stable semantics and they are + useful for proofs. Treat other raw Yul as an explicit trust-report surface, + and use `--deny-local-obligations` / low-level deny gates for strict builds. +- **Reference**: See [docs/LOW_LEVEL_YUL.md](docs/LOW_LEVEL_YUL.md). + ### 11. Consumer-Declared Intrinsics - **Role**: Let downstream packages bind a source-level Verity function to a target EVM opcode or Yul builtin without adding opcode-specific code to diff --git a/docs-site/content/compiler.mdx b/docs-site/content/compiler.mdx index a152d542d..4621d46b0 100644 --- a/docs-site/content/compiler.mdx +++ b/docs-site/content/compiler.mdx @@ -166,6 +166,8 @@ constructor := some { > **Linear-memory boundary**: Memory-oriented intrinsics (`mload`, `mstore`, `calldatacopy`, `returndataCopy`, `returndataOptionalBoolAt`) compile, but the current proof interpreters still model them only partially. When they appear, surface that boundary with `--trust-report` / `--deny-linear-memory-mechanics`; the remaining gap is tracked under issue `#1411`. > > **Axiomatized-primitive boundary**: The `keccak256` intrinsic also compiles, but it remains axiomatized in the current proof stack rather than fully modeled end to end. When it appears, archive `--trust-report` and add `--deny-axiomatized-primitives` if the selected contracts must stay inside the proved subset (see issue `#1411`). +> +> **Raw Yul boundary**: One-off single-instruction escapes should be modeled as `Stmt.unsafeYul` fragments, not new `Stmt` constructors. For example, raw memory reverts should use `UnsafeYulFragment.rawRevert`. Keep typed primitives such as `mstore` and `calldatacopy` first-class when Verity has stable semantics and proof/audit value for them. **Statements** cover local variables, storage and mapping writes, `require`, `return`, memory writes, returndata copy and revert bubbling, `stop`, `ite` branching, event emission, internal calls, and a precisely scoped `forEach` fragment. The proved `forEach` cases are zero-bound loops with supported bodies and arbitrary literal-bound empty-body loops; positive literal loops with non-empty bodies remain future proof work. diff --git a/docs-site/content/edsl-api-reference.mdx b/docs-site/content/edsl-api-reference.mdx index 36e1ecf58..05059ef64 100644 --- a/docs-site/content/edsl-api-reference.mdx +++ b/docs-site/content/edsl-api-reference.mdx @@ -397,4 +397,20 @@ When the low-level form is `delegatecall`, the trust report now also isolates it First-class linear-memory forms (`Expr.mload`, `Stmt.mstore`, `Stmt.calldatacopy`, `Stmt.returndataCopy`, `Expr.returndataOptionalBoolAt`) also compile today, but they are still only partially modeled by the current proof interpreters. When they appear, treat them as an explicit memory/ABI trust boundary, archive `--trust-report`, and use `--deny-linear-memory-mechanics` for proof-strict runs (see issue `#1411`). +One-off raw Yul instructions should use `Stmt.unsafeYul` with an +`UnsafeYulFragment` helper instead of becoming new first-class statements. Raw +memory revert is the canonical small helper: + +```lean +Stmt.unsafeYul + (UnsafeYulFragment.rawRevert + (Compiler.Yul.YulExpr.ident "offset") + (Compiler.Yul.YulExpr.ident "size") + { name := "raw_revert_memory_slice_refinement" + obligation := "Caller-provided raw revert memory slice must refine the intended failure payload." + proofStatus := .assumed }) +``` + +Raw memory reverts should use the explicit raw-Yul fragment boundary. + Prefer ECM wrappers when they fit. For the remaining unavoidable cases, attach a `localObligations` entry at the usage site and discharge it before shipping. diff --git a/docs-site/content/trust-model.mdx b/docs-site/content/trust-model.mdx index ad3d11d68..cdaaee5a9 100644 --- a/docs-site/content/trust-model.mdx +++ b/docs-site/content/trust-model.mdx @@ -60,6 +60,11 @@ What remains outside the proof envelope is **assumptions**, not axioms: - **Externally Callable Modules (ECMs)** in `Compiler/Modules/*.lean` carry named assumptions like `erc20_balanceOf_interface`, `evm_ecrecover_precompile`, `keccak256_memory_slice_matches_evm`. These are trust-report metadata, not Lean axioms, they document that the call mechanics depend on the EVM behaving as specified. - **`local_obligations`** declared on a constructor or function carry a named refinement obligation at that exact usage site. +- **Raw Yul fragments** use `Stmt.unsafeYul` with `UnsafeYulFragment` + metadata. One-off instruction escapes, such as raw memory reverts, belong here + rather than as new first-class statement constructors. Common typed primitives + like `Stmt.mstore` and `Stmt.calldatacopy` stay first-class when Verity has + stable semantics and proof/audit value for them. - **Consumer-declared intrinsics** bind small opcodes or Yul builtins that Verity does not yet model directly. They do not add Verity project axioms; the consumer owns the declared obligation and `min_fork` target. See [Intrinsics](/intrinsics). - **Not-modeled features** (parts of low-level call mechanics, linear-memory primitives, raw `rawLog`, dynamic `keccak256` over memory) compile but the proof interpreter does not yet model their full semantics. diff --git a/docs/INTERPRETER_FEATURE_MATRIX.md b/docs/INTERPRETER_FEATURE_MATRIX.md index 33641cf8c..c5eb21ea9 100644 --- a/docs/INTERPRETER_FEATURE_MATRIX.md +++ b/docs/INTERPRETER_FEATURE_MATRIX.md @@ -140,6 +140,13 @@ segment followed by a 32-byte value, use 32-byte widths. Dynamic `bytes` / `string` packed encoding remains outside the current core surface. +One-off raw instruction surfaces should not be added to this statement table by +default. Use `Stmt.unsafeYul` with a small `UnsafeYulFragment` helper, such as +`UnsafeYulFragment.rawRevert`, when the feature is just an explicit Yul escape +hatch. Keep common typed primitives such as `Stmt.mstore` and +`Stmt.calldatacopy` first-class when they have stable Verity semantics and are +useful for proofs. + --- ## Builtin Bridge (Verity vs EVMYulLean) diff --git a/docs/LOW_LEVEL_YUL.md b/docs/LOW_LEVEL_YUL.md new file mode 100644 index 000000000..4dd09ac9d --- /dev/null +++ b/docs/LOW_LEVEL_YUL.md @@ -0,0 +1,32 @@ +# Low-Level Yul Surface + +Verity keeps two low-level escape routes separate: + +- First-class typed primitives, such as `Stmt.mstore` and + `Stmt.calldatacopy`, are kept when they have stable Verity semantics, trust + reporting, and proof value. +- One-off statements that only expose a single Yul instruction should be helper + constructors returning `UnsafeYulFragment`, used through `Stmt.unsafeYul`. + +Raw Yul is the explicit escape hatch. An `UnsafeYulFragment` carries the EVMYul +AST payload, low-level mechanics, local obligations, scope effects, and +termination metadata at the same boundary. This keeps ad-hoc assembly visible +in trust reports without making every Yul instruction look like a modeled +Verity statement. + +For example, raw memory reverts now use the fragment helper: + +```lean +Stmt.unsafeYul + (UnsafeYulFragment.rawRevert + (Compiler.Yul.YulExpr.ident "offset") + (Compiler.Yul.YulExpr.ident "size") + { name := "raw_revert_memory_slice_refinement" + obligation := "Caller-provided raw revert memory slice must refine the intended failure payload." + proofStatus := .assumed }) +``` + +Raw memory reverts should use `UnsafeYulFragment.rawRevert`. Typed primitives such as +`mstore`, `calldatacopy`, and similar common operations should remain +first-class only when Verity commits to their semantics and they are useful in +proofs or audits. diff --git a/packages/verity-edsl/lakefile.lean b/packages/verity-edsl/lakefile.lean index fb84031ed..35c5e5480 100644 --- a/packages/verity-edsl/lakefile.lean +++ b/packages/verity-edsl/lakefile.lean @@ -27,5 +27,6 @@ lean_lib «Verity» where .one `Verity.Specs.Common, .one `Verity.Specs.Common.Sum, .one `Verity.Proofs.Stdlib.Math, - .one `Verity.Proofs.Stdlib.ListSum + .one `Verity.Proofs.Stdlib.ListSum, + .one `Verity.Proofs.Stdlib.Automation ]