From 06e99c912660c11739912b86e965889d98065063 Mon Sep 17 00:00:00 2001 From: samuelburnham <45365069+samuelburnham@users.noreply.github.com> Date: Wed, 18 Feb 2026 11:18:37 -0500 Subject: [PATCH 1/8] chore: Update Lean to v4.27.0 --- Benchmarks/Blake3.lean | 12 +++- Ix/Common.lean | 8 ++- Ix/Meta.lean | 4 +- Ix/Store.lean | 11 ++-- Tests/FFI/Basic.lean | 4 +- Tests/Gen/Basic.lean | 2 +- Tests/Ix/CanonM.lean | 14 ++-- Tests/Ix/Commit.lean | 4 +- Tests/Ix/Compile.lean | 12 ++-- Tests/Ix/CondenseM.lean | 6 +- Tests/Ix/Decompile.lean | 6 +- Tests/Ix/GraphM.lean | 6 +- Tests/Ix/RustDecompile.lean | 8 +-- Tests/Ix/RustSerialize.lean | 8 +-- Tests/ShardMap.lean | 124 ++++++++++++++++++------------------ flake.lock | 81 +++++++++++------------ flake.nix | 6 +- lake-manifest.json | 16 ++--- lakefile.lean | 14 ++-- lean-toolchain | 2 +- 20 files changed, 175 insertions(+), 173 deletions(-) diff --git a/Benchmarks/Blake3.lean b/Benchmarks/Blake3.lean index 03f33bd6..c48fc387 100644 --- a/Benchmarks/Blake3.lean +++ b/Benchmarks/Blake3.lean @@ -45,7 +45,7 @@ def blake3Bench : IO $ Array BenchReport := do bgroup "prove blake3" benches.toList { oneShot := true } def parseFunction (words : List String) (param : String): Option String := - words.find? (·.startsWith param) |> .map (·.stripPrefix param) + words.find? (·.startsWith param) |> .map (·.dropPrefix param |>.toString) def main : IO Unit := do let result ← blake3Bench @@ -53,8 +53,14 @@ def main : IO Unit := do let mut weightedSum := 0.0 for report in result do let words := report.function.splitOn - let dataSize := (parseFunction words "dataSize=").get!.toNat! - let numHashes := (parseFunction words "numHashes=").get!.toNat! + let .some dataSizeStr := parseFunction words "dataSize=" + | throw $ IO.userError s!"Missing dataSize in: {report.function}" + let .some dataSize := dataSizeStr.toNat? + | throw $ IO.userError s!"Invalid dataSize: {dataSizeStr}" + let .some numHashesStr := parseFunction words "numHashes=" + | throw $ IO.userError s!"Missing numHashes in: {report.function}" + let .some numHashes := numHashesStr.toNat? + | throw $ IO.userError s!"Invalid numHashes: {numHashesStr}" let sizeFloat := (dataSize * numHashes).toFloat let throughput := sizeFloat / (report.newBench.getTime.toSeconds ) weightedSum := weightedSum + sizeFloat * throughput diff --git a/Ix/Common.lean b/Ix/Common.lean index 2004aef5..2a38f40f 100644 --- a/Ix/Common.lean +++ b/Ix/Common.lean @@ -279,8 +279,10 @@ def checkToolchain : IO Unit := do match ← runCmd' "lake" #["--version"] with | .error e => throw $ IO.userError e | .ok out => - let version := (out.splitOn "(Lean version ")[1]! - let version := version.splitOn ")" |>.head! + let .some version := (out.splitOn "(Lean version ")[1]? + | throw $ IO.userError s!"Could not parse Lean version from: {out}" + let .some version := (version.splitOn ")").head? + | throw $ IO.userError s!"Could not parse Lean version from: {out}" let expectedVersion := Lean.versionString if version != expectedVersion then IO.println s!"Warning: expected toolchain '{expectedVersion}' but got '{version}'" @@ -298,7 +300,7 @@ def runFrontend (input : String) (filePath : FilePath) : IO Environment := do let msgs := s.commandState.messages if msgs.hasErrors then throw $ IO.userError $ "\n\n".intercalate $ - (← msgs.toList.mapM (·.toString)).map String.trim + (← msgs.toList.mapM (·.toString)).map (String.trimAscii · |>.toString) else return s.commandState.env end Lean diff --git a/Ix/Meta.lean b/Ix/Meta.lean index 3ad07882..3aec1d65 100644 --- a/Ix/Meta.lean +++ b/Ix/Meta.lean @@ -14,7 +14,7 @@ def getFileEnv (path : FilePath) : IO Environment := do args := #["env", "printenv", "LEAN_PATH"] cwd := path.parent } - let paths := out.stdout.trim.splitOn ":" |>.map FilePath.mk + let paths := out.stdout.trimAscii.toString.splitOn ":" |>.map FilePath.mk initSearchPath (← findSysroot) paths let source ← IO.FS.readFile path @@ -23,7 +23,7 @@ def getFileEnv (path : FilePath) : IO Environment := do let (env, messages) ← processHeader header default messages inputCtx 0 if messages.hasErrors then throw $ IO.userError $ "\n\n".intercalate $ - (← messages.toList.mapM (·.toString)).map String.trim + (← messages.toList.mapM (·.toString)).map (String.trimAscii · |>.toString) return env elab "this_file!" : term => do diff --git a/Ix/Store.lean b/Ix/Store.lean index d8c6d5ad..dbde4657 100644 --- a/Ix/Store.lean +++ b/Ix/Store.lean @@ -41,12 +41,11 @@ def storeDir : StoreIO FilePath := do def storePath (addr: Address): StoreIO FilePath := do let store <- storeDir let hex := hexOfBytes addr.hash - -- TODO: Use Slice API once it matures - let hexChars := hex.toSlice.chars.toList - let dir1 := String.ofList [hexChars[0]!, hexChars[1]!] - let dir2 := String.ofList [hexChars[2]!, hexChars[3]!] - let dir3 := String.ofList [hexChars[4]!, hexChars[5]!] - let file := hex.drop 6 + let s := hex.toSlice + let dir1 := (s.take 2).toString + let dir2 := (s.drop 2 |>.take 2).toString + let dir3 := (s.drop 4 |>.take 2).toString + let file := (s.drop 6).toString let path := store / dir1 / dir2 / dir3 if !(<- path.pathExists) then IO.toEIO .ioError (IO.FS.createDirAll path) diff --git a/Tests/FFI/Basic.lean b/Tests/FFI/Basic.lean index 6a020eb5..aac3d543 100644 --- a/Tests/FFI/Basic.lean +++ b/Tests/FFI/Basic.lean @@ -84,9 +84,9 @@ def largeNatTests : TestSeq := let testCases : List Nat := [0, 1, 255, 256, 65535, 65536, (2^32 - 1), 2^32, (2^63 - 1), 2^63, (2^64 - 1), 2^64, 2^64 + 1, 2^128, 2^256] testCases.foldl (init := .done) fun acc n => - acc ++ .individualIO s!"Nat {n}" (do + acc ++ .individualIO s!"Nat {n}" none (do let rt := roundtripNat n - pure (rt == n, if rt == n then none else some s!"got {rt}")) .done + pure (rt == n, 0, 0, if rt == n then none else some s!"got {rt}")) .done /-! ## Helper to compare HashMaps -/ diff --git a/Tests/Gen/Basic.lean b/Tests/Gen/Basic.lean index aa6e1a76..4c146f37 100644 --- a/Tests/Gen/Basic.lean +++ b/Tests/Gen/Basic.lean @@ -146,7 +146,7 @@ instance : Shrinkable ByteArray where shrink ba := if ba.isEmpty then [] else [ba.extract 0 (ba.size - 1)] instance : Shrinkable String where - shrink s := if s.isEmpty then [] else [s.dropRight 1] + shrink s := if s.isEmpty then [] else [s.dropEnd 1 |>.toString] instance : Shrinkable Point where shrink p := if p.x == 0 && p.y == 0 then [] else [⟨p.x / 2, p.y / 2⟩] diff --git a/Tests/Ix/CanonM.lean b/Tests/Ix/CanonM.lean index e8c4d2fa..9201f9bb 100644 --- a/Tests/Ix/CanonM.lean +++ b/Tests/Ix/CanonM.lean @@ -237,7 +237,7 @@ This test verifies the full canonicalization pipeline: /-- Run the full canonicalization roundtrip test. -/ def testFullCanonRoundtrip : TestSeq := - .individualIO "full canonicalization roundtrip" (do + .individualIO "full canonicalization roundtrip" none (do let env ← get_env! let numConsts := env.constants.toList.length @@ -311,7 +311,7 @@ def testFullCanonRoundtrip : TestSeq := IO.println s!"\r[Test] Compared {processed}: {mismatches} mismatches, {rustMissing} missing in Rust, {leanMissing} missing in Lean ({formatTime compareTime})" if rustMissing > 0 || leanMissing > 0 || mismatches > 0 then - return (false, some s!"Rust vs Lean: {mismatches} mismatches, {rustMissing} missing in Rust, {leanMissing} missing in Lean") + return (false, 0, 0, some s!"Rust vs Lean: {mismatches} mismatches, {rustMissing} missing in Rust, {leanMissing} missing in Lean") IO.println "" -- Step 4: Uncanonicalize Lean's Ix constants back to Lean (parallel) @@ -353,7 +353,7 @@ def testFullCanonRoundtrip : TestSeq := some s!"rustMissing={rustMissing}, leanMissing={leanMissing}, mismatches={mismatches}, rtMissing={rtMissing}, rtMismatches={rtMismatches}" else none - pure (success, failMsg) + pure (success, 0, 0, failMsg) ) .done /-! ## Pure Lean canonicalization roundtrip test @@ -368,7 +368,7 @@ in pure Lean without any Rust FFI: /-- Run the pure Lean canonicalization roundtrip test. -/ def testPureLeanRoundtrip : TestSeq := - .individualIO "pure Lean canonicalization roundtrip" (do + .individualIO "pure Lean canonicalization roundtrip" none (do let env ← get_env! let numConsts := env.constants.toList.length @@ -420,7 +420,7 @@ def testPureLeanRoundtrip : TestSeq := some s!"missing={missing}, mismatches={mismatches}" else none - pure (success, failMsg) + pure (success, 0, 0, failMsg) ) .done /-! ## Parallel Lean canonicalization roundtrip test @@ -434,7 +434,7 @@ This test verifies parallel canonicalization using ShardMap: /-- Run the parallel Lean canonicalization roundtrip test. -/ def testParallelLeanRoundtrip : TestSeq := - .individualIO "parallel Lean canonicalization roundtrip" (do + .individualIO "parallel Lean canonicalization roundtrip" none (do let env ← get_env! let numConsts := env.constants.toList.length @@ -486,7 +486,7 @@ def testParallelLeanRoundtrip : TestSeq := some s!"missing={missing}, mismatches={mismatches}" else none - pure (success, failMsg) + pure (success, 0, 0, failMsg) ) .done /-- Full canonicalization roundtrip test suite (expensive, in ignored tests). -/ diff --git a/Tests/Ix/Commit.lean b/Tests/Ix/Commit.lean index 9b639a52..a48345ac 100644 --- a/Tests/Ix/Commit.lean +++ b/Tests/Ix/Commit.lean @@ -223,11 +223,11 @@ def claimConstructorTests : TestSeq := /-! ## IO tests for commitConst -/ def commitConstIOTest : TestSeq := - .individualIO "commitConst: different random secrets produce different addresses" (do + .individualIO "commitConst: different random secrets produce different addresses" none (do let payload := Address.blake3 "test-payload".toUTF8 let (_, commitAddr1) ← Ix.Commit.commitConst payload let (_, commitAddr2) ← Ix.Commit.commitConst payload - return (commitAddr1 != commitAddr2, none)) .done + return (commitAddr1 != commitAddr2, 0, 0, none)) .done /-! ## Suite registration -/ diff --git a/Tests/Ix/Compile.lean b/Tests/Ix/Compile.lean index fa6dadff..3d46830c 100644 --- a/Tests/Ix/Compile.lean +++ b/Tests/Ix/Compile.lean @@ -128,7 +128,7 @@ def serializeEnv (env : Ixon.Env) : ByteArray := /-- Cross-implementation compilation test using the new CompilePhases API -/ def testCrossImpl : TestSeq := - .individualIO "Compilation Cross-Implementation" (do + .individualIO "Compilation Cross-Implementation" none (do let leanEnv ← get_env! let totalConsts := leanEnv.constants.toList.length @@ -155,8 +155,8 @@ def testCrossImpl : TestSeq := IO.println s!"[Step 2] Compilation failed after {leanTime}ms" if let some sysErr := err.systemError then IO.println s!"[Error] {sysErr}" - return (false, some sysErr) - return (false, some "Compilation failed") + return (false, 0, 0, some sysErr) + return (false, 0, 0, some "Compilation failed") | .ok (leanIxonEnv, totalBytes) => let leanTime := (← IO.monoMsNow) - leanStart @@ -367,7 +367,7 @@ def testCrossImpl : TestSeq := IO.println s!"[Step 4] Serialized environments match exactly! ✓" IO.println "" - return (true, none) + return (true, 0, 0, none) else IO.println s!"[Step 4] Serialized environments DIFFER" if let some diffPos := findFirstDiff leanEnvBytes rustEnvBytes then @@ -410,7 +410,7 @@ def testCrossImpl : TestSeq := IO.println "" -- Note: We expect this to fail until Lean generates metadata - return (false, some s!"Serialized environments differ (Lean: {fmtBytes leanEnvBytes.size}, Rust: {fmtBytes rustEnvBytes.size})") + return (false, 0, 0, some s!"Serialized environments differ (Lean: {fmtBytes leanEnvBytes.size}, Rust: {fmtBytes rustEnvBytes.size})") else -- Report mismatches IO.println s!"[Step 3] Found {result.mismatchedConstants.size} mismatches!" @@ -455,7 +455,7 @@ def testCrossImpl : TestSeq := IO.println s!" ... and {result.missingInLean.size - 5} more" IO.println "" - return (false, some s!"Found {result.mismatchedConstants.size} mismatches") + return (false, 0, 0, some s!"Found {result.mismatchedConstants.size} mismatches") ) .done /-! ## Test Suite -/ diff --git a/Tests/Ix/CondenseM.lean b/Tests/Ix/CondenseM.lean index d54d85fe..db7140da 100644 --- a/Tests/Ix/CondenseM.lean +++ b/Tests/Ix/CondenseM.lean @@ -315,7 +315,7 @@ def compareSCCResults /-- Cross-implementation test: compare Lean and Rust SCC computation -/ def testSccComparison : TestSeq := - .individualIO "SCC Computation: Lean vs Rust" (do + .individualIO "SCC Computation: Lean vs Rust" none (do let env ← get_env! let numConsts := env.constants.toList.length @@ -370,9 +370,9 @@ def testSccComparison : TestSeq := IO.println s!"[Test] SCCs match: {sccsMatch}" if !sccsMatch then - return (false, some s!"SCCs do not match: {mismatches.size} mismatches") + return (false, 0, 0, some s!"SCCs do not match: {mismatches.size} mismatches") - return (true, none) + return (true, 0, 0, none) ) .done /-- Cross-implementation test suite (expensive, run with --ignored) -/ diff --git a/Tests/Ix/Decompile.lean b/Tests/Ix/Decompile.lean index 2d659f34..1012de79 100644 --- a/Tests/Ix/Decompile.lean +++ b/Tests/Ix/Decompile.lean @@ -21,7 +21,7 @@ namespace Tests.Decompile /-- Decompile roundtrip test: Rust compile → parallel decompile → hash comparison -/ def testDecompile : TestSeq := - .individualIO "Decompilation Roundtrip" (do + .individualIO "Decompilation Roundtrip" none (do let leanEnv ← get_env! let totalConsts := leanEnv.constants.toList.length @@ -114,9 +114,9 @@ def testDecompile : TestSeq := let success := decompErrors.size == 0 && nMismatch == 0 && nMissing == 0 if success then - return (true, none) + return (true, 0, 0, none) else - return (false, some s!"{decompErrors.size} decompilation errors") + return (false, 0, 0, some s!"{decompErrors.size} decompilation errors") ) .done /-! ## Test Suite -/ diff --git a/Tests/Ix/GraphM.lean b/Tests/Ix/GraphM.lean index 29458ca7..b66f6bc7 100644 --- a/Tests/Ix/GraphM.lean +++ b/Tests/Ix/GraphM.lean @@ -406,7 +406,7 @@ def compareRefGraphs (lean rust : Std.HashMap Ix.Name (Std.HashSet Ix.Name)) /-- Cross-implementation test: compare Lean and Rust reference graph construction -/ def testRefGraphComparison : TestSeq := - .individualIO "Reference Graph: Lean vs Rust" (do + .individualIO "Reference Graph: Lean vs Rust" none (do let env ← get_env! let numConsts := env.constants.toList.length @@ -456,9 +456,9 @@ def testRefGraphComparison : TestSeq := IO.println s!"[Test] Match: {isEqual}" if !isEqual then - return (false, some s!"Reference graphs do not match: {mismatches.size} mismatches") + return (false, 0, 0, some s!"Reference graphs do not match: {mismatches.size} mismatches") - return (true, none) + return (true, 0, 0, none) ) .done /-- Cross-implementation test suite (expensive, run with --ignored) -/ diff --git a/Tests/Ix/RustDecompile.lean b/Tests/Ix/RustDecompile.lean index 89bdd5d2..6f150cad 100644 --- a/Tests/Ix/RustDecompile.lean +++ b/Tests/Ix/RustDecompile.lean @@ -21,7 +21,7 @@ namespace Tests.RustDecompile /-- Test Rust decompilation: compile → rsDecompileEnv → hash comparison -/ def testRustDecompile : TestSeq := - .individualIO "Rust Decompilation Roundtrip" (do + .individualIO "Rust Decompilation Roundtrip" none (do let leanEnv ← get_env! let totalConsts := leanEnv.constants.toList.length @@ -45,7 +45,7 @@ def testRustDecompile : TestSeq := | .ok env => pure env | .error e => do IO.println s!"[Step 2] FAILED: {toString e}" - return (false, some (toString e)) + return (false, 0, 0, some (toString e)) let decompTime := (← IO.monoMsNow) - decompStart IO.println s!"[Step 2] {decompiled.size} constants decompiled in {decompTime}ms" IO.println "" @@ -112,9 +112,9 @@ def testRustDecompile : TestSeq := let success := nMismatch == 0 && nMissing == 0 if success then - return (true, none) + return (true, 0, 0, none) else - return (false, some s!"{nMismatch} mismatches, {nMissing} missing") + return (false, 0, 0, some s!"{nMismatch} mismatches, {nMissing} missing") ) .done /-! ## Test Suite -/ diff --git a/Tests/Ix/RustSerialize.lean b/Tests/Ix/RustSerialize.lean index dd5e4684..ff54d5ac 100644 --- a/Tests/Ix/RustSerialize.lean +++ b/Tests/Ix/RustSerialize.lean @@ -18,7 +18,7 @@ namespace Tests.RustSerialize /-- Test Rust serde roundtrip: compile → rsSerEnv → rsDesEnv → Lean serEnv → byte compare -/ def testRustSerdeRoundtrip : TestSeq := - .individualIO "Rust Serialize/Deserialize Roundtrip" (do + .individualIO "Rust Serialize/Deserialize Roundtrip" none (do let leanEnv ← get_env! let totalConsts := leanEnv.constants.toList.length @@ -57,7 +57,7 @@ def testRustSerdeRoundtrip : TestSeq := | .ok env => pure env | .error e => do IO.println s!"[Step 4] FAILED: {e}" - return (false, some e) + return (false, 0, 0, some e) let rustDesTime := (← IO.monoMsNow) - rustDesStart IO.println s!"[Step 4] {roundtrippedFromRust.constCount} constants in {rustDesTime}ms" IO.println "" @@ -75,7 +75,7 @@ def testRustSerdeRoundtrip : TestSeq := if leanBytes == roundtrippedBytes then IO.println s!"[Step 6] Byte-exact match! ({leanBytes.size} bytes) ✓" IO.println "" - return (true, none) + return (true, 0, 0, none) else IO.println s!"[Step 6] MISMATCH: {leanBytes.size} bytes vs {roundtrippedBytes.size} bytes" -- Find first diff @@ -87,7 +87,7 @@ def testRustSerdeRoundtrip : TestSeq := break IO.println s!"[Step 6] First difference at byte {firstDiff}" IO.println "" - return (false, some s!"Bytes differ at offset {firstDiff} (original {leanBytes.size} vs roundtripped {roundtrippedBytes.size})") + return (false, 0, 0, some s!"Bytes differ at offset {firstDiff} (original {leanBytes.size} vs roundtripped {roundtrippedBytes.size})") ) .done /-! ## Test Suite -/ diff --git a/Tests/ShardMap.lean b/Tests/ShardMap.lean index c7ed382a..e5815a13 100644 --- a/Tests/ShardMap.lean +++ b/Tests/ShardMap.lean @@ -6,20 +6,20 @@ open LSpec Ix namespace Tests.ShardMap def testInsertAndGet : TestSeq := - .individualIO "basic insert and get" (do + .individualIO "basic insert and get" none (do let map ← ShardMap.new (α := String) (β := Nat) (shardBits := 2) map.insert "hello" 42 let v ← map.get? "hello" - pure (v == some 42, none)) .done + pure (v == some 42, 0, 0, none)) .done def testGetNonExistent : TestSeq := - .individualIO "get non-existent returns none" (do + .individualIO "get non-existent returns none" none (do let map ← ShardMap.new (α := String) (β := Nat) (shardBits := 2) let v ← map.get? "nonexistent" - pure (v == none, none)) .done + pure (v == none, 0, 0, none)) .done def testMultipleInserts : TestSeq := - .individualIO "multiple inserts" (do + .individualIO "multiple inserts" none (do let map ← ShardMap.new (α := String) (β := Nat) (shardBits := 2) map.insert "foo" 1 map.insert "bar" 2 @@ -27,85 +27,85 @@ def testMultipleInserts : TestSeq := let v1 ← map.get? "foo" let v2 ← map.get? "bar" let v3 ← map.get? "baz" - pure (v1 == some 1 && v2 == some 2 && v3 == some 3, none)) .done + pure (v1 == some 1 && v2 == some 2 && v3 == some 3, 0, 0, none)) .done def testOverwrite : TestSeq := - .individualIO "overwrite existing key" (do + .individualIO "overwrite existing key" none (do let map ← ShardMap.new (α := String) (β := Nat) (shardBits := 2) map.insert "key" 1 map.insert "key" 2 let v ← map.get? "key" - pure (v == some 2, none)) .done + pure (v == some 2, 0, 0, none)) .done def testSize : TestSeq := - .individualIO "size" (do + .individualIO "size" none (do let map ← ShardMap.new (α := String) (β := Nat) (shardBits := 2) map.insert "a" 1 map.insert "b" 2 map.insert "c" 3 let sz ← map.size - pure (sz == 3, none)) .done + pure (sz == 3, 0, 0, none)) .done def testContains : TestSeq := - .individualIO "contains" (do + .individualIO "contains" none (do let map ← ShardMap.new (α := String) (β := Nat) (shardBits := 2) map.insert "exists" 1 let c1 ← map.contains "exists" let c2 ← map.contains "missing" - pure (c1 && !c2, none)) .done + pure (c1 && !c2, 0, 0, none)) .done def testRemove : TestSeq := - .individualIO "remove" (do + .individualIO "remove" none (do let map ← ShardMap.new (α := String) (β := Nat) (shardBits := 2) map.insert "key" 42 let removed ← map.remove "key" let after ← map.get? "key" - pure (removed == some 42 && after == none, none)) .done + pure (removed == some 42 && after == none, 0, 0, none)) .done def testModify : TestSeq := - .individualIO "modify" (do + .individualIO "modify" none (do let map ← ShardMap.new (α := String) (β := Nat) (shardBits := 2) map.insert "key" 10 let modified ← map.modify "key" (· + 5) let v ← map.get? "key" - pure (modified && v == some 15, none)) .done + pure (modified && v == some 15, 0, 0, none)) .done def testGetOrInsertExisting : TestSeq := - .individualIO "getOrInsert existing" (do + .individualIO "getOrInsert existing" none (do let map ← ShardMap.new (α := String) (β := Nat) (shardBits := 2) map.insert "key" 42 let v ← map.getOrInsert "key" (fun () => pure 999) - pure (v == 42, none)) .done + pure (v == 42, 0, 0, none)) .done def testGetOrInsertNew : TestSeq := - .individualIO "getOrInsert new" (do + .individualIO "getOrInsert new" none (do let map ← ShardMap.new (α := String) (β := Nat) (shardBits := 2) let v ← map.getOrInsert "key" (fun () => pure 999) let check ← map.get? "key" - pure (v == 999 && check == some 999, none)) .done + pure (v == 999 && check == some 999, 0, 0, none)) .done def testClear : TestSeq := - .individualIO "clear" (do + .individualIO "clear" none (do let map ← ShardMap.new (α := String) (β := Nat) (shardBits := 2) map.insert "a" 1 map.insert "b" 2 map.clear let sz ← map.size - pure (sz == 0, none)) .done + pure (sz == 0, 0, 0, none)) .done def testToList : TestSeq := - .individualIO "toList" (do + .individualIO "toList" none (do let map ← ShardMap.new (α := Nat) (β := String) (shardBits := 1) map.insert 1 "one" map.insert 2 "two" let list ← map.toList - pure (list.length == 2, none)) .done + pure (list.length == 2, 0, 0, none)) .done -- Concurrent tests /-- Test concurrent reads don't block each other with SharedMutex -/ def testConcurrentReads : TestSeq := - .individualIO "concurrent reads" (do + .individualIO "concurrent reads" none (do let map ← ShardMap.new (α := Nat) (β := Nat) (shardBits := 2) -- Insert many values for i in [:1000] do @@ -127,11 +127,11 @@ def testConcurrentReads : TestSeq := match task.get with | .ok ok => if !ok then allPassed := false | .error _ => allPassed := false - pure (allPassed, none)) .done + pure (allPassed, 0, 0, none)) .done /-- Test concurrent writes to different keys -/ def testConcurrentWritesDifferentKeys : TestSeq := - .individualIO "concurrent writes different keys" (do + .individualIO "concurrent writes different keys" none (do let map ← ShardMap.new (α := Nat) (β := Nat) (shardBits := 4) let numWriters := 16 let keysPerWriter := 100 @@ -150,11 +150,11 @@ def testConcurrentWritesDifferentKeys : TestSeq := for i in [:(numWriters * keysPerWriter)] do let v ← map.get? i if v != some (i * 3) then allCorrect := false - pure (allCorrect, none)) .done + pure (allCorrect, 0, 0, none)) .done /-- Test concurrent getOrInsert with same keys (race condition test) -/ def testConcurrentGetOrInsert : TestSeq := - .individualIO "concurrent getOrInsert consistency" (do + .individualIO "concurrent getOrInsert consistency" none (do let map ← ShardMap.new (α := Nat) (β := Nat) (shardBits := 2) let numWorkers := 32 let numKeys := 100 @@ -180,64 +180,64 @@ def testConcurrentGetOrInsert : TestSeq := let firstVal := allResults[0]![k]! for results in allResults do if results[k]! != firstVal then consistent := false - pure (consistent, none)) .done + pure (consistent, 0, 0, none)) .done /-- Test getOrInsertLazy works correctly -/ def testGetOrInsertLazy : TestSeq := - .individualIO "getOrInsertLazy" (do + .individualIO "getOrInsertLazy" none (do let map ← ShardMap.new (α := String) (β := Nat) (shardBits := 2) let v1 ← map.getOrInsertLazy "key" (fun () => 42) let v2 ← map.getOrInsertLazy "key" (fun () => 999) -- Should not be called - pure (v1 == 42 && v2 == 42, none)) .done + pure (v1 == 42 && v2 == 42, 0, 0, none)) .done /-- Test getOrInsertIO works correctly -/ def testGetOrInsertIO : TestSeq := - .individualIO "getOrInsertIO" (do + .individualIO "getOrInsertIO" none (do let map ← ShardMap.new (α := String) (β := Nat) (shardBits := 2) let counter ← IO.mkRef 0 let v1 ← map.getOrInsertIO "key" (fun () => do counter.modify (· + 1); pure 42) let v2 ← map.getOrInsertIO "key" (fun () => do counter.modify (· + 1); pure 999) let calls ← counter.get - pure (v1 == 42 && v2 == 42 && calls == 1, none)) .done + pure (v1 == 42 && v2 == 42 && calls == 1, 0, 0, none)) .done /-! ## Tests for try operations -/ /-- Test tryGet? returns value when unlocked -/ def testTryGetUnlocked : TestSeq := - .individualIO "tryGet? unlocked" (do + .individualIO "tryGet? unlocked" none (do let map ← ShardMap.new (α := String) (β := Nat) (shardBits := 2) map.insert "key" 42 let v ← map.tryGet? "key" - pure (v == some (some 42), none)) .done + pure (v == some (some 42), 0, 0, none)) .done /-- Test tryGet? returns none for non-existent key -/ def testTryGetNonExistent : TestSeq := - .individualIO "tryGet? non-existent" (do + .individualIO "tryGet? non-existent" none (do let map ← ShardMap.new (α := String) (β := Nat) (shardBits := 2) let v ← map.tryGet? "missing" - pure (v == some none, none)) .done + pure (v == some none, 0, 0, none)) .done /-- Test tryInsert succeeds when unlocked -/ def testTryInsert : TestSeq := - .individualIO "tryInsert" (do + .individualIO "tryInsert" none (do let map ← ShardMap.new (α := String) (β := Nat) (shardBits := 2) let ok ← map.tryInsert "key" 42 let v ← map.get? "key" - pure (ok && v == some 42, none)) .done + pure (ok && v == some 42, 0, 0, none)) .done /-- Test tryGetOrInsertLazy works correctly -/ def testTryGetOrInsertLazy : TestSeq := - .individualIO "tryGetOrInsertLazy" (do + .individualIO "tryGetOrInsertLazy" none (do let map ← ShardMap.new (α := String) (β := Nat) (shardBits := 2) let v1 ← map.tryGetOrInsertLazy "key" (fun () => 42) let v2 ← map.tryGetOrInsertLazy "key" (fun () => 999) -- Should return existing - pure (v1 == some 42 && v2 == some 42, none)) .done + pure (v1 == some 42 && v2 == some 42, 0, 0, none)) .done /-! ## Tests for insertMany -/ /-- Test insertMany inserts all items correctly -/ def testInsertMany : TestSeq := - .individualIO "insertMany" (do + .individualIO "insertMany" none (do let map ← ShardMap.new (α := Nat) (β := String) (shardBits := 2) let items := #[(1, "one"), (2, "two"), (3, "three"), (4, "four"), (5, "five")] map.insertMany items @@ -248,29 +248,29 @@ def testInsertMany : TestSeq := let v5 ← map.get? 5 let sz ← map.size pure (v1 == some "one" && v2 == some "two" && v3 == some "three" - && v4 == some "four" && v5 == some "five" && sz == 5, none)) .done + && v4 == some "four" && v5 == some "five" && sz == 5, 0, 0, none)) .done /-- Test insertMany with empty array -/ def testInsertManyEmpty : TestSeq := - .individualIO "insertMany empty" (do + .individualIO "insertMany empty" none (do let map ← ShardMap.new (α := Nat) (β := Nat) (shardBits := 2) map.insertMany #[] let sz ← map.size - pure (sz == 0, none)) .done + pure (sz == 0, 0, 0, none)) .done /-- Test insertMany overwrites existing keys -/ def testInsertManyOverwrite : TestSeq := - .individualIO "insertMany overwrite" (do + .individualIO "insertMany overwrite" none (do let map ← ShardMap.new (α := Nat) (β := Nat) (shardBits := 2) map.insert 1 100 map.insertMany #[(1, 200), (2, 300)] let v1 ← map.get? 1 let v2 ← map.get? 2 - pure (v1 == some 200 && v2 == some 300, none)) .done + pure (v1 == some 200 && v2 == some 300, 0, 0, none)) .done /-- Test concurrent insertMany operations -/ def testConcurrentInsertMany : TestSeq := - .individualIO "concurrent insertMany" (do + .individualIO "concurrent insertMany" none (do let map ← ShardMap.new (α := Nat) (β := Nat) (shardBits := 4) let numWorkers := 8 let itemsPerWorker := 100 @@ -291,38 +291,38 @@ def testConcurrentInsertMany : TestSeq := let v ← map.get? i if v != some (i * 2) then allCorrect := false let sz ← map.size - pure (allCorrect && sz == numWorkers * itemsPerWorker, none)) .done + pure (allCorrect && sz == numWorkers * itemsPerWorker, 0, 0, none)) .done /-! ## Tests for modifyGet -/ /-- Test modifyGet returns result and updates value -/ def testModifyGet : TestSeq := - .individualIO "modifyGet" (do + .individualIO "modifyGet" none (do let map ← ShardMap.new (α := String) (β := Nat) (shardBits := 2) map.insert "counter" 10 let result ← map.modifyGet "counter" fun v => (v, v + 1) let newVal ← map.get? "counter" - pure (result == some 10 && newVal == some 11, none)) .done + pure (result == some 10 && newVal == some 11, 0, 0, none)) .done /-- Test modifyGet returns none for non-existent key -/ def testModifyGetNonExistent : TestSeq := - .individualIO "modifyGet non-existent" (do + .individualIO "modifyGet non-existent" none (do let map ← ShardMap.new (α := String) (β := Nat) (shardBits := 2) let result ← map.modifyGet "missing" fun v => (v, v + 1) - pure (result == none, none)) .done + pure (result == none, 0, 0, none)) .done /-- Test modifyGet can return different type than value -/ def testModifyGetDifferentType : TestSeq := - .individualIO "modifyGet different type" (do + .individualIO "modifyGet different type" none (do let map ← ShardMap.new (α := String) (β := Nat) (shardBits := 2) map.insert "key" 42 let result ← map.modifyGet "key" fun v => (s!"was {v}", v * 2) let newVal ← map.get? "key" - pure (result == some "was 42" && newVal == some 84, none)) .done + pure (result == some "was 42" && newVal == some 84, 0, 0, none)) .done /-- Test concurrent modifyGet operations -/ def testConcurrentModifyGet : TestSeq := - .individualIO "concurrent modifyGet" (do + .individualIO "concurrent modifyGet" none (do let map ← ShardMap.new (α := Nat) (β := Nat) (shardBits := 2) -- Initialize counters for i in [:10] do @@ -346,13 +346,13 @@ def testConcurrentModifyGet : TestSeq := for i in [:10] do let v ← map.get? i if v != some expected then allCorrect := false - pure (allCorrect, none)) .done + pure (allCorrect, 0, 0, none)) .done /-! ## Tests for newWithCapacity -/ /-- Test newWithCapacity creates a working map -/ def testNewWithCapacity : TestSeq := - .individualIO "newWithCapacity" (do + .individualIO "newWithCapacity" none (do let map ← ShardMap.newWithCapacity (α := Nat) (β := Nat) (shardBits := 4) (capacityPerShard := 1000) -- Insert many values @@ -364,11 +364,11 @@ def testNewWithCapacity : TestSeq := let v ← map.get? i if v != some (i * 2) then allOk := false let sz ← map.size - pure (allOk && sz == 500, none)) .done + pure (allOk && sz == 500, 0, 0, none)) .done /-- Test concurrent tryGet? operations -/ def testConcurrentTryGet : TestSeq := - .individualIO "concurrent tryGet?" (do + .individualIO "concurrent tryGet?" none (do let map ← ShardMap.new (α := Nat) (β := Nat) (shardBits := 2) -- 4 shards for i in [:100] do map.insert i i @@ -391,7 +391,7 @@ def testConcurrentTryGet : TestSeq := -- Most should succeed (reads don't block each other with SharedMutex) -- With 32 readers × 100 keys = 3200 operations, expect at least 100 to succeed -- (conservative threshold to avoid flakiness) - pure (successes > 100, none)) .done + pure (successes > 100, 0, 0, none)) .done def suite : List TestSeq := [ testInsertAndGet, diff --git a/flake.lock b/flake.lock index 78c17721..0490bc41 100644 --- a/flake.lock +++ b/flake.lock @@ -3,16 +3,16 @@ "blake3": { "flake": false, "locked": { - "lastModified": 1745192552, - "narHash": "sha256-IABVErXWYQFXZcwsFKfQhm3ox7UZUcW5uzVrGwsSp94=", + "lastModified": 1767892649, + "narHash": "sha256-aj+fru2saqWxDDiV3mNCZZeZIGTxSgta/X50R87hoko=", "owner": "BLAKE3-team", "repo": "BLAKE3", - "rev": "df610ddc3b93841ffc59a87e3da659a15910eb46", + "rev": "8b829b697fa4cfe35de35e9aa8c20b56266cb091", "type": "github" }, "original": { "owner": "BLAKE3-team", - "ref": "refs/tags/1.8.2", + "ref": "refs/tags/1.8.3", "repo": "BLAKE3", "type": "github" } @@ -31,26 +31,23 @@ ] }, "locked": { - "lastModified": 1768515341, - "narHash": "sha256-r98AAunFEidRoXFWTb8kJkjch9nSEcq95w1ZADJm9Dk=", - "owner": "argumentcomputer", - "repo": "Blake3.lean", - "rev": "f66794edb4612106cd7b04a7fbd04917fb1abb7d", - "type": "github" + "lastModified": 1771368498, + "narHash": "sha256-+nviIXVXexnqijW1hJlRiHiiTsdtuNZuRREkN0U6MCE=", + "path": "/home/sam/repos/argument/Blake3.lean", + "type": "path" }, "original": { - "owner": "argumentcomputer", - "repo": "Blake3.lean", - "type": "github" + "path": "/home/sam/repos/argument/Blake3.lean", + "type": "path" } }, "crane": { "locked": { - "lastModified": 1762538466, - "narHash": "sha256-8zrIPl6J+wLm9MH5ksHcW7BUHo7jSNOu0/hA0ohOOaM=", + "lastModified": 1771121070, + "narHash": "sha256-aIlv7FRXF9q70DNJPI237dEDAznSKaXmL5lfK/Id/bI=", "owner": "ipetkov", "repo": "crane", - "rev": "0cea393fffb39575c46b7a0318386467272182fe", + "rev": "a2812c19f1ed2e5ed5ce2ef7109798b575c180e1", "type": "github" }, "original": { @@ -68,11 +65,11 @@ "rust-analyzer-src": "rust-analyzer-src" }, "locked": { - "lastModified": 1763016383, - "narHash": "sha256-eYmo7FNvm3q08iROzwIi8i9dWuUbJJl3uLR3OLnSmdI=", + "lastModified": 1771312404, + "narHash": "sha256-eJ1YY3a+uQTfa1T3LsR2JX7n3F9vAKAwsuX/3Aecve0=", "owner": "nix-community", "repo": "fenix", - "rev": "0fad5c0e5c531358e7174cd666af4608f08bc3ba", + "rev": "b9696f35e4413cbd2873e4ac0252cd444f772772", "type": "github" }, "original": { @@ -86,11 +83,11 @@ "nixpkgs-lib": "nixpkgs-lib" }, "locked": { - "lastModified": 1768135262, - "narHash": "sha256-PVvu7OqHBGWN16zSi6tEmPwwHQ4rLPU9Plvs8/1TUBY=", + "lastModified": 1769996383, + "narHash": "sha256-AnYjnFWgS49RlqX7LrC4uA+sCCDBj0Ry/WOJ5XWAsa0=", "owner": "hercules-ci", "repo": "flake-parts", - "rev": "80daad04eddbbf5a4d883996a73f3f542fa437ac", + "rev": "57928607ea566b5db3ad13af0e57e921e6b12381", "type": "github" }, "original": { @@ -104,11 +101,11 @@ "nixpkgs-lib": "nixpkgs-lib_2" }, "locked": { - "lastModified": 1762980239, - "narHash": "sha256-8oNVE8TrD19ulHinjaqONf9QWCKK+w4url56cdStMpM=", + "lastModified": 1769996383, + "narHash": "sha256-AnYjnFWgS49RlqX7LrC4uA+sCCDBj0Ry/WOJ5XWAsa0=", "owner": "hercules-ci", "repo": "flake-parts", - "rev": "52a2caecc898d0b46b2b905f058ccc5081f842da", + "rev": "57928607ea566b5db3ad13af0e57e921e6b12381", "type": "github" }, "original": { @@ -141,17 +138,14 @@ "nixpkgs": "nixpkgs" }, "locked": { - "lastModified": 1768025957, - "narHash": "sha256-o9AUUOBq1SKEPGiwjBIP628N9fPNwAjqSm9xXhVEDNY=", - "owner": "lenianiva", - "repo": "lean4-nix", - "rev": "ecaa70749083e6a0e6e0814c6a66b7561754b6db", - "type": "github" + "lastModified": 1771368440, + "narHash": "sha256-xx4lS7oUoUNvIWxPOXwxGoR5N2xMt1tOU+9ePp9L7GQ=", + "path": "/home/sam/repos/argument/lean4-nix", + "type": "path" }, "original": { - "owner": "lenianiva", - "repo": "lean4-nix", - "type": "github" + "path": "/home/sam/repos/argument/lean4-nix", + "type": "path" } }, "nixpkgs": { @@ -172,11 +166,11 @@ }, "nixpkgs-lib": { "locked": { - "lastModified": 1765674936, - "narHash": "sha256-k00uTP4JNfmejrCLJOwdObYC9jHRrr/5M/a/8L2EIdo=", + "lastModified": 1769909678, + "narHash": "sha256-cBEymOf4/o3FD5AZnzC3J9hLbiZ+QDT/KDuyHXVJOpM=", "owner": "nix-community", "repo": "nixpkgs.lib", - "rev": "2075416fcb47225d9b68ac469a5c4801a9c4dd85", + "rev": "72716169fe93074c333e8d0173151350670b824c", "type": "github" }, "original": { @@ -187,11 +181,11 @@ }, "nixpkgs-lib_2": { "locked": { - "lastModified": 1761765539, - "narHash": "sha256-b0yj6kfvO8ApcSE+QmA6mUfu8IYG6/uU28OFn4PaC8M=", + "lastModified": 1769909678, + "narHash": "sha256-cBEymOf4/o3FD5AZnzC3J9hLbiZ+QDT/KDuyHXVJOpM=", "owner": "nix-community", "repo": "nixpkgs.lib", - "rev": "719359f4562934ae99f5443f20aa06c2ffff91fc", + "rev": "72716169fe93074c333e8d0173151350670b824c", "type": "github" }, "original": { @@ -231,11 +225,11 @@ "rust-analyzer-src": { "flake": false, "locked": { - "lastModified": 1762860488, - "narHash": "sha256-rMfWMCOo/pPefM2We0iMBLi2kLBAnYoB9thi4qS7uk4=", + "lastModified": 1771264911, + "narHash": "sha256-vDNZ6Y1M3DSa1JbPGgqtdJPl4rMzxebUK9hmZcopxX0=", "owner": "rust-lang", "repo": "rust-analyzer", - "rev": "2efc80078029894eec0699f62ec8d5c1a56af763", + "rev": "3360aebb35a099ff4a7bbd37e9a0dd44b8f23748", "type": "github" }, "original": { @@ -249,4 +243,3 @@ "root": "root", "version": 7 } - diff --git a/flake.nix b/flake.nix index a51fc428..6c1877c7 100644 --- a/flake.nix +++ b/flake.nix @@ -15,7 +15,8 @@ nixpkgs.follows = "lean4-nix/nixpkgs"; # Lean 4 & Lake - lean4-nix.url = "github:lenianiva/lean4-nix"; + #lean4-nix.url = "github:lenianiva/lean4-nix?rev=561f1a779737e109d4e03a6f967108497bbbd73f"; + lean4-nix.url = "path:/home/sam/repos/argument/lean4-nix"; # Helper: flake-parts for easier outputs flake-parts.url = "github:hercules-ci/flake-parts"; @@ -31,7 +32,8 @@ # Blake3 C bindings for Lean blake3-lean = { - url = "github:argumentcomputer/Blake3.lean"; + #url = "github:argumentcomputer/Blake3.lean?ref=lean-v4.27.0"; + url = "path:/home/sam/repos/argument/Blake3.lean"; # System packages, follows lean4-nix so we stay in sync inputs.lean4-nix.follows = "lean4-nix"; }; diff --git a/lake-manifest.json b/lake-manifest.json index c836ec33..d1cfefea 100644 --- a/lake-manifest.json +++ b/lake-manifest.json @@ -5,40 +5,40 @@ "type": "git", "subDir": null, "scope": "", - "rev": "24241822ef9d3e7f6a3bcc53ad136e12663db8f3", + "rev": "b25b36a7caf8e237e7d1e6121543078a06777c8a", "name": "batteries", "manifestFile": "lake-manifest.json", - "inputRev": "v4.26.0", + "inputRev": "v4.27.0", "inherited": false, "configFile": "lakefile.toml"}, {"url": "https://github.com/leanprover/lean4-cli", "type": "git", "subDir": null, "scope": "", - "rev": "933fce7e893f65969714c60cdb4bd8376786044e", + "rev": "55c37290ff6186e2e965d68cf853a57c0702db82", "name": "Cli", "manifestFile": "lake-manifest.json", - "inputRev": "v4.26.0", + "inputRev": "v4.27.0", "inherited": false, "configFile": "lakefile.toml"}, {"url": "https://github.com/argumentcomputer/Blake3.lean", "type": "git", "subDir": null, "scope": "", - "rev": "f66794edb4612106cd7b04a7fbd04917fb1abb7d", + "rev": "62ec6c8cea811907433a401136fe822ae6516292", "name": "Blake3", "manifestFile": "lake-manifest.json", - "inputRev": "f66794edb4612106cd7b04a7fbd04917fb1abb7d", + "inputRev": "lean-v4.27.0", "inherited": false, "configFile": "lakefile.lean"}, {"url": "https://github.com/argumentcomputer/LSpec", "type": "git", "subDir": null, "scope": "", - "rev": "1e6da63a9c92473747e816d07d5c6f6bc7c8a59e", + "rev": "4ce8259e303e7b8c287ca66c65587bf823da6a79", "name": "LSpec", "manifestFile": "lake-manifest.json", - "inputRev": "1e6da63a9c92473747e816d07d5c6f6bc7c8a59e", + "inputRev": "lean-v4.27.0", "inherited": false, "configFile": "lakefile.toml"}], "name": "ix", diff --git a/lakefile.lean b/lakefile.lean index ada02900..a0d35bd7 100644 --- a/lakefile.lean +++ b/lakefile.lean @@ -12,16 +12,16 @@ lean_exe ix where supportInterpreter := true require LSpec from git - "https://github.com/argumentcomputer/LSpec" @ "1e6da63a9c92473747e816d07d5c6f6bc7c8a59e" + "https://github.com/argumentcomputer/LSpec" @ "lean-v4.27.0" require Blake3 from git - "https://github.com/argumentcomputer/Blake3.lean" @ "f66794edb4612106cd7b04a7fbd04917fb1abb7d" + "https://github.com/argumentcomputer/Blake3.lean" @ "lean-v4.27.0" require Cli from git - "https://github.com/leanprover/lean4-cli" @ "v4.26.0" + "https://github.com/leanprover/lean4-cli" @ "v4.27.0" require batteries from git - "https://github.com/leanprover-community/batteries" @ "v4.26.0" + "https://github.com/leanprover-community/batteries" @ "v4.27.0" section Tests @@ -133,11 +133,11 @@ script install := do | some homeDir => let binDir : FilePath := homeDir / ".local" / "bin" print s!"Target directory for the ix binary? (default={binDir}) " - let input := (← (← getStdin).getLine).trim + let input := (← (← getStdin).getLine).trimAscii.toString pure $ if input.isEmpty then binDir else ⟨input⟩ | none => print s!"Target directory for the ix binary? " - let input := (← (← getStdin).getLine).trim + let input := (← (← getStdin).getLine).trimAscii.toString if input.isEmpty then eprintln "Target directory can't be empty."; return 1 pure ⟨input⟩ @@ -175,7 +175,7 @@ script "get-exe-targets" := do let pkg ← getRootPackage let exeTargets := pkg.configTargets LeanExe.configKind for tgt in exeTargets do - IO.println <| tgt.name.toString |>.stripPrefix "«" |>.stripSuffix "»" + IO.println <| tgt.name.toString |>.dropPrefix "«" |>.dropSuffix "»" |>.toString return 0 script "build-all" := do diff --git a/lean-toolchain b/lean-toolchain index e59446d5..5249182c 100644 --- a/lean-toolchain +++ b/lean-toolchain @@ -1 +1 @@ -leanprover/lean4:v4.26.0 +leanprover/lean4:v4.27.0 From 6f369b220c3b527e9f4618605985a7d67581cd8e Mon Sep 17 00:00:00 2001 From: samuelburnham <45365069+samuelburnham@users.noreply.github.com> Date: Fri, 20 Feb 2026 11:53:28 -0500 Subject: [PATCH 2/8] Cleanup --- flake.lock | 32 ++++++++++++++++++++------------ flake.nix | 6 ++---- lake-manifest.json | 6 +++--- lakefile.lean | 2 +- 4 files changed, 26 insertions(+), 20 deletions(-) diff --git a/flake.lock b/flake.lock index 0490bc41..ddaf0b7a 100644 --- a/flake.lock +++ b/flake.lock @@ -31,14 +31,18 @@ ] }, "locked": { - "lastModified": 1771368498, - "narHash": "sha256-+nviIXVXexnqijW1hJlRiHiiTsdtuNZuRREkN0U6MCE=", - "path": "/home/sam/repos/argument/Blake3.lean", - "type": "path" + "lastModified": 1771606207, + "narHash": "sha256-npGCsTdLRNw6xvaPkzy1Ul/IimiPiz9o+v9OoLwqaOk=", + "owner": "argumentcomputer", + "repo": "Blake3.lean", + "rev": "d886ce88c55eb210ff664c38f8c8782f1156b0b2", + "type": "github" }, "original": { - "path": "/home/sam/repos/argument/Blake3.lean", - "type": "path" + "owner": "argumentcomputer", + "ref": "lean-v4.27.0", + "repo": "Blake3.lean", + "type": "github" } }, "crane": { @@ -138,14 +142,18 @@ "nixpkgs": "nixpkgs" }, "locked": { - "lastModified": 1771368440, - "narHash": "sha256-xx4lS7oUoUNvIWxPOXwxGoR5N2xMt1tOU+9ePp9L7GQ=", - "path": "/home/sam/repos/argument/lean4-nix", - "type": "path" + "lastModified": 1771604035, + "narHash": "sha256-35kZxaGTpP0mGHaxKzb7WXQD2hkw5z/kGxIJ/bE+7cA=", + "owner": "argumentcomputer", + "repo": "lean4-nix", + "rev": "6ba23dd08cfcdf92c4e2aaae7952088a739d3bca", + "type": "github" }, "original": { - "path": "/home/sam/repos/argument/lean4-nix", - "type": "path" + "owner": "argumentcomputer", + "ref": "lake-config", + "repo": "lean4-nix", + "type": "github" } }, "nixpkgs": { diff --git a/flake.nix b/flake.nix index 6c1877c7..c7e9a80d 100644 --- a/flake.nix +++ b/flake.nix @@ -15,8 +15,7 @@ nixpkgs.follows = "lean4-nix/nixpkgs"; # Lean 4 & Lake - #lean4-nix.url = "github:lenianiva/lean4-nix?rev=561f1a779737e109d4e03a6f967108497bbbd73f"; - lean4-nix.url = "path:/home/sam/repos/argument/lean4-nix"; + lean4-nix.url = "github:argumentcomputer/lean4-nix?ref=lake-config"; # Helper: flake-parts for easier outputs flake-parts.url = "github:hercules-ci/flake-parts"; @@ -32,8 +31,7 @@ # Blake3 C bindings for Lean blake3-lean = { - #url = "github:argumentcomputer/Blake3.lean?ref=lean-v4.27.0"; - url = "path:/home/sam/repos/argument/Blake3.lean"; + url = "github:argumentcomputer/Blake3.lean?ref=lean-v4.27.0"; # System packages, follows lean4-nix so we stay in sync inputs.lean4-nix.follows = "lean4-nix"; }; diff --git a/lake-manifest.json b/lake-manifest.json index d1cfefea..d2687705 100644 --- a/lake-manifest.json +++ b/lake-manifest.json @@ -25,7 +25,7 @@ "type": "git", "subDir": null, "scope": "", - "rev": "62ec6c8cea811907433a401136fe822ae6516292", + "rev": "d886ce88c55eb210ff664c38f8c8782f1156b0b2", "name": "Blake3", "manifestFile": "lake-manifest.json", "inputRev": "lean-v4.27.0", @@ -35,10 +35,10 @@ "type": "git", "subDir": null, "scope": "", - "rev": "4ce8259e303e7b8c287ca66c65587bf823da6a79", + "rev": "7f5bb9de3aab89c2c24a1c917b17d9b75e6f220e", "name": "LSpec", "manifestFile": "lake-manifest.json", - "inputRev": "lean-v4.27.0", + "inputRev": "7f5bb9de3aab89c2c24a1c917b17d9b75e6f220e", "inherited": false, "configFile": "lakefile.toml"}], "name": "ix", diff --git a/lakefile.lean b/lakefile.lean index a0d35bd7..19b10f3e 100644 --- a/lakefile.lean +++ b/lakefile.lean @@ -12,7 +12,7 @@ lean_exe ix where supportInterpreter := true require LSpec from git - "https://github.com/argumentcomputer/LSpec" @ "lean-v4.27.0" + "https://github.com/argumentcomputer/LSpec" @ "7f5bb9de3aab89c2c24a1c917b17d9b75e6f220e" require Blake3 from git "https://github.com/argumentcomputer/Blake3.lean" @ "lean-v4.27.0" From 188859df9cf681831dc90e1b6672e56ee1c2bb10 Mon Sep 17 00:00:00 2001 From: samuelburnham <45365069+samuelburnham@users.noreply.github.com> Date: Mon, 23 Feb 2026 09:27:25 -0500 Subject: [PATCH 3/8] Update lean4-nix --- .github/workflows/nix.yml | 4 ---- flake.lock | 16 +++++++--------- flake.nix | 11 ++--------- lake-manifest.json | 4 ++-- lakefile.lean | 8 ++++---- 5 files changed, 15 insertions(+), 28 deletions(-) diff --git a/.github/workflows/nix.yml b/.github/workflows/nix.yml index 2f87c928..9be2f5e4 100644 --- a/.github/workflows/nix.yml +++ b/.github/workflows/nix.yml @@ -27,10 +27,6 @@ jobs: # Ix CLI - run: nix build --print-build-logs --accept-flake-config - run: nix run .#ix -- --help - # Ix benches - - run: nix build .#bench-aiur --print-build-logs --accept-flake-config - - run: nix build .#bench-blake3 --print-build-logs --accept-flake-config - - run: nix build .#bench-shardmap --print-build-logs --accept-flake-config # Ix tests - run: nix run .#test --accept-flake-config # Expensive tests are only built in Nix to save time diff --git a/flake.lock b/flake.lock index ddaf0b7a..d4ab2b13 100644 --- a/flake.lock +++ b/flake.lock @@ -31,16 +31,15 @@ ] }, "locked": { - "lastModified": 1771606207, - "narHash": "sha256-npGCsTdLRNw6xvaPkzy1Ul/IimiPiz9o+v9OoLwqaOk=", + "lastModified": 1771855602, + "narHash": "sha256-kF96mxMjZLZIMZhcO3DtpUbHLLGgOgpZgrFFEGxlXRY=", "owner": "argumentcomputer", "repo": "Blake3.lean", - "rev": "d886ce88c55eb210ff664c38f8c8782f1156b0b2", + "rev": "686c397ae8a540b25bf6b18bbd4fb9f6cf0459e8", "type": "github" }, "original": { "owner": "argumentcomputer", - "ref": "lean-v4.27.0", "repo": "Blake3.lean", "type": "github" } @@ -142,16 +141,15 @@ "nixpkgs": "nixpkgs" }, "locked": { - "lastModified": 1771604035, + "lastModified": 1771784682, "narHash": "sha256-35kZxaGTpP0mGHaxKzb7WXQD2hkw5z/kGxIJ/bE+7cA=", - "owner": "argumentcomputer", + "owner": "lenianiva", "repo": "lean4-nix", - "rev": "6ba23dd08cfcdf92c4e2aaae7952088a739d3bca", + "rev": "7a5424eb7cfad9c855cd31d958d84b2209549bbf", "type": "github" }, "original": { - "owner": "argumentcomputer", - "ref": "lake-config", + "owner": "lenianiva", "repo": "lean4-nix", "type": "github" } diff --git a/flake.nix b/flake.nix index c7e9a80d..4af41012 100644 --- a/flake.nix +++ b/flake.nix @@ -15,7 +15,7 @@ nixpkgs.follows = "lean4-nix/nixpkgs"; # Lean 4 & Lake - lean4-nix.url = "github:argumentcomputer/lean4-nix?ref=lake-config"; + lean4-nix.url = "github:lenianiva/lean4-nix"; # Helper: flake-parts for easier outputs flake-parts.url = "github:hercules-ci/flake-parts"; @@ -31,7 +31,7 @@ # Blake3 C bindings for Lean blake3-lean = { - url = "github:argumentcomputer/Blake3.lean?ref=lean-v4.27.0"; + url = "github:argumentcomputer/Blake3.lean"; # System packages, follows lean4-nix so we stay in sync inputs.lean4-nix.follows = "lean4-nix"; }; @@ -126,9 +126,6 @@ testAiur = lake2nix.mkPackage (lakeBinArgs // {name = "test-aiur";}); testAiurHashes = lake2nix.mkPackage (lakeBinArgs // {name = "test-aiur-hashes";}); testIxVM = lake2nix.mkPackage (lakeBinArgs // {name = "test-ixvm";}); - benchAiur = lake2nix.mkPackage (lakeBinArgs // {name = "bench-aiur";}); - benchBlake3 = lake2nix.mkPackage (lakeBinArgs // {name = "bench-blake3";}); - benchShardMap = lake2nix.mkPackage (lakeBinArgs // {name = "bench-shardmap";}); in { # Lean overlay _module.args.pkgs = import nixpkgs { @@ -143,10 +140,6 @@ test-aiur = testAiur; test-aiur-hashes = testAiurHashes; test-ixvm = testIxVM; - # Ix benches - bench-aiur = benchAiur; - bench-blake3 = benchBlake3; - bench-shardmap = benchShardMap; }; # Provide a unified dev shell with Lean + Rust diff --git a/lake-manifest.json b/lake-manifest.json index d2687705..2c413d0a 100644 --- a/lake-manifest.json +++ b/lake-manifest.json @@ -25,10 +25,10 @@ "type": "git", "subDir": null, "scope": "", - "rev": "d886ce88c55eb210ff664c38f8c8782f1156b0b2", + "rev": "686c397ae8a540b25bf6b18bbd4fb9f6cf0459e8", "name": "Blake3", "manifestFile": "lake-manifest.json", - "inputRev": "lean-v4.27.0", + "inputRev": "686c397ae8a540b25bf6b18bbd4fb9f6cf0459e8", "inherited": false, "configFile": "lakefile.lean"}, {"url": "https://github.com/argumentcomputer/LSpec", diff --git a/lakefile.lean b/lakefile.lean index 19b10f3e..e8e03ee4 100644 --- a/lakefile.lean +++ b/lakefile.lean @@ -15,7 +15,7 @@ require LSpec from git "https://github.com/argumentcomputer/LSpec" @ "7f5bb9de3aab89c2c24a1c917b17d9b75e6f220e" require Blake3 from git - "https://github.com/argumentcomputer/Blake3.lean" @ "lean-v4.27.0" + "https://github.com/argumentcomputer/Blake3.lean" @ "686c397ae8a540b25bf6b18bbd4fb9f6cf0459e8" require Cli from git "https://github.com/leanprover/lean4-cli" @ "v4.27.0" @@ -43,8 +43,6 @@ lean_exe «test-ixvm» where end Tests -section IxApplications - section Benchmarks lean_exe «bench-aiur» where @@ -61,6 +59,8 @@ lean_exe «bench-shardmap» where end Benchmarks +section IxApplications + lean_lib Apps lean_exe Apps.ZKVoting.Prover where @@ -155,7 +155,7 @@ script install := do return 0 script "check-lean-h-hash" := do - let cachedLeanHHash := 11261383907494897568 + let cachedLeanHHash := 11953097959587138033 let leanIncludeDir ← getLeanIncludeDir let includedLeanHPath := leanIncludeDir / "lean" / "lean.h" From 72f52322085e56a525c6701cb1c622802fc02b7a Mon Sep 17 00:00:00 2001 From: samuelburnham <45365069+samuelburnham@users.noreply.github.com> Date: Mon, 23 Feb 2026 09:43:59 -0500 Subject: [PATCH 4/8] Remove expensive tests from default suite --- Tests/Main.lean | 6 ------ 1 file changed, 6 deletions(-) diff --git a/Tests/Main.lean b/Tests/Main.lean index 4b2d4e52..e25300a8 100644 --- a/Tests/Main.lean +++ b/Tests/Main.lean @@ -1,6 +1,3 @@ -import Tests.Aiur -import Tests.AiurHashes -import Tests.IxVM import Tests.ByteArray import Tests.Ix.Ixon import Tests.Ix.Claim @@ -25,9 +22,6 @@ opaque tmpDecodeConstMap : @& List (Lean.Name × Lean.ConstantInfo) → USize /-- Primary test suites - run by default -/ def primarySuites : Std.HashMap String (List LSpec.TestSeq) := .ofList [ - ("aiur", Tests.Aiur.suite), - ("aiur-hashes", Tests.AiurHashes.suite), - ("ixvm", Tests.IxVM.suite), ("ffi", Tests.FFI.suite), ("byte-array", Tests.ByteArray.suite), ("ixon", Tests.Ixon.suite), From 8df854a1a06b3fc584b68254dba4e208c98b6aae Mon Sep 17 00:00:00 2001 From: samuelburnham <45365069+samuelburnham@users.noreply.github.com> Date: Mon, 23 Feb 2026 13:49:30 -0500 Subject: [PATCH 5/8] Refactor Aiur tests into subdir --- Tests.lean | 2 - Tests/Aiur.lean | 274 +------------------ Tests/Aiur/Aiur.lean | 276 ++++++++++++++++++++ Tests/Aiur/Common.lean | 72 +++++ Tests/{AiurHashes.lean => Aiur/Hashes.lean} | 22 +- Tests/{IxVMMain.lean => Aiur/IxVM.lean} | 7 +- Tests/AiurHashesMain.lean | 4 - Tests/AiurMain.lean | 4 - Tests/Cli.lean | 3 +- Tests/Common.lean | 57 ---- Tests/IxVM.lean | 6 - lakefile.lean | 6 +- 12 files changed, 374 insertions(+), 359 deletions(-) create mode 100644 Tests/Aiur/Aiur.lean create mode 100644 Tests/Aiur/Common.lean rename Tests/{AiurHashes.lean => Aiur/Hashes.lean} (70%) rename Tests/{IxVMMain.lean => Aiur/IxVM.lean} (53%) delete mode 100644 Tests/AiurHashesMain.lean delete mode 100644 Tests/AiurMain.lean delete mode 100644 Tests/Common.lean delete mode 100644 Tests/IxVM.lean diff --git a/Tests.lean b/Tests.lean index 3378820d..22932177 100644 --- a/Tests.lean +++ b/Tests.lean @@ -1,5 +1,4 @@ import Tests.Aiur -import Tests.AiurHashes import Tests.ByteArray import Tests.Ix.Ixon import Tests.Ix.Claim @@ -16,4 +15,3 @@ import Tests.FFI import Tests.Keccak import Tests.Cli import Tests.ShardMap -import Tests.Common diff --git a/Tests/Aiur.lean b/Tests/Aiur.lean index 130cba67..0f5c56d1 100644 --- a/Tests/Aiur.lean +++ b/Tests/Aiur.lean @@ -1,273 +1 @@ -import Tests.Common -import Ix.Aiur.Meta - -open LSpec - -def toplevel := ⟦ - fn id(n: G) -> G { - n - } - - fn proj1(a: G, _b: G) -> G { - a - } - - fn sum(x: G, y: G) -> G { - x + y - } - - fn prod(x: G, y: G) -> G { - x * y - } - - fn match_mul(x: G) -> G { - match x { - 0 => 0, - _ => x * x * x, - } - } - - fn sum_prod(x: G, y: G, z: G) -> G { - (x + y) * z - } - - fn eq_zero_dummy(a: G, b: G) -> [G; 4] { - let c = 0; - let d = 101; - [eq_zero(a), eq_zero(b), eq_zero(c), eq_zero(d)] - } - - fn store_and_load(x: G) -> G { - load(store(x)) - } - - enum Nat { - Zero, - Succ(&Nat) - } - - -- fn cast_zero() -> (G, G) { - -- cast(Nat.Zero, (G, G)) - -- } - - fn pointer_match() -> G { - let two = Nat.Succ(store(Nat.Succ(store(Nat.Zero)))); - match two { - Nat.Succ(&Nat.Succ(&Nat.Zero)) => 1, - _ => 0, - } - } - - fn even(m: Nat) -> G { - match m { - Nat.Zero => 1, - Nat.Succ(m) => odd(load(m)), - } - } - - fn odd(m: Nat) -> G { - match m { - Nat.Zero => 0, - Nat.Succ(m) => even(load(m)), - } - } - - fn is_0_even() -> G { - even(Nat.Zero) - } - - fn is_1_even() -> G { - even(Nat.Succ(store(Nat.Zero))) - } - - fn is_2_even() -> G { - even(Nat.Succ(store(Nat.Succ(store(Nat.Zero))))) - } - - fn is_3_even() -> G { - even(Nat.Succ(store(Nat.Succ(store(Nat.Succ(store(Nat.Zero))))))) - } - - fn is_4_even() -> G { - even(Nat.Succ(store(Nat.Succ(store(Nat.Succ(store(Nat.Succ(store(Nat.Zero))))))))) - } - - fn is_0_odd() -> G { - odd(Nat.Zero) - } - - fn is_1_odd() -> G { - odd(Nat.Succ(store(Nat.Zero))) - } - - fn is_2_odd() -> G { - odd(Nat.Succ(store(Nat.Succ(store(Nat.Zero))))) - } - - fn is_3_odd() -> G { - odd(Nat.Succ(store(Nat.Succ(store(Nat.Succ(store(Nat.Zero))))))) - } - - fn is_4_odd() -> G { - odd(Nat.Succ(store(Nat.Succ(store(Nat.Succ(store(Nat.Succ(store(Nat.Zero))))))))) - } - - fn factorial(n: G) -> G { - match n { - 0 => 1, - _ => n * factorial(n - 1), - } - } - - fn fibonacci(n: G) -> G { - match n { - 0 => 1, - _ => - let n_minus_1 = n - 1; - match n_minus_1 { - 0 => 1, - _ => - let n_minus_2 = n_minus_1 - 1; - fibonacci(n_minus_1) + fibonacci(n_minus_2), - }, - } - } - - #[unconstrained] - fn unconstrained_fibonacci(n: G) -> G { - match n { - 0 => 1, - _ => - let n_minus_1 = n - 1; - match n_minus_1 { - 0 => 1, - _ => - let n_minus_2 = n_minus_1 - 1; - fibonacci(n_minus_1) + unconstrained_fibonacci(n_minus_2), - }, - } - } - - fn unconstrained_fibonacci_entrypoint(n: G) -> G { - unconstrained_fibonacci(n) - } - - fn projections(as: (G, G, G, G, G)) -> (G, G) { - (proj(as, 1), proj(as, 3)) - } - - fn slice_and_get(as: [G; 5]) -> [G; 2] { - let left = as[0 .. 2]; - let right = as[3 .. 5]; - [left[1], right[0]] - } - - fn deconstruct_tuple(as: (G, G, G, G, G)) -> (G, G) { - let (_, b, _, d, _) = as; - (b, d) - } - - fn deconstruct_array(as: [G; 5]) -> [G; 2] { - let [_, b, _, d, _] = as; - [b, d] - } - - fn array_set(arr: [(G, G); 3]) -> [(G, G); 3] { - set(arr, 1, (0, 0)) - } - - fn assert_eq_trivial() { - assert_eq!([1, 2, 3], [1, 2, 3]); - } - - fn read_write_io() { - let (idx, len) = io_get_info([0]); - let xs: [G; 4] = io_read(idx, 4); - io_write(xs); - io_set_info([1], idx, len + 4); - } - - fn shr_shr_shl_decompose(byte: G) -> [G; 8] { - let byte_shr = u8_shift_right(byte); - let byte_shr_shr = u8_shift_right(byte_shr); - let byte_shr_shr_shl = u8_shift_left(byte_shr_shr); - u8_bit_decomposition(byte_shr_shr_shl) - } - - fn u8_add_xor(i: G, j: G) -> ((G, G), (G, G)) { - let i_xor_j = u8_xor(i, j); - (u8_add(i_xor_j, i), u8_add(i_xor_j, j)) - } - - fn u8_sub_function(i: G, j: G) -> (G, G) { - u8_sub(i, j) - } - - fn u8_less_than_function(i: G, j: G) -> G { - u8_less_than(i, j) - } - - fn u8_and_function(i: G, j: G) -> G { - u8_and(i, j) - } - - fn u8_or_function(i: G, j: G) -> G { - u8_or(i, j) - } - - fn fold_matrix_sum(m: [[G; 2]; 2]) -> G { - fold(0 .. 2, 0, |acc_outer, @i| - fold(0 .. 2, acc_outer, |acc_inner, @j| - acc_inner + m[@i][@j] - ) - ) - } -⟧ - -def aiurTestCases : List AiurTestCase := [ - .noIO `id #[42] #[42], - .noIO `proj1 #[42, 64] #[42], - .noIO `sum #[3, 5] #[8], - .noIO `prod #[3, 5] #[15], - .noIO `match_mul #[2] #[8], - .noIO `sum_prod #[2, 3, 4] #[20], - .noIO `eq_zero_dummy #[0, 37] #[1, 0, 1, 0], - .noIO `store_and_load #[42] #[42], - -- .noIO `cast_zero #[] #[0, 0], - .noIO `pointer_match #[] #[1], - .noIO `is_0_even #[] #[1], - .noIO `is_1_even #[] #[0], - .noIO `is_2_even #[] #[1], - .noIO `is_3_even #[] #[0], - .noIO `is_4_even #[] #[1], - .noIO `is_0_odd #[] #[0], - .noIO `is_1_odd #[] #[1], - .noIO `is_2_odd #[] #[0], - .noIO `is_3_odd #[] #[1], - .noIO `is_4_odd #[] #[0], - .noIO `factorial #[5] #[120], - .noIO `fibonacci #[0] #[1], - .noIO `fibonacci #[1] #[1], - .noIO `fibonacci #[6] #[13], - .noIO `unconstrained_fibonacci_entrypoint #[6] #[13], - .noIO `projections #[1, 2, 3, 4, 5] #[2, 4], - .noIO `slice_and_get #[1, 2, 3, 4, 5] #[2, 4], - .noIO `deconstruct_tuple #[1, 2, 3, 4, 5] #[2, 4], - .noIO `deconstruct_array #[1, 2, 3, 4, 5] #[2, 4], - .noIO `array_set #[1, 1, 2, 2, 3, 3] #[1, 1, 0, 0, 3, 3], - .noIO `assert_eq_trivial #[] #[], - ⟨`read_write_io, #[], #[], - ⟨#[1, 2, 3, 4], .ofList [(#[0], ⟨0, 4⟩)]⟩, - ⟨#[1, 2, 3, 4, 1, 2, 3, 4], .ofList [(#[0], ⟨0, 4⟩), (#[1], ⟨0, 8⟩)]⟩⟩, - .noIO `shr_shr_shl_decompose #[87] #[0, 1, 0, 1, 0, 1, 0, 0], - .noIO `u8_add_xor #[45, 131] #[219, 0, 49, 1], - .noIO `u8_sub_function #[45, 131] #[170, 1], - .noIO `u8_less_than_function #[45, 131] #[1], - .noIO `u8_and_function #[45, 131] #[1], - .noIO `u8_or_function #[45, 131] #[175], - .noIO `fold_matrix_sum #[1, 2, 3, 4] #[10], - ] - -def Tests.Aiur.suite := [ - mkAiurTests (pure toplevel) aiurTestCases -] +import Tests.Aiur.Common diff --git a/Tests/Aiur/Aiur.lean b/Tests/Aiur/Aiur.lean new file mode 100644 index 00000000..ce1a1a5a --- /dev/null +++ b/Tests/Aiur/Aiur.lean @@ -0,0 +1,276 @@ +import Tests.Aiur.Common +import Ix.Aiur.Meta + +open LSpec + +def toplevel := ⟦ + fn id(n: G) -> G { + n + } + + fn proj1(a: G, _b: G) -> G { + a + } + + fn sum(x: G, y: G) -> G { + x + y + } + + fn prod(x: G, y: G) -> G { + x * y + } + + fn match_mul(x: G) -> G { + match x { + 0 => 0, + _ => x * x * x, + } + } + + fn sum_prod(x: G, y: G, z: G) -> G { + (x + y) * z + } + + fn eq_zero_dummy(a: G, b: G) -> [G; 4] { + let c = 0; + let d = 101; + [eq_zero(a), eq_zero(b), eq_zero(c), eq_zero(d)] + } + + fn store_and_load(x: G) -> G { + load(store(x)) + } + + enum Nat { + Zero, + Succ(&Nat) + } + + -- fn cast_zero() -> (G, G) { + -- cast(Nat.Zero, (G, G)) + -- } + + fn pointer_match() -> G { + let two = Nat.Succ(store(Nat.Succ(store(Nat.Zero)))); + match two { + Nat.Succ(&Nat.Succ(&Nat.Zero)) => 1, + _ => 0, + } + } + + fn even(m: Nat) -> G { + match m { + Nat.Zero => 1, + Nat.Succ(m) => odd(load(m)), + } + } + + fn odd(m: Nat) -> G { + match m { + Nat.Zero => 0, + Nat.Succ(m) => even(load(m)), + } + } + + fn is_0_even() -> G { + even(Nat.Zero) + } + + fn is_1_even() -> G { + even(Nat.Succ(store(Nat.Zero))) + } + + fn is_2_even() -> G { + even(Nat.Succ(store(Nat.Succ(store(Nat.Zero))))) + } + + fn is_3_even() -> G { + even(Nat.Succ(store(Nat.Succ(store(Nat.Succ(store(Nat.Zero))))))) + } + + fn is_4_even() -> G { + even(Nat.Succ(store(Nat.Succ(store(Nat.Succ(store(Nat.Succ(store(Nat.Zero))))))))) + } + + fn is_0_odd() -> G { + odd(Nat.Zero) + } + + fn is_1_odd() -> G { + odd(Nat.Succ(store(Nat.Zero))) + } + + fn is_2_odd() -> G { + odd(Nat.Succ(store(Nat.Succ(store(Nat.Zero))))) + } + + fn is_3_odd() -> G { + odd(Nat.Succ(store(Nat.Succ(store(Nat.Succ(store(Nat.Zero))))))) + } + + fn is_4_odd() -> G { + odd(Nat.Succ(store(Nat.Succ(store(Nat.Succ(store(Nat.Succ(store(Nat.Zero))))))))) + } + + fn factorial(n: G) -> G { + match n { + 0 => 1, + _ => n * factorial(n - 1), + } + } + + fn fibonacci(n: G) -> G { + match n { + 0 => 1, + _ => + let n_minus_1 = n - 1; + match n_minus_1 { + 0 => 1, + _ => + let n_minus_2 = n_minus_1 - 1; + fibonacci(n_minus_1) + fibonacci(n_minus_2), + }, + } + } + + #[unconstrained] + fn unconstrained_fibonacci(n: G) -> G { + match n { + 0 => 1, + _ => + let n_minus_1 = n - 1; + match n_minus_1 { + 0 => 1, + _ => + let n_minus_2 = n_minus_1 - 1; + fibonacci(n_minus_1) + unconstrained_fibonacci(n_minus_2), + }, + } + } + + fn unconstrained_fibonacci_entrypoint(n: G) -> G { + unconstrained_fibonacci(n) + } + + fn projections(as: (G, G, G, G, G)) -> (G, G) { + (proj(as, 1), proj(as, 3)) + } + + fn slice_and_get(as: [G; 5]) -> [G; 2] { + let left = as[0 .. 2]; + let right = as[3 .. 5]; + [left[1], right[0]] + } + + fn deconstruct_tuple(as: (G, G, G, G, G)) -> (G, G) { + let (_, b, _, d, _) = as; + (b, d) + } + + fn deconstruct_array(as: [G; 5]) -> [G; 2] { + let [_, b, _, d, _] = as; + [b, d] + } + + fn array_set(arr: [(G, G); 3]) -> [(G, G); 3] { + set(arr, 1, (0, 0)) + } + + fn assert_eq_trivial() { + assert_eq!([1, 2, 3], [1, 2, 3]); + } + + fn read_write_io() { + let (idx, len) = io_get_info([0]); + let xs: [G; 4] = io_read(idx, 4); + io_write(xs); + io_set_info([1], idx, len + 4); + } + + fn shr_shr_shl_decompose(byte: G) -> [G; 8] { + let byte_shr = u8_shift_right(byte); + let byte_shr_shr = u8_shift_right(byte_shr); + let byte_shr_shr_shl = u8_shift_left(byte_shr_shr); + u8_bit_decomposition(byte_shr_shr_shl) + } + + fn u8_add_xor(i: G, j: G) -> ((G, G), (G, G)) { + let i_xor_j = u8_xor(i, j); + (u8_add(i_xor_j, i), u8_add(i_xor_j, j)) + } + + fn u8_sub_function(i: G, j: G) -> (G, G) { + u8_sub(i, j) + } + + fn u8_less_than_function(i: G, j: G) -> G { + u8_less_than(i, j) + } + + fn u8_and_function(i: G, j: G) -> G { + u8_and(i, j) + } + + fn u8_or_function(i: G, j: G) -> G { + u8_or(i, j) + } + + fn fold_matrix_sum(m: [[G; 2]; 2]) -> G { + fold(0 .. 2, 0, |acc_outer, @i| + fold(0 .. 2, acc_outer, |acc_inner, @j| + acc_inner + m[@i][@j] + ) + ) + } +⟧ + +def aiurTestCases : List AiurTestCase := [ + .noIO `id #[42] #[42], + .noIO `proj1 #[42, 64] #[42], + .noIO `sum #[3, 5] #[8], + .noIO `prod #[3, 5] #[15], + .noIO `match_mul #[2] #[8], + .noIO `sum_prod #[2, 3, 4] #[20], + .noIO `eq_zero_dummy #[0, 37] #[1, 0, 1, 0], + .noIO `store_and_load #[42] #[42], + -- .noIO `cast_zero #[] #[0, 0], + .noIO `pointer_match #[] #[1], + .noIO `is_0_even #[] #[1], + .noIO `is_1_even #[] #[0], + .noIO `is_2_even #[] #[1], + .noIO `is_3_even #[] #[0], + .noIO `is_4_even #[] #[1], + .noIO `is_0_odd #[] #[0], + .noIO `is_1_odd #[] #[1], + .noIO `is_2_odd #[] #[0], + .noIO `is_3_odd #[] #[1], + .noIO `is_4_odd #[] #[0], + { AiurTestCase.noIO `factorial #[5] #[120] with label := "factorial(5)" }, + { AiurTestCase.noIO `fibonacci #[0] #[1] with label := "fibonacci(0)" }, + { AiurTestCase.noIO `fibonacci #[1] #[1] with label := "fibonacci(1)" }, + { AiurTestCase.noIO `fibonacci #[6] #[13] with label := "fibonacci(6)" }, + .noIO `unconstrained_fibonacci_entrypoint #[6] #[13], + .noIO `projections #[1, 2, 3, 4, 5] #[2, 4], + .noIO `slice_and_get #[1, 2, 3, 4, 5] #[2, 4], + .noIO `deconstruct_tuple #[1, 2, 3, 4, 5] #[2, 4], + .noIO `deconstruct_array #[1, 2, 3, 4, 5] #[2, 4], + .noIO `array_set #[1, 1, 2, 2, 3, 3] #[1, 1, 0, 0, 3, 3], + .noIO `assert_eq_trivial #[] #[], + ⟨`read_write_io, "read_write_io", #[], #[], + ⟨#[1, 2, 3, 4], .ofList [(#[0], ⟨0, 4⟩)]⟩, + ⟨#[1, 2, 3, 4, 1, 2, 3, 4], .ofList [(#[0], ⟨0, 4⟩), (#[1], ⟨0, 8⟩)]⟩⟩, + .noIO `shr_shr_shl_decompose #[87] #[0, 1, 0, 1, 0, 1, 0, 0], + .noIO `u8_add_xor #[45, 131] #[219, 0, 49, 1], + .noIO `u8_sub_function #[45, 131] #[170, 1], + .noIO `u8_less_than_function #[45, 131] #[1], + .noIO `u8_and_function #[45, 131] #[1], + .noIO `u8_or_function #[45, 131] #[175], + .noIO `fold_matrix_sum #[1, 2, 3, 4] #[10], + ] + +def main (_args : List String) : IO UInt32 := do + match AiurTestEnv.build (pure toplevel) with + | .error e => IO.eprintln s!"Setup failed: {e}"; return 1 + | .ok env => + lspecEachIO aiurTestCases fun testCase => + pure (env.runTestCase testCase) diff --git a/Tests/Aiur/Common.lean b/Tests/Aiur/Common.lean new file mode 100644 index 00000000..fb31675b --- /dev/null +++ b/Tests/Aiur/Common.lean @@ -0,0 +1,72 @@ +/- + Common Aiur test utilities. + Basic type generators have been moved to Tests/Gen/Basic.lean. +-/ + +import LSpec +import Tests.Gen.Basic +import Ix.Unsigned +import Ix.Aiur.Goldilocks +import Ix.Aiur.Protocol +import Ix.Aiur.Simple +import Ix.Aiur.Compile + +open LSpec SlimCheck Gen + +structure AiurTestCase where + functionName : Lean.Name + label : String + input : Array Aiur.G + expectedOutput : Array Aiur.G + inputIOBuffer: Aiur.IOBuffer + expectedIOBuffer: Aiur.IOBuffer + +def AiurTestCase.noIO (name : Lean.Name) := + (AiurTestCase.mk name (toString name) · · default default) + +def commitmentParameters : Aiur.CommitmentParameters := { + logBlowup := 1 +} + +def friParameters : Aiur.FriParameters := { + logFinalPolyLen := 0 + numQueries := 100 + commitProofOfWorkBits := 20 + queryProofOfWorkBits := 0 +} + +structure AiurTestEnv where + toplevel : Aiur.Toplevel + aiurSystem : Aiur.AiurSystem + +def AiurTestEnv.build (toplevelFn : Except Aiur.Global Aiur.Toplevel) : + Except String AiurTestEnv := do + let toplevel ← toplevelFn.mapError toString + let decls ← toplevel.checkAndSimplify.mapError toString + let bytecodeToplevel := decls.compile + let aiurSystem := Aiur.AiurSystem.build bytecodeToplevel commitmentParameters + return ⟨toplevel, aiurSystem⟩ + +def AiurTestEnv.runTestCase (env : AiurTestEnv) (testCase : AiurTestCase) : TestSeq := + let label := testCase.label + let funIdx := env.toplevel.getFuncIdx testCase.functionName |>.get! + let (claim, proof, ioBuffer) := env.aiurSystem.prove + friParameters funIdx testCase.input testCase.inputIOBuffer + let claimTest := test s!"Claim matches for {label}" + (claim == Aiur.buildClaim funIdx testCase.input testCase.expectedOutput) + let ioTest := test s!"IOBuffer matches for {label}" + (ioBuffer == testCase.expectedIOBuffer) + let proof := .ofBytes proof.toBytes + let pvTest := withExceptOk s!"Prove/verify works for {label}" + (env.aiurSystem.verify friParameters claim proof) fun _ => .done + claimTest ++ ioTest ++ pvTest + +def mkAiurTests (toplevelFn : Except Aiur.Global Aiur.Toplevel) + (cases : List AiurTestCase) : TestSeq := + withExceptOk "Toplevel merging succeeds" toplevelFn fun toplevel => + withExceptOk "Check and simplification succeed" toplevel.checkAndSimplify fun decls => + let bytecodeToplevel := decls.compile + let aiurSystem := Aiur.AiurSystem.build bytecodeToplevel commitmentParameters + let env : AiurTestEnv := ⟨toplevel, aiurSystem⟩ + cases.foldl (init := .done) fun tSeq testCase => + tSeq ++ env.runTestCase testCase diff --git a/Tests/AiurHashes.lean b/Tests/Aiur/Hashes.lean similarity index 70% rename from Tests/AiurHashes.lean rename to Tests/Aiur/Hashes.lean index d7df00bc..c826b484 100644 --- a/Tests/AiurHashes.lean +++ b/Tests/Aiur/Hashes.lean @@ -1,4 +1,4 @@ -import Tests.Common +import Tests.Aiur.Common import Ix.IxVM.ByteStream import Ix.IxVM.Blake3 import Ix.IxVM.Sha256 @@ -13,7 +13,7 @@ def mkBlake3HashTestCase (size : Nat) : AiurTestCase := let input := inputBytes.map .ofUInt8 let output := outputBytes.map .ofUInt8 let buffer := ⟨input, .ofList [(#[0], ⟨0, size⟩)]⟩ -- key is fixed as #[0] - ⟨`blake3_test, #[], output, buffer, buffer⟩ + ⟨`blake3_test, s!"blake3 (size={size})", #[], output, buffer, buffer⟩ def mkSha256HashTestCase (size : Nat) : AiurTestCase := let inputBytes := Array.range size |>.map Nat.toUInt8 @@ -21,7 +21,7 @@ def mkSha256HashTestCase (size : Nat) : AiurTestCase := let input := inputBytes.map .ofUInt8 let output := outputBytes.map .ofUInt8 let buffer := ⟨input, .ofList [(#[0], ⟨0, size⟩)]⟩ -- key is fixed as #[0] - ⟨`sha256_test, #[], output, buffer, buffer⟩ + ⟨`sha256_test, s!"sha256 (size={size})", #[], output, buffer, buffer⟩ def blake3TestCases : List AiurTestCase := [ mkBlake3HashTestCase 0, @@ -58,7 +58,15 @@ def sha256TestCases : List AiurTestCase := [ mkSha256HashTestCase 1200, ] -def Tests.AiurHashes.suite := [ - mkAiurTests (IxVM.byteStream.merge IxVM.blake3) blake3TestCases, - mkAiurTests (IxVM.byteStream.merge IxVM.sha256) sha256TestCases, -] +open LSpec + +def main (_args : List String) : IO UInt32 := do + let .ok blake3Env := AiurTestEnv.build (IxVM.byteStream.merge IxVM.blake3) + | IO.eprintln "Blake3 setup failed"; return 1 + let r1 ← lspecEachIO blake3TestCases fun testCase => + pure (blake3Env.runTestCase testCase) + let .ok sha256Env := AiurTestEnv.build (IxVM.byteStream.merge IxVM.sha256) + | IO.eprintln "SHA256 setup failed"; return 1 + let r2 ← lspecEachIO sha256TestCases fun testCase => + pure (sha256Env.runTestCase testCase) + return if r1 == 0 && r2 == 0 then 0 else 1 diff --git a/Tests/IxVMMain.lean b/Tests/Aiur/IxVM.lean similarity index 53% rename from Tests/IxVMMain.lean rename to Tests/Aiur/IxVM.lean index 5af85eed..b5e5c234 100644 --- a/Tests/IxVMMain.lean +++ b/Tests/Aiur/IxVM.lean @@ -1,4 +1,9 @@ -import Tests.IxVM +import Tests.Aiur.Common +import Ix.IxVM + +def Tests.IxVM.suite := [ + mkAiurTests IxVM.ixVM [] +] def main (args : List String) : IO UInt32 := do LSpec.lspecIO (.ofList [("ixvm", Tests.IxVM.suite)]) args diff --git a/Tests/AiurHashesMain.lean b/Tests/AiurHashesMain.lean deleted file mode 100644 index 6dec2e21..00000000 --- a/Tests/AiurHashesMain.lean +++ /dev/null @@ -1,4 +0,0 @@ -import Tests.AiurHashes - -def main (args : List String) : IO UInt32 := do - LSpec.lspecIO (.ofList [("aiur-hashes", Tests.AiurHashes.suite)]) args diff --git a/Tests/AiurMain.lean b/Tests/AiurMain.lean deleted file mode 100644 index 0918686d..00000000 --- a/Tests/AiurMain.lean +++ /dev/null @@ -1,4 +0,0 @@ -import Tests.Aiur - -def main (args : List String) : IO UInt32 := do - LSpec.lspecIO (.ofList [("aiur", Tests.Aiur.suite)]) args diff --git a/Tests/Cli.lean b/Tests/Cli.lean index fb62e84a..26170235 100644 --- a/Tests/Cli.lean +++ b/Tests/Cli.lean @@ -13,8 +13,7 @@ def Tests.Cli.run (buildCmd: String) (buildArgs : Array String) (buildDir : Opti IO.println out.stdout def Tests.Cli.suite : IO UInt32 := do - Tests.Cli.run "lake" (#["run", "install"]) none - Tests.Cli.run "ix" (#["--help"]) none + Tests.Cli.run "lake" (#["exe", "ix", "--help"]) none --Tests.Cli.run "ix" (#["store", "ix_test/IxTest.lean"]) none --Tests.Cli.run "ix" (#["prove", "ix_test/IxTest.lean", "one"]) none return 0 diff --git a/Tests/Common.lean b/Tests/Common.lean deleted file mode 100644 index 85e2dd07..00000000 --- a/Tests/Common.lean +++ /dev/null @@ -1,57 +0,0 @@ -/- - Common test utilities. - Basic type generators have been moved to Tests/Gen/Basic.lean. --/ - -import LSpec -import Tests.Gen.Basic -import Ix.Unsigned -import Ix.Aiur.Goldilocks -import Ix.Aiur.Protocol -import Ix.Aiur.Simple -import Ix.Aiur.Compile - -open LSpec SlimCheck Gen - -structure AiurTestCase where - functionName : Lean.Name - input : Array Aiur.G - expectedOutput : Array Aiur.G - inputIOBuffer: Aiur.IOBuffer - expectedIOBuffer: Aiur.IOBuffer - -def AiurTestCase.noIO := - (AiurTestCase.mk · · · default default) - -def commitmentParameters : Aiur.CommitmentParameters := { - logBlowup := 1 -} - -def friParameters : Aiur.FriParameters := { - logFinalPolyLen := 0 - numQueries := 100 - commitProofOfWorkBits := 20 - queryProofOfWorkBits := 0 -} - -def mkAiurTests (toplevelFn : Except Aiur.Global Aiur.Toplevel) - (cases : List AiurTestCase) : TestSeq := - withExceptOk "Toplevel merging succeeds" toplevelFn fun toplevel => - withExceptOk "Check and simplification succeed" toplevel.checkAndSimplify fun decls => - let bytecodeToplevel := decls.compile - let aiurSystem := Aiur.AiurSystem.build bytecodeToplevel commitmentParameters - let runTestCase := fun testCase => - let functionName := testCase.functionName - let funIdx := toplevel.getFuncIdx functionName |>.get! - let (claim, proof, ioBuffer) := aiurSystem.prove - friParameters funIdx testCase.input testCase.inputIOBuffer - let claimTest := test s!"Claim matches for {functionName}" - (claim == Aiur.buildClaim funIdx testCase.input testCase.expectedOutput) - let ioTest := test s!"IOBuffer matches for {functionName}" - (ioBuffer == testCase.expectedIOBuffer) - let proof := .ofBytes proof.toBytes - let pvTest := withExceptOk s!"Prove/verify works for {functionName}" - (aiurSystem.verify friParameters claim proof) fun _ => .done - claimTest ++ ioTest ++ pvTest - cases.foldl (init := .done) fun tSeq testCase => - tSeq ++ runTestCase testCase diff --git a/Tests/IxVM.lean b/Tests/IxVM.lean deleted file mode 100644 index 4d38aa8d..00000000 --- a/Tests/IxVM.lean +++ /dev/null @@ -1,6 +0,0 @@ -import Tests.Common -import Ix.IxVM - -def Tests.IxVM.suite := [ - mkAiurTests IxVM.ixVM [] -] diff --git a/lakefile.lean b/lakefile.lean index e8e03ee4..229b5f70 100644 --- a/lakefile.lean +++ b/lakefile.lean @@ -33,13 +33,13 @@ lean_exe IxTests where supportInterpreter := true lean_exe «test-aiur» where - root := `Tests.AiurMain + root := `Tests.Aiur.Aiur lean_exe «test-aiur-hashes» where - root := `Tests.AiurHashesMain + root := `Tests.Aiur.Hashes lean_exe «test-ixvm» where - root := `Tests.IxVMMain + root := `Tests.Aiur.IxVM end Tests From b299c51f6fc8a6eb64814471e62629f525fa5886 Mon Sep 17 00:00:00 2001 From: samuelburnham <45365069+samuelburnham@users.noreply.github.com> Date: Mon, 23 Feb 2026 14:35:38 -0500 Subject: [PATCH 6/8] Integrate Aiur tests with `lake test` --- .github/workflows/ci.yml | 5 ++--- .github/workflows/nix.yml | 4 ---- Tests/Aiur.lean | 2 ++ Tests/Aiur/Aiur.lean | 6 ------ Tests/Aiur/Common.lean | 5 ----- Tests/Aiur/Hashes.lean | 12 ------------ Tests/Aiur/IxVM.lean | 9 --------- Tests/Main.lean | 36 ++++++++++++++++++++++++++++++------ flake.nix | 6 ------ lakefile.lean | 9 --------- 10 files changed, 34 insertions(+), 60 deletions(-) delete mode 100644 Tests/Aiur/IxVM.lean diff --git a/.github/workflows/ci.yml b/.github/workflows/ci.yml index 0ef1861e..117480f4 100644 --- a/.github/workflows/ci.yml +++ b/.github/workflows/ci.yml @@ -40,9 +40,8 @@ jobs: run: | mkdir -p ~/.local/bin lake test -- cli - - run: lake exe test-aiur - - run: lake exe test-aiur-hashes - - run: lake exe test-ixvm + - name: Aiur tests + run: lake test -- --ignored aiur aiur-hashes ixvm - name: Check lean.h.hash run: lake run check-lean-h-hash diff --git a/.github/workflows/nix.yml b/.github/workflows/nix.yml index 9be2f5e4..ab6ff22c 100644 --- a/.github/workflows/nix.yml +++ b/.github/workflows/nix.yml @@ -29,10 +29,6 @@ jobs: - run: nix run .#ix -- --help # Ix tests - run: nix run .#test --accept-flake-config - # Expensive tests are only built in Nix to save time - - run: nix build .#test-aiur --accept-flake-config - - run: nix build .#test-aiur-hashes --accept-flake-config - - run: nix build .#test-ixvm --accept-flake-config # Tests Nix devShell support on Ubuntu nix-devshell: diff --git a/Tests/Aiur.lean b/Tests/Aiur.lean index 0f5c56d1..6dc81075 100644 --- a/Tests/Aiur.lean +++ b/Tests/Aiur.lean @@ -1 +1,3 @@ import Tests.Aiur.Common +import Tests.Aiur.Aiur +import Tests.Aiur.Hashes diff --git a/Tests/Aiur/Aiur.lean b/Tests/Aiur/Aiur.lean index ce1a1a5a..50e07246 100644 --- a/Tests/Aiur/Aiur.lean +++ b/Tests/Aiur/Aiur.lean @@ -268,9 +268,3 @@ def aiurTestCases : List AiurTestCase := [ .noIO `fold_matrix_sum #[1, 2, 3, 4] #[10], ] -def main (_args : List String) : IO UInt32 := do - match AiurTestEnv.build (pure toplevel) with - | .error e => IO.eprintln s!"Setup failed: {e}"; return 1 - | .ok env => - lspecEachIO aiurTestCases fun testCase => - pure (env.runTestCase testCase) diff --git a/Tests/Aiur/Common.lean b/Tests/Aiur/Common.lean index fb31675b..05c3cb25 100644 --- a/Tests/Aiur/Common.lean +++ b/Tests/Aiur/Common.lean @@ -1,8 +1,3 @@ -/- - Common Aiur test utilities. - Basic type generators have been moved to Tests/Gen/Basic.lean. --/ - import LSpec import Tests.Gen.Basic import Ix.Unsigned diff --git a/Tests/Aiur/Hashes.lean b/Tests/Aiur/Hashes.lean index c826b484..1dd0a11e 100644 --- a/Tests/Aiur/Hashes.lean +++ b/Tests/Aiur/Hashes.lean @@ -58,15 +58,3 @@ def sha256TestCases : List AiurTestCase := [ mkSha256HashTestCase 1200, ] -open LSpec - -def main (_args : List String) : IO UInt32 := do - let .ok blake3Env := AiurTestEnv.build (IxVM.byteStream.merge IxVM.blake3) - | IO.eprintln "Blake3 setup failed"; return 1 - let r1 ← lspecEachIO blake3TestCases fun testCase => - pure (blake3Env.runTestCase testCase) - let .ok sha256Env := AiurTestEnv.build (IxVM.byteStream.merge IxVM.sha256) - | IO.eprintln "SHA256 setup failed"; return 1 - let r2 ← lspecEachIO sha256TestCases fun testCase => - pure (sha256Env.runTestCase testCase) - return if r1 == 0 && r2 == 0 then 0 else 1 diff --git a/Tests/Aiur/IxVM.lean b/Tests/Aiur/IxVM.lean deleted file mode 100644 index b5e5c234..00000000 --- a/Tests/Aiur/IxVM.lean +++ /dev/null @@ -1,9 +0,0 @@ -import Tests.Aiur.Common -import Ix.IxVM - -def Tests.IxVM.suite := [ - mkAiurTests IxVM.ixVM [] -] - -def main (args : List String) : IO UInt32 := do - LSpec.lspecIO (.ofList [("ixvm", Tests.IxVM.suite)]) args diff --git a/Tests/Main.lean b/Tests/Main.lean index e25300a8..1f282294 100644 --- a/Tests/Main.lean +++ b/Tests/Main.lean @@ -1,3 +1,4 @@ +import Tests.Aiur import Tests.ByteArray import Tests.Ix.Ixon import Tests.Ix.Claim @@ -16,6 +17,7 @@ import Tests.Cli import Tests.ShardMap import Ix.Common import Ix.Meta +import Ix.IxVM @[extern "rs_tmp_decode_const_map"] opaque tmpDecodeConstMap : @& List (Lean.Name × Lean.ConstantInfo) → USize @@ -49,6 +51,25 @@ def ignoredSuites : Std.HashMap String (List LSpec.TestSeq) := .ofList [ ("commit-io", Tests.Commit.suiteIO), ] +/-- Ignored test runners - expensive, deferred IO actions run only when explicitly requested -/ +def ignoredRunners : List (String × IO UInt32) := [ + ("aiur", do + IO.println "aiur" + match AiurTestEnv.build (pure toplevel) with + | .error e => IO.eprintln s!"Aiur setup failed: {e}"; return 1 + | .ok env => LSpec.lspecEachIO aiurTestCases fun tc => pure (env.runTestCase tc)), + ("aiur-hashes", do + IO.println "aiur-hashes" + let .ok blake3Env := AiurTestEnv.build (IxVM.byteStream.merge IxVM.blake3) + | IO.eprintln "Blake3 setup failed"; return 1 + let r1 ← LSpec.lspecEachIO blake3TestCases fun tc => pure (blake3Env.runTestCase tc) + let .ok sha256Env := AiurTestEnv.build (IxVM.byteStream.merge IxVM.sha256) + | IO.eprintln "SHA256 setup failed"; return 1 + let r2 ← LSpec.lspecEachIO sha256TestCases fun tc => pure (sha256Env.runTestCase tc) + return if r1 == 0 && r2 == 0 then 0 else 1), + ("ixvm", do LSpec.lspecIO (.ofList [("ixvm", [mkAiurTests IxVM.ixVM []])]) []), +] + def main (args : List String) : IO UInt32 := do -- Special case: rust-compile diagnostic if args.contains "rust-compile" then @@ -65,15 +86,18 @@ def main (args : List String) : IO UInt32 := do let runIgnored := args.contains "--ignored" let filterArgs := args.filter (· != "--ignored") - -- Check if any filterArg matches an ignored suite - let ignoredRequested := filterArgs.any (ignoredSuites.contains ·) - -- Run primary tests let primaryResult ← LSpec.lspecIO primarySuites filterArgs if primaryResult != 0 then return primaryResult - -- Run ignored tests if --ignored flag or specific ignored suite requested - if runIgnored || ignoredRequested then - LSpec.lspecIO ignoredSuites filterArgs + -- Run ignored tests only when --ignored is specified + if runIgnored then + let mut result ← LSpec.lspecIO ignoredSuites filterArgs + let filtered := if filterArgs.isEmpty then ignoredRunners + else ignoredRunners.filter fun (key, _) => filterArgs.any fun arg => key == arg + for (_, action) in filtered do + let r ← action + if r != 0 then result := r + return result else return 0 diff --git a/flake.nix b/flake.nix index 4af41012..d4e6a802 100644 --- a/flake.nix +++ b/flake.nix @@ -123,9 +123,6 @@ }; ixCLI = lake2nix.mkPackage (lakeBinArgs // {name = "ix";}); ixTest = lake2nix.mkPackage (lakeBinArgs // {name = "IxTests";}); - testAiur = lake2nix.mkPackage (lakeBinArgs // {name = "test-aiur";}); - testAiurHashes = lake2nix.mkPackage (lakeBinArgs // {name = "test-aiur-hashes";}); - testIxVM = lake2nix.mkPackage (lakeBinArgs // {name = "test-ixvm";}); in { # Lean overlay _module.args.pkgs = import nixpkgs { @@ -137,9 +134,6 @@ default = ixLib; ix = ixCLI; test = ixTest; - test-aiur = testAiur; - test-aiur-hashes = testAiurHashes; - test-ixvm = testIxVM; }; # Provide a unified dev shell with Lean + Rust diff --git a/lakefile.lean b/lakefile.lean index 229b5f70..23e174ed 100644 --- a/lakefile.lean +++ b/lakefile.lean @@ -32,15 +32,6 @@ lean_exe IxTests where root := `Tests.Main supportInterpreter := true -lean_exe «test-aiur» where - root := `Tests.Aiur.Aiur - -lean_exe «test-aiur-hashes» where - root := `Tests.Aiur.Hashes - -lean_exe «test-ixvm» where - root := `Tests.Aiur.IxVM - end Tests section Benchmarks From dea10535c3c583f6a9115fafd99530759a6c18e5 Mon Sep 17 00:00:00 2001 From: samuelburnham <45365069+samuelburnham@users.noreply.github.com> Date: Mon, 23 Feb 2026 15:19:49 -0500 Subject: [PATCH 7/8] Cleanup --- .github/workflows/ci.yml | 2 +- Benchmarks/Sha256.lean | 2 +- Tests.lean | 18 +----------------- lakefile.lean | 10 ++++++---- 4 files changed, 9 insertions(+), 23 deletions(-) diff --git a/.github/workflows/ci.yml b/.github/workflows/ci.yml index 117480f4..b2a33bcf 100644 --- a/.github/workflows/ci.yml +++ b/.github/workflows/ci.yml @@ -35,7 +35,7 @@ jobs: build-args: "--wfail -v" test: true - name: Build all targets - run: lake run build-all + run: lake run build-all --wfail - name: Test Ix CLI run: | mkdir -p ~/.local/bin diff --git a/Benchmarks/Sha256.lean b/Benchmarks/Sha256.lean index 643b797a..751a7e46 100644 --- a/Benchmarks/Sha256.lean +++ b/Benchmarks/Sha256.lean @@ -45,7 +45,7 @@ def sha256Bench : IO $ Array BenchReport := do bgroup "prove sha256" benches.toList { oneShot := true } def parseFunction (words : List String) (param : String): Option String := - words.find? (·.startsWith param) |> .map (·.stripPrefix param) + words.find? (·.startsWith param) |>.map (·.dropPrefix param |>.toString) def main : IO Unit := do let result ← sha256Bench diff --git a/Tests.lean b/Tests.lean index 22932177..a3a4606d 100644 --- a/Tests.lean +++ b/Tests.lean @@ -1,17 +1 @@ -import Tests.Aiur -import Tests.ByteArray -import Tests.Ix.Ixon -import Tests.Ix.Claim -import Tests.Ix.Commit -import Tests.Ix.Compile -import Tests.Ix.Decompile -import Tests.Ix.RustSerialize -import Tests.Ix.RustDecompile -import Tests.Ix.Sharing -import Tests.Ix.CanonM -import Tests.Ix.GraphM -import Tests.Ix.CondenseM -import Tests.FFI -import Tests.Keccak -import Tests.Cli -import Tests.ShardMap +import Tests.Main diff --git a/lakefile.lean b/lakefile.lean index 23e174ed..b7f8b4a4 100644 --- a/lakefile.lean +++ b/lakefile.lean @@ -169,16 +169,18 @@ script "get-exe-targets" := do IO.println <| tgt.name.toString |>.dropPrefix "«" |>.dropSuffix "»" |>.toString return 0 -script "build-all" := do - let ws ← getWorkspace +script "build-all" (args) := do let pkg ← getRootPackage let libNames := pkg.configTargets LeanLib.configKind |>.map (·.name.toString) let exeNames := pkg.configTargets LeanExe.configKind |>.map (·.name.toString) let allNames := libNames ++ exeNames |>.toList for name in allNames do IO.println s!"Building: {name}" - let specs ← EIO.toIO (·.toString) <| Lake.parseTargetSpecs ws [name] - ws.runBuild (buildSpecs specs) + let child ← IO.Process.spawn { + cmd := "lake", args := #["build", name] ++ args + stdout := .inherit, stderr := .inherit } + let exitCode ← child.wait + if exitCode != 0 then return exitCode return 0 end Scripts From b196fe1ed23756bbe7740afa884fee9871759a3c Mon Sep 17 00:00:00 2001 From: samuelburnham <45365069+samuelburnham@users.noreply.github.com> Date: Mon, 23 Feb 2026 16:05:15 -0500 Subject: [PATCH 8/8] Update Readme --- README.md | 32 +++++++------------------------- 1 file changed, 7 insertions(+), 25 deletions(-) diff --git a/README.md b/README.md index 23b3a498..c4fd9caf 100644 --- a/README.md +++ b/README.md @@ -182,20 +182,16 @@ Compiler performance benchmarks are tracked at https://bencher.dev/console/proje ### Testing -**Lean tests:** `lake test` runs all primary test suites. +**Lean tests:** `lake test` -- `lake test -- ` runs a specific suite. Primary suites: `ffi`, `byte-array`, `ixon`, `claim`, `commit`, `canon`, `keccak`, `sharing`, `graph-unit`, `condense-unit` -- `lake test -- --ignored` runs expensive test suites: `shard-map`, `rust-canon-roundtrip`, `serial-canon-roundtrip`, `parallel-canon-roundtrip`, `graph-cross`, `condense-cross`, `compile`, `decompile`, `rust-serialize`, `rust-decompile`, `commit-io`, `sharing-io` -- `lake test -- ` runs a specific expensive suite by name +- `lake test -- ` runs a specific test suite. Primary suites: `ffi`, `byte-array`, `ixon`, `claim`, `commit`, `canon`, `keccak`, `sharing`, `graph-unit`, `condense-unit` +- `lake test -- --ignored` runs expensive test suites: `shard-map`, `rust-canon-roundtrip`, `serial-canon-roundtrip`, `parallel-canon-roundtrip`, `graph-cross`, `condense-cross`, `compile`, `decompile`, `rust-serialize`, `rust-decompile`, `commit-io`, `aiur`, `aiur-hashes`, `ixvm` + - Any `canon` or `compile` test will require significant RAM, beware of OOM + - `aiur` and `aiur-hashes` generate ZK proofs and use significant CPU +- `lake test -- --ignored ` runs a specific expensive suite by name - `lake test -- cli` runs CLI integration tests - `lake test -- rust-compile` runs the Rust cross-compilation diagnostic -To run tests that involve zk proofs, which are slower, run: - -- `lake exe test-aiur` -- `lake exe test-aiur-hashes` -- `lake exe test-ixvm` - **Rust tests:** `cargo test` - Run the Ix CLI with `lake exe ix`. Install the binary with `lake run install` @@ -220,20 +216,6 @@ To run tests that involve zk proofs, which are slower, run: Build and run the Ix CLI with `nix build` and `nix run`. -This will prompt you to enable the Garnix cache, which can also be done by passing `--accept-flake-config` to the Nix command. Then when building, you should see `copying path '/nix/store/<...>' from https://cache.garnix.io` +This will prompt you to optionally enable the Garnix cache, which can also be done by passing `--accept-flake-config` to the Nix command. Then when building, you should see `copying path '/nix/store/<...>' from https://cache.garnix.io` To build and run the test suite, run `nix build .#test` and `nix run .#test`. - -#### Cache Troubleshooting - -If the Nix build hangs with a message like `building lean-stage0`, it's not -finding the cached packages and will likely take >15 minutes to build the Lean -compiler from source. Ctrl+C and check the following: - -- Note that caching is only provided for `x86_64-linux` at - the moment -- Make sure `substituters` and `trusted-public-keys` have been added to - `~/.config/nix/nix.conf`, or you've built with `nix build --accept-flake-config` -- Check the Lean version is supported at https://github.com/lenianiva/lean4-nix/tree/main/manifests -- If using Ix as a flake input, make sure any top-level nixpkgs version is also pinned to follow `lean4-nix/nixpkgs`. Otherwise the overlay will have to rebuild lean4-nix from scratch -- Try restarting the Nix daemon