diff --git a/aes/verif_gen_tables_LL.v b/aes/verif_gen_tables_LL.v index 04630a9ed1..80a537441a 100644 --- a/aes/verif_gen_tables_LL.v +++ b/aes/verif_gen_tables_LL.v @@ -226,8 +226,8 @@ Proof. && data_at Tsh (tarray tint 256) pow v_pow; tables_uninitialized (gv _tables))). { (* init *) - forward. forward. Exists 0. entailer!. do 2 Exists (repeat Vundef 256). - entailer!. + forward. forward. Exists 0. entailer!!. do 2 Exists (repeat Vundef 256). + entailer!!. } { (* body *) (* forward. TODO floyd: "forward" should tell me to use Intros instead of just failing *) @@ -238,7 +238,7 @@ Proof. TODO floyd: error message should say that I have to thaw *) thaw Fr. forward. - + entailer!. apply pow3_range; lia. + + entailer!!. apply pow3_range; lia. + (* t'1 = ( x & 0x80 ) ? 0x1B : 0x00 ) *) forward_if_diff (PROP () LOCAL (temp _t'1 (Vint ( if Int.eq (Int.and (pow3 i) (Int.repr 128)) Int.zero @@ -246,18 +246,18 @@ Proof. else (Int.repr 27) ))) SEP ()). * (* then-branch of "_ ? _ : _" *) - forward. rewrite Int.eq_false by assumption. entailer!. + forward. rewrite Int.eq_false by assumption. entailer!!. * (* else-branch of "_ ? _ : _" *) forward. match goal with | H: @eq int _ _ |- _ => rewrite H end. rewrite Int.eq_true. - entailer!. + entailer!!. * (* after "_ ? _ : _" *) (* x = (x ^ ((x << 1) ^ t'1)) & 0xFF *) forward. - entailer!. + entailer!!. { f_equal. unfold pow3. rewrite repeat_op_step by lia. reflexivity. } { Exists (upd_Znth i pow (Vint (pow3 i))). Exists (upd_Znth (Int.unsigned (pow3 i)) log (Vint (Int.repr i))). @@ -291,10 +291,10 @@ Proof. forward_for_simple_bound 10 (rcon_loop_inv0 v_pow v_log gv Fr). { (* init *) - forward. forward. Exists 0. entailer!. + forward. forward. Exists 0. entailer!!. } { (* body *) - forward. entailer!. + forward. entailer!!. (* t'2 = ( x & 0x80 ) ? 0x1B : 0x00 ) *) forward_if_diff (PROP () LOCAL (temp _t'2 (Vint ( if Int.eq (Int.and (pow2 i) (Int.repr 128)) Int.zero @@ -302,18 +302,18 @@ Proof. else (Int.repr 27) ))) SEP ()). * (* then-branch of "_ ? _ : _" *) - forward. rewrite Int.eq_false by assumption. entailer!. + forward. rewrite Int.eq_false by assumption. entailer!!. * (* else-branch of "_ ? _ : _" *) forward. match goal with | H: @eq int _ _ |- _ => rewrite H end. rewrite Int.eq_true. - entailer!. + entailer!!. * (* after "_ ? _ : _" *) (* x = ((x << 1) ^ t'2)) & 0xFF *) forward. - entailer!. + entailer!!. - f_equal. unfold pow2 at 1. rewrite repeat_op_step by lia. reflexivity. - apply field_at_update_val. rewrite upd_Znth_app2. @@ -389,16 +389,16 @@ Proof. forward_for_simple_bound 256 (gen_sbox_inv0 v_pow v_log (map Z_to_val log) (map Vint pow) gv Fr). { (* loop invariant holds initially: *) unfold gen_sbox_inv00. - entailer!. + entailer!!. Exists (upd_Znth 99 Vundef256 (Vint (Int.repr 0))). Exists (upd_Znth 0 Vundef256 (Vint (Int.repr 99))). - entailer!. + entailer!!. intros. assert (j = 0) by lia. subst j. rewrite upd_Znth_same. * reflexivity. * change (Zlength Vundef256) with 256. lia. } { (* loop body preserves invariant: *) - forward. { entailer!. rewrite Hlog' by lia. auto. } + forward. { entailer!!. rewrite Hlog' by lia. auto. } pose proof (log3range i). rewrite Hlog' by lia. (* TODO floyd: If I don't do the above to make sure that "temp _logi" is a Vint, @@ -426,14 +426,14 @@ Proof. Intro fsb. Intro rsb. forward. forward. - (* entailment of "forward" *) - entailer!. + entailer!!. apply FSb_range. - (* postcondition implies loop invariant *) - entailer!. + entailer!!. match goal with | |- (field_at _ _ _ ?fsb' _ * field_at _ _ _ ?rsb' _)%logic |-- _ => Exists rsb'; Exists fsb' end. - entailer!. repeat split. + entailer!!. repeat split. + rewrite upd_Znth_diff; (lia || auto). + rewrite upd_Znth_Zlength; lia. + intros. @@ -477,7 +477,7 @@ Proof. (forall j : Z, 1 <= j < 256 -> Znth (Int.unsigned (Znth j FSb)) rsb = Vint (Int.repr j)) /\ (Znth 99 rsb = Vint Int.zero) - ) as P. { entailer!. } + ) as P. { entailer!!. } destruct P as [?H [?H ?H]]. normalize. (* match goal with | |- semax ?D (PROPx ?P (LOCALx ?Q (SEPx ?R))) ?e ?Post => match R with @@ -518,7 +518,7 @@ Proof. forward_for_simple_bound 256 (gen_ftrt_inv0 v_pow v_log (map Z_to_val log) (map Vint pow) gv). { (* loop invariant holds initially: *) unfold gen_ftrt_inv00. - entailer!. + entailer!!. } { (* loop body preserves invariant: *) @@ -535,14 +535,14 @@ Proof. else (Int.repr 27) ))) SEP ()). * (* then-branch of "_ ? _ : _" *) - forward. rewrite Int.eq_false by assumption. entailer!. + forward. rewrite Int.eq_false by assumption. entailer!!. * (* else-branch of "_ ? _ : _" *) forward. match goal with | H: @eq int _ _ |- _ => rewrite H end. rewrite Int.eq_true. - entailer!. + entailer!!. * (* after "_ ? _ : _" *) forward. match goal with @@ -619,7 +619,7 @@ Proof. } pose proof (RSb_range i). forward. forward. forward. { - entailer!. + entailer!!. (* We have to show that we're not in the case "INT_MIN % -1", because that's undefined behavior. TODO floyd: Make sure floyd can solve this automatically, also in solve_efield_denote, so that we don't have to factor out the modulo, but can use it directly as the array index. *) @@ -635,13 +635,15 @@ Proof. } pose proof (mod_range _ 255 A). forward. - entailer!. + entailer!!. + fold Int.zero in *. destruct (Int.eq (Znth i RSb) Int.zero) eqn: E. - - exfalso. apply H3. reflexivity. + - exfalso. apply H3; auto. - simpl. reflexivity. } { (* else-branch *) - forward. entailer!. + forward. entailer!!. + fold Int.zero in *. destruct (Int.eq (Znth i RSb) Int.zero) eqn: E. - simpl. reflexivity. - discriminate. @@ -663,7 +665,7 @@ Proof. pose proof (RSb_range i). forward. forward. forward. { - entailer!. + entailer!!. split. intros [? H99]; inv H99. apply add_no_overflow; auto; computable. @@ -675,13 +677,15 @@ Proof. } pose proof (mod_range _ 255 A). forward. - entailer!. + fold Int.zero in *. + entailer!!. destruct (Int.eq (Znth i RSb) Int.zero) eqn: E. - exfalso. apply H3. reflexivity. - simpl. reflexivity. } { (* else-branch *) - forward. entailer!. + forward. entailer!!. + fold Int.zero in *. destruct (Int.eq (Znth i RSb) Int.zero) eqn: E. - simpl. reflexivity. - discriminate. @@ -703,7 +707,7 @@ Proof. pose proof (RSb_range i). forward. forward. forward. { - entailer!. + entailer!!. split. intros [? H99]; inv H99. apply add_no_overflow; auto; computable. @@ -716,12 +720,14 @@ Proof. pose proof (mod_range _ 255 A). forward. entailer!. + fold Int.zero in *. destruct (Int.eq (Znth i RSb) Int.zero) eqn: E. - exfalso. apply H3. reflexivity. - simpl. reflexivity. } { (* else-branch *) - forward. entailer!. + forward. entailer!!. + fold Int.zero in *. destruct (Int.eq (Znth i RSb)) eqn: E. - simpl. reflexivity. - discriminate. @@ -743,7 +749,7 @@ Proof. pose proof (RSb_range i). forward. forward. forward. { - entailer!. + entailer!!. split. intros [? H99]; inv H99. apply add_no_overflow; auto; computable. @@ -756,12 +762,14 @@ Proof. pose proof (mod_range _ 255 A). forward. entailer!. + fold Int.zero in *. destruct (Int.eq (Znth i RSb) Int.zero) eqn: E. - exfalso. apply H3. reflexivity. - simpl. reflexivity. } { (* else-branch *) forward. entailer!. + fold Int.zero in *. destruct (Int.eq (Znth i RSb) Int.zero) eqn: E. - simpl. reflexivity. - discriminate. @@ -814,7 +822,7 @@ Proof. Ltac canon_load_result ::= default_canon_load_result. (* postcondition implies loop invariant: *) - entailer!. + entailer!!. } unfold partially_filled. change (repeat_op_table (256 - 256) Vundef id) with (@nil val). do 8 rewrite app_nil_r. @@ -837,11 +845,17 @@ Proof. forget RT1 as RT1'. forget RT2 as RT2'. forget RT3 as RT3'. - - entailer!. + repeat (let j := fresh "j" in set (j := field_at _ _ _ _ _); clearbody j). + go_lowerx. cancel. + unfold stackframe_of. + simpl. + rewrite sepcon_emp. + apply sepcon_derives; + sep_apply data_at_data_at_; eapply var_block_lvar0; eauto; reflexivity. } } (* Show.*) Time Qed. (* Coq 8.5.2: 177s Coq 8.6 : 75s + Coq 8.18 with VST 2.13+ and some tweaks to this proof, and a Mac M2: 5.6 secs *) diff --git a/floyd/for_lemmas.v b/floyd/for_lemmas.v index e49c1cea4b..04257c83d4 100644 --- a/floyd/for_lemmas.v +++ b/floyd/for_lemmas.v @@ -824,13 +824,16 @@ intros. eapply derives_trans; try eassumption; auto. Qed. Ltac quick_typecheck3 := + (* do not clear hyps anymore! See issue #772 clear; repeat match goal with | H := _ |- _ => clear H | H : _ |- _ => clear H - end; + end; *) apply quick_derives_right; clear; go_lowerx; intros; - clear; repeat apply andp_right; auto; fail. + clear; repeat apply andp_right; + try apply derives_refl; (* see issue #756 *) + auto; fail. Ltac default_entailer_for_load_store := repeat match goal with H := _ |- _ => clear H end; diff --git a/floyd/sc_set_load_store.v b/floyd/sc_set_load_store.v index a8b9a5cc1b..3924434123 100644 --- a/floyd/sc_set_load_store.v +++ b/floyd/sc_set_load_store.v @@ -1785,7 +1785,9 @@ Qed. Ltac quick_typecheck3 := (* do not clear hyps anymore! See issue #772 *) apply quick_derives_right; go_lowerx; intros; - repeat apply andp_right; auto; fail. + repeat apply andp_right; + try apply derives_refl; (* see issue #756 *) + auto; fail. Ltac default_entailer_for_load_store := (* Don't clear! See issue #772 repeat match goal with H := _ |- _ => clear H end; *) diff --git a/tweetnacl20140427/verif_crypto_stream_salsa20_xor.v b/tweetnacl20140427/verif_crypto_stream_salsa20_xor.v index 3ddb4f6216..a87a258a78 100644 --- a/tweetnacl20140427/verif_crypto_stream_salsa20_xor.v +++ b/tweetnacl20140427/verif_crypto_stream_salsa20_xor.v @@ -335,15 +335,23 @@ forward_if (IfPost v_z v_x bInit (N0, N1, N2, N3) K mCont (Int64.unsigned bInit) eapply (loop2 Espec (FRZL FR1) v_x v_z c mInit); try eassumption; try lia. unfold IfPost. Intros l. - unfold typed_true in BR. inversion BR; clear BR. + (* unfold typed_true in BR. inversion BR; clear BR.*) entailer!!. - rename H1 into H8. + rewrite Int64.eq_false. + 2:{intro; subst. rewrite Int64.unsigned_zero in *. + assert (rounds=0%nat) by (clear - R64a; lia). subst rounds. + clear - H'. simpl in H'. lia. + } +(* + rename H1 into H8. rewrite RR in *. eapply negb_true_iff in H8. unfold Int64.eq in H8. rewrite RR in H8. unfold Int64.zero in H8. rewrite Int64.unsigned_repr in H8. 2: lia. - if_tac in H8. inv H8. clear H8. thaw FR1. + if_tac in H8. inv H8. clear H8. *) + thaw FR1. unfold CoreInSEP. - rewrite Int64.eq_false. 2: assumption. +(* rewrite Int64.eq_false. 2: assumption. +*) Exists (srbytes ++ l). unfold SByte. specialize (CONT_Zlength _ _ _ _ _ _ _ _ CONT); intros CZ. entailer!. @@ -361,31 +369,41 @@ forward_if (IfPost v_z v_x bInit (N0, N1, N2, N3) K mCont (Int64.unsigned bInit) assert (Arith2: Int64.unsigned bInit mod 64 = Int64.unsigned bInit - Z.of_nat rounds * 64). { symmetry; eapply Zmod_unique. lia. instantiate (1:=Z.of_nat rounds); lia. } rewrite Arith1, Arith2, (CONTCONT _ _ _ _ _ _ _ _ CONT). + rewrite <- (Int64.repr_unsigned bInit) in H. + rewrite sub64_repr in H. rewrite Int64.unsigned_repr in H by lia. rewrite if_false. - - exists zbytesR, srbytes, d, snuff, sr_bytes, l. - intuition. - - trivial. - + erewrite (split2_data_at_Tarray_tuchar _ (Int64.unsigned bInit) (Z.of_nat rounds * 64)). + - exists zbytesR, srbytes, d, snuff, sr_bytes, l. + repeat simple apply conj; auto. + - rewrite <- (Int64.repr_unsigned bInit) in BR. + rewrite sub64_repr in BR. contradict BR. rewrite BR. reflexivity. + + + rewrite <- (Int64.repr_unsigned bInit). rewrite !sub64_repr. + rewrite !Int64.unsigned_repr by lia. rewrite Int64.repr_unsigned. + erewrite (split2_data_at_Tarray_tuchar _ (Int64.unsigned bInit) (Z.of_nat rounds * 64)). 2: lia. 2: rewrite Zlength_Bl2VL in *; rewrite Zlength_app. 2: lia. rewrite Zlength_Bl2VL in *; unfold Bl2VL in *. repeat rewrite map_app. autorewrite with sublist. - unfold Sigma_vector. cancel. + cancel. rewrite field_address0_clarify; simpl. rewrite Zplus_0_l, Z.mul_1_l; trivial. unfold field_address0; simpl. rewrite Zplus_0_l, Z.mul_1_l, if_true; trivial. - apply field_compatible_isptr in H13. + apply field_compatible_isptr in H12. destruct cInit; simpl in *; try contradiction; trivial. auto with field_compatible. } { forward. - hnf in H. inversion H; clear H. rewrite RR in *. eapply negb_false_iff in H1. - unfold Int64.eq in H1. rewrite RR in H1. unfold Int64.zero in H1. - rewrite Int64.unsigned_repr in H1 by lia. - if_tac in H1. 2: inv H1. clear H1. + hnf in H. inversion H; clear H. rewrite RR in *. (* eapply negb_false_iff in H1. *) + (* unfold Int64.eq in H1. rewrite RR in H1. unfold Int64.zero in H1.*) + (* rewrite Int64.unsigned_repr in H1 by lia.*) + (* if_tac in H1. 2: inv H1. clear H1. *) + clear RR. + rewrite !Int64.Z_mod_modulus_eq in H1. + rewrite Zminus_mod_idemp_r in H1. + rewrite Z.mod_small in H1 by rep_lia. assert (XX: Int64.unsigned bInit = r64) by lia. - rewrite XX in *. clear H RR. + rewrite XX in *. clear H1. unfold IfPost, CoreInSEP. entailer!. rewrite Zminus_diag in *; rewrite Tarray_0_emp_iff_; try assumption. diff --git a/tweetnacl20140427/verif_fcore_epilogue_htrue.v b/tweetnacl20140427/verif_fcore_epilogue_htrue.v index 29f2e2c295..34cd251c39 100644 --- a/tweetnacl20140427/verif_fcore_epilogue_htrue.v +++ b/tweetnacl20140427/verif_fcore_epilogue_htrue.v @@ -607,7 +607,7 @@ deadvars!. Time entailer!. (*3.6 versus 11.5*) assert (AA: Z.to_nat (i + 1) = S (Z.to_nat i)). - rewrite (Z.add_comm _ 1), Z2Nat.inj_add. simpl. apply NPeano.Nat.add_1_l. lia. lia. + rewrite (Z.add_comm _ 1), Z2Nat.inj_add. simpl. lia. lia. lia. rewrite AA. simpl. thaw FR6. thaw FR5. Time cancel. (*0.8*) (* rewrite <- Heqll. clear Heqll.*)