From ac37d2ceced1d8965db3323346c4efc4bb12319b Mon Sep 17 00:00:00 2001 From: samuelburnham <45365069+samuelburnham@users.noreply.github.com> Date: Wed, 12 Aug 2026 16:58:05 +0000 Subject: [PATCH 1/9] chore: Update Lean to v4.33.0 Toolchain and dependencies bumped by lean-update. --- lake-manifest.json | 13 +++++++------ lakefile.lean | 4 ++-- lean-toolchain | 2 +- 3 files changed, 10 insertions(+), 9 deletions(-) diff --git a/lake-manifest.json b/lake-manifest.json index 4080aa994..de07d4a22 100644 --- a/lake-manifest.json +++ b/lake-manifest.json @@ -1,4 +1,4 @@ -{"version": "1.1.0", +{"version": "1.2.0", "packagesDir": ".lake/packages", "packages": [{"url": "https://github.com/argumentcomputer/lean4lean", @@ -15,20 +15,20 @@ "type": "git", "subDir": null, "scope": "", - "rev": "756e3321fd3b02a85ffda19fef789916223e578c", + "rev": "4488d40d070b9700d4d5a6aa342f0d40c31b2a2d", "name": "batteries", "manifestFile": "lake-manifest.json", - "inputRev": "v4.29.0", + "inputRev": "v4.33.0", "inherited": false, "configFile": "lakefile.toml"}, {"url": "https://github.com/leanprover/lean4-cli", "type": "git", "subDir": null, "scope": "", - "rev": "7802da01beb530bf051ab657443f9cd9bc3e1a29", + "rev": "6130a47896ce867c6a4a55373441e59e565bad0f", "name": "Cli", "manifestFile": "lake-manifest.json", - "inputRev": "v4.29.0", + "inputRev": "v4.33.0", "inherited": false, "configFile": "lakefile.toml"}, {"url": "https://github.com/argumentcomputer/Blake3.lean", @@ -52,4 +52,5 @@ "inherited": false, "configFile": "lakefile.toml"}], "name": "ix", - "lakeDir": ".lake"} + "lakeDir": ".lake", + "fixedToolchain": false} diff --git a/lakefile.lean b/lakefile.lean index 65077fb0d..e2da393d7 100644 --- a/lakefile.lean +++ b/lakefile.lean @@ -11,10 +11,10 @@ require Blake3 from git "https://github.com/argumentcomputer/Blake3.lean" @ "c6db090374cb3c3c717691beb6cd18bb08936598" require Cli from git - "https://github.com/leanprover/lean4-cli" @ "v4.29.0" + "https://github.com/leanprover/lean4-cli" @ "v4.33.0" require batteries from git - "https://github.com/leanprover-community/batteries" @ "v4.29.0" + "https://github.com/leanprover-community/batteries" @ "v4.33.0" /- Reference Lean4-in-Lean4 theory and checker. `IxTcVerify` imports its Theory/Verify specification surface, while `bench-lean4lean` and the ignored diff --git a/lean-toolchain b/lean-toolchain index 14791d727..025e59548 100644 --- a/lean-toolchain +++ b/lean-toolchain @@ -1 +1 @@ -leanprover/lean4:v4.29.0 +leanprover/lean4:v4.33.0 From a8619ce7063be7a3f9a8565097ec856241043b45 Mon Sep 17 00:00:00 2001 From: samuelburnham <45365069+samuelburnham@users.noreply.github.com> Date: Wed, 12 Aug 2026 14:44:49 -0400 Subject: [PATCH 2/9] ci: Use lean-update's pr setting `pr: true` opens the update PR on any outcome and skips the updater's validation build by default; the PR's own CI is the authority on whether the update builds. --- .github/workflows/update.yml | 5 ++++- 1 file changed, 4 insertions(+), 1 deletion(-) diff --git a/.github/workflows/update.yml b/.github/workflows/update.yml index 78293653d..391a8ffe7 100644 --- a/.github/workflows/update.yml +++ b/.github/workflows/update.yml @@ -32,6 +32,9 @@ jobs: # pinned to a commit hash is reported and left alone. - uses: argumentcomputer/lean-update@dev with: + # The root package and the compile benchmarks; Benchmarks/CompileFC + # is deliberately left on its old toolchain, so no glob here. + lake_package_directory: ". Benchmarks/Compile" bump_mode: pinned-tags - on_update_fails: pr + pr: true token: ${{ steps.app-token.outputs.token }} From aef357cbc4bdf577aa58baca81199e8e356dbfe0 Mon Sep 17 00:00:00 2001 From: samuelburnham <45365069+samuelburnham@users.noreply.github.com> Date: Fri, 17 Jul 2026 17:50:09 -0400 Subject: [PATCH 3/9] chore: Adapt sources and pins to Lean v4.33.0 MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Carries the v4.31 adaptation work forward: Std.HashMap `find?` renames to `get?` (including call sites added on main since), the ByteArray FFI helpers removed on the Lean and Rust sides, and assorted API fixes. Dependency pins move to v4.33.0: Cli and batteries by tag, LSpec to the merge commit of its v4.33.0 bump, and Blake3 to its v4.33.0 bump commit — the manifest entry for Blake3 still needs `lake update Blake3` once that commit is reachable on the remote. Benchmarks/Compile moves to the v4.33.0 toolchain with mathlib and FLT at their v4.33.0 tags. --- Benchmarks/Compile/lake-manifest.json | 63 ++++++++++++++------------- Benchmarks/Compile/lakefile.toml | 4 +- Benchmarks/Compile/lean-toolchain | 2 +- Cargo.lock | 4 +- Cargo.toml | 4 +- Ix/Address.lean | 1 - Ix/Aiur/Compiler.lean | 2 +- Ix/Aiur/Goldilocks.lean | 2 +- Ix/Benchmark/Bench.lean | 2 - Ix/ByteArray.lean | 18 -------- Ix/Common.lean | 1 + Ix/CompileM.lean | 12 ++--- Ix/Environment.lean | 7 +-- Ix/IxonUniv.lean | 4 +- Ix/Merkle.lean | 1 - Ix/Meta.lean | 3 +- Tests/ByteArray.lean | 24 ---------- Tests/Ix/Kernel/TutorialMeta.lean | 2 +- Tests/Keccak.lean | 1 - Tests/Main.lean | 2 - crates/ffi/src/byte_array.rs | 11 ----- crates/ffi/src/lib.rs | 1 - flake.lock | 12 ++--- lake-manifest.json | 18 ++++++-- lakefile.lean | 4 +- 25 files changed, 77 insertions(+), 128 deletions(-) delete mode 100644 Ix/ByteArray.lean delete mode 100644 Tests/ByteArray.lean delete mode 100644 crates/ffi/src/byte_array.rs diff --git a/Benchmarks/Compile/lake-manifest.json b/Benchmarks/Compile/lake-manifest.json index 0e93ed2c8..40bb5e64e 100644 --- a/Benchmarks/Compile/lake-manifest.json +++ b/Benchmarks/Compile/lake-manifest.json @@ -1,24 +1,24 @@ -{"version": "1.1.0", +{"version": "1.2.0", "packagesDir": ".lake/packages", "packages": [{"url": "https://github.com/leanprover-community/mathlib4", "type": "git", "subDir": null, "scope": "", - "rev": "8a178386ffc0f5fef0b77738bb5449d50efeea95", + "rev": "db584cd6d46c92f209a44c0f1c829460d327499d", "name": "mathlib", "manifestFile": "lake-manifest.json", - "inputRev": "v4.29.0", + "inputRev": "v4.33.0", "inherited": false, "configFile": "lakefile.lean"}, {"url": "https://github.com/ImperialCollegeLondon/FLT", "type": "git", "subDir": null, "scope": "", - "rev": "2d9083d31e10033122dedbcd9406389c2df5be86", + "rev": "45eb9afc55ce36516fc98ba10618c010fdced7dc", "name": "flt", "manifestFile": "lake-manifest.json", - "inputRev": "v4.29.0", + "inputRev": "v4.33.0", "inherited": false, "configFile": "lakefile.toml"}, {"type": "path", @@ -32,7 +32,7 @@ "type": "git", "subDir": null, "scope": "leanprover-community", - "rev": "83e90935a17ca19ebe4b7893c7f7066e266f50d3", + "rev": "b7eb3304aeae834b12dda98993a37f6a41f6f0bb", "name": "plausible", "manifestFile": "lake-manifest.json", "inputRev": "main", @@ -42,7 +42,7 @@ "type": "git", "subDir": null, "scope": "leanprover-community", - "rev": "c5d5b8fe6e5158def25cd28eb94e4141ad97c843", + "rev": "5f4d51b81cbd3f6b32b156bfad9056621a040404", "name": "LeanSearchClient", "manifestFile": "lake-manifest.json", "inputRev": "main", @@ -52,7 +52,7 @@ "type": "git", "subDir": null, "scope": "leanprover-community", - "rev": "48d5698bc464786347c1b0d859b18f938420f060", + "rev": "16f02aa7642864af59f1ff0e384a015994db9118", "name": "importGraph", "manifestFile": "lake-manifest.json", "inputRev": "main", @@ -62,17 +62,17 @@ "type": "git", "subDir": null, "scope": "leanprover-community", - "rev": "3c52dee17f0cd89c1ec14de78920d1bdaa3d26b3", + "rev": "4be2e3d5087eeb272cf5a8853b8f9dd025ef5957", "name": "proofwidgets", "manifestFile": "lake-manifest.json", - "inputRev": "v0.0.95", + "inputRev": "main", "inherited": true, "configFile": "lakefile.lean"}, {"url": "https://github.com/leanprover-community/aesop", "type": "git", "subDir": null, "scope": "leanprover-community", - "rev": "7152850e7b216a0d409701617721b6e469d34bf6", + "rev": "3448c0bcc5ce01b2d1546e483ec3620e32df3d0e", "name": "aesop", "manifestFile": "lake-manifest.json", "inputRev": "master", @@ -82,7 +82,7 @@ "type": "git", "subDir": null, "scope": "leanprover-community", - "rev": "707efb56d0696634e9e965523a1bbe9ac6ce141d", + "rev": "92c15be17b7caf78c2ad767ec40f89052d908d81", "name": "Qq", "manifestFile": "lake-manifest.json", "inputRev": "master", @@ -92,22 +92,12 @@ "type": "git", "subDir": null, "scope": "leanprover-community", - "rev": "756e3321fd3b02a85ffda19fef789916223e578c", + "rev": "4488d40d070b9700d4d5a6aa342f0d40c31b2a2d", "name": "batteries", "manifestFile": "lake-manifest.json", "inputRev": "main", "inherited": true, "configFile": "lakefile.toml"}, - {"url": "https://github.com/leanprover/lean4-cli", - "type": "git", - "subDir": null, - "scope": "leanprover", - "rev": "7802da01beb530bf051ab657443f9cd9bc3e1a29", - "name": "Cli", - "manifestFile": "lake-manifest.json", - "inputRev": "v4.29.0", - "inherited": true, - "configFile": "lakefile.toml"}, {"url": "https://github.com/PatrickMassot/checkdecls.git", "type": "git", "subDir": null, @@ -118,35 +108,46 @@ "inputRev": null, "inherited": true, "configFile": "lakefile.lean"}, - {"url": "https://github.com/digama0/lean4lean", + {"url": "https://github.com/argumentcomputer/lean4lean", "type": "git", "subDir": null, "scope": "", - "rev": "8865b155abbf68d3a827fb3568bf6839780163c2", + "rev": "5e5bb767b3491d21a71908d4c58bcbaa007283bb", "name": "lean4lean", "manifestFile": "lake-manifest.json", - "inputRev": "8865b155abbf68d3a827fb3568bf6839780163c2", + "inputRev": "5e5bb767b3491d21a71908d4c58bcbaa007283bb", + "inherited": true, + "configFile": "lakefile.toml"}, + {"url": "https://github.com/leanprover/lean4-cli", + "type": "git", + "subDir": null, + "scope": "leanprover", + "rev": "6130a47896ce867c6a4a55373441e59e565bad0f", + "name": "Cli", + "manifestFile": "lake-manifest.json", + "inputRev": "v4.33.0", "inherited": true, "configFile": "lakefile.toml"}, {"url": "https://github.com/argumentcomputer/Blake3.lean", "type": "git", "subDir": null, "scope": "", - "rev": "d15f36cf76eb5834b0e623e02b97fd4d95e56cc7", + "rev": "c9b2273fb9c2c33b94eba091dc4111163f5db2bc", "name": "Blake3", "manifestFile": "lake-manifest.json", - "inputRev": "d15f36cf76eb5834b0e623e02b97fd4d95e56cc7", + "inputRev": "c9b2273fb9c2c33b94eba091dc4111163f5db2bc", "inherited": true, "configFile": "lakefile.lean"}, {"url": "https://github.com/argumentcomputer/LSpec", "type": "git", "subDir": null, "scope": "", - "rev": "d3c15b93a1dd4e7c8d5c0c3825c9555737e55c3e", + "rev": "e780f4188c9649aef988270f4d126651460ca9c4", "name": "LSpec", "manifestFile": "lake-manifest.json", - "inputRev": "d3c15b93a1dd4e7c8d5c0c3825c9555737e55c3e", + "inputRev": "e780f4188c9649aef988270f4d126651460ca9c4", "inherited": true, "configFile": "lakefile.toml"}], "name": "Compile", - "lakeDir": ".lake"} + "lakeDir": ".lake", + "fixedToolchain": false} diff --git a/Benchmarks/Compile/lakefile.toml b/Benchmarks/Compile/lakefile.toml index ee3edaa71..fb8be16f3 100644 --- a/Benchmarks/Compile/lakefile.toml +++ b/Benchmarks/Compile/lakefile.toml @@ -30,9 +30,9 @@ path = "../.." [[require]] name = "flt" git = "https://github.com/ImperialCollegeLondon/FLT" -rev = "v4.29.0" +rev = "v4.33.0" [[require]] name = "mathlib" git = "https://github.com/leanprover-community/mathlib4" -rev = "v4.29.0" +rev = "v4.33.0" diff --git a/Benchmarks/Compile/lean-toolchain b/Benchmarks/Compile/lean-toolchain index 14791d727..025e59548 100644 --- a/Benchmarks/Compile/lean-toolchain +++ b/Benchmarks/Compile/lean-toolchain @@ -1 +1 @@ -leanprover/lean4:v4.29.0 +leanprover/lean4:v4.33.0 diff --git a/Cargo.lock b/Cargo.lock index 34329059d..9f5f14d09 100644 --- a/Cargo.lock +++ b/Cargo.lock @@ -190,7 +190,7 @@ checksum = "2af50177e190e07a26ab74f8b1efbfe2ef87da2116221318cb1c2e82baf7de06" [[package]] name = "bignat" version = "0.1.0" -source = "git+https://github.com/argumentcomputer/lean-ffi.git?rev=839b405de708b80504fda39abe1402114b4135a5#839b405de708b80504fda39abe1402114b4135a5" +source = "git+https://github.com/argumentcomputer/lean-ffi.git?rev=a6e781bc55cec99b99fa7a4bee105c5000cec967#a6e781bc55cec99b99fa7a4bee105c5000cec967" dependencies = [ "num-bigint", ] @@ -1902,7 +1902,7 @@ checksum = "bbd2bcb4c963f2ddae06a2efc7e9f3591312473c50c6685e1f298068316e66fe" [[package]] name = "lean-ffi" version = "0.1.0" -source = "git+https://github.com/argumentcomputer/lean-ffi.git?rev=839b405de708b80504fda39abe1402114b4135a5#839b405de708b80504fda39abe1402114b4135a5" +source = "git+https://github.com/argumentcomputer/lean-ffi.git?rev=a6e781bc55cec99b99fa7a4bee105c5000cec967#a6e781bc55cec99b99fa7a4bee105c5000cec967" dependencies = [ "bignat", "bindgen", diff --git a/Cargo.toml b/Cargo.toml index 90ac6ca5f..003d2d195 100644 --- a/Cargo.toml +++ b/Cargo.toml @@ -38,8 +38,8 @@ ixon = { path = "crates/ixon" } ix-kernel = { path = "crates/kernel" } # lean-ffi tree (lean-ffi crate + factored-out bignat sub-crate) -bignat = { git = "https://github.com/argumentcomputer/lean-ffi.git", rev = "839b405de708b80504fda39abe1402114b4135a5" } -lean-ffi = { git = "https://github.com/argumentcomputer/lean-ffi.git", rev = "839b405de708b80504fda39abe1402114b4135a5" } +bignat = { git = "https://github.com/argumentcomputer/lean-ffi.git", rev = "a6e781bc55cec99b99fa7a4bee105c5000cec967" } +lean-ffi = { git = "https://github.com/argumentcomputer/lean-ffi.git", rev = "a6e781bc55cec99b99fa7a4bee105c5000cec967" } # External shared deps anyhow = "1" diff --git a/Ix/Address.lean b/Ix/Address.lean index 22a61b110..a3a75bf25 100644 --- a/Ix/Address.lean +++ b/Ix/Address.lean @@ -1,6 +1,5 @@ module public import Lean.ToExpr -public import Ix.ByteArray public import Ix.Common public import Blake3.Rust diff --git a/Ix/Aiur/Compiler.lean b/Ix/Aiur/Compiler.lean index d85266632..cef51cdae 100644 --- a/Ix/Aiur/Compiler.lean +++ b/Ix/Aiur/Compiler.lean @@ -37,7 +37,7 @@ structure CompiledToplevel where bytecode : Bytecode.Toplevel nameMap : Std.HashMap Global Bytecode.FunIdx -@[inline, expose] +@[inline] def CompiledToplevel.getFuncIdx (ct : CompiledToplevel) (name : Lean.Name) : Option Bytecode.FunIdx := ct.nameMap[Global.mk name]? diff --git a/Ix/Aiur/Goldilocks.lean b/Ix/Aiur/Goldilocks.lean index dc6c485c8..e2f4c45b2 100644 --- a/Ix/Aiur/Goldilocks.lean +++ b/Ix/Aiur/Goldilocks.lean @@ -26,7 +26,7 @@ instance : OfNat G n := ⟨G.ofNat n⟩ let u64 := u8.toUInt64 have h : u64 < gSize := by have lt256 : u64 < 256 := by - simpa [UInt64.lt_iff_toNat_lt] using UInt8.toNat_lt _ + simpa [u64, UInt64.lt_iff_toNat_lt, UInt8.toNat_toUInt64] using UInt8.toNat_lt _ exact UInt64.lt_trans lt256 (by decide) ⟨u64, h⟩ diff --git a/Ix/Benchmark/Bench.lean b/Ix/Benchmark/Bench.lean index 4a77d1ccf..50a90cd53 100644 --- a/Ix/Benchmark/Bench.lean +++ b/Ix/Benchmark/Bench.lean @@ -9,8 +9,6 @@ public import Ix.Benchmark.Report public section -open Batteries (RBMap) - /-! # Benchmarking library modeled after Criterion in Rust and Haskell diff --git a/Ix/ByteArray.lean b/Ix/ByteArray.lean deleted file mode 100644 index 06f56e2b5..000000000 --- a/Ix/ByteArray.lean +++ /dev/null @@ -1,18 +0,0 @@ -module - -public section - -namespace ByteArray - -def beqNoFFI (a b : ByteArray) : Bool := - a.data == b.data - -@[extern "rs_byte_array_beq"] -def beq : @& ByteArray → @& ByteArray → Bool := - beqNoFFI - -instance : BEq ByteArray := ⟨ByteArray.beq⟩ - -end ByteArray - -end diff --git a/Ix/Common.lean b/Ix/Common.lean index 83a9b3a52..2fa53a9a6 100644 --- a/Ix/Common.lean +++ b/Ix/Common.lean @@ -297,6 +297,7 @@ def runFrontend (input : String) (filePath : FilePath) : IO Environment := do checkToolchain let inputCtx := Parser.mkInputContext input filePath.toString let (header, parserState, messages) ← Parser.parseHeader inputCtx + unsafe enableInitializersExecution -- required for `processHeader`'s `loadExts := true` import let (env, messages) ← processHeader header default messages inputCtx 0 let env := env.setMainModule default let commandState := Command.mkState env messages default diff --git a/Ix/CompileM.lean b/Ix/CompileM.lean index 529ca758e..a242dfa61 100644 --- a/Ix/CompileM.lean +++ b/Ix/CompileM.lean @@ -704,7 +704,7 @@ partial def compileExpr (e : Expr) : CompileM (Ixon.Expr × UInt64) := do let recordPatch (root : UInt64) : CompileM Unit := do if compiled.any (·.2.isSome) then pushUnivPatch root (compiled.map fun (cidx, orig?) => orig?.getD cidx) - match mutCtx.find? name with + match mutCtx.get? name with | some recIdx => let root ← allocArenaNode (.ref nameAddr) recordPatch root @@ -1253,7 +1253,7 @@ def collectExprTables (top : Expr) (ctxKey : Address) | .const name lvls _ => for lvl in lvls do univs := univs.push (← compileUniv lvl) - if (mutCtx.find? name).isNone then + if (mutCtx.get? name).isNone then refs := refs.push (← lookupConstAddr name) | .app func arg _ => stack := stack.push arg |>.push func @@ -1389,7 +1389,7 @@ partial def compareExpr (ctx : Ix.MutCtx) (xlvls ylvls : List Name) let univs ← SOrder.zipM (compareLevel xlvls ylvls) xls.toList yls.toList if univs.ord != .eq then pure univs else if x == y then pure ⟨true, .eq⟩ - else match ctx.find? x, ctx.find? y with + else match ctx.get? x, ctx.get? y with | some nx, some ny => pure ⟨false, compare nx ny⟩ | some _, none => pure ⟨true, .lt⟩ | none, some _ => pure ⟨true, .gt⟩ @@ -1423,7 +1423,7 @@ partial def compareExpr (ctx : Ix.MutCtx) (xlvls ylvls : List Name) | .lit .., _ => pure ⟨true, .lt⟩ | _, .lit .. => pure ⟨true, .gt⟩ | .proj tnx ix tx _, .proj tny iy ty _ => do - let tn ← match ctx.find? tnx, ctx.find? tny with + let tn ← match ctx.get? tnx, ctx.get? tny with | some nx, some ny => pure ⟨false, compare nx ny⟩ | none, some _ => pure ⟨true, .gt⟩ | some _, none => pure ⟨true, .lt⟩ @@ -2211,7 +2211,7 @@ def compileMutualBlock (classes : List (List MutConst)) /-- Build mutCtx for an inductive: includes the inductive and all its constructors. -/ def buildInductiveMutCtx (i : InductiveVal) (ctorVals : Array ConstructorVal) : Ix.MutCtx := Id.run do - let mut ctx : Ix.MutCtx := Batteries.RBMap.empty + let mut ctx : Ix.MutCtx := Std.TreeMap.empty -- Inductive at index 0 ctx := ctx.insert i.cnst.name 0 -- Constructors at indices 1, 2, ... @@ -2230,7 +2230,7 @@ def BlockResult.mk' (block : Ixon.Constant) (blockMeta : Ixon.ConstantMeta := .e Returns BlockResult with the constant and any projections needed. -/ def compileConstantInfo (const : ConstantInfo) : CompileM BlockResult := do let name := const.getCnst.name - let mutCtx : Ix.MutCtx := Batteries.RBMap.empty.insert name 0 + let mutCtx : Ix.MutCtx := Std.TreeMap.empty.insert name 0 withMutCtx mutCtx do match const with | .defnInfo d => diff --git a/Ix/Environment.lean b/Ix/Environment.lean index b7cf4da8f..4bb2c6c3f 100644 --- a/Ix/Environment.lean +++ b/Ix/Environment.lean @@ -8,7 +8,7 @@ module public import Blake3.Rust public import Std.Data.HashMap -public import Batteries.Data.RBMap +public import Std.Data.TreeMap public import Ix.Address public section @@ -662,14 +662,11 @@ def Environment.toRaw (env : Environment) : RawEnvironment := /-! ## Context Types for Compilation -/ /-- Mutual context mapping Name to index within block. -/ -abbrev MutCtx := Batteries.RBMap Name Nat nameCompare +abbrev MutCtx := Std.TreeMap Name Nat nameCompare instance : Ord MutCtx where compare a b := compare a.toList b.toList -/-- Set of Names (for tracking constants in a block). -/ -abbrev NameSet := Batteries.RBSet Name nameCompare - end Ix end diff --git a/Ix/IxonUniv.lean b/Ix/IxonUniv.lean index 62e7f9f00..192bb3824 100644 --- a/Ix/IxonUniv.lean +++ b/Ix/IxonUniv.lean @@ -403,12 +403,12 @@ def linearize (norm : CNorm) : Univ := Id.run do for j in [0:order.length] do let p := order[j]! let mctx := (order.take j).mergeSort (· ≤ ·) - if (groups.find? mctx).any (fun sg => sg.atoms.find? p == some 0) then + if (groups.get? mctx).any (fun sg => sg.atoms.get? p == some 0) then consumed := (mctx, p) :: consumed -- Emission. let mut terms : List Univ := [] let mut rootCAbsorbed := false - if let some top := groups.find? [] then + if let some top := groups.get? [] then for (i, k) in top.atoms.toList do if k == 0 && consumed.contains ([], i) then continue diff --git a/Ix/Merkle.lean b/Ix/Merkle.lean index 411ba1400..383989c82 100644 --- a/Ix/Merkle.lean +++ b/Ix/Merkle.lean @@ -34,7 +34,6 @@ module public import Ix.Address -public import Ix.ByteArray public section diff --git a/Ix/Meta.lean b/Ix/Meta.lean index 1e7e38351..7caf96ce2 100644 --- a/Ix/Meta.lean +++ b/Ix/Meta.lean @@ -35,6 +35,7 @@ def getFileEnv (path : FilePath) : IO Environment := do let source ← IO.FS.readFile path let inputCtx := Parser.mkInputContext source path.toString let (header, parserState, messages) ← Parser.parseHeader inputCtx + unsafe enableInitializersExecution -- required for `processHeaderCore`'s `loadExts := true` import let (env, messages) ← processHeaderCore (HeaderSyntax.startPos header) (HeaderSyntax.imports header) (isModule := false) default messages inputCtx 0 @@ -79,7 +80,7 @@ def fetchMathlibCache (cwd : Option FilePath) : IO Unit := do let root := cwd.getD "." let manifest := root / "lake-manifest.json" let contents ← IO.FS.readFile manifest - if contents.containsSubstr "leanprover-community/mathlib4" then + if contents.contains "leanprover-community/mathlib4" then let mathlibBuild := root / ".lake" / "packages" / "mathlib" / ".lake" / "build" if ← mathlibBuild.pathExists then println! "Mathlib cache already present, skipping fetch." diff --git a/Tests/ByteArray.lean b/Tests/ByteArray.lean deleted file mode 100644 index 92be1a47b..000000000 --- a/Tests/ByteArray.lean +++ /dev/null @@ -1,24 +0,0 @@ -module - -public import LSpec -public import Ix.ByteArray - -def arrays : List ByteArray := [ - ⟨#[]⟩, ⟨#[1]⟩, ⟨#[0, 3]⟩, ⟨#[1, 1, 1]⟩, ⟨#[3, 3, 3, 3]⟩, ⟨#[13]⟩ -] - -def arrays' : List ByteArray := [ - ⟨#[1]⟩, ⟨#[2]⟩, ⟨#[0, 3, 0]⟩, ⟨#[1, 2, 1]⟩, ⟨#[3, 3, 4, 3]⟩, ⟨#[13, 0]⟩ -] - -open LSpec - -def beq : TestSeq := - arrays.zip arrays |>.foldl (init := .done) fun tSeq (x, y) => - tSeq ++ (test s!"{x} == {y}" $ x.beq y && x.beqNoFFI y && y.beq x && y.beqNoFFI x) - -def neq : TestSeq := - arrays.zip arrays' |>.foldl (init := .done) fun tSeq (x, y) => - tSeq ++ (test s!"{x} != {y}" $ !x.beq y && !x.beqNoFFI y && !y.beq x && !y.beqNoFFI x) - -public def Tests.ByteArray.suite := [beq, neq] diff --git a/Tests/Ix/Kernel/TutorialMeta.lean b/Tests/Ix/Kernel/TutorialMeta.lean index 7bd6a027b..ac875fb13 100644 --- a/Tests/Ix/Kernel/TutorialMeta.lean +++ b/Tests/Ix/Kernel/TutorialMeta.lean @@ -194,7 +194,7 @@ def elabAndAddTestCaseDecl (name : TSyntax ``declId) (type value : Term) (outcom (declKind : ConstantKind) (skipTC := false) : CommandElabM Unit := liftTermElabM do let (declName, lparams) ← match name with | `(declId| $n:ident) => pure (n.getId, []) - | `(declId| $n:ident .{ $[$ls:ident],* }) => pure (n.getId, ls.toList.map (·.getId)) + | `(declId| $n:ident.{ $[$ls:ident],* }) => pure (n.getId, ls.toList.map (·.getId)) | _ => throwUnsupportedSyntax withLevelNames lparams do let typeExpr ← elabTermAndSynthesize type none diff --git a/Tests/Keccak.lean b/Tests/Keccak.lean index 98d614ef8..1110d329b 100644 --- a/Tests/Keccak.lean +++ b/Tests/Keccak.lean @@ -2,7 +2,6 @@ module public import Ix.Keccak public import LSpec -public import Ix.ByteArray open LSpec diff --git a/Tests/Main.lean b/Tests/Main.lean index 736f65958..529608fa4 100644 --- a/Tests/Main.lean +++ b/Tests/Main.lean @@ -1,5 +1,4 @@ import Tests.Aiur -import Tests.ByteArray import Tests.Ix.Ixon import Tests.Ix.IxonCorpus import Tests.Ix.IxonSyntax @@ -66,7 +65,6 @@ opaque tmpDecodeConstMap : @& List (Lean.Name × Lean.ConstantInfo) → USize /-- Primary test suites - run by default -/ def primarySuites : Std.HashMap String (List LSpec.TestSeq) := .ofList [ ("ffi", Tests.FFI.suite), - ("byte-array", Tests.ByteArray.suite), ("ixon", Tests.Ixon.suite), ("ixon-syntax", Tests.IxonSyntax.suite), ("claim", Tests.Claim.suite), diff --git a/crates/ffi/src/byte_array.rs b/crates/ffi/src/byte_array.rs deleted file mode 100644 index ab53b2d8b..000000000 --- a/crates/ffi/src/byte_array.rs +++ /dev/null @@ -1,11 +0,0 @@ -use lean_ffi::object::{LeanBorrowed, LeanByteArray}; - -/// `@& ByteArray → @& ByteArray → Bool` -/// Efficient implementation for `BEq ByteArray` -#[unsafe(no_mangle)] -extern "C" fn rs_byte_array_beq( - a: LeanByteArray>, - b: LeanByteArray>, -) -> bool { - a.as_bytes() == b.as_bytes() -} diff --git a/crates/ffi/src/lib.rs b/crates/ffi/src/lib.rs index 38df7e1dd..5b404001c 100644 --- a/crates/ffi/src/lib.rs +++ b/crates/ffi/src/lib.rs @@ -8,7 +8,6 @@ ))] pub mod _iroh; pub mod aiur; -pub mod byte_array; #[cfg(all( feature = "net", not(all(target_os = "macos", target_arch = "aarch64")) diff --git a/flake.lock b/flake.lock index 7468797d5..f991113e3 100644 --- a/flake.lock +++ b/flake.lock @@ -33,11 +33,11 @@ ] }, "locked": { - "lastModified": 1776364162, - "narHash": "sha256-l3FectIPaz5Fq1q0YSG7wR7VyybZqt56Sj4kebEoZ+Q=", + "lastModified": 1784318821, + "narHash": "sha256-mgyIRIZAs5pKAD8HT1sATU9QibhEXXaCovjUFT0j3gg=", "owner": "argumentcomputer", "repo": "Blake3.lean", - "rev": "aaf530784082a2c00b0a93648741429d274102ca", + "rev": "2342f0d7f5af12e232b12b8815cd2ada5d0c2bb6", "type": "github" }, "original": { @@ -254,11 +254,11 @@ "nixpkgs": "nixpkgs" }, "locked": { - "lastModified": 1775267043, - "narHash": "sha256-yUCn4Wc5kLboN9JHom/SJAknn7aoSEDyerqFq3k7g0I=", + "lastModified": 1784223297, + "narHash": "sha256-rmEX8SXvtT7Fi8hOZuCXCbpyzno3iTQYnV3WKzsAVHw=", "owner": "lenianiva", "repo": "lean4-nix", - "rev": "56e917e2766385d0b096ea8be9c40ae54bfe138a", + "rev": "82993165f5f30879fc9d40734615ec54cb541e61", "type": "github" }, "original": { diff --git a/lake-manifest.json b/lake-manifest.json index de07d4a22..2f490a921 100644 --- a/lake-manifest.json +++ b/lake-manifest.json @@ -35,21 +35,31 @@ "type": "git", "subDir": null, "scope": "", - "rev": "c6db090374cb3c3c717691beb6cd18bb08936598", + "rev": "c9b2273fb9c2c33b94eba091dc4111163f5db2bc", "name": "Blake3", "manifestFile": "lake-manifest.json", - "inputRev": "c6db090374cb3c3c717691beb6cd18bb08936598", + "inputRev": "c9b2273fb9c2c33b94eba091dc4111163f5db2bc", "inherited": false, "configFile": "lakefile.lean"}, {"url": "https://github.com/argumentcomputer/LSpec", "type": "git", "subDir": null, "scope": "", - "rev": "d3c15b93a1dd4e7c8d5c0c3825c9555737e55c3e", + "rev": "e780f4188c9649aef988270f4d126651460ca9c4", "name": "LSpec", "manifestFile": "lake-manifest.json", - "inputRev": "d3c15b93a1dd4e7c8d5c0c3825c9555737e55c3e", + "inputRev": "e780f4188c9649aef988270f4d126651460ca9c4", "inherited": false, + "configFile": "lakefile.toml"}, + {"url": "https://github.com/leanprover-community/plausible", + "type": "git", + "subDir": null, + "scope": "", + "rev": "b7eb3304aeae834b12dda98993a37f6a41f6f0bb", + "name": "plausible", + "manifestFile": "lake-manifest.json", + "inputRev": "v4.33.0", + "inherited": true, "configFile": "lakefile.toml"}], "name": "ix", "lakeDir": ".lake", diff --git a/lakefile.lean b/lakefile.lean index e2da393d7..f059b888c 100644 --- a/lakefile.lean +++ b/lakefile.lean @@ -5,10 +5,10 @@ package ix where version := v!"0.1.0" require LSpec from git - "https://github.com/argumentcomputer/LSpec" @ "d3c15b93a1dd4e7c8d5c0c3825c9555737e55c3e" + "https://github.com/argumentcomputer/LSpec" @ "e780f4188c9649aef988270f4d126651460ca9c4" require Blake3 from git - "https://github.com/argumentcomputer/Blake3.lean" @ "c6db090374cb3c3c717691beb6cd18bb08936598" + "https://github.com/argumentcomputer/Blake3.lean" @ "c9b2273fb9c2c33b94eba091dc4111163f5db2bc" require Cli from git "https://github.com/leanprover/lean4-cli" @ "v4.33.0" From 097724d3a4412798f031ec20eae6207afe2a5fff Mon Sep 17 00:00:00 2001 From: samuelburnham <45365069+samuelburnham@users.noreply.github.com> Date: Wed, 12 Aug 2026 14:58:48 -0400 Subject: [PATCH 4/9] nix: Switch to the lean4-nix fork API Upstream lean4-nix stops at Lean v4.32.0 and builds toolchains from source behind an overlay; the fork provides released toolchains as plain derivations and removed the overlay API. The overlay block is replaced by `lib.${system}.fromToolchainFile`, and the Lean sysroot for bindgen, the Lake build inputs, the binary wrappers, and the dev shell take the toolchain derivation directly. The dev shell and the crane-side derivations evaluate now. The Lake packages remain blocked on the `blake3-lean` input: it follows this flake's lean4-nix, so Blake3.lean's own fork migration must be pushed and merged, after which `nix flake update blake3-lean` and `lake update Blake3` complete the move. --- flake.lock | 16 ++++++++-------- flake.nix | 22 +++++++++------------- 2 files changed, 17 insertions(+), 21 deletions(-) diff --git a/flake.lock b/flake.lock index f991113e3..faa15cb92 100644 --- a/flake.lock +++ b/flake.lock @@ -33,11 +33,11 @@ ] }, "locked": { - "lastModified": 1784318821, - "narHash": "sha256-mgyIRIZAs5pKAD8HT1sATU9QibhEXXaCovjUFT0j3gg=", + "lastModified": 1786554796, + "narHash": "sha256-4BDdZZ8JNAbPGU2d2hnIfc5gTjj0ZDpaAFLcA6EgMeI=", "owner": "argumentcomputer", "repo": "Blake3.lean", - "rev": "2342f0d7f5af12e232b12b8815cd2ada5d0c2bb6", + "rev": "c9b2273fb9c2c33b94eba091dc4111163f5db2bc", "type": "github" }, "original": { @@ -254,15 +254,15 @@ "nixpkgs": "nixpkgs" }, "locked": { - "lastModified": 1784223297, - "narHash": "sha256-rmEX8SXvtT7Fi8hOZuCXCbpyzno3iTQYnV3WKzsAVHw=", - "owner": "lenianiva", + "lastModified": 1786543565, + "narHash": "sha256-zHMoHO85jizkIXH0OfnvabpNLTl90rR3GCc1h/e2sx4=", + "owner": "argumentcomputer", "repo": "lean4-nix", - "rev": "82993165f5f30879fc9d40734615ec54cb541e61", + "rev": "4026c657eecf16beea7d266ce32933ef3d7db2e5", "type": "github" }, "original": { - "owner": "lenianiva", + "owner": "argumentcomputer", "repo": "lean4-nix", "type": "github" } diff --git a/flake.nix b/flake.nix index ea6640914..b7487c7cf 100644 --- a/flake.nix +++ b/flake.nix @@ -15,7 +15,7 @@ nixpkgs.follows = "lean4-nix/nixpkgs"; # Lean 4 & Lake - lean4-nix.url = "github:lenianiva/lean4-nix"; + lean4-nix.url = "github:argumentcomputer/lean4-nix"; # Helper: flake-parts for easier outputs flake-parts.url = "github:hercules-ci/flake-parts"; @@ -48,7 +48,6 @@ outputs = inputs@{ - nixpkgs, flake-parts, lean4-nix, fenix, @@ -74,6 +73,9 @@ ... }: let + # Pins the Lean toolchain; a plain derivation, no overlay involved + lean = lean4-nix.lib.${system}.fromToolchainFile ./lean-toolchain; + # Pins the Rust toolchain rustToolchain = fenix.packages.${system}.fromToolchainFile { file = ./rust-toolchain.toml; @@ -90,7 +92,7 @@ strictDeps = true; # build.rs uses LEAN_SYSROOT to locate lean/lean.h for bindgen - LEAN_SYSROOT = "${pkgs.lean.lean-all}"; + LEAN_SYSROOT = "${lean}"; # bindgen needs libclang to parse C headers LIBCLANG_PATH = "${pkgs.llvmPackages.libclang.lib}/lib"; @@ -149,7 +151,7 @@ ); # Lake package - lake2nix = pkgs.callPackage lean4-nix.lake { }; + lake2nix = pkgs.callPackage lean4-nix.lake { inherit lean; }; # Restrict the Lake build inputs to Lean-relevant files so edits to # unrelated files (flake.nix, CI, docs) don't invalidate the whole # Lean build. The Rust side gets the same via cleanCargoSource. @@ -199,7 +201,7 @@ ''; buildInputs = [ pkgs.gmp - pkgs.lean.lean-all + lean pkgs.rsync ]; }; @@ -233,7 +235,7 @@ for f in ${drv}/bin/*; do [ -x "$f" ] || continue makeWrapper "$f" "$out/bin/$(basename "$f")" \ - --set LEAN_SYSROOT "${pkgs.lean.lean-all}" \ + --set LEAN_SYSROOT "${lean}" \ --set LEAN_PATH "${drv}/.lake/build/lib/lean:${leanPath}" done ''; @@ -270,12 +272,6 @@ ); in { - # Lean overlay - _module.args.pkgs = import nixpkgs { - inherit system; - overlays = [ (lean4-nix.readToolchainFile ./lean-toolchain) ]; - }; - packages = { default = ixLib; ix = ixCLI; @@ -324,7 +320,7 @@ clang rustToolchain rust-analyzer - lean.lean-all + lean cargo-deny valgrind ]; From 9d7fefbf41efd7df316d515742e23db10a185fd5 Mon Sep 17 00:00:00 2001 From: samuelburnham <45365069+samuelburnham@users.noreply.github.com> Date: Wed, 12 Aug 2026 14:58:52 -0400 Subject: [PATCH 5/9] chore: Move from alejandra to nixfmt Formatting-only, plus the formatter declaration itself; nixfmt-tree wraps nixfmt so `nix fmt .` can still take a directory. --- flake.nix | 7 ++++--- 1 file changed, 4 insertions(+), 3 deletions(-) diff --git a/flake.nix b/flake.nix index b7487c7cf..526a535bf 100644 --- a/flake.nix +++ b/flake.nix @@ -144,8 +144,7 @@ // { inherit cargoArtifacts; cargoExtraArgs = - "--locked --features parallel" - + pkgs.lib.optionalString (!pkgs.stdenv.isDarwin) ",net"; + "--locked --features parallel" + pkgs.lib.optionalString (!pkgs.stdenv.isDarwin) ",net"; doCheck = false; } ); @@ -352,7 +351,9 @@ # ]; # }; - formatter = pkgs.alejandra; + # The treefmt wrapper around `nixfmt`, so `nix fmt .` can take a + # directory; bare `nixfmt` only accepts individual files. + formatter = pkgs.nixfmt-tree; }; }; } From 42b2cdf1b42a36d43e609ba91fae53ed5fcd8381 Mon Sep 17 00:00:00 2001 From: samuelburnham <45365069+samuelburnham@users.noreply.github.com> Date: Wed, 12 Aug 2026 16:04:20 -0400 Subject: [PATCH 6/9] fix(tc): classify Prop up to universe normalization MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Lean v4.33.0 fixed two kernel soundness bugs (leanprover/lean4#14613, leanprover/lean4#14615) where a sort spelled e.g. `Sort (imax 1 0)` was not recognized as `Prop` because the zero test was syntactic; a non-proof field could then be projected out of a proof, and the inductive checker could misclassify Prop-only elimination and K-like reduction. Both ix kernels had the same syntactic test. `KUniv.isSemanticZero` / `KUniv::is_semantic_zero` decide `u ≡ 0` through the existing Géran normal form (zero normalizes to empty entries only, and norm-level equality already ignores empty entries), and replace the syntactic test at the four affected sites, in lockstep across both kernels: - proof-irrelevance Prop classification (Tc/DefEq, kernel/def_eq) - the struct-eta H3 Prop-major guard (Tc/Whnf, kernel/whnf) - the A4 field-universe Prop exemption (Tc/Inductive, kernel/inductive) - recursor-generation isProp/isLarge (AuxGen/Recursor; compile-side, Lean only) The IxVM kernel model retains the syntactic test and needs the same treatment separately. --- Ix/AuxGen/Recursor.lean | 4 ++-- Ix/Tc/DefEq.lean | 2 +- Ix/Tc/Inductive.lean | 2 +- Ix/Tc/Level.lean | 8 ++++++++ Ix/Tc/Whnf.lean | 2 +- crates/kernel/src/def_eq.rs | 2 +- crates/kernel/src/inductive.rs | 2 +- crates/kernel/src/level.rs | 12 ++++++++++++ crates/kernel/src/whnf.rs | 3 ++- 9 files changed, 29 insertions(+), 8 deletions(-) diff --git a/Ix/AuxGen/Recursor.lean b/Ix/AuxGen/Recursor.lean index 010a71a32..a6587bbcf 100644 --- a/Ix/AuxGen/Recursor.lean +++ b/Ix/AuxGen/Recursor.lean @@ -1619,10 +1619,10 @@ def computeIsLargeAndK (classes : Array FlatInfo) (nClasses nParams : Nat) {classes[0]!.ind.cnst.name.pretty}: {e}") -- Spec-level override: non-Prop inductives always get large elimination. - let isLarge := if !isLarge && !resultKuniv.isZero then true else isLarge + let isLarge := if !isLarge && !resultKuniv.isSemanticZero then true else isLarge -- Prop determination from the WHNF-reduced kernel-derived level. - let isProp := resultKuniv.isZero + let isProp := resultKuniv.isSemanticZero -- C1 fix: Prop block with nested auxiliaries the KEnv didn't see → -- small elimination (Lean treats nested auxes as full mutual members). diff --git a/Ix/Tc/DefEq.lean b/Ix/Tc/DefEq.lean index 196baf93a..9be4d1999 100644 --- a/Ix/Tc/DefEq.lean +++ b/Ix/Tc/DefEq.lean @@ -814,7 +814,7 @@ def classifyPropTypeUncached (ty : KExpr m) : RecM m Bool := do | none => pure false | some sort => match (← try? (whnf sort)) with - | some (.sort u _) => pure u.isZero + | some (.sort u _) => pure u.isSemanticZero | _ => pure false /-- Is `ty : Sort 0`? Memoized on `(tyAddr, ctxAddr)`; inner-chain errors diff --git a/Ix/Tc/Inductive.lean b/Ix/Tc/Inductive.lean index dd5efd2de..c9f251f64 100644 --- a/Ix/Tc/Inductive.lean +++ b/Ix/Tc/Inductive.lean @@ -682,7 +682,7 @@ def checkNestedCtorFieldsLoopFuel : are exempt). -/ def checkFieldUniverses (ctorTy : KExpr m) (nParams : Nat) (indLevel : KUniv m) : RecM m Unit := do - if indLevel.isZero then + if indLevel.isSemanticZero then return () let saved := (← get).lctx.size let mut ty := ctorTy diff --git a/Ix/Tc/Level.lean b/Ix/Tc/Level.lean index b99735d03..ad6192b35 100644 --- a/Ix/Tc/Level.lean +++ b/Ix/Tc/Level.lean @@ -497,6 +497,14 @@ def univGeq (u v : KUniv m) : Bool := u == v || v.isZero || Level.normLevelLe (Level.normalizeLevel v) (Level.normalizeLevel u) +/-- Semantic Prop test: `u ≡ 0` under every parameter assignment. The + syntactic `KUniv.isZero` misses spellings like `imax 1 0`, which the + kernel must classify as `Prop` (leanprover/lean4#14613, #14615). Zero + normalizes to empty entries only and `normLevelEq` ignores empty + entries, so all-empty is exactly `univEq u zero`. -/ +def KUniv.isSemanticZero (u : KUniv m) : Bool := + u.isZero || (Level.normalizeLevel u).toList.all (!Level.entryNonEmpty ·) + end Ix.Tc end diff --git a/Ix/Tc/Whnf.lean b/Ix/Tc/Whnf.lean index 7b12c0ddf..56d425e97 100644 --- a/Ix/Tc/Whnf.lean +++ b/Ix/Tc/Whnf.lean @@ -1133,7 +1133,7 @@ def finishStructEtaResult (indId : KId m) (major rhs : KExpr m) this test pure makes the semantic boundary independently inspectable without moving any checker effects across it. -/ def structEtaSortRejected : KExpr m → Bool - | .sort u _ => u.isZero + | .sort u _ => u.isSemanticZero | _ => false /-- Apply the H3 Prop guard and, for an admissible major sort, instantiate diff --git a/crates/kernel/src/def_eq.rs b/crates/kernel/src/def_eq.rs index 3eea05073..bfbd0d1f4 100644 --- a/crates/kernel/src/def_eq.rs +++ b/crates/kernel/src/def_eq.rs @@ -875,7 +875,7 @@ impl TypeChecker<'_, M> { let result = match self.with_infer_only(|tc| tc.infer(ty)) { Ok(sort) => match self.whnf(&sort) { Ok(reduced) => match reduced.data() { - ExprData::Sort(u, _) => u.is_zero(), + ExprData::Sort(u, _) => u.is_semantic_zero(), _ => false, }, Err(_) => false, diff --git a/crates/kernel/src/inductive.rs b/crates/kernel/src/inductive.rs index 2d5e25fc9..7ac3168b5 100644 --- a/crates/kernel/src/inductive.rs +++ b/crates/kernel/src/inductive.rs @@ -2424,7 +2424,7 @@ peers={} flat={} rec_ids={} failed_gi={failed_gi}", ind_level: &KUniv, ) -> Result<(), TcError> { // Skip if inductive is Prop (Sort 0) — any universe is allowed - if ind_level.is_zero() { + if ind_level.is_semantic_zero() { return Ok(()); } diff --git a/crates/kernel/src/level.rs b/crates/kernel/src/level.rs index 3e4267432..d90d70cb7 100644 --- a/crates/kernel/src/level.rs +++ b/crates/kernel/src/level.rs @@ -113,6 +113,18 @@ impl KUniv { matches!(self.data(), UnivData::Zero(_)) } + /// Semantic Prop test: `u ≡ 0` under every parameter assignment. The + /// syntactic `is_zero` misses spellings like `imax 1 0`, which the + /// kernel must classify as `Prop` (leanprover/lean4#14613, #14615). + /// Zero normalizes to empty entries only and `norm_level_eq` ignores + /// empty entries, so all-empty is exactly `univ_eq(u, zero)`. + pub fn is_semantic_zero(&self) -> bool { + self.is_zero() + || normalize_level(self) + .values() + .all(|n| n.constant == 0 && n.var.is_empty()) + } + /// True if this level is an explicit numeral: `Succ^n(Zero)` for some n ≥ 0. pub fn is_explicit(&self) -> bool { match self.data() { diff --git a/crates/kernel/src/whnf.rs b/crates/kernel/src/whnf.rs index 57f5cd9d8..288f61c42 100644 --- a/crates/kernel/src/whnf.rs +++ b/crates/kernel/src/whnf.rs @@ -1881,7 +1881,8 @@ impl TypeChecker<'_, M> { Ok(w) => w, Err(_) => return Ok(None), }; - if matches!(major_sort_w.data(), ExprData::Sort(u, _) if u.is_zero()) { + if matches!(major_sort_w.data(), ExprData::Sort(u, _) if u.is_semantic_zero()) + { return Ok(None); } let rec_us_vec: Vec<_> = rec_us.to_vec(); From f17a757b2373de7b0cb2687e3136fa882fa9b814 Mon Sep 17 00:00:00 2001 From: samuelburnham <45365069+samuelburnham@users.noreply.github.com> Date: Wed, 12 Aug 2026 16:12:30 -0400 Subject: [PATCH 7/9] fix: Adapt to Lean/batteries v4.33 API changes Fallout of the v4.29 -> v4.33 bump that the skipped updater validation never surfaced: - batteries retired the `Batteries.Data.RBMap` umbrella module and moved the type to `RBTree.RBMap` in `Batteries.Recycling.RBTree`; ix keeps the recycled structure (the Verify layer proves theorems about it) rather than migrating `NormLevel`/`CNorm` to `Std.TreeMap`. - Two `groups`/`atoms` lookups in IxonUniv were RBMap sites caught in the earlier `Std.HashMap` `find?` -> `get?` rename; RBMap kept `find?`. - `do match` arms are non-dependent since v4.32 (leanprover/lean4#13305); the ShardMap size-invariant proofs need `match (dependent := true)`. - `Environment.addDeclCore` gained a `maxRecDepth` parameter (leanprover/lean4#13956); pass Lean's default. - The Canonicity alias fixtures need `@[expose]` under the module system's cross-module compilation-type check. --- Ix/Commit.lean | 3 +- Ix/IxonUniv.lean | 12 +++---- Ix/ShardMap.lean | 4 ++- Ix/Tc/Level.lean | 4 +-- Ix/Tc/Verify/Level.lean | 62 ++++++++++++++++---------------- Tests/Ix/Compile/Canonicity.lean | 7 ++-- 6 files changed, 49 insertions(+), 43 deletions(-) diff --git a/Ix/Commit.lean b/Ix/Commit.lean index bbd3ca533..fcb170a3d 100644 --- a/Ix/Commit.lean +++ b/Ix/Commit.lean @@ -143,7 +143,8 @@ def commitDef (compileEnv : CompileM.CompileEnv) (leanEnv : Lean.Environment) safety := .safe } let decl := Lean.Declaration.defnDecl defnVal - let leanEnv' ← match Lean.Environment.addDeclCore leanEnv 0 decl .none with + let leanEnv' ← match Lean.Environment.addDeclCore leanEnv 0 + Lean.defaultMaxRecDepth.toUSize decl .none with | .ok env => pure env | .error _e => throw $ IO.userError "commitDef: addDeclCore failed" diff --git a/Ix/IxonUniv.lean b/Ix/IxonUniv.lean index 192bb3824..922372c41 100644 --- a/Ix/IxonUniv.lean +++ b/Ix/IxonUniv.lean @@ -1,7 +1,7 @@ module public import Ix.Ixon -public import Batteries.Data.RBMap +public import Batteries.Recycling.RBTree.Basic /-! Universe-level canonicalization (canonicity §10.6). @@ -152,7 +152,7 @@ def CNode.isEmpty (n : CNode) : Bool := n.constant == 0 && n.vars.isEmpty /-- Canonical form: map from imax-paths to nodes (lexicographic). -/ -abbrev CNorm := Batteries.RBMap CPath CNode compare +abbrev CNorm := RBTree.RBMap CPath CNode compare instance : Inhabited CNorm := ⟨.empty⟩ @@ -343,7 +343,7 @@ recovery, marker consumption, emission order). -/ /-- Context-group accumulator. -/ structure CGroup where constant : UInt64 := 0 - atoms : Batteries.RBMap UInt64 UInt64 compare := .empty + atoms : RBTree.RBMap UInt64 UInt64 compare := .empty deriving Inhabited /-- Is a `u_i = 0` fallout of `k` dominated under `ctx`? Some entry at @@ -382,7 +382,7 @@ def maxChain (terms : List Univ) : Univ := def linearize (norm : CNorm) : Univ := Id.run do let cRoot := (norm.findD [] {}).constant -- Explode into per-atom items; self-strip under domination coverage. - let mut groups : Batteries.RBMap CPath CGroup compare := .empty + let mut groups : RBTree.RBMap CPath CGroup compare := .empty for (path, node) in norm.toList do if !path.isEmpty && node.constant > 0 then let g := groups.findD path {} @@ -403,12 +403,12 @@ def linearize (norm : CNorm) : Univ := Id.run do for j in [0:order.length] do let p := order[j]! let mctx := (order.take j).mergeSort (· ≤ ·) - if (groups.get? mctx).any (fun sg => sg.atoms.get? p == some 0) then + if (groups.find? mctx).any (fun sg => sg.atoms.find? p == some 0) then consumed := (mctx, p) :: consumed -- Emission. let mut terms : List Univ := [] let mut rootCAbsorbed := false - if let some top := groups.get? [] then + if let some top := groups.find? [] then for (i, k) in top.atoms.toList do if k == 0 && consumed.contains ([], i) then continue diff --git a/Ix/ShardMap.lean b/Ix/ShardMap.lean index ef1eca264..e3e5dd5f7 100644 --- a/Ix/ShardMap.lean +++ b/Ix/ShardMap.lean @@ -80,7 +80,9 @@ private def mkShardArrayWithCapacity (n : Nat) (capacity : Nat) : BaseIO { arr : Array (PaddedShard α β) // arr.size = n } := do let rec go (remaining : Nat) (acc : Array (PaddedShard α β)) (hacc : acc.size + remaining = n) : BaseIO { arr : Array (PaddedShard α β) // arr.size = n } := do - match remaining with + -- `dependent := true`: the proof arms need `hacc` refined by the + -- scrutinee, which `do match` stopped doing by default in v4.32. + match (dependent := true) remaining with | 0 => pure ⟨acc, by omega⟩ | r + 1 => let mutex ← Std.SharedMutex.new (Std.HashMap.emptyWithCapacity capacity) diff --git a/Ix/Tc/Level.lean b/Ix/Tc/Level.lean index ad6192b35..a57d19314 100644 --- a/Ix/Tc/Level.lean +++ b/Ix/Tc/Level.lean @@ -3,7 +3,7 @@ module public import Ix.Tc.Mode public import Ix.Address public import Ix.Unsigned -public import Batteries.Data.RBMap +public import Batteries.Recycling.RBTree.Basic /-! Mirror: crates/kernel/src/level.rs @@ -265,7 +265,7 @@ abbrev Path := List UInt64 /-- Canonical form: map from imax-paths to nodes. Rust `BTreeMap, Node>`; `Ord Path` is lexicographic in both. -/ -abbrev NormLevel := Batteries.RBMap Path NormNode compare +abbrev NormLevel := RBTree.RBMap Path NormNode compare instance : Inhabited NormLevel := ⟨.empty⟩ diff --git a/Ix/Tc/Verify/Level.lean b/Ix/Tc/Verify/Level.lean index f953866f1..589a1675f 100644 --- a/Ix/Tc/Verify/Level.lean +++ b/Ix/Tc/Verify/Level.lean @@ -1,5 +1,5 @@ import Ix.Tc.Level -import Batteries.Data.RBMap.Lemmas +import Batteries.Recycling.RBTree.Lemmas import Lean4Lean.Theory.VLevel /-! @@ -307,16 +307,16 @@ theorem evalPath_max {ρ : List Nat} {path : Path} {a b : Nat} : theorem NormLevel.eval_le {ρ : List Nat} {l : NormLevel} {x : Nat} : l.eval ρ ≤ x ↔ ∀ p n, l.find? p = some n → evalPath ρ p (n.eval ρ) ≤ x := by - rw [NormLevel.eval, Batteries.RBMap.foldl_eq_foldl_toList, foldl_max_le] + rw [NormLevel.eval, RBTree.RBMap.foldl_eq_foldl_toList, foldl_max_le] simp only [Nat.zero_le, true_and] constructor · intro H p n hf - obtain ⟨y, hy, hcmp⟩ := Batteries.RBMap.find?_some_mem_toList hf + obtain ⟨y, hy, hcmp⟩ := RBTree.RBMap.find?_some_mem_toList hf cases Std.LawfulEqCmp.eq_of_compare hcmp exact H (p, n) hy · intro H pn hpn exact H pn.1 pn.2 - (Batteries.RBMap.find?_some.mpr ⟨pn.1, hpn, Std.ReflCmp.compare_self⟩) + (RBTree.RBMap.find?_some.mpr ⟨pn.1, hpn, Std.ReflCmp.compare_self⟩) theorem NormLevel.le_eval {ρ : List Nat} {l : NormLevel} {p : Path} {n : NormNode} (h : l.find? p = some n) : @@ -574,7 +574,7 @@ theorem NormNode.addVar_eval {ρ : List Nat} {n : NormNode} {idx k : UInt64} : denotation. -/ private theorem findD_evalPath_le {ρ : List Nat} {l : NormLevel} {path : Path} : evalPath ρ path ((l.findD path {}).eval ρ) ≤ l.eval ρ := by - rw [Batteries.RBMap.findD] + rw [RBTree.RBMap.findD] cases hf : l.find? path with | some n => simpa using NormLevel.le_eval hf | none => @@ -594,7 +594,7 @@ private theorem insert_findD_eval {ρ : List Nat} {l : NormLevel} {path : Path} = max (l.eval ρ) (evalPath ρ path c) := by have hfind : ∀ p, (l.insert path v').find? p = if compare p path = .eq then some v' else l.find? p := fun p => by - rw [Batteries.RBMap.find?_insert] + rw [RBTree.RBMap.find?_insert] have ext : ∀ x, (NormLevel.eval ρ (l.insert path v') ≤ x ↔ max (l.eval ρ) (evalPath ρ path c) ≤ x) := by intro x @@ -608,7 +608,7 @@ private theorem insert_findD_eval {ρ : List Nat} {l : NormLevel} {path : Path} by_cases hcmp : compare p path = .eq · cases Std.LawfulEqCmp.eq_of_compare hcmp have hD : l.findD path {} = n := by - rw [Batteries.RBMap.findD, hf, Option.getD_some] + rw [RBTree.RBMap.findD, hf, Option.getD_some] rw [← hD] exact hpath.1 · exact H p n (by rw [hfind, if_neg hcmp]; exact hf) @@ -1212,13 +1212,13 @@ theorem subsumption_eq_model (acc : NormLevel) : theorem seed_eval {ρ : List Nat} : NormLevel.eval ρ ((∅ : NormLevel).insert [] {}) = 0 := by refine Nat.le_antisymm (NormLevel.eval_le.mpr fun p n hf => ?_) (Nat.zero_le _) - rw [Batteries.RBMap.find?_insert] at hf + rw [RBTree.RBMap.find?_insert] at hf split at hf · rename_i hcmp cases Std.LawfulEqCmp.eq_of_compare hcmp cases hf simp [evalPath, allNZ, NormNode.eval] - · obtain ⟨y, hy, -⟩ := Batteries.RBMap.find?_some_mem_toList hf + · obtain ⟨y, hy, -⟩ := RBTree.RBMap.find?_some_mem_toList hf simp at hy /-! #### Canonical-form comparison soundness -/ @@ -1308,7 +1308,7 @@ theorem normLevelEq_eval {ρ : List Nat} {l₁ l₂ : NormLevel} intro p n hf by_cases hne : entryNonEmpty (p, n) = true · have hmem : (p, n) ∈ la.toList := by - obtain ⟨y, hy, hcmp⟩ := Batteries.RBMap.find?_some_mem_toList hf + obtain ⟨y, hy, hcmp⟩ := RBTree.RBMap.find?_some_mem_toList hf cases Std.LawfulEqCmp.eq_of_compare hcmp exact hy have hmem₂ : (p, n) ∈ lb.toList := by @@ -1316,7 +1316,7 @@ theorem normLevelEq_eval {ρ : List Nat} {l₁ l₂ : NormLevel} rw [← hfe] exact List.mem_filter.mpr ⟨hmem, hne⟩ exact (List.mem_filter.mp hfmem).1 - exact NormLevel.le_eval (Batteries.RBMap.find?_some.mpr + exact NormLevel.le_eval (RBTree.RBMap.find?_some.mpr ⟨p, hmem₂, Std.ReflCmp.compare_self⟩) · rw [eval_of_not_entryNonEmpty (Bool.eq_false_iff.mpr hne)] exact evalPath_le.mpr fun _ => Nat.zero_le _ @@ -1340,7 +1340,7 @@ private theorem covering_entry_le {ρ : List Nat} {l₂ : NormLevel} (hnz₂ : allNZ ρ p₂ = true) : NormNode.eval ρ n₂ ≤ NormLevel.eval ρ l₂ := by have hfind : l₂.find? p₂ = some n₂ := - Batteries.RBMap.find?_some.mpr ⟨p₂, hmem, Std.ReflCmp.compare_self⟩ + RBTree.RBMap.find?_some.mpr ⟨p₂, hmem, Std.ReflCmp.compare_self⟩ simpa [evalPath, hnz₂] using NormLevel.le_eval (ρ := ρ) hfind /-- The coverage argument (level.rs:634-643, no upstream counterpart): @@ -1352,7 +1352,7 @@ theorem normLevelLe_eval {ρ : List Nat} {l₁ l₂ : NormLevel} rw [normLevelLe, List.all_eq_true] at h rw [NormLevel.eval_le] intro p₁ n₁ hf - obtain ⟨y, hymem, hycmp⟩ := Batteries.RBMap.find?_some_mem_toList hf + obtain ⟨y, hymem, hycmp⟩ := RBTree.RBMap.find?_some_mem_toList hf cases Std.LawfulEqCmp.eq_of_compare hycmp have h1 := h (p₁, n₁) hymem simp only at h1 @@ -1393,7 +1393,7 @@ theorem normLevelLe_eval {ρ : List Nat} {l₁ l₂ : NormLevel} have hvmem : n₂.vars[i] ∈ n₂.vars := Array.getElem_mem hi have hidx : n₂.vars[i].idx ∈ p₂ := by have hfind₂ : l₂.find? p₂ = some n₂ := - Batteries.RBMap.find?_some.mpr + RBTree.RBMap.find?_some.mpr ⟨p₂, hmem₂, Std.ReflCmp.compare_self⟩ exact hwf p₂ n₂ hfind₂ _ hvmem have h1ev : 1 ≤ evalParam ρ n₂.vars[i].idx := by @@ -1483,7 +1483,7 @@ theorem VarsOnPath.addVar {l : NormLevel} {idx k : UInt64} {path : Path} (hl : VarsOnPath l) (hidx : idx ∈ path) : VarsOnPath (l.addVar idx k path) := by intro p n hf v hv - rw [NormLevel.addVar, Batteries.RBMap.find?_insert] at hf + rw [NormLevel.addVar, RBTree.RBMap.find?_insert] at hf split at hf · rename_i hcmp cases Std.LawfulEqCmp.eq_of_compare hcmp @@ -1491,7 +1491,7 @@ theorem VarsOnPath.addVar {l : NormLevel} {idx k : UInt64} {path : Path} rcases NormNode.addVar_idx_mem v hv with rfl | ⟨v', hv', heq⟩ · exact hidx · rw [heq] - rw [Batteries.RBMap.findD] at hv' + rw [RBTree.RBMap.findD] at hv' cases hff : l.find? path with | some n₀ => rw [hff, Option.getD_some] at hv' @@ -1508,12 +1508,12 @@ theorem VarsOnPath.addConst {l : NormLevel} {k : UInt64} {path : Path} simp only [NormLevel.addConst] at hf split at hf · exact hl p n hf v hv - · rw [Batteries.RBMap.find?_insert] at hf + · rw [RBTree.RBMap.find?_insert] at hf split at hf · rename_i hcmp cases Std.LawfulEqCmp.eq_of_compare hcmp cases hf - rw [Batteries.RBMap.findD] at hv + rw [RBTree.RBMap.findD] at hv cases hff : l.find? path with | some n₀ => rw [hff, Option.getD_some] at hv @@ -1642,11 +1642,11 @@ end private theorem varsOnPath_seed : VarsOnPath ((∅ : NormLevel).insert [] ({} : NormNode)) := by intro p n hf v hv - rw [Batteries.RBMap.find?_insert] at hf + rw [RBTree.RBMap.find?_insert] at hf split at hf · cases hf simp at hv - · obtain ⟨y, hy, -⟩ := Batteries.RBMap.find?_some_mem_toList hf + · obtain ⟨y, hy, -⟩ := RBTree.RBMap.find?_some_mem_toList hf simp at hy /-- `subsumeVars` only filters: every survivor comes from the first @@ -1766,7 +1766,7 @@ private theorem VarsOnPath.insert_of_subset {res : NormLevel} {p1 : Path} (h0 : ∀ v ∈ n0.vars, v.idx ∈ p1) : VarsOnPath (res.insert p1 nf) := by intro p n hf v hv - rw [Batteries.RBMap.find?_insert] at hf + rw [RBTree.RBMap.find?_insert] at hf split at hf · rename_i hcmp cases Std.LawfulEqCmp.eq_of_compare hcmp @@ -1804,7 +1804,7 @@ theorem varsOnPath_subsumption {l : NormLevel} (hl : VarsOnPath l) : · exact hcur v hv · intro v hv have hf1 : l.find? p1 = some n1₀ := - Batteries.RBMap.find?_some.mpr ⟨p1, hmem, Std.ReflCmp.compare_self⟩ + RBTree.RBMap.find?_some.mpr ⟨p1, hmem, Std.ReflCmp.compare_self⟩ exact hl p1 n1₀ hf1 v hv /-! #### Subsumption: the `≤` half and the per-key characterization -/ @@ -1871,7 +1871,7 @@ private theorem processEntry_eval_le {ρ : List Nat} {p1 : Path} : /-- Keys of an `RBMap`'s `toList` are nodup (strict sortedness). -/ private theorem toList_keys_nodup (l : NormLevel) : (l.toList.map Prod.fst).Nodup := by - refine List.Pairwise.map _ ?_ Batteries.RBMap.toList_sorted + refine List.Pairwise.map _ ?_ RBTree.RBMap.toList_sorted intro a b hlt heq have hc := Batteries.RBNode.cmpLT_iff.mp hlt rw [heq] at hc @@ -1890,7 +1890,7 @@ private theorem foldl_insert_find?_of_not_mem | pn :: rest, res, p, h => by rw [List.foldl_cons, foldl_insert_find?_of_not_mem f rest _ p fun q hq => h q (List.mem_cons_of_mem _ hq)] - refine Batteries.RBMap.find?_insert_of_ne _ fun hcmp => ?_ + refine RBTree.RBMap.find?_insert_of_ne _ fun hcmp => ?_ exact h pn (List.mem_cons_self ..) (Std.LawfulEqCmp.eq_of_compare hcmp) /-- With nodup keys, the fold writes each entry exactly once. -/ @@ -1907,7 +1907,7 @@ private theorem foldl_insert_find?_self rcases List.mem_cons.mp hmem with rfl | hmem' · rw [foldl_insert_find?_of_not_mem f rest _ p fun q hq heq => hnd.1 (heq ▸ List.mem_map.mpr ⟨q, hq, rfl⟩)] - exact Batteries.RBMap.find?_insert_of_eq _ Std.ReflCmp.compare_self + exact RBTree.RBMap.find?_insert_of_eq _ Std.ReflCmp.compare_self · exact foldl_insert_find?_self f rest _ p n hmem' hnd.2 /-- Forward characterization: every entry of the model comes from an @@ -1917,7 +1917,7 @@ private theorem subsumptionModel_find?_some {l : NormLevel} {p : Path} ∃ n₀, l.find? p = some n₀ ∧ n = processEntry l.toList p n₀ := by cases hf₀ : l.find? p with | some n₀ => - obtain ⟨y, hy, hycmp⟩ := Batteries.RBMap.find?_some_mem_toList hf₀ + obtain ⟨y, hy, hycmp⟩ := RBTree.RBMap.find?_some_mem_toList hf₀ cases Std.LawfulEqCmp.eq_of_compare hycmp refine ⟨n₀, rfl, ?_⟩ rw [subsumptionModel, @@ -1927,7 +1927,7 @@ private theorem subsumptionModel_find?_some {l : NormLevel} {p : Path} | none => rw [subsumptionModel, foldl_insert_find?_of_not_mem _ l.toList l p (fun pn hpn heq => by - rw [heq, Batteries.RBMap.find?_some.mpr + rw [heq, RBTree.RBMap.find?_some.mpr ⟨pn.1, hpn, Std.ReflCmp.compare_self⟩] at hf₀ simp at hf₀), hf₀] at hf @@ -2215,14 +2215,14 @@ private theorem le_subsumptionModel_eval {ρ : List Nat} {l : NormLevel} intro p1 n1₀ hf hlen hnz v hv rcases processEntry_var_cases l.toList n1₀ v hv with hsurv | ⟨pn, hpn, hsub, hsame, y, hy, hidx, hoff⟩ - · obtain ⟨yy, hyy, hyycmp⟩ := Batteries.RBMap.find?_some_mem_toList hf + · obtain ⟨yy, hyy, hyycmp⟩ := RBTree.RBMap.find?_some_mem_toList hf cases Std.LawfulEqCmp.eq_of_compare hyycmp have hfm := subsumptionModel_find?_of_mem hyy refine Nat.le_trans (((NormNode.eval_le (ρ := ρ)).mp (Nat.le_refl _)).2 v hsurv) ?_ simpa [evalPath, hnz] using NormLevel.le_eval (ρ := ρ) hfm · have hf₂ : l.find? pn.1 = some pn.2 := - Batteries.RBMap.find?_some.mpr + RBTree.RBMap.find?_some.mpr ⟨pn.1, hpn, Std.ReflCmp.compare_self⟩ have hnz₂ : allNZ ρ pn.1 = true := allNZ_of_isSubset hsub hnz have hlt : pn.1.length < p1.length := by @@ -2248,7 +2248,7 @@ private theorem le_subsumptionModel_eval {ρ : List Nat} {l : NormLevel} intro p1 n1₀ hf hlen hnz rcases processEntry_const_cases l.toList n1₀ with hkeep | ⟨pn, hpn, hsub, m, hmc, hmv, hexp⟩ - · obtain ⟨yy, hyy, hyycmp⟩ := Batteries.RBMap.find?_some_mem_toList hf + · obtain ⟨yy, hyy, hyycmp⟩ := RBTree.RBMap.find?_some_mem_toList hf cases Std.LawfulEqCmp.eq_of_compare hyycmp have hfm := subsumptionModel_find?_of_mem hyy have hb : NormNode.eval ρ (processEntry l.toList p1 n1₀) @@ -2258,7 +2258,7 @@ private theorem le_subsumptionModel_eval {ρ : List Nat} {l : NormLevel} rw [← hkeep] exact ((NormNode.eval_le (ρ := ρ)).mp (Nat.le_refl _)).1 · have hf₂ : l.find? pn.1 = some pn.2 := - Batteries.RBMap.find?_some.mpr + RBTree.RBMap.find?_some.mpr ⟨pn.1, hpn, Std.ReflCmp.compare_self⟩ have hnz₂ : allNZ ρ pn.1 = true := allNZ_of_isSubset hsub hnz rw [Bool.and_eq_false_iff] at hexp diff --git a/Tests/Ix/Compile/Canonicity.lean b/Tests/Ix/Compile/Canonicity.lean index f3653ac10..3cf2a4fb4 100644 --- a/Tests/Ix/Compile/Canonicity.lean +++ b/Tests/Ix/Compile/Canonicity.lean @@ -625,8 +625,11 @@ namespace AliasProvenance universe u -public def WrapA (V : Type u) : Type u := V -public def WrapB (V : Type u) : Type u := V +-- `@[expose]`: the inductives below take these as (reducible) index +-- types; without exposed bodies the compiler infers a different +-- compilation type locally than importers would and refuses to compile. +@[expose] public def WrapA (V : Type u) : Type u := V +@[expose] public def WrapB (V : Type u) : Type u := V public abbrev RelOn (C : Type u) : Type u := C → C → Prop From 60102c45ea336d30a10d514499d90b6762fa4311 Mon Sep 17 00:00:00 2001 From: samuelburnham <45365069+samuelburnham@users.noreply.github.com> Date: Wed, 12 Aug 2026 16:18:07 -0400 Subject: [PATCH 8/9] fix(ffi): decode Lean.Int by value, not as a constructor MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit `Lean.Int` is in the compiler's `builtinRuntimeTypes`, so at runtime it shares `Nat`'s representation — a tagged scalar or a GMP mpz object; `Int.ofNat` compiles to the identity `lean_nat_to_int` and no ctor cell ever exists. The mdata `DataValue.ofInt` decode path nevertheless read it through the `LeanIxInt` ctor layout, dereferencing a tagged scalar (or reading mpz limbs as ctor fields) whenever an `Expr.mdata` KVMap carried an integer. Decode by value instead: arithmetic-shift the tagged scalar to recover the signed payload, and for mpz objects take the sign from `lean_int_dec_lt` and the magnitude from `lean_nat_abs`. `LeanIxInt` remains in use for `Ix.Int`, a genuine two-ctor inductive. Pre-existing bug surfaced by the v4.33 FFI layout audit, which found no other divergence between the hardcoded layouts and Lean v4.33.0. --- crates/ffi/src/lean_env.rs | 49 +++++++++++++++++++++++++++++--------- 1 file changed, 38 insertions(+), 11 deletions(-) diff --git a/crates/ffi/src/lean_env.rs b/crates/ffi/src/lean_env.rs index 021bd1375..477ffca3e 100644 --- a/crates/ffi/src/lean_env.rs +++ b/crates/ffi/src/lean_env.rs @@ -24,16 +24,16 @@ use std::sync::Arc; use lean_ffi::nat::Nat; use lean_ffi::object::LeanNat; use lean_ffi::object::{ - LeanArray, LeanBorrowed, LeanList, LeanRef, LeanShared, + LeanArray, LeanBorrowed, LeanList, LeanOwned, LeanRef, LeanShared, }; use crate::lean::{ LeanIxAxiomVal, LeanIxConstantInfo, LeanIxConstantVal, LeanIxConstructorVal, LeanIxDataValue, LeanIxDefinitionVal, LeanIxExpr, LeanIxInductiveVal, - LeanIxInt, LeanIxLevel, LeanIxLiteral, LeanIxName, LeanIxOpaqueVal, - LeanIxQuotVal, LeanIxRecursorRule, LeanIxRecursorVal, - LeanIxReducibilityHints, LeanIxSourceInfo, LeanIxSubstring, LeanIxSyntax, - LeanIxSyntaxPreresolved, LeanIxTheoremVal, + LeanIxLevel, LeanIxLiteral, LeanIxName, LeanIxOpaqueVal, LeanIxQuotVal, + LeanIxRecursorRule, LeanIxRecursorVal, LeanIxReducibilityHints, + LeanIxSourceInfo, LeanIxSubstring, LeanIxSyntax, LeanIxSyntaxPreresolved, + LeanIxTheoremVal, }; use ix_common::env::{ @@ -824,12 +824,39 @@ fn decode_name_data_value( 2 => DataValue::OfName(decode_name(dv.get_obj(0), cache.global)), 3 => DataValue::OfNat(LeanNat::to_nat(&dv.get_obj(0))), 4 => { - let i = LeanIxInt::from_ctor(dv.get_obj(0).as_ctor()); - let nat = LeanNat::to_nat(&i.get_obj(0)); - let int = match i.as_ctor().tag() { - 0 => Int::OfNat(nat), - 1 => Int::NegSucc(nat), - tag => unreachable!("Invalid Lean.Int tag: {tag}"), + // `Lean.Int` is a builtin runtime type sharing `Nat`'s + // representation — a tagged scalar or a GMP mpz object, never an + // `ofNat`/`negSucc` ctor cell (`Int.ofNat` compiles to the + // identity `lean_nat_to_int`). Decode by value and rebuild the + // ctor view; `LeanIxInt` describes only the `Ix.Int` mirror + // inductive, which really is a two-ctor object. + let iobj = dv.get_obj(0); + let int = if iobj.is_scalar() { + // Scalars box `v` as `(v << 1) | 1`; an arithmetic shift + // recovers the signed value. + let v = (iobj.as_raw() as isize) >> 1; + if v >= 0 { + Int::OfNat(Nat::from(v as u64)) + } else { + Int::NegSucc(Nat::from((-(v + 1)) as u64)) + } + } else { + let neg = unsafe { + lean_ffi::include::lean_int_dec_lt( + iobj.as_raw(), + lean_ffi::include::lean_box(0), + ) + } != 0; + let abs = unsafe { + LeanOwned::from_raw(lean_ffi::include::lean_nat_abs(iobj.as_raw())) + }; + let mag = LeanNat::to_nat(&abs); + if neg { + // negSucc n = -(n + 1), so n = |v| - 1 (|v| ≥ 1 here). + Int::NegSucc(Nat(mag.0 - 1u32)) + } else { + Int::OfNat(mag) + } }; DataValue::OfInt(int) }, From 001b1c9837d81b56ddc056367a0bfb5788c9ca35 Mon Sep 17 00:00:00 2001 From: samuelburnham <45365069+samuelburnham@users.noreply.github.com> Date: Wed, 12 Aug 2026 17:29:34 -0400 Subject: [PATCH 9/9] docs: Add v4.33 bump handoff Records the lean4lean integration steps and their verification queue, the open kernel-semantics divergences from upstream (theorem opacity, the IxVM syntactic zero test, the deliberately-unenforced mutual universe uniformity, missing regression fixtures), the divergences considered and cleared during the audit, and the non-blocking follow-ups (FFI pointer liveness, benchmark re-baselining, thread-pool stack ordering, OpenSSL link watch, setup-file JSON parsing). --- HANDOFF.md | 213 +++++++++++++++++++++++++++++++++++++++++++++++++++++ 1 file changed, 213 insertions(+) create mode 100644 HANDOFF.md diff --git a/HANDOFF.md b/HANDOFF.md new file mode 100644 index 000000000..3bdecf3a6 --- /dev/null +++ b/HANDOFF.md @@ -0,0 +1,213 @@ +# Handoff: Lean v4.33.0 bump — remaining integration work + +Status of this branch (`update/lean-v4.33.0`): ix is adapted to Lean v4.33.0 +and verified as far as is possible without lean4lean. `lake build Ix` is +green, `cargo check --workspace` is clean, the Rust kernel's 674 tests pass, +and every ix-side test target compiles. The one dependency blocker is the +`lean4lean` pin (v4.31-era, does not compile under v4.33); the test suite and +lint gate execute lean4lean-linked binaries and are queued behind it. + +This file records everything still open from the v4.29 → v4.33 release-notes +audit: the lean4lean integration steps, kernel-semantics divergences between +ix's checkers and the upstream Lean kernel (open and cleared), and +non-blocking follow-ups. Ingest fully before starting integration. + +## 1. lean4lean: why the bump matters + +The pinned lean4lean (`5e5bb767`, in `lakefile.lean`) reproduces the kernel +soundness bug fixed upstream in Lean v4.32.1 (leanprover/lean4#14498): its +`addOpaque` (`Lean4Lean/Environment.lean:64-72` at the pinned rev) never +calls `checkNoMVarNoFVar` on the opaque's *value*, so it accepts the +axiom-free `False` construction from leanprover/lean4#14484. Reachable from +ix via `Benchmarks/Lean4Lean.lean:209` (`.opaqueInfo → addDeclAt`). + +Upstream `digama0/lean4lean` master has the complete v4.32/v4.33 hardening: +`779c51fde` (the #14498 value check + `Tests/DeclFVar.lean`), `d7e70a5f0` +(nested-inductive phantom params, #14577), `5518bf838` (mutual `levelParams` +uniformity #14608, reserved `_nested` prefix #14616, `checkNoMVarNoFVar` on +inductive/ctor types #14607, + `Tests/KernelHardening.lean`), and the +verified level-normalization algorithm enabled in the typechecker. + +The fork update is being done as `argumentcomputer/lean4lean` PR #4 +(`jcb/formalization2`) — formalization on top of latest upstream. Do not +integrate an intermediate state; wait for it to land on the fork's dev. + +## 2. Integration steps once lean4lean lands + +1. **Bump the pin.** In `lakefile.lean`, set the `lean4lean` rev to the new + dev tip; `lake update lean4lean`. Confirm its `lean-toolchain` is stable + `leanprover/lean4:v4.33.0` (upstream tracks rc toolchains). + +2. **Run the suite**: `lake test`. First actual execution on v4.33. + Watch-points from the audit: + - `Tests/FFI/Refcount.lean` — v4.30's borrow-inference overhaul + (leanprover/lean4#12830, #13136 RC coalescing) may shift caller-side + inc/dec counts. Diagnose with `trace.Compiler.inferBorrow` before + adjusting expectations. + - `Tests/Ix/Kernel/CheckEnv.lean:191-192` pins private `Std.Time` names + (`Std.Time.PlainTime.format._sparseCasesOn_1`); `Std.Time` was + refactored in v4.32 and the fixtures may not resolve. + - Decompile roundtrip — v4.30 #12987 introduced `foo._f` helper + constants for structural recursion. `classifyAuxGen` + (`Ix/CallSiteSurgery.lean`) deliberately routes unknown suffixes to the + plain-definition path and ix's own v4.33 oleans contain no `._f`, but + dependency environments may carry them; the roundtrip suite confirms. + - `Ix/Tc/Primitive.lean:221-222` hard-codes canonical addresses for + `PUnit._sizeOf_1` and `SizeOf.sizeOf`; v4.31 #13320 un-exposed + auto-generated `sizeOf` definitions, which can invalidate those hashes. + - Expect broad content-address churn vs v4.29-era artifacts and + re-baseline rather than debug: derived Prop instances flipped + `def`→`theorem` (v4.31 #13304), imported `partial` defs regain their + marking across module boundaries (v4.33 #14609), `Float`/`Float32` + were redefined around `Float.Model`, derived `BEq`/`Inhabited` bodies + changed, and several core decls changed exposure/reducibility. All + `.ixe` fixtures and pinned address tables from v4.29 will differ. + +3. **Run the lint gate**: `lake lint -- --wfail -v`. Not yet run on v4.33; + v4.31 enabled `linter.redundantVisibility` (ix: ~174 files with `public + section` + explicit `public`, ~800 `private` decls), + `linter.redundantExpose` (`Ix/Lib.lean:11`), and + `warning.simp.varHead`/`otherHead` (~257 `@[simp]`s). Escape hatch: + `leanOptions := #[⟨`linter.redundantVisibility, false⟩]`; prefer fixing + genuinely redundant modifiers. + +4. **Limits, only if they fire.** v4.31 #13030 made heartbeats accumulate + faster (upstream raised limits 20–50% in places); v4.33 #13956 bounded + kernel recursion by `maxRecDepth` instead of the physical stack. If + `IxTcVerify` or deep replays hit deterministic timeouts or + `(kernel) deep recursion`, raise the seven + `set_option maxHeartbeats 800000` sites under `Ix/Tc/Verify/` and add + `maxRecDepth` options before chasing phantom regressions. + +## 3. Kernel-semantics divergences vs upstream v4.33 — OPEN + +These are places where ix's checkers (Ix/Tc reference kernel, Rust +`crates/kernel`, IxVM model) knowingly differ from the upstream C++ kernel +after this branch. Each needs a decision or work; none is a known +unsoundness. + +- **Theorem delta-unfolding (v4.30 #12973).** Upstream made theorem bodies + kernel-opaque "in almost all ways"; ix still unfolds `.thm` like `.defn` + (`Ix/Tc/Whnf.lean:404,421`; IxVM `Ix/IxVM/Kernel/DefEq.lean:1002`, + `Whnf.lean:486,775`). Sound (theorem bodies are well-typed) but strictly + more permissive: ix can certify proofs Lean's kernel rejects. Do NOT gate + blindly — the kernel still unfolds theorems in iota-major position (see + the comment near `Ix/IxVM/Kernel/Whnf.lean:755` citing + `Rat.instEncodable._proof_1`), so a blanket gate rejects real mathlib. + The updated lean4lean is the executable spec for exactly where theorem + unfolding is allowed: replay a corpus (ix's env, then the + `Benchmarks/Compile` mathlib/FLT environments) through both checkers, + diff acceptance, then port lean4lean's exact rule into `Ix/Tc/Whnf.lean`, + the Rust kernel, and IxVM together, with a regression fixture. + +- **IxVM still uses the syntactic universe-zero test.** The Lean and Rust + kernels were fixed on this branch to classify Prop up to normalization + (`KUniv.isSemanticZero` / `is_semantic_zero`; see commit `fix(tc): + classify Prop up to universe normalization`, mirroring + leanprover/lean4#14613/#14615 — `Sort (imax 1 0)` is `Prop`). The IxVM + model retains the literal-`Zero` test (`Ix/IxVM/Kernel/DefEq.lean:647-669` + documents the old three-kernel lockstep, now stale). Until ported, IxVM + diverges from the other two ix kernels AND from upstream: proof + irrelevance, struct-eta's Prop guard, and Prop-elimination classification + can disagree on normalizable-zero universes. Port `isSemanticZero` into + the IxVM model and its fixtures as a dedicated change, and update the + lockstep comment. + +- **Mutual-block universe uniformity (v4.33 #14608) — deliberately not + enforced.** Upstream's kernel now requires identical `levelParams` across + a mutual block (only reachable via metaprogramming, only + `partial`/`unsafe`). ix checks members compositionally (cross-references + arity-checked at infer; per-member `lvls` in the `muts` form) and its own + block clustering may legitimately group members Lean never required to be + uniform — enforcing uniformity could reject valid content. Consequence: + ix accepts (metaprogrammed, unsafe) blocks upstream rejects. Revisit only + if lean4lean-parity replays surface a real case; otherwise this stands as + a documented, justified divergence. + +- **Regression-fixture ports.** ix has no fixtures for the v4.32/v4.33 + soundness-bug shapes. Port upstream's repros as Ix/Tc test fixtures: + `issue14484.lean` (opaque fvar; ix ingress rejects fvars/mvars at + `Ix/CompileM.lean:777` — the fixture pins that), `issue_14576_min.lean` + (nested phantom params; see cleared item below), and a + `Sort (imax 1 0)` Prop-classification case exercising `isSemanticZero` + end-to-end (the Rust unit tests cover `univ_eq`; an integration-level + fixture does not exist yet). + +## 4. Kernel-semantics divergences — CONSIDERED AND CLEARED + +Verified during this branch's audit; recorded so they are not re-derived. + +- **Nested-inductive phantom params (#14577/#14607): not vulnerable.** + Upstream's bug was checking ctor types only *after* nested elimination + (dropped `Ds` escaped checking). ix fully infers the declared ctor type + in its original nested form (`Ix/Tc/Check.lean:441`) before the + positivity walk (`Ix/Tc/Inductive.lean:585-624`), so the params are + checked as ordinary subterms; ix's aux expansion is ephemeral and + compile-side. The exploit's `Expr`-hash/approxDepth collision vector does + not map to Blake3 content addressing. + +- **Universe-arity at delta (v4.30 #12817): already defended.** Both + kernels check const arity at infer (`Ix/Tc/Infer.lean:63`, + `crates/kernel/src/infer.rs:99`) and error — never default — on + out-of-range substitution (`substUniv`, `tc.rs` `subst_univ`). The + egress-side `getD mkAnon` (`Ix/Tc/EgressLean.lean:63`) is display + metadata; Lean re-checks anything re-added. + +- **`_nested` reserved prefix (v4.33 #14616): no collision.** ix's + `._nested.` auxiliaries (`Ix/AuxGen/Nested.lean`) are ephemeral — never + persisted, never re-added to a Lean environment; the commit path + (`Ix/Commit.lean`) adds commitment-address names. Names are erased + metadata in anon-mode checking, so no checker-side rejection is needed. + +- **`isNeverZero` (`Ix/Tc/Inductive.lean:301`): sound as-is.** Its + true-cases are genuinely never-zero under any assignment; false just + falls through to the conservative single-ctor analysis, matching the + large-eliminator semantics. + +- **FFI/ABI across v4.29 → v4.33: no layout regression.** All 17 hardcoded + constructor layouts in `crates/ffi/src/lean.rs` were audited against + v4.33 declarations — byte-correct for both the `Ix.*` mirror types and + the real Lean kernel objects `lean_env.rs` decodes. The one real bug + found (pre-existing): `Lean.Int` decoded as a ctor when it is a + `Nat`-representation builtin — fixed on this branch (`fix(ffi): decode + Lean.Int by value`). `lean-ffi` needs no changes (bindings regenerate per + build; none of the removed/changed `lean.h` symbols are used). + +## 5. Non-blocking follow-ups + +- **FFI pointer-liveness hardening.** `crates/ffi/src/lean_env.rs:594,615` + key caches by raw `lean_object*` across a decode session; soundness rests + on callers keeping arguments alive, and v4.30's RC/borrow changes shift + free/reuse timing. v4.30 added `Runtime.hold` (#13270) for exactly this — + wrap the Lean-side callers of the env-decoding externs, or take explicit + refs in Rust. Related audit caveats: the `LeanIx*` layout types' `alloc` + path must never be pointed at real Lean types (the phantom trailing + `hash` object slot coincidentally overlays Lean's computed-field scalar, + which is safe to read one-below but wrong to allocate), and the + `assert!(i < num_obj)` bound cannot catch an off-by-one into that slot. + +- **Benchmark re-baselining.** Pre-v4.30 numbers are not comparable: the + LCNF backend rewrite landed end-to-end (~15% smaller binaries), LLVM + 19 → 22, DiscrTree fixes (~10% faster `import Mathlib`), `ByteArray` + equality is now `memcmp`, default 1GB stacks on all threads. Re-baseline + `bench.json` / CI benchmarks; do not chase cross-version deltas. + +- **Thread-pool interaction.** v4.32 #13123 reclaims idle pool workers + after 5s; reclaimed-and-respawned workers pick up the stack size current + at spawn. ix sets it via `rs_lean_set_thread_stack_size` + (`Ix/Tc/ParCheck.lean:57`) — verify it still runs before the parallel + check phase, and expect lower RSS with possible thread-churn in bursty + phases. + +- **OpenSSL now linked into the Lean runtime** (v4.32 #12030/#13988): a + plausible duplicate-symbol/version-skew source on the `net`-featured + `ix` exe, where iroh brings its own TLS stack. No breakage observed; + watch link errors on that target. + +- **`lake setup-file` JSON parsing.** `Ix/Common.lean:266-274` string-splits + the JSON and v4.33 #14300 enlarged `setup.json`; the code's own TODO asks + for a real JSON parse. + +- **`Benchmarks/CompileFC`** is deliberately frozen at Lean v4.27.0 on + upstream `lenianiva/lean4-nix` (its overlay API still works there). Do + not bump it as part of toolchain updates.