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

small upadates

parent f207bdce
......@@ -5,7 +5,6 @@ Require Export TrippleRel.
Open Scope Z.
(*Eval simpl in (ZofList_Bound 16 16 (2 ^ 62) < 1 * 2^303).*)
SearchAbout Z.modulo.
Theorem Zcar25519_bounds:
forall l1 l2 l3,
......@@ -24,7 +23,7 @@ Proof.
apply (ZofList_bounds 16 l1 16 (-2^62) (2^62)) in Hbounds.
split ;
[apply bounds_car_inf| apply bounds_car_sup];
try assumption ; rewrite Hcarr2 ;
try assumption ; rewrite Hcarr2;
rewrite <- car25519_eq_car25519 by assumption;
eapply (doubleCar_ext_str (16.lst l1) _ 303) ;
try omega ; try (eapply le_lt_trans ; [eapply Hbounds| | ] ; compute ; reflexivity);
......
......@@ -313,7 +313,8 @@ Proof.
| _ => progress autorewrite with listdb
end.
f_equal; ring.
rewrite! Ht.
}
(* rewrite! Ht.
rewrite! ZscalarMultnil.
rewrite ZsumList_nil_r.
rewrite Ht.
......@@ -321,7 +322,7 @@ Proof.
rewrite ZofList_nil.
f_equal.
ring.
}
}*)
{
assert(Hlength: length (slice 16 (l 38 tail 16 l)) = 16%nat).
rewrite slice_length_min.
......
......@@ -77,7 +77,7 @@ Proof.
assert(Hs: 38 * (x / 2 ^ 256) + x mod 2 ^ 256 < 38 * (x / 2 ^ 256) + 2 ^ 256).
apply Zplus_lt_compat_l.
apply Z_mod_lt.
compute ; reflexivity.
reflexivity.
assert(38 * (x / 2 ^ 256) + 2 ^ 256 < 2 ^ 256).
clear Hs.
apply (Z.le_lt_add_lt (-2^256) (-2^256)).
......@@ -219,22 +219,44 @@ Proof.
end.
Qed.
Fact lower_eq_256: forall a,
2 ^ 256 <= a ->
a < 2 ^ 257 ->
1 <= a / 2 ^ 256.
Proof.
intros.
rewrite <- (Z_div_same_full (2^256)).
apply Z_div_le ; go.
intro; false.
Qed.
Fact upper_eq_256: forall a,
2 ^ 256 <= a ->
a < 2 ^ 257 ->
a / 2 ^ 256 < 2.
Proof.
intros ; apply Z.div_lt_upper_bound ; go.
Qed.
Fact eq1 : forall a, a = 1 <-> a < 2 /\ 1 <= a.
Proof. intros. omega. Qed.
Fact eq_1_div256: forall a,
2 ^ 256 <= a ->
a < 2 ^ 257 ->
a / 2 ^ 256 = 1.
Proof.
intros a Hamin Hamax.
assert(1 <= a / 2 ^ 256).
rewrite <- (Z_div_same_full (2^256)).
apply Z_div_le ; go.
intro ; false.
assert(a / 2 ^ 256 < 2).
apply Z.div_lt_upper_bound ; go.
omega.
repeat match goal with
| _ => progress intros
| _ => assumption
| [ |- _ < 2 ] => apply upper_eq_256
| [ |- 1 <= _ ] => apply lower_eq_256
| [ |- _ /\ _ ] => progress split
| _ => progress apply eq1
end.
Qed.
Eval compute in (Z.pow 2 256).
(* in the previous proof the order of the tactics matter !
if apply eq1 is before split : infinite loop *)
Lemma getCarryNeg:
forall x,
......@@ -261,24 +283,9 @@ Lemma sndCar_neg_str:
Proof.
intros x Hx.
unfold Zcar25519.
assert(Hcarry: getCarry 256 x = -1).
{
unfold getCarry.
rewrite Z.shiftr_div_pow2 by omega.
pose(r := x + 2 ^ 256).
symmetry.
eapply (Z.div_unique_pos x (2^256) (-1) r).
- subst r.
assert(2^256 - 2 ^ 250 < x + 2 ^ 256).
omega.
simpl in * ; omega.
- subst r.
omega.
}
rewrite Hcarry.
rewrite (getCarryNeg x Hx).
rewrite getResidue_mod_eq by omega.
unfold getResidue_mod.
clear Hcarry.
rewrite <- (Z_mod_plus_full x 1 (2^256)).
replace ((x + 1 * 2 ^ 256) mod 2 ^ 256) with (x + 1 * 2 ^ 256).
replace (38 * -1 + (x + 1 * 2 ^ 256)) with (2 ^ 256 - 38 + x).
......@@ -287,7 +294,6 @@ Proof.
simpl (2 ^ 256 - 38 - 2 ^ 250 ) in H.
omega.
omega.
omega.
symmetry.
apply Zmod_small.
......
Require Import Clightdefs.
Local Open Scope Z_scope.
Definition _A : ident := 115%positive.
......
Require Import floyd.proofauto. (* Import the Verifiable C system *)
Require Import tweetnacl. (* Import the AST of this C program *)
(* The next line is "boilerplate", always required after importing an AST. *)
Instance CompSpecs : compspecs. make_compspecs prog. Defined.
Definition Vprog : varspecs. mk_varspecs prog. Defined.
Require Import SumList.
Require Import ToFF.
Open Scope Z.
Lemma SumListForall : forall n a b c,
n > 0 ->
Forall (fun x : Z => 0 <= x < 2 ^ n) a ->
Forall (fun x : Z => 0 <= x < 2 ^ n) b ->
sum_list_Z a b = c ->
Forall (fun x : Z => 0 <= x < 2 ^ (Z.succ n)) c.
Proof.
induction n ; [intros | | intros; assert(Hp:=Zlt_neg_0)] ; go.
assert(Hp: exists n, n = Z.pos p) by (exists (Z.pos p); reflexivity); destruct Hp as [n Hp].
rewrite <- Hp in *.
assert(Hfa: forall a, 0 <= a < 2^n -> 0 <= a < 2^Z.succ n).
intros x Hx ; split ; destruct Hx ; auto ; rewrite Z.pow_succ_r ; assert(Hpp:= Zgt_pos_0 p) ; rewrite <- Hp in Hpp ; omega.
induction a,b ; intros c Hn Ha Hb Hsum ; simpl in Hsum ; subst c ; auto.
- eapply (Forall_impl (fun x : Z => 0 <= x < 2 ^ Z.succ n) Hfa) ; auto.
- eapply (Forall_impl (fun x : Z => 0 <= x < 2 ^ Z.succ n) Hfa) ; auto.
apply Forall_cons.
{
inv Ha.
inv Hb.
destruct H1.
destruct H3.
split ; try omega.
apply addition ; try omega.
}
{
apply (IHa b); auto.
inv Ha ; auto.
inv Hb ; auto.
}
Qed.
(* Beginning of the API spec for the sumarray.c program *)
Definition A_spec :=
DECLARE _A
WITH i: val, o: val, a: val, b: val, aux1: val, aux2: val, sh : share, contents_o : list Z, contents_a : list Z, contents_b : list Z
PRE [ _o OF (tptr tlong), _a OF (tptr tlong), _b OF (tptr tlong) ]
PROP (writable_share sh;
Forall (fun x => 0 <= x < Z.pow 2 63) contents_a;
Forall (fun x => 0 <= x < Z.pow 2 63) contents_b;
length contents_a = 16%nat;
length contents_b = 16%nat;
length contents_o = 16%nat)
LOCAL (temp _i i; temp _aux1 aux1; temp _aux2 aux2)
SEP (data_at sh (tarray tlong 16) (map Vlong (map Int64.repr contents_a)) a;
data_at sh (tarray tlong 16) (map Vlong (map Int64.repr contents_b)) b;
data_at sh (tarray tlong 16) (map Vlong (map Int64.repr contents_o)) o)
POST [ tvoid ]
PROP (writable_share sh)
LOCAL()
SEP (data_at sh (tarray tlong 16) (map Vlong (map Int64.repr contents_a)) a;
data_at sh (tarray tlong 16) (map Vlong (map Int64.repr contents_b)) b;
data_at sh (tarray tlong 16) (map Vlong (map Int64.repr (sum_list_Z contents_a contents_b))) o).
(* Note: It would also be reasonable to let [contents] have type [list int].
Then the [Forall] would not be needed in the PROP part of PRE.
*)
Check temp.
Definition A_Inv sh o a b contents_o contents_a contents_b aux1 aux2:=
EX i : Z,
PROP (writable_share sh;
Forall (fun x => 0 <= x < Z.pow 2 63) contents_a;
Forall (fun x => 0 <= x < Z.pow 2 63) contents_b;
length contents_a = 16%nat;
length contents_b = 16%nat;
length contents_o = 16%nat;
i >= 0;
sum_list_Z_n (nat_of_Z i) contents_a contents_b = slice (nat_of_Z i) contents_o)
LOCAL (temp _aux1 aux1; temp _aux2 aux2)
SEP (data_at sh (tarray tlong 16) (map Vlong (map Int64.repr (sum_list_Z_n (nat_of_Z i) contents_a contents_b ++ tail (nat_of_Z i) contents_o))) o;
data_at sh (tarray tlong 16) (map Vlong (map Int64.repr contents_a)) a;
data_at sh (tarray tlong 16) (map Vlong (map Int64.repr contents_b)) b).
(* Packaging the API spec all together. *)
Definition Gprog : funspecs :=
augment_funspecs prog [A_spec].
(** Proof that f_sumarray, the body of the sumarray() function,
** satisfies sumarray_spec, in the global context (Vprog,Gprog).
**)
Lemma body_sumarray: semax_body Vprog Gprog f_A A_spec.
Proof.
start_function.
forward_for_simple_bound 16 (A_Inv sh o a b contents_o contents_a contents_b aux1 aux2).
- go_lowerx.
entailer!.
flatten.
flatten ; entailer!.
- go_lowerx.
normalize.
entailer!.
unfold tc_expr.
unfold "`" in *.
simpl in *.
entailer!.
- normalize.
forward. (* ??? *)
- normalize.
rewrite <- sum_list_eq in H5 ; go.
rewrite slice_length_eq in H5 ; go.
rewrite tail_length_eq ; go.
rewrite app_nill_r.
change (nat_of_Z 16) with (16%nat) in *.
rewrite <- sum_list_eq ; go.
assert(HSum:= SumListForall 63 contents_a contents_b (sum_list_Z contents_a contents_b)).
assert(HSum': 63 > 0) by omega.
apply HSum in HSum' ; go.
normalize.
rewrite H5 in HSum'.
entailer!.
forward.
Admitted.
Require Import floyd.proofauto. (* Import the Verifiable C system *)
Require Import tweetnacl. (* Import the AST of this C program *)
(* The next line is "boilerplate", always required after importing an AST. *)
Instance CompSpecs : compspecs. make_compspecs prog. Defined.
Definition Vprog : varspecs. mk_varspecs prog. Defined.
Require Import M.
Definition M_spec :=
DECLARE _M
WITH i: val, o: val, a: val, b: val, aux1: val, aux2: val, sh : share, contents_o : list Z, contents_a : list Z, contents_b : list Z
PRE [ _o OF (tptr tlong), _a OF (tptr tlong), _b OF (tptr tlong) ]
PROP (readable_share sh;
Forall (fun x => 0 <= x < Z.pow 2 63) contents_a;
Forall (fun x => 0 <= x < Z.pow 2 63) contents_b;
length contents_a = 16%nat;
length contents_b = 16%nat;
length contents_o = 16%nat)
LOCAL (temp _i i; temp _aux1 aux1; temp _aux2 aux2)
SEP (data_at sh (tarray tlong 16) (map Vlong (map Int64.repr contents_a)) a;
data_at sh (tarray tlong 16) (map Vlong (map Int64.repr contents_b)) b;
data_at sh (tarray tlong 16) (map Vlong (map Int64.repr contents_o)) o)
POST [ tvoid ]
PROP (readable_share sh;
Forall (fun x => 0 <= x < Z.pow 2 (Z.succ 63)) contents_o)
LOCAL()
SEP (data_at sh (tarray tlong 16) (map Vlong (map Int64.repr contents_a)) a;
data_at sh (tarray tlong 16) (map Vlong (map Int64.repr contents_b)) b;
data_at sh (tarray tlong 16) (map Vlong (map Int64.repr (sum_list_Z contents_a contents_b))) o).
(* Packaging the API spec all together. *)
Definition Gprog : funspecs :=
augment_funspecs prog [M_spec].
(** Proof that f_sumarray, the body of the sumarray() function,
** satisfies sumarray_spec, in the global context (Vprog,Gprog).
**)
Lemma body_sumarray: semax_body Vprog Gprog f_M M_spec.
Proof.
start_function.
forward_for_simple_bound 16 (A_Inv sh o a b contents_o contents_a contents_b aux1 aux2).
- go_lowerx.
entailer!.
flatten.
flatten ; entailer!.
- go_lowerx.
normalize.
entailer!.
admit.
- admit.
- normalize.
rewrite <- sum_list_eq in H5 ; go.
rewrite slice_length_eq in H5 ; go.
rewrite tail_length_eq ; go.
rewrite app_nill_r.
change (nat_of_Z 16) with (16%nat) in *.
rewrite <- sum_list_eq ; go.
assert(HSum:= SumListForall 63 contents_a contents_b (sum_list_Z contents_a contents_b)).
assert(HSum': 63 > 0) by omega.
apply HSum in HSum' ; go.
normalize.
rewrite H5 in HSum'.
Qed.
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