feat: Add SP1 and Zisk kernel proving backends

.gitignore

@@ -2,7 +2,7 @@
 **/.lake
 
 # Rust
-/target
+**/target
 
 # Nix
 result*

Cargo.toml

@@ -1,55 +1,59 @@
-[package]
-name = "ix_rs"
+[workspace]
+members = [
+  "crates/aiur",
+  "crates/common",
+  "crates/compile",
+  "crates/ffi",
+  "crates/ixon",
+  "crates/kernel",
+]
+# `zisk/` and `sp1/` are their own Cargo workspaces (guest + host) built via
+# the respective zkVM toolchains; excluded so host workspace ops don't pick
+# them up.
+exclude = ["zisk", "sp1"]
+resolver = "2"
+
+[profile.dev]
+panic = "abort"
+
+[profile.release]
+panic = "abort"
+
+[workspace.package]
 version = "0.1.0"
 edition = "2024"
+license = "MIT OR Apache-2.0"
+
+[workspace.dependencies]
+# Internal crates
+aiur = { path = "crates/aiur" }
+ix-common = { path = "crates/common" }
+ix-compile = { path = "crates/compile" }
+ixon = { path = "crates/ixon" }
+ix-kernel = { path = "crates/kernel" }
 
-[lib]
-crate-type = ["staticlib"]
+# lean-ffi tree (lean-ffi crate + factored-out bignat sub-crate)
+bignat = { git = "https://github.com/argumentcomputer/lean-ffi.git", branch = "bignat" }
+lean-ffi = { git = "https://github.com/argumentcomputer/lean-ffi.git", branch = "bignat" }
 
-[dependencies]
+# External shared deps
 anyhow = "1"
 blake3 = "1.8.4"
+dashmap = "6.1.0"
+indexmap = "2"
 itertools = "0.14.0"
-indexmap = { version = "2", features = ["rayon"] }
-lean-ffi = { git = "https://github.com/argumentcomputer/lean-ffi", rev = "cc98ebf67bf453ac3827cb767f78b13ea674dd6a" }
+log = "0.4"
 mimalloc = { version = "0.1", default-features = false }
 multi-stark = { git = "https://github.com/argumentcomputer/multi-stark.git", rev = "a8a15ea6aa2890f9f60f32a6e0e5e66afc1535ff" }
 num-bigint = "0.4.6"
+quickcheck = "1.0.3"
+quickcheck_macros = "1.0.0"
 rayon = "1"
 rustc-hash = "2"
-tiny-keccak = { version = "2", features = ["keccak"] }
-dashmap = { version = "6.1.0", features = ["rayon"] }
 sha2 = "0.10"
-# Iroh dependencies
-bytes = { version = "1.10.1", optional = true }
-tokio = { version = "1.44.1", optional = true }
-iroh = { version = "0.97", optional = true }
-iroh-base = { version = "0.97", optional = true }
-n0-error = { version = "0.1", optional = true }
-getrandom = { version = "0.3", optional = true }
-tracing = { version = "0.1", optional = true }
-tracing-subscriber = { version = "0.3", features = ["env-filter"], optional = true }
-bincode = { version = "2.0.1", optional = true }
-serde = { version = "1.0.219", features = ["derive"], optional = true }
-
-[dev-dependencies]
-quickcheck = "1.0.3"
-rand = "0.10.1"
-quickcheck_macros = "1.0.0"
-
-[features]
-default = []
-parallel = ["multi-stark/parallel"]
-test-ffi = []
-net = ["bytes", "tokio", "iroh", "iroh-base", "n0-error", "getrandom", "tracing", "tracing-subscriber", "bincode", "serde" ]
-
-[profile.dev]
-panic = "abort"
-
-[profile.release]
-panic = "abort"
+tiny-keccak = { version = "2", features = ["keccak"] }
 
-[lints.rust]
+[workspace.lints.rust]
 invalid_reference_casting = "warn"
 nonstandard_style = "warn"
 rust_2018_idioms = { level = "warn", priority = -1 }
@@ -58,7 +62,7 @@ unreachable_pub = "warn"
 unused_lifetimes = "warn"
 unused_qualifications = "warn"
 
-[lints.clippy]
+[workspace.lints.clippy]
 all = { level = "warn", priority = -1 }
 cast_lossless = "warn"
 cast_possible_truncation = "warn"

Ix/Cli/CompileCmd.lean

@@ -20,17 +20,29 @@ def runCompileCmd (p : Cli.Parsed) : IO UInt32 := do
   let pathStr := path.as! String
   let outPath : String :=
     (p.flag? "out").map (·.as! String) |>.getD (defaultOutPathFor pathStr)
+  let rootName? : Option Lean.Name :=
+    (p.flag? "root").map (·.as! String |>.toName)
 
   buildFile pathStr
   let leanEnv ← getFileEnv pathStr
 
   println! "Running Ix compiler on {pathStr}"
 
-  let totalConsts := leanEnv.constants.toList.length
-  println! "Total constants: {totalConsts}"
+  let constList ← match rootName? with
+    | none => pure leanEnv.constants.toList
+    | some root =>
+      if !leanEnv.constants.contains root then
+        IO.eprintln s!"error: root constant `{root}` not found in environment"
+        IO.Process.exit 1
+      pure (Lean.collectDependencies root leanEnv.constants)
+  let totalConsts := constList.length
+  if let some root := rootName? then
+    println! "Slicing to transitive closure of `{root}`: {totalConsts} constants"
+  else
+    println! "Total constants: {totalConsts}"
 
   let start ← IO.monoMsNow
-  let bytes ← Ix.CompileM.rsCompileEnvBytes leanEnv
+  let bytes ← Ix.CompileM.rsCompileEnvBytesFFI constList
   let elapsed := (← IO.monoMsNow) - start
 
   println! "Compiled {fmtBytes bytes.size} env in {elapsed.formatMs}"
@@ -56,6 +68,7 @@ def compileCmd : Cli.Cmd := `[Cli|
   FLAGS:
     path : String; "Path to file to compile"
     out  : String; "Output path for serialized Ixon.Env bytes; defaults to the lowercased input file stem with `.ixe` (e.g. CompileMathlib.lean -> compilemathlib.ixe)"
+    root : String; "If set, emit only the transitive Const-closure of this constant (e.g. `Nat.add_comm`) instead of the entire environment"
 ]
 
 end