Add typed unsafe Yul fragments to CompilationModel (#1942)

* Add raw revert statement support

* Fix rawRevert validation and trust surface coverage

* Handle rawRevert in source semantics proof

* Cover rawRevert in function body scope proofs

* Cover rawRevert in generic induction proofs

* Add typed raw Yul fragments

* Prove raw Yul lowering preserves fragments

* Refine unsafe Yul fragment architecture

* Fix unsafe Yul validation regressions

* Reject stop-only return paths

* Track unsafe Yul effects in modifies and CEI checks

Surface declared raw-Yul storage writes in the modifies() write-set,
flag computed-slot writes as untrackable, and treat fragment call
mechanics as external interactions for CEI ordering and external-call
detection.

Author: Th0rgal

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

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

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
 

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