feat: Poseidon2 hashing

Benchmarks/Poseidon2.lean

@@ -0,0 +1,66 @@
+import Ix.IxVM
+import Ix.Aiur.Simple
+import Ix.Aiur.Compile
+import Ix.Aiur.Protocol
+import Ix.Benchmark.Bench
+
+abbrev dataSizes := #[64, 128, 256, 512, 1024, 2048]
+abbrev numHashesPerProof := #[1, 2, 4, 8, 16, 32]
+
+def commitmentParameters : Aiur.CommitmentParameters := {
+  logBlowup := 1
+}
+
+def friParameters : Aiur.FriParameters := {
+  logFinalPolyLen := 0
+  numQueries := 100
+  commitProofOfWorkBits := 20
+  queryProofOfWorkBits := 0
+}
+
+def poseidon2Bench : IO $ Array BenchReport := do
+  let .ok ixVM := IxVM.ixVM
+    | throw (IO.userError "IxVM merging failed")
+  let some funIdx := ixVM.getFuncIdx `poseidon2_bench
+    | throw (IO.userError "Aiur function not found")
+  -- let .error err := ixVM.checkAndSimplify
+  --   | throw (IO.userError "Simplification failed")
+  -- println! err
+  let .ok decls := ixVM.checkAndSimplify
+    | throw (IO.userError "Simplification failed")
+  let aiurSystem := Aiur.AiurSystem.build decls.compile commitmentParameters
+
+  let mut benches := Array.emptyWithCapacity $ dataSizes.size * numHashesPerProof.size
+  for dataSize in dataSizes do
+    for numHashes in numHashesPerProof do
+      let ioBuffer := Array.range numHashes |>.foldl
+        (init := default)
+        fun ioBuffer idx =>
+          let data := Array.range dataSize |>.map
+            -- Add `idx` so every preimage is different and avoids memoization.
+            fun i => Aiur.G.ofUInt8 (i + idx).toUInt8
+          let ioKeyInfo := ⟨ioBuffer.data.size, dataSize⟩
+          { ioBuffer with
+              data := ioBuffer.data ++ data
+              map := ioBuffer.map.insert #[.ofNat idx] ioKeyInfo }
+      benches := benches.push <| bench s!"dataSize={dataSize} numHashes={numHashes}" (aiurSystem.prove friParameters funIdx #[Aiur.G.ofNat numHashes]) ioBuffer
+  bgroup "prove poseidon2" benches.toList { oneShot := true }
+
+def parseFunction (words : List String) (param : String): Option String :=
+  words.find? (·.startsWith param) |> .map (·.stripPrefix param)
+
+def main : IO Unit := do
+  let result ← poseidon2Bench
+
+  let mut sumWeights := 0.0
+  let mut weightedSum := 0.0
+  for report in result do
+    let words := report.function.splitOn
+    let dataSize := (parseFunction words "dataSize=").get!.toNat!
+    let numHashes := (parseFunction words "numHashes=").get!.toNat!
+    let sizeFloat := (dataSize * numHashes).toFloat
+    let throughput := sizeFloat / (report.newBench.getTime.toSeconds )
+    weightedSum := weightedSum + sizeFloat * throughput
+    sumWeights := sumWeights + sizeFloat
+  let avgThroughput := weightedSum / sumWeights
+  println! "Average throughput: {avgThroughput.toUSize} bytes/s"

Ix/IxVM.lean

@@ -1,6 +1,7 @@
 import Ix.Aiur.Meta
 import Ix.IxVM.ByteStream
 import Ix.IxVM.Blake3
+import Ix.IxVM.Poseidon2
 import Ix.IxVM.Ixon
 import Ix.IxVM.IxonSerialize
 import Ix.IxVM.IxonDeserialize
@@ -48,10 +49,23 @@ def entrypoints := ⟦
       _ => blake3_bench(num_hashes_pred),
     }
   }
+
+  fn poseidon2_bench(num_hashes: G) -> G {
+    let num_hashes_pred = num_hashes - 1;
+    let key = [num_hashes_pred];
+    let (idx, len) = io_get_info(key);
+    let byte_stream = read_byte_stream(idx, len);
+    let _x = poseidon2(byte_stream);
+    match num_hashes_pred {
+      0 => 0,
+      _ => poseidon2_bench(num_hashes_pred),
+    }
+  }
 ⟧
 
 def ixVM : Except Aiur.Global Aiur.Toplevel := do
   let vm ← byteStream.merge blake3
+  let vm ← vm.merge poseidon2
   let vm ← vm.merge ixon
   let vm ← vm.merge ixonSerialize
   let vm ← vm.merge ixonDeserialize