do not use tuples in Semantics, Memory

bedrock2/src/bedrock2/FrameRule.v

@@ -24,12 +24,15 @@ Section semantics.
       load a mSmall r = Some v ->
       load a mBig r = Some v.
   Proof.
-    unfold load, load_Z. intros. fwd. eapply sep_of_load_bytes in E0.
+    unfold load, load_Z. intros.
+    rewrite <-to_list_load_bytes in *.
+    cbv [option_map] in *; fwd.
+    eapply sep_of_load_bytes in E.
     2: destruct a; simpl; destruct width_cases as [W | W]; rewrite W; cbv; discriminate.
-    fwd. unfold sep in E0. fwd.
-    eapply map.split_alt in E0p0.
+    fwd. unfold sep in E. fwd.
+    eapply map.split_alt in Ep0.
     unfold mmap.split in *.
-    rewrite E0p0 in H.
+    rewrite Ep0 in H.
     rewrite mmap.du_assoc in H. unfold mmap.du in H at 1. fwd.
     erewrite load_bytes_of_sep. 1: reflexivity.
     unfold sep. do 2 eexists.
@@ -97,7 +100,11 @@ Section semantics.
       store sz mSmall a v = Some mSmall' ->
       exists mBig', mmap.split mBig' mSmall' mAdd /\ store sz mBig a v = Some mBig'.
   Proof.
-    intros. eapply (store_bytes_frame (F := eq mAdd)) in H0.
+    intros *.
+    cbv [store store_Z].
+    setoid_rewrite <-tuple.to_list_of_list; setoid_rewrite <-store_bytes_correct.
+    intros.
+    eapply (store_bytes_frame (F := eq mAdd)) in H0.
     2: {
       unfold sep. do 2 eexists. ssplit. 2,3: reflexivity. eapply map.split_alt; exact H.
     }

bedrock2/src/bedrock2/Memory.v

@@ -112,41 +112,20 @@ End Memory. End WithoutTuples.
 Section Memory.
   Context {width: Z} {word: word width} {mem: map.map word byte}.
 
-  Definition ftprint(a: word)(n: Z): list word :=
-    List.unfoldn (fun w => word.add w (word.of_Z 1)) (Z.to_nat n) a.
-
-  Definition anybytes(a: word)(n: Z)(m: mem): Prop :=
-    exists bytes: list byte, map.of_disjoint_list_zip (ftprint a n) bytes = Some m.
-
-  Definition footprint(a: word)(sz: nat): tuple word sz :=
-    tuple.unfoldn (fun w => word.add w (word.of_Z 1)) sz a.
-
-  Definition load_bytes(sz: nat)(m: mem)(addr: word): option (tuple byte sz) :=
-    map.getmany_of_tuple m (footprint addr sz).
-
-  Definition unchecked_store_bytes(sz: nat)(m: mem)(a: word)(bs: tuple byte sz): mem :=
-    map.putmany_of_tuple (footprint a sz) bs m.
-
-  Definition store_bytes(sz: nat)(m: mem)(a: word)(v: tuple byte sz): option mem :=
-    match load_bytes sz m a with
-    | Some _ => Some (unchecked_store_bytes sz m a v)
-    | None => None (* some addresses were invalid *)
-    end.
-
   Definition bytes_per sz :=
     match sz with
       | access_size.one => 1 | access_size.two => 2 | access_size.four => 4
       | access_size.word => Z.to_nat (bytes_per_word width)
     end%nat.
 
   Definition load_Z(sz: access_size)(m: mem)(a: word): option Z :=
-    match load_bytes (bytes_per sz) m a with
-    | Some bs => Some (LittleEndianList.le_combine (tuple.to_list bs))
+    match WithoutTuples.load_bytes m a (bytes_per sz) with
+    | Some bs => Some (LittleEndianList.le_combine bs)
     | None => None
     end.
 
   Definition store_Z(sz: access_size)(m: mem)(a: word)(v: Z): option mem :=
-    store_bytes _ m a (tuple.of_list (LittleEndianList.le_split (bytes_per sz) v)).
+    WithoutTuples.store_bytes m a (LittleEndianList.le_split (bytes_per sz) v).
 
   Definition load(sz: access_size)(m: mem)(a: word): option word :=
     match load_Z sz m a with
@@ -157,39 +136,42 @@ Section Memory.
   Definition store(sz: access_size)(m: mem)(a: word)(v: word): option mem :=
     store_Z sz m a (word.unsigned v).
 
-  Lemma load_None: forall sz m a,
-      8 <= width -> (* note: [0 < width] is sufficient *)
-      map.get m a = None ->
-      load sz m a = None.
-  Proof.
-    intros. destruct sz; cbv [load load_Z load_bytes map.getmany_of_tuple footprint bytes_per bytes_per_word tuple.option_all tuple.map tuple.unfoldn];
-    try solve [ rewrite H0; reflexivity].
-    destruct (Z.to_nat ((width + 7) / 8)) eqn: E.
-    - exfalso.
-      assert (0 < (width + 7) / 8) as A. {
-        apply Z.div_str_pos. blia.
-      }
-      change O with (Z.to_nat 0) in E.
-      apply Z2Nat.inj in E; blia.
-    - cbv [tuple.option_all tuple.map tuple.unfoldn].
-      rewrite H0.
-      reflexivity.
-  Qed.
+
+  Section Deprecated. (* The below functions needlessly use tuples for what can be done with lists *)
+
+
+  (* deprecated since 2025 *)
+  Definition footprint(a: word)(sz: nat): tuple word sz :=
+    tuple.unfoldn (fun w => word.add w (word.of_Z 1)) sz a.
+
+  (* deprecated since 2025 *)
+  Definition load_bytes(sz: nat)(m: mem)(addr: word): option (tuple byte sz) :=
+    map.getmany_of_tuple m (footprint addr sz).
+
+  (* deprecated since 2025 *)
+  Definition unchecked_store_bytes(sz: nat)(m: mem)(a: word)(bs: tuple byte sz): mem :=
+    map.putmany_of_tuple (footprint a sz) bs m.
+
+  (* deprecated since 2025 *)
+  Definition store_bytes(sz: nat)(m: mem)(a: word)(v: tuple byte sz): option mem :=
+    match load_bytes sz m a with
+    | Some _ => Some (unchecked_store_bytes sz m a v)
+    | None => None (* some addresses were invalid *)
+    end.
 
   Context {mem_ok: map.ok mem}.
   Context {word_ok: word.ok word}.
 
-  Lemma store_preserves_domain: forall sz m a v m',
-      store sz m a v = Some m' -> map.same_domain m m'.
+  Lemma to_list_footprint a sz :
+    tuple.to_list (footprint a sz) = WithoutTuples.footprint a sz.
   Proof.
-    destruct sz;
-      cbv [store store_Z store_bytes bytes_per load_bytes unchecked_store_bytes];
-      intros;
-      (destruct_one_match_hyp; [|discriminate]);
-      inversion_option;
-      subst;
-      eapply map.putmany_of_tuple_preserves_domain;
-      eassumption.
+    revert a; induction sz; cbn; intros; f_equal.
+    { rewrite Properties.word.add_0_r; trivial. }
+    { cbv [footprint] in IHsz. rewrite IHsz, <-List.seq_shift, List.map_map.
+      eapply List.map_ext; intros.
+      rewrite Nat2Z.inj_succ; cbv [BinInt.Z.succ]; rewrite Properties.word.ring_morph_add.
+      rewrite <-!Properties.word.add_assoc; f_equal.
+      rewrite Properties.word.add_comm; f_equal. }
   Qed.
 
   Lemma anybytes_unique_domain: forall a n m1 m2,
@@ -202,4 +184,37 @@ Section Memory.
     eapply map.of_disjoint_list_zip_same_domain; eassumption.
   Qed.
 
+  Lemma to_list_getmany_of_tuple [key value] [map : map.map key value] sz ks (m : map) :
+    option_map tuple.to_list (map.getmany_of_tuple m (sz:=sz) ks) =
+    option_all (List.map (map.get m) (tuple.to_list ks)).
+  Proof.
+    induction sz; cbn; trivial.
+    case map.get; trivial; intros.
+    erewrite <-IHsz; clear IHsz. cbv [map.getmany_of_tuple].
+    case tuple.option_all; trivial.
+  Qed.
+
+  Lemma to_list_load_bytes sz m a :
+    option_map tuple.to_list (load_bytes sz m a) = WithoutTuples.load_bytes m a sz.
+  Proof.
+    cbv [load_bytes]. rewrite to_list_getmany_of_tuple, to_list_footprint; trivial.
+  Qed.
+
+  Lemma unchecked_store_bytes_correct sz m a bs :
+    unchecked_store_bytes sz m a bs = WithoutTuples.unchecked_store_bytes m a (tuple.to_list bs).
+  Proof.
+    cbv [unchecked_store_bytes WithoutTuples.unchecked_store_bytes].
+    revert a; induction sz; cbn; intros; rewrite ?map.of_list_word_nil, ?map.putmany_empty_r; trivial.
+    rewrite map.of_list_word_at_cons, <-map.put_putmany_commute; f_equal.
+    erewrite <-IHsz; trivial.
+  Qed.
+
+  Lemma store_bytes_correct sz m a bs :
+    store_bytes sz m a bs = WithoutTuples.store_bytes m a (tuple.to_list bs).
+  Proof.
+    cbv [store_bytes WithoutTuples.store_bytes].
+    rewrite <-to_list_load_bytes, tuple.length_to_list; case load_bytes as []; cbn; trivial.
+    rewrite unchecked_store_bytes_correct; trivial.
+  Qed.
+  End Deprecated.
 End Memory.

bedrock2/src/bedrock2/Scalars.v

@@ -44,9 +44,11 @@ Section Scalars.
     : Memory.load_Z sz m addr = Some (truncate_Z (bytes_per (width:=width) sz) value).
   Proof.
     cbv [truncate_Z load scalar littleendian load_Z] in *.
+    rewrite <-to_list_load_bytes.
     unshelve erewrite (_ : bytes_per sz = _); shelve_unifiable; cycle 1.
     1:erewrite load_bytes_of_sep by eassumption.
     2:rewrite length_le_split; trivial.
+    cbv [option_map].
     rewrite tuple.to_list_of_list, LittleEndianList.le_combine_split.
     set (x := (Z.of_nat (bytes_per sz) * 8)%Z).
     assert ((0 <= x)%Z) by (subst x; destruct sz; blia).
@@ -61,6 +63,8 @@ Section Scalars.
   Proof.
     assert (length (le_split (bytes_per(width:=width) sz) oldvalue) = length (le_split (bytes_per(width:=width) sz) value)) as pf
       by (rewrite 2LittleEndianList.length_le_split; trivial).
+    cbv [store_Z].
+    setoid_rewrite <-tuple.to_list_of_list; setoid_rewrite <-store_bytes_correct.
     unshelve eapply store_bytes_of_sep; [..|eapply Hpost]; destruct pf; [|eassumption].
   Qed.
 
@@ -85,8 +89,9 @@ Section Scalars.
     (Hsep : sep (scalar8 addr value) R m)
     : Memory.load Syntax.access_size.one m addr = Some (word.of_Z (byte.unsigned value)).
   Proof.
-    cbv [load load_Z load_bytes bytes_per footprint tuple.unfoldn map.getmany_of_tuple tuple.option_all tuple.map tuple.to_list].
-    erewrite get_sep, le_combine_1 by exact Hsep; repeat f_equal.
+    cbv [load load_Z WithoutTuples.load_bytes bytes_per WithoutTuples.footprint List.map List.seq option_all].
+    erewrite get_sep, le_combine_1; trivial.
+    rewrite Properties.word.add_0_r; eauto.
   Qed.
 
   Lemma load_two_of_sep addr value R m
@@ -149,6 +154,8 @@ Section Scalars.
     (Hpost : forall m, sep (scalar8 addr (byte.of_Z (word.unsigned value))) R m -> post m)
     : exists m1, Memory.store Syntax.access_size.one m addr value = Some m1 /\ post m1.
   Proof.
+    cbv [store store_Z].
+    setoid_rewrite <-tuple.to_list_of_list; setoid_rewrite <-store_bytes_correct.
     eapply (store_bytes_of_sep _ 1 (PrimitivePair.pair.mk _ tt)); cbn; [ecancel_assumption|].
     cbv [LittleEndianList.le_split PrimitivePair.pair._1 tuple.of_list].
     intros; eapply Hpost; ecancel_assumption.
@@ -170,19 +177,26 @@ Section Scalars.
     (Hsep : sep (scalar16 addr oldvalue) R m)
     (Hpost : forall m, sep (scalar16 addr value) R m -> post m)
     : exists m1, Memory.store Syntax.access_size.two m addr value = Some m1 /\ post m1.
-  Proof. eapply store_bytes_of_sep; [eapply Hsep|eapply Hpost]. Qed.
+  Proof.
+    cbv [store store_Z]; setoid_rewrite <-tuple.to_list_of_list; setoid_rewrite <-store_bytes_correct.
+    eapply store_bytes_of_sep; [eapply Hsep|eapply Hpost].
+  Qed.
 
   Lemma store_four_of_sep addr (oldvalue : word) (value : word) R m (post:_->Prop)
     (Hsep : sep (scalar32 addr oldvalue) R m)
     (Hpost : forall m, sep (scalar32 addr value) R m -> post m)
     : exists m1, Memory.store Syntax.access_size.four m addr value = Some m1 /\ post m1.
-  Proof. eapply store_bytes_of_sep; [eapply Hsep|eapply Hpost]. Qed.
+  Proof.
+    cbv [store store_Z]; setoid_rewrite <-tuple.to_list_of_list; setoid_rewrite <-store_bytes_correct.
+    eapply store_bytes_of_sep; [eapply Hsep|eapply Hpost].
+  Qed.
 
   Lemma store_word_of_sep addr (oldvalue value: word) R m (post:_->Prop)
     (Hsep : sep (scalar addr oldvalue) R m)
     (Hpost : forall m, sep (scalar addr value) R m -> post m)
     : exists m1, Memory.store Syntax.access_size.word m addr value = Some m1 /\ post m1.
   Proof.
+    cbv [store store_Z]; setoid_rewrite <-tuple.to_list_of_list; setoid_rewrite <-store_bytes_correct.
     let sz := Syntax.access_size.word in
     assert (length (le_split (bytes_per(width:=width) sz) (word.unsigned oldvalue)) = length (le_split (bytes_per(width:=width) sz) (word.unsigned value))) as pf
       by (rewrite 2LittleEndianList.length_le_split; trivial).

bedrock2/src/bedrock2Examples/memconst.v

@@ -135,7 +135,7 @@ Section WithParameters.
       rewrite word.unsigned_of_Z_nowrap, byte.of_Z_unsigned in H9 by ZnWords.
       replace (Z.to_nat v0) with (1 + (Z.to_nat i0))%nat in H9 by ZnWords.
       rewrite <-List.skipn_skipn in H9.
-      rewrite List.nth_error_as_skipn in Heqo.
+      rewrite List.nth_error_as_skipn, Properties.word.add_0_r  in Heqo.
       remember (List.skipn (Z.to_nat i0) bs) as ts in *.
       destruct ts in *; cbn [List.skipn List.hd_error Array.array] in *; [discriminate|].
       subst v.

bedrock2/src/bedrock2Examples/memmove.v

@@ -166,13 +166,15 @@ Section WithParameters.
           rewrite map.get_of_list_word_at in H14.
           progress replace (Z.to_nat (word.sub src0 src0)) with O in H14 by ZnWords;
             cbn in H14; case H14 as [[? ?]|[? ?]]; try discriminate.
+          rewrite Properties.word.add_0_r.
           rewrite H14. split. { rewrite LittleEndianList.le_combine_1. trivial. }
 
-          cbv [WeakestPrecondition.store load load_Z load_bytes store store_Z store_bytes unchecked_store_bytes LittleEndianList.le_split]; cbn.
+          cbv [WeakestPrecondition.store load load_Z WithoutTuples.load_bytes store store_Z WithoutTuples.store_bytes WithoutTuples.unchecked_store_bytes LittleEndianList.le_split]; cbn.
           pose proof map.get_split dst0 _ _ _ H8.
           rewrite map.get_of_list_word_at in H16.
           progress replace (Z.to_nat (word.sub dst0 dst0)) with O in H16 by ZnWords;
             cbn in H16; case H16 as [[? ?]|[? ?]]; try discriminate.
+          rewrite Properties.word.add_0_r.
           eexists. rewrite H16. split.
           { rewrite word.unsigned_of_Z, Scalars.wrap_byte_unsigned.
             rewrite byte.of_Z_unsigned; trivial. }
@@ -210,8 +212,8 @@ Section WithParameters.
               repeat (destruct String.eqb; trivial). } }
           eexists _, _, _, _, (length s0); split; ssplit.
           { ZnWords. }
-          { eassumption. }
-          { eassumption. }
+          { rewrite map.of_list_word_singleton, <-map.put_putmany_commute, map.putmany_empty_r; eassumption. }
+          { rewrite map.of_list_word_singleton, <-map.put_putmany_commute, map.putmany_empty_r; eassumption. }
           { ZnWords. }
           { cbn in *; ZnWords. }
           { cbn in *; ZnWords. }
@@ -306,14 +308,16 @@ Section WithParameters.
           match goal with H : context[List.nth_error [_] ?i = None] |- _ =>
               replace i with O in H by ZnWords; cbn [List.nth_error] in H end.
           cbn in H14; case H14 as [[? ?]|[? ?]]; try discriminate.
+          rewrite Properties.word.add_0_r.
           rewrite H14. split. { rewrite LittleEndianList.le_combine_1. trivial. }
 
-          cbv [WeakestPrecondition.store load load_Z load_bytes store store_Z store_bytes unchecked_store_bytes LittleEndianList.le_split]; cbn.
+          cbv [WeakestPrecondition.store load load_Z WithoutTuples.load_bytes store store_Z WithoutTuples.store_bytes WithoutTuples.unchecked_store_bytes LittleEndianList.le_split]; cbn.
           pose proof map.get_split dst0 _ _ _ H8.
           rewrite !map.get_of_list_word_at, !List.nth_error_app2 in H16 by ZnWords.
           match goal with H : context[List.nth_error [_] ?i = None] |- _ =>
               replace i with O in H by ZnWords; cbn [List.nth_error] in H end.
           case H16 as [[? ?]|[? ?]]; try discriminate.
+          rewrite Properties.word.add_0_r.
           eexists. rewrite H16. split.
           { rewrite word.unsigned_of_Z, Scalars.wrap_byte_unsigned.
             rewrite byte.of_Z_unsigned; trivial. }
@@ -353,10 +357,10 @@ Section WithParameters.
           { ZnWords. }
           { replace (word.sub (word.sub src0 (word.of_Z 1))(word.sub (word.sub n0 (word.of_Z 1)) (word.of_Z 1)))
               with (word.sub src0 (word.sub n0 (word.of_Z 1))) by ZnWords.
-            eassumption. }
+            rewrite map.of_list_word_singleton, <-map.put_putmany_commute, map.putmany_empty_r; eassumption. }
           { replace (word.sub (word.sub dst0 (word.of_Z 1)) (word.sub (word.sub n0 (word.of_Z 1)) (word.of_Z 1)))
               with (word.sub dst0 (word.sub n0 (word.of_Z 1))) by ZnWords.
-            eassumption. }
+            rewrite map.of_list_word_singleton, <-map.put_putmany_commute, map.putmany_empty_r; eassumption. }
           { ZnWords. }
           { cbn in *; ZnWords. }
           { cbn in *; ZnWords. }

compiler/src/compiler/FlatToRiscvCommon.v

@@ -434,6 +434,7 @@ Section FlatToRiscv1.
       mcomp_sat (Bind (execute (compile_load iset sz x a ofs)) f) initialL post.
   Proof using word_ok PR BWM.
     unfold compile_load, Memory.load, Memory.load_Z, Memory.bytes_per, Memory.bytes_per_word.
+    setoid_rewrite <-Memory.to_list_load_bytes; cbv [option_map].
     rewrite bitwidth_matches.
     destruct width_cases as [E | E];
       (* note: "rewrite E" does not work because "width" also appears in the type of "word",
@@ -466,8 +467,9 @@ Section FlatToRiscv1.
                                       (getXAddrs initialL))
                        (withMem m' (updateMetrics (addMetricStores 1) initialL))) post ->
       mcomp_sat (Bind (execute (compile_store iset sz a x ofs)) f) initialL post.
-  Proof using PR BWM.
+  Proof using PR BWM mem_ok word_ok.
     unfold compile_store, Memory.store, Memory.store_Z, Memory.bytes_per, Memory.bytes_per_word.
+    setoid_rewrite <-HList.tuple.to_list_of_list; setoid_rewrite <-Memory.store_bytes_correct; setoid_rewrite HList.tuple.to_list_of_list.
     rewrite bitwidth_matches.
     destruct width_cases as [E | E];
       (* note: "rewrite E" does not work because "width" also appears in the type of "word",
@@ -880,7 +882,10 @@ Section FlatToRiscv1.
     intros *. intros L M0.
     destruct (program_compile_byte_list table addr) as [Padding P].
     apply (Proper_sep_impl1 _ _ P R R) in M0; [|reflexivity]; clear P.
-    unfold Memory.load, Memory.load_Z in *. simp.
+    revert L.
+    unfold Memory.load, Memory.load_Z.
+    setoid_rewrite <-Memory.to_list_load_bytes; cbv [option_map]; intros.
+    simp. rename E1 into E0.
     eapply shift_load_bytes_in_of_list_word in E0.
     pose proof @subst_load_bytes_for_eq as P. cbv zeta in P.
     specialize P with (1 := E0) (2 := M0).

compiler/src/compiler/FlatToRiscvFunctions.v

@@ -1647,19 +1647,26 @@ Section Proofs.
 
     - idtac "Case compile_stmt_correct/SLoad".
       progress unfold Memory.load, Memory.load_Z in *. fwd.
+      rewrite <-Memory.to_list_load_bytes in *; cbv [option_map] in *; fwd.
       subst_load_bytes_for_eq.
       assert (x <> RegisterNames.sp). {
         unfold valid_FlatImp_var, RegisterNames.sp in *.
         blia.
       }
       inline_iff1.
-      run1det. clear H0. (* <-- TODO this should not be needed *) run1done.
+
+      eapply runsTo_det_step_with_valid_machine; [ assumption | simulate' | ].
+      { unfold Memory.load, Memory.load_Z in *; simpl_MetricRiscvMachine_mem.
+        erewrite <-Memory.to_list_load_bytes, load_bytes_of_sep; [ reflexivity | ecancel_assumption ]. }
+      1:reflexivity.
+      intros. clear H0. (* <-- TODO this should not be needed *) run1done.
 
 
     - idtac "Case compile_stmt_correct/SStore".
       inline_iff1.
       simpl_MetricRiscvMachine_get_set.
       unfold Memory.store, Memory.store_Z in *.
+      setoid_rewrite <-HList.tuple.to_list_of_list in H1; setoid_rewrite <-Memory.store_bytes_correct in H1.
       change Memory.store_bytes with (Platform.Memory.store_bytes(word:=word)) in *.
       match goal with
       | H: Platform.Memory.store_bytes _ _ _ _ = _ |- _ =>
@@ -1673,7 +1680,13 @@ Section Proofs.
       unfold Platform.Memory.store_bytes, Memory.store_Z, Memory.store_bytes in A. fwd.
       destruct (eq_sym (LittleEndianList.length_le_split (Memory.bytes_per(width:=width) sz) (word.unsigned val))) in t0, E.
       subst_load_bytes_for_eq.
-      run1det. run1done.
+      eapply runsTo_det_step_with_valid_machine; [ assumption | simulate' | ].
+      { unfold Memory.store, Memory.store_Z.
+        setoid_rewrite <-HList.tuple.to_list_of_list; setoid_rewrite <-Memory.store_bytes_correct.
+        eassumption. }
+      1:reflexivity.
+      intros.
+      run1done.
       eapply preserve_subset_of_xAddrs. 1: assumption.
       ecancel_assumption.