.ackrc

+# Configuration file for the 'ack' search utility
+# See https://beyondgrep.com/ for details.
+
+# Ignore misc files generated by the build process
+--ignore-file=ext:glob,aux,d,conf,orig
+--ignore-dir=html

.gitattributes

+*.v gitlab-language=coq

.gitignore

+*.d
+*.glob
+*.vo
+*.vos
+*.vok
+*.html
+/html
+*.aux
+Makefile.coq*
+Makefile.conf
+*.crashcoqide
+*.v#
+*.cache
+*~
+*.swp
+*.orig
+*/.#*
+#*#
+.#*
+*.DS_Store
+/proof-state
+/with-proof-state
+/html-alectryon
+_esy
+esy.lock/
+_CoqProject

.gitlab-ci.yml

+###################### Global Config ######################
+
+workflow:
+  rules:
+    - if: '$CI_PIPELINE_SOURCE == "merge_request_event"'
+    - if: '$CI_COMMIT_BRANCH && $CI_OPEN_MERGE_REQUESTS'
+      when: never
+    - if: '$CI_COMMIT_BRANCH'
+
+stages:
+  - build
+
+###################### Rules and Scripts ##################
+
+.not_in_wip_branches:
+  rules:
+    - if: ($CI_COMMIT_BRANCH !~ /^wip-.*$/) || ($CI_PIPELINE_SOURCE == "merge_request_event")
+
+.only_in_wip_branches:
+  rules:
+    - if: ($CI_COMMIT_BRANCH =~ /^wip-.*$/) && ($CI_PIPELINE_SOURCE != "merge_request_event")
+
+.build-common:
+  stage: build
+  script:
+    - opam pin add -n -y -k path coq-prosa .
+    - opam install -y -v -j ${NJOBS} coq-prosa
+    - opam pin add -n -y -k path coq-prosa-refinements .
+    - opam install -y -v -j ${NJOBS} coq-prosa-refinements
+
+.preferred-stable-version:
+    image: registry.mpi-sws.org/mathcomp-for-prosa:2.3.0-coq-8.20
+
+.build:
+  image: registry.mpi-sws.org/mathcomp-for-prosa:${CI_JOB_NAME}
+  extends: .build-common
+
+.build-and-test-POET:
+  extends: .build
+  script:
+    - git clone https://gitlab.mpi-sws.org/RT-PROOFS/POET.git -b POET-for-Prosa-CI-next /tmp/POET
+    - !reference [.build-common, script]
+    - mv /tmp/POET .
+    - cd POET
+    - pip3 install --break-system-packages -r requirements.txt
+    - >-
+      for WORKLOAD in examples/*.yaml;
+      do
+        CERT=certs/cert-for-`basename $WORKLOAD`;
+        echo; echo; echo;
+        echo "==================";
+        echo "Testing $WORKLOAD:";
+        mkdir -p $CERT;
+        time ./poet -v -o $CERT -j ${NJOBS} -s $WORKLOAD;
+      done;
+      
+
+.make-html:
+  script:
+    - make html -j ${NJOBS}
+    - mv html with-proofs
+    - make gallinahtml -j ${NJOBS}
+    - mv html without-proofs
+    - make htmlpretty -j ${NJOBS}
+    - mv html pretty
+
+###################### The Jobs ######################
+
+2.2.0-coq-8.19:
+  extends:
+    - .build
+    - .not_in_wip_branches
+
+2.3.0-coq-8.20:
+  extends:
+    - .build
+    - .not_in_wip_branches
+
+POET:
+  extends:
+    - .build-and-test-POET
+    - .preferred-stable-version
+    - .not_in_wip_branches
+
+compile-and-doc:
+  stage: build
+  extends:
+    - .only_in_wip_branches
+    - .preferred-stable-version
+  script:
+    - make -j ${NJOBS} all
+    - !reference [.make-html, script]
+  artifacts:
+    name: "prosa-spec-$CI_COMMIT_REF_NAME"
+    paths:
+      - "with-proofs/"
+      - "without-proofs/"
+      - "pretty/"
+    expire_in: 1 week
+
+compile-and-doc-and-validate:
+  stage: build
+  extends:
+    - .not_in_wip_branches
+    - .preferred-stable-version
+  script:
+    - make -j ${NJOBS} all 2>&1 | tee coqc-messages.txt
+    - if grep -q Warning coqc-messages.txt; then (echo "Please fix all Coq warnings:"; echo "--"; grep -B1 Warning coqc-messages.txt; exit 1); fi
+    - !reference [.make-html, script]
+    - scripts/check-axiom-free.sh results
+##### `make validate` disabled because of https://github.com/LPCIC/coq-elpi/issues/677 and https://github.com/coq/coq/issues/17345
+#     - make validate 2>&1 | tee validation-results.txt
+#     - scripts/check-validation-output.sh --accept-proof-irrelevance validation-results.txt
+  artifacts:
+    name: "prosa-spec-$CI_COMMIT_REF_NAME"
+    paths:
+      - "with-proofs/"
+      - "without-proofs/"
+      - "pretty/"
+    expire_in: 1 week
+
+mangle-names:
+  stage: build
+  extends:
+    - .not_in_wip_branches
+    - .preferred-stable-version
+  script:
+    - make -j ${NJOBS} mangle-names
+
+# Check that proof irrelevance shows up only due to refinements.
+compile-and-validate:
+  stage: build
+  extends:
+    - .not_in_wip_branches
+    - .preferred-stable-version
+  script:
+    - make -j ${NJOBS}
+    - scripts/check-axiom-free.sh results
+##### `make validate` disabled because of https://github.com/LPCIC/coq-elpi/issues/677 and https://github.com/coq/coq/issues/17345
+#     - make validate 2>&1 | tee validation-results.txt
+#     - scripts/check-validation-output.sh validation-results.txt
+
+proof-length:
+  stage: build
+  image: python:3
+  script:
+    - make proof-length
+
+spell-check:
+  extends:
+    - .not_in_wip_branches
+  stage: build
+  image: registry.mpi-sws.org/aspell-ci:2023-03
+  script:
+    - make spell
+
+# mathcomp-dev with stable Coq
+#coq-8.17:
+#  extends:
+#    - .build-dev
+#    - .not_in_wip_branches
+#  # it's ok to fail with an unreleased version of ssreflect
+#  allow_failure: true
+
+# mathcomp-dev with coq-dev
+#coq-dev:
+#  extends:
+#    - .build-dev
+#    - .not_in_wip_branches
+#  # it's ok to fail with an unreleased version of ssreflect and Coq
+#  allow_failure: true
+
+proof-state:
+  extends:
+   - .not_in_wip_branches
+  stage: build
+  image: registry.mpi-sws.org/alectryon-ci:2.3.0-coq-8.20
+  script:
+    - eval $(opam env)
+    - make -j ${NJOBS} all
+    - make -j ${NJOBS} alectryon
+  artifacts:
+    name: "prosa-proof-state-$CI_COMMIT_REF_NAME"
+    paths:
+      - "html-alectryon/"
+    expire_in: 1 week

.mailmap

+Björn Brandenburg <bbb@mpi-sws.org> Björn Brandenburg <bbb@mpi-sws.org>
+
+Sergey Bozhko <sbozhko@mpi-sws.org> Sergei Bozhko <sbozhko@mpi-sws.org>
+Sergey Bozhko <sbozhko@mpi-sws.org> Sergey Bozhko <gkerfimf@gmail.com>
+Sergey Bozhko <sbozhko@mpi-sws.org> Sergey Bozhko <sbozhko@sws-mpi.org>
+
+Kimaya Bedarkar <kbedarka@mpi-sws.org> Kimaya <f20171026@goa.bits-pilani.ac.in>
+Kimaya Bedarkar <kbedarka@mpi-sws.org> Kimaya Bedarkar <f20171026@goa.bits-pilani.ac.in>
+Kimaya Bedarkar <kbedarka@mpi-sws.org> kbedarka <kbedarka@mpi-sws.org>
+Kimaya Bedarkar <kbedarka@mpi-sws.org> kimaya <f20171026@goa.bits-pilani.ac.in>
+Kimaya Bedarkar <kbedarka@mpi-sws.org> Kimaya <kbedarka@mpi-sws.org>
+
+Marco Maida <mmaida@mpi-sws.org> Marco Maida <>
+Marco Maida <mmaida@mpi-sws.org> mmaida <mmaida@mpi-sws.org>
+
+Mariam Vardishvili <mariamvardishvili@gmail.com> mariamvardishvili <mariamvardishvili@gmail.com>
+Mariam Vardishvili <mariamvardishvili@gmail.com> mariamvardishvili <mvardishvili@mpi-sws.org>
+Mariam Vardishvili <mariamvardishvili@gmail.com> Mariam Vardishvili <mvardishvili@mpi-sws.org>
+
+Maxime Lesourd <maxime.lesourd@inria.fr> Maxime Lesourd <maxime.lesourd@gmail.com>
+Martin Bodin <martin.bodin@inria.fr> Martin Constantino–Bodin <martin.bodin@ens-lyon.org>
+Martin Bodin <martin.bodin@inria.fr> Martin Constantino–Bodin <martin.bodin@inria.fr>
+Pierre Roux <pierre.roux@onera.fr> Pierre Roux <pierre@roux01.fr>
+Pierre Roux <pierre.roux@onera.fr> Pierre Roux <proux@mpi-sws.org>
+Sophie Quinton <sophie.quinton@inria.fr> sophie quinton <squinton@inrialpes.fr>
+Sophie Quinton <sophie.quinton@inria.fr> sophie quinton <sophie.quinton@inria.fr>
+Xiaojie GUO <xiaojie.guo@inria.fr> Xiaojie GUO <gxj0303@loic.inrialpes.fr>
+
+Meenal Gupta <meenalg727@gmail.com> Meenal-27 <80755301+Meenal-27@users.noreply.github.com>

ExtraRelations.v

-(******************************************************************************)
-(* c11comp: Coq development attached to the paper                             *)
-(*                                                                            *)
-(*  Vafeiadis, Balabonski, Chakraborty, Morisset, and Zappa Nardelli.         *)
-(*  Common compiler optimisations are invalid in the C11 memory model         *)
-(*  and what we can do about it.                                              *)
-(*  In POPL 2015.                                                             *)
-(*                                                                            *)
-(* Copyright (c) MPI-SWS and INRIA                                            *)
-(* Released under a BSD-style license. See README.txt for details.            *)
-(******************************************************************************)
-
-(******************************************************************************)
-(** * Basic properties of relations *)
-(******************************************************************************)
-
-Require Import Vbase List Relations Classical. 
-Set Implicit Arguments.
-
-(** Definitions of relations *)
-(******************************************************************************)
-
-Definition immediate X (rel : relation X) (a b: X) :=
-  rel a b /\ (forall c (R1: rel a c) (R2: rel c b), False).
-
-Definition irreflexive X (rel : relation X) := forall x, rel x x -> False.
-
-Definition asymmetric X (rel : relation X) := forall x y, rel x y /\ rel y x -> False.
-
-Definition acyclic X (rel : relation X) := irreflexive (clos_trans X rel).
-
-Definition is_total X (cond: X -> Prop) (rel: relation X) :=
-  forall a (IWa: cond a)
-         b (IWb: cond b) (NEQ: a <> b),
-    rel a b \/ rel b a.
-
-Definition restr_subset X (cond: X -> Prop) (rel rel': relation X) :=
-  forall a (IWa: cond a)
-         b (IWb: cond b) (REL: rel a b),
-    rel' a b.
-
-Definition restr_rel X (cond : X -> Prop) (rel : relation X) : relation X :=
-  fun a b => rel a b /\ cond a /\ cond b.
-
-Definition restr_eq_rel A B (f : A -> B) rel x y :=
-  rel x y /\ f x = f y.
-
-Definition upward_closed (X: Type) (rel: relation X) (P: X -> Prop) :=
-  forall x y (REL: rel x y) (POST: P y), P x.
-
-Definition max_elt (X: Type) (rel: relation X) (a: X) :=
-  forall b (REL: rel a b), False.
-
-Notation "r 'UNION1' ( a , b )" := 
-  (fun x y => x = a /\ y = b \/ r x y) (at level 100). 
-
-Notation "a <--> b" := (same_relation _ a b)  (at level 110).
-
-
-(** Very basic properties of relations *)
-(******************************************************************************)
-
-
-Lemma clos_trans_mon A (r r' : relation A) a b :
-  clos_trans A r a b ->
-  (forall a b, r a b -> r' a b) ->
-  clos_trans A r' a b.
-Proof.
-  induction 1; ins; eauto using clos_trans.
-Qed.
-
-Lemma clos_refl_trans_mon A (r r' : relation A) a b :
-  clos_refl_trans A r a b ->
-  (forall a b, r a b -> r' a b) ->
-  clos_refl_trans A r' a b.
-Proof.
-  induction 1; ins; eauto using clos_refl_trans.
-Qed.
-
-
-Lemma clos_refl_transE A r a b :
-  clos_refl_trans A r a b <-> a = b \/ clos_trans A r a b.
-Proof.
-  split; ins; desf; vauto; induction H; desf; vauto. 
-Qed.
-
-Lemma clos_trans_in_rt A r a b :
-  clos_trans A r a b -> clos_refl_trans A r a b.
-Proof.
-  induction 1; vauto. 
-Qed.
-
-Lemma rt_t_trans A r a b c :
-  clos_refl_trans A r a b -> clos_trans A r b c -> clos_trans A r a c.
-Proof.
-  ins; induction H; eauto using clos_trans. 
-Qed.
-
-Lemma t_rt_trans A r a b c :
-  clos_trans A r a b -> clos_refl_trans A r b c -> clos_trans A r a c.
-Proof.
-  ins; induction H0; eauto using clos_trans. 
-Qed.
-
-
-Lemma t_step_rt A R x y : 
-  clos_trans A R x y <-> exists z, R x z /\ clos_refl_trans A R z y.
-Proof.
-  split; ins; desf.
-    by apply clos_trans_tn1 in H; induction H; desf; eauto using clos_refl_trans.
-  by rewrite clos_refl_transE in *; desf; eauto using clos_trans.
-Qed.
-
-Lemma t_rt_step A R x y : 
-  clos_trans A R x y <-> exists z, clos_refl_trans A R x z /\ R z y.
-Proof.
-  split; ins; desf.
-    by apply clos_trans_t1n in H; induction H; desf; eauto using clos_refl_trans.
-  by rewrite clos_refl_transE in *; desf; eauto using clos_trans.
-Qed.
-
-Lemma clos_trans_of_transitive A R (T: transitive A R) x y : 
-  clos_trans A R x y -> R x y.
-Proof.
-  induction 1; eauto.
-Qed.
-
-Lemma clos_trans_eq :
-  forall X (rel: relation X) Y (f : X -> Y) 
-         (H: forall a b (SB: rel a b), f a = f b) a b
-         (C: clos_trans _ rel a b),
-    f a = f b.
-Proof.
-  ins; induction C; eauto; congruence.
-Qed.
-
-Lemma trans_irr_acyclic : 
-  forall A R, irreflexive R -> transitive A R -> acyclic R.
-Proof.
-  eby repeat red; ins; eapply H, clos_trans_of_transitive. 
-Qed.
-
-Lemma restr_rel_trans :
-  forall X dom rel, transitive X rel -> transitive X (restr_rel dom rel).
-Proof.
-  unfold restr_rel; red; ins; desf; eauto.
-Qed.
-
-Lemma clos_trans_of_clos_trans1 :
-  forall X rel1 rel2 x y,
-    clos_trans X (fun a b => clos_trans _ rel1 a b \/ rel2 a b) x y <->
-    clos_trans X (fun a b => rel1 a b \/ rel2 a b) x y.
-Proof.
-  split; induction 1; desf; 
-  eauto using clos_trans, clos_trans_mon.
-Qed.
-
-Lemma upward_clos_trans:
-  forall X (rel: X -> X -> Prop) P,
-    upward_closed rel P -> upward_closed (clos_trans _ rel) P.
-Proof.
-  ins; induction 1; by eauto.
-Qed.
-
-Lemma max_elt_clos_trans:
-  forall X rel a b
-         (hmax: max_elt rel a)
-         (hclos: clos_trans X rel a b),
-    False.
-Proof.
-  ins. eapply clos_trans_t1n in hclos. induction hclos; eauto.
-Qed.
-
-Lemma is_total_restr :
-  forall X (dom : X -> Prop) rel,
-    is_total dom rel ->
-    is_total dom (restr_rel dom rel).
-Proof.
-  red; ins; eapply H in NEQ; eauto; desf; vauto.
-Qed.
-
-Lemma clos_trans_restrD :
-  forall X rel f x y, clos_trans X (restr_rel f rel) x y -> f x /\ f y.
-Proof.
-  unfold restr_rel; induction 1; ins; desf. 
-Qed.
-
-Lemma clos_trans_restr_eqD :
-  forall A rel B (f: A -> B) x y, clos_trans _ (restr_eq_rel f rel) x y -> f x = f y.
-Proof.
-  unfold restr_eq_rel; induction 1; ins; desf; congruence. 
-Qed.
-
-Lemma irreflexive_inclusion:
-  forall X (R1 R2: relation X),
-  inclusion X R1 R2 ->
-  irreflexive R2 ->
-  irreflexive R1.
-Proof.
-  unfold irreflexive, inclusion.
-  by eauto.
-Qed.
-
-Lemma clos_trans_inclusion:
-  forall X (R: relation X),
-  inclusion X R (clos_trans X R).
-Proof.
-  unfold inclusion. intros.
-  by econstructor; eauto.
-Qed.
-
-Lemma clos_trans_inclusion_clos_refl_trans:
-  forall X (R: relation X),
-  inclusion X (clos_trans X R) (clos_refl_trans X R).
-Proof.
-  unfold inclusion. intros.
-  induction H.
-    by eauto using rt_step.
-    by eauto using rt_trans.
-Qed.
-
-Lemma clos_trans_monotonic:
-  forall X (R1 R2: relation X),
-  inclusion X R1 R2 ->
-  inclusion X (clos_trans X R1) (clos_trans X R2).
-Proof.
-  intros.
-  intros x y hR1.
-  eapply clos_t1n_trans.
-  eapply clos_trans_t1n in hR1.
-  induction hR1.
-    by eauto using clos_t1n_trans, t1n_step.
-    (* [t1n_trans] is masked by a notation for [clos_t1n_trans] *)
-    by eauto using clos_t1n_trans, Relation_Operators.t1n_trans.
-Qed.
-
-(******************************************************************************)
-(** Set up setoid rewriting *)
-(******************************************************************************)
-
-Require Import Setoid.
-
-Lemma same_relation_refl: forall A, reflexive _ (same_relation A).
-Proof. split; ins. Qed.
-
-Lemma same_relation_sym: forall A, symmetric _ (same_relation A).
-Proof. unfold same_relation; split; ins; desf. Qed.
-
-Lemma same_relation_trans: forall A, transitive _ (same_relation A).
-Proof. unfold same_relation; split; ins; desf; red; eauto. Qed.
-
-Add Parametric Relation (X : Type) : (relation X) (same_relation X) 
- reflexivity proved by (@same_relation_refl X)
- symmetry proved by (@same_relation_sym X)
- transitivity proved by (@same_relation_trans X)
- as same_rel.
-
-Add Parametric Morphism X : (@union X) with 
-  signature (@same_relation X) ==> (@same_relation X) ==> (@same_relation X) as union_mor.
-Proof.
-  unfold same_relation, union; ins; desf; split; red; ins; desf; eauto.
-Qed.
-
-Add Parametric Morphism X P : (@restr_rel X P) with 
-  signature (@same_relation X) ==> (@same_relation X) as restr_rel_mor.
-Proof.
-  unfold same_relation, restr_rel; ins; desf; split; red; ins; desf; eauto.
-Qed.
-
-Add Parametric Morphism X : (@clos_trans X) with 
-  signature (@same_relation X) ==> (@same_relation X) as clos_trans_mor.
-Proof.
-  unfold same_relation; ins; desf; split; red; ins; desf; eauto using clos_trans_mon.
-Qed.
-
-Add Parametric Morphism X : (@clos_refl_trans X) with 
-  signature (@same_relation X) ==> (@same_relation X) as clos_relf_trans_mor.
-Proof.
-  unfold same_relation; ins; desf; split; red; ins; desf; eauto using clos_refl_trans_mon.
-Qed.
-
-Add Parametric Morphism X : (@irreflexive X) with 
-  signature (@same_relation X) ==> iff as irreflexive_mor.
-Proof.
-  unfold same_relation; ins; desf; split; red; ins; desf; eauto using clos_refl_trans_mon.
-Qed.
-
-Add Parametric Morphism X : (@acyclic X) with 
-  signature (@same_relation X) ==> iff as acyclic_mor.
-Proof.
-  unfold acyclic; ins; rewrite H; reflexivity.
-Qed.
-
-
-Lemma same_relation_restr X (f : X -> Prop) rel rel' :
-   (forall x (CONDx: f x) y (CONDy: f y), rel x y <-> rel' x y) ->
-   (restr_rel f rel <--> restr_rel f rel').
-Proof.
-  unfold restr_rel; split; red; ins; desf; rewrite H in *; eauto.
-Qed.
-
-Lemma union_restr X f rel rel' :
-  union X (restr_rel f rel) (restr_rel f rel')
-  <--> restr_rel f (union _ rel rel').
-Proof.
-  split; unfold union, restr_rel, inclusion; ins; desf; eauto.
-Qed.
-
-Lemma clos_trans_restr X f rel (UC: upward_closed rel f) :
-  clos_trans X (restr_rel f rel) 
-  <--> restr_rel f (clos_trans _ rel).
-Proof.
-  split; unfold union, restr_rel, inclusion; ins; desf; eauto.
-    split; [|by apply clos_trans_restrD in H].
-    by eapply clos_trans_mon; eauto; unfold restr_rel; ins; desf.
-  clear H0; apply clos_trans_tn1 in H.
-  induction H; eauto 10 using clos_trans.
-Qed.
-
-
-(******************************************************************************)
-(** ** Lemmas about cycles *)
-(******************************************************************************)
-
-Lemma path_decomp_u1 X (rel : relation X) a b c d : 
-  clos_trans X (rel UNION1 (a, b)) c d ->
-  clos_trans X rel c d \/ 
-  clos_refl_trans X rel c a /\ clos_refl_trans X rel b d.
-Proof.
-  induction 1; desf; eauto using clos_trans, clos_refl_trans, clos_trans_in_rt.
-Qed.
-
-Lemma cycle_decomp_u1 X (rel : relation X) a b c : 
-  clos_trans X (rel UNION1 (a, b)) c c ->
-  clos_trans X rel c c \/ clos_refl_trans X rel b a.
-Proof.
-  ins; apply path_decomp_u1 in H; desf; eauto using clos_refl_trans.
-Qed.
-
-Lemma path_decomp_u_total :
-  forall X rel1 dom rel2 (T: is_total dom rel2) 
-    (D: forall a b (REL: rel2 a b), dom a /\ dom b) x y
-    (C: clos_trans X (fun a b => rel1 a b \/ rel2 a b) x y),
-    clos_trans X rel1 x y \/
-    (exists m n, 
-      clos_refl_trans X rel1 x m /\ clos_trans X rel2 m n /\ clos_refl_trans X rel1 n y) \/
-    (exists m n, 
-      clos_refl_trans X rel1 m n /\ clos_trans X rel2 n m).
-Proof.
-  ins; induction C; desf; eauto 8 using rt_refl, clos_trans.
-  by right; left; exists m, n; eauto using clos_trans_in_rt, rt_trans.
-  by right; left; exists m, n; eauto using clos_trans_in_rt, rt_trans.
-
-  destruct (classic (m = n0)) as [|NEQ]; desf.
-  by right; left; exists m0, n; eauto using t_trans, rt_trans.
-  eapply T in NEQ; desf.
-    by right; right; exists n0, m; eauto 8 using clos_trans, rt_trans.
-    by right; left; exists m0, n; eauto 8 using clos_trans, rt_trans.
-    by apply t_step_rt in IHC0; desf; eapply D in IHC0; desf.
-    by apply t_rt_step in IHC4; desf; eapply D in IHC6; desf.
-Qed.
-
-Lemma cycle_decomp_u_total :
-  forall X rel1 dom rel2 (T: is_total dom rel2) 
-    (D: forall a b (REL: rel2 a b), dom a /\ dom b) x
-    (C: clos_trans X (fun a b => rel1 a b \/ rel2 a b) x x),
-    clos_trans X rel1 x x \/
-    (exists m n, clos_refl_trans X rel1 m n /\ clos_trans X rel2 n m).
-Proof.
-  ins; exploit path_decomp_u_total; eauto; ins; desf; eauto 8 using rt_trans.
-Qed.
-
-Lemma clos_trans_disj_rel :
-  forall X (rel rel' : relation X)
-    (DISJ: forall x y (R: rel x y) z (R': rel' y z), False) x y
-    (R: clos_trans _ rel x y) z
-    (R': clos_trans _ rel' y z),
-    False.
-Proof.
-  ins; induction R; eauto; induction R'; eauto.
-Qed.
-
-Lemma path_decomp_u_1 :
-  forall X (rel rel' : relation X)
-    (DISJ: forall x y (R: rel x y) z (R': rel' y z), False) x y
-    (T: clos_trans X (union X rel rel') x y),
-    clos_trans _ rel x y \/ clos_trans _ rel' x y
-    \/ exists z, clos_trans _ rel' x z /\ clos_trans _ rel z y.
-Proof.
-  unfold union; ins.
- induction T; desf; eauto 6 using clos_trans;
-   try by exfalso; eauto using clos_trans_disj_rel.
-Qed.
-
-Lemma cycle_decomp_u_1 :
-  forall X (rel rel' : relation X)
-    (DISJ: forall x y (R: rel x y) z (R': rel' y z), False) x
-    (T: clos_trans X (union X rel rel') x x),
-    clos_trans _ rel x x \/ clos_trans _ rel' x x. 
-Proof.
-  ins; exploit path_decomp_u_1; eauto; ins; desf; eauto.
-  exfalso; eauto using clos_trans_disj_rel.
-Qed.
-
-Lemma cycle_disj :
-  forall X (rel : relation X)
-    (DISJ: forall x y (R: rel x y) z (R': rel y z), False) x
-    (T: clos_trans X rel x x), False.
-Proof.
-  ins; inv T; eauto using clos_trans_disj_rel.
-Qed.
-
-Lemma clos_trans_restr_trans_mid : 
-  forall X (rel rel' : relation X) f x y
-    (A : clos_trans _ (restr_rel f (fun x y => rel x y \/ rel' x y)) x y)
-    z (B : rel y z) w
-    (C : clos_trans _ (restr_rel f (fun x y => rel x y \/ rel' x y)) z w),
-    clos_trans _ (restr_rel f (fun x y => rel x y \/ rel' x y)) x w.
-Proof.
-  ins; eapply t_trans, t_trans; vauto.
-  eapply t_step; repeat split; eauto.
-    by apply clos_trans_restrD in A; desc.
-  by apply clos_trans_restrD in C; desc.
-Qed.
-
-Lemma clos_trans_restr_trans_cycle : 
-  forall X (rel rel' : relation X) f x y
-    (A : clos_trans _ (restr_rel f (fun x y => rel x y \/ rel' x y)) x y)
-    (B : rel y x),
-    clos_trans _ (restr_rel f (fun x y => rel x y \/ rel' x y)) x x.
-Proof.
-  ins; eapply t_trans, t_step; eauto. 
-  by red; apply clos_trans_restrD in A; desf; auto.
-Qed.
-
-
-Lemma restr_eq_union : 
-  forall X (rel rel' : relation X) B (f: X -> B) x y
-         (R: forall x y, rel' x y -> f x = f y),
-   restr_eq_rel f (fun x y => rel x y \/ rel' x y) x y <->
-   restr_eq_rel f rel x y \/ rel' x y.
-Proof.
-  unfold restr_eq_rel; ins; intuition.
-Qed.
-
-Lemma clos_trans_restr_eq_union : 
-  forall X (rel rel' : relation X) B (f: X -> B)
-         (R: forall x y, rel' x y -> f x = f y),
-   clos_trans _ (restr_eq_rel f (fun x y => rel x y \/ rel' x y)) <-->
-   clos_trans _ (fun x y => restr_eq_rel f rel x y \/ rel' x y).
-Proof.
-  split; red; ins; eapply clos_trans_mon; eauto; ins; instantiate;
-  rewrite restr_eq_union in *; eauto.
-Qed.
-
-Lemma acyclic_mon X (rel rel' : relation X) :
-  acyclic rel -> inclusion _ rel' rel -> acyclic rel'.
-Proof.
-  eby repeat red; ins; eapply H, clos_trans_mon.
-Qed. 
-
-(** Extension of a partial order to a total order *)
-
-Section one_extension.
-
-  Variable X : Type.
-  Variable elem : X.
-  Variable rel : relation X.
-
-  Definition one_ext : relation X := 
-    fun x y =>
-      clos_trans _ rel x y 
-      \/ clos_refl_trans _ rel x elem /\ ~ clos_refl_trans _ rel y elem.
-
-  Lemma one_ext_extends x y : rel x y -> one_ext x y. 
-  Proof. vauto. Qed.
-
-  Lemma one_ext_trans : transitive _ one_ext.
-  Proof. 
-    red; ins; unfold one_ext in *; desf; desf; 
-      intuition eauto using clos_trans_in_rt, t_trans, rt_trans.
-  Qed.
- 
-  Lemma one_ext_irr : acyclic rel -> irreflexive one_ext.
-  Proof.
-    red; ins; unfold one_ext in *; desf; eauto using clos_trans_in_rt.
-  Qed.
-
-  Lemma one_ext_total_elem : 
-    forall x, x <> elem -> one_ext elem x \/ one_ext x elem.
-  Proof.
-    unfold one_ext; ins; rewrite !clos_refl_transE; tauto.
-  Qed.
-
-End one_extension.
-
-Fixpoint tot_ext X (dom : list X) (rel : relation X) : relation X :=
-  match dom with 
-    | nil => clos_trans _ rel
-    | x::l => one_ext x (tot_ext l rel) 
-  end.
-
-Lemma tot_ext_extends : 
-  forall X dom (rel : relation X) x y, rel x y -> tot_ext dom rel x y. 
-Proof. 
-  induction dom; ins; eauto using t_step, one_ext_extends.
-Qed.
-
-Lemma tot_ext_trans : forall X dom rel, transitive X (tot_ext dom rel).
-Proof. 
-  induction dom; ins; vauto; apply one_ext_trans. 
-Qed.
-
-Lemma tot_ext_irr : 
-  forall X (dom : list X) rel, acyclic rel -> irreflexive (tot_ext dom rel).
-Proof.
-  induction dom; ins.
-  apply one_ext_irr, trans_irr_acyclic; eauto using tot_ext_trans.
-Qed.
-
-(*Lemma tot_ext_total : 
-  forall X (dom : list X) rel, is_total (fun x => In x dom) (tot_ext dom rel).
-Proof.
-  induction dom; red; ins; desf.
-  eapply one_ext_total_elem in NEQ; desf; eauto.
-  eapply nesym, one_ext_total_elem in NEQ; desf; eauto.
-  eapply IHdom in NEQ; desf; eauto using one_ext_extends.
-Qed.*)
-
-Lemma tot_ext_inv :
-  forall X dom rel (x y : X),
-    acyclic rel -> tot_ext dom rel x y -> ~ rel y x.
-Proof.
-  red; ins; eapply tot_ext_irr, tot_ext_trans, tot_ext_extends; eauto.
-Qed.
-
-
-(** Misc properties *)
-(******************************************************************************)
-
-
-Lemma clos_trans_imm :
-  forall X (R : relation X) (I: irreflexive R) 
-         (T: transitive _ R) L (ND: NoDup L) a b
-         (D: forall c, R a c -> R c b -> In c L)
-         (REL: R a b),
-    clos_trans _ (immediate R) a b.
-Proof.
-  intros until 3; induction ND; ins; vauto.
-  destruct (classic (R a x /\ R x b)) as [|N]; desf;
-    [apply t_trans with x|]; eapply IHND; ins;
-    exploit (D c); eauto; intro; desf; exfalso; eauto.
-Qed.
-
-
-(** Remove duplicate list elements (classical) *)
-(******************************************************************************)
-
-Require Import extralib.
-
-Fixpoint undup A dec (l: list A) :=
-  match l with nil => nil
-    | x :: l =>
-      if In_dec dec x l then undup dec l else x :: undup dec l
-  end.
-
-Lemma In_undup X dec (x: X) l : In x (undup dec l) <-> In x l.
-Proof.
-  induction l; ins; des_if; ins; rewrite IHl; split; ins; desf; vauto.
-Qed.
-
-Lemma NoDup_undup X dec (l : list X) : NoDup (undup dec l).
-Proof.
-  induction l; ins; desf; constructor; eauto; rewrite In_undup; eauto. 
-Qed.
-
-
-Lemma clos_trans_imm2 :
-  forall X (dec : forall x y : X, {x = y} + {x <> y}) 
-         (R : relation X) (I: irreflexive R) 
-         (T: transitive _ R) L a b
-         (D: forall c, R a c -> R c b -> In c L)
-         (REL: R a b),
-    clos_trans _ (immediate R) a b.
-Proof.
-  ins; eapply clos_trans_imm with (L := undup dec L); ins;
-  try rewrite In_undup; eauto using NoDup_undup.
-Qed.
-
-
-
-
-Lemma total_immediate_unique:
-  forall X (eq_X_dec: forall (x y: X), {x=y} + {x<>y}) (rel: X -> X -> Prop) (P: X -> Prop)
-         (Tot: is_total P rel)
-         a b c (pa: P a) (pb: P b) (pc: P c)
-         (iac: immediate rel a c)
-         (ibc: immediate rel b c),
-    a = b.
-Proof.
-  ins.
-  destruct (eq_X_dec a b); eauto.
-  exfalso.
-  unfold immediate in *; desf.
-  eapply Tot in n; eauto.
-  desf; eauto.
-Qed.
-

JobDefs.v

-Require Import TaskDefs helper ssrnat ssrbool eqtype.  
-
-Module Job.
-
-  Section ValidJob.
-
-    Context {Job: eqType}.
-    Variable job_cost: Job -> nat.
-
-    Variable j: Job.
-
-    Definition job_cost_positive (j: Job) := job_cost j > 0.
-
-  End ValidJob.
-
-  Section ValidRealtimeJob.
-
-    Context {Job: eqType}.
-    Variable job_cost: Job -> nat.
-    Variable job_deadline: Job -> nat.
-    
-    Variable j: Job.
-
-    Definition job_cost_le_deadline := job_cost j <= job_deadline j.
-    Definition job_deadline_positive := job_deadline j > 0.
-        
-    Definition valid_realtime_job :=
-      job_cost_positive job_cost j /\
-      job_cost_le_deadline /\
-      job_deadline_positive.
-
-  End ValidRealtimeJob.
-
-  Section ValidSporadicTaskJob.
-
-    Context {sporadic_task: eqType}.
-    Variable task_cost: sporadic_task -> nat.
-    Variable task_deadline: sporadic_task -> nat.
-    
-    Context {Job: eqType}.
-    Variable job_cost: Job -> nat.
-    Variable job_deadline: Job -> nat.
-    Variable job_task: Job -> sporadic_task.
-    
-    Variable j: Job.
-
-    Definition job_cost_le_task_cost :=
-      job_cost j <= task_cost (job_task j).
-    Definition job_deadline_eq_task_deadline :=
-      job_deadline j = task_deadline (job_task j).
-
-    Definition valid_sporadic_job :=
-      valid_realtime_job job_cost job_deadline j /\
-      job_cost_le_task_cost /\
-      job_deadline_eq_task_deadline.
-
-  End ValidSporadicTaskJob.
-
-  Section ValidSporadicTaskJobWithJitter.
-
-    Context {sporadic_task: eqType}.
-    Variable task_cost: sporadic_task -> nat.
-    Variable task_deadline: sporadic_task -> nat.
-    Variable task_jitter: sporadic_task -> nat.
-    
-    Context {Job: eqType}.
-    Variable job_cost: Job -> nat.
-    Variable job_deadline: Job -> nat.
-    Variable job_task: Job -> sporadic_task.
-    Variable job_jitter: Job -> nat.
-    
-    Variable j: Job.
-
-    Definition job_jitter_leq_task_jitter :=
-      job_jitter j <= task_jitter (job_task j).
-
-    Let j_is_valid_job :=
-      valid_sporadic_job task_cost task_deadline job_cost job_deadline job_task j.
-
-    Definition valid_sporadic_job_with_jitter :=
-      j_is_valid_job /\ job_jitter_leq_task_jitter.
-
-  End ValidSporadicTaskJobWithJitter.
-
-End Job.
\ No newline at end of file

LICENSE

+BSD 2-Clause License
+
+Copyright (c) 2014–2022, The Prosa Project & Contributors
+All rights reserved.
+
+Redistribution and use in source and binary forms, with or without
+modification, are permitted provided that the following conditions are met:
+
+* Redistributions of source code must retain the above copyright notice, this
+  list of conditions and the following disclaimer.
+
+* Redistributions in binary form must reproduce the above copyright notice,
+  this list of conditions and the following disclaimer in the documentation
+  and/or other materials provided with the distribution.
+
+THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS "AS IS"
+AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED TO, THE
+IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR PURPOSE ARE
+DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT HOLDER OR CONTRIBUTORS BE LIABLE
+FOR ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL, EXEMPLARY, OR CONSEQUENTIAL
+DAMAGES (INCLUDING, BUT NOT LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR
+SERVICES; LOSS OF USE, DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER
+CAUSED AND ON ANY THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY,
+OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE
+OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.

Makefile.coq.local

+# Prosa: include pretty documentation targets
+include scripts/coqdocjs/Makefile.coqdocjs
+include scripts/Makefile.alectryon
+
+# Hack to enable esy support:
+#
+# In the esy container, $HOME is hidden, but this causes Coq to complain.
+# We thus include a dummy $HOME value.
+HOME ?= $(DESTDIR)
+export HOME