Commit 84a0d100 authored by Benoit Viguier's avatar Benoit Viguier
Browse files

WIP - working of positivity

parent b6230376
...@@ -13,32 +13,46 @@ Notation "ℤ.lst A" := (ZofList n A) (at level 65, right associativity). ...@@ -13,32 +13,46 @@ Notation "ℤ.lst A" := (ZofList n A) (at level 65, right associativity).
Lemma ZsumList_correct_impl : forall a b o, a b = o -> (.lst a) + (.lst b) = .lst o. Lemma ZsumList_correct_impl : forall a b o, a b = o -> (.lst a) + (.lst b) = .lst o.
Proof. Proof.
induction a , b. induction a , b.
- intros o HSum ; go. - intros o HSum ; go.
- intros o HSum ; go. - intros o HSum ; go.
- intros o HSum ; go. - intros o HSum ; go.
- intros o HSum. - intros o HSum.
destruct o ; go. destruct o ; go.
simpl in HSum. simpl in HSum.
assert(Hh:= HSum). assert(Hh:= HSum).
apply headSame in Hh. apply headSame in Hh.
apply tailSame in HSum. apply tailSame in HSum.
apply IHa in HSum. apply IHa in HSum.
unfold ZofList. unfold ZofList.
rewrite <- Z.add_shuffle2. rewrite <- Z.add_shuffle2.
rewrite Zred_factor4. rewrite Zred_factor4.
apply Zplus_eq_compat. apply Zplus_eq_compat.
apply Hh. apply Hh.
f_equal. f_equal.
rewrite Z.add_comm. rewrite Z.add_comm.
apply HSum. apply HSum.
Qed. Qed.
Corollary ZsumList_correct: forall a b, (.lst a b) = (.lst a) + (.lst b). Corollary ZsumList_correct: forall a b, (.lst a b) = (.lst a) + (.lst b).
Proof. Proof.
intros a b. intros a b.
assert(exists o, o = a b) by (exists (a b) ; go) ; destruct H. assert(exists o, o = a b) by (exists (a b) ; go) ; destruct H.
symmetry; subst x ; apply ZsumList_correct_impl ; go. symmetry; subst x ; apply ZsumList_correct_impl ; go.
Qed.
Lemma ZsumList_pos: forall a b, ZList_pos a -> ZList_pos b -> ZList_pos (a b).
Proof.
induction a , b ; intros.
- auto.
- auto.
- auto.
- simpl.
unfold ZList_pos in *.
rewrite Forall_cons'.
rewrite Forall_cons' in H.
rewrite Forall_cons' in H0.
destruct H, H0. go.
Qed. Qed.
End Integer. End Integer.
...@@ -187,17 +187,19 @@ Qed. ...@@ -187,17 +187,19 @@ Qed.
Lemma car25519_bound : forall i l, (length l = 16)%nat -> (i <> 0)%nat -> nth i (car25519 l) 0 < 2 ^ 16. Lemma car25519_bound : forall i l, (length l = 16)%nat -> (i <> 0)%nat -> nth i (car25519 l) 0 < 2 ^ 16.
Proof. Proof.
destruct i ; intros l H Hi ; [false|]. destruct i ; intros l H Hi ; [false|].
repeat (destruct l ; tryfalse). apply destruct_length_16 in H.
do 16 destruct H.
unfold car25519. unfold car25519.
unfold backCarry. unfold backCarry.
flatten. symmetry ; reflexivity. flatten. symmetry ; reflexivity.
rewrite nth_cons. rewrite nth_cons.
subst l.
repeat rewrite Carry_n_step in Eq. repeat rewrite Carry_n_step in Eq.
rewrite Carry_n_step_0 in Eq. rewrite Carry_n_step_0 in Eq.
repeat (destruct l ; tryfalse). repeat (destruct l0 ; tryfalse).
repeat rewrite ListSame in Eq. repeat rewrite ListSame in Eq.
jauto_set. jauto_set.
clear Hi H16. clear Hi H15.
(* destruct the big /\ construction *) (* destruct the big /\ construction *)
assert(Hi: (i < 14 \/ i = 14 \/ i > 14)%nat) by omega. assert(Hi: (i < 14 \/ i = 14 \/ i > 14)%nat) by omega.
(* case analisys on i: in slice, last elem or outside *) (* case analisys on i: in slice, last elem or outside *)
...@@ -286,6 +288,25 @@ Proof. ...@@ -286,6 +288,25 @@ Proof.
rewrite Z.mul_comm ; rewrite Z_div_plus ; [|compute] ; reflexivity. rewrite Z.mul_comm ; rewrite Z_div_plus ; [|compute] ; reflexivity.
Qed. Qed.
Fact getCarry16_256: forall (z z0 z1 z2 z3 z4 z5 z6 z7 z8 z9 z10 z11 z12 z13 z14:Z),
getCarry 16 (getCarry 16 (getCarry 16 (getCarry 16 (getCarry 16 (getCarry 16 (getCarry 16 (getCarry 16 (getCarry 16 (getCarry 16 (getCarry 16 (getCarry 16 (getCarry 16 (getCarry 16 (getCarry 16 (getCarry 16 (0 + z) + z0) + z1) + z2) + z3) + z4) + z5) + z6) + z7) + z8) + z9) + z10) + z11) + z12) + z13) + z14) =
getCarry 256 (16.lst [z; z0; z1; z2; z3; z4; z5; z6; z7; z8; z9; z10; z11; z12; z13; z14]).
Proof.
intros.
unfold getCarry in *.
unfold getResidute in *.
repeat rewrite Zshiftr_div_pow2_16.
rewrite Z.shiftr_div_pow2 by omega.
unfold ZofList.
rewrite <- Zmult_0_r_reverse.
rewrite <- Zplus_0_r_reverse.
change (0 + z) with z.
rewrite factors_256.
repeat (rewrite <- Z.div_div ; [|intro ; false | symmetry ; auto]).
apply pre_compute_equality_factor.
Qed.
Lemma getCarry_16_eq_256 : Lemma getCarry_16_eq_256 :
forall (z z0 z1 z2 z3 z4 z5 z6 z7 z8 z9 z10 z11 z12 z13 z14 z15:Z) (l:list Z), forall (z z0 z1 z2 z3 z4 z5 z6 z7 z8 z9 z10 z11 z12 z13 z14 z15:Z) (l:list Z),
Carrying_n 16 15 0 [z; z0; z1; z2; z3; z4; z5; z6; z7; z8; z9; z10; z11; z12; z13; z14] = z15 :: l -> Carrying_n 16 15 0 [z; z0; z1; z2; z3; z4; z5; z6; z7; z8; z9; z10; z11; z12; z13; z14] = z15 :: l ->
...@@ -300,17 +321,7 @@ Proof. ...@@ -300,17 +321,7 @@ Proof.
clear H H0 H1 H2 H3 H4 H5 H6 H7 H8 H9 H10 H11 H12 H13 H15. clear H H0 H1 H2 H3 H4 H5 H6 H7 H8 H9 H10 H11 H12 H13 H15.
unfold nth. unfold nth.
subst z30. subst z30.
unfold getCarry in *. apply getCarry16_256.
unfold getResidute in *.
repeat rewrite Zshiftr_div_pow2_16.
rewrite Z.shiftr_div_pow2 by omega.
unfold ZofList.
rewrite <- Zmult_0_r_reverse.
rewrite <- Zplus_0_r_reverse.
change (0 + z) with z.
rewrite factors_256.
repeat (rewrite <- Z.div_div ; [|intro ; false | symmetry ; auto]).
apply pre_compute_equality_factor.
Qed. Qed.
Fact pre_compute_rewrite: forall (z z0 z1 z2 z3 z4 z5 z6 z7 z8 z9 z10 z11 z12 z13 z14 : ), Fact pre_compute_rewrite: forall (z z0 z1 z2 z3 z4 z5 z6 z7 z8 z9 z10 z11 z12 z13 z14 : ),
...@@ -325,10 +336,12 @@ Qed. ...@@ -325,10 +336,12 @@ Qed.
Lemma car25519_eq_car25519: forall (l : list ), (length l = 16)%nat -> car25519 (16.lst l) = 16.lst (car25519 l). Lemma car25519_eq_car25519: forall (l : list ), (length l = 16)%nat -> car25519 (16.lst l) = 16.lst (car25519 l).
Proof. Proof.
intros l Hlength. intros l H.
unfold car25519. unfold car25519.
unfold car25519. unfold car25519.
repeat (destruct l ; tryfalse). apply destruct_length_16 in H.
do 16 destruct H.
subst l.
unfold backCarry. unfold backCarry.
flatten ; tryfalse. flatten ; tryfalse.
symmetry. symmetry.
...@@ -341,14 +354,14 @@ Proof. ...@@ -341,14 +354,14 @@ Proof.
assumption. assumption.
- rewrite Carry_n_step in Eq. - rewrite Carry_n_step in Eq.
repeat rewrite ListSame in Eq ; jauto_set. repeat rewrite ListSame in Eq ; jauto_set.
subst l z15. subst l z.
rewrite ZofList_cons. rewrite ZofList_cons.
rewrite ZofList_app by omega. rewrite ZofList_app by omega.
rewrite ZofList_slice by omega. rewrite ZofList_slice by omega.
rewrite <- CarrynPreserveConst by omega. rewrite <- CarrynPreserveConst by omega.
change (0 + z) with z. change (0 + x) with x.
repeat rewrite Carry_n_step ; rewrite Carry_n_step_0. repeat rewrite Carry_n_step ; rewrite Carry_n_step_0.
remember (getCarry 16 (getCarry 16 (getCarry 16 (getCarry 16 (getCarry 16 (getCarry 16 (getCarry 16 (getCarry 16 (getCarry 16 (getCarry 16 (getCarry 16 (getCarry 16 (getCarry 16 (getCarry 16 (getCarry 16 z + z0) + z1) + z2) + z3) + z4) + z5) + z6) + z7) + z8) + z9) + z10) + z11) + z12) + z13) + z14) as t. remember (getCarry 16 (getCarry 16 (getCarry 16 (getCarry 16 (getCarry 16 (getCarry 16 (getCarry 16 (getCarry 16 (getCarry 16 (getCarry 16 (getCarry 16 (getCarry 16 (getCarry 16 (getCarry 16 (getCarry 16 x + x0) + x1) + x2) + x3) + x4) + x5) + x6) + x7) + x8) + x9) + x10) + x11) + x12) + x13) + x14) as t.
unfold length. unfold length.
unfold nth. unfold nth.
unfold slice. unfold slice.
...@@ -422,12 +435,26 @@ Proof. ...@@ -422,12 +435,26 @@ Proof.
unfold nth. unfold nth.
unfold slice. unfold slice.
f_equal. f_equal.
- clear H H0 H1 H2 H3 H4 H5 H6 H7 H8 H9 H10 H11 H12 H13 H14 H16.
subst z30.
rewrite getCarry16_256.
assert(getCarry 256 (16.lst [z0; z1; z2; z3; z4; z5; z6; z7; z8; z9; z10; z11; z12; z13; z14; z15]) = 0).
unfold getCarry.
rewrite Z.shiftr_div_pow2 by omega.
(* SearchAbout Z.div 0.*)
apply Zdiv_small.
admit. admit.
change ([z16; z17; z18; z19; z20; z21; z22; z23; z24; z25; z26; z27; z28; z29; z30]) with admit.
- change ([z16; z17; z18; z19; z20; z21; z22; z23; z24; z25; z26; z27; z28; z29; z30]) with
([z16; z17; z18; z19; z20; z21; z22; z23; z24; z25; z26; z27; z28; z29] ++ [z30]). ([z16; z17; z18; z19; z20; z21; z22; z23; z24; z25; z26; z27; z28; z29] ++ [z30]).
f_equal. f_equal.
clear H H0 H1 H2 H3 H4 H5 H6 H7 H8 H9 H10 H11 H12 H13 H14 H16. clear H H0 H1 H2 H3 H4 H5 H6 H7 H8 H9 H10 H11 H12 H13 H14 H16.
f_equal.
rewrite pre_compute_rewrite in H15.
Admitted.
(*
unfold getResidute. unfold getResidute.
subst z30.
...@@ -442,3 +469,4 @@ Proof. ...@@ -442,3 +469,4 @@ Proof.
repeat (destruct l ; tryfalse). repeat (destruct l ; tryfalse).
unfold car25519. unfold car25519.
unfold backCarry. unfold backCarry.
*)
\ No newline at end of file
Require Export Tools.
Require Export ZofList.
Require Export Forall.
Require Export notations.
Lemma Forall_slice : forall n A (l:list A) (P:A -> Prop), Forall P l -> Forall P (slice n l).
Proof.
induction n.
- intros A [] P H ; go.
- intros A [] P H ; go.
simpl.
rewrite Forall_cons'.
rewrite Forall_cons' in H.
destruct H.
go.
Qed.
Lemma Forall_app : forall A (a b:list A) (P:A -> Prop), Forall P a -> Forall P b -> Forall P (a ++ b).
Proof.
induction a.
- intros b P Ha Hb ; go.
- intros b P Ha Hb ; go.
simpl.
rewrite Forall_cons'.
rewrite Forall_cons' in Ha.
destruct Ha.
go.
Qed.
Lemma Forall_tail : forall n A (l:list A) (P:A -> Prop), Forall P l -> Forall P (tail n l).
Proof.
induction n.
- intros A [] P H ; go.
- intros A [] P H ; go.
simpl.
rewrite Forall_cons' in H.
destruct H.
go.
Qed.
Open Scope Z.
Import ListNotations.
Section Integer.
Variable n:Z.
Hypothesis Hn: n > 0.
(*
Forall LEMMAS
*)
Definition ZList_pos (l:list Z) : Prop := Forall (Zle 0) l.
Notation "ℤ.lst A" := (ZofList n A) (at level 65, right associativity).
Lemma ZofList_pos : forall l, ZList_pos l -> 0 <= .lst l.
Proof.
intros l Hl.
dependent induction Hl.
- go.
- rewrite ZofList_cons.
apply OMEGA2.
assumption.
rewrite Z.mul_comm.
apply Zmult_gt_0_le_0_compat.
apply pown0.
auto.
auto.
Qed.
Lemma ZofList_null : forall l, ZList_pos l -> .lst l = 0 -> Forall (Z.eq 0) l.
Proof.
intros l HFl HSl.
induction HFl.
- go.
- assert(Hx: {x < 0} + {x = 0} + {x > 0}) by apply Ztrichotomy_inf.
assert(Hl: {.lst l < 0} + {.lst l = 0} + {.lst l > 0}) by apply Ztrichotomy_inf.
rewrite ZofList_cons in HSl.
assert(Hlpos:= ZofList_pos l HFl).
case Hl ; intro Hl'.
case Hl' ; intro Hl''.
apply Zle_not_lt in Hlpos.
false.
+ clear Hl' Hl Hlpos.
case Hx ; intro Hx'.
case Hx' ; intro Hx''.
apply Zle_not_lt in H.
false.
* clear Hx' Hx.
apply Forall_cons ; go.
* assert(2 ^ n * (.lst l) = 0).
rewrite Z.eq_mul_0 ; auto.
rewrite H0 in HSl.
omega. (* contradiction between x = 0 and x > 0*)
+ clear Hlpos Hl.
case Hx ; intro Hx'.
case Hx' ; intro Hx''.
apply Zle_not_lt in H.
false.
* clear Hx' Hx.
subst x ; clear H.
rewrite Z.add_0_l in HSl.
rewrite Z.eq_mul_0 in HSl.
destruct HSl.
assert(H0' := pown0 n Hn) ; omega.
omega (* contraction between H and Hl'*).
* (*once again we need to show a contradiction in HSl. *)
assert(0 < x + 2 ^ n * (.lst l)).
apply Z.add_pos_pos.
omega. (*see Hx' *)
rewrite Z.lt_0_mul.
left ; split ; rewrite <- Z.gt_lt_iff.
apply pown0 ; auto.
assumption. (* apply Hl' *)
omega.
Qed.
Lemma ZofList_bound : forall (m:Z) l , 0 <= m < 2 ^ n -> ZList_pos l -> .lst l = m -> nth 0 l 0 = m.
Proof.
intros m l Hm HFl HSlm.
destruct l.
- go.
- rewrite ZofList_cons in HSlm.
unfold nth.
subst m.
replace (2 ^ n * (.lst l)) with 0.
apply Zplus_0_r_reverse.
unfold ZList_pos in HFl.
rewrite Forall_cons' in HFl.
destruct HFl as [Hz Hpos].
apply ZofList_pos in Hpos.
assert(Hl: {.lst l < 0} + {.lst l = 0} + {.lst l > 0}) by apply Ztrichotomy_inf.
case Hl ; intro Hl'.
case Hl' ; intro Hl''.
apply Zle_not_lt in Hpos.
false.
+ symmetry. rewrite Z.eq_mul_0 ; auto.
+ exfalso.
clear Hl Hpos.
assert(1 <= .lst l).
omega.
assert(2 ^ n * 1 <= 2 ^ n * (.lst l)).
apply Zmult_le_compat_l ; auto.
rewrite <- Z.ge_le_iff.
assert(Ht:= pown0).
omega.
omega.
Qed.
End Integer.
...@@ -4,14 +4,62 @@ Import ListNotations. ...@@ -4,14 +4,62 @@ Import ListNotations.
Require Export Tools. Require Export Tools.
Open Scope Z. Open Scope Z.
Lemma ZscalarMult_pos: forall a b, 0 <= a -> ZList_pos b -> ZList_pos (a b).
Proof.
induction b ; intros.
- auto.
- simpl.
unfold ZList_pos.
unfold ZList_pos in H0.
rewrite Forall_cons' in H0.
rewrite Forall_cons'.
destruct H0.
split.
+ apply Z.mul_nonneg_nonneg ; auto.
+ apply IHb ; auto.
Qed.
Fixpoint mult_1 (a b:list Z) : list Z := match a, b with Fixpoint mult_1 (a b:list Z) : list Z := match a, b with
| [],_ => [] | [],_ => []
| _,[] => [] | _,[] => []
| ha :: qa, hb :: qb => ha * hb :: (ha qb) (mult_1 qa (hb::qb)) | ha :: qa, hb :: qb => ha * hb :: (ha qb) (mult_1 qa (hb::qb))
end. end.
Lemma mult_1_pos : forall a b, ZList_pos a -> ZList_pos b -> ZList_pos (mult_1 a b).
Proof.
induction a, b ; intros.
- auto.
- auto.
- auto.
- simpl.
unfold ZList_pos in *.
rewrite Forall_cons' in H.
rewrite Forall_cons' in H0.
destruct H, H0.
rewrite Forall_cons'.
split.
+ apply Z.mul_nonneg_nonneg ; auto.
+ apply ZsumList_pos.
* apply ZscalarMult_pos ; auto.
* apply IHa; auto.
Qed.
Definition mult_2 (a:list Z) : list Z := a (38 (tail 16 a)). Definition mult_2 (a:list Z) : list Z := a (38 (tail 16 a)).
Lemma mult_2_pos : forall a, ZList_pos a -> ZList_pos (mult_2 a).
Proof.
intros.
unfold mult_2.
apply ZsumList_pos ; auto.
apply ZscalarMult_pos ; try omega.
Definition mult_3 (a:list Z) : list Z := slice 16 a. Definition mult_3 (a:list Z) : list Z := slice 16 a.
Definition M (a b:list Z) : list Z := Definition M (a b:list Z) : list Z :=
...@@ -19,6 +67,8 @@ Definition M (a b:list Z) : list Z := ...@@ -19,6 +67,8 @@ Definition M (a b:list Z) : list Z :=
let m2 := mult_2 m1 in let m2 := mult_2 m1 in
mult_3 m2. mult_3 m2.
Section Integer. Section Integer.
Variable n:Z. Variable n:Z.
......
Require Export Tools. Require Export Tools.
Require Export Forall. Require Export Forall_extended.
Require Export notations. Require Export notations.
Open Scope Z. Open Scope Z.
...@@ -12,24 +12,14 @@ Variable n:Z. ...@@ -12,24 +12,14 @@ Variable n:Z.
Hypothesis Hn: n > 0. Hypothesis Hn: n > 0.
Lemma addition: forall a b : Z, Lemma addition: forall a b : Z,
a < 2^n -> a < 2^n -> b < 2^n ->
b < 2^n -> a + b < 2^Z.succ n.
a + b < 2^Z.succ n.
Proof. Proof.
intros a b Ha Hb. intros.
assert(H: 2 ^ Z.succ n = 2 * 2 ^ n) by (apply Z.pow_succ_r ; omega). assert(H': 2 ^ Z.succ n = 2 * 2 ^ n) by (apply Z.pow_succ_r ; omega).
rewrite H. rewrite H' ; omega.
omega.
Qed.
(* By J-M Madiot *)
Lemma addition': forall a b : Z, a < 2^63 -> b < 2^63 -> a + b < 2^64.
Proof.
change (2 ^ 64) with (2 ^ 63 * 2).
intros; omega.
Qed. Qed.
Fixpoint ZofListi (a: list Z) (i:Z) : Z := match a with Fixpoint ZofListi (a: list Z) (i:Z) : Z := match a with
| [] => 0 | [] => 0
| h :: q => h * Z.pow 2 (n * i) + ZofListi q (Z.succ i) | h :: q => h * Z.pow 2 (n * i) + ZofListi q (Z.succ i)
...@@ -182,100 +172,21 @@ Proof. ...@@ -182,100 +172,21 @@ Proof.
go. go.
Qed. Qed.
Lemma ZofList_le_0 : forall l, Forall (Zle 0) l -> 0 <= .lst l.
Proof.
intros l Hl.
dependent induction Hl.
- go.
- rewrite ZofList_cons.
apply OMEGA2.
assumption.
rewrite Z.mul_comm.
apply Zmult_gt_0_le_0_compat.
apply pown0.
auto.
Qed.
Lemma ZofList_null : forall l, Forall (Zle 0) l -> .lst l = 0 -> Forall (Z.eq 0) l. End Integer.
Proof.
intros l HFl HSl.
induction HFl.
- go.
- assert(Hx: {x < 0} + {x = 0} + {x > 0}) by apply Ztrichotomy_inf.
assert(Hl: {.lst l < 0} + {.lst l = 0} + {.lst l > 0}) by apply Ztrichotomy_inf.
rewrite ZofList_cons in HSl.
assert(Hlpos:= ZofList_le_0 l HFl).
case Hl ; intro Hl'.
case Hl' ; intro Hl''.
apply Zle_not_lt in Hlpos.
false.
+ clear Hl' Hl Hlpos.
case Hx ; intro Hx'.
case Hx' ; intro Hx''.
apply Zle_not_lt in H.
false.
* clear Hx' Hx.
apply Forall_cons ; go.
* assert(2 ^ n * (.lst l) = 0).
rewrite Z.eq_mul_0 ; auto.
rewrite H0 in HSl.
omega.
+ clear Hlpos Hl.
case Hx ; intro Hx'.
case Hx' ; intro Hx''.
apply Zle_not_lt in H.
false.
* clear Hx' Hx.
subst x.
rewrite Z.add_0_l in HSl.
rewrite Z.eq_mul_0 in HSl.
destruct HSl.
assert(H0' := pown0) ; omega.
omega.
* assert(0 < x + 2 ^ n * (.lst l)).
apply Z.add_pos_pos.
omega.
rewrite Z.lt_0_mul.
left.
split ; rewrite <- Z.gt_lt_iff.
apply pown0.
assumption.
omega.
Qed.
Lemma ZofList_bound : forall (m:Z) l , 0 <= m < 2 ^ n -> Forall (Zle 0) l -> .lst l = m -> nth 0 l 0 = m.