Fix CREATE2 ECM low-level deny gate

Author: Th0rgal

Compiler/CompilationModel/TrustSurface.lean

@@ -175,6 +175,25 @@ private def collectLowLevelMechanicsFromStmts (stmts : List Stmt) : List String
       []
       stmts
 
+private def lowLevelMechanicsFromEcmModule (mod : ECM.ExternalCallModule) : List String :=
+  match mod.name with
+  | "create2Deploy" => ["create2"]
+  | "sstore2ReadCode" => ["extcodecopy"]
+  | _ => []
+
+private def collectLowLevelMechanicsFromEcmModules (modules : List ECM.ExternalCallModule) : List String :=
+  dedupPreserve (modules.flatMap lowLevelMechanicsFromEcmModule)
+
+private def collectUsedEcmModulesFromStmts (stmts : List Stmt) : List ECM.ExternalCallModule :=
+  dedupEcmModules <|
+    Stmt.foldList
+      (fun acc stmt _ =>
+        match stmt with
+        | .ecm mod _ => acc ++ [mod]
+        | _ => acc)
+      []
+      stmts
+
 private def collectAxiomatizedPrimitivesFromStmts (stmts : List Stmt) : List String :=
   dedupPreserve <|
     Stmt.foldList
@@ -385,7 +404,8 @@ def collectEventEmissionMechanics (spec : CompilationModel) : List String :=
 
 private def isDeniedLowLevelMechanic (mechanic : String) : Bool :=
   match mechanic with
-  | "call" | "staticcall" | "delegatecall" | "create2" | "returndataSize" | "returndataCopy"
+  | "call" | "staticcall" | "delegatecall" | "create2" | "codecopy" | "extcodecopy"
+  | "returndataSize" | "returndataCopy"
   | "revertReturndata" | "rawRevert" | "returndataOptionalBoolAt" | "blobbasefee" => true
   | _ => false
 
@@ -399,7 +419,8 @@ def collectLowLevelMechanics (spec : CompilationModel) : List String :=
     | some ctor => ctor.body
     | none => []
   let allStmts := stmtsFromCtor ++ spec.functions.flatMap stmtsFromFn
-  collectLowLevelMechanicsFromStmts allStmts
+  dedupPreserve (collectLowLevelMechanicsFromStmts allStmts ++
+    collectLowLevelMechanicsFromEcmModules (collectUsedEcmModulesFromStmts allStmts))
 
 /-- Collect partially modeled linear-memory mechanics used by a spec. -/
 def collectLinearMemoryMechanics (spec : CompilationModel) : List String :=
@@ -667,16 +688,6 @@ private def collectUsedExternalNamesByStatus
 example : collectUsedExternalNamesFromStmts [stmtExternalArgSmoke] = ["oracle"] := by
   native_decide
 
-private def collectUsedEcmModulesFromStmts (stmts : List Stmt) : List ECM.ExternalCallModule :=
-  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
     compiler summaries aligned. -/
@@ -923,13 +934,15 @@ private def usageSiteSummary
     (localObligations : List LocalObligation)
     (stmts : List Stmt) :
     UsageSiteSummary :=
-  let mechanics := collectLowLevelMechanicsFromStmts stmts
+  let siteModules := collectUsedEcmModulesFromStmts stmts
+  let mechanics :=
+    dedupPreserve (collectLowLevelMechanicsFromStmts stmts ++
+      collectLowLevelMechanicsFromEcmModules siteModules)
   let eventEmission := collectEventEmissionMechanicsFromStmts stmts
   let proxyUpgradeability := collectProxyUpgradeabilityMechanicsFromMechanics mechanics
   let runtimeIntrospection := collectRuntimeIntrospectionMechanicsFromStmts stmts
   let primitives := collectAxiomatizedPrimitivesFromStmts stmts
   let siteExternals := collectUsedExternalAssumptionsFromStmts spec.externals stmts
-  let siteModules := collectUsedEcmModulesFromStmts stmts
   let siteLocalObligations := collectLocalObligationsFromStmts localObligations stmts
   let siteUnsafeYulContracts := collectUnsafeYulContractsFromStmts stmts
   let siteUnsafeBlocks := collectUnsafeBlockReasonsFromStmts stmts

Compiler/CompilationModelFeatureTest.lean

@@ -6185,6 +6185,13 @@ set_option maxRecDepth 4096 in
       contains macroCreate2SSTORE2TrustReport "\"module\":\"sstore2ReadCode\"" &&
       contains macroCreate2SSTORE2TrustReport "\"assumption\":\"create2_initcode_layout\"" &&
       contains macroCreate2SSTORE2TrustReport "\"assumption\":\"sstore2_pointer_code_layout\"")
+  expectTrue "macro create2/SSTORE2 trust report surfaces low-level mechanics"
+    (contains macroCreate2SSTORE2TrustReport "\"modeledLowLevelMechanics\":[\"create2\",\"extcodecopy\"]")
+  let macroCreate2SSTORE2LowLevelLines :=
+    String.intercalate "\n" (emitLowLevelMechanicsUsageSiteLines [Contracts.Smoke.Create2SSTORE2Smoke.spec])
+  expectTrue "macro create2/SSTORE2 deny-low-level diagnostics include ECM mechanics"
+    (contains macroCreate2SSTORE2LowLevelLines "- Create2SSTORE2Smoke [function:deploy]: create2" &&
+      contains macroCreate2SSTORE2LowLevelLines "- Create2SSTORE2Smoke [function:readCode]: extcodecopy")
   let macroCallbackYul ←
     expectCompileToYul "macro callback ABI smoke spec" Contracts.Smoke.CallbackABISmoke.spec
   expectTrue "macro callback ABI surface stores selector and bytes length"