Commit 8b122c77 authored by Benoit Viguier's avatar Benoit Viguier
Browse files

even less change

parent 60fe8dfa
......@@ -279,7 +279,7 @@ sv car25519(gf o)
}
}
sv sel25519(gf p,gf q,i64 b)
sv sel25519(gf p,gf q,int b)
{
int i;
i64 t,c=~(b-1);
......@@ -292,8 +292,7 @@ sv sel25519(gf p,gf q,i64 b)
sv pack25519(u8 *o,const gf n)
{
int i,j;
i64 b;
int i,j,b;
gf t,m={0};
set25519(t,n);
car25519(t);
......@@ -395,8 +394,7 @@ sv pow2523(gf o,const gf i)
int crypto_scalarmult(u8 *q,const u8 *n,const u8 *p)
{
u8 z[32];
i64 r;
int i;
int r,i;
gf x,a,b,c,d,e,f;
FOR(i,31) z[i]=n[i];
z[31]=(n[31]&127)|64;
......
......@@ -389,17 +389,16 @@ forward.
entailer!.
rewrite HintluTrue ; simpl; trivial.
replace (force_val
(sem_cast tint tlg
(eval_binop Oand tint tint
(eval_binop Oshr tuchar tint (Vint (Int.repr (Znth (i / two_p 3) z 0)))
(eval_binop Oand tint tint (Vint (Int.repr i)) (Vint (Int.repr 7))))
(Vint (Int.repr 1))))) with
(Vlong (Int64.repr (Low.getbit i z))).
(sem_binary_operation' Oand tint tint
(eval_binop Oshr tuchar tint (Vint (Int.repr (Znth (i / two_p 3) z 0)))
(eval_binop Oand tint tint (Vint (Int.repr i)) (Vint (Int.repr 7))))
(Vint (Int.repr 1)))) with
(Vint (Int.repr (Low.getbit i z))).
2:{
clean_context_from_VST. clears v_a v_b v_c v_d v_e v_f.
simpl.
rewrite and_repr /tuchar /tint /sem_shift ; simpl.
rewrite and_repr /tuchar /sem_shift ; simpl.
rewrite HintluTrue ; simpl.
rewrite Int.shr_div_two_p.
rewrite Int.unsigned_repr.
......@@ -407,32 +406,8 @@ replace (force_val
rewrite Int.signed_repr.
2: solve_bounds_by_values_Znth.
rewrite and_repr.
assert(H0landdiv8: 0 <= Z.land (Znth (i / two_p 3) z 0 / two_p (Z.land i 7)) 1).
{
apply Z.land_nonneg ; right ; omega.
}
assert(Hlanddiv81: Z.land (Znth (i / two_p 3) z 0 / two_p (Z.land i 7)) 1 <= 1).
{
apply Z.log2_null.
assert(Hlanddiv8min: Z.log2 (Z.land (Znth (i / two_p 3) z 0 / two_p (Z.land i 7)) 1) <=
Z.min (Z.log2 (Znth (i / two_p 3) z 0 / two_p (Z.land i 7))) (Z.log2 1)).
apply Z.log2_land.
solve_bounds_by_values_Znth.
apply Z_div_pos.
apply two_p_gt_ZERO.
apply Z.land_nonneg; right; omega.
omega.
omega.
replace (Z.min (Z.log2 (Znth (i / two_p 3) z 0 / two_p (Z.land i 7))) (Z.log2 1)) with 0 in Hlanddiv8min.
assert(Htemp := Z.log2_nonneg (Z.land (Znth (i / two_p 3) z 0 / two_p (Z.land i 7)) 1)).
omega.
simpl.
rewrite Z.min_r.
omega.
apply Z.log2_nonneg.
}
rewrite Int.signed_repr.
2: solve_bounds_by_values.
assert(0 <= Z.land (Znth (i / two_p 3) z 0 / two_p (Z.land i 7)) 1 <= 1).
apply and_0_or_1.
rewrite /Low.getbit ?Z.shiftr_div_pow2 ?Znth_nth /nat_of_Z ?Z2Nat.id ?two_p_correct; try omega.
reflexivity.
apply Z_div_pos.
......
......@@ -382,6 +382,36 @@ eexists ; reflexivity.
rewrite Zlength_map.
rewrite upd_Znth_Zlength ; omega.
forward.
rewrite (Znth_map Int64.zero).
simpl eval_binop.
rewrite (Znth_map 0).
rewrite Int.signed_repr.
rewrite Int.unsigned_repr.
rewrite Int64.shr_div_two_p.
rewrite Int64.unsigned_repr.
rewrite Int64.signed_repr.
rewrite and64_repr.
simpl.
3: solve_bounds_by_values.
3: solve_bounds_by_values.
3: solve_bounds_by_values.
2: {
rewrite upd_Znth_same ; try omega.
assert(0 <= Z.land (Znth 14 m''' 0 / two_power_pos 16) 1 <= 1).
apply and_0_or_1.
assert(0 <= Znth 15 t' 0 < 2^16).
apply Forall_Znth; try omega ; apply Hboundt'.
solve_bounds_by_values.
}
2: rewrite upd_Znth_Zlength ; omega.
2: rewrite Zlength_map upd_Znth_Zlength ; omega.
rewrite Int64.unsigned_repr.
2: assert(0 <= Z.land
(Znth 15 (upd_Znth 15 m''' (Znth 15 t' 0 - 32767 - Z.land (Znth 14 m''' 0 / two_power_pos 16) 1)) 0 /
two_power_pos 16) 1 <= 1).
2: apply and_0_or_1.
2: solve_bounds_by_values.
change (two_power_pos 16) with (two_p 16).
forward ; rewrite -Hmi3.
entailer!.
rewrite (Znth_map Int64.zero) in Hmi3.
......@@ -399,81 +429,26 @@ rewrite ?Int.signed_repr.
subst mi1.
rewrite and64_repr.
rewrite ?upd_Znth_map.
rewrite (Znth_map Int64.zero).
2: rewrite Zlength_map upd_Znth_Zlength ; omega.
rewrite (Znth_map 0).
2: rewrite upd_Znth_Zlength ; omega.
remember (upd_Znth 14 (upd_Znth 15 m''' (Znth 15 t' 0 - 32767 - Z.land (Znth 14 m''' 0 / two_p 16) 1))
(Z.land (Znth 14 m''' 0) 65535)) as msub.
assert(Hmi2 : exists mi2, Vlong mi2 = Znth 15 (mVI64 msub) Vundef).
{
subst msub.
rewrite (Znth_map Int64.zero).
eexists ; reflexivity.
rewrite Zlength_map.
rewrite upd_Znth_Zlength upd_Znth_Zlength ; omega.
}
destruct Hmi2 as [mi2 Hmi2].
assert(Zlength msub = 16).
{
subst msub.
rewrite ?upd_Znth_Zlength ; omega.
}
rewrite (Znth_map Int64.zero) in Hmi2.
2: rewrite Zlength_map ; omega.
rewrite (Znth_map 0) in Hmi2.
2: omega.
replace (Vlong
(Int64.repr
(Znth 15 (upd_Znth 15 m''' (Znth 15 t' 0 - 32767 - Z.land (Znth 14 m''' 0 / two_p 16) 1)) 0))) with (Vlong mi2).
2:{
rewrite Hmi2.
subst msub.
f_equal.
f_equal.
rewrite upd_Znth_diff ?upd_Znth_Zlength => // ; omega.
}
rewrite /sem_binary_operation' /sem_and.
simpl.
rewrite Hmi2.
assert (Hmi2_simpl: mi2 = (Int64.repr (Znth 15 msub 0))).
inv Hmi2 => //.
remember (Z.land
(Znth 15 (upd_Znth 15 m''' (Znth 15 t' 0 - 32767 - Z.land (Znth 14 m''' 0 / two_p 16) 1)) 0 /
two_p 16) 1) as t'''''.
assert(0 <= t''''' <= 1) by (subst ; apply and_0_or_1).
forward.
rewrite Hmi2_simpl.
assert(Htmp:= verif_pack25519_10 (Znth 15 msub 0)).
entailer!.
simpl cast_int_long.
rewrite Hmi2_simpl.
rewrite ?Int.signed_repr.
2: solve_bounds_by_values.
rewrite ?Int.unsigned_repr.
2: solve_bounds_by_values.
rewrite Int64.shr_div_two_p.
rewrite ?Int64.unsigned_repr.
2: solve_bounds_by_values.
rewrite ?Int64.signed_repr.
rewrite sub_repr.
subst t'''''.
replace (Znth 15 (upd_Znth 15 m''' (Znth 15 t' 0 - 32767 - Z.land (Znth 14 m''' 0 / two_p 16) 1)) 0) with (Znth 15 msub 0).
2: {
subst msub.
rewrite upd_Znth_diff ?upd_Znth_Zlength ; try omega.
rewrite upd_Znth_same ; try omega.
assert(0 <= Z.land (Znth 14 m''' 0 / two_p 16) 1 <= 1).
apply and_0_or_1.
assert(HZland: Z.land (Znth 14 m''' 0 / two_p 16) 1 = 0 \/
Z.land (Znth 14 m''' 0 / two_p 16) 1 = 1) by omega.
destruct HZland as [HZland | HZland]; rewrite HZland.
1,2: assert(Int64.min_signed + 32767 <= Znth 15 t' 0 <= Int64.max_signed + 32767).
1,3: apply Forall_Znth ; [omega|]; eapply list.Forall_impl ; [apply Hboundt' |];
intros x Hx ; simpl in Hx ; solve_bounds_by_values.
1,2: repeat rewrite Int64.signed_repr.
split; solve_bounds_by_values.
apply Forall_Znth ; [omega|]; eapply list.Forall_impl ; [apply Hboundt' |];
intros x Hx ; simpl in Hx ; solve_bounds_by_values.
rewrite upd_Znth_diff => //=.
all: rewrite upd_Znth_Zlength Hlengthm''' => //=.
}
rewrite and64_repr.
rewrite sub64_repr.
remember (1 - Z.land (Znth 15 msub 0 / two_p 16) 1) as b'.
deadvars!.
forward_call (v_t, v_m, Tsh, t', msub, b').
......
......@@ -64,30 +64,6 @@ repeat match goal with
end.
Qed.
(*
Lemma verif_pack25519_3:
forall F,
OracleKind ->
forall (v_o v_n : val) (tsh : share) (contents_o : list val) (n : list ) (v_t v_m : val),
writable_share tsh ->
Zlength n = 16 ->
writable_share Tsh ->
forall t : list ,
Zlength t = 16 ->
ENTAIL initialized_list [] (func_tycontext f_pack25519 Vprog Gprog []),
PROP ( )
LOCAL (lvar _m lg16 v_m; lvar _t lg16 v_t; temp _o v_o)
SEP (FRZL F ; Tsh [{v_t}]<<( lg16 )-- mVI64 t;
Tsh [{v_m}]<<( lg16 )-- mVI64 nil16)
|-- PROP (writable_share Tsh; Zlength nil16 = 16; Zlength t = 16; 0 >= 0)
LOCAL (lvar _m lg16 v_m; lvar _t lg16 v_t; temp _o v_o)
SEP (FRZL F;
Tsh [{v_t}]<<( lg16 )-- mVI64 (get_t (nil16, t)); Tsh [{v_m}]<<( lg16 )-- mVI64 (get_m (nil16, t))).
Proof.
intros.
entailer.
Qed.
*)
Lemma verif_pack25519_4:
forall t',
Zlength t' = 16 ->
......@@ -128,7 +104,7 @@ all: rewrite ?Int64.signed_repr.
all: solve_bounds_by_values.
Qed.
Lemma verif_pack25519_6:
(* Lemma verif_pack25519_6:
forall t' : list ,
forall m' : list ,
Zlength t' = 16 ->
......@@ -165,9 +141,9 @@ apply sub_fn_rev_f_bound_nth ; try assumption.
omega.
match goal with | [ |- _ <= ?a <= _ ] => remember a as blabla end.
solve_bounds_by_values.
Qed.
Qed. *)
Lemma verif_pack25519_7:
(* Lemma verif_pack25519_7:
forall t' : list ,
forall m'' : list ,
Zlength m'' = 16 ->
......@@ -191,7 +167,7 @@ rewrite /sub_step /subst_0xffffc.
rewrite Reduce.Zshiftr_div_pow2_16.
change (two_p 16) with (2^16).
reflexivity.
Qed.
Qed. *)
Lemma verif_pack25519_8:
forall t' : list ,
......@@ -219,60 +195,7 @@ intros x Hx ; simpl in Hx ; solve_bounds_by_values].
all: solve_bounds_by_values.
Qed.
(* Lemma verif_pack25519_9:
forall j : ,
0 <= j < 2 ->
forall t' : list ,
forall m' : list ,
Zlength t' = 16 ->
Forall (fun x : => 0 <= x < 2 ^ 16) t' ->
Zlength m' = 16 ->
forall m'' : list ,
m'' = upd_Znth 0 m' (Znth 0 t' 0 - 65517) ->
forall m''' : list ,
m''' = sub_fn_rev 1 sub_step 15 m'' t' ->
Zlength m''' = 16
-> Int64.min_signed <= Znth 14 m''' 0 <= Int64.max_signed.
Proof.
intros.
repeat match goal with
| [ H: context[Znth] |- _ ]=> rewrite Znth_nth in H
| [ |- context[Znth] ]=> rewrite Znth_nth
| _ => omega
end.
match goal with | [ |- context[nth ?a ?b ?c]] => replace (nth a b c) with (nth a b 0) end.
match goal with | [ H: context[nth ?a ?b ?c] |- _ ] => replace (nth a b c) with (nth a b 0) in H end.
2,3: apply nth_indep.
2,3: match goal with | [ |- (_ < ?A)%nat ] => rewrite -(Nat2Z.id A) end.
2,3: rewrite /nat_of_Z ; apply Z2Nat.inj_lt ; rewrite -?Zlength_correct ; omega.
subst m''' m''.
rewrite ?Znth_nth ?upd_Znth_upd_nth ; try omega.
assert(Hbt: - 2 ^ 16 <= nth (Z.to_nat (15 - 1)) (sub_fn_rev 1 sub_step 15 (upd_nth 0 m' (subst_0xffed (nth 0 t' 0))) t') 0 <
2 ^ 16).
apply sub_fn_rev_f_bound_nth ; try assumption ; omega.
move: Hbt.
Grind_add_Z ; rewrite /nat_of_Z /subst_0xffed; repeat change_Z_to_nat.
intros Hbt.
match goal with | [ |- _ <= ?a <= _ ] => remember a as blabla end.
solve_bounds_by_values.
Qed. *)
Lemma verif_pack25519_10:
forall msub15,
Int64.min_signed <=
1 - Int64.signed (Int64.and (Int64.shr (Int64.repr msub15) (Int64.repr 16)) (Int64.repr 1)) <= Int64.max_signed.
Proof.
intros.
rewrite and64_repr.
remember (Z.shiftr (Int64.signed (Int64.repr msub15)) (Int64.unsigned (Int64.repr 16))) as mi2.
assert(0 <= Z.land mi2 1 <= 1).
apply and_0_or_1.
assert(HZland: Z.land mi2 1 = 0 \/ Z.land mi2 1 = 1) by omega.
destruct HZland as [HZland | HZland]; rewrite HZland.
1,2: rewrite Int64.signed_repr ; solve_bounds_by_values.
Qed.
Lemma verif_pack25519_11:
(* Lemma verif_pack25519_11:
forall t' : list ,
Zlength t' = 16 ->
Forall (fun x : => 0 <= x < 2 ^ 16) t' ->
......@@ -304,7 +227,7 @@ reflexivity.
all: destruct HZland as [HZland | HZland]; rewrite ?HZland.
all: solve_bounds_by_values.
Qed.
*)
(* Lemma verif_pack25519_12:
forall t : list ,
Forall (fun x : => 0 <= x < 2 ^ 16) t ->
......
......@@ -23,20 +23,31 @@ assert(Hqqq: (Datatypes.length contents_q = 16)%nat).
move: H H0 ; rewrite ?Zlength_correct => H H0; omega.
assert(Hppp: (Datatypes.length contents_p = 16)%nat).
move: H H0 ; rewrite ?Zlength_correct => H H0; omega.
rewrite Int.sub_signed.
rewrite Int.signed_repr.
rewrite Int.signed_repr.
2: solve_bounds_by_values.
rewrite Int64.sub_signed.
rewrite ?Int64.signed_repr.
2: solve_bounds_by_values.
2: destruct H1 ; subst b ; solve_bounds_by_values.
assert(Hc: exists c, c = (Int64.not (Int64.repr (b - 1)))) by (eexists; reflexivity).
rewrite /Int.not.
rewrite /Int.mone.
replace (Int.xor (Int.repr (b - 1)) (Int.repr (-1))) with
(Int.repr (Z.lxor (b - 1) (-1))).
2:{
move: H1 => [] -> //= ; change (Int.repr 0) with Int.zero ; rewrite Int.xor_zero_l //.
}
assert(Hbb: (Z.lxor (b - 1) (-1)) = 0 \/ (Z.lxor (b - 1) (-1)) = -1).
{
move: H1 => [] -> /= ; auto.
}
rewrite Int.signed_repr.
2: move: Hbb => [] -> ; solve_bounds_by_values.
assert(Hc: exists c, c = (Int64.repr (Z.lxor (b - 1) (-1)))) by (eexists; reflexivity).
destruct Hc as [c Hc] ; rewrite <- Hc.
assert(c = Int64.repr (set_xor b)).
assert(Int64.repr (-1) = Int64.mone) by reflexivity.
assert(Int64.repr 0 = Int64.zero) by reflexivity.
destruct H1 ; subst ; rewrite ?set_xor_0 ?set_xor_1 ?H2 ?H3; simpl.
apply Int64.not_mone.
apply Int64.not_zero.
{
destruct H1 ; subst ; rewrite ?set_xor_0 ?set_xor_1 ?H2 ?H3 => //=.
}
assert(Hd: exists d, d = set_xor b) by (eexists; reflexivity).
destruct Hd as [d Hd].
forward_for_simple_bound 16 (sel25519_Inv sh p q b d contents_p contents_q).
......
......@@ -22,12 +22,12 @@ Import Low.
Definition sel25519_spec :=
DECLARE _sel25519
WITH p: val, q: val, sh : share, contents_p : list Z, contents_q : list Z, b:Z
PRE [ _p OF (tptr tlg), _q OF (tptr tlg), _b OF tlg]
PRE [ _p OF (tptr tlg), _q OF (tptr tlg), _b OF tint]
PROP (writable_share sh;
Zlength contents_p = 16;
Zlength contents_q = 16;
b = 0 \/ b = 1)
LOCAL (temp _p p; temp _q q; temp _b (Vlong (Int64.repr b)))
LOCAL (temp _p p; temp _q q; temp _b (Vint (Int.repr b)))
SEP ( sh [{ p }] <<(lg16)-- mVI64 contents_p;
sh [{ q }] <<(lg16)-- mVI64 contents_q)
POST [ tvoid ]
......@@ -43,7 +43,7 @@ Definition sel25519_Inv sh p q b c contents_p contents_q :=
Zlength contents_q = 16;
b = 0 \/ b = 1;
c = set_xor b)
LOCAL (temp _c (Vlong (Int64.repr c)); temp _p p; temp _q q; temp _b (Vlong (Int64.repr b)))
LOCAL (temp _c (Vlong (Int64.repr c)); temp _p p; temp _q q; temp _b (Vint (Int.repr b)))
SEP ( sh [{ p }] <<(lg16)-- mVI64 (list.take (nat_of_Z i) (Sel25519 b contents_p contents_q) ++ list.drop (nat_of_Z i) contents_p);
sh [{ q }] <<(lg16)-- mVI64 (list.take (nat_of_Z i) (Sel25519 b contents_q contents_p) ++ list.drop (nat_of_Z i) contents_q)).
......
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