Commit 78b09e76 authored by benoit's avatar benoit
Browse files

fix

parent 510cad59
......@@ -17,6 +17,7 @@
.depend
.loadpath
_CoqProject
!packages/**/_CoqProject
*.cache
*~
*#
......
DIST=coq-verif-tweetnacl
# NO_COLOR="\033[0m"
# RED = "\033[38;5;009m"
# GREEN = "\033[38;5;010m"
# YELLOW = "\033[38;5;011m"
# ORANGE = "\033[38;5;214m"
# LIGHTPURPLE = "\033[38;5;177m"
# PURPLE = "\033[38;5;135m"
# CYAN = "\033[38;5;014m"
# LIGHTGRAY = "\033[38;5;252m"
# DARKGRAY = "\033[38;5;242m"
# BRIGHTRED = "\033[91m"
# BOLD = "\033[1m"
#
# all: coq-tweetnacl-spec coq-tweetnacl-vst
include coq.mk
.PHONY: clean
clean: clean-spec clean-vst clean-dist
# build paper
.PHONY: paper
paper:
@cd paper && $(MAKE)
clean-paper:
cd paper && $(MAKE) clean
# generate artefact
$(DIST):
@echo $(BOLD)$(ORANGE)"Creating $(DIST)"$(NO_COLOR)$(DARKGRAY)
mkdir $(DIST)
$(DIST)/specs_map.pdf:
@echo $(BOLD)$(YELLOW)"Building map for specs"$(NO_COLOR)$(DARKGRAY)
cd paper && $(MAKE) specs_map.pdf
mv specs_map.pdf $(DIST)/specs_map.pdf
dist: clean-dist $(DIST) $(DIST)/specs_map.pdf
@echo $(BOLD)$(YELLOW)"Preparing $(DIST)"$(NO_COLOR)$(DARKGRAY)
cp -r proofs $(DIST)
cd $(DIST)/proofs/spec && $(MAKE) clean
cd $(DIST)/proofs/vst && $(MAKE) clean
mkdir $(DIST)/packages
cp -r packages/coq-compcert $(DIST)/packages/
cp -r packages/coq-reciprocity $(DIST)/packages/
cp -r packages/coq-ssr-elliptic-curves $(DIST)/packages/
cp -r packages/coq-vst $(DIST)/packages/
cp repo $(DIST)/
cp version $(DIST)/
cp README.md $(DIST)/
cp coq.mk $(DIST)/Makefile
cp opam $(DIST)/
@echo $(BOLD)$(LIGHTPURPLE)"Building $(DIST).tar.gz"$(NO_COLOR)$(DARKGRAY)
tar -czvf $(DIST).tar.gz $(DIST)
@echo $(BOLD)$(GREEN)"Done."$(NO_COLOR)
clean-dist:
@echo $(BOLD)$(YELLOW)"removing $(DIST)"$(NO_COLOR)$(DARKGRAY)
-rm -r $(DIST)
-rm $(DIST).tar.gz
@echo $(BOLD)$(GREEN)"Done."$(NO_COLOR)
BigN/NMake_gen.v
*.d
*.o
*.cmi
*.cmx
*.cmxs
*.vo
*.glob
*.aux
Makefile.coq
Makefile.coq.conf
(************************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
(** * Efficient arbitrary large natural numbers in base 2^31 *)
(** Initial Author: Arnaud Spiwack *)
Require Export Int31.
Require Import CyclicAxioms Cyclic31 Ring31 NSig NSigNAxioms NMake
NProperties GenericMinMax.
(** The following [BigN] module regroups both the operations and
all the abstract properties:
- [NMake.Make Int31Cyclic] provides the operations and basic specs
w.r.t. ZArith
- [NTypeIsNAxioms] shows (mainly) that these operations implement
the interface [NAxioms]
- [NProp] adds all generic properties derived from [NAxioms]
- [MinMax*Properties] provides properties of [min] and [max].
*)
Delimit Scope bigN_scope with bigN.
Module BigN <: NType <: OrderedTypeFull <: TotalOrder :=
NMake.Make Int31Cyclic
<+ NTypeIsNAxioms
<+ NBasicProp [no inline] <+ NExtraProp [no inline]
<+ HasEqBool2Dec [no inline]
<+ MinMaxLogicalProperties [no inline]
<+ MinMaxDecProperties [no inline].
(** Notations about [BigN] *)
Local Open Scope bigN_scope.
Notation bigN := BigN.t.
Bind Scope bigN_scope with bigN BigN.t BigN.t'.
Arguments BigN.N0 _%int31.
Local Notation "0" := BigN.zero : bigN_scope. (* temporary notation *)
Local Notation "1" := BigN.one : bigN_scope. (* temporary notation *)
Local Notation "2" := BigN.two : bigN_scope. (* temporary notation *)
Infix "+" := BigN.add : bigN_scope.
Infix "-" := BigN.sub : bigN_scope.
Infix "*" := BigN.mul : bigN_scope.
Infix "/" := BigN.div : bigN_scope.
Infix "^" := BigN.pow : bigN_scope.
Infix "?=" := BigN.compare : bigN_scope.
Infix "=?" := BigN.eqb (at level 70, no associativity) : bigN_scope.
Infix "<=?" := BigN.leb (at level 70, no associativity) : bigN_scope.
Infix "<?" := BigN.ltb (at level 70, no associativity) : bigN_scope.
Infix "==" := BigN.eq (at level 70, no associativity) : bigN_scope.
Notation "x != y" := (~x==y) (at level 70, no associativity) : bigN_scope.
Infix "<" := BigN.lt : bigN_scope.
Infix "<=" := BigN.le : bigN_scope.
Notation "x > y" := (y < x) (only parsing) : bigN_scope.
Notation "x >= y" := (y <= x) (only parsing) : bigN_scope.
Notation "x < y < z" := (x<y /\ y<z) : bigN_scope.
Notation "x < y <= z" := (x<y /\ y<=z) : bigN_scope.
Notation "x <= y < z" := (x<=y /\ y<z) : bigN_scope.
Notation "x <= y <= z" := (x<=y /\ y<=z) : bigN_scope.
Notation "[ i ]" := (BigN.to_Z i) : bigN_scope.
Infix "mod" := BigN.modulo (at level 40, no associativity) : bigN_scope.
(** Example of reasoning about [BigN] *)
Theorem succ_pred: forall q : bigN,
0 < q -> BigN.succ (BigN.pred q) == q.
Proof.
intros; apply BigN.succ_pred.
intro H'; rewrite H' in H; discriminate.
Qed.
(** [BigN] is a semi-ring *)
Lemma BigNring : semi_ring_theory 0 1 BigN.add BigN.mul BigN.eq.
Proof.
constructor.
exact BigN.add_0_l. exact BigN.add_comm. exact BigN.add_assoc.
exact BigN.mul_1_l. exact BigN.mul_0_l. exact BigN.mul_comm.
exact BigN.mul_assoc. exact BigN.mul_add_distr_r.
Qed.
Lemma BigNeqb_correct : forall x y, (x =? y) = true -> x==y.
Proof. now apply BigN.eqb_eq. Qed.
Lemma BigNpower : power_theory 1 BigN.mul BigN.eq BigN.of_N BigN.pow.
Proof.
constructor.
intros. red. rewrite BigN.spec_pow, BigN.spec_of_N.
rewrite Zpower_theory.(rpow_pow_N).
destruct n; simpl. reflexivity.
induction p; simpl; intros; BigN.zify; rewrite ?IHp; auto.
Qed.
Lemma BigNdiv : div_theory BigN.eq BigN.add BigN.mul (@id _)
(fun a b => if b =? 0 then (0,a) else BigN.div_eucl a b).
Proof.
constructor. unfold id. intros a b.
BigN.zify.
case Z.eqb_spec.
BigN.zify. auto with zarith.
intros NEQ.
generalize (BigN.spec_div_eucl a b).
generalize (Z_div_mod_full [a] [b] NEQ).
destruct BigN.div_eucl as (q,r), Z.div_eucl as (q',r').
intros (EQ,_). injection 1 as EQr EQq.
BigN.zify. rewrite EQr, EQq; auto.
Qed.
(** Detection of constants *)
Ltac isStaticWordCst t :=
match t with
| W0 => constr:(true)
| WW ?t1 ?t2 =>
match isStaticWordCst t1 with
| false => constr:(false)
| true => isStaticWordCst t2
end
| _ => isInt31cst t
end.
Ltac isBigNcst t :=
match t with
| BigN.N0 ?t => isStaticWordCst t
| BigN.N1 ?t => isStaticWordCst t
| BigN.N2 ?t => isStaticWordCst t
| BigN.N3 ?t => isStaticWordCst t
| BigN.N4 ?t => isStaticWordCst t
| BigN.N5 ?t => isStaticWordCst t
| BigN.N6 ?t => isStaticWordCst t
| BigN.Nn ?n ?t => match isnatcst n with
| true => isStaticWordCst t
| false => constr:(false)
end
| BigN.zero => constr:(true)
| BigN.one => constr:(true)
| BigN.two => constr:(true)
| _ => constr:(false)
end.
Ltac BigNcst t :=
match isBigNcst t with
| true => constr:(t)
| false => constr:(NotConstant)
end.
Ltac BigN_to_N t :=
match isBigNcst t with
| true => eval vm_compute in (BigN.to_N t)
| false => constr:(NotConstant)
end.
Ltac Ncst t :=
match isNcst t with
| true => constr:(t)
| false => constr:(NotConstant)
end.
(** Registration for the "ring" tactic *)
Add Ring BigNr : BigNring
(decidable BigNeqb_correct,
constants [BigNcst],
power_tac BigNpower [BigN_to_N],
div BigNdiv).
Section TestRing.
Let test : forall x y, 1 + x*y^1 + x^2 + 1 == 1*1 + 1 + y*x + 1*x*x.
intros. ring_simplify. reflexivity.
Qed.
End TestRing.
(** We benefit also from an "order" tactic *)
Ltac bigN_order := BigN.order.
Section TestOrder.
Let test : forall x y : bigN, x<=y -> y<=x -> x==y.
Proof. bigN_order. Qed.
End TestOrder.
(** We can use at least a bit of (r)omega by translating to [Z]. *)
Section TestOmega.
Let test : forall x y : bigN, x<=y -> y<=x -> x==y.
Proof. intros x y. BigN.zify. omega. Qed.
End TestOmega.
(** Todo: micromega *)
(************************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
(* Benjamin Gregoire, Laurent Thery, INRIA, 2007 *)
(************************************************************************)
(** * NMake *)
(** From a cyclic Z/nZ representation to arbitrary precision natural numbers.*)
(** NB: This file contain the part which is independent from the underlying
representation. The representation-dependent (and macro-generated) part
is now in [NMake_gen]. *)
Require Import Bool BigNumPrelude ZArith Nnat Ndigits CyclicAxioms DoubleType
Nbasic Wf_nat StreamMemo NSig NMake_gen.
Module Make (W0:CyclicType) <: NType.
(** Let's include the macro-generated part. Even if we can't functorize
things (due to Eval red_t below), the rest of the module only uses
elements mentionned in interface [NAbstract]. *)
Include NMake_gen.Make W0.
Open Scope Z_scope.
Local Notation "[ x ]" := (to_Z x).
Definition eq (x y : t) := [x] = [y].
Declare Reduction red_t :=
lazy beta iota delta
[iter_t reduce same_level mk_t mk_t_S succ_t dom_t dom_op].
Ltac red_t :=
match goal with |- ?u => let v := (eval red_t in u) in change v end.
(** * Generic results *)
Tactic Notation "destr_t" constr(x) "as" simple_intropattern(pat) :=
destruct (destr_t x) as pat; cbv zeta;
rewrite ?iter_mk_t, ?spec_mk_t, ?spec_reduce.
Lemma spec_same_level : forall A (P:Z->Z->A->Prop)
(f : forall n, dom_t n -> dom_t n -> A),
(forall n x y, P (ZnZ.to_Z x) (ZnZ.to_Z y) (f n x y)) ->
forall x y, P [x] [y] (same_level f x y).
Proof.
intros. apply spec_same_level_dep with (P:=fun _ => P); auto.
Qed.
Theorem spec_pos: forall x, 0 <= [x].
Proof.
intros x. destr_t x as (n,x). now case (ZnZ.spec_to_Z x).
Qed.
Lemma digits_dom_op_incr : forall n m, (n<=m)%nat ->
(ZnZ.digits (dom_op n) <= ZnZ.digits (dom_op m))%positive.
Proof.
intros.
change (Zpos (ZnZ.digits (dom_op n)) <= Zpos (ZnZ.digits (dom_op m))).
rewrite !digits_dom_op, !Pshiftl_nat_Zpower.
apply Z.mul_le_mono_nonneg_l; auto with zarith.
apply Z.pow_le_mono_r; auto with zarith.
Qed.
Definition to_N (x : t) := Z.to_N (to_Z x).
(** * Zero, One *)
Definition zero := mk_t O ZnZ.zero.
Definition one := mk_t O ZnZ.one.
Theorem spec_0: [zero] = 0.
Proof.
unfold zero. rewrite spec_mk_t. exact ZnZ.spec_0.
Qed.
Theorem spec_1: [one] = 1.
Proof.
unfold one. rewrite spec_mk_t. exact ZnZ.spec_1.
Qed.
(** * Successor *)
(** NB: it is crucial here and for the rest of this file to preserve
the let-in's. They allow to pre-compute once and for all the
field access to Z/nZ initial structures (when n=0..6). *)
Local Notation succn := (fun n =>
let op := dom_op n in
let succ_c := ZnZ.succ_c in
let one := ZnZ.one in
fun x => match succ_c x with
| C0 r => mk_t n r
| C1 r => mk_t_S n (WW one r)
end).
Definition succ : t -> t := Eval red_t in iter_t succn.
Lemma succ_fold : succ = iter_t succn.
Proof. red_t; reflexivity. Qed.
Theorem spec_succ: forall n, [succ n] = [n] + 1.
Proof.
intros x. rewrite succ_fold. destr_t x as (n,x).
generalize (ZnZ.spec_succ_c x); case ZnZ.succ_c.
intros. rewrite spec_mk_t. assumption.
intros. unfold interp_carry in *.
rewrite spec_mk_t_S. simpl. rewrite ZnZ.spec_1. assumption.
Qed.
(** Two *)
(** Not really pretty, but since W0 might be Z/2Z, we're not sure
there's a proper 2 there. *)
Definition two := succ one.
Lemma spec_2 : [two] = 2.
Proof.
unfold two. now rewrite spec_succ, spec_1.
Qed.
(** * Addition *)
Local Notation addn := (fun n =>
let op := dom_op n in
let add_c := ZnZ.add_c in
let one := ZnZ.one in
fun x y =>match add_c x y with
| C0 r => mk_t n r
| C1 r => mk_t_S n (WW one r)
end).
Definition add : t -> t -> t := Eval red_t in same_level addn.
Lemma add_fold : add = same_level addn.
Proof. red_t; reflexivity. Qed.
Theorem spec_add: forall x y, [add x y] = [x] + [y].
Proof.
intros x y. rewrite add_fold. apply spec_same_level; clear x y.
intros n x y. cbv beta iota zeta.
generalize (ZnZ.spec_add_c x y); case ZnZ.add_c; intros z H.
rewrite spec_mk_t. assumption.
rewrite spec_mk_t_S. unfold interp_carry in H.
simpl. rewrite ZnZ.spec_1. assumption.
Qed.
(** * Predecessor *)
Local Notation predn := (fun n =>
let pred_c := ZnZ.pred_c in
fun x => match pred_c x with
| C0 r => reduce n r
| C1 _ => zero
end).
Definition pred : t -> t := Eval red_t in iter_t predn.
Lemma pred_fold : pred = iter_t predn.
Proof. red_t; reflexivity. Qed.
Theorem spec_pred_pos : forall x, 0 < [x] -> [pred x] = [x] - 1.
Proof.
intros x. rewrite pred_fold. destr_t x as (n,x). intros H.
generalize (ZnZ.spec_pred_c x); case ZnZ.pred_c; intros y H'.
rewrite spec_reduce. assumption.
exfalso. unfold interp_carry in *.
generalize (ZnZ.spec_to_Z x) (ZnZ.spec_to_Z y); auto with zarith.
Qed.
Theorem spec_pred0 : forall x, [x] = 0 -> [pred x] = 0.
Proof.
intros x. rewrite pred_fold. destr_t x as (n,x). intros H.
generalize (ZnZ.spec_pred_c x); case ZnZ.pred_c; intros y H'.
rewrite spec_reduce.
unfold interp_carry in H'.
generalize (ZnZ.spec_to_Z y); auto with zarith.
exact spec_0.
Qed.
Lemma spec_pred x : [pred x] = Z.max 0 ([x]-1).
Proof.
rewrite Z.max_comm.
destruct (Z.max_spec ([x]-1) 0) as [(H,->)|(H,->)].
- apply spec_pred0; generalize (spec_pos x); auto with zarith.
- apply spec_pred_pos; auto with zarith.
Qed.
(** * Subtraction *)
Local Notation subn := (fun n =>
let sub_c := ZnZ.sub_c in
fun x y => match sub_c x y with
| C0 r => reduce n r
| C1 r => zero
end).
Definition sub : t -> t -> t := Eval red_t in same_level subn.
Lemma sub_fold : sub = same_level subn.
Proof. red_t; reflexivity. Qed.
Theorem spec_sub_pos : forall x y, [y] <= [x] -> [sub x y] = [x] - [y].
Proof.
intros x y. rewrite sub_fold. apply spec_same_level. clear x y.
intros n x y. simpl.
generalize (ZnZ.spec_sub_c x y); case ZnZ.sub_c; intros z H LE.
rewrite spec_reduce. assumption.
unfold interp_carry in H.
exfalso.
generalize (ZnZ.spec_to_Z z); auto with zarith.
Qed.
Theorem spec_sub0 : forall x y, [x] < [y] -> [sub x y] = 0.
Proof.
intros x y. rewrite sub_fold. apply spec_same_level. clear x y.
intros n x y. simpl.
generalize (ZnZ.spec_sub_c x y); case ZnZ.sub_c; intros z H LE.
rewrite spec_reduce.
unfold interp_carry in H.
generalize (ZnZ.spec_to_Z z); auto with zarith.
exact spec_0.
Qed.
Lemma spec_sub : forall x y, [sub x y] = Z.max 0 ([x]-[y]).
Proof.
intros. destruct (Z.le_gt_cases [y] [x]).
rewrite Z.max_r; auto with zarith. apply spec_sub_pos; auto.
rewrite Z.max_l; auto with zarith. apply spec_sub0; auto.
Qed.
(** * Comparison *)
Definition comparen_m n :
forall m, word (dom_t n) (S m) -> dom_t n -> comparison :=
let op := dom_op n in
let zero := ZnZ.zero (Ops:=op) in
let compare := ZnZ.compare (Ops:=op) in
let compare0 := compare zero in
fun m => compare_mn_1 (dom_t n) (dom_t n) zero compare compare0 compare (S m).
Let spec_comparen_m:
forall n m (x : word (dom_t n) (S m)) (y : dom_t n),
comparen_m n m x y = Z.compare (eval n (S m) x) (ZnZ.to_Z y).
Proof.
intros n m x y.
unfold comparen_m, eval.
rewrite nmake_double.
apply spec_compare_mn_1.
exact ZnZ.spec_0.
intros. apply ZnZ.spec_compare.
exact ZnZ.spec_to_Z.
exact ZnZ.spec_compare.
exact ZnZ.spec_compare.
exact ZnZ.spec_to_Z.
Qed.
Definition comparenm n m wx wy :=
let mn := Max.max n m in
let d := diff n m in
let op := make_op mn in
ZnZ.compare
(castm (diff_r n m) (extend_tr wx (snd d)))
(castm (diff_l n m) (extend_tr wy (fst d))).
Local Notation compare_folded :=
(iter_sym _
(fun n => ZnZ.compare (Ops:=dom_op n))
comparen_m
comparenm
CompOpp).
Definition compare : t -> t -> comparison :=
Eval lazy beta iota delta [iter_sym dom_op dom_t comparen_m] in
compare_folded.
Lemma compare_fold : compare = compare_folded.
Proof.
lazy beta iota delta [iter_sym dom_op dom_t comparen_m]. reflexivity.
Qed.
Theorem spec_compare : forall x y,