Add target-fork conditional compilation (#1940)

* Add target-fork conditional compilation

* Close fork condition proof surfaces

* Define fork condition source fallback

* chore: auto-refresh derived artifacts

* Close fork conditional proof surface

* Close fork conditional generic induction case

---------

Co-authored-by: github-actions[bot] <github-actions[bot]@users.noreply.github.com>

Author: Th0rgal

Compiler/CompilationModel/EcmAxiomCollection.lean

@@ -23,6 +23,7 @@ where
     | _ => []
   collectExprEcmAxioms : Expr → List (String × String)
     | .ite cond a b => collectExprEcmAxioms cond ++ collectExprEcmAxioms a ++ collectExprEcmAxioms b
+    | .forkIfAtLeast _ thenExpr elseExpr => collectExprEcmAxioms thenExpr ++ collectExprEcmAxioms elseExpr
     | _ => []
 
 end Compiler.CompilationModel

Compiler/CompilationModel/ExpressionCompile.lean

@@ -453,6 +453,8 @@ def compileExpr (fields : List Field)
           if args.length != inArity then
             throw s!"Compilation error: intrinsic {name} builtin {builtinName} expects {inArity} arg(s), got {args.length}"
           pure (YulExpr.call builtinName argExprs)
+  | Expr.forkIfAtLeast required _thenExpr _elseExpr =>
+      throw s!"Compilation error: unresolved fork_if_at_least {required}; compile through compileSpecsWithOptions so the branch can be selected from --target-fork before Yul emission"
   | Expr.eq a b      => return yulBinOp "eq"  (← compileExpr fields dynamicSource a) (← compileExpr fields dynamicSource b)
   | Expr.gt a b      => return yulBinOp "gt"  (← compileExpr fields dynamicSource a) (← compileExpr fields dynamicSource b)
   | Expr.sgt a b     => return yulBinOp "sgt" (← compileExpr fields dynamicSource a) (← compileExpr fields dynamicSource b)

Compiler/CompilationModel/LogicalPurity.lean

@@ -51,6 +51,8 @@ partial def exprContainsCallLike (expr : Expr) : Bool :=
       exprContainsCallLike a || exprContainsCallLike b
   | Expr.intrinsic _ _ _ args =>
       exprListContainsCallLike args
+  | Expr.forkIfAtLeast _ thenExpr elseExpr =>
+      exprContainsCallLike thenExpr || exprContainsCallLike elseExpr
   | Expr.mulDivDown a b c | Expr.mulDivUp a b c
   | Expr.mulDiv512Down a b c | Expr.mulDiv512Up a b c =>
       exprContainsCallLike a || exprContainsCallLike b || exprContainsCallLike c
@@ -159,6 +161,8 @@ def exprContainsUnsafeLogicalCallLike (expr : Expr) : Bool :=
       exprContainsUnsafeLogicalCallLike a || exprContainsUnsafeLogicalCallLike b
   | Expr.intrinsic _ _ _ args =>
       exprListAnyUnsafeLogicalCallLike args
+  | Expr.forkIfAtLeast _ thenExpr elseExpr =>
+      exprContainsUnsafeLogicalCallLike thenExpr || exprContainsUnsafeLogicalCallLike elseExpr
   | Expr.mulDivDown a b c
   | Expr.mulDiv512Down a b c =>
       exprContainsUnsafeLogicalCallLike a || exprContainsUnsafeLogicalCallLike b || exprContainsUnsafeLogicalCallLike c

Compiler/CompilationModel/ScopeValidation.lean

@@ -367,6 +367,9 @@ def validateScopedExprIdentifiers
       validateScopedExprIdentifiers context params paramScope dynamicParams localScope constructorArgCount b
   | Expr.intrinsic _ _ _ args =>
       validateScopedExprIdentifiersList context params paramScope dynamicParams localScope constructorArgCount args
+  | Expr.forkIfAtLeast _ thenExpr elseExpr => do
+      validateScopedExprIdentifiers context params paramScope dynamicParams localScope constructorArgCount thenExpr
+      validateScopedExprIdentifiers context params paramScope dynamicParams localScope constructorArgCount elseExpr
   | Expr.wDivUp a b => do
       validateArithDuplicatedOperandPurity context [b]
       validateScopedExprIdentifiers context params paramScope dynamicParams localScope constructorArgCount a

Compiler/CompilationModel/Types.lean

@@ -483,6 +483,14 @@ inductive Expr
       (lowering : Verity.Core.Intrinsics.YulLowering)
       (minFork : Verity.Core.Intrinsics.HardFork)
       (args : List Expr)
+  /-- Compile-time fork selection. `thenExpr` is selected when the compiler
+      target fork is at least `required`; otherwise `elseExpr` is selected.
+      The unselected branch is removed before intrinsic fork gates and Yul
+      lowering run, so this is suitable for explicit opcode/emulation fallback
+      pairs without silently weakening `min_fork` on the intrinsic itself. -/
+  | forkIfAtLeast
+      (required : Verity.Core.Intrinsics.HardFork)
+      (thenExpr elseExpr : Expr)
   | eq (a b : Expr)
   | ge (a b : Expr)
   | gt (a b : Expr)  -- Greater than (strict)

Compiler/CompilationModel/UsageAnalysis.lean

@@ -173,6 +173,9 @@ def exprUsesArrayElementKind (includePlain includeWord : Bool) : Expr → Bool
         exprUsesArrayElementKind includePlain includeWord b
   | Expr.intrinsic _ _ _ args =>
       exprListUsesArrayElementKind includePlain includeWord args
+  | Expr.forkIfAtLeast _ thenExpr elseExpr =>
+      exprUsesArrayElementKind includePlain includeWord thenExpr ||
+        exprUsesArrayElementKind includePlain includeWord elseExpr
   | Expr.mulDivDown a b c | Expr.mulDivUp a b c | Expr.mulDiv512Down a b c | Expr.mulDiv512Up a b c =>
       exprUsesArrayElementKind includePlain includeWord a ||
         exprUsesArrayElementKind includePlain includeWord b ||
@@ -356,6 +359,8 @@ def exprUsesArrayElement : Expr → Bool
     Expr.ceilDiv a b =>
       exprUsesArrayElement a || exprUsesArrayElement b
   | Expr.intrinsic _ _ _ args => exprListUsesArrayElement args
+  | Expr.forkIfAtLeast _ thenExpr elseExpr =>
+      exprUsesArrayElement thenExpr || exprUsesArrayElement elseExpr
   | Expr.mulDivDown a b c | Expr.mulDivUp a b c | Expr.mulDiv512Down a b c | Expr.mulDiv512Up a b c =>
       exprUsesArrayElement a || exprUsesArrayElement b || exprUsesArrayElement c
   | Expr.bitNot a | Expr.logicalNot a =>
@@ -559,6 +564,8 @@ def exprUsesParamDynamicHeadWord : Expr → Bool
   | Expr.wMulDown a b | Expr.wDivUp a b | Expr.min a b | Expr.max a b | Expr.ceilDiv a b =>
       exprUsesParamDynamicHeadWord a || exprUsesParamDynamicHeadWord b
   | Expr.intrinsic _ _ _ args => exprListUsesParamDynamicHeadWord args
+  | Expr.forkIfAtLeast _ thenExpr elseExpr =>
+      exprUsesParamDynamicHeadWord thenExpr || exprUsesParamDynamicHeadWord elseExpr
   | Expr.mulDivDown a b c | Expr.mulDivUp a b c
   | Expr.mulDiv512Down a b c | Expr.mulDiv512Up a b c
   | Expr.ite a b c =>
@@ -701,6 +708,8 @@ def exprUsesMulDiv512 : Expr → Bool
   | Expr.wMulDown a b | Expr.wDivUp a b | Expr.min a b | Expr.max a b | Expr.ceilDiv a b =>
       exprUsesMulDiv512 a || exprUsesMulDiv512 b
   | Expr.intrinsic _ _ _ args => exprListUsesMulDiv512 args
+  | Expr.forkIfAtLeast _ thenExpr elseExpr =>
+      exprUsesMulDiv512 thenExpr || exprUsesMulDiv512 elseExpr
   | Expr.mulDivDown a b c | Expr.mulDivUp a b c | Expr.ite a b c =>
       exprUsesMulDiv512 a || exprUsesMulDiv512 b || exprUsesMulDiv512 c
   | Expr.literal _ | Expr.param _ | Expr.constructorArg _
@@ -859,6 +868,8 @@ def exprUsesStorageArrayElement : Expr → Bool
     Expr.ceilDiv a b =>
       exprUsesStorageArrayElement a || exprUsesStorageArrayElement b
   | Expr.intrinsic _ _ _ args => exprListUsesStorageArrayElement args
+  | Expr.forkIfAtLeast _ thenExpr elseExpr =>
+      exprUsesStorageArrayElement thenExpr || exprUsesStorageArrayElement elseExpr
   | Expr.mulDivDown a b c | Expr.mulDivUp a b c | Expr.mulDiv512Down a b c | Expr.mulDiv512Up a b c =>
       exprUsesStorageArrayElement a || exprUsesStorageArrayElement b || exprUsesStorageArrayElement c
   | Expr.bitNot a | Expr.logicalNot a =>
@@ -1021,6 +1032,8 @@ def exprUsesDynamicBytesEq : Expr → Bool
   | Expr.ceilDiv a b =>
       exprUsesDynamicBytesEq a || exprUsesDynamicBytesEq b
   | Expr.intrinsic _ _ _ args => exprListUsesDynamicBytesEq args
+  | Expr.forkIfAtLeast _ thenExpr elseExpr =>
+      exprUsesDynamicBytesEq thenExpr || exprUsesDynamicBytesEq elseExpr
   | Expr.mulDivDown a b c | Expr.mulDivUp a b c | Expr.mulDiv512Down a b c | Expr.mulDiv512Up a b c =>
       exprUsesDynamicBytesEq a || exprUsesDynamicBytesEq b || exprUsesDynamicBytesEq c
   | Expr.bitNot a | Expr.logicalNot a =>

Compiler/CompilationModel/Validation.lean

@@ -302,6 +302,8 @@ def exprReadsStateOrEnv : Expr → Bool
     Expr.ceilDiv a b =>
       exprReadsStateOrEnv a || exprReadsStateOrEnv b
   | Expr.intrinsic _ _ _ args => exprListReadsStateOrEnv args
+  | Expr.forkIfAtLeast _ thenExpr elseExpr =>
+      exprReadsStateOrEnv thenExpr || exprReadsStateOrEnv elseExpr
   | Expr.mulDivDown a b c | Expr.mulDivUp a b c
   | Expr.mulDiv512Down a b c | Expr.mulDiv512Up a b c =>
       exprReadsStateOrEnv a || exprReadsStateOrEnv b || exprReadsStateOrEnv c
@@ -361,6 +363,8 @@ def exprWritesState : Expr → Bool
   | Expr.externalCall name args =>
       if name == builtinExpName then exprListWritesState args else true
   | Expr.intrinsic _ _ _ args => exprListWritesState args
+  | Expr.forkIfAtLeast _ thenExpr elseExpr =>
+      exprWritesState thenExpr || exprWritesState elseExpr
   | Expr.internalCall _ _ => true
   | Expr.adtConstruct _ _ args => exprListWritesState args
   | Expr.extcodesize addr =>
@@ -519,6 +523,8 @@ def exprHasUntrackableWrites : Expr → Bool
   | Expr.byte a b =>
       exprHasUntrackableWrites a || exprHasUntrackableWrites b
   | Expr.intrinsic _ _ _ args => exprListHasUntrackableWrites args
+  | Expr.forkIfAtLeast _ thenExpr elseExpr =>
+      exprHasUntrackableWrites thenExpr || exprHasUntrackableWrites elseExpr
   | Expr.lt a b | Expr.gt a b | Expr.slt a b | Expr.sgt a b | Expr.eq a b
   | Expr.ge a b | Expr.le a b | Expr.signextend a b
   | Expr.logicalAnd a b | Expr.logicalOr a b
@@ -671,6 +677,8 @@ def exprContainsExternalCall : Expr → Bool
   | Expr.byte a b =>
       exprContainsExternalCall a || exprContainsExternalCall b
   | Expr.intrinsic _ _ _ args => exprListContainsExternalCall args
+  | Expr.forkIfAtLeast _ thenExpr elseExpr =>
+      exprContainsExternalCall thenExpr || exprContainsExternalCall elseExpr
   | Expr.lt a b | Expr.gt a b | Expr.slt a b | Expr.sgt a b | Expr.eq a b
   | Expr.ge a b | Expr.le a b | Expr.signextend a b
   | Expr.logicalAnd a b | Expr.logicalOr a b
@@ -753,6 +761,8 @@ def exprMayContainExternalCall : Expr → Bool
   | Expr.byte a b =>
       exprMayContainExternalCall a || exprMayContainExternalCall b
   | Expr.intrinsic _ _ _ args => exprListMayContainExternalCall args
+  | Expr.forkIfAtLeast _ thenExpr elseExpr =>
+      exprMayContainExternalCall thenExpr || exprMayContainExternalCall elseExpr
   | Expr.lt a b | Expr.gt a b | Expr.slt a b | Expr.sgt a b | Expr.eq a b
   | Expr.ge a b | Expr.le a b | Expr.signextend a b
   | Expr.logicalAnd a b | Expr.logicalOr a b
@@ -1065,6 +1075,9 @@ def exprWritesStateWithFunctionEffects
       exprWritesStateWithFunctionEffects effects a ||
         exprWritesStateWithFunctionEffects effects b
   | Expr.intrinsic _ _ _ args => exprListWritesStateWithFunctionEffects effects args
+  | Expr.forkIfAtLeast _ thenExpr elseExpr =>
+      exprWritesStateWithFunctionEffects effects thenExpr ||
+        exprWritesStateWithFunctionEffects effects elseExpr
   | Expr.mulDivDown a b c | Expr.mulDivUp a b c
   | Expr.mulDiv512Down a b c | Expr.mulDiv512Up a b c =>
       exprWritesStateWithFunctionEffects effects a ||
@@ -1312,6 +1325,9 @@ def exprReadsStateOrEnvWithFunctionEffects
       exprReadsStateOrEnvWithFunctionEffects effects a ||
         exprReadsStateOrEnvWithFunctionEffects effects b
   | Expr.intrinsic _ _ _ args => exprListReadsStateOrEnvWithFunctionEffects effects args
+  | Expr.forkIfAtLeast _ thenExpr elseExpr =>
+      exprReadsStateOrEnvWithFunctionEffects effects thenExpr ||
+        exprReadsStateOrEnvWithFunctionEffects effects elseExpr
   | Expr.mulDivDown a b c | Expr.mulDivUp a b c
   | Expr.mulDiv512Down a b c | Expr.mulDiv512Up a b c =>
       exprReadsStateOrEnvWithFunctionEffects effects a ||
@@ -1633,6 +1649,8 @@ def exprContainsAdtConstruct : Expr → Bool
   | Expr.byte a b =>
       exprContainsAdtConstruct a || exprContainsAdtConstruct b
   | Expr.intrinsic _ _ _ args => exprListContainsAdtConstruct args
+  | Expr.forkIfAtLeast _ thenExpr elseExpr =>
+      exprContainsAdtConstruct thenExpr || exprContainsAdtConstruct elseExpr
   | Expr.lt a b | Expr.gt a b | Expr.slt a b | Expr.sgt a b | Expr.eq a b
   | Expr.ge a b | Expr.le a b | Expr.signextend a b
   | Expr.logicalAnd a b | Expr.logicalOr a b

Compiler/CompilationModel/ValidationCalls.lean

@@ -242,6 +242,9 @@ def validateInternalCallShapesInExpr
       validateInternalCallShapesInExpr functions callerName b
   | Expr.intrinsic _ _ _ args =>
       validateInternalCallShapesInExprList functions callerName args
+  | Expr.forkIfAtLeast _ thenExpr elseExpr => do
+      validateInternalCallShapesInExpr functions callerName thenExpr
+      validateInternalCallShapesInExpr functions callerName elseExpr
   | Expr.mulDivDown a b c | Expr.mulDivUp a b c
   | Expr.mulDiv512Down a b c | Expr.mulDiv512Up a b c => do
       validateInternalCallShapesInExpr functions callerName a
@@ -517,6 +520,9 @@ def validateExternalCallTargetsInExpr
       validateExternalCallTargetsInExpr externals context b
   | Expr.intrinsic _ _ _ args =>
       validateExternalCallTargetsInExprList externals context args
+  | Expr.forkIfAtLeast _ thenExpr elseExpr => do
+      validateExternalCallTargetsInExpr externals context thenExpr
+      validateExternalCallTargetsInExpr externals context elseExpr
   | Expr.mulDivDown a b c | Expr.mulDivUp a b c
   | Expr.mulDiv512Down a b c | Expr.mulDiv512Up a b c => do
       validateExternalCallTargetsInExpr externals context a

Compiler/CompilationModel/ValidationHelpers.lean

@@ -112,6 +112,7 @@ def collectExprNames : Expr → List String
   | Expr.byte index value => collectExprNames index ++ collectExprNames value
   | Expr.signextend byteIndex value => collectExprNames byteIndex ++ collectExprNames value
   | Expr.intrinsic _name _ _ args => collectExprListNames args
+  | Expr.forkIfAtLeast _ thenExpr elseExpr => collectExprNames thenExpr ++ collectExprNames elseExpr
   | Expr.eq a b => collectExprNames a ++ collectExprNames b
   | Expr.ge a b => collectExprNames a ++ collectExprNames b
   | Expr.gt a b => collectExprNames a ++ collectExprNames b

Compiler/CompilationModel/ValidationInterop.lean

@@ -105,6 +105,9 @@ def validateInteropExpr (context : String) : Expr → Except String Unit
       validateInteropExpr context b
   | Expr.intrinsic _ _ _ args =>
       validateInteropExprList context args
+  | Expr.forkIfAtLeast _ thenExpr elseExpr => do
+      validateInteropExpr context thenExpr
+      validateInteropExpr context elseExpr
   | Expr.mulDivDown a b c | Expr.mulDivUp a b c
   | Expr.mulDiv512Down a b c | Expr.mulDiv512Up a b c => do
       validateInteropExpr context a