Commit d1f9f00e authored by Benoit Viguier's avatar Benoit Viguier
Browse files

add structure to the folder, change some library settings

parent 97451271
# Object files, in general
*.o
*.a
*.cmi
*.cmo
*.cmx
*.cma
*.cmxa
.*.aux
*.cmti
*.cmt
*.merlin
*.vo
*.glob
*.v.d
.depend
.loadpath
*.cache
*~
*#
.#*
*.aux
*.bck *.bck
*.bak *.bak
bin bin
Debug Debug
others
ipch ipch
.idea .idea
*.pdf *.pdf
......
/* Hello World program */
#include <stdlib.h>
#include <stdio.h>
typedef unsigned char u8;
typedef unsigned long u32;
typedef unsigned long long u64;
typedef long long i64;
typedef i64 gf[16];
#define BYTE_TO_BINARY_PATTERN "%c%c%c%c%c%c%c%c"
#define BYTE_TO_BINARY(byte) \
(byte & 0x80 ? '1' : '0'), \
(byte & 0x40 ? '1' : '0'), \
(byte & 0x20 ? '1' : '0'), \
(byte & 0x10 ? '1' : '0'), \
(byte & 0x08 ? '1' : '0'), \
(byte & 0x04 ? '1' : '0'), \
(byte & 0x02 ? '1' : '0'), \
(byte & 0x01 ? '1' : '0')
static void A(gf o,const gf a,const gf b)
{
int i;
for (i = 0;i < 16;++i) o[i]=a[i]+b[i];
}
static void printb64(i64 val)
{
printf(BYTE_TO_BINARY_PATTERN BYTE_TO_BINARY_PATTERN BYTE_TO_BINARY_PATTERN BYTE_TO_BINARY_PATTERN BYTE_TO_BINARY_PATTERN BYTE_TO_BINARY_PATTERN BYTE_TO_BINARY_PATTERN BYTE_TO_BINARY_PATTERN,
BYTE_TO_BINARY(val>>56), BYTE_TO_BINARY(val>>48), BYTE_TO_BINARY(val>>40), BYTE_TO_BINARY(val>>32), BYTE_TO_BINARY(val>>24), BYTE_TO_BINARY(val>>16), BYTE_TO_BINARY(val>>8), BYTE_TO_BINARY(val));
}
int main() {
int i;
gf a, b, o;
for (i = 0; i < 16; ++i)
{
a[i] = 0;
b[i] = 0;
o[i] = 0;
}
a[0] = ((long long) 1) << 62;
b[0] = ((long long) 1) << 62;
A(o,a,b);
printb64(a[0]);
printf("\n");
printb64(b[0]);
printf("\n");
printb64(o[0]);
printf("\n");
return 1;
}
\ No newline at end of file
Require Export Coq.ZArith.ZArith.
Require Import Psatz.
Open Scope Z.
Lemma Zred_factor6 : forall m n, (1 + m) * n = n + n * m.
Proof. intros ; Psatz.nia. Qed.
Lemma Zred_factor7 : forall m n, (1 + m) * n = n + m * n.
Proof. intros ; Psatz.nia. Qed.
Lemma Zred_factor8: forall n m p : Z, m * n + p * n = (m + p) * n.
Proof. intros ; Psatz.nia. Qed.
Fact le_mul_neg : forall m n, m < 0 -> 1 <= n -> n * m <= m.
Proof. intros m n Hm Hn. Psatz.nia. Qed.
Fact le_mul_pos : forall m n, 0 < m -> 1 <= n -> m <= n * m.
Proof. intros m n Hm Hn. Psatz.nia. Qed.
Lemma le_mul_neg_le: forall m n : Z, m <= 0 -> 1 <= n -> n * m <= m.
Proof. intros m n Hm Hn. Psatz.nia. Qed.
Fact le_mul_pos_le : forall m n, 0 <= m -> 1 <= n -> m <= n * m.
Proof. intros m n Hm Hn. Psatz.nia. Qed.
Close Scope Z.
\ No newline at end of file
Require Export ZCarry. Require Import Libs.Export.
Require Export Forall_ZofList. Require Import ListsOp.Export.
Require Export TrippleRel. Require Import Car.Carry.
Require Import Car.ZCarry.
Require Import Car.Reduce.
Open Scope Z. Open Scope Z.
...@@ -25,9 +27,10 @@ Proof. ...@@ -25,9 +27,10 @@ Proof.
[apply bounds_car_inf| apply bounds_car_sup]; [apply bounds_car_inf| apply bounds_car_sup];
try assumption ; rewrite Hcarr2; try assumption ; rewrite Hcarr2;
rewrite <- car25519_eq_car25519 by assumption; rewrite <- car25519_eq_car25519 by assumption;
eapply (doubleCar_ext_str (16.lst l1) _ 303) ; eapply (doubleCar_ext_str (16.lst l1) _ 303) ;
try omega ; try (eapply le_lt_trans ; [eapply Hbounds| | ] ; compute ; reflexivity); try omega ;
try (eapply bounds.le_lt_trans ; [eapply Hbounds | | ] ; compute ; reflexivity) ;
try (rewrite car25519_eq_car25519 by assumption ; rewrite Hcarr1 ; reflexivity). try (rewrite car25519_eq_car25519 by assumption ; rewrite Hcarr1 ; reflexivity).
compute ; auto. compute ; auto.
apply HForalll1. apply HForalll1.
Qed. Qed.
\ No newline at end of file
Require Export ZofList. Require Import Libs.Export.
Require Export Reduce. Require Import ListsOp.Export.
Require Import Car.Reduce.
Import ListNotations. Import ListNotations.
Section Integer. Section Integer.
...@@ -392,7 +394,7 @@ Proof. ...@@ -392,7 +394,7 @@ Proof.
unfold length. unfold length.
unfold nth. unfold nth.
unfold slice. unfold slice.
unfold Tools.tail. unfold tail.
rewrite <- Zred_factor4. rewrite <- Zred_factor4.
rewrite Zmult_minus_distr_l. rewrite Zmult_minus_distr_l.
rewrite <- Zred_factor4. rewrite <- Zred_factor4.
......
Require Export Tools. Require Import Libs.Export.
Require Export ZofList. Require Import ListsOp.Export.
Require Export Calc_lib.
Require Export notations.
Open Scope Z. Open Scope Z.
......
Require Export Carry. Require Import Libs.Export.
Require Import Car.Carry.
Require Import Car.Reduce.
Require Import Nsatz. Require Import Nsatz.
Require Import Psatz. Require Import Psatz.
Import ListNotations. Import ListNotations.
...@@ -358,7 +360,7 @@ Lemma doubleCar_str: ...@@ -358,7 +360,7 @@ Lemma doubleCar_str:
y = Zcar25519 x -> y = Zcar25519 x ->
Zcar25519 y < 2 ^ 256. Zcar25519 y < 2 ^ 256.
Proof. Proof.
Print Zcar25519. Print getCarry. (*Print Zcar25519. Print getCarry.*)
intros x y m Hm Hx Hy. intros x y m Hm Hx Hy.
assert(Hx_dec: x = 0 \/ 0 < x < 2^256 \/ 2 ^ 256 <= x) by omega. assert(Hx_dec: x = 0 \/ 0 < x < 2^256 \/ 2 ^ 256 <= x) by omega.
assert(Hy_dec: y < 0 \/ 0 <= y < 2^256 \/ 2 ^ 256 <= y) by omega. assert(Hy_dec: y < 0 \/ 0 <= y < 2^256 \/ 2 ^ 256 <= y) by omega.
......
Require Export Libs.LibTactics_SF.
Require Export Libs.LibTactics_Rennes.
Require Export Libs.LibTactics.
Require Export Libs.Lists_extended.
Require Export Libs.Forall.
Require Export Libs.Forall_extended.
Require Export Libs.Logic_extended.
Require Export Libs.ZArith_extended.
Require Export Libs.Relations.
Require Export Coq.ZArith.BinInt. Require Export Coq.ZArith.BinInt.
Require Export Coq.ZArith.Zdiv. Require Export Coq.ZArith.Zdiv.
......
Require Export Tools. Require Export Libs.Lists_extended.
Require Export Forall. Require Export Libs.Forall.
Lemma Forall_slice: forall n A (l:list A) (P:A -> Prop), Lemma Forall_slice: forall n A (l:list A) (P:A -> Prop),
Forall P l -> Forall P l ->
......
Require Export Libs.LibTactics_Rennes.
Ltac transparent_specialize_one H arg :=
first [ let test := eval unfold H in H in idtac;
let H' := fresh in rename H into H'; pose (H' arg) as H; subst H'
| specialize (H arg) ].
Ltac specialize_by' tac :=
idtac;
match goal with
| [ H : ?A -> ?B |- _ ] =>
match type of A with
Prop =>
let H' := fresh in
assert (H' : A) by tac;
transparent_specialize_one H H';
try clear H' (* if [H] was transparent, [H'] will remain *)
end
end.
Ltac specialize_by tac := repeat specialize_by' tac.
Ltac boum :=
repeat match goal with
| [ |- context[_ <-> _] ] => progress split
| [ H : _ /\ _ |- _ ] => progress destruct H
| [ H : _ \/ _ |- _ ] => progress destruct H
| _ => progress intros
| _ => go
end.
Ltac ind_boum l :=
induction l ; boum.
Ltac destr_boum n :=
destruct n ; boum.
Ltac inv_boum H :=
inversion H ; boum.
...@@ -2,15 +2,11 @@ Require Export Coq.Bool.Bool. ...@@ -2,15 +2,11 @@ Require Export Coq.Bool.Bool.
Require Export Coq.Arith.Arith. Require Export Coq.Arith.Arith.
Require Export Coq.Arith.EqNat. Require Export Coq.Arith.EqNat.
Require Export Coq.omega.Omega. Require Export Coq.omega.Omega.
Require Export Coq.Lists.List.
Require Export Coq.ZArith.ZArith. Require Export Coq.ZArith.ZArith.
Require Export Coq.Numbers.Natural.Peano.NPeano. Require Export Coq.Numbers.Natural.Peano.NPeano.
Require Export Coq.Setoids.Setoid. Require Export Coq.Setoids.Setoid.
Require Export Coq.Program.Equality. (**r Necessary for 'dependent induction'. *) Require Export Coq.Program.Equality. (**r Necessary for 'dependent induction'. *)
Require Export LibTactics.
Ltac autoinjection := Ltac autoinjection :=
repeat match goal with repeat match goal with
| h: ?f _ = ?f _ |- _ => injection h; intros; clear h; subst | h: ?f _ = ?f _ |- _ => injection h; intros; clear h; subst
......
Require Export Libs. Require Export Libs.LibTactics.
Require Export Coq.Lists.List.
Set Implicit Arguments.
Import ListNotations. Import ListNotations.
(* Iterative tools *)
Section All.
Variable T : Type.
Variable T1 : Type.
Variable T2 : Type.
Fixpoint All (o: T -> T1 -> T1) (d:T1) (ls:list T) : T1 := match ls with
| nil => d
| h :: q => o h (All o d q)
end.
End All.
Section AllApp.
Variable T : Type.
Variable T2 : Type.
Variable P : T -> Prop.
Variable V : T -> nat.
Variable V2 : T -> T2.
Variable LS : T -> list T2.
Definition orAll (ls:list Prop): Prop :=
All or False ls.
Definition andAll (ls: list Prop): Prop :=
All and True ls.
Definition SumAll (ls:list nat) : nat :=
All plus 0 ls.
Definition MaxAll (ls:list nat) : nat :=
All max 0 ls.
Inductive orderedList : list nat -> Prop :=
| NilOrdered : orderedList nil
| SingletonOrdered n : orderedList (n::nil)
| ConOrdered a h q
(ORDER: a < h)
(ORDERED: orderedList (h::q))
: (* ===================== *)
orderedList (a::h::q).
End AllApp.
(* Lists Tools *)
Lemma app_nill_r : forall (A:Type) (l:list A), l ++ nil = l. Lemma app_nill_r : forall (A:Type) (l:list A), l ++ nil = l.
Proof. go. Qed. Proof. boum. Qed.
Lemma app_nill_l : forall (A:Type) (l:list A), nil ++ l = l. Lemma app_nill_l : forall (A:Type) (l:list A), nil ++ l = l.
Proof. go. Qed. Proof. boum. Qed.
Lemma headSame : forall A (h1 h2: A) (q1 q2:list A), h1 :: q1 = h2 :: q2 -> h1 = h2. Lemma headSame : forall A (h1 h2: A) (q1 q2:list A), h1 :: q1 = h2 :: q2 -> h1 = h2.
Proof. go. Qed. Proof. boum. Qed.
Lemma tailSame : forall A (h1 h2: A) (q1 q2:list A), h1 :: q1 = h2 :: q2 -> q1 = q2. Lemma tailSame : forall A (h1 h2: A) (q1 q2:list A), h1 :: q1 = h2 :: q2 -> q1 = q2.
Proof. go. Qed. Proof. boum. Qed.
Lemma ListSame : forall A (h1 h2: A) (q1 q2:list A), h1 :: q1 = h2 :: q2 <-> h1 = h2 /\ q1 = q2. Lemma ListSame : forall A (h1 h2: A) (q1 q2:list A), h1 :: q1 = h2 :: q2 <-> h1 = h2 /\ q1 = q2.
Proof. split ; intro; [|destruct H] ; go. Qed. Proof. boum. Qed.
Lemma length_cons : forall (A:Type) (h:A) (q:list A), length (h :: q) = S (length q). Lemma length_cons : forall (A:Type) (h:A) (q:list A), length (h :: q) = S (length q).
Proof. intros. go. Qed. Proof. boum. Qed.
Lemma lengthNil : forall (A:Type) (l:list A), l = nil <-> length l = 0. Lemma lengthNil : forall (A:Type) (l:list A), l = nil <-> length l = 0.
Proof. intros. split ; intro ; induction l ; go. Qed. Proof. ind_boum l. Qed.
Lemma consApp : forall A l (a:A), a :: l = a :: nil ++ l. Lemma consApp : forall A l (a:A), a :: l = a :: nil ++ l.
Proof. go. Qed. Proof. boum. Qed.
Lemma consApp2 : forall A l1 l2 (a:A), (a :: l1) ++ l2 = a :: l1 ++ l2. Lemma consApp2 : forall A l1 l2 (a:A), (a :: l1) ++ l2 = a :: l1 ++ l2.
Proof. go. Qed. Proof. boum. Qed.
Lemma consApp3 : forall A l1 l2 (a:A), l1 ++ a :: l2 = (l1 ++ a :: nil) ++ l2. Lemma consApp3 : forall A l1 l2 (a:A), l1 ++ a :: l2 = (l1 ++ a :: nil) ++ l2.
Proof. induction l1 ; intros ; go. Qed. Proof. ind_boum l1. Qed.
Lemma app_assoc2 : forall (A:Type) (l1 l2 l3:list A), l1 ++ l2 ++ l3 = l1 ++ (l2 ++ l3). Lemma app_assoc2 : forall (A:Type) (l1 l2 l3:list A), l1 ++ l2 ++ l3 = l1 ++ (l2 ++ l3).
Proof. go. Qed. Proof. boum. Qed.
Lemma list_to_length: forall A (l1 l2:list A), l1 = l2 -> length l1 = length l2. Lemma list_to_length: forall A (l1 l2:list A), l1 = l2 -> length l1 = length l2.
Proof. go. Qed. Proof. boum. Qed.
Lemma list_eq_False : forall (A:Type) (l:list A) (a:A), a :: l = l -> False. Lemma list_eq_False : forall (A:Type) (l:list A) (a:A), a :: l = l -> False.
Proof. dependent induction l ; intros ; inversion H ; eapply IHl ; eauto. Qed. Proof. ind_boum l. Qed.
Lemma app_inv : forall A (l1 l2 l3 l4:list A), l1 = l2 -> l3 = l4 -> l1 ++ l3 = l2 ++ l4. Lemma app_inv : forall A (l1 l2 l3 l4:list A), l1 = l2 -> l3 = l4 -> l1 ++ l3 = l2 ++ l4.
Proof. induction l1 ; destruct l2 ; intros ; go. Qed. Proof. ind_boum l1. Qed.
Lemma orderedCon : forall l a, orderedList (a :: l) -> orderedList l.
Proof. intros ; dependent induction H ; go. Qed.
Lemma orderedConcat : forall l1 l2, orderedList (l1 ++ l2) -> orderedList l1 /\ orderedList l2. Theorem appappNil: forall A (l1 l2:list A), l1 ++ l2 = nil -> l1 = nil /\ l2 = nil.
Proof. Proof. boum. Qed.
intros.
split.
- dependent induction l1 ; go.
+ dependent induction l1.
* go.
* apply ConOrdered.
inv H ; go.
apply IHl0 with l2.
apply orderedCon with a.
go.
- induction l1.
+ go.
+ apply IHl1.
apply orderedCon with a.
go.
Qed.
Lemma rev_nth_error : forall A (l:list A) n, n < length l -> Lemma rev_nth_error : forall A (l:list A) n, n < length l ->
nth_error (rev l) n = nth_error l (length l - S n). nth_error (rev l) n = nth_error l (length l - S n).
Proof. Proof.
induction l. ind_boum l.
- intros.
inversion H.
- intros.
simpl in H. simpl in H.
simpl (rev (a::l)). simpl (rev (a::l)).
simpl (length (a :: l) - S n). simpl (length (a :: l) - S n).
...@@ -135,26 +67,6 @@ Proof. ...@@ -135,26 +67,6 @@ Proof.
rewrite rev_length; auto. rewrite rev_length; auto.
Qed. Qed.
Ltac transparent_specialize_one H arg :=
first [ let test := eval unfold H in H in idtac;
let H' := fresh in rename H into H'; pose (H' arg) as H; subst H'
| specialize (H arg) ].
Ltac specialize_by' tac :=
idtac;
match goal with
| [ H : ?A -> ?B |- _ ] =>
match type of A with
Prop =>
let H' := fresh in
assert (H' : A) by tac;
transparent_specialize_one H H';
try clear H' (* if [H] was transparent, [H'] will remain *)
end
end.
Ltac specialize_by tac := repeat specialize_by' tac.
Lemma NoDup_rev_impl: forall A (l: list A), NoDup l -> NoDup (rev l). Lemma NoDup_rev_impl: forall A (l: list A), NoDup l -> NoDup (rev l).
Proof. Proof.
intros A l. intros A l.
...@@ -204,90 +116,28 @@ Proof. ...@@ -204,90 +116,28 @@ Proof.
end. end.
Qed. Qed.
Fixpoint beq_listnat (l1 l2:list nat) : bool := match (l1,l2) with
| (nil, nil) => true
| (h1 :: q1, h2 :: q2) => (beq_nat h1 h2) && (beq_listnat q1 q2)
| _ => false
end.
Fact listEqRefl : forall l, beq_listnat l l = true.
Proof.
induction l ; go.
apply andb_true_iff ; split ; go ; rewrite beq_nat_refl with a; go.
Qed.
(* props*)
Lemma orFalse : forall (P:Prop), P \/ False <-> P.
Proof. intros ; split ; intro ; [destruct H|] ; go. Qed.
Lemma Falseor : forall (P:Prop), False \/ P <-> P.
Proof. intros ; split ; intro ; [destruct H|] ; go. Qed.
Lemma andTrue : forall (P:Prop), P /\ True <-> P.
Proof. intros ; split ; intro; [destruct H|] ; go. Qed.
Lemma Trueand : forall (P:Prop), True /\ P <-> P.
Proof. intros ; split ; intro; [destruct H|] ; go. Qed.
Theorem GaussSum: forall a b c, a + c = b + c <-> a = b.
Proof. intros ; split ; intros ; omega. Qed.
(* Tupples *)
Lemma tupple_eq : forall A B (x1 x2:A) (y1 y2:B), (x1,y1) = (x2,y2) <->
(x1 = x2 /\ y1 = y2).
Proof. intros ; split ; intro ; go ; destruct H as [Hx Hy] ; go. Qed.
Theorem consconsNil: forall A (l1 l2:list A), l1 ++ l2 = nil -> l1 = nil /\ l2 = nil.
Proof. go. Qed.
Fact flat_map_map X Y Z (f : Y -> list Z) (g : X -> Y) l :
flat_map f (map g l) = flat_map (fun x => f (g x)) l.
Proof. induction l; simpl; f_equal; auto. Qed.
Fact flat_map_distr Y Z (f : Y -> list Z) l1 l2 :
flat_map f (l1 ++ l2) = flat_map f l1 ++ flat_map f l2.
Proof. induction l1 ; go ; simpl ; rewrite IHl1 ; go. Qed.
Fact flat_map_ext X Y (f g : X -> list Y) l :
(forall x, In x l -> f x = g x) -> flat_map f l = flat_map g l.
Proof. induction l; simpl; intro; f_equal; auto. Qed.
Fact map_ext X Y (f g : X -> Y) l :
(forall x, In x l -> f x = g x) -> map f l = map g l.
Proof. induction l; simpl; intro; f_equal; auto. Qed.
Lemma sumAllapp : forall (h:nat) (q:list nat), SumAll (h::q) = h + SumAll q.
Proof. intros ; induction q ; go. Qed.
Theorem SomeEq: forall A (a b:A), Some a = Some b <-> a = b.
Proof. go. Qed.
Lemma nth_error_Some_Eq : forall A (l:list A) n, n < length l -> exists st, nth_error l n = Some st.