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

fix proof verif_inv25519.v

parent e6470f0e
......@@ -112,20 +112,20 @@ all: assert(HRTsh:= writable_readable_share HWTsh).
1,2: Exists 2;
orewrite pow_fn_rev_n;
oreplace (253 - (2 - 1) - 1) (253 - 2);
oreplace (254 - 1 - (253 - (2 - 1))) 1;
oreplace (254 - (253 - (2 - 1))) 2;
subst c0;
remember (pow_fn_rev (253 - 2) 254 a a) as c0;
remember (pow_fn_rev (253 - 2) 254 i i) as c0;
clear Heqc0;
replace (step_pow 1 c0 a) with (Low.S c0); [entailer!|];
replace (step_pow 2 c0 i) with (Low.S c0); [entailer!|];
rewrite /step_pow /Inv25519_gen.step_pow ;
change (Zneq_bool 1 1 && Zneq_bool 1 3) with false ; flatten.
1,2: destruct Hi as [Hi|Hi] ; try subst i.
change (Zneq_bool 2 2 && Zneq_bool 2 4) with false ; flatten.
1,2: destruct Ha as [Ha|Ha] ; try subst a.
1: forward_if (PROP ( )
LOCAL (temp _i (Vint (Int.repr 4)); temp _t'1 (Vint (Int.repr 0)); temp _o v_o; temp _a v_o; lvar _c (tarray tlg 16) v_c)
SEP (data_at Tsh (tarray tlg 16) (mVI64 (Low.S c0)) v_c; data_at sho (tarray tlg 16) (mVI64 a) v_o)).
LOCAL (temp _a (Vint (Int.repr 4)); temp _t'1 (Vint (Int.repr 0)); temp _o v_o; temp _i v_o; lvar _c (tarray tlg 16) v_c)
SEP (data_at Tsh (tarray tlg 16) (mVI64 (Low.S c0)) v_c; data_at sho (tarray tlg 16) (mVI64 i) v_o)).
5: forward_if (PROP ( )
LOCAL (temp _i (Vint (Int.repr 4)); temp _t'1 (Vint (Int.repr 0)); temp _o v_o; temp _a v_a; lvar _c (tarray tlg 16) v_c)
SEP (Tsh [{v_c}]<<( lg16 )-- mVI64 (Low.S c0); sho [{v_o}]<<( lg16 )-- o; sha [{v_a}]<<( lg16 )-- mVI64 a)).
LOCAL (temp _a (Vint (Int.repr 4)); temp _t'1 (Vint (Int.repr 0)); temp _o v_o; temp _i v_i; lvar _c (tarray tlg 16) v_c)
SEP (Tsh [{v_c}]<<( lg16 )-- mVI64 (Low.S c0); sho [{v_o}]<<( lg16 )-- o; shi [{v_i}]<<( lg16 )-- mVI64 i)).
1,5: forward.
1,2: entailer!.
1,4: match goal with [ H : Int.one = Int.zero |- _ ] => inversion H end.
......@@ -140,25 +140,25 @@ all: assert(HRTsh:= writable_readable_share HWTsh).
1,2: Exists 4;
orewrite pow_fn_rev_n;
oreplace (253 - (4 - 1) - 1) (253 - 4);
oreplace (254 - 1 - (253 - (4 - 1))) 3;
oreplace (254 - (253 - (4 - 1))) 4;
subst c0;
remember (pow_fn_rev (253 - 4) 254 a a) as c0;
remember (pow_fn_rev (253 - 4) 254 i i) as c0;
clear Heqc0;
replace (step_pow 3 c0 a) with (Low.S c0); [entailer!|];
replace (step_pow 4 c0 i) with (Low.S c0); [entailer!|];
rewrite /step_pow /Inv25519_gen.step_pow ;
change (Zneq_bool 3 1 && Zneq_bool 3 3) with false ; flatten.
1,2: destruct Hi as [Hi2 Hi4].
change (Zneq_bool 4 2 && Zneq_bool 4 4) with false ; flatten.
1,2: destruct Ha as [Ha2 Ha4].
1: forward_if (PROP ( )
LOCAL (temp _i (Vint (Int.repr i)); temp _t'1 (Vint (Int.repr 1)); temp _o v_o; temp _a v_o; lvar _c (tarray tlg 16) v_c)
SEP (data_at Tsh (tarray tlg 16) (mVI64 (Low.S c0)) v_c; data_at sho (tarray tlg 16) (mVI64 a) v_o)).
LOCAL (temp _a (Vint (Int.repr a)); temp _t'1 (Vint (Int.repr 1)); temp _o v_o; temp _i v_o; lvar _c (tarray tlg 16) v_c)
SEP (data_at Tsh (tarray tlg 16) (mVI64 (Low.S c0)) v_c; data_at sho (tarray tlg 16) (mVI64 i) v_o)).
4: forward_if (PROP ( )
LOCAL (temp _i (Vint (Int.repr i)); temp _t'1 (Vint (Int.repr 1)); temp _o v_o; temp _a v_a; lvar _c (tarray tlg 16) v_c)
SEP (Tsh [{v_c}]<<( lg16 )-- mVI64 (Low.S c0); sho [{v_o}]<<( lg16 )-- o; sha [{v_a}]<<( lg16 )-- mVI64 a)).
LOCAL (temp _a (Vint (Int.repr a)); temp _t'1 (Vint (Int.repr 1)); temp _o v_o; temp _i v_i; lvar _c (tarray tlg 16) v_c)
SEP (Tsh [{v_c}]<<( lg16 )-- mVI64 (Low.S c0); sho [{v_o}]<<( lg16 )-- o; shi [{v_i}]<<( lg16 )-- mVI64 i)).
1,4: forward.
1,2: entailer!.
1,2: clean_context_from_VST ; simpl ;
replace (negb (Int.eq (Int.repr i) (Int.repr 4))) with true ; try reflexivity ;
replace (Int.eq (Int.repr i) (Int.repr 4)) with false ; try reflexivity ;
replace (negb (Int.eq (Int.repr a) (Int.repr 4))) with true ; try reflexivity ;
replace (Int.eq (Int.repr a) (Int.repr 4)) with false ; try reflexivity ;
symmetry ; apply Int.eq_false;
intro Hifalse;
inversion Hifalse as [Hifalsee];
......@@ -168,8 +168,8 @@ rewrite Z.mod_small in Hifalsee ; omega.
1,3: exfalso ; omega.
1,2: forward_if.
2,4: exfalso; match goal with [ H : Int.repr 1 = Int.zero |- _ ] => inversion H end.
1: forward_call (v_c,v_c,v_o,Tsh,Tsh,sho,mVI64 (Low.S c0),Low.S c0,a, 0).
4: forward_call (v_c,v_c,v_a,Tsh,Tsh,sha,mVI64 (Low.S c0),Low.S c0,a, 0).
1: forward_call (v_c,v_c,v_o,Tsh,Tsh,sho,mVI64 (Low.S c0),Low.S c0,i, 0).
4: forward_call (v_c,v_c,v_i,Tsh,Tsh,shi,mVI64 (Low.S c0),Low.S c0,i, 0).
1,4: unfold_nm_overlap_array_sep ; simpl ; entailer!.
all: assert(HRsho:= writable_readable_share SH).
1,3: repeat match goal with | [ |- _ /\ _ ] => split | _ => assumption end.
......@@ -180,49 +180,49 @@ all: assert(HRsho:= writable_readable_share SH).
1,2: change (0 =? 0) with true.
1,2: change (1 =? 0) with false.
1,2: flatten.
1,2: Exists i.
1,2: Exists a.
1,2: entailer!.
1,2: replace ((Low.M (Low.S (pow_fn_rev (253 - i) 254 a a)) a)) with (pow_fn_rev (253 - (i - 1)) 254 a a).
1,2: replace ((Low.M (Low.S (pow_fn_rev (253 - a) 254 i i)) i)) with (pow_fn_rev (253 - (a - 1)) 254 i i).
1,3: cancel.
1,2: orewrite pow_fn_rev_n.
1,2: oreplace (253 - (i - 1) - 1) (253 - i).
1,2: oreplace (254 - 1 - (253 - (i - 1))) (i - 1).
1,2: oreplace (253 - (a - 1) - 1) (253 - a).
1,2: oreplace (254 - (253 - (a - 1))) a.
1,2: rewrite /step_pow /Inv25519_gen.step_pow.
1,2: replace (Zneq_bool (i - 1) 1 && Zneq_bool (i - 1) 3) with true ; try reflexivity.
1,2: replace (Zneq_bool a 2 && Zneq_bool a 4) with true ; try reflexivity.
1,2: symmetry ; apply andb_true_iff.
1,2: split ; rewrite /Zneq_bool ; flatten ; apply Z.compare_eq_iff in Eq2; omega.
(* Goal 3 *)
1,4: forward.
1,2: Exists (i - 1).
1,2: Exists (a - 1).
1,2: entailer!.
(* Goal 4 *)
1,3: assert(i = -1) by omega.
1,2: subst i.
1,3: assert(a = -1) by omega.
1,2: subst a.
all: rewrite /inv25519_PostInv.
1,2: oreplace (253 - - 1) 254.
all: unfold_nm_overlap_array_sep.
all: change (0 =? 0) with true.
all: change (1 =? 0) with false.
all: flatten.
all: remember (pow_fn_rev 254 254 a a) as p. (* the expension is always anoying... *)
all: remember (pow_fn_rev 254 254 i i) as p. (* the expension is always anoying... *)
1,2: entailer!.
1,2: assert(Zlength (pow_fn_rev 254 254 a a) = 16) by (apply pow_fn_rev_Zlength ; assumption).
1,2: assert(Zlength (pow_fn_rev 254 254 i i) = 16) by (apply pow_fn_rev_Zlength ; assumption).
(* 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 sha Tsh v_o v_o v_c (mVI64 a) a p 0) ; subst L.
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 sha Tsh v_o v_a v_c o a p 1) ; subst L.
4: forward_for_simple_bound 16 (copy_Inv L sho shi Tsh v_o v_i v_c o i p 1) ; subst L.
4: thaw_local.
1,4: entailer!.
1,3: assert(Hd: exists d, Vlong d = Znth i (mVI64 p) Vundef) by
1,3: assert(Hd: exists d, Vlong d = Znth i0 (mVI64 p) Vundef) by
(eexists ; rewrite map_map (Znth_map 0) ; subst p; try reflexivity ; omega).
1,2: destruct Hd as [d Hd].
1,2: subst p; remember (pow_fn_rev 254 254 a a) as p. (* the expension is always anoying... *)
1,2: subst p; remember (pow_fn_rev 254 254 i i) as p. (* the expension is always anoying... *)
all: unfold_nm_overlap_array_sep.
all: change (0 =? 0) with true.
all: change (1 =? 0) with false.
......@@ -237,9 +237,9 @@ all: flatten ; Intros.
1,2: entailer!.
1,2: unfold data_at ; replace_cancel.
1,2: repeat orewrite simple_S_i.
1,2: remember (pow_fn_rev 254 254 a a) as p.
1,2: rewrite (upd_Znth_app_step_Zlength i _ _ Vundef) ?Hd ; rewrite ?Zlength_map ; try omega ; reflexivity.
1: replace ((firstn (nat_of_Z 16) (mVI64 p) ++ skipn (nat_of_Z 16) (mVI64 a))) with (tkdp (Zlength (mVI64 p)) (mVI64 p) (mVI64 a)).
1,2: remember (pow_fn_rev 254 254 i i) as p.
1,2: rewrite (upd_Znth_app_step_Zlength i0 _ _ Vundef) ?Hd ; rewrite ?Zlength_map ; try omega ; reflexivity.
1: replace ((firstn (nat_of_Z 16) (mVI64 p) ++ skipn (nat_of_Z 16) (mVI64 i))) with (tkdp (Zlength (mVI64 p)) (mVI64 p) (mVI64 i)).
2: replace (Zlength (mVI64 p)) with 16 ; try reflexivity ; rewrite ?Zlength_map ; subst p ; omega.
2: replace ((firstn (nat_of_Z 16) (mVI64 p) ++ skipn (nat_of_Z 16) o)) with (tkdp (Zlength (mVI64 p)) (mVI64 p) o).
3: replace (Zlength (mVI64 p)) with 16 ; try reflexivity ; rewrite ?Zlength_map ; subst p ; omega.
......@@ -256,10 +256,10 @@ all: try (eapply canonicalize_stackframe ; [ reflexivity| ]).
all: try (apply Forall2_cons; [apply fn_data_at_intro ; reflexivity | apply Forall2_nil]).
all: match goal with | [ |- context[[?A] ++ [?B]] ] => change ([A] ++ [B]) with ([A ; B]) end.
all: unfold_nm_overlap_array_sep.
all: assert(Zlength (Inv25519 a) = 16) by (apply Inv25519_Zlength ; omega).
all: assert(Forall (fun x : => -38 <= x < 2 ^ 16 + 38) (Inv25519 a)) by (apply Inv25519_bound_Zlength ; assumption).
all: subst p ; replace (pow_fn_rev 254 254 a a) with (Inv25519 a) by reflexivity.
all: remember (Inv25519 a) as p.
all: assert(Zlength (Inv25519 i) = 16) by (apply Inv25519_Zlength ; omega).
all: assert(Forall (fun x : => -38 <= x < 2 ^ 16 + 38) (Inv25519 i)) by (apply Inv25519_bound_Zlength ; assumption).
all: subst p ; replace (pow_fn_rev 254 254 i i) with (Inv25519 i) by reflexivity.
all: remember (Inv25519 i) as p.
all: rewrite Eq.
all: entailer!.
Qed.
\ No newline at end of file
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