Aiur interpreter

Ix/Aiur/Compiler/Concretize.lean

@@ -1,5 +1,5 @@
 module
-public import Ix.Aiur.Compiler.Check
+public import Ix.Aiur.Check
 public import Std.Data.HashSet
 public import Std.Data.HashMap
 

Ix/Aiur/Compiler/Simple.lean

@@ -1,6 +1,6 @@
 module
 public import Ix.Aiur.Compiler.Match
-public import Ix.Aiur.Compiler.Check
+public import Ix.Aiur.Check
 
 public section
 

Kernel.lean

@@ -1,32 +1,45 @@
 import Ix.Meta
 import Ix.Aiur.Protocol
 import Ix.Aiur.Statistics
+import Ix.Aiur.Interpret
 import Ix.IxVM
 import Tests.Ix.IxVM
 import Tests.Aiur.Common
 
+def parseName (arg : String) : Lean.Name :=
+  arg.splitOn "." |>.foldl (init := .anonymous)
+    fun acc s => match s.toNat? with
+      | some n => Lean.Name.mkNum acc n
+      | none   => Lean.Name.mkStr acc s
+
 def main (args : List String) : IO UInt32 := do
   let env ← get_env!
+  let dbg := args.contains "--dbg"
+  let args := args.filter (· != "--dbg")
   let toplevel ← match IxVM.ixVM with
     | .error e => IO.eprintln s!"Toplevel merging failed: {e}"; return 1
     | .ok t => pure t
-  let compiled ← match toplevel.compile with
-    | .error e => IO.eprintln s!"Compilation failed: {e}"; return 1
-    | .ok c => pure c
+  let run ← if dbg then
+      let decls ← match toplevel.mkDecls with
+        | .error e => IO.eprintln s!"mkDecls failed: {e}"; return 1
+        | .ok d => pure d
+      pure (interpCheck decls · env)
+    else
+      let compiled ← match toplevel.compile with
+        | .error e => IO.eprintln s!"Compilation failed: {e}"; return 1
+        | .ok c => pure c
+      pure (check compiled · env)
   if args.isEmpty then
     for (name, _) in env.constants do
-      let res ← check compiled name env
+      let res ← run name
       if res ≠ 0 then return res
   else
     for arg in args do
-      let name := arg.splitOn "." |>.foldl (init := .anonymous)
-        fun acc s => match s.toNat? with
-          | some n => Lean.Name.mkNum acc n
-          | none   => Lean.Name.mkStr acc s
+      let name := parseName arg
       if !env.constants.contains name then
         IO.eprintln s!"{name} not found"
         return 1
-      let res ← check compiled name env
+      let res ← run name
       if res ≠ 0 then return res
   pure 0
 where
@@ -37,14 +50,25 @@ where
     let funIdx := compiled.getFuncIdx testCase.functionName |>.get!
     let (output, ioBuffer, queryCounts) :=
       compiled.bytecode.execute funIdx testCase.input testCase.inputIOBuffer
-    let outputOk := output == testCase.expectedOutput
-    let ioOk := ioBuffer == testCase.expectedIOBuffer
-    if !outputOk then
+    if output != testCase.expectedOutput then
       IO.eprintln s!"{name}: output mismatch"
       return 1
-    if !ioOk then
+    if ioBuffer != testCase.expectedIOBuffer then
       IO.eprintln s!"{name}: IOBuffer mismatch"
       return 1
     let stats := Aiur.computeStats compiled queryCounts
     Aiur.printStats stats
     pure 0
+  interpCheck decls name env : IO UInt32 := do
+    IO.println s!"Interpreting {name}"
+    (← IO.getStdout).flush
+    let testCase ← kernelCheck name env
+    let funcName := Aiur.Global.mk testCase.functionName
+    let inputs := testCase.input.toList.map Aiur.Value.field
+    match Aiur.runFunction decls funcName inputs testCase.inputIOBuffer with
+    | .error e =>
+      IO.eprintln s!"{name}: interpreter error:\n{e}"
+      return 1
+    | .ok (output, _state) =>
+      IO.println s!"{name}: {output}"
+      pure 0

Tests/Aiur/Common.lean

@@ -6,6 +6,7 @@ public import Ix.Unsigned
 public import Ix.Aiur.Goldilocks
 public import Ix.Aiur.Protocol
 public import Ix.Aiur.Compiler
+public import Ix.Aiur.Interpret
 
 public section
 
@@ -18,6 +19,7 @@ structure AiurTestCase where
   expectedOutput : Array Aiur.G := #[]
   inputIOBuffer : Aiur.IOBuffer := default
   expectedIOBuffer : Aiur.IOBuffer := default
+  interpret : Bool := true
   executionOnly : Bool := false
 
 def AiurTestCase.noIO (functionName : Lean.Name)
@@ -26,7 +28,7 @@ def AiurTestCase.noIO (functionName : Lean.Name)
 
 def AiurTestCase.exec (functionName : Lean.Name)
     (input : Array Aiur.G := #[]) (expectedOutput : Array Aiur.G := #[]) : AiurTestCase :=
-  { functionName, input, expectedOutput, executionOnly := true }
+  { functionName, input, expectedOutput, interpret := false, executionOnly := true }
 
 def commitmentParameters : Aiur.CommitmentParameters := {
   logBlowup := 1
@@ -43,14 +45,36 @@ def friParameters : Aiur.FriParameters := {
 
 structure AiurTestEnv where
   compiled : Aiur.CompiledToplevel
+  decls : Aiur.Decls
   aiurSystem : Aiur.AiurSystem
 
 def AiurTestEnv.build (toplevelFn : Except Aiur.Global Aiur.Toplevel) :
     Except String AiurTestEnv := do
   let toplevel ← toplevelFn.mapError toString
   let compiled ← toplevel.compile
+  let decls ← toplevel.mkDecls.mapError toString
   let aiurSystem := Aiur.AiurSystem.build compiled.bytecode commitmentParameters
-  return ⟨compiled, aiurSystem⟩
+  return ⟨compiled, decls, aiurSystem⟩
+
+def AiurTestEnv.interpTest (env : AiurTestEnv) (testCase : AiurTestCase)
+    (execOutput : Array Aiur.G) (execIOBuffer : Aiur.IOBuffer) : TestSeq :=
+  let label := testCase.label
+  let funcName := Aiur.Global.mk testCase.functionName
+  let inputTypes := match env.decls.getByKey funcName with
+    | some (.function f) => f.inputs.map (·.2)
+    | _ => []
+  let inputs := Aiur.unflattenInputs env.decls testCase.input inputTypes
+  let funcIdx g := env.compiled.getFuncIdx g.toName
+  match Aiur.runFunction env.decls funcName inputs testCase.inputIOBuffer with
+  | .error e =>
+    test s!"Interpret succeeds for {label}: {e}" false
+  | .ok (output, state) =>
+    let flat := Aiur.flattenValue env.decls funcIdx output
+    let interpOutputTest := test s!"Interpret output matches for {label}"
+      (flat == execOutput)
+    let interpIOTest := test s!"Interpret IOBuffer matches for {label}"
+      (state.ioBuffer == execIOBuffer)
+    interpOutputTest ++ interpIOTest
 
 def AiurTestEnv.runTestCase (env : AiurTestEnv) (testCase : AiurTestCase) : TestSeq :=
   let label := testCase.label
@@ -62,7 +86,10 @@ def AiurTestEnv.runTestCase (env : AiurTestEnv) (testCase : AiurTestCase) : Test
   let execIOTest := test s!"Execute IOBuffer matches for {label}"
     (execIOBuffer == testCase.expectedIOBuffer)
   let execTest := execOutputTest ++ execIOTest
-  if testCase.executionOnly then execTest
+  let interpTest :=
+    if testCase.interpret then env.interpTest testCase execOutput execIOBuffer
+    else .done
+  if testCase.executionOnly then execTest ++ interpTest
   else
     let (claim, proof, ioBuffer) := env.aiurSystem.prove
       friParameters funIdx testCase.input testCase.inputIOBuffer
@@ -73,15 +100,16 @@ def AiurTestEnv.runTestCase (env : AiurTestEnv) (testCase : AiurTestCase) : Test
     let proof := .ofBytes proof.toBytes
     let pvTest := withExceptOk s!"Prove/verify works for {label}"
       (env.aiurSystem.verify friParameters claim proof) fun _ => .done
-    execTest ++ claimTest ++ ioTest ++ pvTest
+    execTest ++ interpTest ++ claimTest ++ ioTest ++ pvTest
 
 def mkAiurTests (toplevelFn : Except Aiur.Global Aiur.Toplevel)
     (cases : List AiurTestCase) : TestSeq :=
   withExceptOk "Toplevel merging succeeds" toplevelFn fun toplevel =>
     withExceptOk "Compilation succeeds" toplevel.compile fun compiled =>
-      let aiurSystem := Aiur.AiurSystem.build compiled.bytecode commitmentParameters
-      let env : AiurTestEnv := ⟨compiled, aiurSystem⟩
-      cases.foldl (init := .done) fun tSeq testCase =>
-        tSeq ++ env.runTestCase testCase
+      withExceptOk "mkDecls succeeds" (toplevel.mkDecls.mapError toString) fun decls =>
+        let aiurSystem := Aiur.AiurSystem.build compiled.bytecode commitmentParameters
+        let env : AiurTestEnv := ⟨compiled, decls, aiurSystem⟩
+        cases.foldl (init := .done) fun tSeq testCase =>
+          tSeq ++ env.runTestCase testCase
 
 end

Tests/Aiur/Hashes.lean

@@ -14,7 +14,8 @@ def mkBlake3HashTestCase (size : Nat) : AiurTestCase :=
   let output := outputBytes.map .ofUInt8
   let buffer := ⟨input, .ofList [(#[0], ⟨0, size⟩)]⟩ -- key is fixed as #[0]
   { functionName := `blake3_test, label := s!"blake3 (size={size})"
-    expectedOutput := output, inputIOBuffer := buffer, expectedIOBuffer := buffer }
+    expectedOutput := output, inputIOBuffer := buffer, expectedIOBuffer := buffer
+    interpret := false }
 
 def mkSha256HashTestCase (size : Nat) : AiurTestCase :=
   let inputBytes := Array.range size |>.map Nat.toUInt8
@@ -23,7 +24,8 @@ def mkSha256HashTestCase (size : Nat) : AiurTestCase :=
   let output := outputBytes.map .ofUInt8
   let buffer := ⟨input, .ofList [(#[0], ⟨0, size⟩)]⟩ -- key is fixed as #[0]
   { functionName := `sha256_test, label := s!"sha256 (size={size})"
-    expectedOutput := output, inputIOBuffer := buffer, expectedIOBuffer := buffer }
+    expectedOutput := output, inputIOBuffer := buffer, expectedIOBuffer := buffer
+    interpret := false }
 
 public def blake3TestCases : List AiurTestCase := [
   mkBlake3HashTestCase 0,

Tests/Aiur/RBTreeMap.lean

@@ -6,13 +6,14 @@ public import Ix.IxVM.RBTreeMap
 public section
 
 public def rbTreeMapTestCases : List AiurTestCase := [
-  .noIO `rbtree_map_test #[] #[
-    42,
-    50, 100, 200,
-    999,
-    10, 20, 30, 40, 50,
-    10, 20, 30, 40, 50,
-    200, 300, 400, 500, 600, 700, 800],
+  { AiurTestCase.noIO `rbtree_map_test #[] #[
+      42,
+      50, 100, 200,
+      999,
+      10, 20, 30, 40, 50,
+      10, 20, 30, 40, 50,
+      200, 300, 400, 500, 600, 700, 800]
+    with interpret := false },
 ]
 
 end

Tests/Ix/IxVM.lean

@@ -14,7 +14,7 @@ public def serdeNatAddComm (env : Lean.Environment) : IO AiurTestCase := do
     (ioBuffer.extend #[.ofNat i] (bytes.data.map .ofUInt8), i + 1)
   pure { functionName := `ixon_serde_test, label := "Ixon serde test"
          input := #[.ofNat n], inputIOBuffer := ioBuffer, expectedIOBuffer := ioBuffer
-         executionOnly := true }
+         interpret := false, executionOnly := true }
 
 public def kernelCheck (name : Lean.Name) (env : Lean.Environment) : IO AiurTestCase := do
   let constList := Lean.collectDependencies name env.constants
@@ -46,7 +46,7 @@ public def kernelCheck (name : Lean.Name) (env : Lean.Environment) : IO AiurTest
 
   pure { functionName := `kernel_check_test, label := s!"Kernel check {name}"
          input := targetAddrBytes, inputIOBuffer := ioBuffer, expectedIOBuffer := ioBuffer,
-         executionOnly := true }
+         interpret := false, executionOnly := true }
 
 public def kernelChecks (env : Lean.Environment) : IO (List AiurTestCase) :=
   -- List in strings to prevent instantiation errors (e.g. with numerical limbs)