bump bedrock2 (do not use tuples in memory semantics

Author: andres-erbsen

rupicola

@@ -85,7 +85,7 @@ End Byte.
 Require Import coqutil.Word.Interface.
 Require Import coqutil.Map.Interface. (* coercions *)
 Require Import coqutil.Word.LittleEndianList.
-Require Import bedrock2.Memory. Import WithoutTuples.
+Require Import bedrock2.Memory. Import coqutil.Map.Memory.
 Require coqutil.Word.Naive coqutil.Map.SortedListWord.
 Definition mem_state := (SortedListWord.map (Naive.word 64) Byte.byte).
 

src/Assembly/WithBedrock/Semantics.v

@@ -19,7 +19,7 @@ Import Sorting.Permutation.
 
 Require Import bedrock2.Map.Separation.
 Require Import bedrock2.Map.SeparationLogic.
-Require Import bedrock2.Memory. Import WithoutTuples.
+Require Import bedrock2.Memory. Import coqutil.Map.Memory.
 Require Import coqutil.Map.Interface. (* coercions *)
 Require Import coqutil.Word.Interface.
 Require Import coqutil.Word.LittleEndianList.

src/Assembly/WithBedrock/SymbolicProofs.v

@@ -809,20 +809,10 @@ Section WeakestPrecondition.
       forall s (m:mem) a post,
         load s map.empty a post -> load s m a post.
     Proof.
-      intros *.
-      cbv [load Memory.load Memory.load_Z Memory.load_bytes].
-      rewrite getmany_of_tuple_empty; intros;
-        repeat match goal with
-               | H : exists _, _ |- _ => destruct H
-               | H : _ /\ _ |- _ => destruct H
-               | _ => congruence
-               end.
-      cbv [Memory.bytes_per]; break_match; try congruence.
-      change 0%nat with (Z.to_nat 0).
-      pose proof word.width_pos.
-      rewrite Z2Nat.inj_iff by (try apply Z.div_pos; lia).
-      rewrite Z.eq_sym_iff.
-      apply Z.lt_neq, Z.div_str_pos; lia.
+      cbv [load Memory.load Memory.load_Z Map.Memory.load_bytes]; intros *.
+      destruct option_all eqn:E; [exfalso|intros (?&?&?); discriminate].
+      destruct BW as [ [-> | ->] ], s in E;
+        simpl map in E; rewrite ?map.get_empty in E; discriminate.
     Qed.
   End Load.