Claim builder API and Prove CLI

Apps/ZKVoting/Prover.lean

@@ -1,52 +1,64 @@
-import Ix
-import Apps.ZKVoting.ProverInit
-import Apps.ZKVoting.Common
+import Ix.Claim
+import Ix.Address
+import Ix.Meta
+import Ix.CompileM
+import Batteries
 
-open Lean
+inductive Candidate
+   | alice | bob | charlie
+   deriving Inhabited, Lean.ToExpr, Repr, BEq, Ord
 
-partial def collectVotes (env : Environment) : IO $ List Vote :=
-  collectVotesLoop [] initSecret (0 : UInt64)
-where
-  collectVotesLoop votes secret count := do
-    let input := (← (← IO.getStdin).getLine).trim
-    let consts := env.constants
-    let voteAbe ← mkCommit secret Candidate.abe consts
-    let voteBam ← mkCommit secret Candidate.bam consts
-    let voteCot ← mkCommit secret Candidate.cot consts
-    IO.println s!"a: Abe | {voteAbe}"
-    IO.println s!"b: Bam | {voteBam}"
-    IO.println s!"b: Cot | {voteCot}"
-    IO.println "_: End voting"
-    let vote ← match input with
-      | "a" => pure voteAbe | "b" => pure voteBam | "c" => pure voteCot
-      | _ => return votes
-    let secret' := (← mkCommit secret count consts).adr
-    IO.println vote
-    collectVotesLoop (vote :: votes) secret' (count + 1)
+structure Result where
+  aliceVotes: Nat
+  bobVotes: Nat
+  charlieVotes: Nat
+deriving Repr, Lean.ToExpr
 
-structure VoteCounts where
-  abe : UInt64
-  bam : UInt64
-  cot : UInt64
-  deriving ToExpr
+def privateVotes : List Candidate := 
+  [.alice, .alice, .bob]
 
-def countVotes : List Vote → VoteCounts
-  | [] => ⟨0, 0, 0⟩
-  | vote :: votes =>
-    let counts := countVotes votes
-    match (reveal vote : Candidate) with
-    | .abe => { counts with abe := counts.abe + 1 }
-    | .bam => { counts with bam := counts.bam + 1 }
-    | .cot => { counts with cot := counts.cot + 1 }
+def runElection (votes: List Candidate) : Result :=
+  votes.foldr tally ⟨0,0,0⟩
+    where
+      tally (comm: Candidate) (res: Result): Result :=
+      match comm, res with
+      | .alice, ⟨a, b, c⟩ => ⟨a+1, b, c⟩
+      | .bob, ⟨a, b, c⟩ => ⟨a, b+1, c⟩
+      | .charlie, ⟨a, b, c⟩ => ⟨a, b, c+1⟩
+
+open Ix.Compile
 
 def main : IO UInt32 := do
-  let env ← get_env!
-  let votes ← collectVotes env
-  let .defnInfo countVotesDefn ← runCore (getConstInfo ``countVotes) env
-    | unreachable!
-  let claimValue := .app countVotesDefn.value (toExpr votes)
-  let claimType ← runMeta (Meta.inferType claimValue) env
-  let claimAdr := computeIxAddress (mkAnonDefInfoRaw claimType claimValue) env.constants
-  match ← prove claimAdr with
-  | .ok proof => IO.FS.writeBinFile proofPath $ Ixon.Serialize.put proof; return 0
-  | .error err => IO.eprintln $ toString err; return 1
+  let mut stt : CompileState := .init (<- get_env!)
+  -- simulate getting the votes from somewhere
+  let votes : List Candidate <- pure privateVotes
+  let mut as : List Lean.Name := []
+  -- default maxHeartBeats
+  let ticks : USize := 200000
+  -- the type of each vote to commit
+  let voteType := Lean.toTypeExpr Candidate
+  -- loop over the votes
+  for v in votes do
+    -- add each vote to our environment as a commitment
+    let (lvls, typ, val) <- runMeta (metaMakeDef v) stt.env
+    let ((addr, _), stt') <- (commitDef lvls typ val).runIO' ticks stt
+    stt := stt'
+    as := (Address.toUniqueName addr)::as
+    IO.println s!"vote: {repr v}, commitment: {addr}"
+  -- build a Lean list of our commitments as the argument to runElection
+  let arg : Lean.Expr <- runMeta (metaMakeList voteType as) stt.env
+  let (lvls, input, output, type, sort) <-
+    runMeta (metaMakeEvalClaim ``runElection [arg]) stt.env
+  let inputPretty <- runMeta (Lean.Meta.ppExpr input) stt.env
+  let outputPretty <- runMeta (Lean.Meta.ppExpr output) stt.env
+  let typePretty <- runMeta (Lean.Meta.ppExpr type) stt.env
+  IO.println s!"claim: {inputPretty}"
+  IO.println s!"  ~> {outputPretty}"
+  IO.println s!"  : {typePretty}"
+  IO.println s!"  @ {repr lvls}"
+  let ((claim,_,_,_), _stt') <-
+     (evalClaim lvls input output type sort true).runIO' ticks stt
+  IO.println s!"{claim}"
+  -- Ix.prove claim stt
+  return 0
+

Apps/ZKVoting/Verifier.lean

@@ -1,18 +1,18 @@
 import Ix.Ixon.Serialize
 import Ix.Prove
-import Apps.ZKVoting.Common
 
 def main (args : List String) : IO UInt32 := do
-  let mut votes := #[]
-  for commStr in args do
-    match Commitment.ofString commStr with
-    | none => IO.eprintln s!"Couldn't parse {commStr} as a commitment"; return 1
-    | some (comm : Vote) => votes := votes.push comm
-  let proofBytes ← IO.FS.readBinFile proofPath
-  match Ixon.Serialize.get proofBytes with
-  | .error err => IO.eprintln s!"Proof deserialization error: {err}"; return 1
-  | .ok (_proof : Proof) =>
-    -- TODO: print the resulting vote counts in the claim
-    -- TODO: assert that every vote in `votes` is in the proof claim
-    -- TODO: verify proof
+--  TODO
+--  let mut votes := #[]
+--  for commStr in args do
+--    match Commitment.ofString commStr with
+--    | none => IO.eprintln s!"Couldn't parse {commStr} as a commitment"; return 1
+--    | some (comm : Vote) => votes := votes.push comm
+--  let proofBytes ← IO.FS.readBinFile proofPath
+--  match Ixon.Serialize.get proofBytes with
+--  | .error err => IO.eprintln s!"Proof deserialization error: {err}"; return 1
+--  | .ok (_proof : Proof) =>
+--    -- TODO: print the resulting vote counts in the claim
+--    -- TODO: assert that every vote in `votes` is in the proof claim
+--    -- TODO: verify proof
     return 0

Ix.lean

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

Ix/Address.lean

@@ -9,33 +9,98 @@ structure Address where
   hash : ByteArray
   deriving Inhabited, Lean.ToExpr, BEq, Hashable
 
-def Address.ofChars (_adrChars : List Char) : Option Address :=
-  some default -- TODO
-
-def Address.ofString (adrStr: String) : Option Address :=
-  Address.ofChars adrStr.data
-
 def Address.blake3 (x: ByteArray) : Address := ⟨(Blake3.hash x).val⟩
 
-open Lean
+def hexOfNat : Nat -> Option Char
+| 0 => .some '0'
+| 1 => .some '1'
+| 2 => .some '2'
+| 3 => .some '3'
+| 4 => .some '4'
+| 5 => .some '5'
+| 6 => .some '6'
+| 7 => .some '7'
+| 8 => .some '8'
+| 9 => .some '9'
+| 10 => .some 'a'
+| 11 => .some 'b'
+| 12 => .some 'c'
+| 13 => .some 'd'
+| 14 => .some 'e'
+| 15 => .some 'f'
+|  _ => .none
+
+def natOfHex : Char -> Option Nat
+| '0' => .some 0
+| '1' => .some 1
+| '2' => .some 2
+| '3' => .some 3
+| '4' => .some 4
+| '5' => .some 5
+| '6' => .some 6
+| '7' => .some 7
+| '8' => .some 8
+| '9' => .some 9
+| 'a' => .some 10
+| 'b' => .some 11
+| 'c' => .some 12
+| 'd' => .some 13
+| 'e' => .some 14
+| 'f' => .some 15
+| 'A' => .some 10
+| 'B' => .some 11
+| 'C' => .some 12
+| 'D' => .some 13
+| 'E' => .some 14
+| 'F' => .some 15
+|  _ => .none
 
-/-- Convert a byte (UInt8) to a two‐digit hex string. -/
-def byteToHex (b : UInt8) : String :=
-  let hexDigits :=
-    #['0', '1', '2', '3', '4', '5', '6', '7', '8', '9', 'a', 'b', 'c', 'd', 'e', 'f']
-  let hi := hexDigits[(UInt8.toNat (b >>> 4))]!
-  let lo := hexDigits[(UInt8.toNat (b &&& 0xF))]!
-  String.mk [hi, lo]
+/-- Convert a byte (UInt8) to a two‐digit big-endian hexadecimal string. -/
+def hexOfByte (b : UInt8) : String :=
+  let hi := hexOfNat (UInt8.toNat (b >>> 4))
+  let lo := hexOfNat (UInt8.toNat (b &&& 0xF))
+  String.mk [hi.get!, lo.get!]
 
-/-- Convert a ByteArray to a hexadecimal string. -/
-def byteArrayToHex (ba : ByteArray) : String :=
-  (ba.toList.map byteToHex).foldl (· ++ ·) ""
+/-- Convert a ByteArray to a big-endian hexadecimal string. -/
+def hexOfBytes (ba : ByteArray) : String :=
+  (ba.toList.map hexOfByte).foldl (· ++ ·) ""
 
 instance : ToString Address where
-  toString adr := byteArrayToHex adr.hash
+  toString adr := hexOfBytes adr.hash
 
 instance : Repr Address where
   reprPrec a _ := "#" ++ (toString a).toFormat
 
 instance : Ord Address where
   compare a b := compare a.hash.data.toList b.hash.data.toList
+
+def byteOfHex : Char -> Char -> Option UInt8
+| hi, lo => do
+  let hi <- natOfHex hi
+  let lo <- natOfHex lo
+  UInt8.ofNat (hi <<< 4 + lo)
+
+def bytesOfHex (s: String) : Option ByteArray := do
+  let bs <- go s.toList
+  return ⟨bs.toArray⟩
+  where
+    go : List Char -> Option (List UInt8)
+    | hi::lo::rest => do
+      let b <- byteOfHex hi lo
+      let bs <- go rest
+      b :: bs
+    | [] => return []
+    | _ => .none
+
+def Address.fromString (s: String) : Option Address := do
+  let ba <- bytesOfHex s
+  if ba.size == 32 then .some ⟨ba⟩ else .none
+
+def Address.toUniqueName (addr: Address): Lean.Name :=
+  .str (.str (.str .anonymous "Ix") "_#") (hexOfBytes addr.hash)
+
+def Address.fromUniqueName (name: Lean.Name) : Option Address :=
+  match name with
+  | .str (.str (.str .anonymous "Ix") "_#") s => Address.fromString s
+  | _ => .none
+