port to Coq 8.16, MathComp 1.15, FCSL-PCM 1.7.0

palmskog · palmskog · commit 6c0e946dfb56 · 2022-11-27T00:13:37.000+01:00
diff --git a/Core/Actions.v b/Core/Actions.v
@@ -4,7 +4,7 @@ From mathcomp
 Require Import path.
 Require Import Eqdep.
 Require Import Relation_Operators.
-From fcsl
+From pcm
 Require Import axioms pred prelude ordtype finmap pcm unionmap heap.
 From DiSeL
 Require Import Freshness State EqTypeX Protocols Worlds NetworkSem.
diff --git a/Core/Always.v b/Core/Always.v
@@ -1,15 +1,9 @@
-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 axioms pred prelude ordtype finmap pcm unionmap heap.
-From DiSeL
-Require Import Freshness State EqTypeX DepMaps Protocols Worlds NetworkSem Rely.
-From DiSeL
-Require Import Actions Injection Process InductiveInv.
+From mathcomp Require Import ssreflect ssrbool ssrnat eqtype ssrfun seq path.
+From Coq Require Import Eqdep Relation_Operators.
+From pcm Require Import axioms pred prelude ordtype finmap pcm unionmap heap.
+From DiSeL Require Import Freshness State EqTypeX DepMaps Protocols Worlds.
+From DiSeL Require Import NetworkSem Rely Actions Injection.
+From DiSeL Require Import Process InductiveInv.
 
 Set Implicit Arguments.
 Unset Strict Implicit.
@@ -425,15 +419,16 @@ have [E1 E2] : x1 = i1 /\ y1 = j1.
   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: (C)=>C'; rewrite (cohE w) in C.
+  move: C => [s1 [s2][E]D1 D2].
   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). 
+  by case/step_coh: (pstep_network_sem T).
 move/(alw_step Ls): T=>{Ls} Ls.
 apply: alw_imp' (IH _ _ _ C' Ls)=>{IH Ls C' C Ci Ci1 i i1 i2 p q' sc' scs}.
 move=>s p _ [i2][j2][->{s}] Ci2 S2 H; exists i2, j2; split=>//.
-by apply: rely_trans S1 S2.  
+by apply: rely_trans S1 S2.
 Qed.
 
 Lemma aft_inject (p : proc this V A) (P : A -> state -> Prop) i j :
diff --git a/Core/DepMaps.v b/Core/DepMaps.v
@@ -4,7 +4,7 @@ From mathcomp
 Require Import path.
 Require Import Eqdep.
 Require Import Relation_Operators.
-From fcsl
+From pcm
 Require Import pred prelude ordtype finmap pcm unionmap heap.
 From DiSeL
 Require Import Freshness EqTypeX.
diff --git a/Core/Domain.v b/Core/Domain.v
@@ -1,6 +1,6 @@
 From mathcomp.ssreflect
 Require Import ssreflect ssrbool ssrfun ssrnat eqtype seq.
-From fcsl
+From pcm
 Require Import axioms pred prelude.
 Set Implicit Arguments.
 Unset Strict Implicit.
diff --git a/Core/Freshness.v b/Core/Freshness.v
@@ -1,9 +1,6 @@
-From mathcomp.ssreflect
-Require Import ssreflect ssrbool ssrnat eqtype ssrfun seq.
-From mathcomp
-Require Import path.
-From fcsl
-Require Import pred prelude ordtype finmap pcm unionmap.
+From mathcomp Require Import ssreflect ssrbool ssrnat eqtype ssrfun seq.
+From mathcomp Require Import path.
+From pcm Require Import pred prelude ordtype finmap pcm unionmap seqext.
 Set Implicit Arguments.
 Unset Strict Implicit.
 Unset Printing Implicit Defensive.
diff --git a/Core/HoareTriples.v b/Core/HoareTriples.v
@@ -4,7 +4,7 @@ From mathcomp
 Require Import path.
 Require Import Eqdep.
 Require Import Relation_Operators.
-From fcsl
+From pcm
 Require Import axioms pred prelude ordtype finmap pcm unionmap heap.
 From DiSeL
 Require Import Domain Freshness State EqTypeX DepMaps Protocols Worlds NetworkSem Rely.
diff --git a/Core/InductiveInv.v b/Core/InductiveInv.v
@@ -4,7 +4,7 @@ From mathcomp
 Require Import path.
 Require Import Eqdep.
 Require Import Relation_Operators.
-From fcsl
+From pcm
 Require Import axioms pred prelude ordtype finmap pcm unionmap heap.
 From DiSeL
 Require Import Freshness State EqTypeX Protocols Worlds NetworkSem Rely.
diff --git a/Core/InferenceRules.v b/Core/InferenceRules.v
@@ -4,7 +4,7 @@ From mathcomp
 Require Import path.
 Require Import Eqdep.
 Require Import Relation_Operators.
-From fcsl
+From pcm
 Require Import pred prelude ordtype finmap pcm unionmap heap.
 From DiSeL
 Require Import Domain Freshness State EqTypeX DepMaps Protocols Worlds NetworkSem Rely.
diff --git a/Core/Injection.v b/Core/Injection.v
@@ -4,7 +4,7 @@ From mathcomp
 Require Import path.
 Require Import Eqdep.
 Require Import Relation_Operators.
-From fcsl
+From pcm
 Require Import axioms pred prelude ordtype finmap pcm unionmap heap.
 From DiSeL
 Require Import Freshness State EqTypeX Protocols Worlds NetworkSem Actions.
diff --git a/Core/NetworkSem.v b/Core/NetworkSem.v
@@ -4,7 +4,7 @@ From mathcomp
 Require Import path.
 Require Import Eqdep.
 Require Import Relation_Operators.
-From fcsl
+From pcm
 Require Import axioms pred prelude ordtype finmap pcm unionmap heap.
 From DiSeL
 Require Import Freshness State EqTypeX Protocols Worlds.
diff --git a/Core/NewStatePredicates.v b/Core/NewStatePredicates.v
@@ -4,7 +4,7 @@ From mathcomp
 Require Import path.
 Require Import Eqdep.
 Require Import Relation_Operators.
-From fcsl
+From pcm
 Require Import pred prelude ordtype finmap pcm unionmap heap.
 From DiSeL
 Require Import Freshness State EqTypeX DepMaps.
diff --git a/Core/Process.v b/Core/Process.v
@@ -4,7 +4,7 @@ From mathcomp
 Require Import path.
 Require Import Eqdep.
 Require Import Relation_Operators.
-From fcsl
+From pcm
 Require Import pred prelude ordtype finmap pcm unionmap heap.
 From DiSeL
 Require Import Freshness State EqTypeX DepMaps Protocols Worlds NetworkSem.
diff --git a/Core/Protocols.v b/Core/Protocols.v
@@ -4,7 +4,7 @@ From mathcomp
 Require Import path.
 Require Import Eqdep.
 Require Import Relation_Operators.
-From fcsl
+From pcm
 Require Import pred prelude ordtype finmap pcm unionmap heap.
 From DiSeL
 Require Import Freshness State EqTypeX.
diff --git a/Core/Rely.v b/Core/Rely.v
@@ -4,7 +4,7 @@ From mathcomp
 Require Import path.
 Require Import Eqdep.
 Require Import Relation_Operators.
-From fcsl
+From pcm
 Require Import pred prelude ordtype finmap pcm unionmap heap.
 From DiSeL
 Require Import Freshness State EqTypeX Protocols Worlds NetworkSem.
diff --git a/Core/State.v b/Core/State.v
@@ -4,7 +4,7 @@ From mathcomp
 Require Import path.
 Require Import Eqdep.
 Require Import Relation_Operators.
-From fcsl
+From pcm
 Require Import pred prelude ordtype finmap pcm unionmap heap.
 From DiSeL
 Require Import Freshness DepMaps EqTypeX.
diff --git a/Core/StatePredicates.v b/Core/StatePredicates.v
@@ -4,7 +4,7 @@ From mathcomp
 Require Import path.
 Require Import Eqdep.
 Require Import Relation_Operators.
-From fcsl
+From pcm
 Require Import pred prelude ordtype finmap pcm unionmap heap.
 From DiSeL
 Require Import Freshness State EqTypeX DepMaps.
diff --git a/Core/While.v b/Core/While.v
@@ -1,15 +1,9 @@
-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 State EqTypeX DepMaps Protocols Worlds NetworkSem Rely.
-From DiSeL
-Require Import Actions Injection Process Always HoareTriples InferenceRules.
+From mathcomp Require Import ssreflect ssrbool ssrnat eqtype ssrfun seq path.
+From Coq Require Import Eqdep Relation_Operators.
+From pcm Require Import pred prelude ordtype finmap pcm unionmap heap.
+From DiSeL Require Import Freshness State EqTypeX DepMaps Protocols.
+From DiSeL Require Import Worlds NetworkSem Rely Actions Injection.
+From DiSeL Require Import Process Always HoareTriples InferenceRules.
 Set Implicit Arguments.
 Unset Strict Implicit.
 Import Prenex Implicits.
diff --git a/Core/Worlds.v b/Core/Worlds.v
@@ -4,7 +4,7 @@ From mathcomp
 Require Import path.
 Require Import Eqdep.
 Require Import Relation_Operators.
-From fcsl
+From pcm
 Require Import pred prelude ordtype finmap pcm unionmap heap.
 From DiSeL
 Require Import Freshness State EqTypeX Protocols.
diff --git a/Examples/Calculator/CalculatorClientLib.v b/Examples/Calculator/CalculatorClientLib.v
@@ -4,7 +4,7 @@ From mathcomp
 Require Import path.
 Require Import Eqdep.
 Require Import Relation_Operators.
-From fcsl
+From pcm
 Require Import axioms pred prelude ordtype finmap pcm unionmap heap.
 From DiSeL
 Require Import Freshness State EqTypeX Protocols Worlds NetworkSem Rely.
diff --git a/Examples/Calculator/CalculatorInvariant.v b/Examples/Calculator/CalculatorInvariant.v
@@ -4,7 +4,7 @@ From mathcomp
 Require Import path.
 Require Import Eqdep.
 Require Import Relation_Operators.
-From fcsl
+From pcm
 Require Import axioms pred prelude ordtype finmap pcm unionmap heap.
 From DiSeL
 Require Import Freshness State EqTypeX Protocols Worlds NetworkSem Rely.
diff --git a/Examples/Calculator/CalculatorProtocol.v b/Examples/Calculator/CalculatorProtocol.v
@@ -4,7 +4,7 @@ From mathcomp
 Require Import path.
 Require Import Eqdep.
 Require Import Relation_Operators.
-From fcsl
+From pcm
 Require Import axioms pred prelude ordtype finmap pcm unionmap heap.
 From DiSeL
 Require Import Freshness State EqTypeX Protocols Worlds NetworkSem Rely.
diff --git a/Examples/Calculator/CalculatorServerLib.v b/Examples/Calculator/CalculatorServerLib.v
@@ -4,7 +4,7 @@ From mathcomp
 Require Import path.
 Require Import Eqdep.
 Require Import Relation_Operators.
-From fcsl
+From pcm
 Require Import axioms pred prelude ordtype finmap pcm unionmap heap.
 From DiSeL
 Require Import Freshness State EqTypeX Protocols Worlds NetworkSem Rely.
diff --git a/Examples/Calculator/DelegatingCalculatorServer.v b/Examples/Calculator/DelegatingCalculatorServer.v
@@ -4,7 +4,7 @@ From mathcomp
 Require Import path.
 Require Import Eqdep.
 Require Import Relation_Operators.
-From fcsl
+From pcm
 Require Import pred prelude ordtype finmap pcm unionmap heap.
 From DiSeL
 Require Import Freshness State EqTypeX Protocols Worlds NetworkSem Rely.
diff --git a/Examples/Calculator/SimpleCalculatorApp.v b/Examples/Calculator/SimpleCalculatorApp.v
@@ -4,7 +4,7 @@ From mathcomp
 Require Import path.
 Require Import Eqdep.
 Require Import Relation_Operators.
-From fcsl
+From pcm
 Require Import pred prelude ordtype finmap pcm unionmap heap.
 From DiSeL
 Require Import Freshness State EqTypeX Protocols Worlds NetworkSem Rely.
diff --git a/Examples/Calculator/SimpleCalculatorServers.v b/Examples/Calculator/SimpleCalculatorServers.v
@@ -4,7 +4,7 @@ From mathcomp
 Require Import path.
 Require Import Eqdep.
 Require Import Relation_Operators.
-From fcsl
+From pcm
 Require Import pred prelude ordtype finmap pcm unionmap heap.
 From DiSeL
 Require Import Freshness State EqTypeX DepMaps Protocols Worlds NetworkSem Rely.
diff --git a/Examples/Greeter/Greeter.v b/Examples/Greeter/Greeter.v
@@ -4,7 +4,7 @@ From mathcomp
 Require Import path.
 Require Import Eqdep.
 Require Import Relation_Operators.
-From fcsl
+From pcm
 Require Import axioms pred prelude ordtype finmap pcm unionmap heap.
 From DiSeL
 Require Import Freshness State EqTypeX Protocols Worlds NetworkSem Rely.
diff --git a/Examples/LockResource/LockProtocol.v b/Examples/LockResource/LockProtocol.v
@@ -4,7 +4,7 @@ From mathcomp
 Require Import path.
 Require Import Eqdep.
 Require Import Relation_Operators.
-From fcsl
+From pcm
 Require Import axioms pred prelude ordtype finmap pcm unionmap heap.
 From DiSeL
 Require Import Freshness State EqTypeX Protocols Worlds NetworkSem Rely.
diff --git a/Examples/LockResource/ResourceProtocol.v b/Examples/LockResource/ResourceProtocol.v
@@ -4,7 +4,7 @@ From mathcomp
 Require Import path.
 Require Import Eqdep.
 Require Import Relation_Operators.
-From fcsl
+From pcm
 Require Import axioms pred prelude ordtype finmap pcm unionmap heap.
 From DiSeL
 Require Import Freshness State EqTypeX Protocols Worlds NetworkSem Rely.
diff --git a/Examples/Querying/QueryHooked.v b/Examples/Querying/QueryHooked.v
@@ -1,14 +1,10 @@
-From mathcomp.ssreflect
-Require Import ssreflect ssrbool ssrnat eqtype ssrfun seq path.
-Require Import Eqdep.
-From fcsl
-Require Import axioms pred prelude ordtype finmap pcm unionmap heap.
-From DiSeL
-Require Import Freshness State EqTypeX Protocols Worlds NetworkSem Rely Actions.
-From DiSeL
-Require Import SeqLib QueryProtocol NewStatePredicates Actions.
-From DiSeL
-Require Import Injection Process Always HoareTriples InferenceRules While.
+From mathcomp Require Import ssreflect ssrbool ssrnat eqtype ssrfun seq path.
+From Coq Require Import Eqdep.
+From pcm Require Import axioms pred prelude ordtype finmap pcm unionmap heap.
+From DiSeL Require Import Freshness State EqTypeX Protocols Worlds.
+From DiSeL Require Import NetworkSem Rely Actions SeqLib QueryProtocol.
+From DiSeL Require Import NewStatePredicates Actions Injection Process.
+From DiSeL Require Import Always HoareTriples InferenceRules While.
 Obligation Tactic := Tactics.program_simpl.
 
 Section QueryHooked.
@@ -1101,13 +1097,12 @@ split=>//; try apply: (msg_story_rely _ _ _ _ _ _ _ H3 H0).
 Defined.
 
 Next Obligation.
-rename H into d.
 apply: ghC=>i0 [[reqs resp] data][G0 H0] C0; apply: step.
 apply: act_rule=>i1 R1/=; split; first by case: (rely_coh R1).
 case=>[[[from tg] body] i2 i3|i2 i3]; last first.
 - case=>S/=[]C1; case; last by case=>?[?][?][?][?][?][].
   case=>_ _ Z; subst i2=>R3; apply: ret_rule=>i4 R4/=.
-  case: d G0 H0=>//=_[H1 H2 H3].
+  case: o G0 H0=>//=_[H1 H2 H3].
   rewrite !(rely_loc' _ R4)!(rely_loc' _ R3)!(rely_loc' _ R1); split=>//.
   by apply: (msg_story_rely _ _ _ _ _ _ _ _ R4);
     apply: (msg_story_rely _ _ _ _ _ _ _ _ R3);
@@ -1127,14 +1122,14 @@ suff X : [/\ getLocal this (getStatelet i2 lq) = qst :-> (reqs, resp),
           deserialize (behead tms) = data].
 - case: X=>X1 X2 X3 X4; split=>//.
   by apply: (query_init_rely _ _ _ _ R3); apply: (query_init_rely _ _ _ _ R).
-- case: d G0 H0=>//=_[_ H2][_] H3 _ _; case: X3=>Nq _ _ _.
+- case: o G0 H0=>//=_[_ H2][_] H3 _ _; case: X3=>Nq _ _ _.
   move: (X2); rewrite -(rely_loc' _ R)=>X3.
   apply: (core_state_stable _ _ _ _ R3 Nq X3).
   apply: (core_state_stable _ _ _ _ R Nq X2).
   move: (core_state_stable _ _ _ _ R1 Nq H2 H3)=>{H2 H3 X3 X4}Y.
   by subst i2; rewrite /getStatelet findU eq_sym; move/negbTE:Lab_neq=>->.
 clear R i4 R3.
-case: d G0 H0=>//=_[Q1 Q2 Q3]; rewrite -!(rely_loc' _ R1) in Q1 Q2.
+case: o G0 H0=>//=_[Q1 Q2 Q3]; rewrite -!(rely_loc' _ R1) in Q1 Q2.
 move: (msg_story_rely _ _ _ _ _ _ _ Q3 R1)=>{Q3}Q3.
 have P1: valid (dstate (getSq i1)) by case: (C1')=>P1 P2 P3 P4.
 have P2: valid i1 by apply: (cohS C1).
diff --git a/Examples/Querying/QueryPlusTPC.v b/Examples/Querying/QueryPlusTPC.v
@@ -3,7 +3,7 @@ Require Import ssreflect ssrbool ssrnat eqtype ssrfun seq.
 From mathcomp
 Require Import path.
 Require Import Eqdep.
-From fcsl
+From pcm
 Require Import pred prelude ordtype finmap pcm unionmap heap.
 From DiSeL
 Require Import Freshness State EqTypeX Protocols Worlds NetworkSem Rely.
diff --git a/Examples/Querying/QueryProtocol.v b/Examples/Querying/QueryProtocol.v
@@ -1,14 +1,8 @@
-From mathcomp.ssreflect
-Require Import ssreflect ssrbool ssrnat eqtype ssrfun seq.
-From mathcomp
-Require Import path.
-Require Import Eqdep.
-From fcsl
-Require Import axioms pred prelude ordtype finmap pcm unionmap heap.
-From DiSeL
-Require Import Freshness State EqTypeX Protocols Worlds NetworkSem Rely Actions.
-From DiSeL
-Require Import SeqLib.
+From mathcomp Require Import ssreflect ssrbool ssrnat eqtype ssrfun seq path.
+From Coq Require Import Eqdep.
+From pcm Require Import axioms pred prelude ordtype finmap pcm unionmap heap seqext.
+From DiSeL Require Import Freshness State EqTypeX Protocols.
+From DiSeL Require Import Worlds NetworkSem Rely Actions SeqLib.
 
 Set Implicit Arguments.
 Unset Strict Implicit.
diff --git a/Examples/TwoPhaseCommit/SimpleTPCApp.v b/Examples/TwoPhaseCommit/SimpleTPCApp.v
@@ -4,7 +4,7 @@ From mathcomp
 Require Import path.
 Require Import Eqdep.
 Require Import Relation_Operators.
-From fcsl
+From pcm
 Require Import pred prelude ordtype finmap pcm unionmap heap.
 From DiSeL
 Require Import State Protocols Worlds NetworkSem Rely.
diff --git a/Examples/TwoPhaseCommit/TwoPhaseClient.v b/Examples/TwoPhaseCommit/TwoPhaseClient.v
diff --git a/Examples/TwoPhaseCommit/TwoPhaseCoordinator.v b/Examples/TwoPhaseCommit/TwoPhaseCoordinator.v
diff --git a/Examples/TwoPhaseCommit/TwoPhaseInductiveInv.v b/Examples/TwoPhaseCommit/TwoPhaseInductiveInv.v
diff --git a/Examples/TwoPhaseCommit/TwoPhaseInductiveProof.v b/Examples/TwoPhaseCommit/TwoPhaseInductiveProof.v
diff --git a/Examples/TwoPhaseCommit/TwoPhaseParticipant.v b/Examples/TwoPhaseCommit/TwoPhaseParticipant.v
diff --git a/Examples/TwoPhaseCommit/TwoPhaseProtocol.v b/Examples/TwoPhaseCommit/TwoPhaseProtocol.v
diff --git a/_CoqProject b/_CoqProject
