Merge pull request #766 from PrincetonUniversity/cstring_compspecs

change_compspecs adjusts cstring
PrincetonUniversity · Apr 9, 2024 · 4f687ce · 4f687ce
2 parents 519d1ac + bf4e6fe
commit 4f687ce
Show file tree

Hide file tree

Showing 9 changed files with 47 additions and 9 deletions.
diff --git a/fcf b/fcf
diff --git a/floyd/forward.v b/floyd/forward.v
@@ -10,6 +10,7 @@ Require Import VST.floyd.efield_lemmas.
 Require Import VST.floyd.type_induction.
 Require Import VST.floyd.mapsto_memory_block.
 Require Import VST.floyd.data_at_rec_lemmas.
+Require Import VST.floyd.data_at_lemmas.
 Require Import VST.floyd.field_at.
 Require Import VST.floyd.loadstore_mapsto.
 Require Import VST.floyd.loadstore_field_at.
@@ -712,6 +713,32 @@ a "versus" b ")"
  else fail
 end.
 
+Lemma change_compspecs_cstring: forall cs1 cs2: compspecs, 
+    @cstring cs1 = @cstring cs2.
+Proof.
+intros.
+extensionality sh s p.
+unfold cstring.
+f_equal.
+set (u := map _ _). clearbody u.
+set (n := Zlength _ + _). clearbody n.
+unfold data_at.
+unfold field_at.
+f_equal.
+f_equal.
+unfold field_compatible.
+f_equal; auto.
+f_equal; auto.
+f_equal; auto.
+f_equal; auto.
+unfold align_compatible.
+destruct p; simpl; auto.
+apply prop_ext; split; intro;
+(apply align_compatible_rec_Tarray; intros j ?;
+ apply align_compatible_rec_Tarray_inv with (i:=j) in H; auto;
+ inv H; econstructor; eauto).
+Qed.
+
 Ltac change_compspecs_warning A cs cs' := 
      idtac "Remark: change_compspecs on user-defined mpred:" A cs cs'
  "(to disable this message, Ltac change_compspecs_warning A cs cs' ::= idtac".
@@ -750,7 +777,8 @@ Ltac change_compspecs cs :=
  match goal with |- context [?cs'] =>
    match type of cs' with compspecs =>
      try (constr_eq cs cs'; fail 1);
-     change_compspecs' cs cs';
+     first [rewrite !(change_compspecs_cstring cs' cs)
+            | change_compspecs' cs' cs];
      repeat change_compspecs' cs cs'
    end
 end.

diff --git a/floyd/library.v b/floyd/library.v
@@ -16,6 +16,7 @@ Require Import VST.floyd.aggregate_type.
 Require VST.floyd.aggregate_pred. Import VST.floyd.aggregate_pred.aggregate_pred.
 Require Import VST.floyd.reptype_lemmas.
 Require Import VST.floyd.data_at_rec_lemmas.
+Require Import VST.floyd.data_at_lemmas.
 Require Import VST.floyd.field_at.
 Require Import VST.floyd.field_compat.
 Require Import VST.floyd.stronger.

diff --git a/hmacdrbg/spec_hmac_drbg.v b/hmacdrbg/spec_hmac_drbg.v
@@ -980,7 +980,8 @@ f_equal. unfold hmac_init_funspec. simpl.
         unfold env_set, eval_id in *.  simpl in *. subst. entailer!.
       * unfold argsassert2assert, local, lift1, liftx, lift; simpl. destruct x as [g args]. simpl.
         normalize. entailer!.  discriminate. 
-    - unfold convertPre. simpl. unfold PROPx, LAMBDAx, GLOBALSx, LOCALx, SEPx. change_compspecs CompSepcs.
+    - unfold convertPre. simpl. unfold PROPx, LAMBDAx, GLOBALSx, LOCALx, SEPx.
+      change_compspecs CompSpecs.
       apply pred_ext; simpl; intros.
       * unfold argsassert2assert, local, lift1, liftx, lift; simpl. destruct x as [g args]. simpl.
         normalize. destruct args; [ inv H |]. destruct args; [ inv H |]. destruct args; [ inv H |].
@@ -991,7 +992,7 @@ f_equal. unfold hmac_init_funspec. simpl.
   + extensionality ts x.
     destruct x as [[[[[c sh] l] key] gv] | [[[[[[[c sh] l] key] b] i] shk] gv]].
     - auto.
-    - change_compspecs CompSepcs.
+    - change_compspecs CompSpecs.
       auto.
 Qed.
 

diff --git a/mailbox/verif_mailbox_specs.v b/mailbox/verif_mailbox_specs.v
@@ -14,6 +14,10 @@ Open Scope funspec_scope.
 #[export] Instance CompSpecs_Preserve: change_composite_env verif_atomic_exchange.CompSpecs CompSpecs.
   make_cs_preserve verif_atomic_exchange.CompSpecs CompSpecs.
 Defined.
+#[export] Instance CompSpecs_Preserve': change_composite_env CompSpecs verif_atomic_exchange.CompSpecs.
+  make_cs_preserve CompSpecs verif_atomic_exchange.CompSpecs.
+Defined.
+
 Definition Vprog : varspecs. mk_varspecs prog. Defined.
 
 (* import concurrency funspecs *)

diff --git a/sha/spec_hmac.v b/sha/spec_hmac.v
@@ -13,6 +13,9 @@ Require Import VST.veric.change_compspecs.
 #[export] Instance CompSpecs_Preserve: change_composite_env spec_sha.CompSpecs CompSpecs.
   make_cs_preserve spec_sha.CompSpecs CompSpecs.
 Defined.
+#[export] Instance CompSpecs_Preserve': change_composite_env CompSpecs spec_sha.CompSpecs.
+  make_cs_preserve CompSpecs spec_sha.CompSpecs.
+Defined.
 Definition Vprog : varspecs.  mk_varspecs prog. Defined.
 
 Record TREP := mkTrep { t: type; v: reptype t}.

diff --git a/sha/verif_hmac_final.v b/sha/verif_hmac_final.v
@@ -108,6 +108,7 @@ apply semax_pre with (P':=
       simpl. rewrite Ptrofs.add_zero.
       fold t_struct_SHA256state_st.
       change (Tstruct _SHA256state_st noattr) with t_struct_SHA256state_st.
+      change_compspecs CompSpecs.
       Time cancel. (*0.9*)
 }
 subst l'. clear FR1.
@@ -181,6 +182,7 @@ match goal with |- _ |-- data_at _ _ ?A _ =>
 change A with (default_val t_struct_SHA256state_st, (iCTX, oCTX))
 end.
 subst c.
+change_compspecs CompSpecs.
 Time unfold_data_at (@data_at CompSpecs _ _ _ (Vptr b i)).
 Time assert_PROP (field_compatible t_struct_SHA256state_st [] (Vptr b i)) as FC by entailer!. (*1.2*)
 Time cancel. (*0.7*)

diff --git a/sha/verif_hmac_init.v b/sha/verif_hmac_init.v
@@ -272,6 +272,7 @@ forward_if (EX shaStates:_ ,
     { (*opad loop*)
       eapply semax_pre.
       2: apply (opadloop Espec pb pofs cb cofs ckb ckoff kb kofs l wsh key gv (FRZL FR4) Hwsh IPADcont) with (ipadSHAabs:=ipadSHAabs); try reflexivity; subst ipadSHAabs; try assumption.
+      change_compspecs CompSpecs.
       entailer!.
     }
 
@@ -289,7 +290,7 @@ forward_if (EX shaStates:_ ,
     unfold MORE_COMMANDS, abbreviate.
 
     Time forward_call (Vptr cb (Ptrofs.add cofs (Ptrofs.repr 216)), wsh). (*6.4 versus 10.6*)
-
+    change_compspecs CompSpecs; cancel.
     (* Call to sha_update*)
     thaw FR6.
     Time forward_call (@nil byte,

diff --git a/sha/verif_hmac_init_part1.v b/sha/verif_hmac_init_part1.v
@@ -184,9 +184,7 @@ Proof. intros. abbreviate_semax.
       thaw FR1.
       freeze FR4 := - (sha256state_ _ _ _) (data_at _ _ _ (Vptr kb _)) (K_vector _).
       Time forward_call (@nil byte, key, Vptr cb cofs, wsh, Vptr kb kofs, sh, l, gv). (*4.5*)
-
-      rewrite sublist_same; trivial.
-
+      change_compspecs CompSpecs. cancel.
      (*call Final*)
      thaw FR4. simpl.
      freeze FR5 := - (K_vector _) (sha256state_ _ _ _) (data_at_ _ _ (Vptr ckb _)).
@@ -213,7 +211,7 @@ Proof. intros. abbreviate_semax.
      thaw FR6.
      freeze FR7 := - (K_vector _) (sha256state_ _ _ _) (memory_block _ _ (Vptr ckb _)).
      Time forward_call (key, Vptr ckb ckoff, Vptr cb cofs, wsh, Tsh, gv). (*3.3.versus 4.3*)
-       
+     rewrite sublist_same by lia. cancel.
      (*call memset*)
      thaw FR7.
      unfold tarray.