Merge pull request #8 from DistributedComponents/fcsl-pcm

Port to fcsl-pcm

.gitignore

@@ -83,3 +83,4 @@ extraction/**/*.ml
 _build
 *.d.byte
 Makefile.coq.conf
+.coqdeps.d

.travis-ci.sh

@@ -1,15 +1,10 @@
+#!/usr/bin/env bash
+
 set -ev
 
-opam init --yes --no-setup
 eval $(opam config env)
 
-opam repo add coq-released https://coq.inria.fr/opam/released
-opam repo add coq-core-dev https://coq.inria.fr/opam/core-dev
-opam repo add coq-extra-dev https://coq.inria.fr/opam/extra-dev
-
-opam pin add coq $COQ_VERSION --kind=version --yes
-opam pin add coq-mathcomp-ssreflect $SSREFLECT_VERSION --kind=version --yes --verbose
+opam update
 
-opam pin add Heaps --yes --verbose
 opam pin add Core --yes --verbose
 make -j4 -C Examples

.travis.yml

@@ -1,16 +1,54 @@
-language: c
-addons:
-  apt:
-    sources:
-      - avsm
-    packages:
-      - ocaml
-      - opam
-      - aspcud
+language: generic
+sudo: false
+
+services:
+  - docker
+
 env:
+  global:
+    - THIS_REPO=disel
   matrix:
-    - COQ_VERSION=8.7.1 SSREFLECT_VERSION=1.6.4
-script: bash -ex .travis-ci.sh
-sudo: false
+    - COQ_VERSION=coq8.7-32bit
+    - COQ_VERSION=coq8.8-32bit
+
+# The "docker run" command will pull if needed.
+# Running this first gives two tries in case of network lossage.
+before_script:
+  - timeout 5m docker pull palmskog/xenial-for-verdi-$COQ_VERSION || true
+
+# Using travis_wait here seems to cause the job to terminate after 1 minute
+# with no error (!).
+# The git commands are tried twice, in case of temporary network failure.
+# The fcntl line works around a bug where Travis truncates logs and fails.
+script:
+  - python -c "import fcntl; fcntl.fcntl(1, fcntl.F_SETFL, 0)"
+  - REMOTE_ORIGIN_URL=`git config --get remote.origin.url`
+  - echo "THIS_REPO=${THIS_REPO}"
+  - echo "COQ_VERSION=${COQ_VERSION}"
+  - echo "TRAVIS_BRANCH=${TRAVIS_BRANCH}"
+  - echo "REMOTE_ORIGIN_URL=${REMOTE_ORIGIN_URL}"
+  - echo "TRAVIS_EVENT_TYPE=${TRAVIS_EVENT_TYPE}"
+  - echo "TRAVIS_COMMIT=${TRAVIS_COMMIT}"
+  - echo "TRAVIS_PULL_REQUEST=${TRAVIS_PULL_REQUEST}"
+  - echo "TRAVIS_PULL_REQUEST_BRANCH=${TRAVIS_PULL_REQUEST_BRANCH}"
+  - echo "TRAVIS_PULL_REQUEST_SHA=${TRAVIS_PULL_REQUEST_SHA}"
+  - echo "TRAVIS_REPO_SLUG=${TRAVIS_REPO_SLUG}"
+  - >-
+    docker run palmskog/xenial-for-verdi-$COQ_VERSION /bin/bash -c "true &&
+       if [ $TRAVIS_EVENT_TYPE = pull_request ] ; then
+         git clone --quiet --depth 9 $REMOTE_ORIGIN_URL $THIS_REPO || git clone --quiet --depth 9 $REMOTE_ORIGIN_URL $THIS_REPO
+         cd $THIS_REPO
+         git fetch origin +refs/pull/$TRAVIS_PULL_REQUEST/merge
+         git checkout -qf $TRAVIS_PULL_REQUEST_SHA
+       else
+         git clone --quiet --depth 9 -b $TRAVIS_BRANCH $REMOTE_ORIGIN_URL $THIS_REPO || git clone --quiet --depth 9 -b $TRAVIS_BRANCH $REMOTE_ORIGIN_URL $THIS_REPO
+         cd $THIS_REPO
+         git checkout -qf $TRAVIS_COMMIT
+       fi &&
+       ./.travis-ci.sh"
+
+git:
+  depth: 9
+
 notifications:
   email: false

Core/Actions.v

@@ -4,9 +4,9 @@ From mathcomp
 Require Import path.
 Require Import Eqdep.
 Require Import Relation_Operators.
-From DiSeL.Heaps
-Require Import pred prelude idynamic ordtype finmap pcm unionmap heap coding.
-From DiSeL.Core
+From fcsl
+Require Import axioms pred prelude ordtype finmap pcm unionmap heap.
+From DiSeL
 Require Import Freshness State EqTypeX Protocols Worlds NetworkSem.
 Require Classical_Prop.
 
@@ -285,19 +285,19 @@ set s2 := let: d :=  getS s l in
           upd l (DStatelet f' s') s.
 exists s2, msg; split=>//; exists b; split=>//.
 move: (safe_safe (And4 C S J K))=> S''.
-by rewrite -E (proof_irrelevance S'' S') .
+by rewrite -E (pf_irr S'' S') .
 Qed.
 
 Lemma send_act_step_sem s1 (S : send_act_safe s1) s2 r:
   send_act_step S s2 r -> network_step W this s1 s2.
 Proof.
 case=>_[b][E Z]; case: (S)=>C S' /andP[D1] D2 K; subst s2=>/=.
-rewrite (proof_irrelevance (safe_safe S) S') in E; clear S.
+rewrite (pf_irr (safe_safe S) S') in E; clear S.
 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_um_filt/= eqxx.
+by rewrite find_umfilt/= eqxx.
 Qed.
 
 Definition send_action_wrapper :=

Core/Always.v

@@ -4,14 +4,12 @@ From mathcomp
 Require Import path.
 Require Import Eqdep.
 Require Import Relation_Operators.
-From DiSeL.Heaps
-Require Import pred prelude idynamic ordtype finmap pcm unionmap heap coding.
-From DiSeL.Core
+From fcsl
+Require Import axioms pred prelude ordtype finmap pcm unionmap heap.
+From DiSeL
 Require Import Freshness State EqTypeX DepMaps Protocols Worlds NetworkSem Rely.
-From DiSeL.Core
-Require Import Actions Injection Process.
-From DiSeL.Core
-Require InductiveInv.
+From DiSeL
+Require Import Actions Injection Process InductiveInv.
 
 Set Implicit Arguments.
 Unset Strict Implicit.
@@ -27,7 +25,7 @@ Variable W : world.
 
 Notation coherent := (Coh W).
 
-Implicit Arguments proc [W this]. 
+Arguments proc [this W].
 
 Fixpoint always_sc A (s1 : state) p scs (P : state -> proc A -> Prop) : Prop :=
   s1 \In coherent /\ 
@@ -152,7 +150,7 @@ Proof.
 move=>C H [|sc scs]; split=>// s2; case/H=>// H1[H2]H3//. 
 split=>//; first by case: sc.
 move=>s3 q /stepAct [v][pf][_ -> St].
-rewrite (proof_irrelevance H1 pf) in H3.
+rewrite (pf_irr H1 pf) in H3.
 apply: alw_ret'; last by move=>s4; apply: H3 St.
 by case: (step_coh (a_step_sem St)).
 Qed.
@@ -207,7 +205,7 @@ move=>Ls; split.
 by move=>H ps; apply/(alwA' _ (Ls ps))=>x; apply: H.
 Qed.
 
-Implicit Arguments alwA [A B s p P].
+Arguments alwA [A B s p P].
 
 (* always commutes with implication, so we can weaken the postconditions *)
 
@@ -240,7 +238,7 @@ move=>Ls; split; first by move=>H Hp scs; apply/alwI': Hp.
 by move=>H scs; apply/alwI'=>//; move/H; move/(_ scs).
 Qed.
 
-Implicit Arguments alwI [A s p P Q].
+Arguments alwI [A s p P Q].
 
 
 Lemma alw_bnd A B (p1 : proc A) (p12 : proc B) pp2 s1 
@@ -336,8 +334,8 @@ split; apply: alw_imp=>t q _ I.
 by move=>v; move/I.
 Qed.
 
-Implicit Arguments aftA [A B s p P].
-Implicit Arguments aftI [A s p P Q].
+Arguments aftA [A B s p P].
+Arguments aftI [A s p P Q].
 
 End Always.
 
@@ -364,8 +362,8 @@ case: (sem_split w C1 C2 N); case=>R E; [subst s2'|subst s2];
 split=>//; apply: Idle; split=>//.
 case: (step_coh N)=>C _.
 case/(cohE w): (C)=>s3[s4][E]C' C''.
-move: (coh_prec (cohS C) E C1 C')=>Z; subst s3.
-by rewrite (joinfK (cohS C) E).
+move: (coh_prec (cohS C) C1 C' E)=>Z; subst s3.
+by rewrite (joinxK (cohS C) E).
 Qed.
 
 Lemma rely_split s1 s1' s2 s2' : 
@@ -382,12 +380,12 @@ elim: n s1 s1' E C1 C2=>[|n IH] /= s1 s1'; last first.
   + by case: G1=>m R; exists m.+1, z, s4. 
   by case: G2=>m R; exists m.+1, z, s5. 
 move=> [E1 E2] C1 C2.
-move: (coh_prec (cohS E2) E1 C1 C2)=>Z; subst s2.
-rewrite (joinfK (cohS E2) E1); split; exists 0=>//. 
-split=>//; rewrite -(joinfK (cohS E2) E1)=>{E1 s2' C2}.
+move: (coh_prec (cohS E2) C1 C2 E1)=>Z; subst s2.
+rewrite (joinxK (cohS E2) E1); split; exists 0=>//. 
+split=>//; rewrite -(joinxK (cohS E2) E1)=>{E1 s2' C2}.
 move/(cohE w): (E2)=>[t1][t2][E]C' C''.
-move: ((coh_prec (cohS E2)) E C1 C')=>Z; subst t1.
-by rewrite (joinfK (cohS E2) E).
+move: ((coh_prec (cohS E2)) C1 C' E)=>Z; subst t1.
+by rewrite (joinxK (cohS E2) E).
 Qed.
 
 
@@ -423,13 +421,13 @@ case=>sc' [q'][x1][i2][y1][_ -> E -> {sc q s}] _ T Ls.
 
 have [E1 E2] : x1 = i1 /\ y1 = j1.
 - case: T=>Cx1 _.
-  move: (coh_prec (cohS C) E Ci1 Cx1) (E)=><-{E Cx1 x1}.
-  by move/(joinfK (cohS C)).
+  move: (coh_prec (cohS C) Ci1 Cx1 E) (E)=><-{E Cx1 x1}.
+  by move/(joinxK (cohS C)).
 rewrite {E x1}E1 {y1}E2 in T *.
 have C' : i2 \+ j1 \In Coh W.
 - move: (C)=>C'; rewrite (cohE w) in C *=>[[s1]][s2][E]D1 D2.
-  move: (coh_prec (cohS C') E Ci1 D1)=>Z; subst i1.
-  move: (joinfK (cohS C') E)=>Z; subst s2; clear E.
+  move: (coh_prec (cohS C') Ci1 D1 E)=>Z; subst i1.
+  move: (joinxK (cohS C') E)=>Z; subst s2; clear E.
   apply/(cohE w); exists i2, j1; split=>//.
   by case/step_coh: (pstep_network_sem T). 
 move/(alw_step Ls): T=>{Ls} Ls.

Core/DepMaps.v

@@ -4,15 +4,14 @@ From mathcomp
 Require Import path.
 Require Import Eqdep.
 Require Import Relation_Operators.
-From DiSeL.Heaps
-Require Import pred prelude idynamic ordtype finmap pcm unionmap heap coding.
-From DiSeL.Core
+From fcsl
+Require Import pred prelude ordtype finmap pcm unionmap heap.
+From DiSeL
 Require Import Freshness EqTypeX.
 Set Implicit Arguments.
 Unset Strict Implicit.
 Unset Printing Implicit Defensive.
 
-
 (* An implementation of a dependent map structure *)
 
 Module DepMaps.
@@ -25,7 +24,7 @@ Variable V : Type.
 Variable labF: V -> Label.
 
 Definition dmDom (u : union_map Label V) : bool :=
-    all (fun l => if find l u is Some p then (labF p) == l else false) (keys_of u).
+    all (fun l => if find l u is Some p then (labF p) == l else false) (dom u).
 
 Record depmap := DepMap {
    dmap : union_map Label V;
@@ -37,9 +36,7 @@ Section PCMOps.
 Variable dm : depmap.
 
 Lemma dmDom_unit : dmDom Unit.
-Proof.
-by apply/allP=>l; rewrite keys_dom dom0 inE.
-Qed.
+Proof. by apply/allP=>l; rewrite dom0. Qed.
 
 Definition unit := DepMap dmDom_unit.
 
@@ -53,12 +50,12 @@ Lemma dmDom_join um1 um2:
   dmDom um1 -> dmDom um2 -> dmDom (um1 \+ um2).
 Proof.
 case; case W: (valid (um1 \+ um2)); last first.
-- by move=> _ _; apply/allP=>l; rewrite keys_dom=>/dom_valid; rewrite W.
-move/allP=>D1/allP D2; apply/allP=>l; rewrite keys_dom.
+- 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.
-- by apply: D1; rewrite keys_dom.
+- by apply: D1.
 rewrite joinC in W; case: validUn W=>// _ _ /(_ l E)/negbTE->_.
-by apply: D2; rewrite keys_dom.
+by apply: D2.
 Qed.
 
 Definition join : depmap := DepMap (dmDom_join (@pf dm1) (@pf dm2)).
@@ -84,21 +81,21 @@ Lemma joinC f1 f2 : f1 \+ f2 = f2 \+ f1.
 Proof.
 case: f1 f2=>d1 pf1[d2 pf2]; rewrite /join/=.
 move: (dmDom_join pf1 pf2) (dmDom_join pf2 pf1); rewrite joinC=>G1 G2.
-by move: (proof_irrelevance G1 G2)=>->.
+by move: (bool_irrelevance G1 G2)=>->.
 Qed.
 
 Lemma joinCA f1 f2 f3 : f1 \+ (f2 \+ f3) = f2 \+ (f1 \+ f3).
 Proof.
 case: f1 f2 f3=>d1 pf1[d2 pf2][d3 pf3]; rewrite /join/=.
 move: (dmDom_join pf1 (dmDom_join pf2 pf3)) (dmDom_join pf2 (dmDom_join pf1 pf3)).
-by rewrite joinCA=>G1 G2; move: (proof_irrelevance G1 G2)=>->.
+by rewrite joinCA=>G1 G2; move: (bool_irrelevance G1 G2)=>->.
 Qed.
 
 Lemma joinA f1 f2 f3 : f1 \+ (f2 \+ f3) = (f1 \+ f2) \+ f3.
 Proof.
 case: f1 f2 f3=>d1 pf1[d2 pf2][d3 pf3]; rewrite /join/=.
 move: (dmDom_join pf1 (dmDom_join pf2 pf3)) (dmDom_join (dmDom_join pf1 pf2) pf3).
-by rewrite joinA=>G1 G2; move: (proof_irrelevance G1 G2)=>->.
+by rewrite joinA=>G1 G2; move: (bool_irrelevance G1 G2)=>->.
 Qed.
 
 Lemma validL f1 f2 : valid (f1 \+ f2) -> valid f1.
@@ -108,7 +105,7 @@ Lemma unitL f : unit \+ f = f.
 Proof.
 rewrite /join/unit/=; case: f=>//=u pf.
 move: pf (dmDom_join (dmDom_unit labF) pf); rewrite unitL=>g1 g2.
-by move: (proof_irrelevance g1 g2)=>->.
+by move: (bool_irrelevance g1 g2)=>->.
 Qed.
 
 Lemma validU : valid unit.
@@ -127,7 +124,7 @@ Definition DepMap := DepMap.
 Lemma dep_unit (d : depmap labF) : dmap d = Unit -> d = unit labF.
 Proof.
 case: d=>u pf/=; rewrite /unit. move: (dmDom_unit labF)=>pf' Z; subst u.
-by rewrite (proof_irrelevance pf).
+by rewrite (bool_irrelevance pf).
 Qed.
 
 Coercion dmap := dmap.

Core/DiSeLExtraction.v

@@ -1,4 +1,4 @@
-From DiSeL.Core
+From DiSeL
 Require Import While.
 
 Require Import ExtrOcamlBasic.