Skip to content

Commit 4e8ab5f

Browse files
authored
Merge pull request #757 from PrincetonUniversity/issue756
Patch to partially address issue #756 (localize/unlocalize/quick_typecheck3). closes #756
2 parents 0c4670d + 2235bad commit 4e8ab5f

File tree

5 files changed

+90
-53
lines changed

5 files changed

+90
-53
lines changed

aes/verif_gen_tables_LL.v

Lines changed: 48 additions & 34 deletions
Original file line numberDiff line numberDiff line change
@@ -226,8 +226,8 @@ Proof.
226226
&& data_at Tsh (tarray tint 256) pow v_pow;
227227
tables_uninitialized (gv _tables))).
228228
{ (* init *)
229-
forward. forward. Exists 0. entailer!. do 2 Exists (repeat Vundef 256).
230-
entailer!.
229+
forward. forward. Exists 0. entailer!!. do 2 Exists (repeat Vundef 256).
230+
entailer!!.
231231
}
232232
{ (* body *)
233233
(* forward. TODO floyd: "forward" should tell me to use Intros instead of just failing *)
@@ -238,26 +238,26 @@ Proof.
238238
TODO floyd: error message should say that I have to thaw *)
239239
thaw Fr.
240240
forward.
241-
+ entailer!. apply pow3_range; lia.
241+
+ entailer!!. apply pow3_range; lia.
242242
+ (* t'1 = ( x & 0x80 ) ? 0x1B : 0x00 ) *)
243243
forward_if_diff (PROP () LOCAL (temp _t'1 (Vint (
244244
if Int.eq (Int.and (pow3 i) (Int.repr 128)) Int.zero
245245
then Int.zero
246246
else (Int.repr 27)
247247
))) SEP ()).
248248
* (* then-branch of "_ ? _ : _" *)
249-
forward. rewrite Int.eq_false by assumption. entailer!.
249+
forward. rewrite Int.eq_false by assumption. entailer!!.
250250
* (* else-branch of "_ ? _ : _" *)
251251
forward.
252252
match goal with
253253
| H: @eq int _ _ |- _ => rewrite H
254254
end.
255255
rewrite Int.eq_true.
256-
entailer!.
256+
entailer!!.
257257
* (* after "_ ? _ : _" *)
258258
(* x = (x ^ ((x << 1) ^ t'1)) & 0xFF *)
259259
forward.
260-
entailer!.
260+
entailer!!.
261261
{ f_equal. unfold pow3. rewrite repeat_op_step by lia. reflexivity. }
262262
{ Exists (upd_Znth i pow (Vint (pow3 i))).
263263
Exists (upd_Znth (Int.unsigned (pow3 i)) log (Vint (Int.repr i))).
@@ -291,29 +291,29 @@ Proof.
291291

292292
forward_for_simple_bound 10 (rcon_loop_inv0 v_pow v_log gv Fr).
293293
{ (* init *)
294-
forward. forward. Exists 0. entailer!.
294+
forward. forward. Exists 0. entailer!!.
295295
}
296296
{ (* body *)
297-
forward. entailer!.
297+
forward. entailer!!.
298298
(* t'2 = ( x & 0x80 ) ? 0x1B : 0x00 ) *)
299299
forward_if_diff (PROP () LOCAL (temp _t'2 (Vint (
300300
if Int.eq (Int.and (pow2 i) (Int.repr 128)) Int.zero
301301
then Int.zero
302302
else (Int.repr 27)
303303
))) SEP ()).
304304
* (* then-branch of "_ ? _ : _" *)
305-
forward. rewrite Int.eq_false by assumption. entailer!.
305+
forward. rewrite Int.eq_false by assumption. entailer!!.
306306
* (* else-branch of "_ ? _ : _" *)
307307
forward.
308308
match goal with
309309
| H: @eq int _ _ |- _ => rewrite H
310310
end.
311311
rewrite Int.eq_true.
312-
entailer!.
312+
entailer!!.
313313
* (* after "_ ? _ : _" *)
314314
(* x = ((x << 1) ^ t'2)) & 0xFF *)
315315
forward.
316-
entailer!.
316+
entailer!!.
317317
- f_equal. unfold pow2 at 1. rewrite repeat_op_step by lia. reflexivity.
318318
- apply field_at_update_val.
319319
rewrite upd_Znth_app2.
@@ -389,16 +389,16 @@ Proof.
389389
forward_for_simple_bound 256 (gen_sbox_inv0 v_pow v_log (map Z_to_val log) (map Vint pow) gv Fr).
390390
{ (* loop invariant holds initially: *)
391391
unfold gen_sbox_inv00.
392-
entailer!.
392+
entailer!!.
393393
Exists (upd_Znth 99 Vundef256 (Vint (Int.repr 0))).
394394
Exists (upd_Znth 0 Vundef256 (Vint (Int.repr 99))).
395-
entailer!.
395+
entailer!!.
396396
intros. assert (j = 0) by lia. subst j. rewrite upd_Znth_same.
397397
* reflexivity.
398398
* change (Zlength Vundef256) with 256. lia.
399399
}
400400
{ (* loop body preserves invariant: *)
401-
forward. { entailer!. rewrite Hlog' by lia. auto. }
401+
forward. { entailer!!. rewrite Hlog' by lia. auto. }
402402
pose proof (log3range i).
403403
rewrite Hlog' by lia.
404404
(* TODO floyd: If I don't do the above to make sure that "temp _logi" is a Vint,
@@ -426,14 +426,14 @@ Proof.
426426
Intro fsb. Intro rsb.
427427
forward. forward.
428428
- (* entailment of "forward" *)
429-
entailer!.
429+
entailer!!.
430430
apply FSb_range.
431431
- (* postcondition implies loop invariant *)
432-
entailer!.
432+
entailer!!.
433433
match goal with
434434
| |- (field_at _ _ _ ?fsb' _ * field_at _ _ _ ?rsb' _)%logic |-- _ => Exists rsb'; Exists fsb'
435435
end.
436-
entailer!. repeat split.
436+
entailer!!. repeat split.
437437
+ rewrite upd_Znth_diff; (lia || auto).
438438
+ rewrite upd_Znth_Zlength; lia.
439439
+ intros.
@@ -477,7 +477,7 @@ Proof.
477477
(forall j : Z, 1 <= j < 256 ->
478478
Znth (Int.unsigned (Znth j FSb)) rsb = Vint (Int.repr j)) /\
479479
(Znth 99 rsb = Vint Int.zero)
480-
) as P. { entailer!. }
480+
) as P. { entailer!!. }
481481
destruct P as [?H [?H ?H]]. normalize. (*
482482
match goal with
483483
| |- semax ?D (PROPx ?P (LOCALx ?Q (SEPx ?R))) ?e ?Post => match R with
@@ -518,7 +518,7 @@ Proof.
518518
forward_for_simple_bound 256 (gen_ftrt_inv0 v_pow v_log (map Z_to_val log) (map Vint pow) gv).
519519
{ (* loop invariant holds initially: *)
520520
unfold gen_ftrt_inv00.
521-
entailer!.
521+
entailer!!.
522522
}
523523
{ (* loop body preserves invariant: *)
524524

@@ -535,14 +535,14 @@ Proof.
535535
else (Int.repr 27)
536536
))) SEP ()).
537537
* (* then-branch of "_ ? _ : _" *)
538-
forward. rewrite Int.eq_false by assumption. entailer!.
538+
forward. rewrite Int.eq_false by assumption. entailer!!.
539539
* (* else-branch of "_ ? _ : _" *)
540540
forward.
541541
match goal with
542542
| H: @eq int _ _ |- _ => rewrite H
543543
end.
544544
rewrite Int.eq_true.
545-
entailer!.
545+
entailer!!.
546546
* (* after "_ ? _ : _" *)
547547
forward.
548548
match goal with
@@ -619,7 +619,7 @@ Proof.
619619
}
620620
pose proof (RSb_range i).
621621
forward. forward. forward. {
622-
entailer!.
622+
entailer!!.
623623
(* We have to show that we're not in the case "INT_MIN % -1", because that's undefined behavior.
624624
TODO floyd: Make sure floyd can solve this automatically, also in solve_efield_denote, so
625625
that we don't have to factor out the modulo, but can use it directly as the array index. *)
@@ -635,13 +635,15 @@ Proof.
635635
}
636636
pose proof (mod_range _ 255 A).
637637
forward.
638-
entailer!.
638+
entailer!!.
639+
fold Int.zero in *.
639640
destruct (Int.eq (Znth i RSb) Int.zero) eqn: E.
640-
- exfalso. apply H3. reflexivity.
641+
- exfalso. apply H3; auto.
641642
- simpl. reflexivity.
642643
}
643644
{ (* else-branch *)
644-
forward. entailer!.
645+
forward. entailer!!.
646+
fold Int.zero in *.
645647
destruct (Int.eq (Znth i RSb) Int.zero) eqn: E.
646648
- simpl. reflexivity.
647649
- discriminate.
@@ -663,7 +665,7 @@ Proof.
663665
pose proof (RSb_range i).
664666
forward. forward.
665667
forward. {
666-
entailer!.
668+
entailer!!.
667669
split.
668670
intros [? H99]; inv H99.
669671
apply add_no_overflow; auto; computable.
@@ -675,13 +677,15 @@ Proof.
675677
}
676678
pose proof (mod_range _ 255 A).
677679
forward.
678-
entailer!.
680+
fold Int.zero in *.
681+
entailer!!.
679682
destruct (Int.eq (Znth i RSb) Int.zero) eqn: E.
680683
- exfalso. apply H3. reflexivity.
681684
- simpl. reflexivity.
682685
}
683686
{ (* else-branch *)
684-
forward. entailer!.
687+
forward. entailer!!.
688+
fold Int.zero in *.
685689
destruct (Int.eq (Znth i RSb) Int.zero) eqn: E.
686690
- simpl. reflexivity.
687691
- discriminate.
@@ -703,7 +707,7 @@ Proof.
703707
pose proof (RSb_range i).
704708
forward. forward.
705709
forward. {
706-
entailer!.
710+
entailer!!.
707711
split.
708712
intros [? H99]; inv H99.
709713
apply add_no_overflow; auto; computable.
@@ -716,12 +720,14 @@ Proof.
716720
pose proof (mod_range _ 255 A).
717721
forward.
718722
entailer!.
723+
fold Int.zero in *.
719724
destruct (Int.eq (Znth i RSb) Int.zero) eqn: E.
720725
- exfalso. apply H3. reflexivity.
721726
- simpl. reflexivity.
722727
}
723728
{ (* else-branch *)
724-
forward. entailer!.
729+
forward. entailer!!.
730+
fold Int.zero in *.
725731
destruct (Int.eq (Znth i RSb)) eqn: E.
726732
- simpl. reflexivity.
727733
- discriminate.
@@ -743,7 +749,7 @@ Proof.
743749
pose proof (RSb_range i).
744750
forward. forward.
745751
forward. {
746-
entailer!.
752+
entailer!!.
747753
split.
748754
intros [? H99]; inv H99.
749755
apply add_no_overflow; auto; computable.
@@ -756,12 +762,14 @@ Proof.
756762
pose proof (mod_range _ 255 A).
757763
forward.
758764
entailer!.
765+
fold Int.zero in *.
759766
destruct (Int.eq (Znth i RSb) Int.zero) eqn: E.
760767
- exfalso. apply H3. reflexivity.
761768
- simpl. reflexivity.
762769
}
763770
{ (* else-branch *)
764771
forward. entailer!.
772+
fold Int.zero in *.
765773
destruct (Int.eq (Znth i RSb) Int.zero) eqn: E.
766774
- simpl. reflexivity.
767775
- discriminate.
@@ -814,7 +822,7 @@ Proof.
814822
Ltac canon_load_result ::= default_canon_load_result.
815823

816824
(* postcondition implies loop invariant: *)
817-
entailer!.
825+
entailer!!.
818826
}
819827
unfold partially_filled. change (repeat_op_table (256 - 256) Vundef id) with (@nil val).
820828
do 8 rewrite app_nil_r.
@@ -837,11 +845,17 @@ Proof.
837845
forget RT1 as RT1'.
838846
forget RT2 as RT2'.
839847
forget RT3 as RT3'.
840-
841-
entailer!.
848+
repeat (let j := fresh "j" in set (j := field_at _ _ _ _ _); clearbody j).
849+
go_lowerx. cancel.
850+
unfold stackframe_of.
851+
simpl.
852+
rewrite sepcon_emp.
853+
apply sepcon_derives;
854+
sep_apply data_at_data_at_; eapply var_block_lvar0; eauto; reflexivity.
842855
} }
843856
(* Show.*)
844857
Time Qed.
845858
(* Coq 8.5.2: 177s
846859
Coq 8.6 : 75s
860+
Coq 8.18 with VST 2.13+ and some tweaks to this proof, and a Mac M2: 5.6 secs
847861
*)

floyd/for_lemmas.v

Lines changed: 5 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -824,13 +824,16 @@ intros. eapply derives_trans; try eassumption; auto.
824824
Qed.
825825

826826
Ltac quick_typecheck3 :=
827+
(* do not clear hyps anymore! See issue #772
827828
clear;
828829
repeat match goal with
829830
| H := _ |- _ => clear H
830831
| H : _ |- _ => clear H
831-
end;
832+
end; *)
832833
apply quick_derives_right; clear; go_lowerx; intros;
833-
clear; repeat apply andp_right; auto; fail.
834+
clear; repeat apply andp_right;
835+
try apply derives_refl; (* see issue #756 *)
836+
auto; fail.
834837

835838
Ltac default_entailer_for_load_store :=
836839
repeat match goal with H := _ |- _ => clear H end;

floyd/sc_set_load_store.v

Lines changed: 3 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1785,7 +1785,9 @@ Qed.
17851785
Ltac quick_typecheck3 :=
17861786
(* do not clear hyps anymore! See issue #772 *)
17871787
apply quick_derives_right; go_lowerx; intros;
1788-
repeat apply andp_right; auto; fail.
1788+
repeat apply andp_right;
1789+
try apply derives_refl; (* see issue #756 *)
1790+
auto; fail.
17891791

17901792
Ltac default_entailer_for_load_store :=
17911793
(* Don't clear! See issue #772 repeat match goal with H := _ |- _ => clear H end; *)

tweetnacl20140427/verif_crypto_stream_salsa20_xor.v

Lines changed: 33 additions & 15 deletions
Original file line numberDiff line numberDiff line change
@@ -335,15 +335,23 @@ forward_if (IfPost v_z v_x bInit (N0, N1, N2, N3) K mCont (Int64.unsigned bInit)
335335
eapply (loop2 Espec (FRZL FR1) v_x v_z c mInit); try eassumption; try lia.
336336
unfold IfPost.
337337
Intros l.
338-
unfold typed_true in BR. inversion BR; clear BR.
338+
(* unfold typed_true in BR. inversion BR; clear BR.*)
339339
entailer!!.
340-
rename H1 into H8.
340+
rewrite Int64.eq_false.
341+
2:{intro; subst. rewrite Int64.unsigned_zero in *.
342+
assert (rounds=0%nat) by (clear - R64a; lia). subst rounds.
343+
clear - H'. simpl in H'. lia.
344+
}
345+
(*
346+
rename H1 into H8.
341347
rewrite RR in *. eapply negb_true_iff in H8.
342348
unfold Int64.eq in H8. rewrite RR in H8. unfold Int64.zero in H8.
343349
rewrite Int64.unsigned_repr in H8. 2: lia.
344-
if_tac in H8. inv H8. clear H8. thaw FR1.
350+
if_tac in H8. inv H8. clear H8. *)
351+
thaw FR1.
345352
unfold CoreInSEP.
346-
rewrite Int64.eq_false. 2: assumption.
353+
(* rewrite Int64.eq_false. 2: assumption.
354+
*)
347355
Exists (srbytes ++ l). unfold SByte.
348356
specialize (CONT_Zlength _ _ _ _ _ _ _ _ CONT); intros CZ.
349357
entailer!.
@@ -361,31 +369,41 @@ forward_if (IfPost v_z v_x bInit (N0, N1, N2, N3) K mCont (Int64.unsigned bInit)
361369
assert (Arith2: Int64.unsigned bInit mod 64 = Int64.unsigned bInit - Z.of_nat rounds * 64).
362370
{ symmetry; eapply Zmod_unique. lia. instantiate (1:=Z.of_nat rounds); lia. }
363371
rewrite Arith1, Arith2, (CONTCONT _ _ _ _ _ _ _ _ CONT).
372+
rewrite <- (Int64.repr_unsigned bInit) in H.
373+
rewrite sub64_repr in H. rewrite Int64.unsigned_repr in H by lia.
364374
rewrite if_false.
365-
- exists zbytesR, srbytes, d, snuff, sr_bytes, l.
366-
intuition.
367-
- trivial.
368-
+ erewrite (split2_data_at_Tarray_tuchar _ (Int64.unsigned bInit) (Z.of_nat rounds * 64)).
375+
- exists zbytesR, srbytes, d, snuff, sr_bytes, l.
376+
repeat simple apply conj; auto.
377+
- rewrite <- (Int64.repr_unsigned bInit) in BR.
378+
rewrite sub64_repr in BR. contradict BR. rewrite BR. reflexivity.
379+
+
380+
rewrite <- (Int64.repr_unsigned bInit). rewrite !sub64_repr.
381+
rewrite !Int64.unsigned_repr by lia. rewrite Int64.repr_unsigned.
382+
erewrite (split2_data_at_Tarray_tuchar _ (Int64.unsigned bInit) (Z.of_nat rounds * 64)).
369383
2: lia.
370384
2: rewrite Zlength_Bl2VL in *; rewrite Zlength_app. 2: lia.
371385
rewrite Zlength_Bl2VL in *; unfold Bl2VL in *.
372386
repeat rewrite map_app. autorewrite with sublist.
373-
unfold Sigma_vector. cancel.
387+
cancel.
374388
rewrite field_address0_clarify; simpl.
375389
rewrite Zplus_0_l, Z.mul_1_l; trivial.
376390
unfold field_address0; simpl.
377391
rewrite Zplus_0_l, Z.mul_1_l, if_true; trivial.
378-
apply field_compatible_isptr in H13.
392+
apply field_compatible_isptr in H12.
379393
destruct cInit; simpl in *; try contradiction; trivial.
380394
auto with field_compatible.
381395
}
382396
{ forward.
383-
hnf in H. inversion H; clear H. rewrite RR in *. eapply negb_false_iff in H1.
384-
unfold Int64.eq in H1. rewrite RR in H1. unfold Int64.zero in H1.
385-
rewrite Int64.unsigned_repr in H1 by lia.
386-
if_tac in H1. 2: inv H1. clear H1.
397+
hnf in H. inversion H; clear H. rewrite RR in *. (* eapply negb_false_iff in H1. *)
398+
(* unfold Int64.eq in H1. rewrite RR in H1. unfold Int64.zero in H1.*)
399+
(* rewrite Int64.unsigned_repr in H1 by lia.*)
400+
(* if_tac in H1. 2: inv H1. clear H1. *)
401+
clear RR.
402+
rewrite !Int64.Z_mod_modulus_eq in H1.
403+
rewrite Zminus_mod_idemp_r in H1.
404+
rewrite Z.mod_small in H1 by rep_lia.
387405
assert (XX: Int64.unsigned bInit = r64) by lia.
388-
rewrite XX in *. clear H RR.
406+
rewrite XX in *. clear H1.
389407
unfold IfPost, CoreInSEP.
390408
entailer!.
391409
rewrite Zminus_diag in *; rewrite Tarray_0_emp_iff_; try assumption.

0 commit comments

Comments
 (0)