From mathcomp.ssreflect
Require Import ssreflect ssrbool ssrnat eqtype ssrfun seq.
From mathcomp
Require Import path.
Require Import Eqdep.
Require Import Relation_Operators.
From fcsl
Require Import pred prelude ordtype finmap pcm unionmap heap.
From DiSeL
Require Import Freshness DepMaps EqTypeX.
Set Implicit Arguments.
Unset Strict Implicit.
Unset Printing Implicit Defensive.

(* Shared state, as implemented by the message soup.

   At this point, the implementation is based on top of standard union
   maps. This defines the procedure for allocating new messages: just
(* Goal: @eq soup (@UMC.upd mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage)) j (@mark_msg TaggedMessage mm) (@PCM.join (@union_map_classPCM mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage))) (@um_pts mid (msg TaggedMessage) i mm) s')) (@PCM.join (@union_map_classPCM mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage))) (@um_pts mid (msg TaggedMessage) i (@mark_msg TaggedMessage mm)) s') *)
(* Goal: @eq soup match @UMC.find mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage)) j s' with | Some m => @UMC.upd mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage)) j (@mark_msg TaggedMessage m) (@PCM.join (@union_map_classPCM mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage))) (@um_pts mid (msg TaggedMessage) i mm) s') | None => @PCM.join (@union_map_classPCM mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage))) (@um_pts mid (msg TaggedMessage) i mm) s' end (@PCM.join (@union_map_classPCM mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage))) (@um_pts mid (msg TaggedMessage) i mm) match @UMC.find mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage)) j s' with | Some m => @UMC.upd mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage)) j (@mark_msg TaggedMessage m) s' | None => s' end) *)
   by taking the next-to-the largest id in the corresponding
   batch. Indeed, this is not particularly nice, as it assumes the
   _global_ message soup.

   It's not clear at this moment, what will be the best representation
   of the soup so it would be in the same time _local_ and also would
   allow for th allocation. Perhaps, we should just consider local
   soups, ensuring that they all carry distinct labels, and then when
   cojoin them, make sure that for clashing message id's protocol
   labels are different.

 *)

Section TaggedMessages. 

  Structure TaggedMessage :=
    TMsg {
        tag: nat;
        (* Okay, this is a big omissin, but for now I'm sick and tired
           to deal with casts everywhere, so for the moment the
           contents of the messages are going to be just sequences of
(* Goal: @eq soup (@UMC.upd mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage)) j (@mark_msg TaggedMessage mm) (@PCM.join (@union_map_classPCM mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage))) (@um_pts mid (msg TaggedMessage) i mm) s')) (@PCM.join (@union_map_classPCM mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage))) (@um_pts mid (msg TaggedMessage) i (@mark_msg TaggedMessage mm)) s') *)
(* Goal: @eq soup match @UMC.find mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage)) j s' with | Some m => @UMC.upd mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage)) j (@mark_msg TaggedMessage m) (@PCM.join (@union_map_classPCM mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage))) (@um_pts mid (msg TaggedMessage) i mm) s') | None => @PCM.join (@union_map_classPCM mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage))) (@um_pts mid (msg TaggedMessage) i mm) s' end (@PCM.join (@union_map_classPCM mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage))) (@um_pts mid (msg TaggedMessage) i mm) match @UMC.find mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage)) j s' with | Some m => @UMC.upd mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage)) j (@mark_msg TaggedMessage m) s' | None => s' end) *)
           natural number, and it's up to the client-supplied
           coherence predicate to restrict them appropriately, relating this thing to tags *)
        tms_cont :> seq nat          
      }.

End TaggedMessages.

Section Shared.

  Definition Label := [ordType of nat].

  (* (Heterogenious) messages are parametrized by

(* Goal: @eq soup (@UMC.upd mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage)) j (@mark_msg TaggedMessage mm) (@PCM.join (@union_map_classPCM mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage))) (@um_pts mid (msg TaggedMessage) i mm) s')) (@PCM.join (@union_map_classPCM mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage))) (@um_pts mid (msg TaggedMessage) i (@mark_msg TaggedMessage mm)) s') *)
(* Goal: @eq soup match @UMC.find mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage)) j s' with | Some m => @UMC.upd mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage)) j (@mark_msg TaggedMessage m) (@PCM.join (@union_map_classPCM mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage))) (@um_pts mid (msg TaggedMessage) i mm) s') | None => @PCM.join (@union_map_classPCM mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage))) (@um_pts mid (msg TaggedMessage) i mm) s' end (@PCM.join (@union_map_classPCM mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage))) (@um_pts mid (msg TaggedMessage) i mm) match @UMC.find mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage)) j s' with | Some m => @UMC.upd mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage)) j (@mark_msg TaggedMessage m) s' | None => s' end) *)
     - lab   - protocol Label
(* Goal: @eq soup (@UMC.upd mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage)) j (@mark_msg TaggedMessage mm) (@PCM.join (@union_map_classPCM mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage))) (@um_pts mid (msg TaggedMessage) i mm) s')) (@PCM.join (@union_map_classPCM mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage))) (@um_pts mid (msg TaggedMessage) i (@mark_msg TaggedMessage mm)) s') *)
(* Goal: @eq soup match @UMC.find mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage)) j s' with | Some m => @UMC.upd mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage)) j (@mark_msg TaggedMessage m) (@PCM.join (@union_map_classPCM mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage))) (@um_pts mid (msg TaggedMessage) i mm) s') | None => @PCM.join (@union_map_classPCM mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage))) (@um_pts mid (msg TaggedMessage) i mm) s' end (@PCM.join (@union_map_classPCM mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage))) (@um_pts mid (msg TaggedMessage) i mm) match @UMC.find mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage)) j s' with | Some m => @UMC.upd mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage)) j (@mark_msg TaggedMessage m) s' | None => s' end) *)
     - ptype - protocol, defining the content type
(* Goal: @eq soup (@UMC.upd mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage)) j (@mark_msg TaggedMessage mm) (@PCM.join (@union_map_classPCM mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage))) (@um_pts mid (msg TaggedMessage) i mm) s')) (@PCM.join (@union_map_classPCM mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage))) (@um_pts mid (msg TaggedMessage) i (@mark_msg TaggedMessage mm)) s') *)
(* Goal: @eq soup match @UMC.find mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage)) j s' with | Some m => @UMC.upd mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage)) j (@mark_msg TaggedMessage m) (@PCM.join (@union_map_classPCM mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage))) (@um_pts mid (msg TaggedMessage) i mm) s') | None => @PCM.join (@union_map_classPCM mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage))) (@um_pts mid (msg TaggedMessage) i mm) s' end (@PCM.join (@union_map_classPCM mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage))) (@um_pts mid (msg TaggedMessage) i mm) match @UMC.find mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage)) j s' with | Some m => @UMC.upd mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage)) j (@mark_msg TaggedMessage m) s' | None => s' end) *)
     - content  - the contents of the message
(* Goal: @eq soup (@UMC.upd mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage)) j (@mark_msg TaggedMessage mm) (@PCM.join (@union_map_classPCM mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage))) (@um_pts mid (msg TaggedMessage) i mm) s')) (@PCM.join (@union_map_classPCM mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage))) (@um_pts mid (msg TaggedMessage) i (@mark_msg TaggedMessage mm)) s') *)
(* Goal: @eq soup match @UMC.find mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage)) j s' with | Some m => @UMC.upd mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage)) j (@mark_msg TaggedMessage m) (@PCM.join (@union_map_classPCM mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage))) (@um_pts mid (msg TaggedMessage) i mm) s') | None => @PCM.join (@union_map_classPCM mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage))) (@um_pts mid (msg TaggedMessage) i mm) s' end (@PCM.join (@union_map_classPCM mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage))) (@um_pts mid (msg TaggedMessage) i mm) match @UMC.find mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage)) j s' with | Some m => @UMC.upd mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage)) j (@mark_msg TaggedMessage m) s' | None => s' end) *)
     - from/to  - IDs of the sender.receiver node
(* Goal: @eq soup (@UMC.upd mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage)) j (@mark_msg TaggedMessage mm) (@PCM.join (@union_map_classPCM mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage))) (@um_pts mid (msg TaggedMessage) i mm) s')) (@PCM.join (@union_map_classPCM mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage))) (@um_pts mid (msg TaggedMessage) i (@mark_msg TaggedMessage mm)) s') *)
(* Goal: @eq soup match @UMC.find mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage)) j s' with | Some m => @UMC.upd mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage)) j (@mark_msg TaggedMessage m) (@PCM.join (@union_map_classPCM mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage))) (@um_pts mid (msg TaggedMessage) i mm) s') | None => @PCM.join (@union_map_classPCM mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage))) (@um_pts mid (msg TaggedMessage) i mm) s' end (@PCM.join (@union_map_classPCM mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage))) (@um_pts mid (msg TaggedMessage) i mm) match @UMC.find mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage)) j s' with | Some m => @UMC.upd mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage)) j (@mark_msg TaggedMessage m) s' | None => s' end) *)
     - active - a bit, indicating whether the message hasn't been consumed yet (i.e., read)

     I'm not sure, if we're going to need anything else. *)
  Structure msg (mtype : Type) :=
    Msg {content  : mtype;
         from     : nat;
         to       : nat;
         active   : bool }.

  (* Message IDs: pairs Label * id, where Label comes from the protocol. *)
  Definition mid := [ordType of nat].

  (* Message soup (for a specific protocol) is just a partial finite
     map from message IDs (mid) to arbitrary Messages. *)
  Definition soup : Type :=
    union_map mid (msg (TaggedMessage)).

  Variables (s: soup) (V: valid s).

  (* Allocating new message in the soup *)
  Definition post_msg m : soup * mid :=
(* Goal: @eq soup (@UMC.upd mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage)) j (@mark_msg TaggedMessage mm) (@PCM.join (@union_map_classPCM mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage))) (@um_pts mid (msg TaggedMessage) i mm) s')) (@PCM.join (@union_map_classPCM mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage))) (@um_pts mid (msg TaggedMessage) i (@mark_msg TaggedMessage mm)) s') *)
(* Goal: @eq soup match @UMC.find mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage)) j s' with | Some m => @UMC.upd mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage)) j (@mark_msg TaggedMessage m) (@PCM.join (@union_map_classPCM mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage))) (@um_pts mid (msg TaggedMessage) i mm) s') | None => @PCM.join (@union_map_classPCM mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage))) (@um_pts mid (msg TaggedMessage) i mm) s' end (@PCM.join (@union_map_classPCM mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage))) (@um_pts mid (msg TaggedMessage) i mm) match @UMC.find mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage)) j s' with | Some m => @UMC.upd mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage)) j (@mark_msg TaggedMessage m) s' | None => s' end) *)
    let: f := fresh s in (s \+ f \\-> m, f).

  Lemma post_valid m :  valid (post_msg m).1.
(* Goal: @eq_mem (Equality.sort (Ordered.eqType (@Ordered.clone nid nat_ordType (Ordered.class nat_ordType) (fun x : phantom (Ordered.class_of (Ordered.sort nat_ordType)) (Ordered.class nat_ordType) => x)))) (@mem (Equality.sort (Ordered.eqType (@Ordered.clone nid nat_ordType (Ordered.class nat_ordType) (fun x : phantom (Ordered.class_of (Ordered.sort nat_ordType)) (Ordered.class nat_ordType) => x)))) (seq_predType (Ordered.eqType (@Ordered.clone nid nat_ordType (Ordered.class nat_ordType) (fun x : phantom (Ordered.class_of (Ordered.sort nat_ordType)) (Ordered.class nat_ordType) => x)))) (@UMC.dom (@Ordered.clone nid nat_ordType (Ordered.class nat_ordType) (fun x : phantom (Ordered.class_of (Ordered.sort nat_ordType)) (Ordered.class nat_ordType) => x)) Heap.heap (union_mapUMC (@Ordered.clone nid nat_ordType (Ordered.class nat_ordType) (fun x : phantom (Ordered.class_of (Ordered.sort nat_ordType)) (Ordered.class nat_ordType) => x)) Heap.heap) (dstate empty_dstatelet))) (@mem (Equality.sort (Ordered.eqType (@Ordered.clone nid nat_ordType (Ordered.class nat_ordType) (fun x : phantom (Ordered.class_of (Ordered.sort nat_ordType)) (Ordered.class nat_ordType) => x)))) (seq_predType (Ordered.eqType (@Ordered.clone nid nat_ordType (Ordered.class nat_ordType) (fun x : phantom (Ordered.class_of (Ordered.sort nat_ordType)) (Ordered.class nat_ordType) => x)))) (@Datatypes.nil (Equality.sort (Ordered.eqType (@Ordered.clone nid nat_ordType (Ordered.class nat_ordType) (fun x : phantom (Ordered.class_of (Ordered.sort nat_ordType)) (Ordered.class nat_ordType) => x)))))) *)
  Proof. by rewrite ?valid_fresh. Qed.

  Lemma post_fresh m : (post_msg m).2 \notin dom s.
  Proof. by rewrite ?dom_fresh. Qed.

  (* Marking is  *)
  Definition mark_msg T (m : msg T) : msg T :=
    Msg (content m) (from m) (to m) false.

  (* Updating the message soup, consuming the message id *)
  Definition consume_msg (s : soup) (id : mid) : soup :=
    let: mr := find id s in
    if mr is Some m then upd id (mark_msg m) s else s.

  Definition is_active (id : mid) :=
    exists m, find id s = Some m /\ active m.

  Definition is_consumed (id : mid) :=
    exists m, find id s = Some m /\ ~~ active m.

(* Goal: @eq soup (@UMC.upd mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage)) j (@mark_msg TaggedMessage mm) (@PCM.join (@union_map_classPCM mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage))) (@um_pts mid (msg TaggedMessage) i mm) s')) (@PCM.join (@union_map_classPCM mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage))) (@um_pts mid (msg TaggedMessage) i (@mark_msg TaggedMessage mm)) s') *)
(* Goal: @eq soup match @UMC.find mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage)) j s' with | Some m => @UMC.upd mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage)) j (@mark_msg TaggedMessage m) (@PCM.join (@union_map_classPCM mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage))) (@um_pts mid (msg TaggedMessage) i mm) s') | None => @PCM.join (@union_map_classPCM mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage))) (@um_pts mid (msg TaggedMessage) i mm) s' end (@PCM.join (@union_map_classPCM mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage))) (@um_pts mid (msg TaggedMessage) i mm) match @UMC.find mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage)) j s' with | Some m => @UMC.upd mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage)) j (@mark_msg TaggedMessage m) s' | None => s' end) *)
  (* TODO: consumes "truth table" -- three possible scenarios (how to express?) *)

  (* Obvious fact about marking message *)
  Lemma find_consume s' (id: mid) m:
(* Goal: @eq soup (@UMC.upd mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage)) j (@mark_msg TaggedMessage mm) (@PCM.join (@union_map_classPCM mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage))) (@um_pts mid (msg TaggedMessage) i mm) s')) (@PCM.join (@union_map_classPCM mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage))) (@um_pts mid (msg TaggedMessage) i (@mark_msg TaggedMessage mm)) s') *)
(* Goal: @eq soup match @UMC.find mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage)) j s' with | Some m => @UMC.upd mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage)) j (@mark_msg TaggedMessage m) (@PCM.join (@union_map_classPCM mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage))) (@um_pts mid (msg TaggedMessage) i mm) s') | None => @PCM.join (@union_map_classPCM mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage))) (@um_pts mid (msg TaggedMessage) i mm) s' end (@PCM.join (@union_map_classPCM mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage))) (@um_pts mid (msg TaggedMessage) i mm) match @UMC.find mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage)) j s' with | Some m => @UMC.upd mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage)) j (@mark_msg TaggedMessage m) s' | None => s' end) *)
    valid s' -> find id s' = Some m ->
    find id (consume_msg s' id) = Some (mark_msg m).
  Proof. by move=>V' E; rewrite/consume_msg E findU eqxx V'/=. Qed.

  Lemma find_mark m s' msg :
(* Goal: @eq soup (@UMC.upd mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage)) j (@mark_msg TaggedMessage mm) (@PCM.join (@union_map_classPCM mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage))) (@um_pts mid (msg TaggedMessage) i mm) s')) (@PCM.join (@union_map_classPCM mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage))) (@um_pts mid (msg TaggedMessage) i (@mark_msg TaggedMessage mm)) s') *)
(* Goal: @eq soup match @UMC.find mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage)) j s' with | Some m => @UMC.upd mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage)) j (@mark_msg TaggedMessage m) (@PCM.join (@union_map_classPCM mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage))) (@um_pts mid (msg TaggedMessage) i mm) s') | None => @PCM.join (@union_map_classPCM mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage))) (@um_pts mid (msg TaggedMessage) i mm) s' end (@PCM.join (@union_map_classPCM mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage))) (@um_pts mid (msg TaggedMessage) i mm) match @UMC.find mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage)) j s' with | Some m => @UMC.upd mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage)) j (@mark_msg TaggedMessage m) s' | None => s' end) *)
    valid s' -> find m (consume_msg s' m) = Some msg ->
    exists msg', find m s' = Some msg' /\ msg = mark_msg msg'.
  Proof.
(* Goal: forall (_ : is_true (@PCM.valid (union_mapPCM mid (msg TaggedMessage)) s')) (_ : @eq bool (@eq_op (Ordered.eqType mid) m' m) false), @eq (option (msg TaggedMessage)) (@UMC.find mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage)) m' (consume_msg s' m)) (@UMC.find mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage)) m' s') *)
  move=>V'; rewrite /consume_msg; case D: (m \in dom s').
(* Goal: @eq soup (@UMC.upd mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage)) j (@mark_msg TaggedMessage mm) (@PCM.join (@union_map_classPCM mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage))) (@um_pts mid (msg TaggedMessage) i mm) s')) (@PCM.join (@union_map_classPCM mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage))) (@um_pts mid (msg TaggedMessage) i (@mark_msg TaggedMessage mm)) s') *)
(* Goal: @eq soup match @UMC.find mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage)) j s' with | Some m => @UMC.upd mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage)) j (@mark_msg TaggedMessage m) (@PCM.join (@union_map_classPCM mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage))) (@um_pts mid (msg TaggedMessage) i mm) s') | None => @PCM.join (@union_map_classPCM mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage))) (@um_pts mid (msg TaggedMessage) i mm) s' end (@PCM.join (@union_map_classPCM mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage))) (@um_pts mid (msg TaggedMessage) i mm) match @UMC.find mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage)) j s' with | Some m => @UMC.upd mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage)) j (@mark_msg TaggedMessage m) s' | None => s' end) *)
  - move/um_eta: D=>[msg'][->]_; rewrite findU eqxx/= V'.
(* Goal: @eq soup (@UMC.upd mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage)) j (@mark_msg TaggedMessage mm) (@PCM.join (@union_map_classPCM mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage))) (@um_pts mid (msg TaggedMessage) i mm) s')) (@PCM.join (@union_map_classPCM mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage))) (@um_pts mid (msg TaggedMessage) i (@mark_msg TaggedMessage mm)) s') *)
(* Goal: @eq soup match @UMC.find mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage)) j s' with | Some m => @UMC.upd mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage)) j (@mark_msg TaggedMessage m) (@PCM.join (@union_map_classPCM mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage))) (@um_pts mid (msg TaggedMessage) i mm) s') | None => @PCM.join (@union_map_classPCM mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage))) (@um_pts mid (msg TaggedMessage) i mm) s' end (@PCM.join (@union_map_classPCM mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage))) (@um_pts mid (msg TaggedMessage) i mm) match @UMC.find mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage)) j s' with | Some m => @UMC.upd mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage)) j (@mark_msg TaggedMessage m) s' | None => s' end) *)
    by case=><-; eexists _.
(* Goal: @eq soup (@UMC.upd mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage)) j (@mark_msg TaggedMessage mm) (@PCM.join (@union_map_classPCM mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage))) (@um_pts mid (msg TaggedMessage) i mm) s')) (@PCM.join (@union_map_classPCM mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage))) (@um_pts mid (msg TaggedMessage) i (@mark_msg TaggedMessage mm)) s') *)
(* Goal: @eq soup match @UMC.find mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage)) j s' with | Some m => @UMC.upd mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage)) j (@mark_msg TaggedMessage m) (@PCM.join (@union_map_classPCM mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage))) (@um_pts mid (msg TaggedMessage) i mm) s') | None => @PCM.join (@union_map_classPCM mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage))) (@um_pts mid (msg TaggedMessage) i mm) s' end (@PCM.join (@union_map_classPCM mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage))) (@um_pts mid (msg TaggedMessage) i mm) match @UMC.find mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage)) j s' with | Some m => @UMC.upd mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage)) j (@mark_msg TaggedMessage m) s' | None => s' end) *)
  by case: dom_find (D)=>//->_; move/find_some=>Z; rewrite Z in D.
  Qed.   

  Lemma mark_other m m' s' :
(* Goal: @eq soup (@UMC.upd mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage)) j (@mark_msg TaggedMessage mm) (@PCM.join (@union_map_classPCM mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage))) (@um_pts mid (msg TaggedMessage) i mm) s')) (@PCM.join (@union_map_classPCM mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage))) (@um_pts mid (msg TaggedMessage) i (@mark_msg TaggedMessage mm)) s') *)
(* Goal: @eq soup match @UMC.find mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage)) j s' with | Some m => @UMC.upd mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage)) j (@mark_msg TaggedMessage m) (@PCM.join (@union_map_classPCM mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage))) (@um_pts mid (msg TaggedMessage) i mm) s') | None => @PCM.join (@union_map_classPCM mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage))) (@um_pts mid (msg TaggedMessage) i mm) s' end (@PCM.join (@union_map_classPCM mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage))) (@um_pts mid (msg TaggedMessage) i mm) match @UMC.find mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage)) j s' with | Some m => @UMC.upd mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage)) j (@mark_msg TaggedMessage m) s' | None => s' end) *)
    valid s' -> m' == m = false -> find m' (consume_msg s' m) = find m' s'.
  Proof.
(* Goal: forall (_ : is_true (@PCM.valid (union_mapPCM mid (msg TaggedMessage)) s')) (_ : @eq bool (@eq_op (Ordered.eqType mid) m' m) false), @eq (option (msg TaggedMessage)) (@UMC.find mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage)) m' (consume_msg s' m)) (@UMC.find mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage)) m' s') *)
  move=>V' N; rewrite /consume_msg; case D: (m \in dom s').
(* Goal: @eq soup (@UMC.upd mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage)) j (@mark_msg TaggedMessage mm) (@PCM.join (@union_map_classPCM mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage))) (@um_pts mid (msg TaggedMessage) i mm) s')) (@PCM.join (@union_map_classPCM mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage))) (@um_pts mid (msg TaggedMessage) i (@mark_msg TaggedMessage mm)) s') *)
(* Goal: @eq soup match @UMC.find mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage)) j s' with | Some m => @UMC.upd mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage)) j (@mark_msg TaggedMessage m) (@PCM.join (@union_map_classPCM mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage))) (@um_pts mid (msg TaggedMessage) i mm) s') | None => @PCM.join (@union_map_classPCM mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage))) (@um_pts mid (msg TaggedMessage) i mm) s' end (@PCM.join (@union_map_classPCM mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage))) (@um_pts mid (msg TaggedMessage) i mm) match @UMC.find mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage)) j s' with | Some m => @UMC.upd mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage)) j (@mark_msg TaggedMessage m) s' | None => s' end) *)
  by case: dom_find (D)=>//v->_ _; rewrite findU N.
(* Goal: @eq soup (@UMC.upd mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage)) j (@mark_msg TaggedMessage mm) (@PCM.join (@union_map_classPCM mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage))) (@um_pts mid (msg TaggedMessage) i mm) s')) (@PCM.join (@union_map_classPCM mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage))) (@um_pts mid (msg TaggedMessage) i (@mark_msg TaggedMessage mm)) s') *)
(* Goal: @eq soup match @UMC.find mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage)) j s' with | Some m => @UMC.upd mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage)) j (@mark_msg TaggedMessage m) (@PCM.join (@union_map_classPCM mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage))) (@um_pts mid (msg TaggedMessage) i mm) s') | None => @PCM.join (@union_map_classPCM mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage))) (@um_pts mid (msg TaggedMessage) i mm) s' end (@PCM.join (@union_map_classPCM mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage))) (@um_pts mid (msg TaggedMessage) i mm) match @UMC.find mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage)) j s' with | Some m => @UMC.upd mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage)) j (@mark_msg TaggedMessage m) s' | None => s' end) *)
  by case: dom_find (D)=>//->_.
  Qed.   

(* Goal: @eq soup (@UMC.upd mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage)) j (@mark_msg TaggedMessage mm) (@PCM.join (@union_map_classPCM mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage))) (@um_pts mid (msg TaggedMessage) i mm) s')) (@PCM.join (@union_map_classPCM mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage))) (@um_pts mid (msg TaggedMessage) i (@mark_msg TaggedMessage mm)) s') *)
(* Goal: @eq soup match @UMC.find mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage)) j s' with | Some m => @UMC.upd mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage)) j (@mark_msg TaggedMessage m) (@PCM.join (@union_map_classPCM mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage))) (@um_pts mid (msg TaggedMessage) i mm) s') | None => @PCM.join (@union_map_classPCM mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage))) (@um_pts mid (msg TaggedMessage) i mm) s' end (@PCM.join (@union_map_classPCM mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage))) (@um_pts mid (msg TaggedMessage) i mm) match @UMC.find mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage)) j s' with | Some m => @UMC.upd mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage)) j (@mark_msg TaggedMessage m) s' | None => s' end) *)
  Lemma consume_valid s' m : valid s' -> valid (consume_msg s' m).
  Proof.
(* Goal: forall _ : is_true (@PCM.valid (union_mapPCM mid (msg TaggedMessage)) s'), is_true (@PCM.valid (union_mapPCM mid (msg TaggedMessage)) (consume_msg s' m)) *)
  move=>V'; rewrite /consume_msg; case (find m s')=>//v.
(* Goal: @eq_mem (Equality.sort (Ordered.eqType (@Ordered.clone nid nat_ordType (Ordered.class nat_ordType) (fun x : phantom (Ordered.class_of (Ordered.sort nat_ordType)) (Ordered.class nat_ordType) => x)))) (@mem (Equality.sort (Ordered.eqType (@Ordered.clone nid nat_ordType (Ordered.class nat_ordType) (fun x : phantom (Ordered.class_of (Ordered.sort nat_ordType)) (Ordered.class nat_ordType) => x)))) (seq_predType (Ordered.eqType (@Ordered.clone nid nat_ordType (Ordered.class nat_ordType) (fun x : phantom (Ordered.class_of (Ordered.sort nat_ordType)) (Ordered.class nat_ordType) => x)))) (@UMC.dom (@Ordered.clone nid nat_ordType (Ordered.class nat_ordType) (fun x : phantom (Ordered.class_of (Ordered.sort nat_ordType)) (Ordered.class nat_ordType) => x)) Heap.heap (union_mapUMC (@Ordered.clone nid nat_ordType (Ordered.class nat_ordType) (fun x : phantom (Ordered.class_of (Ordered.sort nat_ordType)) (Ordered.class nat_ordType) => x)) Heap.heap) (dstate empty_dstatelet))) (@mem (Equality.sort (Ordered.eqType (@Ordered.clone nid nat_ordType (Ordered.class nat_ordType) (fun x : phantom (Ordered.class_of (Ordered.sort nat_ordType)) (Ordered.class nat_ordType) => x)))) (seq_predType (Ordered.eqType (@Ordered.clone nid nat_ordType (Ordered.class nat_ordType) (fun x : phantom (Ordered.class_of (Ordered.sort nat_ordType)) (Ordered.class nat_ordType) => x)))) (@Datatypes.nil (Equality.sort (Ordered.eqType (@Ordered.clone nid nat_ordType (Ordered.class nat_ordType) (fun x : phantom (Ordered.class_of (Ordered.sort nat_ordType)) (Ordered.class nat_ordType) => x)))))) *)
  by rewrite /mark_msg validU.
  Qed.

  Lemma consumeUn (s': soup) (i : mid) mm
(* Goal: @eq soup (@UMC.upd mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage)) j (@mark_msg TaggedMessage mm) (@PCM.join (@union_map_classPCM mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage))) (@um_pts mid (msg TaggedMessage) i mm) s')) (@PCM.join (@union_map_classPCM mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage))) (@um_pts mid (msg TaggedMessage) i (@mark_msg TaggedMessage mm)) s') *)
(* Goal: @eq soup match @UMC.find mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage)) j s' with | Some m => @UMC.upd mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage)) j (@mark_msg TaggedMessage m) (@PCM.join (@union_map_classPCM mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage))) (@um_pts mid (msg TaggedMessage) i mm) s') | None => @PCM.join (@union_map_classPCM mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage))) (@um_pts mid (msg TaggedMessage) i mm) s' end (@PCM.join (@union_map_classPCM mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage))) (@um_pts mid (msg TaggedMessage) i mm) match @UMC.find mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage)) j s' with | Some m => @UMC.upd mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage)) j (@mark_msg TaggedMessage m) s' | None => s' end) *)
        (j : mid) : valid (s' \+ i \\-> mm) ->
(* Goal: @eq soup (@UMC.upd mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage)) j (@mark_msg TaggedMessage mm) (@PCM.join (@union_map_classPCM mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage))) (@um_pts mid (msg TaggedMessage) i mm) s')) (@PCM.join (@union_map_classPCM mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage))) (@um_pts mid (msg TaggedMessage) i (@mark_msg TaggedMessage mm)) s') *)
(* Goal: @eq soup match @UMC.find mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage)) j s' with | Some m => @UMC.upd mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage)) j (@mark_msg TaggedMessage m) (@PCM.join (@union_map_classPCM mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage))) (@um_pts mid (msg TaggedMessage) i mm) s') | None => @PCM.join (@union_map_classPCM mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage))) (@um_pts mid (msg TaggedMessage) i mm) s' end (@PCM.join (@union_map_classPCM mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage))) (@um_pts mid (msg TaggedMessage) i mm) match @UMC.find mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage)) j s' with | Some m => @UMC.upd mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage)) j (@mark_msg TaggedMessage m) s' | None => s' end) *)
    consume_msg (s' \+ i \\-> mm) j = 
(* Goal: @eq soup (@UMC.upd mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage)) j (@mark_msg TaggedMessage mm) (@PCM.join (@union_map_classPCM mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage))) (@um_pts mid (msg TaggedMessage) i mm) s')) (@PCM.join (@union_map_classPCM mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage))) (@um_pts mid (msg TaggedMessage) i (@mark_msg TaggedMessage mm)) s') *)
(* Goal: @eq soup match @UMC.find mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage)) j s' with | Some m => @UMC.upd mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage)) j (@mark_msg TaggedMessage m) (@PCM.join (@union_map_classPCM mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage))) (@um_pts mid (msg TaggedMessage) i mm) s') | None => @PCM.join (@union_map_classPCM mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage))) (@um_pts mid (msg TaggedMessage) i mm) s' end (@PCM.join (@union_map_classPCM mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage))) (@um_pts mid (msg TaggedMessage) i mm) match @UMC.find mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage)) j s' with | Some m => @UMC.upd mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage)) j (@mark_msg TaggedMessage m) s' | None => s' end) *)
    if i == j then s' \+ i \\-> mark_msg mm
(* Goal: @eq soup (@UMC.upd mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage)) j (@mark_msg TaggedMessage mm) (@PCM.join (@union_map_classPCM mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage))) (@um_pts mid (msg TaggedMessage) i mm) s')) (@PCM.join (@union_map_classPCM mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage))) (@um_pts mid (msg TaggedMessage) i (@mark_msg TaggedMessage mm)) s') *)
(* Goal: @eq soup match @UMC.find mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage)) j s' with | Some m => @UMC.upd mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage)) j (@mark_msg TaggedMessage m) (@PCM.join (@union_map_classPCM mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage))) (@um_pts mid (msg TaggedMessage) i mm) s') | None => @PCM.join (@union_map_classPCM mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage))) (@um_pts mid (msg TaggedMessage) i mm) s' end (@PCM.join (@union_map_classPCM mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage))) (@um_pts mid (msg TaggedMessage) i mm) match @UMC.find mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage)) j s' with | Some m => @UMC.upd mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage)) j (@mark_msg TaggedMessage m) s' | None => s' end) *)
    else (consume_msg s' j) \+ (i \\-> mm).
  Proof.
(* Goal: @eq soup (@UMC.upd mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage)) j (@mark_msg TaggedMessage mm) (@PCM.join (@union_map_classPCM mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage))) (@um_pts mid (msg TaggedMessage) i mm) s')) (@PCM.join (@union_map_classPCM mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage))) (@um_pts mid (msg TaggedMessage) i (@mark_msg TaggedMessage mm)) s') *)
(* Goal: @eq soup match @UMC.find mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage)) j s' with | Some m => @UMC.upd mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage)) j (@mark_msg TaggedMessage m) (@PCM.join (@union_map_classPCM mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage))) (@um_pts mid (msg TaggedMessage) i mm) s') | None => @PCM.join (@union_map_classPCM mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage))) (@um_pts mid (msg TaggedMessage) i mm) s' end (@PCM.join (@union_map_classPCM mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage))) (@um_pts mid (msg TaggedMessage) i mm) match @UMC.find mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage)) j s' with | Some m => @UMC.upd mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage)) j (@mark_msg TaggedMessage m) s' | None => s' end) *)
  rewrite ![_ \+ i \\-> _]joinC; rewrite eq_sym.
(* Goal: forall _ : is_true (@PCM.valid (union_mapPCM mid (msg TaggedMessage)) (@PCM.join (@union_map_classPCM mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage))) (@um_pts mid (msg TaggedMessage) i mm) s')), @eq soup (consume_msg (@PCM.join (@union_map_classPCM mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage))) (@um_pts mid (msg TaggedMessage) i mm) s') j) (if @eq_op (Ordered.eqType mid) j i then @PCM.join (@union_map_classPCM mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage))) (@um_pts mid (msg TaggedMessage) i (@mark_msg TaggedMessage mm)) s' else @PCM.join (@union_map_classPCM mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage))) (@um_pts mid (msg TaggedMessage) i mm) (consume_msg s' j)) *)
  move=>V'; case B: (j==i); rewrite /consume_msg findPtUn2// B.
(* Goal: @eq soup (@UMC.upd mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage)) j (@mark_msg TaggedMessage mm) (@PCM.join (@union_map_classPCM mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage))) (@um_pts mid (msg TaggedMessage) i mm) s')) (@PCM.join (@union_map_classPCM mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage))) (@um_pts mid (msg TaggedMessage) i (@mark_msg TaggedMessage mm)) s') *)
(* Goal: @eq soup match @UMC.find mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage)) j s' with | Some m => @UMC.upd mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage)) j (@mark_msg TaggedMessage m) (@PCM.join (@union_map_classPCM mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage))) (@um_pts mid (msg TaggedMessage) i mm) s') | None => @PCM.join (@union_map_classPCM mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage))) (@um_pts mid (msg TaggedMessage) i mm) s' end (@PCM.join (@union_map_classPCM mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage))) (@um_pts mid (msg TaggedMessage) i mm) match @UMC.find mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage)) j s' with | Some m => @UMC.upd mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage)) j (@mark_msg TaggedMessage m) s' | None => s' end) *)
  - by move/eqP: B=>?; subst j; rewrite updPtUn.
(* Goal: @eq_mem (Equality.sort (Ordered.eqType (@Ordered.clone nid nat_ordType (Ordered.class nat_ordType) (fun x : phantom (Ordered.class_of (Ordered.sort nat_ordType)) (Ordered.class nat_ordType) => x)))) (@mem (Equality.sort (Ordered.eqType (@Ordered.clone nid nat_ordType (Ordered.class nat_ordType) (fun x : phantom (Ordered.class_of (Ordered.sort nat_ordType)) (Ordered.class nat_ordType) => x)))) (seq_predType (Ordered.eqType (@Ordered.clone nid nat_ordType (Ordered.class nat_ordType) (fun x : phantom (Ordered.class_of (Ordered.sort nat_ordType)) (Ordered.class nat_ordType) => x)))) (@UMC.dom (@Ordered.clone nid nat_ordType (Ordered.class nat_ordType) (fun x : phantom (Ordered.class_of (Ordered.sort nat_ordType)) (Ordered.class nat_ordType) => x)) Heap.heap (union_mapUMC (@Ordered.clone nid nat_ordType (Ordered.class nat_ordType) (fun x : phantom (Ordered.class_of (Ordered.sort nat_ordType)) (Ordered.class nat_ordType) => x)) Heap.heap) (dstate empty_dstatelet))) (@mem (Equality.sort (Ordered.eqType (@Ordered.clone nid nat_ordType (Ordered.class nat_ordType) (fun x : phantom (Ordered.class_of (Ordered.sort nat_ordType)) (Ordered.class nat_ordType) => x)))) (seq_predType (Ordered.eqType (@Ordered.clone nid nat_ordType (Ordered.class nat_ordType) (fun x : phantom (Ordered.class_of (Ordered.sort nat_ordType)) (Ordered.class nat_ordType) => x)))) (@Datatypes.nil (Equality.sort (Ordered.eqType (@Ordered.clone nid nat_ordType (Ordered.class nat_ordType) (fun x : phantom (Ordered.class_of (Ordered.sort nat_ordType)) (Ordered.class nat_ordType) => x)))))) *)
  by case X: (find j s')=>//; rewrite updUnL domPt inE eq_sym B.   
  Qed.

  Notation "'{{' m 'in' s 'at' id '}}'" := (find id s = Some m).
  Notation "'{{' m 'in' s '}}'" := (exists id, {{m in s at id}}).


  
End Shared.

(* Goal: @eq soup (@UMC.upd mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage)) j (@mark_msg TaggedMessage mm) (@PCM.join (@union_map_classPCM mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage))) (@um_pts mid (msg TaggedMessage) i mm) s')) (@PCM.join (@union_map_classPCM mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage))) (@um_pts mid (msg TaggedMessage) i (@mark_msg TaggedMessage mm)) s') *)
(* Goal: @eq soup match @UMC.find mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage)) j s' with | Some m => @UMC.upd mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage)) j (@mark_msg TaggedMessage m) (@PCM.join (@union_map_classPCM mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage))) (@um_pts mid (msg TaggedMessage) i mm) s') | None => @PCM.join (@union_map_classPCM mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage))) (@um_pts mid (msg TaggedMessage) i mm) s' end (@PCM.join (@union_map_classPCM mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage))) (@um_pts mid (msg TaggedMessage) i mm) match @UMC.find mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage)) j s' with | Some m => @UMC.upd mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage)) j (@mark_msg TaggedMessage m) s' | None => s' end) *)
(* Local per-protocol state with per-node resources *)
Section Local.

  Variable U : Type.

  Definition nid := nat.

  (* Local state of a a protocol is simply a partial map from node ids
     to their local contributions, along with the validity of the
     cumulative contribution. *)

  Definition lstate_type := union_map [ordType of nid] U.

End Local.

(*
(* Goal: @eq soup (@UMC.upd mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage)) j (@mark_msg TaggedMessage mm) (@PCM.join (@union_map_classPCM mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage))) (@um_pts mid (msg TaggedMessage) i mm) s')) (@PCM.join (@union_map_classPCM mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage))) (@um_pts mid (msg TaggedMessage) i (@mark_msg TaggedMessage mm)) s') *)
(* Goal: @eq soup match @UMC.find mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage)) j s' with | Some m => @UMC.upd mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage)) j (@mark_msg TaggedMessage m) (@PCM.join (@union_map_classPCM mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage))) (@um_pts mid (msg TaggedMessage) i mm) s') | None => @PCM.join (@union_map_classPCM mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage))) (@um_pts mid (msg TaggedMessage) i mm) s' end (@PCM.join (@union_map_classPCM mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage))) (@um_pts mid (msg TaggedMessage) i mm) match @UMC.find mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage)) j s' with | Some m => @UMC.upd mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage)) j (@mark_msg TaggedMessage m) s' | None => s' end) *)
Definition um_all {A:ordType} {B} (p : A -> B -> bool) (u : union_map A B) : bool :=
  um_recf false true (fun k v f rec Hval Hpath => p k v && rec) u.

(* Goal: @eq soup (@UMC.upd mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage)) j (@mark_msg TaggedMessage mm) (@PCM.join (@union_map_classPCM mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage))) (@um_pts mid (msg TaggedMessage) i mm) s')) (@PCM.join (@union_map_classPCM mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage))) (@um_pts mid (msg TaggedMessage) i (@mark_msg TaggedMessage mm)) s') *)
(* Goal: @eq soup match @UMC.find mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage)) j s' with | Some m => @UMC.upd mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage)) j (@mark_msg TaggedMessage m) (@PCM.join (@union_map_classPCM mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage))) (@um_pts mid (msg TaggedMessage) i mm) s') | None => @PCM.join (@union_map_classPCM mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage))) (@um_pts mid (msg TaggedMessage) i mm) s' end (@PCM.join (@union_map_classPCM mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage))) (@um_pts mid (msg TaggedMessage) i mm) match @UMC.find mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage)) j s' with | Some m => @UMC.upd mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage)) j (@mark_msg TaggedMessage m) s' | None => s' end) *)
Definition um_some {A:ordType} {B} (p : A -> B -> bool) (u : union_map A B) : bool :=
  um_recf false false (fun k v f rec Hval Hpath => p k v || rec) u.
*)

Section Statelets.

  (* A particular statelet instance.
     The Label and the PCM are the parameters and are defined by the protocol.
     The lstate and dsop are subject of the evolution.
   *)
  Structure dstatelet  :=
    DStatelet {
        (* Not sure if it's the best way to represent information
           about kinds of messages in this particular dstatelet, but
           let's think of tags as of integers for now, so dTagToCont
           will map the tags to specific types. *)

        (* Local state for each node as a pair of heaps; first heap is
           real, second heap is a ghost one. Let's deal with this
           model for now before we figure out how to discharge
           equalities in a better way *)
        dstate     : lstate_type heap;
        dsoup      : soup
    }.

  Fixpoint empty_lstate (ns : seq nid) :=
    if ns is n :: ns'
(* Goal: @eq soup (@UMC.upd mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage)) j (@mark_msg TaggedMessage mm) (@PCM.join (@union_map_classPCM mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage))) (@um_pts mid (msg TaggedMessage) i mm) s')) (@PCM.join (@union_map_classPCM mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage))) (@um_pts mid (msg TaggedMessage) i (@mark_msg TaggedMessage mm)) s') *)
(* Goal: @eq soup match @UMC.find mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage)) j s' with | Some m => @UMC.upd mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage)) j (@mark_msg TaggedMessage m) (@PCM.join (@union_map_classPCM mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage))) (@um_pts mid (msg TaggedMessage) i mm) s') | None => @PCM.join (@union_map_classPCM mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage))) (@um_pts mid (msg TaggedMessage) i mm) s' end (@PCM.join (@union_map_classPCM mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage))) (@um_pts mid (msg TaggedMessage) i mm) match @UMC.find mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage)) j s' with | Some m => @UMC.upd mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage)) j (@mark_msg TaggedMessage m) s' | None => s' end) *)
    then n \\-> Heap.empty \+ (empty_lstate ns')
    else  Unit.
    
  (* Definition empty_dstatelet ns : dstatelet := *)
  (*   @DStatelet (empty_lstate (undup ns)) Unit. *)

  (* Lemma valid_mt_soup ns : valid (dsoup (empty_dstatelet ns)). *)
  (* Proof. by rewrite /= valid_unit. Qed. *)

  (* Lemma dom_mt ns : *)
  (*   valid (empty_lstate (undup ns)) /\ dom (empty_lstate (undup ns)) =i undup ns. *)
  (* Proof. *)
(* Goal: @eq_mem (Equality.sort (Ordered.eqType (@Ordered.clone nid nat_ordType (Ordered.class nat_ordType) (fun x : phantom (Ordered.class_of (Ordered.sort nat_ordType)) (Ordered.class nat_ordType) => x)))) (@mem (Equality.sort (Ordered.eqType (@Ordered.clone nid nat_ordType (Ordered.class nat_ordType) (fun x : phantom (Ordered.class_of (Ordered.sort nat_ordType)) (Ordered.class nat_ordType) => x)))) (seq_predType (Ordered.eqType (@Ordered.clone nid nat_ordType (Ordered.class nat_ordType) (fun x : phantom (Ordered.class_of (Ordered.sort nat_ordType)) (Ordered.class nat_ordType) => x)))) (@UMC.dom (@Ordered.clone nid nat_ordType (Ordered.class nat_ordType) (fun x : phantom (Ordered.class_of (Ordered.sort nat_ordType)) (Ordered.class nat_ordType) => x)) Heap.heap (union_mapUMC (@Ordered.clone nid nat_ordType (Ordered.class nat_ordType) (fun x : phantom (Ordered.class_of (Ordered.sort nat_ordType)) (Ordered.class nat_ordType) => x)) Heap.heap) (dstate empty_dstatelet))) (@mem (Equality.sort (Ordered.eqType (@Ordered.clone nid nat_ordType (Ordered.class nat_ordType) (fun x : phantom (Ordered.class_of (Ordered.sort nat_ordType)) (Ordered.class nat_ordType) => x)))) (seq_predType (Ordered.eqType (@Ordered.clone nid nat_ordType (Ordered.class nat_ordType) (fun x : phantom (Ordered.class_of (Ordered.sort nat_ordType)) (Ordered.class nat_ordType) => x)))) (@Datatypes.nil (Equality.sort (Ordered.eqType (@Ordered.clone nid nat_ordType (Ordered.class nat_ordType) (fun x : phantom (Ordered.class_of (Ordered.sort nat_ordType)) (Ordered.class nat_ordType) => x)))))) *)
  (* elim: ns=>//=[|n ns [H1 H2]]; first by rewrite dom0. *)
  (* case B: (n \in ns)=>//=; split. *)
(* Goal: @eq soup (@UMC.upd mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage)) j (@mark_msg TaggedMessage mm) (@PCM.join (@union_map_classPCM mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage))) (@um_pts mid (msg TaggedMessage) i mm) s')) (@PCM.join (@union_map_classPCM mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage))) (@um_pts mid (msg TaggedMessage) i (@mark_msg TaggedMessage mm)) s') *)
(* Goal: @eq soup match @UMC.find mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage)) j s' with | Some m => @UMC.upd mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage)) j (@mark_msg TaggedMessage m) (@PCM.join (@union_map_classPCM mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage))) (@um_pts mid (msg TaggedMessage) i mm) s') | None => @PCM.join (@union_map_classPCM mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage))) (@um_pts mid (msg TaggedMessage) i mm) s' end (@PCM.join (@union_map_classPCM mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage))) (@um_pts mid (msg TaggedMessage) i mm) match @UMC.find mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage)) j s' with | Some m => @UMC.upd mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage)) j (@mark_msg TaggedMessage m) s' | None => s' end) *)
  (* - by rewrite gen_validPtUn/= H1 H2/=; apply/negbT; rewrite mem_undup. *)
  (* move=> z; rewrite um_domPtUn inE/= gen_validPtUn/= H1 H2/=. *)
(* Goal: @eq soup (@UMC.upd mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage)) j (@mark_msg TaggedMessage mm) (@PCM.join (@union_map_classPCM mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage))) (@um_pts mid (msg TaggedMessage) i mm) s')) (@PCM.join (@union_map_classPCM mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage))) (@um_pts mid (msg TaggedMessage) i (@mark_msg TaggedMessage mm)) s') *)
(* Goal: @eq soup match @UMC.find mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage)) j s' with | Some m => @UMC.upd mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage)) j (@mark_msg TaggedMessage m) (@PCM.join (@union_map_classPCM mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage))) (@um_pts mid (msg TaggedMessage) i mm) s') | None => @PCM.join (@union_map_classPCM mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage))) (@um_pts mid (msg TaggedMessage) i mm) s' end (@PCM.join (@union_map_classPCM mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage))) (@um_pts mid (msg TaggedMessage) i mm) match @UMC.find mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage)) j s' with | Some m => @UMC.upd mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage)) j (@mark_msg TaggedMessage m) s' | None => s' end) *)
  (* rewrite -mem_undup in B; rewrite B/=. *)
  (* case C: (n == z)=>//=; first by rewrite in_cons eq_sym C. *)
  (* by rewrite H2 in_cons eq_sym C/=. *)
  (* Qed. *)

  (* Lemma valid_mt_state ns : valid (dstate (empty_dstatelet ns)). *)
  (* Proof. *)
  (* elim:ns=>//=n ns H; case I: (n \in ns)=>//=.   *)
(* Goal: @eq soup (@UMC.upd mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage)) j (@mark_msg TaggedMessage mm) (@PCM.join (@union_map_classPCM mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage))) (@um_pts mid (msg TaggedMessage) i mm) s')) (@PCM.join (@union_map_classPCM mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage))) (@um_pts mid (msg TaggedMessage) i (@mark_msg TaggedMessage mm)) s') *)
(* Goal: @eq soup match @UMC.find mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage)) j s' with | Some m => @UMC.upd mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage)) j (@mark_msg TaggedMessage m) (@PCM.join (@union_map_classPCM mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage))) (@um_pts mid (msg TaggedMessage) i mm) s') | None => @PCM.join (@union_map_classPCM mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage))) (@um_pts mid (msg TaggedMessage) i mm) s' end (@PCM.join (@union_map_classPCM mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage))) (@um_pts mid (msg TaggedMessage) i mm) match @UMC.find mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage)) j s' with | Some m => @UMC.upd mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage)) j (@mark_msg TaggedMessage m) s' | None => s' end) *)
  (* by rewrite gen_validPtUn H/=; case: (dom_mt ns)=>_->; rewrite mem_undup I. *)
  (* Qed. *)

  (* Lemma mt_nodes ns : dom (dstate (empty_dstatelet ns)) =i ns. *)
  (* Proof. *)
(* Goal: @eq soup (@UMC.upd mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage)) j (@mark_msg TaggedMessage mm) (@PCM.join (@union_map_classPCM mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage))) (@um_pts mid (msg TaggedMessage) i mm) s')) (@PCM.join (@union_map_classPCM mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage))) (@um_pts mid (msg TaggedMessage) i (@mark_msg TaggedMessage mm)) s') *)
(* Goal: @eq soup match @UMC.find mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage)) j s' with | Some m => @UMC.upd mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage)) j (@mark_msg TaggedMessage m) (@PCM.join (@union_map_classPCM mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage))) (@um_pts mid (msg TaggedMessage) i mm) s') | None => @PCM.join (@union_map_classPCM mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage))) (@um_pts mid (msg TaggedMessage) i mm) s' end (@PCM.join (@union_map_classPCM mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage))) (@um_pts mid (msg TaggedMessage) i mm) match @UMC.find mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage)) j s' with | Some m => @UMC.upd mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage)) j (@mark_msg TaggedMessage m) s' | None => s' end) *)
  (* by case: (dom_mt ns)=>_ H2 z; rewrite -mem_undup -H2. *)
  (* Qed. *)

  Definition empty_dstatelet : dstatelet :=
    @DStatelet (empty_lstate [::]) Unit.

  Lemma valid_mt_soup : valid (dsoup empty_dstatelet).
  Proof. by rewrite /= valid_unit. Qed.

  Lemma valid_mt_state  : valid (dstate empty_dstatelet).
  Proof. by rewrite valid_unit. Qed.

  Lemma mt_nodes : dom (dstate empty_dstatelet) =i [::].
  Proof. by rewrite dom0. Qed.

End Statelets.


Module StateGetters.
Section StateGetters.

Definition state := union_map Label dstatelet.

(* Retrieve statelet from the state *)
Definition getStatelet (s: state) (i : Label) : dstatelet :=
  match find i s with
  | Some d => d
  | None => empty_dstatelet
  end.

End StateGetters.
End StateGetters.


Export StateGetters.
