forked from PrincetonUniversity/VST
-
Notifications
You must be signed in to change notification settings - Fork 0
/
Copy pathverif_sha_final.v
282 lines (274 loc) · 9.17 KB
/
verif_sha_final.v
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
219
220
221
222
223
224
225
226
227
228
229
230
231
232
233
234
235
236
237
238
239
240
241
242
243
244
245
246
247
248
249
250
251
252
253
254
255
256
257
258
259
260
261
262
263
264
265
266
267
268
269
270
271
272
273
274
275
276
277
278
279
280
281
282
Require Import floyd.proofauto.
Require Import sha.sha.
Require Import sha.SHA256.
Require Import sha.spec_sha.
Require Import sha.sha_lemmas.
Require Import sha.verif_sha_final2.
Require Import sha.verif_sha_final3.
Local Open Scope logic.
Lemma upd_reptype_array_append:
forall t len dd v,
len = Zlength dd ->
upd_reptype_array t len dd v =
dd ++ [v].
Proof.
intros. subst.
unfold upd_reptype_array.
normalize.
rewrite force_lengthn_id by auto.
rewrite skipn_short; auto.
change nat_of_Z with Z.to_nat.
rewrite Z2Nat.inj_add; try omega.
rewrite Zlength_correct. rewrite Nat2Z.id.
omega.
apply Zlength_nonneg.
Qed.
Lemma body_SHA256_Final: semax_body Vprog Gtot f_SHA256_Final SHA256_Final_spec.
Proof.
start_function.
name md_ _md.
name c_ _c.
name p _p.
name n _n.
name cNl _cNl.
name cNh _cNh.
unfold sha256state_.
forward_intro [r_h [r_Nl [r_Nh [r_data r_num]]]].
unfold_data_at 1%nat.
normalize.
unfold s256_relate in H0.
unfold s256_h, s256_Nh,s256_Nl, s256_num, s256_data, fst,snd in H0|-*.
destruct a as [hashed dd].
destruct H0 as [H0 [[H1 H6] [H2 [[H3 DDbytes] [H4 H5]]]]].
subst r_Nh r_Nl r_num r_data.
assert (H3': (Zlength dd < 64)%Z) by assumption.
forward. (* p = c->data; *)
(* This proof should be a lot nicer. *)
assert_LOCAL (temp _p (field_address t_struct_SHA256state_st [StructField _data] c)).
{ entailer.
rewrite field_at_compatible'.
entailer!.
unfold field_address; rewrite if_true by auto. reflexivity.
}
drop_LOCAL 1%nat.
forward. (* n = c->num; *)
rewrite field_at_data_at with (gfs := [StructField _data]) by reflexivity.
normalize.
forward. (* p[n] = 0x80; *)
{
change (nested_field_type2
(nested_field_type2 t_struct_SHA256state_st [StructField _data]) []) with (tarray tuchar 64).
entailer!.
rewrite Zlength_correct in H3' |- *.
omega.
}
change (Int.zero_ext 8 (Int.repr 128)) with (Int.repr 128).
replace (data_at Tsh
(nested_field_type2 t_struct_SHA256state_st [StructField _data])
(upd_reptype_array tuchar (Zlength dd)
(map Vint (map Int.repr dd)) (Vint (Int.repr 128)))) with
(data_at Tsh
(nested_field_type2 t_struct_SHA256state_st [StructField _data])
(map Vint (map Int.repr (dd ++ [128])))).
Focus 2.
{
rewrite !map_app.
simpl (map Vint (map Int.repr [128])).
apply eq_sym.
apply equal_data_one_more_on_list.
+ reflexivity.
+ omega.
+ rewrite !Zlength_map. reflexivity.
} Unfocus.
forward n_old. (* n++; *)
simpl. normalize.
subst r_h. simpl.
set (ddlen := Zlength dd).
assert (Hddlen: (0 <= ddlen < 64)%Z).
unfold ddlen. split; auto. rewrite Zlength_correct; omega.
repeat rewrite initial_world.Zlength_map.
forward_if (invariant_after_if1 hashed dd c md shmd kv).
* (* then-clause *)
change Delta with Delta_final_if1.
match goal with |- semax _ _ ?c _ => change c with Body_final_if1 end.
make_sequential.
normalize_postcondition.
unfold ddlen in *; clear ddlen.
assert (Zlength dd + 1 > 16 * 4 - 8) by omega.
eapply semax_pre0;
[|apply (ifbody_final_if1 Espec hashed md c shmd dd kv H4 H3 H2 DDbytes)].
entailer!.
unfold_data_at 2%nat.
rewrite field_at_data_at with (gfs := [StructField _data]) by reflexivity.
rewrite upd_reptype_array_append
by (rewrite !Zlength_map; auto).
entailer!.
* (* else-clause *)
forward. (* skip; *)
unfold invariant_after_if1.
apply exp_right with hashed.
apply exp_right with (dd ++ [128]).
apply exp_right with 0%Z.
entailer.
apply andp_right; [apply prop_right; repeat split | cancel].
rewrite Forall_app; split; auto.
repeat constructor; omega.
rewrite app_length; simpl. apply Nat2Z.inj_ge.
change (Z.of_nat CBLOCK) with 64; unfold ddlen in H0;
rewrite Zlength_correct in H0.
repeat rewrite Nat2Z.inj_add.
change (Z.of_nat 1) with 1%Z; change (Z.of_nat 8) with 8%Z.
omega.
f_equal. unfold ddlen; repeat rewrite Zlength_correct; f_equal.
rewrite app_length; simpl. rewrite Nat2Z.inj_add; reflexivity.
unfold_data_at 2%nat.
rewrite field_at_data_at with (gfs := [StructField _data]) by reflexivity.
rewrite !map_app.
rewrite upd_reptype_array_append
by (rewrite !Zlength_map; auto).
entailer!.
* unfold invariant_after_if1.
forward_intro hashed'.
forward_intro dd'.
forward_intro pad.
apply semax_extract_PROP; intro DDbytes'.
apply semax_extract_PROP; intro PAD.
normalize.
unfold POSTCONDITION, abbreviate; clear POSTCONDITION.
unfold sha_finish.
unfold SHA_256.
unfold_data_at 1%nat.
replace (field_at Tsh t_struct_SHA256state_st [StructField _data]
(map Vint (map Int.repr dd')) c) with
(field_at Tsh t_struct_SHA256state_st [StructField _data]
(map Vint (map Int.repr dd') ++
list_repeat (CBLOCK - 8 - length dd')%nat Vundef ++ []) c).
Focus 2. {
erewrite field_at_data_equal; [reflexivity |].
rewrite app_nil_r.
apply data_equal_sym, data_equal_list_repeat_default.
} Unfocus.
erewrite array_seg_reroot_lemma
with (gfs := [StructField _data]) (lo := Zlength dd') (hi := Z.of_nat CBLOCK - 8);
[| | | reflexivity | | reflexivity | reflexivity | | ].
2: rewrite Zlength_correct; omega.
Focus 2. {
apply Nat2Z.inj_le in H0.
rewrite Nat2Z.inj_add in H0.
rewrite Zlength_correct.
change 8 with (Z.of_nat 8).
omega.
} Unfocus.
2: change (Z.of_nat CBLOCK) with 64; omega.
2: rewrite !Zlength_map; reflexivity.
Focus 2. {
rewrite !Zlength_correct.
rewrite length_list_repeat.
rewrite !Nat2Z.inj_sub by omega.
reflexivity.
} Unfocus.
normalize.
forward_call' (* memset (p+n,0,SHA_CBLOCK-8-n); *)
(Tsh,
field_address0 t_struct_SHA256state_st
[ArraySubsc (Zlength dd'); StructField _data] c,
(Z.of_nat CBLOCK - 8 - Zlength dd')%Z,
Int.zero) vret.
apply prop_right; repeat constructor; hnf; simpl; auto.
rewrite field_address_clarify by auto.
rewrite field_address0_clarify by auto.
erewrite nested_field_offset2_Tarray by reflexivity.
change (sizeof tuchar) with 1.
rewrite Z.mul_1_l.
normalize.
{pull_left (data_at Tsh (Tarray tuchar (Z.of_nat CBLOCK - 8 - Zlength dd') noattr)
(list_repeat (CBLOCK - 8 - length dd') Vundef)
(field_address0 t_struct_SHA256state_st
[ArraySubsc (Zlength dd'); StructField _data] c)).
repeat rewrite sepcon_assoc; apply sepcon_derives; [ | cancel].
eapply derives_trans; [apply data_at_data_at_; reflexivity |].
assert (sizeof (Tarray tuchar (Z.of_nat CBLOCK - 8 - Zlength dd') noattr) =
Z.of_nat CBLOCK - 8 - Zlength dd').
Focus 1. {
Opaque tuchar.
simpl.
Transparent tuchar.
change (sizeof tuchar) with 1.
rewrite Z.mul_1_l.
rewrite Z.max_r; [reflexivity |].
apply Nat2Z.inj_le in H0.
rewrite Nat2Z.inj_add in H0.
rewrite Zlength_correct.
change 8 with (Z.of_nat 8).
omega.
} Unfocus.
rewrite data_at__memory_block; [| reflexivity |].
Focus 2. {
change Int.modulus with 4294967296.
assert (Z.of_nat CBLOCK = 64) by reflexivity.
pose proof Zlength_correct dd'.
omega.
} Unfocus.
rewrite H7.
entailer!.
}
split; auto.
Omega1.
normalize.
clear vret H7.
forward p_old. (* p += SHA_CBLOCK-8; *)
gather_SEP 0 1 2.
replace_SEP 0 (`(field_at Tsh t_struct_SHA256state_st [StructField _data]
(map Vint (map Int.repr dd') ++ (list_repeat (Z.to_nat (Z.of_nat CBLOCK - 8 - Zlength dd'))
(Vint Int.zero)) ++ []) c)).
{
erewrite array_seg_reroot_lemma
with (gfs := [StructField _data]) (lo := Zlength dd') (hi := Z.of_nat CBLOCK - 8);
[| | | reflexivity | | reflexivity | reflexivity | | ].
2: rewrite Zlength_correct; omega.
Focus 2. {
apply Nat2Z.inj_le in H0.
rewrite Nat2Z.inj_add in H0.
rewrite Zlength_correct.
change 8 with (Z.of_nat 8).
omega.
} Unfocus.
2: change (Z.of_nat CBLOCK) with 64; omega.
2: rewrite !Zlength_map; reflexivity.
Focus 2. {
rewrite !Zlength_correct.
rewrite length_list_repeat.
rewrite !Z2Nat.id by omega.
reflexivity.
} Unfocus.
entailer!.
}
match goal with
| |- semax _ (PROPx nil (LOCALx (_ :: ?L) (SEPx ?S))) _ _ =>
eapply semax_pre with (PROPx nil (LOCALx
((temp _p (field_address t_struct_SHA256state_st
[ArraySubsc (Z.of_nat CBLOCK - 8); StructField _data] c))
:: L) (SEPx S)))
end.
Focus 1. {
clear POSTCONDITION.
entailer!.
clear rho H9 H8.
(* this proof should be nicer. *)
rewrite field_address_clarify.
rewrite field_address_clarify.
normalize.
unfold field_address in *.
if_tac in TC0; try contradiction.
destruct c_; try contradiction; apply I.
unfold field_address in *.
if_tac in TC0; try contradiction.
rewrite if_true.
destruct c_; try contradiction. apply I.
eapply field_compatible_cons_Tarray; try reflexivity; auto.
} Unfocus.
subst n_old p_old.
replace Delta with Delta_final_if1 by (simplify_Delta; reflexivity).
eapply semax_pre; [ | apply final_part2 with pad; try eassumption; try reflexivity].
entailer!.
Qed.