diff options
| -rw-r--r-- | .travis.yml | 16 | ||||
| -rw-r--r-- | src/Algebra.v | 131 | ||||
| -rw-r--r-- | src/Experiments/EdDSARefinement.v | 35 | ||||
| -rw-r--r-- | src/Util/Tactics.v | 23 | ||||
| -rw-r--r-- | src/Util/Tuple.v | 62 |
5 files changed, 237 insertions, 30 deletions
diff --git a/.travis.yml b/.travis.yml index 5412f31a0..afbd96080 100644 --- a/.travis.yml +++ b/.travis.yml @@ -8,12 +8,26 @@ matrix: env: COQ_VERSION="8.5pl1" COQ_PACKAGE="coq-8.5pl1" COQPRIME="coqprime" PPA="ppa:jgross-h/many-coq-versions" - dist: trusty env: COQ_VERSION="8.5" COQ_PACKAGE="coq-8.5" COQPRIME="coqprime" PPA="ppa:jgross-h/many-coq-versions" + - dist: precise + env: COQ_VERSION="8.4pl6" COQ_PACKAGE="coq-8.4pl6 libcoq-ocaml-8.4pl6" COQPRIME="coqprime-8.4" PPA="ppa:jgross-h/many-coq-versions-ocaml-3-temp-while-over-quota-2" + - dist: precise + env: COQ_VERSION="8.4pl5" COQ_PACKAGE="coq-8.4pl5 libcoq-ocaml-8.4pl5" COQPRIME="coqprime-8.4" PPA="ppa:jgross-h/many-coq-versions-ocaml-3-temp-while-over-quota-2" + - dist: precise + env: COQ_VERSION="8.4pl4" COQ_PACKAGE="coq-8.4pl4 libcoq-ocaml-8.4pl4" COQPRIME="coqprime-8.4" PPA="ppa:jgross-h/many-coq-versions-ocaml-3-temp-while-over-quota-2" + - dist: precise + env: COQ_VERSION="8.4pl3" COQ_PACKAGE="coq-8.4pl3 libcoq-ocaml-8.4pl3" COQPRIME="coqprime-8.4" PPA="ppa:jgross-h/many-coq-versions-ocaml-3-temp-while-over-quota-2" + - dist: precise + env: COQ_VERSION="8.4pl2" COQ_PACKAGE="coq-8.4pl2 libcoq-ocaml-8.4pl2" COQPRIME="coqprime-8.4" PPA="ppa:jgross-h/many-coq-versions-ocaml-3-temp-while-over-quota-2" + - dist: precise + env: COQ_VERSION="8.4pl1" COQ_PACKAGE="coq-8.4pl1 libcoq-ocaml-8.4pl1" COQPRIME="coqprime-8.4" PPA="ppa:jgross-h/many-coq-versions-ocaml-3-temp-while-over-quota-2" + - dist: precise + env: COQ_VERSION="8.4" COQ_PACKAGE="coq-8.4 libcoq-ocaml-8.4" COQPRIME="coqprime-8.4" PPA="ppa:jgross-h/many-coq-versions-ocaml-3-temp-while-over-quota-2" - dist: trusty env: COQ_VERSION="8.4" COQ_PACKAGE="coq" COQPRIME="coqprime-8.4" PPA="" before_install: - if [ ! -z "$PPA" ]; then sudo add-apt-repository "$PPA" -y; fi - sudo apt-get update -q - - sudo apt-get install "$COQ_PACKAGE" -y + - sudo apt-get install $COQ_PACKAGE -y script: make COQPATH="$(pwd)/$COQPRIME" TIMED=1 -j2 diff --git a/src/Algebra.v b/src/Algebra.v index ef8e2850a..eca1b2bb1 100644 --- a/src/Algebra.v +++ b/src/Algebra.v @@ -636,6 +636,10 @@ End Field. (*** Tactics for manipulating field equations *) Require Import Coq.setoid_ring.Field_tac. +(** Convention: These tactics put the original goal first, and all + goals for non-zero side-conditions after that. (Exception: + [field_simplify_eq in], which is silly. *) + Ltac guess_field := match goal with | |- ?eq _ _ => constr:(_:field (eq:=eq)) @@ -664,7 +668,8 @@ Ltac common_denominator := end end. -Ltac common_denominator_in H := +(** We jump through some hoops to ensure that the side-conditions come late *) +Ltac common_denominator_in_cycled_side_condition_order H := let fld := guess_field in lazymatch type of fld with field (div:=?div) => @@ -674,6 +679,11 @@ Ltac common_denominator_in H := end end. +Ltac common_denominator_in H := + side_conditions_before_to_side_conditions_after + common_denominator_in_cycled_side_condition_order + H. + Ltac common_denominator_all := common_denominator; repeat match goal with [H: _ |- _ _ _ ] => progress common_denominator_in H end. @@ -724,12 +734,13 @@ Ltac set_nonfraction_pieces_on T eq zero opp add sub mul inv div nonzero_tac con | div ?numerator ?denominator => let d := fresh "d" in pose denominator as d; - assert (~eq d zero); - [ subst d; nonzero_tac - | set_nonfraction_pieces_on + cut (not (eq d zero)); + [ intro; + set_nonfraction_pieces_on numerator eq zero opp add sub mul inv div nonzero_tac ltac:(fun numerator' - => cont (div numerator' d)) ] + => cont (div numerator' d)) + | subst d; nonzero_tac ] | opp ?x => one_arg_recr opp x | inv ?x => one_arg_recr inv x | add ?x ?y => two_arg_recr add x y @@ -778,10 +789,10 @@ Ltac conservative_common_denominator_in H := lazymatch type of H with | appcontext[div] => set_nonfraction_pieces_in H; - [ .. - | common_denominator_in H; - [ repeat split; try assumption.. - | ] ]; + [ common_denominator_in H; + [ + | repeat apply conj; try assumption.. ] + | .. ]; repeat match goal with H := _ |- _ => subst H end | ?T => fail 0 "no division in" H ":" T end. @@ -795,19 +806,60 @@ Ltac conservative_common_denominator := lazymatch goal with | |- appcontext[div] => set_nonfraction_pieces; - [ .. - | common_denominator; - [ repeat split; try assumption.. - | ] ]; + [ common_denominator; + [ + | repeat apply conj; try assumption.. ] + | .. ]; repeat match goal with H := _ |- _ => subst H end | |- ?G => fail 0 "no division in goal" G end. +Ltac conservative_common_denominator_inequality_in H := + let HT := type of H in + lazymatch HT with + | not (?R _ _) => idtac + | (?R _ _ -> False)%type => idtac + | _ => fail 0 "Not an inequality" H ":" HT + end; + let HTT := type of HT in + let HT' := fresh in + evar (HT' : HTT); + let H' := fresh in + rename H into H'; + cut (not HT'); subst HT'; + [ intro H; clear H' + | let H'' := fresh in + intro H''; apply H'; conservative_common_denominator; [ eexact H'' | .. ] ]. +Ltac conservative_common_denominator_inequality := + let G := get_goal in + lazymatch G with + | not (?R _ _) => idtac + | (?R _ _ -> False)%type => idtac + | _ => fail 0 "Not an inequality (goal):" G + end; + let GT := type of G in + let HT' := fresh in + evar (HT' : GT); + let H' := fresh in + assert (H' : not HT'); subst HT'; + [ + | let HG := fresh in + intros HG; apply H'; conservative_common_denominator_in HG; [ eexact HG | .. ] ]. Ltac conservative_common_denominator_all := try conservative_common_denominator; - [ .. - | repeat match goal with [H: _ |- _ ] => progress conservative_common_denominator_in H; [] end ]. + [ repeat match goal with [H: _ |- _ ] => progress conservative_common_denominator_in H; [] end + | .. ]. + +Ltac conservative_common_denominator_inequality_all := + try conservative_common_denominator_inequality; + [ repeat match goal with [H: _ |- _ ] => progress conservative_common_denominator_inequality_in H; [] end + | .. ]. + +Ltac conservative_common_denominator_equality_inequality_all := + conservative_common_denominator_all; + [ conservative_common_denominator_inequality_all + | .. ]. Inductive field_simplify_done {T} : T -> Type := Field_simplify_done : forall H, field_simplify_done H. @@ -916,6 +968,55 @@ Ltac field_algebra := |trivial |apply Ring.opp_nonzero_nonzero;trivial]. +Ltac combine_field_inequalities_step := + match goal with + | [ H : not (?R ?x ?zero), H' : not (?R ?x' ?zero) |- _ ] + => pose proof (mul_nonzero_nonzero x x' H H'); clear H H' + | [ H : (?X -> False)%type |- _ ] + => change (not X) in H + end. + +(** First we split apart the equalities so that we can clear + duplicates; it's easier for us to do this than to give [nsatz] the + extra work. *) + +Ltac split_field_inequalities_step := + match goal with + | [ H : not (?R (?mul ?x ?y) ?zero) |- _ ] + => apply IntegralDomain.mul_nonzero_nonzero_iff in H; destruct H + end. +Ltac split_field_inequalities := + canonicalize_field_inequalities; + repeat split_field_inequalities_step; + clear_duplicates. + +Ltac combine_field_inequalities := + split_field_inequalities; + repeat combine_field_inequalities_step. +(** Handles field inequalities which can be made by splitting multiplications in the goal and the assumptions *) +Ltac solve_simple_field_inequalities := + repeat (apply conj || split_field_inequalities); + try assumption. +Ltac prensatz_contradict := + solve_simple_field_inequalities; + combine_field_inequalities. +Ltac nsatz_inequality_to_equality := + repeat intro; + match goal with + | [ H : not (?R ?x ?zero) |- False ] => apply H + | [ H : (?R ?x ?zero -> False)%type |- False ] => apply H + end. +(** Handles inequalities and fractions *) +Ltac super_nsatz := + (* [nsatz] gives anomalies on duplicate hypotheses, so we strip them *) + clear_algebraic_duplicates; + prensatz_contradict; + (* Each goal left over by [prensatz_contradict] is separate (and + there might not be any), so we handle them all separately *) + [ try conservative_common_denominator_equality_inequality_all; + [ try nsatz_inequality_to_equality; try nsatz + | repeat (apply conj || split_field_inequalities); try assumption; prensatz_contradict; nsatz_inequality_to_equality; try nsatz.. ].. ]. + Section ExtraLemmas. Context {F eq zero one opp add sub mul inv div} `{F_field:field F eq zero one opp add sub mul inv div}. Local Infix "+" := add. Local Infix "*" := mul. Local Infix "-" := sub. Local Infix "/" := div. diff --git a/src/Experiments/EdDSARefinement.v b/src/Experiments/EdDSARefinement.v index cf9083061..79c9b05dd 100644 --- a/src/Experiments/EdDSARefinement.v +++ b/src/Experiments/EdDSARefinement.v @@ -16,6 +16,7 @@ Section EdDSA. Local Notation valid := (@valid E Eeq Eadd EscalarMult b H l B Eenc Senc). Local Infix "*" := EscalarMult. Local Infix "+" := Eadd. Local Infix "++" := combine. Local Notation "P - Q" := (P + Eopp Q). + Local Arguments H {_} _. Context {Proper_Eenc : Proper (Eeq==>Logic.eq) Eenc}. Context {Proper_Eopp : Proper (Eeq==>Eeq) Eopp}. @@ -43,7 +44,7 @@ Section EdDSA. option_rect (fun _ => bool) (fun A : E => weqb (split1 b b sig) - (Eenc (S * B - (wordToNat (H (b + (b + mlen)) (split1 b b sig ++ pk ++ message))) mod l * A)) + (Eenc (S * B - (wordToNat (H (split1 b b sig ++ pk ++ message))) mod l * A)) ) false (decE pk) ) false (decS (split2 b b sig)) . @@ -93,4 +94,36 @@ Section EdDSA. | rewrite scalarmult_assoc, mult_comm, <-scalarmult_assoc, EdDSA_l_order_B, scalarmult_zero_r; reflexivity ]. Qed. + + Section ChangeRep. + Context {A Aeq Aadd Aid Aopp} {Agroup:@group A Aeq Aadd Aid Aopp}. + Context {EtoA} {Ahomom:@is_homomorphism E Eeq Eadd A Aeq Aadd EtoA}. + + Context {Aenc : A -> word b} {Proper_Aenc:Proper (Aeq==>Logic.eq) Aenc} + {Aenc_correct : forall P:E, Eenc P = Aenc (EtoA P)}. + + Context {S Seq} `{@Equivalence S Seq} {natToS:nat->S} + {SAmul:S->A->A} {Proper_SAmul: Proper (Seq==>Aeq==>Aeq) SAmul} + {SAmul_correct: forall n P, Aeq (EtoA (n*P)) (SAmul (natToS n) (EtoA P))} + {SdecS} {SdecS_correct : forall w, (decS w) = (SdecS w)} (* FIXME: equivalence relation *) + {natToS_modl : forall n, Seq (natToS (n mod l)) (natToS n)}. + + Definition verify_using_representation + {mlen} (message:word mlen) (pk:word b) (sig:word (b+b)) + : { answer | answer = verify message pk sig }. + Proof. + eexists. + cbv [verify]. + repeat ( + setoid_rewrite Aenc_correct + || setoid_rewrite homomorphism + || setoid_rewrite homomorphism_id + || setoid_rewrite (homomorphism_inv(INV:=Eopp)(inv:=Aopp)(eq:=Aeq)(phi:=EtoA)) + || setoid_rewrite SAmul_correct + || setoid_rewrite SdecS_correct + || setoid_rewrite natToS_modl + ). + reflexivity. + Defined. + End ChangeRep. End EdDSA. diff --git a/src/Util/Tactics.v b/src/Util/Tactics.v index 6826f638e..abfc2499c 100644 --- a/src/Util/Tactics.v +++ b/src/Util/Tactics.v @@ -228,3 +228,26 @@ Ltac destruct_sig_matcher HT := end. Ltac destruct_sig := destruct_all_matches destruct_sig_matcher. Ltac destruct_sig' := destruct_all_matches' destruct_sig_matcher. + +(** If [tac_in H] operates in [H] and leaves side-conditions before + the original goal, then + [side_conditions_before_to_side_conditions_after tac_in H] does + the same thing to [H], but leaves side-conditions after the + original goal. *) +Ltac side_conditions_before_to_side_conditions_after tac_in H := + let HT := type of H in + let HTT := type of HT in + let H' := fresh in + rename H into H'; + let HT' := fresh in + evar (HT' : HTT); + cut HT'; + [ subst HT'; intro H + | tac_in H'; + [ .. + | subst HT'; eexact H' ] ]; + instantiate; (* required in 8.4 for the [move] to succeed, because evar dependencies *) + [ (* We preserve the order of the hypotheses. We need to do this + here, after evars are instantiated, and not above. *) + move H after H'; clear H' + | .. ]. diff --git a/src/Util/Tuple.v b/src/Util/Tuple.v index d08c52c82..42a242fad 100644 --- a/src/Util/Tuple.v +++ b/src/Util/Tuple.v @@ -26,23 +26,39 @@ Definition to_list {T} (n:nat) : tuple T n -> list T := | S n' => fun xs : tuple T (S n') => to_list' n' xs end. -Fixpoint from_list' {T} (x:T) (xs:list T) : tuple' T (length xs) := - match xs with - | nil => x - | (y :: xs')%list => (from_list' y xs', x) +Program Fixpoint from_list' {T} (y:T) (n:nat) (xs:list T) : length xs = n -> tuple' T n := + match n return _ with + | 0 => + match xs return (length xs = 0 -> tuple' T 0) with + | nil => fun _ => y + | _ => _ (* impossible *) + end + | S n' => + match xs return (length xs = S n' -> tuple' T (S n')) with + | cons x xs' => fun _ => (from_list' x n' xs' _, y) + | _ => _ (* impossible *) + end end. -Definition from_list {T} (xs:list T) : tuple T (length xs) := - match xs as l return (tuple T (length l)) with - | nil => tt - | (t :: xs')%list => from_list' t xs' - end. +Program Definition from_list {T} (n:nat) (xs:list T) : length xs = n -> tuple T n := +match n return _ with +| 0 => + match xs return (length xs = 0 -> tuple T 0) with + | nil => fun _ : 0 = 0 => tt + | _ => _ (* impossible *) + end +| S n' => + match xs return (length xs = S n' -> tuple T (S n')) with + | cons x xs' => fun _ => from_list' x n' xs' _ + | _ => _ (* impossible *) + end +end. -Lemma to_list_from_list : forall {T} (xs:list T), to_list (length xs) (from_list xs) = xs. +Lemma to_list_from_list : forall {T} (n:nat) (xs:list T) pf, to_list n (from_list n xs pf) = xs. Proof. - destruct xs; auto; simpl. - generalize dependent t. - induction xs; auto; simpl; intros; f_equal; auto. + destruct xs; simpl; intros; subst; auto. + generalize dependent t. simpl in *. + induction xs; simpl in *; intros; congruence. Qed. Lemma length_to_list : forall {T} {n} (xs:tuple T n), length (to_list n xs) = n. @@ -52,6 +68,26 @@ Proof. destruct xs; simpl in *; eauto. Qed. +Lemma from_list'_to_list' : forall T n (xs:tuple' T n), + forall x xs' pf, to_list' n xs = cons x xs' -> + from_list' x n xs' pf = xs. +Proof. + induction n; intros. + { simpl in *. injection H; clear H; intros; subst. congruence. } + { destruct xs eqn:Hxs; + destruct xs' eqn:Hxs'; + injection H; clear H; intros; subst; try discriminate. + simpl. f_equal. eapply IHn. assumption. } +Qed. + +Lemma from_list_to_list : forall {T n} (xs:tuple T n) pf, from_list n (to_list n xs) pf = xs. +Proof. + destruct n; auto; intros; simpl in *. + { destruct xs; auto. } + { destruct (to_list' n xs) eqn:H; try discriminate. + eapply from_list'_to_list'; assumption. } +Qed. + Fixpoint fieldwise' {A B} (n:nat) (R:A->B->Prop) (a:tuple' A n) (b:tuple' B n) {struct n} : Prop. destruct n; simpl @tuple' in *. { exact (R a b). } |