Initializing Aiur2 (#179)

* feat: bytecode and execution of aiur2

* Read bytecodes from Lean in Rust

* port simplification and typechecking to Aiur2

* port compilation to Aiur2

* Aiur2 execution tests

Author: arthurpaulino

Cargo.lock

@@ -21,6 +21,8 @@ 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"
 rand = "0.9.1"
 rustc-hash = "2"

Cargo.toml

@@ -44,7 +44,6 @@ def checkAndSimplifyToplevel (toplevel : Toplevel) : Except CheckError TypedDecl
     | .constructor d c => pure $ typedDecls.insert name (.constructor d c)
     | .dataType d => pure $ typedDecls.insert name (.dataType d)
     | .function f => do
-      let _ ← (checkFunction f) (getFunctionContext f decls)
       let f ← (checkFunction f) (getFunctionContext f decls)
       pure $ typedDecls.insert name (.function f)
     | .gadget g => pure $ typedDecls.insert name (.gadget g)

Ix/Aiur/Simple.lean

@@ -0,0 +1,69 @@
+import Ix.Aiur2.Goldilocks
+
+namespace Aiur
+
+namespace Bytecode
+
+abbrev FunIdx := Nat
+abbrev ValIdx := Nat
+abbrev SelIdx := Nat
+
+inductive Op
+  | const : G → Op
+  | add : ValIdx → ValIdx → Op
+  | sub : ValIdx → ValIdx → Op
+  | mul : ValIdx → ValIdx → Op
+  | call : FunIdx → Array ValIdx → Op
+  | store : Array ValIdx → Op
+  | load : (width : Nat) → ValIdx → Op
+  deriving Repr
+
+mutual
+  inductive Ctrl where
+    | match : ValIdx → Array (G × Block) → Option Block → Ctrl
+    | return : SelIdx → Array ValIdx → Ctrl
+    deriving Inhabited, Repr
+
+  structure Block where
+    ops : Array Op
+    ctrl : Ctrl
+    minSelIncluded: SelIdx
+    maxSelExcluded: SelIdx
+    deriving Inhabited, Repr
+end
+
+/-- The circuit layout of a function -/
+structure CircuitLayout where
+  /-- 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
+  deriving Inhabited, Repr
+
+structure Function where
+  inputSize : Nat
+  outputSize : Nat
+  body : Block
+  circuitLayout: CircuitLayout
+  deriving Inhabited, Repr
+
+structure Toplevel where
+  functions : Array Function
+  memoryWidths : 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