forked from PrincetonUniversity/VST
-
Notifications
You must be signed in to change notification settings - Fork 0
/
Copy pathverif_sha_bdo4.v
682 lines (663 loc) · 26.8 KB
/
verif_sha_bdo4.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
283
284
285
286
287
288
289
290
291
292
293
294
295
296
297
298
299
300
301
302
303
304
305
306
307
308
309
310
311
312
313
314
315
316
317
318
319
320
321
322
323
324
325
326
327
328
329
330
331
332
333
334
335
336
337
338
339
340
341
342
343
344
345
346
347
348
349
350
351
352
353
354
355
356
357
358
359
360
361
362
363
364
365
366
367
368
369
370
371
372
373
374
375
376
377
378
379
380
381
382
383
384
385
386
387
388
389
390
391
392
393
394
395
396
397
398
399
400
401
402
403
404
405
406
407
408
409
410
411
412
413
414
415
416
417
418
419
420
421
422
423
424
425
426
427
428
429
430
431
432
433
434
435
436
437
438
439
440
441
442
443
444
445
446
447
448
449
450
451
452
453
454
455
456
457
458
459
460
461
462
463
464
465
466
467
468
469
470
471
472
473
474
475
476
477
478
479
480
481
482
483
484
485
486
487
488
489
490
491
492
493
494
495
496
497
498
499
500
501
502
503
504
505
506
507
508
509
510
511
512
513
514
515
516
517
518
519
520
521
522
523
524
525
526
527
528
529
530
531
532
533
534
535
536
537
538
539
540
541
542
543
544
545
546
547
548
549
550
551
552
553
554
555
556
557
558
559
560
561
562
563
564
565
566
567
568
569
570
571
572
573
574
575
576
577
578
579
580
581
582
583
584
585
586
587
588
589
590
591
592
593
594
595
596
597
598
599
600
601
602
603
604
605
606
607
608
609
610
611
612
613
614
615
616
617
618
619
620
621
622
623
624
625
626
627
628
629
630
631
632
633
634
635
636
637
638
639
640
641
642
643
644
645
646
647
648
649
650
651
652
653
654
655
656
657
658
659
660
661
662
663
664
665
666
667
668
669
670
671
672
673
674
675
676
677
678
679
680
681
682
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.bdo_lemmas.
Local Open Scope logic.
Lemma rearrange_aux:
forall h f c k l,
Int.add (Int.add (Int.add (Int.add h f) c) k) l =
Int.add (Int.add (Int.add (Int.add l h) f) c) k.
Proof.
intros.
rewrite <- (Int.add_commut l).
repeat rewrite (Int.add_assoc h).
rewrite <- (Int.add_assoc l).
repeat rewrite (Int.add_assoc (Int.add l h)).
reflexivity.
Qed.
Lemma force_lengthn_same:
forall {A} i (b: list A) v,
i = length b -> force_lengthn i b v = b.
Proof.
intros.
subst.
induction b; simpl; auto. f_equal; auto.
Qed.
Lemma loop1_aux_lemma1:
forall i v b,
(i < Zlength b) ->
0 <= i * 4 <= Int.max_unsigned ->
v = nthi b i ->
upd_reptype_array tuint i (map Vint (firstn (Z.to_nat i) b))
(Vint v)
= map Vint (firstn (Z.to_nat (i+1)) b).
Proof.
intros.
assert (Z.to_nat i < length b)%nat.
apply Nat2Z.inj_lt. rewrite Z2Nat.id by omega. rewrite <- Zlength_correct; auto.
unfold upd_reptype_array.
repeat rewrite Z2Nat.inj_add by omega.
change (Z.to_nat 1) with 1%nat.
replace (Z.to_nat i +1)%nat with (S (Z.to_nat i)) by (clear; omega).
rewrite force_lengthn_same
by (rewrite map_length, firstn_length, min_l; auto; omega).
subst v.
replace (nthi b i) with (nthi b (Z.of_nat (Z.to_nat i)))
by (rewrite Z2Nat.id by omega; auto).
clear H0 H. rename H2 into H.
revert b H.
induction (Z.to_nat i); destruct b; simpl length; intros; try omega.
reflexivity.
clear i; rename n into i.
simpl map at 1.
change (map Vint (firstn (S (S i)) (i0 :: b)))
with (Vint i0 :: map Vint (firstn (S i) b)).
rewrite <- app_comm_cons.
f_equal.
replace (nthi (i0::b) (Z.of_nat (S i))) with (nthi b (Z.of_nat i)).
change (skipn (S (S i)) (map Vint (firstn (S i) (i0 :: b))))
with (skipn (S i) (map Vint (firstn i b))).
apply IHn.
omega.
unfold nthi.
repeat rewrite Nat2Z.id. reflexivity.
Qed.
Lemma semax_call_id1'':
forall Espec Delta P Q R ret id retty bl argsig A x Pre Post fs tl
(GLBL: (var_types Delta) ! id = None),
(glob_specs Delta) ! id = Some fs ->
(glob_types Delta) ! id = Some (type_of_funspec fs) ->
fs = mk_funspec (argsig, retty) A Pre Post ->
match retty with
| Tvoid => False
| _ => True
end ->
tc_fn_return Delta (Some ret) retty ->
tl = type_of_params argsig ->
forall
(CLOSQ: Forall (closed_wrt_vars (eq ret)) Q)
(CLOSR: Forall (closed_wrt_vars (eq ret)) R),
@semax Espec Delta (PROPx P (LOCALx (tc_exprlist Delta (argtypes argsig) bl :: Q)
(SEPx (`(Pre x) (make_args' (argsig,retty) (eval_exprlist (argtypes argsig) bl)) :: R))))
(Scall (Some ret)
(Evar id (Tfunction tl retty cc_default))
bl)
(normal_ret_assert
(PROPx P (LOCALx Q (SEPx (`(Post x) (get_result1 ret) :: R))))).
Proof.
intros; subst fs tl; eapply semax_call_id1'; eauto.
Qed.
Lemma read32_reversed_in_bytearray:
forall {Espec: OracleKind} Delta (ofs: int) base e sh (contents: list int) i P Q
(VS: (var_types Delta) ! ___builtin_read32_reversed = None)
(GS: (glob_specs Delta) ! ___builtin_read32_reversed =
Some (snd __builtin_read32_reversed_spec))
(GT: (glob_types Delta) ! ___builtin_read32_reversed =
Some (type_of_funspec (snd __builtin_read32_reversed_spec)))
(TE: typeof e = tptr tuint)
(TCi: tc_fn_return Delta (Some i) tuint)
(CLOQ: Forall (closed_wrt_vars (eq i)) Q),
PROPx P (LOCALx (tc_environ Delta :: Q) (SEP (TT))) |--
PROP ((0 <= Int.unsigned ofs <= Zlength contents - 4 )%Z)
LOCAL (tc_expr Delta e; `(eq (offset_val ofs base)) (eval_expr e))
SEP (TT) ->
semax Delta (PROPx P (LOCALx Q
(SEP (`(data_at sh (tarray tuchar (Zlength contents))
(map Vint contents) base)))))
(Scall (Some i)
(Evar ___builtin_read32_reversed
(Tfunction (Tcons (tptr tuint) Tnil) tuint cc_default))
[e])
(normal_ret_assert
(PROP ()
(LOCALx (temp i (Vint (big_endian_integer
(firstn (Z.to_nat WORD) (skipn (Z.to_nat (Int.unsigned ofs)) contents))))
:: Q)
SEP (`(data_at sh (tarray tuchar (Zlength contents)) (map Vint contents) base))))).
Proof.
intros.
apply semax_pre with
(PROP ((0 <= Int.unsigned ofs <= Zlength contents - 4)%Z;
field_compatible (tarray tuchar (Zlength contents))
[ArraySubsc (Int.unsigned ofs)] base)
(LOCALx (tc_expr Delta e :: `(eq (offset_val ofs base)) (eval_expr e) :: Q)
(SEP(`(data_at sh (tarray tuchar (Zlength contents)) (map Vint contents)
base))))).
rewrite <- (andp_dup (PROPx P _)).
eapply derives_trans; [ apply andp_derives | ].
eapply derives_trans; [ | apply H].
apply andp_derives; auto.
apply andp_derives; auto.
go_lowerx.
apply sepcon_derives; auto.
apply TT_right.
instantiate (1:= PROPx nil (LOCALx Q (SEP (`(data_at sh (tarray tuchar (Zlength contents)) (map Vint contents)
base))))).
go_lowerx. entailer.
go_lowerx. entailer.
apply prop_right.
eapply field_compatible_cons_Tarray; eauto.
reflexivity. omega.
normalize.
clear H. rename H1 into COMPAT.
rewrite data_at_field_at.
erewrite (array_seg_reroot_lemma sh (tarray tuchar (Zlength contents))
nil tuchar (Zlength contents) noattr
(Int.unsigned ofs) (Int.unsigned ofs + 4)
(firstn (Z.to_nat (Int.unsigned ofs)) (map Vint contents))
(firstn 4 (skipn (Z.to_nat (Int.unsigned ofs)) (map Vint contents)))
(skipn (Z.to_nat (Int.unsigned ofs+ 4)) (map Vint contents))
); try reflexivity; auto; try omega.
2: rewrite Z2Nat.inj_add, <- !skipn_skipn, !firstn_skipn by omega; reflexivity.
Focus 2.
rewrite Zlength_correct, firstn_length, min_l.
rewrite Z2Nat.id by omega; omega.
rewrite map_length. apply Nat2Z.inj_le. rewrite Z2Nat.id by omega.
rewrite <- Zlength_correct; omega.
Focus 2.
rewrite Zlength_correct, firstn_length, min_l.
change (Z.of_nat 4) with 4; omega.
rewrite skipn_length. rewrite map_length.
apply Nat2Z.inj_le.
rewrite Nat2Z.inj_sub.
rewrite <- Zlength_correct. rewrite Z2Nat.id by omega.
change (Z.of_nat 4) with 4; omega.
apply Nat2Z.inj_le.
rewrite <- Zlength_correct. rewrite Z2Nat.id by omega.
omega.
normalize.
eapply semax_post_flipped'.
match goal with |- semax _ (PROPx ?P (LOCALx ?Q (SEP (?A; ?B; ?C)))) _ _ =>
semax_frame [ ] [A;C]
end.
(*
eapply semax_pre_post;
[ | | semax_frame [ ] [A;C] ]
end.
apply andp_left2; apply derives_refl.
intros; apply andp_left2.
apply normal_ret_assert_derives'.
*)
2: match goal with |- _ |-- PROP() (LOCALx ?Q (SEP ( _ ; ?B; _))) =>
instantiate (1:=[B]);
instantiate (1:=Q);
instantiate (1:=nil);
rewrite <- app_nil_end; entailer!
end.
replace (Int.unsigned ofs + 4 - Int.unsigned ofs) with 4 by omega.
pose (witness :=
(offset_val ofs base, sh,
firstn 4 (skipn (Z.to_nat (Int.unsigned ofs)) contents))).
eapply semax_pre;
[ | eapply semax_post';
[ | eapply semax_call_id1'' with (x := witness);
try eassumption; try reflexivity; auto ]].
instantiate (1:=nil).
unfold witness.
rewrite skipn_map, firstn_map.
set (cts := firstn 4 (skipn (Z.to_nat (Int.unsigned ofs)) contents)).
rewrite data_at_isptr.
go_lowerx.
normalize.
rewrite prop_true_andp; auto.
rewrite field_address0_clarify; auto.
erewrite nested_field_offset2_Tarray; try reflexivity.
change (nested_field_offset2 (tarray tuchar (Zlength contents)) []) with 0%Z.
rewrite Z.add_0_l.
normalize.
rewrite Int.repr_unsigned.
apply derives_refl.
repeat split; auto.
hnf; simpl. repeat rewrite denote_tc_assert_andp; repeat split; auto.
rewrite TE; simpl. apply I.
unfold cts.
rewrite Zlength_correct.
rewrite firstn_length, min_l.
compute; clear; congruence.
rewrite skipn_length.
clear - H0.
apply Nat2Z.inj_le.
rewrite Nat2Z.inj_sub.
rewrite <- Zlength_correct. change (Z.of_nat 4) with 4.
rewrite Z2Nat.id by omega. omega.
apply Nat2Z.inj_le.
rewrite Z2Nat.id by omega.
rewrite <- Zlength_correct. omega.
hnf. rewrite TE. rewrite <- H3.
unfold eval_id, env_set. simpl.
clear - H5.
unfold field_address0 in H5.
if_tac in H5; try contradiction.
destruct base; try contradiction H5.
reflexivity.
unfold witness.
change (Z.to_nat WORD) with 4%nat.
rewrite skipn_map, firstn_map.
set (cts := firstn 4 (skipn (Z.to_nat (Int.unsigned ofs)) contents)).
fold (tarray tuchar 4).
normalize.
rewrite data_at_isptr.
go_lowerx.
normalize.
rewrite fold_right_and_app_lifted in H1.
destruct H1 as [? [? ?]].
rewrite prop_true_andp.
unfold field_address0.
rewrite if_true by (apply field_compatible_field_compatible0; auto).
erewrite nested_field_offset2_Tarray; try reflexivity.
change (nested_field_offset2 (tarray tuchar (Zlength contents)) []) with 0%Z.
rewrite Z.add_0_l.
normalize.
rewrite Int.repr_unsigned by omega.
auto.
split; auto.
Qed.
Definition block_data_order_loop1 :=
Sfor (Sset _i (Econst_int (Int.repr 0) tint))
(Ebinop Olt (Etempvar _i tint) (Econst_int (Int.repr 16) tint) tint)
(Ssequence
(Ssequence
(Ssequence
(Scall (Some _l')
(Evar ___builtin_read32_reversed (Tfunction
(Tcons
(tptr tuint)
Tnil)
tuint
cc_default))
((Ecast (Etempvar _data (tptr tuchar))
(tptr tuint)) :: nil))
(Sset _l (Ecast (Etempvar _l' tuint) tuint)))
(Sset _data
(Ebinop Oadd (Etempvar _data (tptr tuchar))
(Econst_int (Int.repr 4) tint)
(tptr tuchar))))
(Ssequence
(Sassign
(Ederef
(Ebinop Oadd (Evar _X (tarray tuint 16))
(Etempvar _i tint) (tptr tuint)) tuint)
(Etempvar _l tuint))
(Ssequence
(Sset _Ki
(Ederef
(Ebinop Oadd
(Evar _K256 (tarray tuint 64))
(Etempvar _i tint) (tptr tuint)) tuint))
(Ssequence
(Sset _T1
(Ebinop Oadd
(Ebinop Oadd
(Ebinop Oadd
(Ebinop Oadd (Etempvar _l tuint)
(Etempvar _h tuint) tuint)
(Ebinop Oxor
(Ebinop Oxor
(Ebinop Oor
(Ebinop Oshl
(Etempvar _e tuint)
(Econst_int (Int.repr 26) tint)
tuint)
(Ebinop Oshr
(Ebinop Oand
(Etempvar _e tuint)
(Econst_int (Int.repr (-1)) tuint)
tuint)
(Ebinop Osub
(Econst_int (Int.repr 32) tint)
(Econst_int (Int.repr 26) tint)
tint) tuint) tuint)
(Ebinop Oor
(Ebinop Oshl
(Etempvar _e tuint)
(Econst_int (Int.repr 21) tint)
tuint)
(Ebinop Oshr
(Ebinop Oand
(Etempvar _e tuint)
(Econst_int (Int.repr (-1)) tuint)
tuint)
(Ebinop Osub
(Econst_int (Int.repr 32) tint)
(Econst_int (Int.repr 21) tint)
tint) tuint) tuint)
tuint)
(Ebinop Oor
(Ebinop Oshl
(Etempvar _e tuint)
(Econst_int (Int.repr 7) tint)
tuint)
(Ebinop Oshr
(Ebinop Oand
(Etempvar _e tuint)
(Econst_int (Int.repr (-1)) tuint)
tuint)
(Ebinop Osub
(Econst_int (Int.repr 32) tint)
(Econst_int (Int.repr 7) tint)
tint) tuint) tuint) tuint)
tuint)
(Ebinop Oxor
(Ebinop Oand (Etempvar _e tuint)
(Etempvar _f tuint) tuint)
(Ebinop Oand
(Eunop Onotint
(Etempvar _e tuint) tuint)
(Etempvar _g tuint) tuint) tuint)
tuint) (Etempvar _Ki tuint) tuint))
(Ssequence
(Sset _T2
(Ebinop Oadd
(Ebinop Oxor
(Ebinop Oxor
(Ebinop Oor
(Ebinop Oshl
(Etempvar _a tuint)
(Econst_int (Int.repr 30) tint)
tuint)
(Ebinop Oshr
(Ebinop Oand
(Etempvar _a tuint)
(Econst_int (Int.repr (-1)) tuint)
tuint)
(Ebinop Osub
(Econst_int (Int.repr 32) tint)
(Econst_int (Int.repr 30) tint)
tint) tuint) tuint)
(Ebinop Oor
(Ebinop Oshl
(Etempvar _a tuint)
(Econst_int (Int.repr 19) tint)
tuint)
(Ebinop Oshr
(Ebinop Oand
(Etempvar _a tuint)
(Econst_int (Int.repr (-1)) tuint)
tuint)
(Ebinop Osub
(Econst_int (Int.repr 32) tint)
(Econst_int (Int.repr 19) tint)
tint) tuint) tuint) tuint)
(Ebinop Oor
(Ebinop Oshl (Etempvar _a tuint)
(Econst_int (Int.repr 10) tint)
tuint)
(Ebinop Oshr
(Ebinop Oand
(Etempvar _a tuint)
(Econst_int (Int.repr (-1)) tuint)
tuint)
(Ebinop Osub
(Econst_int (Int.repr 32) tint)
(Econst_int (Int.repr 10) tint)
tint) tuint) tuint) tuint)
(Ebinop Oxor
(Ebinop Oxor
(Ebinop Oand (Etempvar _a tuint)
(Etempvar _b tuint) tuint)
(Ebinop Oand (Etempvar _a tuint)
(Etempvar _c tuint) tuint)
tuint)
(Ebinop Oand (Etempvar _b tuint)
(Etempvar _c tuint) tuint) tuint)
tuint))
(Ssequence
(Sset _h (Etempvar _g tuint))
(Ssequence
(Sset _g (Etempvar _f tuint))
(Ssequence
(Sset _f (Etempvar _e tuint))
(Ssequence
(Sset _e
(Ebinop Oadd
(Etempvar _d tuint)
(Etempvar _T1 tuint) tuint))
(Ssequence
(Sset _d (Etempvar _c tuint))
(Ssequence
(Sset _c (Etempvar _b tuint))
(Ssequence
(Sset _b
(Etempvar _a tuint))
(Sset _a
(Ebinop Oadd
(Etempvar _T1 tuint)
(Etempvar _T2 tuint)
tuint))))))))))))))
(Sset _i
(Ebinop Oadd (Etempvar _i tint)
(Econst_int (Int.repr 1) tint) tint)).
(*Definition block_data_order_loop1 :=
nth 0 (loops (fn_body f_sha256_block_data_order)) Sskip.
*)
Lemma sha256_block_data_order_loop1_proof:
forall (Espec : OracleKind) (sh: share)
(b: list int) ctx (data: val) (regs: list int) kv Xv
(Hregs: length regs = 8%nat),
(* (Hdata: isptr data), *)
length b = LBLOCK ->
semax Delta_loop1
(PROP ()
LOCAL (temp _a (Vint (nthi regs 0)); temp _b (Vint (nthi regs 1));
temp _c (Vint (nthi regs 2)); temp _d (Vint (nthi regs 3));
temp _e (Vint (nthi regs 4)); temp _f (Vint (nthi regs 5));
temp _g (Vint (nthi regs 6)); temp _h (Vint (nthi regs 7));
temp _data data; temp _ctx ctx; temp _in data;
gvar _K256 kv; lvar _X (tarray tuint LBLOCKz) Xv)
SEP (`(data_at_ Tsh (tarray tuint 16) Xv);
`(data_block sh (intlist_to_Zlist b) data); `(K_vector kv)))
block_data_order_loop1
(normal_ret_assert
(PROP ()
LOCAL(temp _ctx ctx; temp _i (Vint (Int.repr LBLOCKz));
temp _a (Vint (nthi (Round regs (nthi b) (LBLOCKz - 1)) 0));
temp _b (Vint (nthi (Round regs (nthi b) (LBLOCKz - 1)) 1));
temp _c (Vint (nthi (Round regs (nthi b) (LBLOCKz - 1)) 2));
temp _d (Vint (nthi (Round regs (nthi b) (LBLOCKz - 1)) 3));
temp _e (Vint (nthi (Round regs (nthi b) (LBLOCKz - 1)) 4));
temp _f (Vint (nthi (Round regs (nthi b) (LBLOCKz - 1)) 5));
temp _g (Vint (nthi (Round regs (nthi b) (LBLOCKz - 1)) 6));
temp _h (Vint (nthi (Round regs (nthi b) (LBLOCKz - 1)) 7));
gvar _K256 kv; lvar _X (tarray tuint LBLOCKz) Xv)
SEP (`(K_vector kv);
`(data_at Tsh (tarray tuint LBLOCKz) (map Vint b) Xv);
`(data_block sh (intlist_to_Zlist b) data))) ).
Proof.
unfold block_data_order_loop1.
intros.
simpl nth; fold rearrange_regs.
abbreviate_semax.
name a_ _a.
name b_ _b.
name c_ _c.
name d_ _d.
name e_ _e.
name f_ _f.
name g_ _g.
name h_ _h.
name l_ _l.
name l'_ _l'.
name Ki _Ki.
name in_ _in.
name ctx_ _ctx.
name i_ _i.
name data_ _data.
assert (LBE := LBLOCK_zeq).
forward_for_simple_bound 16
(EX i:Z,
PROP ()
LOCAL (temp _ctx ctx;
temp _data (offset_val (Int.repr (i*4)) data);
temp _a (Vint (nthi (Round regs (nthi b) (i - 1)) 0));
temp _b (Vint (nthi (Round regs (nthi b) (i - 1)) 1));
temp _c (Vint (nthi (Round regs (nthi b) (i - 1)) 2));
temp _d (Vint (nthi (Round regs (nthi b) (i - 1)) 3));
temp _e (Vint (nthi (Round regs (nthi b) (i - 1)) 4));
temp _f (Vint (nthi (Round regs (nthi b) (i - 1)) 5));
temp _g (Vint (nthi (Round regs (nthi b) (i - 1)) 6));
temp _h (Vint (nthi (Round regs (nthi b) (i - 1)) 7));
lvar _X (tarray tuint LBLOCKz) Xv;
gvar _K256 kv)
SEP (`(K_vector kv);
`(data_at Tsh (tarray tuint LBLOCKz) (map Vint (firstn (Z.to_nat i) b)) Xv);
`(data_block sh (intlist_to_Zlist b) data))).
* (* precondition of loop entails the loop invariant *)
rewrite Round_equation. rewrite if_true by (compute; auto).
entailer!.
* (* loop body & loop condition preserves loop invariant *)
do 2 apply -> seq_assoc.
subst POSTCONDITION; unfold abbreviate.
unfold data_block.
assert_PROP (Forall isbyteZ (intlist_to_Zlist b)); [entailer! | ].
rewrite prop_true_andp by auto.
eapply semax_seq'.
semax_frame
[temp _ctx ctx; temp _i (Vint (Int.repr i));
temp _a (Vint (nthi (Round regs (nthi b) (i - 1)) 0));
temp _b (Vint (nthi (Round regs (nthi b) (i - 1)) 1));
temp _c (Vint (nthi (Round regs (nthi b) (i - 1)) 2));
temp _d (Vint (nthi (Round regs (nthi b) (i - 1)) 3));
temp _e (Vint (nthi (Round regs (nthi b) (i - 1)) 4));
temp _f (Vint (nthi (Round regs (nthi b) (i - 1)) 5));
temp _g (Vint (nthi (Round regs (nthi b) (i - 1)) 6));
temp _h (Vint (nthi (Round regs (nthi b) (i - 1)) 7));
lvar _X (tarray tuint LBLOCKz) Xv;
gvar _K256 kv]
[`(K_vector kv);
`(data_at Tsh (tarray tuint LBLOCKz) (map Vint (firstn (Z.to_nat i) b)) Xv)].
rewrite <- (Zlength_map _ _ Int.repr (intlist_to_Zlist b)).
apply (read32_reversed_in_bytearray _ (Int.repr (i * 4)) data _ sh
(map Int.repr (intlist_to_Zlist b)) _ nil);
[ reflexivity | reflexivity | reflexivity | reflexivity | reflexivity
| auto with closed | ].
entailer!.
rewrite Zlength_correct, map_length, length_intlist_to_Zlist, H.
replace (Z.of_nat (4 * LBLOCK) - 4)%Z
with ((Z.of_nat LBLOCK - 1) * 4)%Z
by (rewrite Zmult_comm, Z.mul_sub_distr_l; reflexivity).
omega.
unfold app.
abbreviate_semax.
(* 1,078,128 849,172 *)
set (bei := big_endian_integer
(firstn (Z.to_nat WORD)
(skipn (Z.to_nat (Int.unsigned (Int.repr (i * 4))))
(map Int.repr (intlist_to_Zlist b))))).
forward. (* l := l'; *)
forward data_old. (* data := data + 4; *)
(* 1,194,800 849,172 *)
(* 1,291,784 894,136 *)
(* change LBLOCKz with 16. this shouldn't be necessary *)
forward. (* X[i]=l; *)
simpl.
assert_PROP (bei = nthi b i). {
entailer!.
unfold nthi.
rewrite Z2Nat.inj_mul by omega.
symmetry.
apply nth_big_endian_integer.
apply nth_error_nth; rewrite H; auto.
pose proof LBLOCK_eq. pose proof LBLOCKz_eq.
apply Z2Nat.inj_lt; try omega.
}
subst bei.
change LBLOCKz with (Z.of_nat LBLOCK).
assert (Hi: 0 <= i * 4 <= Int.max_unsigned). {
clear - H0;
assert (0 <= i * 4 < 64); [split; [omega |] | repable_signed ];
change 64 with (Z.of_nat LBLOCK *4)%Z;
apply Zmult_lt_compat_r; [computable | ];
auto.
apply H0.
}
rewrite loop1_aux_lemma1; auto;
[ | rewrite Zlength_correct, H; omega].
(* 1,506,948 1,110,852 *)
(* 1,506,948 1,134,576 *)
unfold K_vector.
assert (i < Zlength K256)
by (change (Zlength K256) with (LBLOCKz + 48);
pose proof LBLOCKz_eq; omega).
change (Zlength K256) with 64 in *.
change (Z.of_nat LBLOCK) with 16. change CBLOCKz with 64.
forward. (* Ki=K256[i]; *)
(* 1,689,280 1,212,872 *)
entailer!.
unfold Znth. rewrite if_false by omega.
rewrite (nth_map' Vint Vundef Int.zero). apply I.
apply Nat2Z.inj_lt. rewrite Z2Nat.id by omega.
change (Z.of_nat (length K256)) with (LBLOCKz + 48);
pose proof LBLOCKz_eq; omega.
(* 1,811,028 1,406,332 *)
subst POSTCONDITION; unfold abbreviate.
replace (i + 1 - 1)%Z with i by omega.
rewrite (Round_equation _ _ i).
rewrite if_false by omega.
forget (nthi b) as M.
drop_LOCAL 3%nat.
replace (big_endian_integer
(firstn (Z.to_nat WORD)
(skipn (Z.to_nat (Int.unsigned (Int.repr (i * 4))))
(map Int.repr (intlist_to_Zlist b)))))
with (W M i)
by (rewrite W_equation; rewrite if_true by omega; auto).
clear H3.
assert_PROP (isptr data); [entailer! | rename H3 into Hdata].
replace (i*4+4) with (Z.succ i * WORD)%Z
by (unfold Z.succ; rewrite Z.mul_add_distr_r; reflexivity).
unfold Znth at 1.
rewrite if_false by omega.
rewrite (nth_map' _ _ Int.zero)
by (change (length K256) with 64%nat;
apply Nat2Z.inj_lt; rewrite Z2Nat.id by omega;
change (Z.of_nat 64) with 64; omega).
fold (nthi K256 i).
change (data_at Tsh (tarray tuint 64) (map Vint K256)) with K_vector.
change (tarray tuint LBLOCKz) with (tarray tuint 16).
rewrite Zlength_map.
match goal with |- semax _ (PROPx _ (LOCALx _ (SEPx ?R))) _ _ =>
semax_frame [ ] R
end.
clear b H1 H.
forget (nthi K256 i) as k.
forget (W M i) as w.
assert (length (Round regs M (i - 1)) = 8)%nat
by (apply length_Round; auto).
forget (Round regs M (i - 1)) as regs'.
change 16%nat with LBLOCK.
destruct regs' as [ | a [ | b [ | c [ | d [ | e [ | f [ | g [ | h [ | ]]]]]]]]]; inv H.
unfold rearrange_regs.
abbreviate_semax.
forward. (* T1 = l + h + Sigma1(e) + Ch(e,f,g) + Ki; *)
rewrite <- Sigma_1_eq, <- Ch_eq, rearrange_aux.
forward. (* T2 = Sigma0(a) + Maj(a,b,c); *)
rewrite <- Sigma_0_eq, <- Maj_eq.
forward h_old.
forward g_old.
forward f_old.
forward e_old.
forward d_old.
forward c_old.
forward b_old.
forward a_old.
(*simplify_Delta. *)
unfold nthi; simpl nth.
entailer!.
+ rewrite Z.mul_add_distr_r; reflexivity.
+ f_equal.
rewrite <- rearrange_aux. symmetry.
rewrite (rearrange_aux Ki). rewrite Int.add_commut.
repeat rewrite Int.add_assoc. reflexivity.
+ f_equal.
symmetry. do 2 rewrite Int.add_assoc.
rewrite Int.add_commut. rewrite <- Int.add_assoc. f_equal.
f_equal. rewrite Int.add_assoc. reflexivity.
* (* loop invariant & not test implies postcondition *)
cbv beta.
change 16 with LBLOCKz.
rewrite firstn_same
by (change (Z.to_nat LBLOCKz) with LBLOCK; omega).
entailer!.
Qed.