Skip to content

Commit 04b1f52

Browse files
johnchandlerburnhamsamuelburnhamarthurpaulinogabriel-barrett
authored
jcb/ix-vm Compilation Roundtrip (#203)
* WIP: ix hash command * make Proof serialize as an Ixon Const * broken: connect canonicalizer to Ix.Meta * fix: Nix devShell & light refactor (#55) * ix store cli command * WIP: store command and new IxM structure * megacommit implementing Ix commitment API * fixup merge * fixup merge 2 * ix prove check command * implement ix prove CLI and simplify metaprogramming - CompileM is now persistent with the filemapped store - constructing evaluation claims is done through MetaM rather than CompileM - CLI now features the Prove command * provecmd examples * cleanup repo * simplify ZKVoting example app * remove IO from the compiler core * add level params to Ix IR to support decompilation * refactor Ix IR to support decompilation * implement decompilation mutdefs, compilation of mixed mutdefs, and tests for new mutdef format * wip * decompilation roundtrip of Ix get_env working * WIP: new mutual definition changes * roundtrip compilation decompilation tests now passing * add count to roundtrip * fixup merge * fixup merge * fixup merge test * remove style guide * merge * Aiur2 prove/verify (#183) * prove and verify for Aiur2 * env var to opt out of parallelism * bump the Rust toolchain --------- Co-authored-by: Gabriel Barreto <gabriel.aquino.barreto@gmail.com> Co-authored-by: Samuel Burnham <45365069+samuelburnham@users.noreply.github.com> * Remove binius (#185) * chore: drop Binius * Drop the dependency on Binius * Remove Aiur * Rename Aiur2 to Aiur * chore: deactivate Iroh * update the hash for the Rust toolchain * satisfy ci * Bench (#186) * add a `clock` executable for performance analysis * clean up for a benchmarking implementation * initial ixon serialization framework * rustfmt * ixon univ/expr roundtrip * new ixon format passing proptest roundtrip * remove old files * implement Ixon v2 in Lean * Ixon reconstruction in Rust from Lean pointers * use standard formatting * fix Ixon Lean serialization * WIP: Lean -> Rust round-trip serialization test * fix FFI * WIP: synchronized Lean and Rust implementations, failing on metadata FFI? * fix FFI for ReducibilityHints::Regular * WIP: improved performance of mutual def sorting, but compilation still OOM on large terms * very WIP compiler rewrite * compiler refactored * proptest for `Ixon` serde * try reverting caches to RBMap * bitblast now compiling * full compilation of Lean->Ixon, but slow * Tarjan's SCC algorithm for mutuals, so we can compile Recursors * simplify mutual compilation, remove IR * compile unsafe Lean? * decompilation wip * decompilation progress, but failing on _cstage2 * preprocessing GroundM step, but CondenseM breaking * fix CondenseM, GroundM breaking * wip * GroundM and CondenseM working * CompileM/DecompileM roundtrip provisionally working up to 5% of get_env! * wip * fixup for comments and clippy * disable aiur benchmarks due to Ixon format change * xclippy warnings * disable Cli test suite --------- Co-authored-by: Samuel Burnham <45365069+samuelburnham@users.noreply.github.com> Co-authored-by: Arthur Paulino <arthurleonardo.ap@gmail.com> Co-authored-by: Gabriel Barreto <gabriel.aquino.barreto@gmail.com>
1 parent 67d095c commit 04b1f52

Some content is hidden

Large Commits have some content hidden by default. Use the searchbox below for content that may be hidden.

56 files changed

+9013
-4152
lines changed

‎Benchmarks/Aiur.lean‎

Lines changed: 128 additions & 127 deletions
Original file line numberDiff line numberDiff line change
@@ -1,128 +1,129 @@
1-
import Ix.Aiur.Meta
2-
import Ix.Aiur.Simple
3-
import Ix.Aiur.Compile
4-
import Ix.Aiur.Protocol
5-
import Ix.Benchmark.Bench
6-
7-
def toplevel := ⟦
8-
enum Nat {
9-
Zero,
10-
Succ(&Nat)
11-
}
12-
13-
fn g_to_nat(g: G) -> Nat {
14-
match g {
15-
0 => Nat.Zero,
16-
_ => Nat.Succ(store(g_to_nat(g - 1))),
17-
}
18-
}
19-
20-
fn nat_to_g(n: Nat) -> G {
21-
match n {
22-
Nat.Zero => 0,
23-
Nat.Succ(ptr) => nat_to_g(load(ptr)) + 1,
24-
}
25-
}
26-
27-
fn nat_add(a: Nat, b: Nat) -> Nat {
28-
match b {
29-
Nat.Zero => a,
30-
Nat.Succ(b'ptr) => nat_add(Nat.Succ(store(a)), load(b'ptr)),
31-
}
32-
}
33-
34-
fn nat_fib(n: Nat) -> Nat {
35-
match n {
36-
Nat.Zero => Nat.Succ(store(Nat.Zero)),
37-
Nat.Succ(n'ptr) =>
38-
let n' = load(n'ptr);
39-
match n' {
40-
Nat.Zero => Nat.Succ(store(Nat.Zero)),
41-
Nat.Succ(n''ptr) =>
42-
let n'' = load(n''ptr);
43-
nat_add(nat_fib(n'), nat_fib(n'')),
44-
},
45-
}
46-
}
47-
48-
fn main(g: G) -> G {
49-
nat_to_g(nat_fib(g_to_nat(g)))
50-
}
51-
⟧
52-
53-
def commitmentParameters : Aiur.CommitmentParameters := {
54-
logBlowup := 1
55-
}
56-
57-
def friParameters : Aiur.FriParameters := {
58-
logFinalPolyLen := 0
59-
numQueries := 100
60-
proofOfWorkBits := 20
61-
}
62-
63-
def proveE2E (name: Lean.Name) : IO UInt32 := do
64-
match toplevel.checkAndSimplify with
65-
| .error e => IO.eprintln e; return 1
66-
| .ok decls =>
67-
let bytecode := decls.compile
68-
let system := Aiur.AiurSystem.build bytecode commitmentParameters
69-
let funIdx := toplevel.getFuncIdx name |>.get!
70-
let (claim, proof, _) := system.prove friParameters funIdx #[10] default
71-
match system.verify friParameters claim proof with
72-
| .ok _ => return 0
73-
| .error e => IO.eprintln e; return 1
74-
75-
76-
-- End-to-end proof generation and verification benchmark
77-
def proveE2EBench := bgroup "prove E2E" [
78-
benchIO "fib 10" proveE2E `main
79-
] { samplingMode := .flat }
80-
81-
-- Individual benchmarks of each step from `proveE2E`
82-
83-
def toplevelBench := bgroup "nat_fib" [
84-
bench "simplify toplevel" Aiur.Toplevel.checkAndSimplify toplevel
85-
]
86-
87-
def compileBench : IO Unit := do
88-
match toplevel.checkAndSimplify with
89-
| .error e => IO.eprintln e
90-
| .ok decls =>
91-
bgroup "nat_fib" [
92-
bench "compile decls" Aiur.TypedDecls.compile decls
93-
]
94-
95-
def buildAiurSystemBench : IO Unit := do
96-
match toplevel.checkAndSimplify with
97-
| .error e => IO.eprintln e
98-
| .ok decls =>
99-
let bytecode := decls.compile
100-
bgroup "nat_fib" [
101-
bench "build AiurSystem" (Aiur.AiurSystem.build bytecode) commitmentParameters
102-
]
103-
104-
def proveBench : IO Unit := do
105-
match toplevel.checkAndSimplify with
106-
| .error e => IO.eprintln e
107-
| .ok decls =>
108-
let bytecode := decls.compile
109-
let system := Aiur.AiurSystem.build bytecode commitmentParameters
110-
let funIdx := toplevel.getFuncIdx `main |>.get!
111-
bgroup "nat_fib" [
112-
bench "prove fib 10" (Aiur.AiurSystem.prove system friParameters funIdx) #[10]
113-
]
114-
115-
def verifyBench : IO Unit := do
116-
match toplevel.checkAndSimplify with
117-
| .error e => IO.eprintln e
118-
| .ok decls =>
119-
let bytecode := decls.compile
120-
let system := Aiur.AiurSystem.build bytecode commitmentParameters
121-
let funIdx := toplevel.getFuncIdx `main |>.get!
122-
let (claim, proof, _) := system.prove friParameters funIdx #[10] default
123-
bgroup "nat_fib" [
124-
bench "verify fib 10" (Aiur.AiurSystem.verify system friParameters claim) proof
125-
]
126-
1+
--import Ix.Aiur.Meta
2+
--import Ix.Aiur.Simple
3+
--import Ix.Aiur.Compile
4+
--import Ix.Aiur.Protocol
5+
--import Ix.Benchmark.Bench
6+
--
7+
--def toplevel := ⟦
8+
-- enum Nat {
9+
-- Zero,
10+
-- Succ(&Nat)
11+
-- }
12+
--
13+
-- fn g_to_nat(g: G) -> Nat {
14+
-- match g {
15+
-- 0 => Nat.Zero,
16+
-- _ => Nat.Succ(store(g_to_nat(g - 1))),
17+
-- }
18+
-- }
19+
--
20+
-- fn nat_to_g(n: Nat) -> G {
21+
-- match n {
22+
-- Nat.Zero => 0,
23+
-- Nat.Succ(ptr) => nat_to_g(load(ptr)) + 1,
24+
-- }
25+
-- }
26+
--
27+
-- fn nat_add(a: Nat, b: Nat) -> Nat {
28+
-- match b {
29+
-- Nat.Zero => a,
30+
-- Nat.Succ(b'ptr) => nat_add(Nat.Succ(store(a)), load(b'ptr)),
31+
-- }
32+
-- }
33+
--
34+
-- fn nat_fib(n: Nat) -> Nat {
35+
-- match n {
36+
-- Nat.Zero => Nat.Succ(store(Nat.Zero)),
37+
-- Nat.Succ(n'ptr) =>
38+
-- let n' = load(n'ptr);
39+
-- match n' {
40+
-- Nat.Zero => Nat.Succ(store(Nat.Zero)),
41+
-- Nat.Succ(n''ptr) =>
42+
-- let n'' = load(n''ptr);
43+
-- nat_add(nat_fib(n'), nat_fib(n'')),
44+
-- },
45+
-- }
46+
-- }
47+
--
48+
-- fn main(g: G) -> G {
49+
-- nat_to_g(nat_fib(g_to_nat(g)))
50+
-- }
51+
--⟧
52+
--
53+
--def commitmentParameters : Aiur.CommitmentParameters := {
54+
-- logBlowup := 1
55+
--}
56+
--
57+
--def friParameters : Aiur.FriParameters := {
58+
-- logFinalPolyLen := 0
59+
-- numQueries := 100
60+
-- proofOfWorkBits := 20
61+
--}
62+
--
63+
--def proveE2E (name: Lean.Name) : IO UInt32 := do
64+
-- match toplevel.checkAndSimplify with
65+
-- | .error e => IO.eprintln e; return 1
66+
-- | .ok decls =>
67+
-- let bytecode := decls.compile
68+
-- let system := Aiur.AiurSystem.build bytecode commitmentParameters
69+
-- let funIdx := toplevel.getFuncIdx name |>.get!
70+
-- let (claim, proof, _) := system.prove friParameters funIdx #[10] default
71+
-- match system.verify friParameters claim proof with
72+
-- | .ok _ => return 0
73+
-- | .error e => IO.eprintln e; return 1
74+
--
75+
--
76+
---- End-to-end proof generation and verification benchmark
77+
--def proveE2EBench := bgroup "prove E2E" [
78+
-- benchIO "fib 10" proveE2E `main
79+
--] { samplingMode := .flat }
80+
--
81+
---- Individual benchmarks of each step from `proveE2E`
82+
--
83+
--def toplevelBench := bgroup "nat_fib" [
84+
-- bench "simplify toplevel" Aiur.Toplevel.checkAndSimplify toplevel
85+
--]
86+
--
87+
--def compileBench : IO Unit := do
88+
-- match toplevel.checkAndSimplify with
89+
-- | .error e => IO.eprintln e
90+
-- | .ok decls =>
91+
-- bgroup "nat_fib" [
92+
-- bench "compile decls" Aiur.TypedDecls.compile decls
93+
-- ]
94+
--
95+
--def buildAiurSystemBench : IO Unit := do
96+
-- match toplevel.checkAndSimplify with
97+
-- | .error e => IO.eprintln e
98+
-- | .ok decls =>
99+
-- let bytecode := decls.compile
100+
-- bgroup "nat_fib" [
101+
-- bench "build AiurSystem" (Aiur.AiurSystem.build bytecode) commitmentParameters
102+
-- ]
103+
--
104+
--def proveBench : IO Unit := do
105+
-- match toplevel.checkAndSimplify with
106+
-- | .error e => IO.eprintln e
107+
-- | .ok decls =>
108+
-- let bytecode := decls.compile
109+
-- let system := Aiur.AiurSystem.build bytecode commitmentParameters
110+
-- let funIdx := toplevel.getFuncIdx `main |>.get!
111+
-- bgroup "nat_fib" [
112+
-- bench "prove fib 10" (Aiur.AiurSystem.prove system friParameters funIdx) #[10]
113+
-- ]
114+
--
115+
--def verifyBench : IO Unit := do
116+
-- match toplevel.checkAndSimplify with
117+
-- | .error e => IO.eprintln e
118+
-- | .ok decls =>
119+
-- let bytecode := decls.compile
120+
-- let system := Aiur.AiurSystem.build bytecode commitmentParameters
121+
-- let funIdx := toplevel.getFuncIdx `main |>.get!
122+
-- let (claim, proof, _) := system.prove friParameters funIdx #[10] default
123+
-- bgroup "nat_fib" [
124+
-- bench "verify fib 10" (Aiur.AiurSystem.verify system friParameters claim) proof
125+
-- ]
126+
--
127127
def main (_args : List String) : IO Unit := do
128-
let _result ← proveBench
128+
return ()
129+
-- let _result ← proveBench

‎Cargo.lock‎

Lines changed: 44 additions & 10 deletions
Some generated files are not rendered by default. Learn more about customizing how changed files appear on GitHub.

‎Cargo.toml‎

Lines changed: 6 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -10,10 +10,10 @@ crate-type = ["staticlib"]
1010
anyhow = "1"
1111
indexmap = { version = "2", features = ["rayon"] }
1212
multi-stark = { git = "https://github.com/argumentcomputer/multi-stark.git", rev = "11a2e444004609174e1ad59e366e7f621bdd427b" }
13-
num-bigint = "0.4"
1413
rayon = "1"
1514
rustc-hash = "2"
1615
tiny-keccak = { version = "2", features = ["keccak"] }
16+
num-bigint = "0.4.6"
1717
blake3 = "1.8.2"
1818
# Iroh dependencies
1919
bytes = { version = "1.10.1", optional = true }
@@ -29,6 +29,11 @@ bincode = { version = "2.0.1", optional = true }
2929
serde = { version = "1.0.219", features = ["derive"], optional = true }
3030

3131

32+
[dev-dependencies]
33+
quickcheck = "1.0.3"
34+
rand = "0.8.5"
35+
quickcheck_macros = "1.0.0"
36+
3237
[features]
3338
default = []
3439
parallel = ["multi-stark/parallel"]

0 commit comments

Comments
 (0)