more cleanup

theories/examples/queue/proof_hw_graph.v

@@ -33,8 +33,8 @@ Definition hwqN (N: namespace) (q : loc) := N .@ q.
 (* Ghost Construction we need *)
 Definition backUR := mono_natUR.
 
-(* a persistent map of from enqueued event ids to slots. *)
-Definition emapUR := authUR $ gmapUR event_id (agreeR (leibnizO nat)).
+(* a persistent map from enqueued event ids to slots. *)
+Definition emapUR := authUR $ agreeMR event_id nat.
 
 Definition prod2UR A B C := prodUR (prodUR A B) C.
 Definition prod3UR A B C D := prodUR (prod2UR A B C) D.
@@ -133,7 +133,9 @@ Proof.
 Qed.
 
 (* Slot states *)
-(* TODO: we can do better than Z *)
+(* We can do better than Z, but our language doesn't have comparison for
+  arbitrary literals, and comparison is needed to check for failures.
+  So we restrict the usage of the queue to Z, for now. *)
 Definition enqueue_info : Type := (Z * logView) * (view * event_id).
 Definition einf_val (ei : enqueue_info) : Z := ei.1.1.
 Definition einf_lview (ei : enqueue_info) : logView := ei.1.2.
@@ -1051,20 +1053,17 @@ Lemma to_enq_slots_fork T e i :
   to_enq_slots T ~~> to_enq_slots T ⋅ ◯ {[e := to_agree i]}.
 Proof.
   intros Eqe. apply auth_update_alloc.
-  etrans; first apply core_id_local_update; last (rewrite left_id; by eauto);
-    [apply _|]. apply singleton_included_l.
-  exists (to_agree i). split; [|done]. by rewrite lookup_fmap Eqe.
+  etrans; first by apply to_agreeM_local_update_fork_singleton.
+  by rewrite {2}/to_agreeM fmap_insert fmap_empty.
 Qed.
 
 Lemma to_enq_slots_insert T e i :
   T !! e = None →
   to_enq_slots T ~~> to_enq_slots (<[e:= i]>T) ⋅ ◯ {[e := to_agree i]}.
 Proof.
-  intros FRe. apply auth_update_alloc.
-  (* TODO: another lemma for to_agreeM *)
-  rewrite /to_agreeM fmap_insert. apply alloc_singleton_local_update.
-  - by rewrite lookup_fmap FRe.
-  - done.
+  intros. apply auth_update_alloc.
+  etrans; first by apply to_agreeM_local_update_insert_singleton.
+  by rewrite {2}/to_agreeM fmap_insert fmap_empty.
 Qed.
 
 Lemma slots_master_set_enqueued {γq slots T i γ v M} e V :