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>

Author: 3 people

Cargo.lock

@@ -21,12 +21,11 @@ binius_utils = { git = "https://github.com/IrreducibleOSS/binius.git", rev = "23
 bumpalo = "3"
 groestl_crypto = { package = "groestl", version = "0.10.1" }
 proptest = "1"
-p3-goldilocks = "0.3.0"
-p3-field = "0.3.0"
-rayon = "1"
+multi-stark = { git = "https://github.com/argumentcomputer/multi-stark.git", rev = "f3017f7f1ad5f3e3149b552e188e9f9e09370a97" }
+rayon = "1.7.0"
 rand = "0.9.1"
 rustc-hash = "2"
-indexmap = "2"
+indexmap = { version = "2", features = ["rayon"] }
 bytes = "1.10.1"
 tiny-keccak = { version = "2.0.2", features = ["keccak"] }
 
@@ -37,4 +36,4 @@ iroh-base = "0.34.0"
 iroh-blobs = { version = "0.34.0", features = ["rpc"] }
 
 [features]
-default = []
+parallel = ["multi-stark/parallel"]

Cargo.toml

@@ -13,9 +13,9 @@ inductive Op
   | add : ValIdx → ValIdx → Op
   | sub : ValIdx → ValIdx → Op
   | mul : ValIdx → ValIdx → Op
-  | call : FunIdx → Array ValIdx → Op
+  | call : FunIdx → Array ValIdx → (outputSize : Nat) → Op
   | store : Array ValIdx → Op
-  | load : (width : Nat) → ValIdx → Op
+  | load : (size : Nat) → ValIdx → Op
   deriving Repr
 
 mutual
@@ -33,37 +33,30 @@ mutual
 end
 
 /-- The circuit layout of a function -/
-structure CircuitLayout where
+structure FunctionLayout where
+  inputSize : Nat
+  outputSize : Nat
   /-- Bit values that identify which path the computation took.
     Exactly one selector must be set. -/
   selectors : Nat
   /-- Represent registers that hold temporary values and can be shared by
     different circuit paths, since they never overlap. -/
   auxiliaries : Nat
-  /-- Constraint slots that can be shared in different paths of the circuit. -/
-  sharedConstraints : Nat
+  /-- Lookups can be shared across calls, stores, loads and returns from
+    different paths. -/
+  lookups : Nat
   deriving Inhabited, Repr
 
 structure Function where
-  inputSize : Nat
-  outputSize : Nat
   body : Block
-  circuitLayout: CircuitLayout
+  layout: FunctionLayout
   deriving Inhabited, Repr
 
 structure Toplevel where
   functions : Array Function
-  memoryWidths : Array Nat
+  memorySizes : Array Nat
   deriving Repr
 
-@[extern "c_rs_toplevel_execute_test"]
-private opaque Toplevel.executeTest' :
-  @& Toplevel → @& FunIdx → @& Array G → USize → Array G
-
-def Toplevel.executeTest (toplevel : Toplevel) (funIdx : FunIdx) (args : Array G) : Array G :=
-  let function := toplevel.functions[funIdx]!
-  toplevel.executeTest' funIdx args function.outputSize.toUSize
-
 end Bytecode
 
 end Aiur