Canonicalize Osaka intrinsic fork

Author: Th0rgal

AXIOMS.md

@@ -204,7 +204,7 @@ its own `AXIOMS.md` or equivalent trust-boundary document.
 For example, a Tamago CLZ intrinsic should document the consumer-side
 `clz_matches_eip7939` assumption: the Lean `semantics` function used by Tamago
 proofs matches the EIP-7939 opcode emitted as `verbatim_1i_1o(hex"1e", x)` on
-Fusaka-or-later chains.
+chains that support Osaka-or-later execution semantics.
 
 These obligations are outside this registry because they are not axioms in the
 Verity project. Future consumer trust reports should surface them

CONTRIBUTING.md

@@ -67,7 +67,7 @@ in this repository should add generic intrinsic mechanics, not opcode-specific
 business logic. The consumer repository must document any generated obligation
 in its own `AXIOMS.md` or trust-boundary document. Set `min_fork` to the first
 fork where the emitted opcode is valid; Verity accepts `cancun`, `prague`, and
-`fusaka` (`osaka` is parsed as the Fusaka execution-layer alias) and enforces
+`osaka` (`fusaka` is parsed as the Ethereum combined-upgrade alias) and enforces
 the declaration against `--target-fork`.
 
 See [docs/INTRINSICS.md](docs/INTRINSICS.md) for the declaration format,

Compiler/CompileDriverTest.lean

@@ -80,7 +80,7 @@ private def futureForkIntrinsicSpec : CompilationModel := {
         Stmt.return
           (Expr.intrinsic "futureIntrinsic"
             (Verity.Core.Intrinsics.YulLowering.verbatim 1 1 "1e")
-            Verity.Core.Intrinsics.HardFork.fusaka
+            Verity.Core.Intrinsics.HardFork.osaka
             [Expr.param "x"])
       ]
     }
@@ -1155,10 +1155,10 @@ unsafe def runTests : IO Unit := do
     (compileSpecsWithOptions [futureForkIntrinsicSpec]
       s!"/tmp/verity-compile-driver-test-{nonce}-future-intrinsic-fail"
       false [] {} none none none none)
-    "requires min_fork=fusaka, but target_fork=cancun"
+    "requires min_fork=osaka, but target_fork=cancun"
   compileSpecsWithOptions [futureForkIntrinsicSpec]
     s!"/tmp/verity-compile-driver-test-{nonce}-future-intrinsic-ok"
-    false [] { targetFork := Verity.Core.Intrinsics.HardFork.fusaka } none none none none
+    false [] { targetFork := Verity.Core.Intrinsics.HardFork.osaka } none none none none
   IO.println "✓ compileSpecsWithOptions accepts intrinsic at matching target fork"
   compileSpecsWithOptions [futureForkIntrinsicSpec]
     s!"/tmp/verity-compile-driver-test-{nonce}-future-intrinsic-override"

Compiler/MainDriver.lean

@@ -73,7 +73,7 @@ private def parseArgs (args : List String) : IO CLIArgs := do
         IO.println "  --manifest <path>  Manifest file with one Lean module per line"
         IO.println "  --module <name>    Import a Lean module and compile its canonical `<Module>.spec`"
         IO.println "  --backend-profile <semantic|solidity-parity-ordering>"
-        IO.println "  --target-fork <cancun|prague|fusaka|osaka>  EVM fork target for intrinsic min_fork checks (default: cancun)"
+        IO.println "  --target-fork <cancun|prague|osaka|fusaka>  EVM fork target for intrinsic min_fork checks (default: cancun; fusaka is an alias for osaka)"
         IO.println "  --allow-future-fork-intrinsics  Allow intrinsics whose min_fork is newer than --target-fork"
         IO.println "  --trust-report <path>       Write JSON trust-surface report"
         IO.println "  --assumption-report <path>  Write JSON assumption inventory report"
@@ -142,7 +142,7 @@ private def parseArgs (args : List String) : IO CLIArgs := do
         | some fork => go rest { cfg with targetFork := fork, targetForkExplicit := true }
         | none =>
             throw (IO.userError
-              s!"Invalid value for --target-fork: {raw} (expected cancun, prague, fusaka, or osaka alias)")
+              s!"Invalid value for --target-fork: {raw} (expected cancun, prague, osaka, or fusaka alias)")
     | ["--target-fork"] =>
         throw (IO.userError "Missing value for --target-fork")
     | "--allow-future-fork-intrinsics" :: rest =>

Compiler/MainPatched.lean

@@ -126,7 +126,7 @@ private def parseArgs (args : List String) : IO CLIArgs := do
         IO.println "  --module <name>    Import a Lean module and compile its canonical `<Module>.spec`"
         IO.println "  --backend-profile <semantic|solidity-parity-ordering|solidity-parity>"
         IO.println "  --parity-pack <id> Versioned parity-pack tuple (see docs/PARITY_PACKS.md)"
-        IO.println "  --target-fork <cancun|prague|fusaka|osaka>  EVM fork target for intrinsic min_fork checks (default: cancun)"
+        IO.println "  --target-fork <cancun|prague|osaka|fusaka>  EVM fork target for intrinsic min_fork checks (default: cancun; fusaka is an alias for osaka)"
         IO.println "  --allow-future-fork-intrinsics  Allow intrinsics whose min_fork is newer than --target-fork"
         IO.println "  --enable-patches   Enable deterministic Yul patch pass"
         IO.println "  --patch-max-iterations <n>  Max patch-pass fixpoint iterations (default: 2)"
@@ -225,7 +225,7 @@ private def parseArgs (args : List String) : IO CLIArgs := do
         | some fork => go rest { cfg with targetFork := fork, targetForkExplicit := true }
         | none =>
             throw (IO.userError
-              s!"Invalid value for --target-fork: {raw} (expected cancun, prague, fusaka, or osaka alias)")
+              s!"Invalid value for --target-fork: {raw} (expected cancun, prague, osaka, or fusaka alias)")
     | ["--target-fork"] =>
         throw (IO.userError "Missing value for --target-fork")
     | "--allow-future-fork-intrinsics" :: rest =>

Contracts/Smoke.lean

@@ -28,10 +28,10 @@ def plusInt256Helper (a : Uint256) (b : Int256) : Uint256 :=
 def eqWordHelper (a : Uint256) (b : Uint256) : Uint256 :=
   if a = b then 1 else 0
 
--- Focused minimal verity_intrinsic example (CLZ via EIP-7939 Fusaka).
+-- Focused minimal verity_intrinsic example (CLZ via EIP-7939 Osaka).
 -- Declaration shape per plan.md; the explicit intrinsic use site emits
 -- verbatim_1i_1o(hex"1e", x) in Yul.
-verity_intrinsic clz (x : Uint256) : Uint256 where pure; yul := verbatim 1 1 (hex "1e"); min_fork := fusaka; semantics := (fun x => Verity.Core.Uint256.ofNat (if x.val = 0 then 256 else 255 - Nat.log2 x.val)); obligation [clz_matches_eip7939 := assumed "EIP-7939 CLZ opcode; chain must be Fusaka+"]
+verity_intrinsic clz (x : Uint256) : Uint256 where pure; yul := verbatim 1 1 (hex "1e"); min_fork := osaka; semantics := (fun x => Verity.Core.Uint256.ofNat (if x.val = 0 then 256 else 255 - Nat.log2 x.val)); obligation [clz_matches_eip7939 := assumed "EIP-7939 CLZ opcode; chain must support Osaka+ execution semantics"]
 
 verity_contract IntrinsicClzSmoke where
   storage

Verity/Core/Intrinsics.lean

@@ -19,13 +19,13 @@ namespace Verity.Core.Intrinsics
 inductive HardFork where
   | cancun
   | prague
-  | fusaka
+  | osaka
   deriving Repr, BEq, DecidableEq, Inhabited
 
 def HardFork.rank : HardFork → Nat
   | .cancun => 0
   | .prague => 1
-  | .fusaka => 2
+  | .osaka => 2
 
 /-- `allows target required` is the fail-closed fork guard used by intrinsic
     callers: the target fork must be at least the intrinsic's minimum fork. -/
@@ -35,17 +35,18 @@ def HardFork.allows (target required : HardFork) : Bool :=
 def HardFork.toString : HardFork → String
   | .cancun => "cancun"
   | .prague => "prague"
-  | .fusaka => "fusaka"
+  | .osaka => "osaka"
 
 instance : ToString HardFork := ⟨HardFork.toString⟩
 
 def HardFork.parse? (raw : String) : Option HardFork :=
   match raw with
   | "cancun" => some .cancun
   | "prague" => some .prague
-  | "fusaka" => some .fusaka
-  -- Solidity's execution-layer name for the Fusaka execution upgrade.
-  | "osaka" => some .fusaka
+  -- Ethereum's combined network upgrade name is Fusaka; the execution-layer
+  -- fork relevant to compiler targets is Osaka.
+  | "fusaka" => some .osaka
+  | "osaka" => some .osaka
   | _ => none
 
 @[simp] theorem HardFork.allows_refl (fork : HardFork) :
@@ -55,20 +56,20 @@ def HardFork.parse? (raw : String) : Option HardFork :=
 @[simp] theorem HardFork.cancun_not_allow_prague :
     HardFork.allows .cancun .prague = false := rfl
 
-@[simp] theorem HardFork.cancun_not_allow_fusaka :
-    HardFork.allows .cancun .fusaka = false := rfl
+@[simp] theorem HardFork.cancun_not_allow_osaka :
+    HardFork.allows .cancun .osaka = false := rfl
 
-@[simp] theorem HardFork.prague_not_allow_fusaka :
-    HardFork.allows .prague .fusaka = false := rfl
+@[simp] theorem HardFork.prague_not_allow_osaka :
+    HardFork.allows .prague .osaka = false := rfl
 
 @[simp] theorem HardFork.prague_allows_cancun :
     HardFork.allows .prague .cancun = true := rfl
 
-@[simp] theorem HardFork.fusaka_allows_cancun :
-    HardFork.allows .fusaka .cancun = true := rfl
+@[simp] theorem HardFork.osaka_allows_cancun :
+    HardFork.allows .osaka .cancun = true := rfl
 
-@[simp] theorem HardFork.fusaka_allows_prague :
-    HardFork.allows .fusaka .prague = true := rfl
+@[simp] theorem HardFork.osaka_allows_prague :
+    HardFork.allows .osaka .prague = true := rfl
 
 theorem HardFork.allows_trans {a b c : HardFork}
     (hab : HardFork.allows a b = true)

Verity/Macro/Elaborate.lean

@@ -169,7 +169,7 @@ def elabVerityIntrinsic : CommandElab := fun stx => do
         match Verity.Core.Intrinsics.HardFork.parse? (toString fork.getId) with
         | some parsed => pure parsed
         | none => throwErrorAt fork
-            s!"unknown intrinsic min_fork '{toString fork.getId}' (expected cancun, prague, fusaka, or osaka alias)"
+            s!"unknown intrinsic min_fork '{toString fork.getId}' (expected cancun, prague, osaka, or fusaka alias)"
       let parsedObligations ← obligations.mapM fun obligation => do
         match obligation with
         | `(verityIntrinsicObligation| $obligationName:ident := $status:ident $message:str) =>

Verity/Macro/Translate.lean

@@ -34,7 +34,7 @@ private def hardForkTermFromParsed (fork : Verity.Core.Intrinsics.HardFork) : Co
   match fork with
   | .cancun => `(Verity.Core.Intrinsics.HardFork.cancun)
   | .prague => `(Verity.Core.Intrinsics.HardFork.prague)
-  | .fusaka => `(Verity.Core.Intrinsics.HardFork.fusaka)
+  | .osaka => `(Verity.Core.Intrinsics.HardFork.osaka)
 
 inductive ValueType where
   | uint256
@@ -4390,9 +4390,9 @@ partial def translatePureExprWithTypes
         | _ => throwErrorAt args "expected list literal [..]"
       `(Compiler.CompilationModel.Expr.externalCall $(strTerm extName) [ $[$argsExprs],* ])
   | `(term| intrinsic_fusaka $name:term $lowering:term $args:term) =>
-      translateIntrinsic name lowering args (← `(Verity.Core.Intrinsics.HardFork.fusaka))
+      translateIntrinsic name lowering args (← `(Verity.Core.Intrinsics.HardFork.osaka))
   | `(term| intrinsic_osaka $name:term $lowering:term $args:term) =>
-      translateIntrinsic name lowering args (← `(Verity.Core.Intrinsics.HardFork.fusaka))
+      translateIntrinsic name lowering args (← `(Verity.Core.Intrinsics.HardFork.osaka))
   | `(term| intrinsic_prague $name:term $lowering:term $args:term) =>
       translateIntrinsic name lowering args (← `(Verity.Core.Intrinsics.HardFork.prague))
   | `(term| intrinsic_cancun $name:term $lowering:term $args:term) =>

docs-site/content/compiler.mdx

@@ -75,7 +75,9 @@ For proof-strict builds, deny flags lock down the trust surface. Each one fails
 | `--deny-layout-incompatibility` | Candidate storage layout breaks baseline (paired with `--layout-compat-report`) |
 | `--deny-unsafe` | Catch-all: any of the above categories trips the build |
 
-Intrinsic users should also set `--target-fork <cancun|prague|fusaka|osaka>`.
+Intrinsic users should also set `--target-fork <cancun|prague|osaka>`.
+`fusaka` is accepted as an alias for Osaka, Ethereum's execution-layer half of
+the combined Fulu/Osaka network upgrade.
 The default is `cancun`; an intrinsic whose `min_fork` is newer than the target
 fails closed unless `--allow-future-fork-intrinsics` is passed explicitly.