for maintainability, use domain module from htt

Author: palmskog

Core/Domain.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 pcm
-Require Import axioms pred prelude ordtype finmap pcm unionmap heap.
-From DiSeL
-Require Import Domain Freshness State EqTypeX DepMaps Protocols Worlds NetworkSem Rely.
-From DiSeL
-Require Import Actions Injection Process Always.
+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 htt Require Import domain.
+From DiSeL Require Import Freshness State EqTypeX DepMaps Protocols.
+From DiSeL Require Import Worlds NetworkSem Rely Actions Injection Process Always.
 Set Implicit Arguments.
 Unset Strict Implicit.
 Unset Printing Implicit Defensive.
@@ -202,7 +196,7 @@ Variable this : nid.
 Variable W : world.
 Variables (A : Type) (s : spec A).
 
-Definition stPosetMixin := PosetMixin (@leq_refl this W A s) 
+Definition stPosetMixin := PosetMixin (@bot_bot this W A s) (@leq_refl this W A s)
                                       (@leq_asym this W A s) (@leq_trans this W A s).
 Canonical stPoset := Eval hnf in Poset (@DTbin this W A s) stPosetMixin.
 

Core/HoareTriples.v

@@ -1,15 +1,10 @@
-From mathcomp.ssreflect
-Require Import ssreflect ssrbool ssrnat eqtype ssrfun seq.
-From mathcomp
-Require Import path.
-Require Import Eqdep.
-Require Import Relation_Operators.
-From pcm
-Require Import pred prelude ordtype finmap pcm unionmap heap.
-From DiSeL
-Require Import Domain Freshness State EqTypeX DepMaps Protocols Worlds NetworkSem Rely.
-From DiSeL
-Require Import Actions Injection Process Always HoareTriples InductiveInv.
+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 htt Require Import domain.
+From DiSeL Require Import Freshness State EqTypeX DepMaps Protocols.
+From DiSeL Require Import Worlds NetworkSem Rely Actions Injection Process.
+From DiSeL Require Import Always HoareTriples InductiveInv.
 Set Implicit Arguments.
 Unset Strict Implicit.
 Import Prenex Implicits.

Core/InferenceRules.v

@@ -6,7 +6,6 @@
 -arg -w -arg -projection-no-head-constant
 -arg -w -arg -deprecated-hint-without-locality
 
-Domain.v
 State.v
 Freshness.v
 Protocols.v

Core/Make

@@ -30,6 +30,7 @@ from implementation details.
 - Additional dependencies:
   - [MathComp](https://math-comp.github.io) 1.13.0 or later (`ssreflect` suffices)
   - [FCSL PCM](https://github.com/imdea-software/fcsl-pcm) 1.7.0 or later
+  - [Hoare Type Theory](https://github.com/imdea-software/htt) 1.2.0 or later
 - Coq namespace: `DiSeL`
 - Related publication(s):
   - [Programming and Proving with Distributed Protocols](http://jamesrwilcox.com/disel.pdf) doi:[10.1145/3158116](https://doi.org/10.1145/3158116)

README.md

@@ -9,7 +9,6 @@
 -arg -w -arg -notation-incompatible-format
 -arg -w -arg -deprecated-hint-without-locality
 
-Core/Domain.v
 Core/State.v
 Core/Freshness.v
 Core/Protocols.v

_CoqProject

@@ -14,6 +14,7 @@ depends: [
   "coq" {>= "8.14"}
   "coq-mathcomp-ssreflect" {>= "1.13"}
   "coq-fcsl-pcm" {>= "1.7.0"}
+  "coq-htt" {>= "1.2.0"}
   "ocamlbuild" {build}
 ]
 

coq-disel-calculator.opam

@@ -14,6 +14,7 @@ depends: [
   "coq" {>= "8.14"}
   "coq-mathcomp-ssreflect" {>= "1.13"}
   "coq-fcsl-pcm" {>= "1.7.0"}
+  "coq-htt" {>= "1.2.0"}
   "coq-disel" {= version}
 ]
 

coq-disel-examples.opam

@@ -14,6 +14,7 @@ depends: [
   "coq" {>= "8.14"}
   "coq-mathcomp-ssreflect" {>= "1.13"}
   "coq-fcsl-pcm" {>= "1.7.0"}
+  "coq-htt" {>= "1.2.0"}
   "ocamlbuild" {build}
 ]
 

coq-disel-tpc.opam

@@ -23,6 +23,7 @@ depends: [
   "coq" {>= "8.14"}
   "coq-mathcomp-ssreflect" {>= "1.13"}
   "coq-fcsl-pcm" {>= "1.7.0"}
+  "coq-htt" {>= "1.2.0"}
 ]
 
 tags: [