Claim builder API and Prove CLI #89
Conversation
- CompileM is now persistent with the filemapped store - constructing evaluation claims is done through MetaM rather than CompileM - CLI now features the Prove command
Apps/ZKVoting/Prover.lean
Outdated
| def runElection (votes: List Candidate) : Result := | ||
| let (a, b, c) := votes.foldr tally (0,0,0) | ||
| if a > b && a > c | ||
| then .winner .alice | ||
| else if b > a && b > c | ||
| then .winner .bob | ||
| else if c > a && c > b | ||
| then .winner .charlie | ||
| else if a == b && b == c | ||
| then .tie [.alice, .bob, .charlie] | ||
| else if a == b | ||
| then .tie [.alice, .bob] | ||
| else if a == c | ||
| then .tie [.alice, .charlie] | ||
| else .tie [.bob, .charlie] | ||
| where | ||
| tally (comm: Candidate) (acc: (Nat × Nat × Nat)): (Nat × Nat × Nat) := | ||
| match comm, acc 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) |
There was a problem hiding this comment.
For the typical use case of this kind of application, the end users are more interested in the raw vote counts so they can compute absolute and relative count diffs with ease. Here's a real example: https://resultados.tse.jus.br/oficial/app/index.html#/eleicao;e=e620;uf=sp;mu=71072;tipo=3/resultados
Also, there are elections with 50+ candidates. For example, when choosing deputies in Brazil. You can see where that would take the complexity of this kind of code to.
There was a problem hiding this comment.
Okay, updated with the Result holding the raw votes. Arguably this should be an RBMap Candidate Nat compare but that needs a ToExpr instance and a future step here is to extend https://github.com/leanprover/lean4/blob/045d07d2349b9989278991fbcd79a6430032930d/src/Lean/ToExpr.lean#L15-L32 in Ix.Common or Ix.Meta to allow users to use more data structures
| 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⟩ |
There was a problem hiding this comment.
It doesn't apply here, but direct recursion (as I had implemented it) is generally better than foldr/foldl/tail-recursion/etc in the IxVM due to auto-memoization. But it doesn't matter at this point. Just something to keep in mind as we want to showcase opinionated guidelines for writing efficient Lean code for our VM.
3 participants
No description provided.