WIP: jcb/ix vm

Cargo.toml

@@ -10,10 +10,10 @@ crate-type = ["staticlib"]
 anyhow = "1"
 indexmap = { version = "2", features = ["rayon"] }
 multi-stark = { git = "https://github.com/argumentcomputer/multi-stark.git", rev = "11a2e444004609174e1ad59e366e7f621bdd427b" }
-num-bigint = "0.4"
 rayon = "1"
 rustc-hash = "2"
 tiny-keccak = { version = "2", features = ["keccak"] }
+num-bigint = "0.4.6"
 blake3 = "1.8.2"
 # Iroh dependencies
 bytes = { version = "1.10.1", optional = true }
@@ -29,6 +29,11 @@ bincode = { version = "2.0.1", optional = true }
 serde = { version = "1.0.219", features = ["derive"], optional = true }
 
 
+[dev-dependencies]
+quickcheck = "1.0.3"
+rand = "0.8.5"
+quickcheck_macros = "1.0.0"
+
 [features]
 default = []
 parallel = ["multi-stark/parallel"]

Ix.lean

@@ -1,10 +1,8 @@
 -- This module serves as the root of the `Ix` library.
 -- Import modules here that should be built as part of the library.
 import Ix.Ixon
-import Ix.TransportM
-import Ix.IR
 import Ix.Meta
+import Ix.GroundM
+import Ix.CondenseM
 import Ix.CompileM
 import Ix.DecompileM
-import Ix.Claim
-import Ix.Prove

Ix/Address.lean

@@ -4,6 +4,7 @@ import Ix.Common
 import Blake3
 
 deriving instance Lean.ToExpr for ByteArray
+deriving instance Repr for ByteArray
 
 structure Address where
   hash : ByteArray
@@ -74,6 +75,9 @@ instance : Repr Address where
 instance : Ord Address where
   compare a b := compare a.hash.data.toList b.hash.data.toList
 
+instance : Inhabited Address where
+  default := Address.blake3 ⟨#[]⟩
+
 def byteOfHex : Char -> Char -> Option UInt8
 | hi, lo => do
   let hi <- natOfHex hi
@@ -104,3 +108,11 @@ def Address.fromUniqueName (name: Lean.Name) : Option Address :=
   | .str (.str (.str .anonymous "Ix") "_#") s => Address.fromString s
   | _ => .none
 
+structure MetaAddress where
+  data : Address
+  «meta» : Address
+  deriving Inhabited, Lean.ToExpr, BEq, Hashable, Repr, Ord
+
+instance : ToString MetaAddress where
+  toString adr := s!"{hexOfBytes adr.data.hash}:{hexOfBytes adr.meta.hash}"
+

Ix/Benchmark/Bench.lean

@@ -1,4 +1,4 @@
-import Ix.Claim
+import Ix.Ixon
 import Ix.Address
 import Ix.Meta
 import Ix.CompileM