Merge pull request #12 from clayrat/pcm-1.3

updates for fcsl-pcm 1.3

Author: palmskog

.travis.yml

@@ -37,11 +37,6 @@ jobs:
   include:
 
   # Test supported versions of Coq via OPAM
-  - env:
-    - COQ_IMAGE=coqorg/coq:8.10
-    - PACKAGE=coq-disel.dev
-    - NJOBS=2
-    <<: *OPAM
   - env:
     - COQ_IMAGE=coqorg/coq:8.11
     - PACKAGE=coq-disel.dev

Core/Actions.v

@@ -58,7 +58,7 @@ Structure action (V : Type) (this : nid)
          (* step_frame : forall s1 s2 r z, *)
          (*     a_lab != z -> Coh W s1 -> *)
          (*     a_safe s1 -> a_step s1 s2 r -> getS s1 z  = getS s2 z; *)
-         
+
          (* Action step semantics respects the overall network semantics *)
          step_sem  : forall s1 (pf : a_safe s1) s2 r,
              a_step pf s2 r -> network_step W this s1 s2
@@ -126,9 +126,9 @@ Notation getP l := (getProtocol W l).
 Notation getS s l := (getStatelet s l).
 Variable this : nid.
 
-(* 
+(*
 
-Filter for specific 
+Filter for specific
  - protocol labels
  - message tags
  - message bodies
@@ -152,13 +152,13 @@ Definition tryrecv_act_step s1 s2 (r : option (nid * nat * seq nat)) :=
   exists (pf : s1 \In Coh W),
   (* No message to receive -- all relevant messages are marked *)
     ([/\ (forall l m tms from rt b,
-          this \in nodes (getP l) (getS s1 l) -> 
+          this \in nodes (getP l) (getS s1 l) ->
           Some (Msg tms from this b) = find m (dsoup (getS s1 l)) ->
           rt \In (rcv_trans (getP l)) ->
           tag tms = (t_rcv rt) ->
           (* This is required for safety *)
           msg_wf rt (coh_s l pf) this from tms ->
-          (* The filter applies *)   
+          (* The filter applies *)
           filter l from (t_rcv rt) (tms_cont tms) ->
           ~~b),
     r = None & s2 = s1] \/
@@ -170,7 +170,7 @@ Definition tryrecv_act_step s1 s2 (r : option (nid * nat * seq nat)) :=
           tag tms = (t_rcv rt),
           (* This is required for safety *)
           msg_wf rt (coh_s l pf) this from tms &
-          (* The filter applies *)   
+          (* The filter applies *)
           filter l from (t_rcv rt) (tms_cont tms)],
       let loc' := receive_step rt from tms (coh_s l pf) pf' in
       let: f' := upd this loc' (dstate d) in
@@ -200,7 +200,7 @@ exists (let: d :=  getS s l in
         let: f' := upd this loc' (dstate d) in
         let: s' := consume_msg (dsoup d) m in
         upd l (DStatelet f' s') s), (Some (from, tag tms, tms_cont tms)).
-by exists C; right; exists l, m, tms, from, rt, T. 
+by exists C; right; exists l, m, tms, from, rt, T.
 Qed.
 
 Lemma tryrecv_act_step_safe s1 s2 r:
@@ -250,11 +250,11 @@ Definition can_send (s : state) := (l \in dom s) && (this \in nodes p (getS s l)
 (* Take only the hooks that affect the transition with a tag st of *)
 (* protocol l *)
 Definition filter_hooks (h : hooks) :=
-  um_filter (fun e => e.2 == (l, t_snd st)) h.
+  um_filterk (fun e => e.2 == (l, t_snd st)) h.
 
 Definition send_act_safe s :=
   [/\ Coh W s, send_safe st this to (getS s l) msg, can_send s &
-      (* All hooks from a "reduced footprint" are applicable *)         
+      (* All hooks from a "reduced footprint" are applicable *)
       all_hooks_fire (filter_hooks (geth W)) l (t_snd st) s this msg to].
 
 Lemma send_act_safe_coh s : send_act_safe s -> Coh W s.
@@ -297,7 +297,7 @@ rewrite /all_hooks_fire/filter_hooks in K.
 move: st S' E K pf'; clear pf' st; subst p=>st S' E K' pf'.
 apply: (@SendMsg W this s1 _ l st pf' to msg)=>////.
 move=>z lc hk E'; apply: (K' z); rewrite E'.
-by rewrite find_umfilt/= eqxx.
+by rewrite find_umfiltk/= eqxx.
 Qed.
 
 Definition send_action_wrapper :=

Core/DepMaps.v

@@ -44,12 +44,12 @@ End PCMOps.
 
 Section DJoin.
 
-Variables (dm1 dm2 : depmap). 
+Variables (dm1 dm2 : depmap).
 
 Lemma dmDom_join um1 um2:
   dmDom um1 -> dmDom um2 -> dmDom (um1 \+ um2).
 Proof.
-case; case W: (valid (um1 \+ um2)); last first.
+case W: (valid (um1 \+ um2)); last first.
 - by move=> _ _; apply/allP=>l; move/dom_valid; rewrite W.
 move/allP=>D1/allP D2; apply/allP=>l.
 rewrite domUn inE=>/andP[_]/orP; rewrite findUnL//; case=>E; rewrite ?E.

Core/Freshness.v

@@ -18,10 +18,11 @@ Lemma keys_last_mono f1 f2 k :
         (forall x, x \in dom f1 -> x \in dom f2) ->
         oleq (last k (dom f1)) (last k (dom f2)).
 Proof.
-rewrite !umEX; case: (UMC.from f1); first by move=>_ H _; apply: path_last H.
+rewrite !umEX; case: (UMC.from f1).
+- by move=>_ H _; apply: path_lastR H=>//; apply: otrans.
 move=>{f1} f1 /= _ H1; case: (UMC.from f2)=>/=.
 - by move=>_ /allP; case: (supp f1)=>//; rewrite /oleq eq_refl orbT.
-by move=>{f2} f2 /= _; apply: seq_last_mono H1.
+by move=>{f2} f2 /= _; apply: seq_last_monoR H1=>//; apply: otrans.
 Qed.
 
 End Keys.
@@ -48,21 +49,23 @@ rewrite /UM.empty UMC.eqE UM.umapE /supp fmapE /= {H H1}.
 by elim: s.
 Qed.
 
-Lemma dom_last_key f :  valid f -> ~~ empb f -> last_key f \in dom f.
-Proof. by move=>X; apply: contraR; move/(last_key_dom X)=>->; apply/empbP. Qed.
+Lemma dom_last_key f :  valid f -> ~~ unitb f -> last_key f \in dom f.
+Proof. by move=>X; apply: contraR; move/(last_key_dom X)=>->; apply: unitb0. Qed.
 
 Lemma last_key_max f x : x \in dom f -> x <= last_key f.
 Proof.
 rewrite /last_key /= !umEX; case: (UMC.from f)=>//; case=>s H _ /=.
 rewrite /supp /ord /= (leq_eqVlt x) orbC.
-by apply: sorted_last_key_max (sorted_oleq H).
+by apply: sorted_last_key_maxR (sorted_oleq H)=>//; apply: otrans.
 Qed.
 
 Lemma max_key_last f x :
         x \in dom f -> {in dom f, forall y, y <= x} -> last_key f = x.
 Proof.
 rewrite /last_key !umEX; case: (UMC.from f)=>//; case=>s H _ /=.
 move=>H1 /= H2; apply: sorted_max_key_last (sorted_oleq H) H1 _.
+- by apply: otrans.
+- by apply: oantisym.
 by move=>z /(H2 z); rewrite leq_eqVlt orbC.
 Qed.