chore: Digest → Address

Ix.lean

@@ -1,5 +1,4 @@
 -- This module serves as the root of the `Ix` library.
 -- Import modules here that should be built as part of the library.
-import Ix.Basic
 import Ix.Ixon
-
+import Ix.Prove

Ix/Address.lean

@@ -1,2 +1,15 @@
+import Lean
+
 structure Address where
   adr : ByteArray
+  deriving Inhabited
+
+open Lean
+
+instance : ToExpr ByteArray where
+  toExpr x   := mkApp (mkConst ``ByteArray.mk) (toExpr x.data)
+  toTypeExpr := mkConst ``ByteArray
+
+instance : ToExpr Address where
+  toExpr x   := mkApp (mkConst ``Address.mk) (toExpr x.adr)
+  toTypeExpr := mkConst ``Address

Ix/BuiltIn.lean

@@ -1,10 +1,10 @@
-import Ix.Basic
+import Ix.Address
 
 structure Commitment (α : Type) where
-  digest : Digest
+  adr : Address
   deriving Inhabited
 
-opaque commit (secret : Digest) (payload : α) : Commitment α
-opaque secret (comm : Commitment α) : Digest
+opaque commit (secret : Address) (payload : α) : Commitment α
+opaque secret (comm : Commitment α) : Address
 opaque reveal [Inhabited α] (comm : Commitment α) : α
 opaque revealThen [Inhabited β] (comm : Commitment α) (f : β) : β

Ix/Command.lean

@@ -1,19 +1,21 @@
 import Lean
-import Ix.Basic
+import Ix.Address
 
-def hashLeanExpr (_expr : Lean.Expr) (_constMap: Lean.ConstMap) : Digest :=
+def computeIxAddress (_expr : Lean.Expr) (_constMap: Lean.ConstMap) : Address :=
   default -- TODO
 
 open Lean Elab Term Command Meta
-elab "#ix" "hash" "⟦" stx:term "⟧" "as" name:ident : command => do
+
+/-- Compute the Ix `Address` of an expression and bind it to a name -/
+elab "#ix" "hash" stx:term "as" name:ident : command => do
   let constMap := (← getEnv).constants
   let expr ← liftTermElabM $ elabTerm stx none >>= instantiateExprMVars
-  let digest := hashLeanExpr expr constMap
+  let adr := computeIxAddress expr constMap
   let decl := Declaration.defnDecl {
     name        := name.getId
     levelParams := []
-    type        := mkConst ``ByteArray
-    value       := mkApp (mkConst ``ByteArray.mk) (toExpr digest.data)
+    type        := mkConst ``Address
+    value       := toExpr adr
     hints       := ReducibilityHints.opaque
     safety      := DefinitionSafety.safe
   }

Ix/Ixon.lean

@@ -1,5 +1,4 @@
 import Ix.Address
-import Lean.Declaration
 import Ix.Ixon.Serialize
 import Ix.Ixon.Univ
 import Ix.Ixon.Expr

Ix/Ixon/Const.lean

@@ -121,5 +121,4 @@ inductive Const where
   -- 0xCE
   | meta   : Metadata -> Const
 
-
 end Ixon

Ix/Ixon/Expr.lean

@@ -1,5 +1,4 @@
 import Ix.Address
-import Lean.Declaration
 import Ix.Ixon.Serialize
 import Ix.Ixon.Univ
 

Ix/Ixon/Univ.lean

@@ -1,4 +1,3 @@
-import Lean.Declaration
 import Ix.Ixon.Serialize
 
 namespace Ixon
@@ -42,7 +41,7 @@ def getUniv : GetM Univ := do
   go (st.bytes.size - st.index)
   where
     go : Nat → GetM Univ
-    | 0 => throw "Out of fuel" 
+    | 0 => throw "Out of fuel"
     | Nat.succ f => do
       let tagByte ← getUInt8
       let tag := UInt8.shiftRight tagByte 5

Ix/Basic.lean → Ix/Prove.lean

@@ -1,18 +1,16 @@
-import Std
-
-abbrev Digest := ByteArray
+import Ix.Address
 
 inductive ProveError
   | mk
 
 abbrev ProveM := ExceptT ProveError IO
 
 structure Proof where
-  inp : Digest
-  out : Digest
-  typ : Digest
+  inp : Address
+  out : Address
+  typ : Address
   bin : ByteArray
   deriving Inhabited
 
-def proveM (_hash : Digest) : ProveM Proof :=
+def proveM (_hash : Address) : ProveM Proof :=
   default -- TODO