Add secret key zero knowledge check to boardroom voting

* Implement the secret key zero knowledge check described in the
  original open vote network paper.
* Change BigZ.boardroom_axioms to only use BigZ for inner computation
* Remove unneeded BignumsSerializable, which is not necessary due to the
  switch above.

_CoqProject

@@ -12,7 +12,6 @@ execution/theories/ChainedList.v
 execution/theories/Circulation.v
 execution/theories/Containers.v
 execution/theories/ContractMonads.v
-execution/theories/Examples/BignumsSerializable.v
 execution/theories/Examples/BoardroomMath.v
 execution/theories/Examples/BoardroomVoting.v
 execution/theories/Examples/BoardroomVotingTest.v

execution/_CoqProject

@@ -12,7 +12,6 @@ theories/ChainedList.v
 theories/Circulation.v
 theories/Containers.v
 theories/ContractMonads.v
-theories/Examples/BignumsSerializable.v
 theories/Examples/BoardroomMath.v
 theories/Examples/BoardroomVoting.v
 theories/Examples/BoardroomVotingTest.v

execution/theories/Examples/BignumsSerializable.v

-From Bignums Require Import BigN.
-From Bignums Require Import BigZ.
-From Coq Require Import ZArith.
-From Coq Require Import DoubleType.
-Require Import Monads.
-Require Import Serializable.
-
-Section IntSer.
-  Definition int_serializable
-             (T := BigN.dom_t 0)
-             (to_Z : T -> Z)
-             (of_Z : Z -> T)
-             (of_to_Z : forall t, of_Z (to_Z t) = t) : Serializable T.
-  Proof.
-    refine
-      {| serialize t := serialize (to_Z t);
-         deserialize p := do z <- deserialize p; ret (of_Z z); |}.
-    intros x.
-    rewrite deserialize_serialize.
-    cbn.
-    now rewrite of_to_Z.
-  Defined.
-
-  (* Massive hack: ltac inside notation is only checked at expansion time.
-   This allows the proof below to work for Coq 8.10 where Bignums uses int63
-   and Coq 8.9 where Bignums uses int31 and int63 does not even exist. *)
-  Local Set Warnings "-non-reversible-notation".
-  Notation "'lazyexp' x" := ltac:(exact x) (at level 70).
-
-  Global Instance int_serializable_inst : Serializable (BigN.dom_t 0).
-  Proof.
-    first
-      [exact
-         (int_serializable
-            (lazyexp Int31.phi)
-            (lazyexp Int31.phi_inv)
-            (lazyexp Cyclic31.phi_inv_phi))|
-       exact
-         (int_serializable
-            (lazyexp Int63.to_Z)
-            (lazyexp Int63.of_Z)
-            (lazyexp Int63.of_to_Z))].
-  Defined.
-End IntSer.
-
-Global Instance zn2z_serializable {A} `{Serializable A} : Serializable (zn2z A).
-Proof.
-  refine
-    {| serialize w1 :=
-         serialize
-           match w1 with
-           | W0 => (0%nat, serialize tt)
-           | WW a b => (1%nat, serialize (a, b))
-           end;
-       deserialize p :=
-         do '(tag, p) <- deserialize p;
-         match tag with
-         | 0%nat => ret W0
-         | _ => do '(a, b) <- deserialize p;
-                ret (WW a b)
-         end |}.
-  intros.
-  rewrite deserialize_serialize.
-  cbn.
-  destruct x; auto.
-  now rewrite deserialize_serialize.
-Defined.
-Global Instance word_serializable {A} `{Serializable A} (n : nat) : Serializable (word A n) :=
-  (fix f (n : nat) :=
-     match n return (Serializable (word A n)) with
-     | 0%nat => _ : Serializable A
-     | S n => zn2z_serializable
-     end) n.
-
-Global Instance BigNw1_serializable : Serializable BigN.w1 := ltac:(apply zn2z_serializable).
-Global Instance BigNw2_serializable : Serializable BigN.w2 := ltac:(apply zn2z_serializable).
-Global Instance BigNw3_serializable : Serializable BigN.w3 := ltac:(apply zn2z_serializable).
-Global Instance BigNw4_serializable : Serializable BigN.w4 := ltac:(apply zn2z_serializable).
-Global Instance BigNw5_serializable : Serializable BigN.w5 := ltac:(apply zn2z_serializable).
-Global Instance BigNw6_serializable : Serializable BigN.w6 := ltac:(apply zn2z_serializable).
-Global Instance BigN_serializable : Serializable bigN.
-Proof.
-  refine
-    {| serialize n :=
-         match n with
-         | BigN.N0 i => serialize (0, serialize i)
-         | BigN.N1 w => serialize (1, serialize w)
-         | BigN.N2 w => serialize (2, serialize w)
-         | BigN.N3 w => serialize (3, serialize w)
-         | BigN.N4 w => serialize (4, serialize w)
-         | BigN.N5 w => serialize (5, serialize w)
-         | BigN.N6 w => serialize (6, serialize w)
-         | BigN.Nn n w => serialize (7, serialize (n, serialize w))
-         end%nat;
-       deserialize p :=
-         do '(tag, p) <- deserialize p;
-         match tag with
-         | 0 => option_map BigN.N0 (deserialize p)
-         | 1 => option_map BigN.N1 (deserialize p)
-         | 2 => option_map BigN.N2 (deserialize p)
-         | 3 => option_map BigN.N3 (deserialize p)
-         | 4 => option_map BigN.N4 (deserialize p)
-         | 5 => option_map BigN.N5 (deserialize p)
-         | 6 => option_map BigN.N6 (deserialize p)
-         | 7 => do '(n, p) <- deserialize p;
-                do w <- deserialize p;
-                ret (BigN.Nn n w)
-         | _ => None
-         end%nat |}.
-  intros [].
-  all: rewrite ?deserialize_serialize; cbn.
-  all: rewrite ?deserialize_serialize; easy.
-Defined.
-Global Instance BigZ_serializable : Serializable bigZ :=
-  Derive Serializable BigZ.t__rect<BigZ.Pos, BigZ.Neg>.

execution/theories/Examples/BoardroomMath.v

@@ -87,19 +87,24 @@ Class BoardroomAxioms {A : Type} :=
 
 Arguments BoardroomAxioms : clear implicits.
 
-Delimit Scope ffield_scope with ffield.
-
-Infix "==" := elmeq (at level 70) : ffield.
-Notation "a !== b" := (~(elmeq a b)) (at level 70) : ffield.
-Notation "0" := zero : ffield.
-Notation "1" := one : ffield.
-Infix "+" := add : ffield.
-Infix "*" := mul : ffield.
-Infix "^" := pow : ffield.
-Notation "a 'exp=' b" := (expeq a b) (at level 70) : ffield.
-Notation "a 'exp<>' b" := (~(expeq a b)) (at level 70) : ffield.
-
-Local Open Scope ffield.
+Delimit Scope broom_scope with broom.
+
+Module BoardroomMathNotations.
+  Infix "==" := elmeq (at level 70) : broom.
+  Infix "=?" := elmeqb (at level 70) : broom.
+  Notation "a !== b" := (~(elmeq a b)) (at level 70) : broom.
+  Notation "0" := zero : broom.
+  Notation "1" := one : broom.
+  Infix "+" := add : broom.
+  Infix "*" := mul : broom.
+  Infix "^" := pow : broom.
+  Notation "a 'exp=' b" := (expeq a b) (at level 70) : broom.
+  Notation "a 'exp<>' b" := (~(expeq a b)) (at level 70) : broom.
+End BoardroomMathNotations.
+
+Import BoardroomMathNotations.
+Local Open Scope broom.
+
 Global Instance oeq_equivalence {A : Type} (field : BoardroomAxioms A) : Equivalence expeq.
 Proof.
   unfold expeq.
@@ -111,7 +116,7 @@ Qed.
 
 Definition BoardroomAxioms_field_theory {A : Type} (field : BoardroomAxioms A) :
   field_theory
-    zero one
+    0 1
     add mul
     (fun x y => x + (opp y)) opp
     (fun x y => x * inv y) inv
@@ -165,18 +170,43 @@ Section WithBoardroomAxioms.
   Context {gen : Generator field}.
   Context {disc_log : DiscreteLog field gen}.
 
-  Add Field ff : (BoardroomAxioms_field_theory field).
-
-  Local Open Scope ffield.
-
-  Hint Resolve one_neq_zero pow_nonzero generator_nonzero inv_nonzero : core.
-
   Fixpoint prod (l : list A) : A :=
     match l with
     | [] => one
     | x :: xs => x * prod xs
     end.
 
+  Definition compute_public_key (sk : Z) : A :=
+    generator ^ sk.
+
+  Definition reconstructed_key (pks : list A) (n : nat) : A :=
+    let lprod := prod (firstn n pks) in
+    let rprod := inv (prod (skipn (S n) pks)) in
+    lprod * rprod.
+
+  Definition compute_public_vote (rk : A) (sk : Z) (sv : bool) : A :=
+    rk ^ sk * if sv then generator else 1.
+
+  Fixpoint bruteforce_tally_aux
+           (n : nat)
+           (votes_product : A) : option nat :=
+    if generator ^ (Z.of_nat n) =? votes_product then
+      Some n
+    else
+      match n with
+      | 0 => None
+      | S n => bruteforce_tally_aux n votes_product
+      end%nat.
+
+  Definition bruteforce_tally (votes : list A) : option nat :=
+    bruteforce_tally_aux (length votes) (prod votes).
+
+  Add Field ff : (BoardroomAxioms_field_theory field).
+
+  Local Open Scope broom.
+
+  Hint Resolve one_neq_zero pow_nonzero generator_nonzero inv_nonzero : core.
+
   Instance plus_expeq_proper : Proper (expeq ==> expeq ==> expeq) Z.add.
   Proof.
     intros x x' xeq y y' yeq.
@@ -299,31 +329,6 @@ Section WithBoardroomAxioms.
   Hint Resolve -> prod_units : core.
   Hint Resolve <- prod_units : core.
 
-  Definition compute_public_key (sk : Z) : A :=
-    generator ^ sk.
-
-  Definition reconstructed_key (pks : list A) (n : nat) : A :=
-    let lprod := prod (firstn n pks) in
-    let rprod := inv (prod (skipn (S n) pks)) in
-    lprod * rprod.
-
-  Definition compute_public_vote (rk : A) (sk : Z) (sv : bool) : A :=
-    rk ^ sk * if sv then generator else 1.
-
-  Fixpoint bruteforce_tally_aux
-           (n : nat)
-           (votes_product : A) : option nat :=
-    if elmeqb (generator ^ (Z.of_nat n)) votes_product then
-      Some n
-    else
-      match n with
-      | 0 => None
-      | S n => bruteforce_tally_aux n votes_product
-      end%nat.
-
-  Definition bruteforce_tally (votes : list A) : option nat :=
-    bruteforce_tally_aux (length votes) (prod votes).
-
   Lemma compute_public_key_unit sk :
     compute_public_key sk !== 0.
   Proof. apply pow_nonzero, generator_nonzero. Qed.
@@ -460,7 +465,7 @@ Section WithBoardroomAxioms.
     destruct (i <? j)%nat; lia.
   Qed.
 
-  Local Open Scope ffield.
+  Local Open Scope broom.
   Lemma mul_public_votes
         (sks : list Z)
         (votes : nat -> bool) :
@@ -1669,24 +1674,25 @@ Module BigZp.
 
   Hint Rewrite BigZ.spec_modulo : zsimpl.
 
-  Definition boardroom_axioms (p : bigZ) :
-    prime [p] -> BoardroomAxioms bigZ.
+  Local Open Scope Z.
+  Definition boardroom_axioms (p : Z) :
+    prime p -> BoardroomAxioms Z.
   Proof.
     intros isprime.
     pose proof (prime_ge_2 _ isprime).
     refine
-      {| elmeq a b := a mod p == b mod p;
+      {| elmeq a b := a mod p = b mod p;
          elmeqb a b := a mod p =? b mod p;
          zero := 0;
          one := 1;
          add a a' := (a + a') mod p;
          mul a a' := (a * a') mod p;
          opp a := p - a;
-         inv a := mod_inv a p;
-         pow a e := mod_pow a e p;
-         order := BigZ.to_Z p;
-      |}; unfold "==".
-    - intros x y; apply BigZ.eqb_spec.
+         inv a := [mod_inv (BigZ.of_Z a) (BigZ.of_Z p)];
+         pow a e := [mod_pow (BigZ.of_Z a) e (BigZ.of_Z p)];
+         order := p;
+      |}.
+    - intros x y; apply Z.eqb_spec.
     - lia.
     - constructor; auto.
       now intros a a' a'' -> ->.
@@ -1736,7 +1742,7 @@ Module BigZp.
     - intros a.
       autorewrite with zsimpl in *.
       rewrite Z.mod_mod by lia.
-      replace ([p] - [a] + [a])%Z with [p] by lia.
+      replace (p - a + a)%Z with p by lia.
       rewrite Z.mod_same, Z.mod_0_l; lia.
     - intros a anp.
       autorewrite with zsimpl in *.

execution/theories/Examples/BoardroomVotingTest.v

-From Bignums Require Import BigZ.
 From Coq Require Import Cyclic31.
 From Coq Require Import List.
 From Coq Require Import Znumtheory.
-Require Import BignumsSerializable.
 Require Import Blockchain.
 Require Import BoardroomMath.
 Require Import BoardroomVoting.
@@ -14,25 +12,26 @@ Require Import Monads.
 Require Import Serializable.
 
 Import ListNotations.
+Import BoardroomMathNotations.
 
-Local Open Scope bigZ.
-Local Open Scope ffield.
+Local Open Scope Z.
+Local Open Scope broom.
 (*
 Definition modulus : bigZ := 1552518092300708935130918131258481755631334049434514313202351194902966239949102107258669453876591642442910007680288864229150803718918046342632727613031282983744380820890196288509170691316593175367469551763119843371637221007210577919.
 Definition generator : bigZ := 2.
 *)
-Definition modulus : bigZ := 201697267445741585806196628073.
-Definition generator : bigZ := 3.
+Definition modulus : Z := 201697267445741585806196628073.
+Definition generator : Z := 3.
 
-Axiom modulus_prime : prime [modulus].
-Instance axioms : BoardroomAxioms bigZ := BigZp.boardroom_axioms modulus modulus_prime.
+Axiom modulus_prime : prime modulus.
+Instance axioms : BoardroomAxioms Z := BigZp.boardroom_axioms modulus modulus_prime.
 
 Lemma generator_nonzero : generator !== 0.
 Proof. discriminate. Qed.
 
 Axiom generator_is_generator :
   forall z,
-    z !== 0 ->
+    ~(z == 0) ->
     exists! (e : Z), (0 <= e < order - 1)%Z /\ pow generator e == z.
 
 Instance generator_instance : Generator axioms :=
@@ -40,7 +39,7 @@ Instance generator_instance : Generator axioms :=
      BoardroomMath.generator_nonzero := generator_nonzero;
      generator_generates := generator_is_generator; |}.
 
-Instance id_scheme : @VoteProofScheme bigZ :=
+Instance id_scheme : @VoteProofScheme Z :=
   {| make_vote_proof l n z b := 0%Z;
      verify_vote l n a z := true; |}.
 
@@ -48,7 +47,7 @@ Definition num_parties : nat := 7.
 Definition votes_for : nat := 4.
 
 (* a pseudo-random generator for secret keys *)
-Definition sk n := [pow ((BigZ.of_Z (Z.of_nat n) + 1234583932) * (modulus - 23241)) 159338231].
+Definition sk n := (Z.of_nat n + 1234583932) * (modulus - 23241)^159338231.
 
 (* Make a list of secret keys, here starting at i=7 *)
 Definition sks : list Z :=
@@ -62,12 +61,17 @@ Definition svs : list bool :=
                          (seq 0 (num_parties - votes_for)).
 
 (* Compute the public keys for each party *)
-Definition pks : list bigZ :=
+Definition pks : list Z :=
   Eval native_compute in map compute_public_key sks.
 
-(* Compute the signup messages that would be sent by each party *)
+Definition hash_func (l : list positive) : positive :=
+  countable.encode l.
+
+(* Compute the signup messages that would be sent by each party.
+   We just use the public key as the chosen randomness here. *)
 Definition signups : list Msg :=
-  Eval native_compute in map make_signup_msg sks.
+  Eval native_compute in map (fun '(sk, pk, i) => make_signup_msg hash_func sk 5 i)
+                             (zip (zip sks pks) (seq 0 (length sks))).
 
 (* Compute the submit_vote messages that would be sent by each party *)
 (* Our functional correctness proof assumes that the votes were computed
@@ -118,7 +122,7 @@ Definition boardroom_example :=
              block_reward := 50; |} in
       builder_add_block chain next_header acts in
   do chain <- add_block chain [];
-  let dep := build_act creator (create_deployment 0 (boardroom_voting BigZ.to_Z) deploy_setup) in
+  let dep := build_act creator (create_deployment 0 (boardroom_voting hash_func) deploy_setup) in
   do chain <- add_block chain [dep];
   do caddr <- hd None (map Some (FMap.keys (lc_contracts (lcb_lc chain))));
   let send addr m := build_act addr (act_call caddr 0 (serialize m)) in
@@ -128,7 +132,7 @@ Definition boardroom_example :=
   do chain <- add_block chain votes;
   let tally := build_act creator (act_call caddr 0 (serialize tally_votes)) in
   do chain <- add_block chain [tally];
-  do state <- @contract_state _ (@State _ bigZ) _ (lcb_lc chain) caddr;
+  do state <- @contract_state _ (@State _ Z) _ (lcb_lc chain) caddr;
   result state.
 
-Check (@eq_refl (option nat) (Some votes_for)) <: boardroom_example = Some votes_for.
+Check (@eq_refl (option nat) (Some votes_for)) <<: boardroom_example = Some votes_for.

execution/theories/Serializable.v

@@ -3,12 +3,14 @@ This format, SerializedValue, is either a unit/int/bool or a pair/list
 of these. We also define Serializable as a type class capturing that a
 type can be converted from and to this format. *)
 
-From Coq Require Import ZArith.
 Require Import Monads.
 Require Import Containers.
 Require Import Automation.
 Require Import BoundedN.
 From Coq Require Import List.
+From Coq Require Import Psatz.
+From Coq Require Import ZArith.
+From stdpp Require countable.
 
 Import ListNotations.
 
@@ -397,3 +399,158 @@ Notation "'Derive' 'Serializable' rect < c0 , .. , cn >" :=
      | [pairs := ?x |- _] => make_serializable rect x
      end))
     (at level 0, rect at level 10, c0, cn at level 9, only parsing).
+
+Section Countable.
+  Instance SerializedType_interp_EqDecision
+           (t : SerializedType) : stdpp.base.EqDecision (interp_type t).
+  Proof. induction t; typeclasses eauto. Defined.
+  Instance SerializedType_interp_Countable
+           (t : SerializedType) : countable.Countable (interp_type t).
+  Proof. induction t; typeclasses eauto. Defined.
+
+  Global Instance SerializedValue_EqDecision : stdpp.base.EqDecision SerializedValue.
+  Proof.
+    intros x y.
+    destruct x as [xt xv], y as [yt yv].
+    destruct (SerializedType.eq_dec xt yt) as [<-|?]; [|right; congruence].
+    destruct (stdpp.base.decide (xv = yv)).
+    - left.
+      congruence.
+    - right.
+      intros eq.
+      inversion eq.
+      congruence.
+  Defined.
+
+  Instance SerializedType_EqDecision : stdpp.base.EqDecision SerializedType.
+  Proof.
+    intros x y.
+    destruct (SerializedType.eq_dec x y) as [<-|?]; [left|right]; easy.
+  Defined.
+  Fixpoint depth st : nat :=
+    match st with
+    | ser_unit => 1
+    | ser_int => 1
+    | ser_bool => 1
+    | ser_pair x y => S (max (depth x) (depth y))
+    | ser_list x => S (depth x)
+    end.
+  Local Open Scope positive.
+  Fixpoint encode_st_body (st : SerializedType) : positive :=
+    match st with
+    | ser_unit => countable.encode (1, 1)
+    | ser_int => countable.encode (2, 1)
+    | ser_bool => countable.encode (3, 1)
+    | ser_pair x y => countable.encode (4, countable.encode (encode_st_body x, encode_st_body y))
+    | ser_list x => countable.encode (5, encode_st_body x)
+    end.
+  Definition encode_st (st : SerializedType) : positive :=
+    countable.encode (depth st, encode_st_body st).
+
+  Fixpoint decode_st_body (depth : nat) (p : positive) : option SerializedType :=
+    match depth with
+    | 0%nat => None
+    | S depth =>
+      do '(tag, body) <- countable.decode p;
+      match tag with
+      | 1 => ret ser_unit
+      | 2 => ret ser_int
+      | 3 => ret ser_bool
+      | 4 => do '(x, y) <- countable.decode body;
+             do x <- decode_st_body depth x;
+             do y <- decode_st_body depth y;
+             ret (ser_pair x y)
+      | 5 => do x <- decode_st_body depth body;
+             ret (ser_list x)
+      | _ => None
+      end
+    end.
+  Definition decode_st (p : positive) : option SerializedType :=
+    do '(depth, body) <- countable.decode p;
+    decode_st_body depth body.
+
+  Local Open Scope nat.
+  Lemma decode_st_body_encode_st_body (d : nat) (st : SerializedType) :
+    depth st <= d ->
+    decode_st_body d (encode_st_body st) = Some st.
+  Proof.
+    revert st.
+    induction d; intros st dle; cbn in *.
+    - exfalso.
+      induction st; cbn in *; lia.
+    - destruct st; auto; cbn in *.
+      + now rewrite !countable.decode_encode, !IHd by lia.
+      + now rewrite !countable.decode_encode, !IHd by lia.
+  Qed.
+
+  Lemma decode_st_encode_st (st : SerializedType) :
+    decode_st (encode_st st) = Some st.
+  Proof.
+    unfold decode_st, encode_st.
+    rewrite countable.decode_encode; cbn.
+    now apply decode_st_body_encode_st_body.
+  Qed.
+
+  Local Open Scope positive.
+  Instance SerializedType_Countable : countable.Countable SerializedType :=
+    {| countable.encode := encode_st;
+       countable.decode := decode_st;
+       countable.decode_encode := decode_st_encode_st |}.
+
+  Definition encode_sv (sv : SerializedValue) : positive :=
+    countable.encode (ser_value_type sv, countable.encode (ser_value sv)).
+
+  Definition decode_sv (p : positive) : option SerializedValue :=
+    do '(ty, p) <- countable.decode p;
+    do v <- countable.decode p;
+    ret {| ser_value_type := ty; ser_value := v |}.
+
+  Lemma decode_sv_encode_sv (sv : SerializedValue) :
+    decode_sv (encode_sv sv) = Some sv.
+  Proof.
+    unfold decode_sv, encode_sv.
+    rewrite countable.decode_encode; cbn.
+    rewrite countable.decode_encode; cbn.
+    reflexivity.
+  Qed.
+
+  Global Instance SerializedValue_Countable : countable.Countable SerializedValue :=
+    {| countable.encode := encode_sv;
+       countable.decode := decode_sv;
+       countable.decode_encode := decode_sv_encode_sv |}.
+
+  Global Instance SerializableType_EqDecision
+         (A : Type) `{Serializable A} : stdpp.base.EqDecision A.
+  Proof.
+    intros a a'.
+    destruct (stdpp.base.decide (serialize a = serialize a')) as [eq|neq].
+    - left.
+      now apply serialize_injective.
+    - right.
+      intros ->.
+      congruence.
+  Defined.
+
+  Definition encode_serializable_type {A : Type} `{Serializable A} (a : A) : positive :=
+    countable.encode (serialize a).
+
+  Definition decode_serializable_type {A : Type} `{Serializable A} (p : positive) : option A :=
+    countable.decode p >>= deserialize.
+
+  Lemma decode_serializable_type_encode_serializable_type
+        {A : Type} `{Serializable A}
+        (a : A) :
+    decode_serializable_type (encode_serializable_type a) = Some a.
+  Proof.
+    unfold decode_serializable_type, encode_serializable_type.
+    rewrite countable.decode_encode.
+    cbn.
+    now rewrite deserialize_serialize.
+  Qed.
+
+  Global Instance SerializableType_Countable {A : Type} `{Serializable A} :
+    countable.Countable A :=
+    {| countable.encode := encode_serializable_type;
+       countable.decode := decode_serializable_type;
+       countable.decode_encode := decode_serializable_type_encode_serializable_type; |}.
+End Countable.