Commit 2e4375a5 authored by Benoit Viguier's avatar Benoit Viguier
Browse files

reorganization finished

parent 9fe06d71
Require Export Tweetnacl.Car.Reduce.
Require Export Tweetnacl.Car.Carry_n.
Require Export Tweetnacl.Car.Carry.
Require Export Tweetnacl.Car.ZCarry.
Require Export Tweetnacl.Car.Car25519.
\ No newline at end of file
......@@ -7,6 +7,7 @@ Require Export Tweetnacl.Libs.Forall_extended.
Require Export Tweetnacl.Libs.ZArith_extended.
Require Export Tweetnacl.Libs.Relations.
Require Export mathcomp.ssreflect.ssreflect.
Require Export stdpp.prelude.
Require Export Coq.ZArith.BinInt.
Require Export Coq.ZArith.Zdiv.
......
......@@ -188,4 +188,20 @@ Lemma Add_interval_mono3:
c <= x + y < b + d.
Proof. intros; change c with (0 + c) ; split ;[apply Z.add_le_mono | apply Z.add_lt_le_mono] ; omega. Qed.
Section Integer.
Variable n:Z.
Hypothesis Hn: n > 0.
Lemma pown: 2 ^ n > 1.
Proof. rewrite Z.gt_lt_iff ; apply Z.pow_gt_1 ; omega. Qed.
Lemma pown0: 2 ^ n > 0.
Proof. assert(Hp:= pown) ; omega. Qed.
Lemma pown2: 2 <= 2 ^ n.
Proof. change 2 with (2 ^ 1) ;apply Z.pow_le_mono ; change (2^1) with 2 ; omega. Qed.
End Integer.
Close Scope Z.
\ No newline at end of file
Require Import stdpp.list.
(* Require Import stdpp.list. *)
Require Import Tweetnacl.Libs.Export.
Require Export Tweetnacl.ListsOp.ZofList.
Open Scope Z.
Import ListNotations.
(* Import ListNotations. *)
Section Integer.
......@@ -220,7 +220,7 @@ Proof.
- rewrite Z.add_comm.
eapply (Z.le_lt_trans _ (2 * a * 2 ^ (n * (. m)) + 2 ^ (n * (. m)) * x))
; [| apply Zplus_lt_compat_r ; omega].
rewrite Z.pow_add_r ; go.
rewrite Z.pow_add_r. 2: omega. 2: go.
replace (2 * a * 2 ^ (n * (. m))) with (2 ^ (n * (. m)) * 2 * a) by ring.
rewrite -!Z.mul_assoc Zred_factor4.
replace (2 * (a * (2 ^ n * 2 ^ (n * (. m))))) with (2 ^ (n * (. m)) * (2 * a * 2 ^ n)) by ring.
......@@ -232,7 +232,7 @@ Proof.
apply pown2 ; omega.
- eapply (Z.lt_le_trans _ (2 * b * 2 ^ (n * (. m)) + 2 ^ (n * (. m)) * x)).
apply Zplus_lt_compat_r ; omega.
rewrite Z.pow_add_r ; go.
rewrite Z.pow_add_r. 2: go. 2: omega.
replace (2 * b * 2 ^ (n * (. m))) with (2 ^ (n * (. m)) * 2 * b) by ring.
rewrite -!Z.mul_assoc Zred_factor4.
replace (2 * (b * (2 ^ (n * (. m))* 2 ^ n))) with (2 ^ (n * (. m)) * (2 * b * 2 ^ n)) by ring.
......
Require Import Tweetnacl.Libs.Export.
Require Import stdpp.prelude.
Import ListNotations.
Open Scope Z.
......@@ -29,15 +27,6 @@ Fixpoint ZofList (a : list Z) : Z := match a with
end.
Notation "ℤ.lst A" := (ZofList A) (at level 65, right associativity).
Lemma pown: 2 ^ n > 1.
Proof. rewrite Z.gt_lt_iff ; apply Z.pow_gt_1 ; omega. Qed.
Lemma pown0: 2 ^ n > 0.
Proof. assert(Hp:= pown) ; omega. Qed.
Lemma pown2: 2 <= 2 ^ n.
Proof. change 2 with (2 ^ 1) ;apply Z.pow_le_mono ; change (2^1) with 2 ; omega. Qed.
Lemma ZofList_eq : forall l i, 0 <= i -> ZofListi l i = 2^(n * i) * ZofList l.
Proof. elim ; go => h l IHl i Hi /=.
assert (H := Hi).
......
......@@ -2,7 +2,6 @@ Require Import Tweetnacl.Libs.Export.
Require Import Tweetnacl.ListsOp.Export.
Require Export Tweetnacl.Mid.SumList.
Require Import stdpp.prelude.
Open Scope Z.
......@@ -102,3 +101,5 @@ Proof. convert_length_to_Zlength ZsumList_bound_length_le. Qed.
End Integer.
Close Scope Z.
Definition A a b := ZsumList a b.
\ No newline at end of file
Require Import Tweetnacl.Libs.Export.
Require Import Tweetnacl.ListsOp.Export.
Require Import Tweetnacl.Mid.Reduce.
Require Import Tweetnacl.Low.Carry_n.
Local Open Scope Z.
Definition backCarry (l:list Z) : (list Z) :=
match l with
| [] => []
| h :: q => let v := nth 15 l 0 in
(h + 38 * getCarry 16 v) :: take 14 q ++ [getResidue 16 v]
end.
Lemma backCarry_ToFF_25519 : forall l, Zlength l <= 16 -> (16.lst l) :𝓖𝓕 = ((16.lst backCarry l) :𝓖𝓕).
Proof.
destruct l as [| h l]; intro Hlength.
- go.
- unfold backCarry.
repeat rewrite ZofList_cons.
rewrite ZofList_app ; try omega.
rewrite Zlength_cons' in Hlength.
apply Z_le_lt_eq_dec in Hlength.
destruct Hlength.
+ rename l0 into H.
assert(Zlength l < 15) by omega.
rewrite Zlength_correct in H0.
repeat match goal with
| _ => simpl; omega
| _ => rewrite nth_overflow
| _ => rewrite take_ge
| _ => rewrite getResidue_0
| _ => rewrite getCarry_0
| _ => rewrite ZofList_cons_0
| _ => f_equal ; ring
end.
+ rename e into H.
assert((length l = 15)%nat) by (rewrite Zlength_correct in H ; omega).
repeat (destruct l ; tryfalse).
clear H H0.
unfold nth , take.
change ([z; z0; z1; z2; z3; z4; z5; z6; z7; z8; z9; z10; z11; z12; z13]) with ([z; z0; z1; z2; z3; z4; z5; z6; z7; z8; z9; z10; z11; z12] ++ [ z13]).
rewrite ZofList_app ; try omega.
repeat rewrite ZofList_cons_0.
do 2 rewrite <- Zred_factor4 ; rewrite Zplus_assoc_reverse.
rewrite <- Z.add_mod_idemp_r by (compute ; omega);symmetry;rewrite <- Z.add_mod_idemp_r by (compute ; omega).
f_equal; f_equal.
rewrite Z.add_shuffle3.
rewrite <- Z.add_mod_idemp_r by (compute ; omega);symmetry;rewrite <- Z.add_mod_idemp_r by (compute ; omega).
f_equal; f_equal.
rewrite <- Z.add_mod_idemp_l by (compute ; omega) ; symmetry.
rewrite Zmult_mod.
rewrite <- t2256is38.
rewrite <- Zmult_mod.
rewrite Z.add_mod_idemp_l.
change 256 with (16 + 16 * 15).
orewrite Z.pow_add_r.
rewrite Zmult_assoc_reverse.
rewrite Zred_factor4.
rewrite Zmult_mod ; symmetry ; rewrite Zmult_mod.
f_equal;f_equal.
change (2 ^ (16 * 15)) with (2 ^ (16 * 14) * 2 ^ 16).
rewrite Zmult_mod.
symmetry.
rewrite Zmult_assoc_reverse ; rewrite Zred_factor4 ; rewrite Zmult_mod.
f_equal; f_equal.
rewrite Z.add_comm.
rewrite residuteCarry ; go.
compute; omega.
Qed.
Close Scope Z.
\ No newline at end of file
Require Import Tweetnacl.Libs.Export.
Require Import stdpp.prelude.
Open Scope Z.
Definition set_xor (i:Z) := Z.lnot (i - 1).
(*
Eval compute in (set_xor 0).
Eval compute in (set_xor 1).
*)
Lemma set_xor_0 : set_xor 0 = 0.
Proof. reflexivity. Qed.
......
Require Import Tweetnacl.Libs.Export.
Require Import Tweetnacl.ListsOp.Export.
Require Import Tweetnacl.Car.Reduce.
Require Import Tweetnacl.Car.Carry_n.
Require Import Tweetnacl.Mid.M.
Require Import stdpp.prelude.
Require Import Tweetnacl.Mid.Reduce.
Require Import Tweetnacl.Low.Carry_n.
Require Import Tweetnacl.Low.BackCarry.
Require Import Tweetnacl.Mid.Carry.
Local Open Scope Z.
Section Integer.
Variable n:Z.
Hypothesis Hn: n > 0.
Notation "ℤ.lst A" := (ZofList n A) (at level 65, right associativity).
Fixpoint Carrying (a:Z) (l:list Z) : list Z := match a,l with
| 0,[] => []
| a,[] => [a]
| a,h :: q => getResidue n (a + h) :: Carrying (getCarry n (a + h)) q
end.
Lemma Carrying_n_eq: forall l (m:nat) a, m = length l -> Carrying_n n m a l = Carrying a l.
Proof.
induction l as [|h q IHl]; intros m a Hm; go.
destruct m.
inv Hm.
simpl in *.
inversion Hm.
replace (h + a) with (a + h) by omega.
flatten ; f_equal ; go.
Qed.
Lemma Carrying_n_eq_Z: forall l (m:nat) a, Zlength l = m -> Carrying_n n m a l = Carrying a l.
Proof. convert_length_to_Zlength Carrying_n_eq. Qed.
Lemma CarryPreserveConst : forall l a , a + (.lst l) = .lst Carrying a l.
Proof.
induction l as [| h q IHl].
intro a ; destruct a ; assert(Hn0: 2 ^ n * 0 = 0) by (symmetry ; apply Zmult_0_r_reverse) ; simpl ; try rewrite Hn0 ; go.
intro a ; unfold Carrying ; fold Carrying.
flatten ;
unfold ZofList ; fold ZofList ; rewrite <- IHl ;
rewrite <- Zplus_assoc_reverse ;
rewrite <- Zred_factor4 ;
rewrite <- Zplus_assoc_reverse ;
rewrite residuteCarry ;
go.
Qed.
Corollary CarryPreserve : forall l, .lst l = .lst Carrying 0 l.
Proof.
intros.
symmetry.
rewrite -CarryPreserveConst.
omega.
Qed.
End Integer.
Definition backCarry (l:list Z) : (list Z) :=
match l with
| [] => []
| h :: q => let v := nth 15 l 0 in
(h + 38 * getCarry 16 v) :: take 14 q ++ [getResidue 16 v]
end.
Lemma backCarry_ToFF_25519 : forall l, Zlength l <= 16 -> (16.lst l) :𝓖𝓕 = ((16.lst backCarry l) :𝓖𝓕).
Proof.
destruct l as [| h l]; intro Hlength.
- go.
- unfold backCarry.
repeat rewrite ZofList_cons.
rewrite ZofList_app ; try omega.
rewrite Zlength_cons' in Hlength.
apply Z_le_lt_eq_dec in Hlength.
destruct Hlength.
+ rename l0 into H.
assert(Zlength l < 15) by omega.
rewrite Zlength_correct in H0.
repeat match goal with
| _ => simpl; omega
| _ => rewrite nth_overflow
| _ => rewrite take_ge
| _ => rewrite getResidue_0
| _ => rewrite getCarry_0
| _ => rewrite ZofList_cons_0
| _ => f_equal ; ring
end.
+ rename e into H.
assert((length l = 15)%nat) by (rewrite Zlength_correct in H ; omega).
repeat (destruct l ; tryfalse).
clear H H0.
unfold nth , take.
change ([z; z0; z1; z2; z3; z4; z5; z6; z7; z8; z9; z10; z11; z12; z13]) with ([z; z0; z1; z2; z3; z4; z5; z6; z7; z8; z9; z10; z11; z12] ++ [ z13]).
rewrite ZofList_app ; try omega.
repeat rewrite ZofList_cons_0.
do 2 rewrite <- Zred_factor4 ; rewrite Zplus_assoc_reverse.
rewrite <- Z.add_mod_idemp_r by (compute ; omega);symmetry;rewrite <- Z.add_mod_idemp_r by (compute ; omega).
f_equal; f_equal.
rewrite Z.add_shuffle3.
rewrite <- Z.add_mod_idemp_r by (compute ; omega);symmetry;rewrite <- Z.add_mod_idemp_r by (compute ; omega).
f_equal; f_equal.
rewrite <- Z.add_mod_idemp_l by (compute ; omega) ; symmetry.
rewrite Zmult_mod.
rewrite <- t2256is38.
rewrite <- Zmult_mod.
rewrite Z.add_mod_idemp_l.
change 256 with (16 + 16 * 15).
orewrite Z.pow_add_r.
rewrite Zmult_assoc_reverse.
rewrite Zred_factor4.
rewrite Zmult_mod ; symmetry ; rewrite Zmult_mod.
f_equal;f_equal.
change (2 ^ (16 * 15)) with (2 ^ (16 * 14) * 2 ^ 16).
rewrite Zmult_mod.
symmetry.
rewrite Zmult_assoc_reverse ; rewrite Zred_factor4 ; rewrite Zmult_mod.
f_equal; f_equal.
rewrite Z.add_comm.
rewrite residuteCarry ; go.
compute; omega.
Qed.
Definition car25519 (l:list Z) : list Z := backCarry (Carrying_n 16 15 0 l).
......@@ -420,14 +303,24 @@ Qed.
Lemma bounds_car_inf_Zlength: forall i l, Zlength l = 16 -> 0 <= 16.lst l < 2^256 -> 0 <= nth i (car25519 l) 0.
Proof. convert_length_to_Zlength bounds_car_inf_length. Qed.
(* ADD LENGTH PROOF *)
Lemma car25519_length : forall l,
length l = 16%nat ->
length (car25519 l) = 16%nat.
Proof.
intros.
apply destruct_length_16 in H.
do 16 destruct H.
subst.
unfold car25519.
repeat rewrite Carry_n.Carry_n_step.
rewrite Carry_n.Carry_n_step_0.
reflexivity.
Qed.
Lemma car25519_Zlength : forall l,
Zlength l = 16 ->
Zlength (car25519 l) = 16.
Proof. convert_length_to_Zlength car25519_length. Qed.
Close Scope Z.
\ No newline at end of file
Require Import Tweetnacl.Libs.Export.
Require Import Tweetnacl.ListsOp.Export.
Require Import Tweetnacl.Car.Reduce.
Require Import Tweetnacl.Mid.M.
Require Import stdpp.prelude.
Require Import Tweetnacl.Mid.Reduce.
Local Open Scope Z.
Section Integer.
......@@ -116,10 +113,9 @@ Proof.
| [ |- -2^62 < getCarry _ _ _ < _ ] => apply getCarry_bound_str63
end.
Qed.
(* THIS QED IS REALLY SLOW... should be improved by reflection ... *)
Lemma Carry_n_length_False: forall (h:Z) (q:list Z), Carrying_n 16 15 0 (h :: q) = [] -> False.
Proof. intros ; rewrite Carry_n_step in H ; false. Qed.
Local Close Scope Z.
Require Import Tweetnacl.Libs.Export.
Require Import stdpp.prelude.
Require Import Recdef.
Local Open Scope Z.
......
Require Import Tweetnacl.Libs.Export.
Require Import stdpp.prelude.
Require Import Tweetnacl.Mid.Inner_M1.
Require Import Tweetnacl.Mid.Outer_M1.
Require Import Tweetnacl.Low.Inner_M1.
Require Import Tweetnacl.Low.Outer_M1.
Local Open Scope Z.
......
Require Import Tweetnacl.Libs.Export.
Require Import Tweetnacl.Mid.Inner_M1.
Require Import stdpp.prelude.
Require Import Tweetnacl.Low.Inner_M1.
Require Import Recdef.
Local Open Scope Z.
......
Require Import Tweetnacl.Libs.Export.
Require Import stdpp.prelude.
Open Scope Z.
......@@ -23,6 +22,6 @@ Proof. intros; unfold list_cswap; destruct (Z.eqb b 0); go. Qed.
Lemma list_cswap_Zlength_eq: forall b p q, Zlength p = Zlength q -> Zlength p = Zlength (list_cswap b p q).
Proof. intros; unfold list_cswap; destruct (Z.eqb b 0); go. Qed.
Close Scope Z.
Definition Sel25519 b p q := list_cswap b p q.
\ No newline at end of file
Require Import Tweetnacl.Libs.Export.
Require Import Tweetnacl.ListsOp.Export.
Require Import stdpp.prelude.
Open Scope Z.
......
......@@ -106,3 +106,5 @@ Proof. convert_length_to_Zlength ZsubList_bound_length_le. Qed.
End Integer.
Close Scope Z.
Definition Z a b := ZsubList a b.
\ No newline at end of file
default_target: .loadpath Libs ListsOp Mid Low Car Sel Unpack
default_target: .loadpath Libs ListsOp Mid Low
all: default_target High
......@@ -12,7 +12,7 @@ SHOW := $(if $(VERBOSE),@true "",@echo "")
HIDE := $(if $(VERBOSE),,@)
DIRS= Libs ListsOp Mid Car Sel High Unpack
DIRS= Libs ListsOp Mid Low High
INCLUDE= $(foreach a,$(DIRS),$(if $(wildcard $(a)), -Q $(a) $(a)))
COQFLAGS=$(foreach d, $(DIRS), $(if $(wildcard $(d)), -Q $(d) $(d))) $(EXTFLAGS)
......@@ -37,13 +37,11 @@ endif
LIBS_FILES = $(wildcard Libs/*.v)
LISTSOP_FILES = $(wildcard ListsOp/*.v)
MID_FILES = $(wildcard Mid/*.v)
CAR_FILES = $(wildcard Car/*.v)
SEL_FILES = $(wildcard Sel/*.v)
UNPACK_FILES = $(wildcard Unpack/*.v)
LOW_FILES = $(wildcard Low/*.v)
HIGH_FILES = $(wildcard High/*.v)
COUNTFILES = $(LIBS_FILES) $(LISTSOP_FILES) $(MID_FILES) $(CAR_FILES) \
$(SEL_FILES) $(UNPACK_FILES)
COUNTFILES = $(LIBS_FILES) $(LISTSOP_FILES) $(MID_FILES) $(LOW_FILES) \
$(UNPACK_FILES)
FILES = $(COUNTFILES) $(HIGH_FILES)
......@@ -87,9 +85,7 @@ quick: .loadpath $(FILES:.v=.vio)
Libs: .loadpath $(LIBS_FILES:%.v=%.vo)
ListsOp: .loadpath $(LISTSOP_FILES:%.v=%.vo)
Mid: .loadpath $(MID_FILES:%.v=%.vo)
Car: .loadpath $(CAR_FILES:%.v=%.vo)
Sel: .loadpath $(SEL_FILES:%.v=%.vo)
Unpack: .loadpath $(UNPACK_FILES:%.v=%.vo)
Low: .loadpath $(LOW_FILES:%.v=%.vo)
High: .loadpath $(HIGH_FILES:%.v=%.vo)
_CoqProject: Makefile
......
Require Import Tweetnacl.Libs.Export.
Require Import Tweetnacl.ListsOp.Export.
Require Import Tweetnacl.Car.Carry.
Require Import Tweetnacl.Car.ZCarry.
Require Import Tweetnacl.Car.Reduce.
Require Import stdpp.prelude.
Require Import Tweetnacl.Mid.Carry.
Require Import Tweetnacl.Mid.ZCarry.
Require Import Tweetnacl.Mid.Reduce.
Require Import Tweetnacl.Low.Car25519.
Open Scope Z.
......@@ -191,7 +191,7 @@ Proof.
rewrite <- Hcarr1 in H.
unfold car25519.
unfold backCarry.
unfold BackCarry.backCarry.
rename H into Hbound_strict.
rename Hl2 into H.
apply destruct_length_16 in H.
......@@ -246,21 +246,3 @@ Proof.
rewrite getCarry_1; omega.
Qed.
Lemma car25519_length : forall l,
length l = 16%nat ->
length (car25519 l) = 16%nat.
Proof.
intros.
apply destruct_length_16 in H.
do 16 destruct H.
subst.
unfold car25519.
repeat rewrite Carry_n.Carry_n_step.
rewrite Carry_n.Carry_n_step_0.
reflexivity.
Qed.
Lemma car25519_Zlength : forall l,
Zlength l = 16 ->
Zlength (car25519 l) = 16.
Proof. convert_length_to_Zlength car25519_length. Qed.
Require Import Tweetnacl.Libs.Export.
Require Import Tweetnacl.ListsOp.Export.
Require Import Tweetnacl.Mid.Reduce.
Require Import Tweetnacl.Low.Carry_n.
Local Open Scope Z.
Section Integer.
Variable n:Z.
Hypothesis Hn: n > 0.
Notation "ℤ.lst A" := (ZofList n A) (at level 65, right associativity).
Fixpoint Carrying (a:Z) (l:list Z) : list Z := match a,l with
| 0,[] => []
| a,[] => [a]
| a,h :: q => getResidue n (a + h) :: Carrying (getCarry n (a + h)) q
end.
Lemma Carrying_n_eq: forall l (m:nat) a, m = length l -> Carrying_n n m a l = Carrying a l.
Proof.
induction l as [|h q IHl]; intros m a Hm; go.
destruct m.
inv Hm.
simpl in *.
inversion Hm.
replace (h + a) with (a + h) by omega.
flatten ; f_equal ; go.
Qed.
Lemma Carrying_n_eq_Z: forall l (m:nat) a, Zlength l = m -> Carrying_n n m a l = Carrying a l.
Proof. convert_length_to_Zlength Carrying_n_eq. Qed.
Lemma CarryPreserveConst : forall l a , a + (.lst l) = .lst Carrying a l.
Proof.
induction l as [| h q IHl].
intro a ; destruct a ; assert(Hn0: 2 ^ n * 0 = 0) by (symmetry ; apply Zmult_0_r_reverse) ; simpl ; try rewrite Hn0 ; go.
intro a ; unfold Carrying ; fold Carrying.
flatten ;
unfold ZofList ; fold ZofList ; rewrite <- IHl ;
rewrite <- Zplus_assoc_reverse ;
rewrite <- Zred_factor4 ;
rewrite <- Zplus_assoc_reverse ;
rewrite residuteCarry ;
go.
Qed.
Corollary CarryPreserve : forall l, .lst l = .lst Carrying 0 l.
Proof.
intros.
symmetry.
rewrite -CarryPreserveConst.
omega.
Qed.
End Integer.
Close Scope Z.
(* ADD LENGTH PROOF *)
Require Export Tweetnacl.Mid.SumList.