Fix memory write

Author: febyeji

ArchSemArm/VMPromising.v

@@ -303,7 +303,7 @@ Module Memory.
       and thus the corresponding executions would be discarded. TODO prove it.
       *)
   Definition fulfill (ev : Ev.t) (prom : list view) (mem : t) : option view :=
-    prom |> filter (fun t => Some ev =? mem !! t)
+    prom |> filter (λ t, mem !! t = Some ev)
          |> reverse
          |> head.
 
@@ -1358,7 +1358,7 @@ Definition write_mem (tid : nat) (loc : Loc.t) (viio : view) (macc : mem_acc)
     ⊔ view_if is_release (ts.(TState.vrd) ⊔ ts.(TState.vwr)) in
   let vpre := ts.(TState.vspec) ⊔ vbob ⊔ viio in
   guard_discard (vpre ⊔ (TState.coh ts !!! loc) < time)%nat;;
-  mset (TState.prom ∘ fst) $ delete time;;
+  mset (TState.prom ∘ fst) (filter (λ t, t ≠ time));;
   mset fst $ TState.update_coh loc time;;
   mset fst $ TState.update TState.vwr time;;
   mset fst $ TState.update TState.vrel (view_if is_release time);;
@@ -1475,7 +1475,7 @@ Definition run_tlbi (tid : nat) (view : nat) (tlbi : TLBIInfo) :
           then mret t
           else Exec.liftSt PPState.mem $ Memory.promise tlbiev);
   guard_discard (vpre < time)%nat;;
-  mset (TState.prom ∘ PPState.state) $ delete time;;
+  mset (TState.prom ∘ PPState.state) (filter (λ t, t ≠ time));;
   mset PPState.state $ TState.update TState.vtlbi time;;
   mset PPState.iis $ IIS.add time.