Commit a7836c1c authored by Jakob Botsch Nielsen's avatar Jakob Botsch Nielsen

Revert "Add secret key zero knowledge check to boardroom voting"

This reverts commit a582074c.
This needs some more work...
parent a582074c
Pipeline #18875 passed with stage
in 8 minutes and 44 seconds
......@@ -87,24 +87,19 @@ Class BoardroomAxioms {A : Type} :=
Arguments BoardroomAxioms : clear implicits.
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.
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.
Global Instance oeq_equivalence {A : Type} (field : BoardroomAxioms A) : Equivalence expeq.
Proof.
unfold expeq.
......@@ -116,7 +111,7 @@ Qed.
Definition BoardroomAxioms_field_theory {A : Type} (field : BoardroomAxioms A) :
field_theory
0 1
zero one
add mul
(fun x y => x + (opp y)) opp
(fun x y => x * inv y) inv
......@@ -170,43 +165,18 @@ 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.
......@@ -329,6 +299,31 @@ 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.
......@@ -465,7 +460,7 @@ Section WithBoardroomAxioms.
destruct (i <? j)%nat; lia.
Qed.
Local Open Scope broom.
Local Open Scope ffield.
Lemma mul_public_votes
(sks : list Z)
(votes : nat -> bool) :
......
......@@ -3,14 +3,12 @@ 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.
......@@ -399,158 +397,3 @@ 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.
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment