aboutsummaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat
-rw-r--r--.gitignore11
-rw-r--r--.mailmap3
-rw-r--r--.travis.yml17
-rw-r--r--_CoqProject2
-rw-r--r--src/Algebra.v329
-rw-r--r--src/CompleteEdwardsCurve/CompleteEdwardsCurveTheorems.v25
-rw-r--r--src/CompleteEdwardsCurve/ExtendedCoordinates.v14
-rw-r--r--src/CompleteEdwardsCurve/Pre.v2
-rw-r--r--src/Experiments/DerivationsOptionRectLetInEncoding.v59
-rw-r--r--src/Experiments/EdDSARefinement.v96
-rw-r--r--src/Experiments/SpecEd25519.v8
-rw-r--r--src/Spec/EdDSA.v25
-rw-r--r--src/Tactics/Nsatz.v3
-rw-r--r--src/Util/Decidable.v35
-rw-r--r--src/Util/Option.v62
-rw-r--r--src/Util/Sum.v16
-rw-r--r--src/Util/Tactics.v28
-rw-r--r--src/Util/Tuple.v15
18 files changed, 618 insertions, 132 deletions
diff --git a/.gitignore b/.gitignore
index 9028c237e..f88b441c8 100644
--- a/.gitignore
+++ b/.gitignore
@@ -1,11 +1,10 @@
-bedrock
-fiat
+.#*
*~
*#
-*.vo
+*.aux
*.d
*.glob
-*.aux
-*.vio
-Makefile.coq
Makefile.bak
+Makefile.coq
+*.vio
+*.vo
diff --git a/.mailmap b/.mailmap
index c170ccdca..d481efdef 100644
--- a/.mailmap
+++ b/.mailmap
@@ -8,8 +8,9 @@ Andres Erbsen <andreser@mit.edu> Andres Erbsen <andres
Jade Philipoom <jadep@mit.edu> Jade Philipoom <jadep@mit.edu>
Jade Philipoom <jadep@mit.edu> jadep <jade.philipoom@gmail.com>
Jade Philipoom <jadep@mit.edu> jadep <jadep@mit.edu>
-Jason Gross <jgross@mit.edu> Jason Gross <jgross@mit.edu>
Jason Gross <jgross@mit.edu> Jason Gross <jagro@google.com>
+Jason Gross <jgross@mit.edu> Jason Gross <jasongross9@gmail.com>
+Jason Gross <jgross@mit.edu> Jason Gross <jgross@mit.edu>
Robert Sloan <varomodt@gmail.com> Robert Sloan <rsloan@sumologic.com>
Robert Sloan <varomodt@gmail.com> Robert Sloan <varomodt@dhcp-18-189-26-21.dyn.MIT.EDU>
Robert Sloan <varomodt@gmail.com> Robert Sloan <varomodt@dhcp-18-189-51-40.dyn.MIT.EDU>
diff --git a/.travis.yml b/.travis.yml
index 1092e385a..5412f31a0 100644
--- a/.travis.yml
+++ b/.travis.yml
@@ -1,16 +1,19 @@
language: generic
sudo: required
-dist: trusty
-env:
- matrix:
- - COQ_VERSION="8.4" COQPRIME="coqprime-8.4"
- - COQ_VERSION="8.5" COQPRIME="coqprime"
+matrix:
+ include:
+ - dist: trusty
+ 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: trusty
+ env: COQ_VERSION="8.4" COQ_PACKAGE="coq" COQPRIME="coqprime-8.4" PPA=""
before_install:
- - if [ "$COQ_VERSION" == "8.5" ]; then sudo add-apt-repository ppa:jgross-h/coq-backports -y; fi
+ - if [ ! -z "$PPA" ]; then sudo add-apt-repository "$PPA" -y; fi
- sudo apt-get update -q
- - sudo apt-get install coq -y
+ - sudo apt-get install "$COQ_PACKAGE" -y
script: make COQPATH="$(pwd)/$COQPRIME" TIMED=1 -j2
diff --git a/_CoqProject b/_CoqProject
index afad38124..904d716b8 100644
--- a/_CoqProject
+++ b/_CoqProject
@@ -29,6 +29,7 @@ src/Encoding/EncodingTheorems.v
src/Encoding/ModularWordEncodingPre.v
src/Encoding/ModularWordEncodingTheorems.v
src/Experiments/DerivationsOptionRectLetInEncoding.v
+src/Experiments/EdDSARefinement.v
src/Experiments/GenericFieldPow.v
src/Experiments/SpecEd25519.v
src/ModularArithmetic/ExtendedBaseVector.v
@@ -58,6 +59,7 @@ src/Util/ListUtil.v
src/Util/NatUtil.v
src/Util/Notations.v
src/Util/NumTheoryUtil.v
+src/Util/Option.v
src/Util/Sum.v
src/Util/Tactics.v
src/Util/Tuple.v
diff --git a/src/Algebra.v b/src/Algebra.v
index 15e0bcd38..ef8e2850a 100644
--- a/src/Algebra.v
+++ b/src/Algebra.v
@@ -1,12 +1,26 @@
Require Import Coq.Classes.Morphisms. Require Coq.Setoids.Setoid.
Require Import Crypto.Util.Tactics Crypto.Tactics.Nsatz.
+Require Import Crypto.Util.Decidable.
+Require Import Crypto.Util.Notations.
+Require Coq.Numbers.Natural.Peano.NPeano.
Local Close Scope nat_scope. Local Close Scope type_scope. Local Close Scope core_scope.
+Module Import ModuloCoq8485.
+ Import NPeano Nat.
+ Infix "mod" := modulo (at level 40, no associativity).
+End ModuloCoq8485.
+
+Notation is_eq_dec := (DecidableRel _) (only parsing).
+Notation "@ 'is_eq_dec' T R" := (DecidableRel (R:T->T->Prop))
+ (at level 10, T at level 8, R at level 8, only parsing).
+Notation eq_dec x y := (@dec (_ x y) _) (only parsing).
+Notation "x =? y" := (eq_dec x y) : type_scope.
+
Section Algebra.
Context {T:Type} {eq:T->T->Prop}.
Local Infix "=" := eq : type_scope. Local Notation "a <> b" := (not (a = b)) : type_scope.
- Class is_eq_dec := { eq_dec : forall x y : T, {x=y} + {x<>y} }.
+ Local Notation is_eq_dec := (@is_eq_dec T eq).
Section SingleOperation.
Context {op:T->T->T}.
@@ -206,7 +220,7 @@ Module Group.
Proof. eauto using Monoid.cancel_right, right_inverse. Qed.
Lemma inv_inv x : inv(inv(x)) = x.
Proof. eauto using Monoid.inv_inv, left_inverse. Qed.
- Lemma inv_op x y : (inv y*inv x)*(x*y) =id.
+ Lemma inv_op_ext x y : (inv y*inv x)*(x*y) =id.
Proof. eauto using Monoid.inv_op, left_inverse. Qed.
Lemma inv_unique x ix : ix * x = id -> ix = inv x.
@@ -217,6 +231,14 @@ Module Group.
- rewrite Hix, left_identity; reflexivity.
Qed.
+ Lemma inv_op x y : inv (x*y) = inv y*inv x.
+ Proof.
+ symmetry. etransitivity.
+ 2:eapply inv_unique.
+ 2:eapply inv_op_ext.
+ reflexivity.
+ Qed.
+
Lemma inv_id : inv id = id.
Proof. symmetry. eapply inv_unique, left_identity. Qed.
@@ -277,8 +299,8 @@ Module Group.
Admitted.
End Homomorphism.
- Section SurjectiveHomomorphism.
- Lemma surjective_homomorphism_group
+ Section GroupByHomomorphism.
+ Lemma surjective_homomorphism_from_group
{G EQ OP ID INV} {groupG:@group G EQ OP ID INV}
{H eq op id inv}
{Equivalence_eq: @Equivalence H eq} {eq_dec: forall x y, {eq x y} + {~ eq x y}}
@@ -286,9 +308,9 @@ Module Group.
{Proper_inv:Proper(eq==>eq)inv}
{phi iph} {Proper_phi:Proper(EQ==>eq)phi} {Proper_iph:Proper(eq==>EQ)iph}
{surj:forall h, phi (iph h) = h}
- {phi_op : forall a b, phi (OP a b) = op (phi a) (phi b)}
- {phi_inv : forall a, phi (INV a) = inv (phi a)}
- {phi_id : phi ID = id}
+ {phi_op : forall a b, eq (phi (OP a b)) (op (phi a) (phi b))}
+ {phi_inv : forall a, eq (phi (INV a)) (inv (phi a))}
+ {phi_id : eq (phi ID) id}
: @group H eq op id inv.
Proof.
repeat split; eauto with core typeclass_instances; intros;
@@ -303,7 +325,78 @@ Module Group.
repeat rewrite <-?phi_op, <-?phi_inv, <-?phi_id;
f_equiv; auto using associative, left_identity, right_identity, left_inverse, right_inverse.
Qed.
- End SurjectiveHomomorphism.
+
+ Lemma isomorphism_to_subgroup_group
+ {G EQ OP ID INV}
+ {Equivalence_EQ: @Equivalence G EQ} {eq_dec: forall x y, {EQ x y} + {~ EQ x y}}
+ {Proper_OP:Proper(EQ==>EQ==>EQ)OP}
+ {Proper_INV:Proper(EQ==>EQ)INV}
+ {H eq op id inv} {groupG:@group H eq op id inv}
+ {phi}
+ {eq_phi_EQ: forall x y, eq (phi x) (phi y) -> EQ x y}
+ {phi_op : forall a b, eq (phi (OP a b)) (op (phi a) (phi b))}
+ {phi_inv : forall a, eq (phi (INV a)) (inv (phi a))}
+ {phi_id : eq (phi ID) id}
+ : @group G EQ OP ID INV.
+ Proof.
+ repeat split; eauto with core typeclass_instances; intros;
+ eapply eq_phi_EQ;
+ repeat rewrite ?phi_op, ?phi_inv, ?phi_id;
+ auto using associative, left_identity, right_identity, left_inverse, right_inverse.
+ Qed.
+ End GroupByHomomorphism.
+
+ Section ScalarMult.
+ Context {G eq add zero opp} `{@group G eq add zero opp}.
+ Context {mul:nat->G->G}.
+ Local Infix "=" := eq : type_scope. Local Infix "=" := eq.
+ Local Infix "+" := add. Local Infix "*" := mul.
+ Class is_scalarmult :=
+ {
+ scalarmult_0_l : forall P, 0 * P = zero;
+ scalarmult_S_l : forall n P, S n * P = P + n * P;
+
+ scalarmult_Proper : Proper (Logic.eq==>eq==>eq) mul
+ }.
+ Global Existing Instance scalarmult_Proper.
+ Context `{is_scalarmult}.
+
+ Lemma scalarmult_1_l : forall P, 1*P = P.
+ Proof. intros. rewrite scalarmult_S_l, scalarmult_0_l, right_identity; reflexivity. Qed.
+
+ Lemma scalarmult_add_l : forall (n m:nat) (P:G), ((n + m)%nat * P = n * P + m * P).
+ Proof.
+ induction n; intros;
+ rewrite ?scalarmult_0_l, ?scalarmult_S_l, ?plus_Sn_m, ?plus_O_n, ?scalarmult_S_l, ?left_identity, <-?associative, <-?IHn; reflexivity.
+ Qed.
+
+ Lemma scalarmult_zero_r : forall m, m * zero = zero.
+ Proof. induction m; rewrite ?scalarmult_S_l, ?scalarmult_0_l, ?left_identity, ?IHm; try reflexivity. Qed.
+
+ Lemma scalarmult_assoc : forall (n m : nat) P, n * (m * P) = (m * n)%nat * P.
+ Proof.
+ induction n; intros.
+ { rewrite <-mult_n_O, !scalarmult_0_l. reflexivity. }
+ { rewrite scalarmult_S_l, <-mult_n_Sm, <-Plus.plus_comm, scalarmult_add_l. apply cancel_left, IHn. }
+ Qed.
+
+ Lemma opp_mul : forall n P, opp (n * P) = n * (opp P).
+ induction n; intros.
+ { rewrite !scalarmult_0_l, inv_id; reflexivity. }
+ { rewrite <-NPeano.Nat.add_1_l, Plus.plus_comm at 1.
+ rewrite scalarmult_add_l, scalarmult_1_l, inv_op, scalarmult_S_l, cancel_left; eauto. }
+ Qed.
+
+ Lemma scalarmult_times_order : forall l B, l*B = zero -> forall n, (l * n) * B = zero.
+ Proof. intros ? ? Hl ?. rewrite <-scalarmult_assoc, Hl, scalarmult_zero_r. reflexivity. Qed.
+
+ Lemma scalarmult_mod_order : forall l B, l <> 0%nat -> l*B = zero -> forall n, n mod l * B = n * B.
+ Proof.
+ intros ? ? Hnz Hmod ?.
+ rewrite (NPeano.Nat.div_mod n l Hnz) at 2.
+ rewrite scalarmult_add_l, scalarmult_times_order, left_identity by auto. reflexivity.
+ Qed.
+ End ScalarMult.
End Group.
Require Coq.nsatz.Nsatz.
@@ -551,6 +644,16 @@ Ltac guess_field :=
| [H: not (?eq _ _) |- _] => constr:(_:field (eq:=eq))
end.
+Ltac field_nonzero_mul_split :=
+ repeat match goal with
+ | [ H : ?R (?mul ?x ?y) ?zero |- _ ]
+ => apply IntegralDomain.mul_nonzero_nonzero_cases in H; destruct H
+ | [ |- not (?R (?mul ?x ?y) ?zero) ]
+ => apply IntegralDomain.mul_nonzero_nonzero_iff; split
+ | [ H : not (?R (?mul ?x ?y) ?zero) |- _ ]
+ => apply IntegralDomain.mul_nonzero_nonzero_iff in H; destruct H
+ end.
+
Ltac common_denominator :=
let fld := guess_field in
lazymatch type of fld with
@@ -575,6 +678,137 @@ Ltac common_denominator_all :=
common_denominator;
repeat match goal with [H: _ |- _ _ _ ] => progress common_denominator_in H end.
+(** Now we have more conservative versions that don't simplify non-division structure. *)
+Ltac deduplicate_nonfraction_pieces mul :=
+ repeat match goal with
+ | [ x0 := ?v, x1 := context[?v] |- _ ]
+ => progress change v with x0 in x1
+ | [ x := mul ?a ?b |- _ ]
+ => not is_var a;
+ let a' := fresh x in
+ pose a as a'; change a with a' in x
+ | [ x := mul ?a ?b |- _ ]
+ => not is_var b;
+ let b' := fresh x in
+ pose b as b'; change b with b' in x
+ | [ x0 := ?v, x1 := ?v |- _ ]
+ => change x1 with x0 in *; clear x1
+ | [ x := ?v |- _ ]
+ => is_var v; subst x
+ | [ x0 := mul ?a ?b, x1 := mul ?a ?b' |- _ ]
+ => subst x0 x1
+ | [ x0 := mul ?a ?b, x1 := mul ?a' ?b |- _ ]
+ => subst x0 x1
+ end.
+
+Ltac set_nonfraction_pieces_on T eq zero opp add sub mul inv div nonzero_tac cont :=
+ idtac;
+ let one_arg_recr :=
+ fun op v
+ => set_nonfraction_pieces_on
+ v eq zero opp add sub mul inv div nonzero_tac
+ ltac:(fun x => cont (op x)) in
+ let two_arg_recr :=
+ fun op v0 v1
+ => set_nonfraction_pieces_on
+ v0 eq zero opp add sub mul inv div nonzero_tac
+ ltac:(fun x
+ =>
+ set_nonfraction_pieces_on
+ v1 eq zero opp add sub mul inv div nonzero_tac
+ ltac:(fun y => cont (op x y))) in
+ lazymatch T with
+ | eq ?x ?y => two_arg_recr eq x y
+ | appcontext[div]
+ => lazymatch T with
+ | div ?numerator ?denominator
+ => let d := fresh "d" in
+ pose denominator as d;
+ assert (~eq d zero);
+ [ subst d; nonzero_tac
+ | set_nonfraction_pieces_on
+ numerator eq zero opp add sub mul inv div nonzero_tac
+ ltac:(fun numerator'
+ => cont (div numerator' d)) ]
+ | opp ?x => one_arg_recr opp x
+ | inv ?x => one_arg_recr inv x
+ | add ?x ?y => two_arg_recr add x y
+ | sub ?x ?y => two_arg_recr sub x y
+ | mul ?x ?y => two_arg_recr mul x y
+ | div ?x ?y => two_arg_recr div x y
+ | _ => idtac
+ end
+ | _ => let x := fresh "x" in
+ pose T as x;
+ cont x
+ end.
+Ltac set_nonfraction_pieces_in_by H nonzero_tac :=
+ idtac;
+ let fld := guess_field in
+ lazymatch type of fld with
+ | @field ?T ?eq ?zero ?one ?opp ?add ?sub ?mul ?inv ?div
+ => let T := type of H in
+ set_nonfraction_pieces_on
+ T eq zero opp add sub mul inv div nonzero_tac
+ ltac:(fun T' => change T' in H);
+ deduplicate_nonfraction_pieces mul
+ end.
+Ltac set_nonfraction_pieces_by nonzero_tac :=
+ idtac;
+ let fld := guess_field in
+ lazymatch type of fld with
+ | @field ?T ?eq ?zero ?one ?opp ?add ?sub ?mul ?inv ?div
+ => let T := get_goal in
+ set_nonfraction_pieces_on
+ T eq zero opp add sub mul inv div nonzero_tac
+ ltac:(fun T' => change T');
+ deduplicate_nonfraction_pieces mul
+ end.
+Ltac set_nonfraction_pieces_in H :=
+ set_nonfraction_pieces_in_by H ltac:(try (intro; field_nonzero_mul_split; try tauto)).
+Ltac set_nonfraction_pieces :=
+ set_nonfraction_pieces_by ltac:(try (intro; field_nonzero_mul_split; tauto)).
+Ltac conservative_common_denominator_in H :=
+ idtac;
+ let fld := guess_field in
+ let div := lazymatch type of fld with
+ | @field ?T ?eq ?zero ?one ?opp ?add ?sub ?mul ?inv ?div
+ => div
+ end in
+ lazymatch type of H with
+ | appcontext[div]
+ => set_nonfraction_pieces_in H;
+ [ ..
+ | common_denominator_in H;
+ [ repeat split; try assumption..
+ | ] ];
+ repeat match goal with H := _ |- _ => subst H end
+ | ?T => fail 0 "no division in" H ":" T
+ end.
+Ltac conservative_common_denominator :=
+ idtac;
+ let fld := guess_field in
+ let div := lazymatch type of fld with
+ | @field ?T ?eq ?zero ?one ?opp ?add ?sub ?mul ?inv ?div
+ => div
+ end in
+ lazymatch goal with
+ | |- appcontext[div]
+ => set_nonfraction_pieces;
+ [ ..
+ | common_denominator;
+ [ repeat split; try assumption..
+ | ] ];
+ repeat match goal with H := _ |- _ => subst H end
+ | |- ?G
+ => fail 0 "no division in goal" G
+ end.
+
+Ltac conservative_common_denominator_all :=
+ try conservative_common_denominator;
+ [ ..
+ | repeat match goal with [H: _ |- _ ] => progress conservative_common_denominator_in H; [] end ].
+
Inductive field_simplify_done {T} : T -> Type :=
Field_simplify_done : forall H, field_simplify_done H.
@@ -592,6 +826,21 @@ Ltac field_simplify_eq_hyps :=
Ltac field_simplify_eq_all := field_simplify_eq_hyps; try field_simplify_eq.
+(** Clear duplicate hypotheses, and hypotheses of the form [R x x] for a reflexive relation [R] *)
+Ltac clear_algebraic_duplicates_step R :=
+ match goal with
+ | [ H : R ?x ?x |- _ ]
+ => clear H
+ end.
+Ltac clear_algebraic_duplicates_guarded R :=
+ let test_reflexive := constr:(_ : Reflexive R) in
+ repeat clear_algebraic_duplicates_step R.
+Ltac clear_algebraic_duplicates :=
+ clear_duplicates;
+ repeat match goal with
+ | [ H : ?R ?x ?x |- _ ] => clear_algebraic_duplicates_guarded R
+ end.
+
(*** Inequalities over fields *)
Ltac assert_expr_by_nsatz H ty :=
let H' := fresh in
@@ -647,6 +896,16 @@ Ltac neq01 :=
|apply one_neq_zero
|apply Group.opp_one_neq_zero].
+Ltac conservative_field_algebra :=
+ intros;
+ conservative_common_denominator_all;
+ try (nsatz; dropRingSyntax);
+ repeat (apply conj);
+ try solve
+ [neq01
+ |trivial
+ |apply Ring.opp_nonzero_nonzero;trivial].
+
Ltac field_algebra :=
intros;
common_denominator_all;
@@ -675,8 +934,62 @@ Section ExtraLemmas.
Proof.
intros; setoid_subst z; eauto using only_two_square_roots'.
Qed.
+
+ Lemma only_two_square_roots'_choice x y : x * x = y * y -> x = y \/ x = opp y.
+ Proof.
+ intro H.
+ destruct (eq_dec x y); [ left; assumption | right ].
+ destruct (eq_dec x (opp y)); [ assumption | exfalso ].
+ eapply only_two_square_roots'; eassumption.
+ Qed.
+
+ Lemma only_two_square_roots_choice x y z : x * x = z -> y * y = z -> x = y \/ x = opp y.
+ Proof.
+ intros; setoid_subst z; eauto using only_two_square_roots'_choice.
+ Qed.
End ExtraLemmas.
+(** We look for hypotheses of the form [x^2 = y^2] and [x^2 = z] together with [y^2 = z], and prove that [x = y] or [x = opp y] *)
+Ltac pose_proof_only_two_square_roots x y H :=
+ not constr_eq x y;
+ match goal with
+ | [ H' : ?eq (?mul x x) (?mul y y) |- _ ]
+ => pose proof (only_two_square_roots'_choice x y H') as H
+ | [ H0 : ?eq (?mul x x) ?z, H1 : ?eq (?mul y y) ?z |- _ ]
+ => pose proof (only_two_square_roots_choice x y z H0 H1) as H
+ end.
+Ltac reduce_only_two_square_roots x y :=
+ let H := fresh in
+ pose_proof_only_two_square_roots x y H;
+ destruct H;
+ try setoid_subst y.
+Ltac pre_clean_only_two_square_roots :=
+ clear_algebraic_duplicates.
+(** Remove duplicates; solve goals by contradiction, and, if goals still remain, substitute the square roots *)
+Ltac post_clean_only_two_square_roots x y :=
+ clear_algebraic_duplicates;
+ try (unfold not in *;
+ match goal with
+ | [ H : (?T -> False)%type, H' : ?T |- _ ] => exfalso; apply H; exact H'
+ | [ H : (?R ?x ?x -> False)%type |- _ ] => exfalso; apply H; reflexivity
+ end);
+ try setoid_subst x; try setoid_subst y.
+Ltac only_two_square_roots_step :=
+ match goal with
+ | [ H : not (?eq ?x (?opp ?y)) |- _ ]
+ (* this one comes first, because it the procedure is asymmetric
+ with respect to [x] and [y], and this order is more likely to
+ lead to solving goals by contradiction. *)
+ => is_var x; is_var y; reduce_only_two_square_roots x y; post_clean_only_two_square_roots x y
+ | [ H : ?eq (?mul ?x ?x) (?mul ?y ?y) |- _ ]
+ => reduce_only_two_square_roots x y; post_clean_only_two_square_roots x y
+ | [ H : ?eq (?mul ?x ?x) ?z, H' : ?eq (?mul ?y ?y) ?z |- _ ]
+ => reduce_only_two_square_roots x y; post_clean_only_two_square_roots x y
+ end.
+Ltac only_two_square_roots :=
+ pre_clean_only_two_square_roots;
+ repeat only_two_square_roots_step.
+
Section Example.
Context {F 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/CompleteEdwardsCurve/CompleteEdwardsCurveTheorems.v b/src/CompleteEdwardsCurve/CompleteEdwardsCurveTheorems.v
index 476592b36..0afc07c5d 100644
--- a/src/CompleteEdwardsCurve/CompleteEdwardsCurveTheorems.v
+++ b/src/CompleteEdwardsCurve/CompleteEdwardsCurveTheorems.v
@@ -119,7 +119,7 @@ Module E.
| |- _ => split
| |- Feq _ _ => field_algebra
| |- _ <> 0 => expand_opp; solve [nsatz_nonzero|eauto 6]
- | |- {_}+{_} => eauto 15 using decide_and, @eq_dec with typeclass_instances
+ | |- Decidable.Decidable _ => solve [ typeclasses eauto ]
end.
Ltac bash := repeat bash_step.
@@ -138,25 +138,14 @@ Module E.
match goal with | |- _ <> 0 => admit end.
Admitted.
- (* TODO: move to [Group] and [AbelianGroup] as appropriate *)
- Lemma mul_0_l : forall P, (0 * P = zero)%E.
- Proof. intros; reflexivity. Qed.
- Lemma mul_S_l : forall n P, (S n * P = P + n * P)%E.
- Proof. intros; reflexivity. Qed.
- Lemma mul_add_l : forall (n m:nat) (P:point), ((n + m)%nat * P = n * P + m * P)%E.
+ Global Instance Proper_mul : Proper (Logic.eq==>eq==>eq) mul.
Proof.
- induction n; intros;
- rewrite ?plus_Sn_m, ?plus_O_n, ?mul_S_l, ?left_identity, <-?associative, <-?IHn; reflexivity.
+ intros n m Hnm P Q HPQ. rewrite <-Hnm; clear Hnm m.
+ induction n; simpl; rewrite ?IHn, ?HPQ; reflexivity.
Qed.
- Lemma mul_assoc : forall (n m : nat) P, (n * (m * P) = (n * m)%nat * P)%E.
- Proof.
- induction n; intros; [reflexivity|].
- rewrite ?mul_S_l, ?Mult.mult_succ_l, ?mul_add_l, ?IHn, commutative; reflexivity.
- Qed.
- Lemma mul_zero_r : forall m, (m * E.zero = E.zero)%E.
- Proof. induction m; rewrite ?mul_S_l, ?left_identity, ?IHm; try reflexivity. Qed.
- Lemma opp_mul : forall n P, (opp (n * P) = n * (opp P))%E.
- Admitted.
+
+ Global Instance mul_is_scalarmult : @is_scalarmult point eq add zero mul.
+ Proof. split; intros; reflexivity || typeclasses eauto. Qed.
Section PointCompression.
Local Notation "x ^ 2" := (x*x).
diff --git a/src/CompleteEdwardsCurve/ExtendedCoordinates.v b/src/CompleteEdwardsCurve/ExtendedCoordinates.v
index deeb795b1..364d7f9ec 100644
--- a/src/CompleteEdwardsCurve/ExtendedCoordinates.v
+++ b/src/CompleteEdwardsCurve/ExtendedCoordinates.v
@@ -63,6 +63,8 @@ Module Extended.
(let '(X,Y,Z,T) := coordinates P in ((X/Z), (Y/Z))) _.
Definition eq (P Q:point) := E.eq (to_twisted P) (to_twisted Q).
+ Global Instance DecidableRel_eq : Decidable.DecidableRel eq.
+ Proof. typeclasses eauto. Qed.
Local Hint Unfold from_twisted to_twisted eq : bash.
@@ -148,6 +150,18 @@ Module Extended.
Lemma homomorphism_from_twisted : @Group.is_homomorphism Epoint E.eq E.add point eq add from_twisted.
Proof. split; trivial using Proper_from_twisted, add_from_twisted. Qed.
+ Definition zero : point := from_twisted E.zero.
+ Definition opp P : point := from_twisted (E.opp (to_twisted P)).
+ Lemma extended_group : @group point eq add zero opp.
+ Proof.
+ eapply @isomorphism_to_subgroup_group; eauto with typeclass_instances core.
+ - apply DecidableRel_eq.
+ - unfold opp. repeat intro. match goal with [H:_|-_] => rewrite H; reflexivity end.
+ - intros. apply to_twisted_add.
+ - unfold opp; intros; rewrite to_twisted_from_twisted; reflexivity.
+ - unfold zero; intros; rewrite to_twisted_from_twisted; reflexivity.
+ Qed.
+
(* TODO: decide whether we still need those, then port *)
(*
Lemma unifiedAddM1_0_r : forall P, unifiedAddM1 P (mkExtendedPoint E.zero) === P.
diff --git a/src/CompleteEdwardsCurve/Pre.v b/src/CompleteEdwardsCurve/Pre.v
index be8ca24a2..be423c05c 100644
--- a/src/CompleteEdwardsCurve/Pre.v
+++ b/src/CompleteEdwardsCurve/Pre.v
@@ -41,7 +41,7 @@ Section Pre.
=> apply d_nonsquare with (sqrt_d:= (f (sqrt_a * x1) (d * x1 * x2 * y1 * y2 * y1))
/(f (sqrt_a * x2) y2 * x1 * y1 ))
| _ => apply a_nonzero
- end; field_algebra; auto using Ring.opp_nonzero_nonzero; intro; nsatz_contradict.
+ end; field_algebra; auto using Ring.opp_nonzero_nonzero; nsatz_contradict.
Qed.
Lemma edwardsAddCompletePlus x1 y1 x2 y2 :
diff --git a/src/Experiments/DerivationsOptionRectLetInEncoding.v b/src/Experiments/DerivationsOptionRectLetInEncoding.v
index e5b74085e..c0b6be25b 100644
--- a/src/Experiments/DerivationsOptionRectLetInEncoding.v
+++ b/src/Experiments/DerivationsOptionRectLetInEncoding.v
@@ -150,63 +150,6 @@ Proof.
end.
Qed.
-Global Instance option_rect_Proper_nd {A T}
- : Proper ((pointwise_relation _ eq) ==> eq ==> eq ==> eq) (@option_rect A (fun _ => T)).
-Proof.
- intros ?? H ??? [|]??; subst; simpl; congruence.
-Qed.
-
-Global Instance option_rect_Proper_nd' {A T}
- : Proper ((pointwise_relation _ eq) ==> eq ==> forall_relation (fun _ => eq)) (@option_rect A (fun _ => T)).
-Proof.
- intros ?? H ??? [|]; subst; simpl; congruence.
-Qed.
-
-Hint Extern 1 (Proper _ (@option_rect ?A (fun _ => ?T))) => exact (@option_rect_Proper_nd' A T) : typeclass_instances.
-
-Lemma option_rect_option_map : forall {A B C} (f:A->B) some none v,
- option_rect (fun _ => C) (fun x => some (f x)) none v = option_rect (fun _ => C) some none (option_map f v).
-Proof.
- destruct v; reflexivity.
-Qed.
-
-Lemma option_rect_function {A B C S' N' v} f
- : f (option_rect (fun _ : option A => option B) S' N' v)
- = option_rect (fun _ : option A => C) (fun x => f (S' x)) (f N') v.
-Proof. destruct v; reflexivity. Qed.
-Local Ltac commute_option_rect_Let_In := (* pull let binders out side of option_rect pattern matching *)
- idtac;
- lazymatch goal with
- | [ |- ?LHS = option_rect ?P ?S ?N (Let_In ?x ?f) ]
- => (* we want to just do a [change] here, but unification is stupid, so we have to tell it what to unfold in what order *)
- cut (LHS = Let_In x (fun y => option_rect P S N (f y))); cbv beta;
- [ set_evars;
- let H := fresh in
- intro H;
- rewrite H;
- clear;
- abstract (cbv [Let_In]; reflexivity)
- | ]
- end.
-
-(** TODO: possibly move me, remove local *)
-Local Ltac replace_option_match_with_option_rect :=
- idtac;
- lazymatch goal with
- | [ |- _ = ?RHS :> ?T ]
- => lazymatch RHS with
- | match ?a with None => ?N | Some x => @?S x end
- => replace RHS with (option_rect (fun _ => T) S N a) by (destruct a; reflexivity)
- end
- end.
-Local Ltac simpl_option_rect := (* deal with [option_rect _ _ _ None] and [option_rect _ _ _ (Some _)] *)
- repeat match goal with
- | [ |- context[option_rect ?P ?S ?N None] ]
- => change (option_rect P S N None) with N
- | [ |- context[option_rect ?P ?S ?N (Some ?x) ] ]
- => change (option_rect P S N (Some x)) with (S x); cbv beta
- end.
-
Definition COMPILETIME {T} (x:T) : T := x.
Lemma N_to_nat_le_mono : forall a b, (a <= b)%N -> (N.to_nat a <= N.to_nat b)%nat.
@@ -348,4 +291,4 @@ End with_unqualified_modulo2.
Lemma F_eqb_iff {q} : forall x y : F q, F_eqb x y = true <-> x = y.
Proof.
split; eauto using F_eqb_eq, F_eqb_complete.
-Qed.
+Qed. \ No newline at end of file
diff --git a/src/Experiments/EdDSARefinement.v b/src/Experiments/EdDSARefinement.v
new file mode 100644
index 000000000..cf9083061
--- /dev/null
+++ b/src/Experiments/EdDSARefinement.v
@@ -0,0 +1,96 @@
+Require Import Crypto.Spec.EdDSA Bedrock.Word.
+Require Import Coq.Classes.Morphisms.
+Require Import Crypto.Algebra. Import Group.
+Require Import Util.Decidable Util.Option Util.Tactics.
+Require Import Omega.
+
+Module Import NotationsFor8485.
+ Import NPeano Nat.
+ Infix "mod" := modulo (at level 40).
+End NotationsFor8485.
+
+Section EdDSA.
+ Context `{prm:EdDSA}.
+ Context {eq_dec:DecidableRel Eeq}.
+ Local Infix "==" := Eeq (at level 69, no associativity).
+ 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).
+
+ Context {Proper_Eenc : Proper (Eeq==>Logic.eq) Eenc}.
+ Context {Proper_Eopp : Proper (Eeq==>Eeq) Eopp}.
+ Context {Proper_Eadd : Proper (Eeq==>Eeq==>Eeq) Eadd}.
+
+ Context {decE:word b-> option E}.
+ Context {decS:word b-> option nat}.
+
+ Context {decE_canonical: forall x s, decE x = Some s -> x = Eenc s }.
+ Context {decS_canonical: forall x s, decS x = Some s -> x = Senc s }.
+
+ Context {decS_Senc: forall x, decS (Senc x) = Some x}.
+ Context {decE_Eenc: forall x, decE (Eenc x) = Some x}. (* FIXME: equivalence relation *)
+
+ Lemma solve_for_R : forall s B R n A, s * B == R + n * A <-> R == s*B - n*A.
+ Proof.
+ intros; split;
+ intro Heq; rewrite Heq; clear Heq.
+ { rewrite <-associative, right_inverse, right_identity; reflexivity. }
+ { rewrite <-associative, left_inverse, right_identity; reflexivity. }
+ Qed.
+
+ Definition verify {mlen} (message:word mlen) (pk:word b) (sig:word (b+b)) : bool :=
+ option_rect (fun _ => bool) (fun S : nat =>
+ 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))
+ ) false (decE pk)
+ ) false (decS (split2 b b sig))
+ .
+
+ Lemma verify_correct mlen (message:word mlen) (pk:word b) (sig:word (b+b)) :
+ verify message pk sig = true <-> valid message pk sig.
+ Proof.
+ cbv [verify option_rect option_map].
+ split.
+ {
+ repeat match goal with
+ | |- false = true -> _ => let H:=fresh "H" in intro H; discriminate H
+ | [H: _ |- _ ] => apply decS_canonical in H
+ | [H: _ |- _ ] => apply decE_canonical in H
+ | _ => rewrite weqb_true_iff
+ | _ => break_match
+ end.
+ intro.
+ subst.
+ rewrite <-combine_split.
+ rewrite Heqo.
+ rewrite H0.
+ constructor.
+ rewrite <-H0.
+ rewrite solve_for_R.
+ reflexivity.
+ }
+ {
+ intros [? ? ? ? Hvalid].
+ rewrite solve_for_R in Hvalid.
+ rewrite split1_combine.
+ rewrite split2_combine.
+ rewrite decS_Senc.
+ rewrite decE_Eenc.
+ rewrite weqb_true_iff.
+ f_equiv. exact Hvalid.
+ }
+ Qed.
+
+ Lemma sign_valid : forall A_ sk {n} (M:word n), A_ = public sk -> valid M A_ (sign A_ sk M).
+ Proof.
+ cbv [sign public]. intros. subst. split.
+ rewrite scalarmult_mod_order, scalarmult_add_l, cancel_left, scalarmult_mod_order, NPeano.Nat.mul_comm, scalarmult_assoc;
+ try solve [ reflexivity
+ | pose proof EdDSA_l_odd; omega
+ | apply EdDSA_l_order_B
+ | rewrite scalarmult_assoc, mult_comm, <-scalarmult_assoc,
+ EdDSA_l_order_B, scalarmult_zero_r; reflexivity ].
+ Qed.
+End EdDSA.
diff --git a/src/Experiments/SpecEd25519.v b/src/Experiments/SpecEd25519.v
index 4e30313d9..659a0ec66 100644
--- a/src/Experiments/SpecEd25519.v
+++ b/src/Experiments/SpecEd25519.v
@@ -149,11 +149,11 @@ Local Infix "*" := (E.mul(H0:=curve25519params)).
Axiom H : forall n : nat, word n -> word (b + b).
Axiom B : point. (* TODO: B = decodePoint (y=4/5, x="positive") *)
Axiom B_nonzero : B <> zero.
-Axiom l_order_B : l * B = zero.
-Axiom point_encoding : canonical encoding of point as word b.
-Axiom scalar_encoding : canonical encoding of {n : nat | n < l} as word b.
+Axiom l_order_B : E.eq (l * B) zero.
+Axiom Eenc : point -> word b.
+Axiom Senc : nat -> word b.
-Global Instance Ed25519 : @EdDSA point E.eq add zero E.opp E.mul b H c n l B point_encoding scalar_encoding :=
+Global Instance Ed25519 : @EdDSA point E.eq add zero E.opp E.mul b H c n l B Eenc Senc :=
{
EdDSA_c_valid := c_valid;
EdDSA_n_ge_c := n_ge_c;
diff --git a/src/Spec/EdDSA.v b/src/Spec/EdDSA.v
index c28ff0482..03a723e10 100644
--- a/src/Spec/EdDSA.v
+++ b/src/Spec/EdDSA.v
@@ -1,4 +1,3 @@
-Require Import Crypto.Spec.Encoding.
Require Bedrock.Word Crypto.Util.WordUtil.
Require Coq.ZArith.Znumtheory Coq.ZArith.BinInt.
Require Coq.Numbers.Natural.Peano.NPeano.
@@ -33,11 +32,12 @@ Section EdDSA.
{B : E} (* base point *)
- {PointEncoding : canonical encoding of E as Word.word b} (* wire format *)
- {FlEncoding : canonical encoding of { n | n < l } as Word.word b}
+ {Eenc : E -> Word.word b} (* normative encoding of elliptic cuve points *)
+ {Senc : nat -> Word.word b} (* normative encoding of scalars *)
:=
{
EdDSA_group:@Algebra.group E Eeq Eadd Ezero Eopp;
+ EdDSA_scalarmult:@Algebra.Group.is_scalarmult E Eeq Eadd Ezero EscalarMult;
EdDSA_c_valid : c = 2 \/ c = 3;
@@ -48,13 +48,14 @@ Section EdDSA.
EdDSA_l_prime : Znumtheory.prime (BinInt.Z.of_nat l);
EdDSA_l_odd : l > 2;
- EdDSA_l_order_B : EscalarMult l B = Ezero
+ EdDSA_l_order_B : Eeq (EscalarMult l B) Ezero
}.
Global Existing Instance EdDSA_group.
+ Global Existing Instance EdDSA_scalarmult.
Context `{prm:EdDSA}.
- Local Infix "=" := Eeq.
+ Local Infix "=" := Eeq : type_scope.
Local Coercion Word.wordToNat : Word.word >-> nat.
Local Notation secretkey := (Word.word b) (only parsing).
Local Notation publickey := (Word.word b) (only parsing).
@@ -75,18 +76,18 @@ Section EdDSA.
Local Infix "*" := EscalarMult.
Definition prngKey (sk:secretkey) : Word.word b := Word.split2 b b (H sk).
- Definition public (sk:secretkey) : publickey := enc (curveKey sk*B).
+ Definition public (sk:secretkey) : publickey := Eenc (curveKey sk*B).
Program Definition sign (A_:publickey) sk {n} (M : Word.word n) :=
let r : nat := H (prngKey sk ++ M) in (* secret nonce *)
let R : E := r * B in (* commitment to nonce *)
let s : nat := curveKey sk in (* secret scalar *)
- let S : {n|n<l} := exist _ ((r + H (enc R ++ public sk ++ M) * s) mod l) _ in
- enc R ++ enc S.
+ let S : nat := (r + H (Eenc R ++ A_ ++ M) * s) mod l in
+ Eenc R ++ Senc S.
(* For a [n]-bit [message] from public key [A_], validity of a signature [R_ ++ S_] *)
Inductive valid {n:nat} : Word.word n -> publickey -> signature -> Prop :=
- ValidityRule : forall (message:Word.word n) (A:E) (R:E) (S:nat) S_lt_l,
- S * B = R + (H (enc R ++ enc A ++ message) mod l) * A
- -> valid message (enc A) (enc R ++ enc (exist _ S S_lt_l)).
-End EdDSA.
+ ValidityRule : forall (message:Word.word n) (A:E) (R:E) (S:nat),
+ S * B = R + (H (Eenc R ++ Eenc A ++ message) mod l) * A
+ -> valid message (Eenc A) (Eenc R ++ Senc S).
+End EdDSA. \ No newline at end of file
diff --git a/src/Tactics/Nsatz.v b/src/Tactics/Nsatz.v
index 84d472e54..04f35c200 100644
--- a/src/Tactics/Nsatz.v
+++ b/src/Tactics/Nsatz.v
@@ -85,7 +85,8 @@ Ltac nsatz_clear_duplicates_for_bug_4851 domain :=
Ltac nsatz_nonzero :=
try solve [apply Integral_domain.integral_domain_one_zero
|apply Integral_domain.integral_domain_minus_one_zero
- |trivial].
+ |trivial
+ |assumption].
Ltac nsatz_domain_sugar_power domain sugar power :=
let nparams := constr:(BinInt.Zneg BinPos.xH) in (* some symbols can be "parameters", treated as coefficients *)
diff --git a/src/Util/Decidable.v b/src/Util/Decidable.v
index 726b52b6b..c2094c765 100644
--- a/src/Util/Decidable.v
+++ b/src/Util/Decidable.v
@@ -14,7 +14,7 @@ Ltac destruct_decidable_step :=
end.
Ltac destruct_decidable := repeat destruct_decidable_step.
-Local Ltac pre_decide :=
+Ltac pre_decide :=
repeat (intros
|| destruct_decidable
|| subst
@@ -22,34 +22,34 @@ Local Ltac pre_decide :=
|| unfold Decidable in *
|| hnf ).
-Local Ltac solve_decidable_transparent_with tac :=
+Ltac solve_decidable_transparent_with tac :=
pre_decide;
try solve [ left; abstract tac
| right; abstract tac
| decide equality; eauto with nocore ].
-Local Ltac solve_decidable_transparent := solve_decidable_transparent_with firstorder.
+Ltac solve_decidable_transparent := solve_decidable_transparent_with firstorder.
Local Hint Extern 0 => solve [ solve_decidable_transparent ] : typeclass_instances.
-Global Instance dec_True : Decidable True := left I.
-Global Instance dec_False : Decidable False := right (fun x => x).
-Global Instance dec_or {A B} `{Decidable A, Decidable B} : Decidable (A \/ B). exact _. Defined.
-Global Instance dec_and {A B} `{Decidable A, Decidable B} : Decidable (A /\ B). exact _. Defined.
-Global Instance dec_impl {A B} `{Decidable (B \/ ~A)} : Decidable (A -> B) | 3. exact _. Defined.
-Global Instance dec_impl_simple {A B} `{Decidable A, Decidable B} : Decidable (A -> B). exact _. Defined.
-Global Instance dec_iff {A B} `{Decidable A, Decidable B} : Decidable (A <-> B). exact _. Defined.
+Global Instance dec_True : Decidable True | 10 := left I.
+Global Instance dec_False : Decidable False | 10 := right (fun x => x).
+Global Instance dec_or {A B} `{Decidable A, Decidable B} : Decidable (A \/ B) | 10. exact _. Defined.
+Global Instance dec_and {A B} `{Decidable A, Decidable B} : Decidable (A /\ B) | 10. exact _. Defined.
+Global Instance dec_impl {A B} `{Decidable (B \/ ~A)} : Decidable (A -> B) | 10. exact _. Defined.
+Global Instance dec_impl_simple {A B} `{Decidable A, Decidable B} : Decidable (A -> B) | 10. exact _. Defined.
+Global Instance dec_iff {A B} `{Decidable A, Decidable B} : Decidable (A <-> B) | 10. exact _. Defined.
Lemma dec_not {A} `{Decidable A} : Decidable (~A).
Proof. solve_decidable_transparent. Defined.
(** Disallow infinite loops of dec_not *)
Hint Extern 0 (Decidable (~?A)) => apply (@dec_not A) : typeclass_instances.
-Global Instance dec_eq_unit : DecidableRel (@eq unit). exact _. Defined.
-Global Instance dec_eq_bool : DecidableRel (@eq bool). exact _. Defined.
-Global Instance dec_eq_Empty_set : DecidableRel (@eq Empty_set). exact _. Defined.
-Global Instance dec_eq_nat : DecidableRel (@eq nat). exact _. Defined.
-Global Instance dec_eq_prod {A B} `{DecidableRel (@eq A), DecidableRel (@eq B)} : DecidableRel (@eq (A * B)). exact _. Defined.
-Global Instance dec_eq_sum {A B} `{DecidableRel (@eq A), DecidableRel (@eq B)} : DecidableRel (@eq (A + B)). exact _. Defined.
+Global Instance dec_eq_unit : DecidableRel (@eq unit) | 10. exact _. Defined.
+Global Instance dec_eq_bool : DecidableRel (@eq bool) | 10. exact _. Defined.
+Global Instance dec_eq_Empty_set : DecidableRel (@eq Empty_set) | 10. exact _. Defined.
+Global Instance dec_eq_nat : DecidableRel (@eq nat) | 10. exact _. Defined.
+Global Instance dec_eq_prod {A B} `{DecidableRel (@eq A), DecidableRel (@eq B)} : DecidableRel (@eq (A * B)) | 10. exact _. Defined.
+Global Instance dec_eq_sum {A B} `{DecidableRel (@eq A), DecidableRel (@eq B)} : DecidableRel (@eq (A + B)) | 10. exact _. Defined.
Lemma Decidable_respects_iff A B (H : A <-> B) : (Decidable A -> Decidable B) * (Decidable B -> Decidable A).
Proof. solve_decidable_transparent. Defined.
@@ -59,3 +59,6 @@ Proof. solve_decidable_transparent. Defined.
Lemma Decidable_iff_to_flip_impl A B (H : A <-> B) : Decidable B -> Decidable A.
Proof. solve_decidable_transparent. Defined.
+
+(** For dubious compatibility with [eauto using]. *)
+Hint Extern 2 (Decidable _) => progress unfold Decidable : typeclass_instances core.
diff --git a/src/Util/Option.v b/src/Util/Option.v
new file mode 100644
index 000000000..db4b69dde
--- /dev/null
+++ b/src/Util/Option.v
@@ -0,0 +1,62 @@
+Require Import Coq.Classes.Morphisms.
+
+Global Instance option_rect_Proper_nd {A T}
+ : Proper ((pointwise_relation _ eq) ==> eq ==> eq ==> eq) (@option_rect A (fun _ => T)).
+Proof.
+ intros ?? H ??? [|]??; subst; simpl; congruence.
+Qed.
+
+Global Instance option_rect_Proper_nd' {A T}
+ : Proper ((pointwise_relation _ eq) ==> eq ==> forall_relation (fun _ => eq)) (@option_rect A (fun _ => T)).
+Proof.
+ intros ?? H ??? [|]; subst; simpl; congruence.
+Qed.
+
+Hint Extern 1 (Proper _ (@option_rect ?A (fun _ => ?T))) => exact (@option_rect_Proper_nd' A T) : typeclass_instances.
+
+Lemma option_rect_option_map : forall {A B C} (f:A->B) some none v,
+ option_rect (fun _ => C) (fun x => some (f x)) none v = option_rect (fun _ => C) some none (option_map f v).
+Proof.
+ destruct v; reflexivity.
+Qed.
+
+Lemma option_rect_function {A B C S' N' v} f
+ : f (option_rect (fun _ : option A => option B) S' N' v)
+ = option_rect (fun _ : option A => C) (fun x => f (S' x)) (f N') v.
+Proof. destruct v; reflexivity. Qed.
+
+(*
+Ltac commute_option_rect_Let_In := (* pull let binders out side of option_rect pattern matching *)
+ idtac;
+ lazymatch goal with
+ | [ |- ?LHS = option_rect ?P ?S ?N (Let_In ?x ?f) ]
+ => (* we want to just do a [change] here, but unification is stupid, so we have to tell it what to unfold in what order *)
+ cut (LHS = Let_In x (fun y => option_rect P S N (f y))); cbv beta;
+ [ set_evars;
+ let H := fresh in
+ intro H;
+ rewrite H;
+ clear;
+ abstract (cbv [Let_In]; reflexivity)
+ | ]
+ end.
+*)
+
+(** TODO: possibly move me, remove local *)
+Ltac replace_option_match_with_option_rect :=
+ idtac;
+ lazymatch goal with
+ | [ |- _ = ?RHS :> ?T ]
+ => lazymatch RHS with
+ | match ?a with None => ?N | Some x => @?S x end
+ => replace RHS with (option_rect (fun _ => T) S N a) by (destruct a; reflexivity)
+ end
+ end.
+
+Ltac simpl_option_rect := (* deal with [option_rect _ _ _ None] and [option_rect _ _ _ (Some _)] *)
+ repeat match goal with
+ | [ |- context[option_rect ?P ?S ?N None] ]
+ => change (option_rect P S N None) with N
+ | [ |- context[option_rect ?P ?S ?N (Some ?x) ] ]
+ => change (option_rect P S N (Some x)) with (S x); cbv beta
+ end.
diff --git a/src/Util/Sum.v b/src/Util/Sum.v
index 2f03639b2..1ee8ea69a 100644
--- a/src/Util/Sum.v
+++ b/src/Util/Sum.v
@@ -1,5 +1,6 @@
Require Import Coq.Classes.Morphisms.
Require Import Relation_Definitions.
+Require Import Crypto.Util.Decidable.
Definition sumwise {A B} (RA:relation A) (RB : relation B) : relation (A + B)
:= fun x y => match x, y with
@@ -16,3 +17,18 @@ Proof.
Qed.
Arguments sumwise {A B} _ _ _ _.
+
+Ltac congruence_sum_step :=
+ match goal with
+ | [ H : inl _ = inr _ |- _ ] => solve [ inversion H ]
+ | [ H : inr _ = inl _ |- _ ] => solve [ inversion H ]
+ | [ H : inl _ = inl _ |- _ ] => inversion H; clear H
+ | [ H : inr _ = inr _ |- _ ] => inversion H; clear H
+ end.
+Ltac congruence_sum := repeat congruence_sum_step.
+
+Local Hint Extern 0 => solve [ solve_decidable_transparent ] : typeclass_instances.
+Global Instance dec_sumwise {A B RA RB} {HA : DecidableRel RA} {HB : DecidableRel RB} : DecidableRel (@sumwise A B RA RB) | 10.
+Proof.
+ intros [x|x] [y|y]; exact _.
+Qed.
diff --git a/src/Util/Tactics.v b/src/Util/Tactics.v
index e8876fee2..fea7dfe16 100644
--- a/src/Util/Tactics.v
+++ b/src/Util/Tactics.v
@@ -56,13 +56,34 @@ Ltac break_match_step only_when :=
| [ |- appcontext[match ?e with _ => _ end] ]
=> only_when e; destruct e eqn:?
end.
+Ltac break_match_hyps_step only_when :=
+ match goal with
+ | [ H : appcontext[match ?e with _ => _ end] |- _ ]
+ => only_when e; is_var e; destruct e
+ | [ H : appcontext[match ?e with _ => _ end] |- _ ]
+ => only_when e;
+ match type of e with
+ | sumbool _ _ => destruct e
+ end
+ | [ H : appcontext[if ?e then _ else _] |- _ ]
+ => only_when e; destruct e eqn:?
+ | [ H : appcontext[match ?e with _ => _ end] |- _ ]
+ => only_when e; destruct e eqn:?
+ end.
Ltac break_match := repeat break_match_step ltac:(fun _ => idtac).
+Ltac break_match_hyps := repeat break_match_hyps_step ltac:(fun _ => idtac).
Ltac break_match_when_head_step T :=
break_match_step
ltac:(fun e => let T' := type of e in
let T' := head T' in
constr_eq T T').
+Ltac break_match_hyps_when_head_step T :=
+ break_match_hyps_step
+ ltac:(fun e => let T' := type of e in
+ let T' := head T' in
+ constr_eq T T').
Ltac break_match_when_head T := repeat break_match_when_head_step T.
+Ltac break_match_hyps_when_head T := repeat break_match_hyps_when_head_step T.
Ltac free_in x y :=
idtac;
@@ -111,3 +132,10 @@ Ltac destruct_trivial_step :=
| [ H : True |- _ ] => clear H || destruct H
end.
Ltac destruct_trivial := repeat destruct_trivial_step.
+
+Ltac clear_duplicates_step :=
+ match goal with
+ | [ H : ?T, H' : ?T |- _ ] => clear H'
+ | [ H := ?T, H' := ?T |- _ ] => clear H'
+ end.
+Ltac clear_duplicates := repeat clear_duplicates_step.
diff --git a/src/Util/Tuple.v b/src/Util/Tuple.v
index 6802a86c3..d08c52c82 100644
--- a/src/Util/Tuple.v
+++ b/src/Util/Tuple.v
@@ -1,5 +1,6 @@
Require Import Coq.Classes.Morphisms.
Require Import Relation_Definitions.
+Require Import Crypto.Util.Decidable.
Fixpoint tuple' T n : Type :=
match n with
@@ -79,3 +80,17 @@ Qed.
Arguments fieldwise' {A B n} _ _ _.
Arguments fieldwise {A B n} _ _ _.
+
+Local Hint Extern 0 => solve [ solve_decidable_transparent ] : typeclass_instances.
+Global Instance dec_fieldwise' {A RA} {HA : DecidableRel RA} {n} : DecidableRel (@fieldwise' A A n RA) | 10.
+Proof.
+ induction n; simpl @fieldwise'.
+ { exact _. }
+ { intros ??.
+ exact _. }
+Qed.
+
+Global Instance dec_fieldwise {A RA} {HA : DecidableRel RA} {n} : DecidableRel (@fieldwise A A n RA) | 10.
+Proof.
+ destruct n; unfold fieldwise; exact _.
+Qed.
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-24 22:03:44 +0000