diff options
author | Robert Sloan <varomodt@gmail.com> | 2016-06-23 00:18:35 -0400 |
---|---|---|
committer | Robert Sloan <varomodt@gmail.com> | 2016-06-23 00:18:35 -0400 |
commit | 4c727f5bf4830b2d41c7528f6a825c7d0a4ea295 (patch) | |
tree | 78acab586083523655dc29411e4721586a6c844e | |
parent | 9523198cd20dc209bb62c52746accb69d59c7e4c (diff) |
Pseudize Let_In
-rw-r--r-- | src/Assembly/Pseudize.v | 38 | ||||
-rw-r--r-- | src/CompleteEdwardsCurve/Pre.v | 15 |
2 files changed, 36 insertions, 17 deletions
diff --git a/src/Assembly/Pseudize.v b/src/Assembly/Pseudize.v index 0ef1dd765..915e28212 100644 --- a/src/Assembly/Pseudize.v +++ b/src/Assembly/Pseudize.v @@ -6,18 +6,20 @@ Require Export Wordize Vectorize. Module Conversion. Import Pseudo ListNotations StateCommon EvalUtil ListState. + Definition Let_In {A P} (x : A) (f : forall a : A, P a) : P x := let y := x in f y. + Hint Unfold setList getList getVar setCarry setCarryOpt getCarry getMem setMem overflows. - Lemma eval_in_length: forall {w s n m} x M c x' M' c' p, + Lemma eval_in_length: forall {w s n m} p x M c x' M' c', @pseudoEval n m w s p (x, M, c) = Some (x', M', c') -> Datatypes.length x = n. - Admitted. + Proof. Admitted. Lemma eval_out_length: forall {w s n m} x M c x' M' c' p, @pseudoEval n m w s p (x, M, c) = Some (x', M', c') -> Datatypes.length x' = m. - Admitted. + Proof. Admitted. Lemma pseudo_var: forall {w s n} b k x v m c, (k < n)%nat @@ -30,11 +32,15 @@ Module Conversion. rewrite H0; simpl; intuition. } - replace (k mod n) with k by admit. (* TODO (rsloan): find lemma name *) + replace (k mod n) with k by ( + assert (n <> 0) as NZ by omega; + pose proof (Nat.div_mod k n NZ); + replace (k mod n) with (k - n * (k / n)) by intuition; + rewrite (Nat.div_small k n); intuition). autounfold; simpl. destruct (nth_error x k); simpl; try inversion H0; intuition. - Admitted. + Qed. Lemma pseudo_mem: forall {w s} n v m c x name len index, TripleM.find (w, name mod n, index mod len)%nat m = Some (@wordToN w v) @@ -178,9 +184,9 @@ Module Conversion. pseudoEval p0 (input, m0, c0) = Some ([a], m1, c1) -> pseudoEval p1 (input ++ [a], m1, c1) = Some (f (nth n (input ++ [a]) (wzero _)), m2, c2) -> pseudoEval (@PLet w s n k m p0 p1) (input, m0, c0) = - Some (let x := a in f a, m2, c2). + Some (Let_In a f, m2, c2). Proof. - intros; cbv zeta. + intros; unfold Let_In; cbv zeta. eapply pseudo_let; try eassumption. replace (f a) with (f (nth n (input ++ [a]) (wzero w))); try assumption. apply f_equal. @@ -197,9 +203,9 @@ Module Conversion. pseudoEval p0 (input, m0, c0) = Some (lst, m1, c1) -> pseudoEval p1 (input ++ lst, m1, c1) = Some (f lst, m2, c2) -> pseudoEval (@PLet w s n k m p0 p1) (input, m0, c0) = - Some (let x := lst in f x, m2, c2). + Some (Let_In lst f, m2, c2). Proof. - intros; cbv zeta. + intros; unfold Let_In; cbv zeta. eapply pseudo_let; try eassumption. Qed. @@ -224,9 +230,9 @@ Module Conversion. Ltac pseudo_step := match goal with - | [ |- pseudoEval ?p _ = Some ((let _ := ?b in _), _, _) ] => + | [ |- pseudoEval ?p _ = Some ((Let_In ?a ?f), _, _) ] => is_evar p; - match (type of b) with + match (type of a) with | word _ => eapply pseudo_let_var | list _ => eapply pseudo_let_list end @@ -239,9 +245,9 @@ Module Conversion. is_evar p; eapply pseudo_cons; try reflexivity | [ |- pseudoEval ?p _ = Some ([natToWord _ ?x], _, _)%p ] => is_evar p; eapply pseudo_const - | [ |- @pseudoEval ?n _ _ _ ?P (?lst, _, _) = + | [ |- @pseudoEval ?n _ _ _ ?P _ = Some ([nth ?i ?lst _], _, _)%p ] => - eapply (pseudo_var None); simpl; intuition + eapply (pseudo_var None i); simpl; intuition end. Ltac pseudo_solve := @@ -251,9 +257,9 @@ Module Conversion. repeat pseudo_step. Definition convert_example: @pseudeq 32 W32 1 1 (fun v => - let a := natToWord _ 1 in - let b := nth 0 v (wzero _) in - [a ^& b]). + Let_In (natToWord _ 1) (fun a => + Let_In (nth 0 v (wzero _)) (fun b => + [a ^& b]))). pseudo_solve. Defined. diff --git a/src/CompleteEdwardsCurve/Pre.v b/src/CompleteEdwardsCurve/Pre.v index be294fb3e..c1b0e7d71 100644 --- a/src/CompleteEdwardsCurve/Pre.v +++ b/src/CompleteEdwardsCurve/Pre.v @@ -4,7 +4,9 @@ Require Import Crypto.Util.Notations. Generalizable All Variables. Section Pre. - Context {F eq zero one opp add sub mul inv div} `{field F eq zero one opp add sub mul inv div}. + Context {F eq zero one opp add sub mul inv div} + `{field F eq zero one opp add sub mul inv div}. + Local Infix "=" := eq. Local Notation "a <> b" := (not (a = b)). Local Infix "=" := eq : type_scope. Local Notation "a <> b" := (not (a = b)) : type_scope. Local Notation "0" := zero. Local Notation "1" := one. @@ -58,6 +60,17 @@ Section Pre. unfold onCurve, unifiedAdd'; intros [x1 y1] [x2 y2] H1 H2. field_algebra; auto using edwardsAddCompleteMinus, edwardsAddCompletePlus. Qed. + + Lemma jason : forall (x y: F), + x^2 = y^2 -> x <> 0-y -> x <> y -> False. + Proof. + intros x y A B C; destruct (eq_dec (x - y) 0). + + - contradict C. field_algebra. + - assert ((x + y) = 0 / (x - y)) as Z by (field_simplify_eq_all; field_algebra). + replace (0 / _) with 0 in Z by admit. + contradict B; field_algebra. + Admitted. End Pre. Import Group Ring Field. |