From 0ff642cd6a6901c3fb0805092df40f5432280ef1 Mon Sep 17 00:00:00 2001 From: Jason Gross Date: Thu, 29 Jun 2017 13:04:32 -0400 Subject: Fix type signatures of saturated things for WBW This required admitting some proofs. @jadephilipoom, please sanity-check this. --- src/Arithmetic/Saturated.v | 80 +++++++++++++++++++++++++++++----------------- 1 file changed, 50 insertions(+), 30 deletions(-) diff --git a/src/Arithmetic/Saturated.v b/src/Arithmetic/Saturated.v index a7b9e6484..5ecb5eebd 100644 --- a/src/Arithmetic/Saturated.v +++ b/src/Arithmetic/Saturated.v @@ -674,7 +674,7 @@ Section UniformWeight. B.Positional.eval wt p = B.Positional.eval_from uweight offset p. Proof. cbv [B.Positional.eval_from]. auto using B.Positional.eval_wt_equiv. Qed. - Lemma uweight_eval_from {n} (p:Z^n): forall offset, + Lemma uweight_eval_from {n} (p:Z^n): forall offset, B.Positional.eval_from uweight offset p = uweight offset * B.Positional.eval uweight p. Proof. induction n; intros; cbv [B.Positional.eval_from]; @@ -683,7 +683,7 @@ Section UniformWeight. | _ => destruct p | _ => rewrite B.Positional.eval_unit; [ ] | _ => rewrite B.Positional.eval_step; [ ] - | _ => rewrite IHn; [ ] + | _ => rewrite IHn; [ ] | _ => rewrite eval_from_eq with (offset0:=S offset) by (intros; f_equal; omega) | _ => rewrite eval_from_eq with @@ -760,7 +760,7 @@ Module Positional. Section AddSub. Let eval {n} := B.Positional.eval (n:=n) (uweight s). - + Definition sat_add_cps {n} p q T (f:Z*Z^n->T) := chain_op_cps (op_get_carry := Z.add_get_carry_full s) (op_with_carry := Z.add_with_get_carry_full s) @@ -781,7 +781,7 @@ Module Positional. Lemma small_sat_add n p q : small (snd (@sat_add n p q)). Admitted. - + Definition sat_sub_cps {n} p q T (f:Z*Z^n->T) := chain_op_cps (op_get_carry := Z.sub_get_borrow_full s) (op_with_carry := Z.sub_with_get_borrow_full s) @@ -802,7 +802,7 @@ Module Positional. Lemma small_sat_sub n p q : small (snd (@sat_sub n p q)). Admitted. - + End AddSub. End Positional. End Positional. @@ -847,19 +847,19 @@ Section API. (fun carry_result =>f (snd carry_result)). Definition scmul {n} c p : T (S n) := @scmul_cps n c p _ id. - Definition add_cps {n} (p q: T n) {R} (f:T n->R) := + Definition add_cps {n} (p q: T n) {R} (f:T (S n)->R) := Positional.sat_add_cps (s:=bound) p q _ - (* drops last carry, this relies on bounds *) - (fun carry_result => f (snd carry_result)). - Definition add {n} p q : T n := @add_cps n p q _ id. + (* join the last carry *) + (fun carry_result => Tuple.left_append_cps (fst carry_result) (snd carry_result) f). + Definition add {n} p q : T (S n) := @add_cps n p q _ id. (* Wrappers for additions with slightly uneven limb counts *) - Definition add_S1_cps {n} (p: T (S n)) (q: T n) {R} (f:T (S n)->R) := + Definition add_S1_cps {n} (p: T (S n)) (q: T n) {R} (f:T (S (S n))->R) := join0_cps q (fun Q => add_cps p Q f). - Definition add_S1 {n} p q := @add_S1_cps n p q _ id. - Definition add_S2_cps {n} (p: T n) (q: T (S n)) {R} (f:T (S n)->R) := + Definition add_S1 {n} p q := @add_S1_cps n p q _ id. + Definition add_S2_cps {n} (p: T n) (q: T (S n)) {R} (f:T (S (S n))->R) := join0_cps p (fun P => add_cps P q f). - Definition add_S2 {n} p q := @add_S2_cps n p q _ id. + Definition add_S2 {n} p q := @add_S2_cps n p q _ id. Definition sub_then_maybe_add_cps {n} mask (p q r : T n) {R} (f:T n -> R) := @@ -923,11 +923,11 @@ Section API. @add_cps n p q R f = f (add p q). Proof. cbv [add_cps add Let_In]. prove_id. Qed. Hint Rewrite add_id : uncps. - + Lemma add_S1_id n p q R f : @add_S1_cps n p q R f = f (add_S1 p q). Proof. cbv [add_S1_cps add_S1 join0_cps]. prove_id. Qed. - + Lemma add_S2_id n p q R f : @add_S2_cps n p q R f = f (add_S2 p q). Proof. cbv [add_S2_cps add_S2 join0_cps]. prove_id. Qed. @@ -1040,7 +1040,7 @@ Section API. pose proof div_correct; pose proof modulo_correct. Lemma eval_add_nz n p q : - n <> 0%nat -> (0 <= eval p + eval q < uweight bound n) -> + n <> 0%nat -> eval (@add n p q) = eval p + eval q. Proof. intros. pose_all. @@ -1053,35 +1053,35 @@ Section API. (rewrite <-!from_list_default_eq with (d:=0); erewrite !length_to_list, !from_list_default_eq, from_list_to_list) - | _ => apply Z.mod_small; omega + | _ => apply Z.mod_small; omega end. - Qed. + Admitted. Lemma eval_add_z n p q : n = 0%nat -> eval (@add n p q) = eval p + eval q. Proof. intros; subst; reflexivity. Qed. - Lemma eval_add n p q (H:0 <= eval p + eval q < uweight bound n) + Lemma eval_add n p q : eval (@add n p q) = eval p + eval q. Proof. destruct (Nat.eq_dec n 0%nat); intuition auto using eval_add_z, eval_add_nz. Qed. - Lemma eval_add_same n p q (H:0 <= eval p + eval q < uweight bound n) + Lemma eval_add_same n p q : eval (@add n p q) = eval p + eval q. Proof. apply eval_add; omega. Qed. - Lemma eval_add_S1 n p q (H:0 <= eval p + eval q < uweight bound (S n)) + Lemma eval_add_S1 n p q : eval (@add_S1 n p q) = eval p + eval q. Proof. cbv [add_S1 add_S1_cps]. autorewrite with uncps push_id. - rewrite eval_add; rewrite eval_join0; [reflexivity|assumption]. - Qed. - Lemma eval_add_S2 n p q (H:0 <= eval p + eval q < uweight bound (S n)) + (*rewrite eval_add; rewrite eval_join0; [reflexivity|assumption].*) + Admitted. + Lemma eval_add_S2 n p q : eval (@add_S2 n p q) = eval p + eval q. Proof. cbv [add_S2 add_S2_cps]. autorewrite with uncps push_id. - rewrite eval_add; rewrite eval_join0; [reflexivity|assumption]. - Qed. + (*rewrite eval_add; rewrite eval_join0; [reflexivity|assumption].*) + Admitted. Hint Rewrite eval_add_same eval_add_S1 eval_add_S2 using (omega || assumption): push_basesystem_eval. Lemma uweight_le_mono n m : (n <= m)%nat -> @@ -1142,13 +1142,33 @@ Section API. Qed. Lemma small_add n a b : - (2 <= bound) -> + (2 <= bound) -> small a -> small b -> small (@add n a b). Proof. intros. pose_all. cbv [add_cps add Let_In]. autorewrite with uncps push_id. - apply Positional.small_sat_add. + (*apply Positional.small_sat_add.*) + Admitted. + + Lemma small_add_S1 n a b : + (2 <= bound) -> + small a -> small b -> small (@add_S1 n a b). + Proof. + intros. pose_all. + cbv [add_cps add add_S1 Let_In]. + autorewrite with uncps push_id. + (*apply Positional.small_sat_add.*) + Admitted. + + Lemma small_add_S2 n a b : + (2 <= bound) -> + small a -> small b -> small (@add_S2 n a b). + Proof. + intros. pose_all. + cbv [add_cps add add_S2 Let_In]. + autorewrite with uncps push_id. + (*apply Positional.small_sat_add.*) Admitted. Lemma small_left_tl n (v:T (S n)) : small v -> small (left_tl v). @@ -1370,7 +1390,7 @@ Section API. End Proofs. End API. -Hint Rewrite nonzero_id join0_id divmod_id drop_high_id scmul_id add_id sub_then_maybe_add_id conditional_sub_id : uncps. +Hint Rewrite nonzero_id join0_id divmod_id drop_high_id scmul_id add_id add_S1_id add_S2_id sub_then_maybe_add_id conditional_sub_id : uncps. (* (* Just some pretty-printing *) @@ -1394,4 +1414,4 @@ Definition base2pow25p5 i := Eval compute in 2^(25*Z.of_nat i + ((Z.of_nat i + 1 Time Eval cbv -[runtime_add runtime_mul Let_In] in (fun adc a0 a1 a2 a3 a4 a5 a6 a7 a8 a9 b0 b1 b2 b3 b4 b5 b6 b7 b8 b9 => Columns.mul_cps (weight := base2pow25p5) (n:=10) (a9,a8,a7,a6,a5,a4,a3,a2,a1,a0) (b9,b8,b7,b6,b5,b4,b3,b2,b1,b0) (fun ab => Columns.compact (n:=19) (add_get_carry:=adc) (weight:=base2pow25p5) ab)). (* Finished transaction in 97.341 secs *) -*) \ No newline at end of file +*) -- cgit v1.2.3