reflect fixes in 64-bit

PrincetonUniversity · Apr 5, 2024 · d132e3b · d132e3b
1 parent 3b4bb6c
commit d132e3b
Show file tree

Hide file tree

Showing 2 changed files with 5 additions and 5 deletions.
diff --git a/progs64/io_mem_dry.v b/progs64/io_mem_dry.v
@@ -93,7 +93,7 @@ Proof.
         iPureIntro; repeat (split; first done).
         subst; simpl.
         rewrite Mem.loadbytes_empty //. }
-      rewrite split2_data_at_Tarray_app //.
+      erewrite split2_data_at_Tarray_app; [| done |].
       iDestruct "Hbuf" as "(Hmsg & _)".
       iDestruct (data_at_bytes with "[$Hz $Hmsg]") as %Hmsg; [done.. | |].
       { rewrite Forall_map Forall_forall //. }

diff --git a/progs64/verif_strlib.v b/progs64/verif_strlib.v
@@ -140,10 +140,10 @@ Qed.
 Lemma split_data_at_app_tschar:
  forall sh n (al bl: list val) p,
    n = Zlength (al++bl) ->
-   data_at sh (tarray tschar n) (al++bl) p ⊣⊢
-         data_at sh (tarray tschar (Zlength al)) al p
-        * data_at sh (tarray tschar (n - Zlength al)) bl
-                 (field_address0 (tarray tschar n) [ArraySubsc (Zlength al)] p).
+   data_at sh (tarray tschar n) (al++bl) p =
+         (data_at sh (tarray tschar (Zlength al)) al p
+          * data_at sh (tarray tschar (n - Zlength al)) bl
+                 (field_address0 (tarray tschar n) [ArraySubsc (Zlength al)] p)).
 Proof.
 intros.
 apply (split2_data_at_Tarray_app _ n  sh tschar al bl); auto.