Commit 4bec812b authored by Benoit Viguier's avatar Benoit Viguier
Browse files

cleaning up proofs

parent d5e242e3
......@@ -149,94 +149,19 @@ Lemma mul_assoc : associative mul.
Proof.
move=> [x1 x2] [y1 y2] [z1 z2].
solve_this.
(* Zmodp2_unfold; ring_unfold.
f_equal.
f_equal.
+ ring.
+ ring. *)
(* ; apply val_inj => /=.
+ rewrite Zminus_mod_idemp_r.
rewrite -(Zplus_mod (y1 * z1)).
rewrite Zmult_mod_idemp_r.
rewrite -(Zplus_mod (y1 * z2)).
rewrite Zmult_mod_idemp_r.
rewrite Zminus_mod_idemp_r.
rewrite -Zplus_mod.
rewrite Zminus_mod_idemp_r.
rewrite -(Zplus_mod (x1 * y1)).
rewrite Zmult_mod_idemp_l.
rewrite -(Zplus_mod (x1 * y2)).
rewrite Zmult_mod_idemp_l.
rewrite Zminus_mod_idemp_r.
rewrite -Zplus_mod.
have ->: (x1 * (y1 * z1 + (p - y2 * z2)) + (p - x2 * (y1 * z2 + y2 * z1)) =
x1 * (y1 * z1 + (- y2 * z2)) + (- x2 * (y1 * z2 + y2 * z1)) + (x1 + 1) * p)%Z by ring.
have ->: ((x1 * y1 + (p - x2 * y2)) * z1 + (p - (x1 * y2 + x2 * y1) * z2) =
x1 * (y1 * z1 + (- y2 * z2)) + (- x2 * (y1 * z2 + y2 * z1)) + (z1 + 1) * p)%Z by ring.
by rewrite ?Z_mod_plus_full.
+ rewrite Zminus_mod_idemp_r.
rewrite -(Zplus_mod (y1 * z2)).
rewrite Zmult_mod_idemp_r.
rewrite -(Zplus_mod (y1 * z1)).
rewrite Zmult_mod_idemp_r.
rewrite -Zplus_mod.
rewrite Zminus_mod_idemp_r.
rewrite -(Zplus_mod (x1 * y1)).
rewrite Zmult_mod_idemp_l.
rewrite -(Zplus_mod (x1 * y2)).
rewrite Zmult_mod_idemp_l.
rewrite -Zplus_mod.
have ->: (x1 * (y1 * z2 + y2 * z1) + x2 * (y1 * z1 + (p - y2 * z2)) =
x1 * (y1 * z2 + y2 * z1) + x2 * (y1 * z1 + ( - y2 * z2)) + (x2 * p))%Z by ring.
have ->: ((x1 * y1 + (p - x2 * y2)) * z2 + (x1 * y2 + x2 * y1) * z1 =
x1 * (y1 * z2 + y2 * z1) + x2 * (y1 * z1 + ( - y2 * z2)) + (z2 * p))%Z by ring.
by rewrite ?Z_mod_plus_full. *)
Qed.
Lemma mul_left_id : left_id one mul.
Proof.
move=> [x1 x2].
solve_this.
(* Zmodp2_unfold; ring_unfold.
rewrite Zmodp_ring.mul_left_id.
rewrite Zmodp_ring.mul_left_id.
have ->: Zmodp2 x1 x2 = pi (x1,x2) => //.
f_equal ; f_equal ; Zmodp_ringify ; ring_simplify_this. *)
Qed.
Lemma mul_left_distr : left_distributive mul add.
Proof.
move=> [x1 x2] [y1 y2] [z1 z2].
solve_this.
(* rewrite /mul /add /GRing.add /=. f_equal.
f_equal.
ring.
ring.
*)
(* + apply val_inj => /=.
rewrite Zmult_mod_idemp_l.
rewrite Zmult_mod_idemp_l.
rewrite Zminus_mod_idemp_r.
rewrite -Zplus_mod.
rewrite Zminus_mod_idemp_r.
rewrite Zminus_mod_idemp_r.
rewrite -(Zplus_mod (x1 * z1)).
rewrite -(Zplus_mod (y1 * z1)).
rewrite -Zplus_mod.
have ->: ((x1 + y1) * z1 + (p - (x2 + y2) * z2) =
(x1 + y1) * z1 + - (x2 + y2) * z2 + 1 * p)%Z by ring.
have ->: (x1 * z1 + (p - x2 * z2) + (y1 * z1 + (p - y2 * z2)) =
(x1 + y1) * z1 + - (x2 + y2) * z2 + 2 * p)%Z by ring.
by rewrite ?Z_mod_plus_full.
+ apply val_inj => /=.
rewrite Zmult_mod_idemp_l.
rewrite Zmult_mod_idemp_l.
rewrite -Zplus_mod.
rewrite -(Zplus_mod (x1 * z2)).
rewrite -(Zplus_mod (y1 * z2)).
rewrite -Zplus_mod.
f_equal.
ring. *)
Qed.
Lemma one_neq_zero : one != zero.
......@@ -283,16 +208,6 @@ Inductive Zinv_spec (x : type) : Type :=
| Zinv_spec_zero : x = zero -> Zinv_spec x
| Zinv_spec_unit : x <> zero -> forall y, (y * x)%R = one -> Zinv_spec x.
(* Local Ltac ringify := repeat match goal with
| [ |- context[Zmodp.pi 2]] => rewrite pi_2
| [ |- context[Zmodp.mul ?a ?b]] => have ->: (Zmodp.mul a b) = a * b => //
| [ |- context[Zmodp.add ?a (Zmodp.opp ?b)]] => have ->: (Zmodp.add a (Zmodp.opp b)) = a - b => //
| [ |- context[Zmodp.opp ?a]] => have ->: Zmodp.opp a = -a => //
| [ |- context[Zmodp.add ?a ?b]] => have ->: (Zmodp.add a b) = a + b => //
| [ |- context[Zmodp.one] ] => have ->: Zmodp.one = 1 => //
| [ |- context[Zmodp.zero] ] => have ->: Zmodp.zero = 0 => //
end.
*)
Lemma Zinv x : Zinv_spec x.
Proof.
case_eq (eqb x zero) ; move/eqb_spec.
......
......@@ -11,27 +11,6 @@ Import GRing.Theory.
Import Zmodp2.
Import BinInt.
(* Lemma expr3 : forall x:Zmodp2.type, x^+3 = x*x*x :> Zmodp2.type. *)
(* Proof. move => x; rewrite ?exprSr expr0 GRing.mul1r //. Qed. *)
(* Lemma expr3' : forall x:Zmodp.type, (x^+3 = x*x*x)%R. *)
(* Proof. move => x; rewrite ?exprSr expr0 GRing.mul1r //. Qed. *)
(* Ltac ring_simplify_this :=
repeat match goal with
| _ => rewrite GRing.exprS
| _ => rewrite GRing.expr0
| _ => rewrite GRing.mul1r
| _ => rewrite GRing.mulr1
| _ => rewrite GRing.mul0r
| _ => rewrite GRing.mulr0
| _ => rewrite GRing.add0r
| _ => rewrite GRing.oppr0
| _ => rewrite GRing.addr0
| _ => done
end.
*)
Local Ltac unfolds := ring_unfold; Zmodp2_unfold.
Ltac ringify := Zmodp_ringify ; Zmodp2_ringify.
......
(* Set Warnings "-notation-overridden".
Require Export Coq.ZArith.ZArith.
(* Require Export Coq.Lists.List. *)
(* Require Import Coq.Sorting.Sorting Orders. *)
(* Require Import ssreflect. *)
Require Import Tweetnacl.Libs.Decidable.
(* Require Import Tweetnacl.Libs.Term_Decidable. *)
Open Scope Z_scope.
(* Local Instance term_dec : Decidable :=
{
decide := term_decide;
denote := term_denote;
decide_impl := term_decide_impl
}.
*)
Section Bound.
(* Context {A:Type}.
*)
Inductive bound :=
| LE_inf : Z -> Z -> bound
| LT_inf : Z -> Z -> bound
| LE_sup : Z -> Z -> bound
| LT_sup : Z -> Z -> bound.
Fixpoint expr_denote (env:environment) (m : bound) : Prop :=
match m with
| LE_inf z a => z <= a
| LT_inf z a => z < a
| LE_sup z a => a <= z
| LT_sup z a => a < z
end.
Inductive bound_formula :=
| Bound_sgl : bound -> bound_formula
| Bound_And : bound_formula -> bound_formula -> bound_formula
| Bound_Impl : bound_formula -> bound_formula.
End Bound.
Close Scope Z. *)
\ No newline at end of file
......@@ -8,14 +8,6 @@ Require Import Tweetnacl.Libs.Decidable.
Require Import Tweetnacl.Libs.Term_Decidable.
Open Scope Z_scope.
(*
Instance term_dec : Decidable :=
{
decide := term_eqb;
denote := term_denote;
decide_impl := term_eqb_impl
}.
*)
Module TermOrder <: TotalLeBool.
Definition t := term.
......
......@@ -6,7 +6,7 @@ Open Scope Z_scope.
Section fun_rec.
Context {T:Type} (n:Z). (* (Hn : 0 <= n). *)
Context {T:Type} (n:Z).
Definition dec_proof_fun (n a : Z) : nat := Z.to_nat (a - n).
......
......@@ -4,8 +4,6 @@ From Tweetnacl Require Import Libs.Export.
From Tweetnacl Require Export ListsOp.ZofList.
Open Scope Z.
(* Import ListNotations. *)
Section Integer.
Variable n:Z.
......@@ -243,7 +241,6 @@ Proof.
replace (n * S m) with (n * m + n).
rewrite Zred_factor2 Z.pow_add_r ; try omega.
apply Zmult_le_compat_l ; try omega.
assert(minilemma : forall a b, a < b -> 1 + a <= b).
intros ; omega.
apply minilemma.
......@@ -310,8 +307,6 @@ Proof.
reflexivity.
simpl.
orewrite Z.shiftl_mul_pow2.
(* replace ((.lst l) * 2 ^ n) with (2^n * (.lst l)). *)
(* 2: rewrite Z.mul_comm ; reflexivity. *)
rewrite -IHl.
rewrite Zxor_add.
f_equal.
......
......@@ -59,8 +59,6 @@ Qed.
End Integer.
Close Scope Z.
(* ADD LENGTH PROOF *)
......
......@@ -95,11 +95,7 @@ Proof.
clear Hi Hi' i Hi''' H17.
rename H into Hi'.
assert(HH : forall k, 0 getResidue 16 k getResidue 16 k < 2 ^ 16) by (clear ; intro; eapply getResidue_bounds ; omega).
(* change (2^62) with 4611686018427387904 in *.
change (2^63) with 9223372036854775808 in *.
change (2^16) with 65536 in *.
*)
repeat match goal with
repeat match goal with
| _ => rewrite Carry_n_step
| _ => rewrite Carry_n_step_0
| [H : _ \/ _ |- _ ] => destruct H ; try subst i'
......
......@@ -12,8 +12,6 @@ Definition C_25519 := [65517;65535;65535;65535;65535;65535;65535;65535;65535;655
End Low.
(* Eval compute in ZofList 16 c_121665. *)
Lemma C_121665_bounds : Forall (fun x0 : => 0 <= x0 < 2 ^ 16) Low.C_121665.
Proof. unfold Low.C_121665;
repeat match goal with
......
Require Import Tweetnacl.Libs.Export.
Require Export Tweetnacl.Gen.Get_abcdef.
(*
Definition get_b (t:(list Z * list Z * list Z * list Z * list Z * list Z)) : list Z := match t with
(a,b,c,d,e,f) => b
end.
Definition get_c (t:(list Z * list Z * list Z * list Z * list Z * list Z)) : list Z := match t with
(a,b,c,d,e,f) => c
end.
Definition get_d (t:(list Z * list Z * list Z * list Z * list Z * list Z)) : list Z := match t with
(a,b,c,d,e,f) => d
end.
Definition get_e (t:(list Z * list Z * list Z * list Z * list Z * list Z)) : list Z := match t with
(a,b,c,d,e,f) => e
end.
Definition get_f (t:(list Z * list Z * list Z * list Z * list Z * list Z)) : list Z := match t with
(a,b,c,d,e,f) => f
end.
*)
Definition get_m (c:(list Z * list Z)) : list Z := match c with
(m,t) => m
end.
......
......@@ -124,11 +124,6 @@ Local Ltac solve_this_assert :=
eapply Forall_take_n_m ; [| eauto];
Grind_add_Z ; change_Z_to_nat ; omega.
(* rewrite sub_fn_rev_s_n; try omega;
rewrite sub_step_2_Z_inv_lss; Grind_add_Z; try assumption;
rewrite ?sub_fn_rev_s_sub_step_2_Zlength ; try omega;
apply bound_a_subst_step_2_lss ; auto ; omega.
*)
Local Ltac gen_goals P j n := match n with
| 0 => idtac
| n =>
......@@ -163,14 +158,6 @@ assert(H2: ℤ16.lst sub_fn_rev_s 1 sub_step_2 2 m = ℤ16.lst m).
rewrite sub_fn_rev_s_n ; try apply sub_step_2_Z_inv_lss; [omega | | omega].
assert(Haspe: 0 < 2 - 1 /\ 2 - 1 < 16) by omega.
apply Hbound in Haspe; omega.
(* assert ((fun x => (16.lst sub_fn_rev_s 1 sub_step_2 x m = 16.lst m)) 3).
rewrite sub_fn_rev_s_n; try omega;
rewrite sub_step_2_Z_inv_lss; Grind_add_Z; try assumption;
rewrite ?sub_fn_rev_s_sub_step_2_Zlength ; try omega;
apply bound_a_subst_step_2_lss ; auto ; try omega;
eapply Forall_take_n_m ; [| eauto];
Grind_add_Z ; change_Z_to_nat ; omega.
*)
gen_goals (fun x => (16.lst sub_fn_rev_s 1 sub_step_2 x m = 16.lst m)) 16 13.
assert_gen_hyp_ Hadec a 15 14 ; try omega.
repeat match goal with
......
......@@ -85,7 +85,6 @@ Local Ltac solve_dependencies_bound :=
repeat match goal with
| _ => assumption
| _ => reflexivity
(* | _ => solve_dependencies_length *)
| _ => apply M_bound_Zlength
| _ => apply Sq_bound_Zlength
| _ => apply A_bound_Zlength_le
......
From Tweetnacl Require Import Libs.Export.
Require Import ssreflect.
Require Import ZArith.
Local Open Scope Z.
Definition modP x := Z.modulo x (Z.pow 2 255 - 19).
......@@ -38,11 +38,6 @@ Z.ones 8;Z.ones 8;Z.ones 8;Z.ones 8;Z.ones 8;Z.ones 8;Z.ones 8;127]). *)
Definition Zclamp (n : Z) : Z :=
(Z.lor (Z.land n (Z.land (Z.ones 255) (-8))) (Z.shiftl 64 (31 * 8))).
(*
Lemma Zclamp_eq : forall n,
Zclamp' n = Zclamp n.
Proof. done. Qed.
*)
Lemma Zclamp_min n : 0 <= Zclamp n.
Proof.
rewrite /Zclamp.
......
......@@ -3,8 +3,6 @@ Require Import ssreflect.
Open Scope Z.
(*Notation "A :𝓖𝓕" := (A mod (2^255 - 19)) (at level 80, right associativity).*)
Lemma t2256is38 : (2^256 :𝓖𝓕 ) = (38 :𝓖𝓕).
Proof.
compute ; reflexivity.
......
This diff is collapsed.
......@@ -98,14 +98,7 @@ all: clean_context_from_VST.
all: rewrite /tkdp -?map_firstn -?map_skipn -?map_app in HHaux3.
all: rewrite /tkdp -?map_firstn -?map_skipn -?map_app in HHaux4.
all: inv HHaux1 ; inv HHaux2 ; inv HHaux3 ; inv HHaux4.
(* all: rewrite ?(Znth_map 0) ?take_drop_Zlength ; try omega. *)
all: rewrite add64_repr /nat_of_Z.
(* all: rewrite ?app_Znth2. *)
(* all: try replace (Zlength (firstn (Z.to_nat i) (A _ _))) with i. *)
(* all: rewrite ?Znth_skipn. *)
(* all: rewrite ?Zlength_firstn ?HA. *)
(* all: rewrite ?Z.max_r ?Z.min_l ; try omega. *)
(* all: replace (i - i + i) with i by omega. *)
all: rewrite ?Znth_nth; try omega.
all: rewrite <- ZsubList_nth_Zlength ; try omega.
all: rewrite /tkdp ?simple_S_i ; try omega.
......
......@@ -32,22 +32,6 @@ Local Instance list_term_dec : Decidable := Build_Decidable
Local Ltac solve_this_thing_please_autorewrite i j:=
subst i;
(* let H' := fresh in
gen_i H' j ; simpl;
repeat rewrite outer_M_i_j_eq by abstract omega;
repeat rewrite inner_M_i_j_eq by abstract omega;
repeat rewrite Znth_nth by abstract omega;
repeat rewrite upd_Znth_upd_nth by omega;
Grind_add_Z;
compute;
repeat rewrite Z.add_0_r;
repeat rewrite Z.add_0_l;
repeat rewrite Z.add_assoc;
reflexivity.
Opaque Z.add.
Opaque Z.mul.*)
let H' := fresh in
gen_i H' j ; simpl;
repeat orewrite inner_M_i_j_eq;
......@@ -101,26 +85,6 @@ Proof.
repeat (destruct H ; [solve_this_thing_please_autorewrite i j|]).
solve_this_thing_please_autorewrite i j.
Qed.
(*
intros i j a b Ha Hb Hi Hj Hii.
rewrite Zlength_correct in Ha.
rewrite Zlength_correct in Hb.
assert(Ha' : (length a = 16)%nat) by go.
assert(Hb' : (length b = 16)%nat) by go.
repeat (destruct a ; tryfalse).
repeat (destruct b ; tryfalse).
rewrite <- Zlength_correct in *.
rewrite (outer_M_fix_equation i).
flatten.
apply Z.leb_le in Eq ; omega.
clear Eq.
assert(H: i = 0 \/ i = 1 \/ i = 2 \/ i = 3) by omega.
destruct H ; try (subst i ; omega).
Opaque outer_M_fix.
repeat (destruct H ; [solve_this_thing_please_autorewrite i j|]). (* i = 1 -> 14 *)
solve_this_thing_please_autorewrite i j.
Qed.
*)
Lemma outer_M_fix_i_1'' : forall i j contents_a contents_b,
Zlength contents_a = 16 ->
......@@ -161,26 +125,6 @@ Proof.
repeat (destruct H ; [solve_this_thing_please_autorewrite i j|]).
solve_this_thing_please_autorewrite i j.
Qed.
(* Admitted. *)
(*
intros i j a b Ha Hb Hi Hj Hii.
rewrite Zlength_correct in Ha.
rewrite Zlength_correct in Hb.
assert(Ha' : (length a = 16)%nat) by go.
assert(Hb' : (length b = 16)%nat) by go.
repeat (destruct a ; tryfalse).
repeat (destruct b ; tryfalse).
rewrite <- Zlength_correct in *.
rewrite (outer_M_fix_equation i).
flatten.
apply Z.leb_le in Eq ; omega.
clear Eq.
assert(H: i = 4 \/ i = 5 \/ i = 6 \/ i = 7) by omega.
Opaque outer_M_fix.
repeat (destruct H ; [solve_this_thing_please_autorewrite i j|]). (* i = 1 -> 14 *)
solve_this_thing_please_autorewrite i j. (* i = 15 *)
Qed.
*)
Lemma outer_M_fix_i_1''' : forall i j contents_a contents_b,
Zlength contents_a = 16 ->
......@@ -221,26 +165,6 @@ Proof.
repeat (destruct H ; [solve_this_thing_please_autorewrite i j|]).
solve_this_thing_please_autorewrite i j.
Qed.
(* Admitted. *)
(*
intros i j a b Ha Hb Hi Hj Hii.
rewrite Zlength_correct in Ha.
rewrite Zlength_correct in Hb.
assert(Ha' : (length a = 16)%nat) by go.
assert(Hb' : (length b = 16)%nat) by go.
repeat (destruct a ; tryfalse).
repeat (destruct b ; tryfalse).
rewrite <- Zlength_correct in *.
rewrite (outer_M_fix_equation i).
flatten.
apply Z.leb_le in Eq ; omega.
clear Eq.
assert(H: i = 8 \/ i = 9 \/ i = 10 \/ i = 11 \/ i = 12) by omega.
Opaque outer_M_fix.
repeat (destruct H ; [solve_this_thing_please_autorewrite i j|]). (* i = 1 -> 14 *)
solve_this_thing_please_autorewrite i j. (* i = 15 *)
Qed.
*)
Lemma outer_M_fix_i_1'''' : forall i j contents_a contents_b,
Zlength contents_a = 16 ->
......@@ -282,26 +206,6 @@ Proof.
repeat (destruct H ; [solve_this_thing_please_autorewrite i j|]).
solve_this_thing_please_autorewrite i j.
Qed.
(* Admitted. *)
(*
intros i j a b Ha Hb Hi Hj Hii.
rewrite Zlength_correct in Ha.
rewrite Zlength_correct in Hb.
assert(Ha' : (length a = 16)%nat) by go.
assert(Hb' : (length b = 16)%nat) by go.
repeat (destruct a ; tryfalse).
repeat (destruct b ; tryfalse).
rewrite <- Zlength_correct in *.
rewrite (outer_M_fix_equation i).
flatten.
apply Z.leb_le in Eq ; omega.
clear Eq.
assert(H: i = 12 \/ i = 13 \/ i = 14 \/ i = 15) by omega.
Opaque outer_M_fix.
repeat (destruct H ; [solve_this_thing_please_autorewrite i j|]). (* i = 1 -> 14 *)
solve_this_thing_please_autorewrite i j. (* i = 15 *)
Qed.
*)
Lemma outer_M_fix_i_1 : forall i j contents_a contents_b,
Zlength contents_a = 16 ->
......
......@@ -253,7 +253,7 @@ Lemma data_at_sh_if : forall T SH i a b p ,
= data_at SH T (if 254 =? i then a else b) p.
Proof. intros ; flatten. Qed.
Local Ltac solve_lengths H48 H4 H5 H6 H7 := repeat match goal with
(* Local Ltac solve_lengths H48 H4 H5 H6 H7 := repeat match goal with
| _ => omega
| _ => rewrite H48
| _ => rewrite H4
......@@ -270,8 +270,8 @@ Local Ltac solve_lengths2 := repeat match goal with
| _ => rewrite undef16_Zlength
| _ => rewrite Zlength_map
end.
Lemma replace_list_app_app_app_app : forall i xx aa bb cc dd va vb vc vd,
*)
(* Lemma replace_list_app_app_app_app : forall i xx aa bb cc dd va vb vc vd,
0 <= i < 16 ->
Zlength aa = 16 ->
Zlength bb = 16 ->
......@@ -412,14 +412,5 @@ Proof.
rewrite ?simple_S_i ; try omega;
rewrite ?Hvd ?Hvb -upd_Znth_app_step_Zlength ; solve_lengths2.
Qed.
(* Definition sc_mult n p :=
let p' := Unpack25519 p in
let n' := clamp n in
let m := montgomery_fn 255 254 n' gf1 p' gf0 gf1 gf0 gf0 p' in
let c := get_c m in
let c' := Inv25519 c in
let a := get_a m in
Pack25519 (M a c').
*)
Close Scope Z.
......@@ -213,7 +213,6 @@ all: remember (pow_fn_rev 254 254 i i) as p. (* the expension is always anoying.
(* Goal 1 *)
1,2: freeze_local L.
(* rewrite {1}/Sfor. (* because forward_for_simple_bound does not work otherwise *) *)
1: forward_for_simple_bound 16 (copy_Inv L sho shi Tsh v_o v_o v_c (mVI64 i) i p 0) ; subst L.
1: thaw_local.
4: forward_for_simple_bound 16 (copy_Inv L sho shi Tsh v_o v_i v_c o i p 1) ; subst L.
......
Supports Markdown
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment