From 37747a6c990a6162368efaa0789d092cbc130846 Mon Sep 17 00:00:00 2001
From: k32 <10274441+k32@users.noreply.github.com>
Date: Sun, 1 Dec 2024 21:44:56 +0100
Subject: [PATCH] Change order of the arguments in Trace and CanonicalTrace

---
 theories/Commutativity.v  |  45 ----
 theories/Foundations.v    |  72 +++---
 theories/Generator.v      | 523 --------------------------------------
 theories/Handlers/Mutex.v |   6 +-
 4 files changed, 37 insertions(+), 609 deletions(-)
 delete mode 100644 theories/Commutativity.v
 delete mode 100644 theories/Generator.v

diff --git a/theories/Commutativity.v b/theories/Commutativity.v
deleted file mode 100644
index d6c81ba..0000000
--- a/theories/Commutativity.v
+++ /dev/null
@@ -1,45 +0,0 @@
-(* SLOT, a formally verified model-checker
-   Copyright (C) 2019-2021  k32
-
-   This program is free software: you can redistribute it and/or modify
-   it under the terms of the GNU General Public License as published by
-   the Free Software Foundation, version 3 of the License.
-
-   This program is distributed in the hope that it will be useful,
-   but WITHOUT ANY WARRANTY; without even the implied warranty of
-   MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
-   GNU General Public License for more details.
-
-   You should have received a copy of the GNU General Public License
-   along with this program.  If not, see <https://www.gnu.org/licenses/>.
- *)
-
-(** * Commutativity of trace elements *)
-From Coq Require Import
-     List
-     Program
-     Logic.Classical_Prop
-     Logic.Decidable
-     Classes.RelationClasses.
-
-Import ListNotations.
-
-From SLOT Require Import
-     Foundations.
-
-Section events_commute.
-  (** ** Commutativity of trace elements
-   *)
-  Context `{StateSpace}.
-
-  Definition events_commute (e1 e2 : Event) :=
-    forall (s s' : State),
-      ReachableByTrace s [e1; e2] s' <-> ReachableByTrace s [e2; e1] s'.
-
-  Global Instance events_commuteSymm : Symmetric events_commute.
-  Proof.
-    intros a b Hab s s''.
-    unfold events_commute in *. specialize (Hab s s'').
-    now symmetry in Hab.
-  Qed.
-End events_commute.
diff --git a/theories/Foundations.v b/theories/Foundations.v
index d20eb10..ff34f67 100644
--- a/theories/Foundations.v
+++ b/theories/Foundations.v
@@ -105,14 +105,13 @@ executing a trace [te :: trace], transitioning the system from [s] to
 Section state_reachability.
   Context `{HT : TransitionSystem}.
 
-  Inductive Trace : list Label -> State -> State -> Prop :=
+  Inductive Trace : State -> State -> list Label -> Prop :=
   | tr_nil : forall s,
-      Trace [] s s
+      Trace s s []
   | tr_cons : forall s s' s'' label trace,
       future s ~[label]~> s' ->
-      Trace trace s' s'' ->
-      Trace (label :: trace) s s''.
-
+      Trace s' s'' trace ->
+      Trace s s'' (label :: trace).
 
   (** ** Hoare logic of traces
 
@@ -124,7 +123,7 @@ Section state_reachability.
                          (trace         : list Label)
                          (postcondition : State -> Prop) :=
     forall s s',
-      Trace trace s s' -> precondition s ->
+      Trace s s' trace -> precondition s ->
       postcondition s'.
 
   (** ** Hoare triple for terminal states
@@ -169,7 +168,7 @@ Section state_invariant.
 
   Definition StateInvariant (trace : list Label) : Prop :=
     forall s s',
-      Trace invTransSys trace s s'.
+      Trace invTransSys s s' trace.
 End state_invariant.
 
 (** * Ensembles of traces
@@ -198,11 +197,11 @@ Section trace_ensembles.
 
   Definition OccupiedTraceEnsemble (e : TraceEnsemble) : Prop :=
     exists t s s',
-      e t -> Trace HT t s s'.
+      e t -> Trace HT s s' t.
 
   Definition FullyOccupiedTraceEnsemble (e : TraceEnsemble) : Prop :=
     forall t,
-      e t -> exists s s', Trace HT t s s'.
+      e t -> exists s s', Trace HT s s' t.
 End trace_ensembles.
 
 Notation "'-{{' a '}}' e '{{' b '}}'" := (EHoareTriple a e b)(at level 40) : slot_scope.
@@ -217,7 +216,7 @@ Section commutativity.
 
     Definition labels_commute (l1 l2 : Label) : Prop :=
       forall (s s' : State),
-        Trace TS [l1; l2] s s' <-> Trace TS [l2; l1] s s'.
+        Trace TS s s' [l1; l2] <-> Trace TS s s' [l2; l1].
 
     Global Instance events_commuteSymm : Symmetric labels_commute.
     Proof.
@@ -235,8 +234,8 @@ Section trace_properties.
   in the state space for each intermediate step of the trace
   execution: *)
   Lemma trace_split : forall s s'' t1 t2,
-      Trace TS (t1 ++ t2) s s'' ->
-      exists s', Trace TS t1 s s' /\ Trace TS t2 s' s''.
+      Trace TS s s'' (t1 ++ t2) ->
+      exists s', Trace TS s s' t1 /\ Trace TS s' s'' t2.
   Proof with sauto.
     intros.
     generalize dependent s.
@@ -251,9 +250,9 @@ Section trace_properties.
 
   (** [trace_concat] lemma demonstrates that traces can be composed: *)
   Lemma trace_concat : forall s s' s'' t1 t2,
-      Trace TS t1 s s' ->
-      Trace TS t2 s' s'' ->
-      Trace TS (t1 ++ t2) s s''.
+      Trace TS s s' t1 ->
+      Trace TS s' s'' t2 ->
+      Trace TS s s'' (t1 ++ t2).
   Proof with sauto.
     intros.
     generalize dependent s.
@@ -261,9 +260,9 @@ Section trace_properties.
   Qed.
 
   Lemma trace_commutateive_permutation s s' t t' :
-    Trace TS t s s' ->
+    Trace TS s s' t ->
     RestrictedPermutation labels_commute t t' ->
-    Trace TS t' s s'.
+    Trace TS s s' t'.
   Proof with sauto.
     intros Hls Hperm.
     generalize dependent s.
@@ -282,8 +281,8 @@ Section trace_equivalence.
 
   Definition sufficient_replacement :=
     forall t s s', e t ->
-              Trace T t s s' ->
-              exists t', e' t' /\ Trace T t' s s'.
+              Trace T s s' t ->
+              exists t', e' t' /\ Trace T s s' t'.
 
   Definition sufficient_replacement_p :=
     forall t, e t ->
@@ -345,18 +344,18 @@ Section trans_prod.
     split; intros H.
     { inversion H. clear H. inversion H5. clear H5. inversion H10. clear H10. subst.
       destruct s' as [s'_l s'_r].
-      inversion_clear H2. inversion_clear H7.
+      inversion_clear H4. inversion_clear H9.
       destruct HT1 as [HT1 _]. destruct HT2 as [HT2 _].
-      assert (HT1p : Trace T1 [l1; l2] s_l s''_l) by sauto. specialize (HT1 HT1p). clear HT1p.
-      assert (HT2p : Trace T2 [l1; l2] s_r s''_r) by sauto. specialize (HT2 HT2p). clear HT2p.
+      assert (HT1p : Trace T1 s_l s''_l [l1; l2]) by sauto. specialize (HT1 HT1p). clear HT1p.
+      assert (HT2p : Trace T2 s_r s''_r [l1; l2] ) by sauto. specialize (HT2 HT2p). clear HT2p.
       sauto.
     }
     { inversion H. clear H. inversion H5. clear H5. inversion H10. clear H10. subst.
       destruct s' as [s'_l s'_r].
-      inversion_clear H2. inversion_clear H7.
+      inversion_clear H4. inversion_clear H9.
       destruct HT1 as [_ HT1]. destruct HT2 as [_ HT2].
-      assert (HT1p : Trace T1 [l2; l1] s_l s''_l) by sauto. specialize (HT1 HT1p). clear HT1p.
-      assert (HT2p : Trace T2 [l2; l1] s_r s''_r) by sauto. specialize (HT2 HT2p). clear HT2p.
+      assert (HT1p : Trace T1 s_l s''_l [l2; l1]) by sauto. specialize (HT1 HT1p). clear HT1p.
+      assert (HT2p : Trace T2 s_r s''_r [l2; l1]) by sauto. specialize (HT2 HT2p). clear HT2p.
       sauto.
     }
   Qed.
@@ -455,14 +454,14 @@ Section canonical_order.
       - simpl. apply can_follow_dec.
     Qed.
 
-    Inductive CanonicalTrace : list Label -> State -> State -> Prop :=
+    Inductive CanonicalTrace : State -> State -> list Label -> Prop :=
     | canontr_nil : forall s,
-        CanonicalTrace [] s s
+        CanonicalTrace s s []
     | canontr_cons : forall s s' s'' label trace,
         future s ~[label]~> s' ->
         can_follow_hd label trace ->
-        CanonicalTrace trace s' s'' ->
-        CanonicalTrace (label :: trace) s s''.
+        CanonicalTrace s' s'' trace ->
+        CanonicalTrace s s'' (label :: trace).
 
     Lemma can_follow_hd_eq {te t1 t2} (Hfoll : can_follow_hd te t1) (Hhd : hd_error t1 = hd_error t2) :
       can_follow_hd te t2.
@@ -475,9 +474,9 @@ Section canonical_order.
     Qed.
 
     Fixpoint canon_trace_add s s' s'' label t (Hlabel : future s ~[label]~> s')
-                             (Ht : CanonicalTrace t s' s'')
+                             (Ht : CanonicalTrace s' s'' t)
                              (Hfoll : ~can_follow_hd label t) {struct Ht} :
-      exists t', CanonicalTrace t' s s'' /\
+      exists t', CanonicalTrace s s'' t' /\
                  RestrictedPermutation labels_commute (label :: t) t' /\
                  (hd_error t = hd_error t').
     Proof with sauto.
@@ -498,7 +497,7 @@ Section canonical_order.
           + firstorder.
         }
         (* Use label commutativity to derive states visited by [label'; label] path: *)
-        assert (Hll' : Trace T [label; label'] s s_). {
+        assert (Hll' : Trace T s s_ [label; label']). {
           constructor 2 with s'. assumption. constructor 2 with s_. assumption. constructor.
         }
         apply Hlcomm in Hll'.
@@ -509,7 +508,7 @@ Section canonical_order.
           repeat split.
           * constructor 2 with s'0...
           * constructor. assumption.
-        + specialize (canon_trace_add s'0 s_ s'' label t' H7 Ht' Hfoll'').
+        + specialize (canon_trace_add s'0 s_ s'' label t' H9 Ht' Hfoll'').
           destruct canon_trace_add as [t'' [Ht'' [Hcomm'' Hhd'']]].
           exists (label' :: t'').
           repeat split.
@@ -518,9 +517,9 @@ Section canonical_order.
           * sauto.
     Defined.
 
-    Fixpoint canon_trace_ (s s'' : State) (t : list Label) (Ht : Trace T t s s'')
+    Fixpoint canon_trace_ (s s'' : State) (t : list Label) (Ht : Trace T s s'' t)
           {struct Ht} :
-      exists t' : list Label, CanonicalTrace t' s s'' /\ RestrictedPermutation labels_commute t t'.
+      exists t' : list Label, CanonicalTrace s s'' t' /\ RestrictedPermutation labels_commute t t'.
     Proof with sauto.
       destruct Ht.
       - exists []...
@@ -534,7 +533,7 @@ Section canonical_order.
     Qed.
 
     Theorem canonicalize_trace s s' :
-      sufficient_replacement_p (fun t => Trace T t s s') (fun t => CanonicalTrace t s s').
+      sufficient_replacement_p (Trace T s s') (CanonicalTrace s s').
     Proof.
       intros t Ht.
       now apply canon_trace_.
@@ -609,7 +608,6 @@ Notation "'call' V '<-' I ; C" := (I (fun V => C))
 (** ** Process ID in SLOT is a natural number: *)
 Definition PID := nat.
 
-
 (** * Concurrency
 
  *)
diff --git a/theories/Generator.v b/theories/Generator.v
deleted file mode 100644
index 9702585..0000000
--- a/theories/Generator.v
+++ /dev/null
@@ -1,523 +0,0 @@
-(* SLOT, a formally verified model-checker
-   Copyright (C) 2019-2021, 2023  k32
-
-   This program is free software: you can redistribute it and/or modify
-   it under the terms of the GNU General Public License as published by
-   the Free Software Foundation, version 3 of the License.
-
-   This program is distributed in the hope that it will be useful,
-   but WITHOUT ANY WARRANTY; without even the implied warranty of
-   MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
-   GNU General Public License for more details.
-
-   You should have received a copy of the GNU General Public License
-   along with this program.  If not, see <https://www.gnu.org/licenses/>.
- *)
-
-(** * Ensembles that can be deconstructed one element at a time
- *)
-
-From Coq Require Import
-     List
-     Lia.
-
-Import ListNotations.
-
-From SLOT Require Import
-     Foundations
-     Commutativity
-     Properties
-     Tactics.
-
-From Hammer Require Import
-     Tactics.
-
-Class Generator TE g :=
-  { gen_step : g -> option (g * TE) -> Prop
-  }.
-
-Open Scope slot_scope.
-
-Notation "A '~~>' B & C" := (gen_step A (Some (B, C))) (at level 20) : slot_scope.
-
-Notation "A '~~>x'" := (gen_step A None) (at level 20) : slot_scope.
-
-Section GenEnsemble.
-  (** Generator as an ensemble *)
-  Context {TE G : Type} `{Generator TE G}.
-
-  Inductive GenEnsemble (g : G) : @TraceEnsemble TE :=
-  | gen_ens_nil :
-      g ~~>x ->
-      GenEnsemble g []
-  | gen_ens_cons : forall g' te t,
-      g ~~> g' & te ->
-      GenEnsemble g' t ->
-      GenEnsemble g (te :: t).
-End GenEnsemble.
-
-Section gen_commutativity.
-  Context {TE} Gen `{Generator (ProcessEvent TE) Gen}.
-
-  Definition different_processes {Evt} (te1 te2 : ProcessEvent Evt) :=
-    match te1, te2 with
-      pid1 @ _, pid2 @ _ => pid1 <> pid2
-    end.
-
-  Definition generator_events_commute :=
-    forall g g' g'' te1 te2,
-      different_processes te1 te2 ->
-      g ~~> g' & te1 ->
-      g' ~~> g'' & te2 ->
-      exists g_,
-        g ~~> g_ & te2 /\ g_ ~~> g'' & te1.
-End gen_commutativity.
-
-Section list_defn.
-  Context (A : Type).
-
-  Let G := list A.
-
-  Inductive ListGenStep : G -> option (G * A) -> Prop :=
-  | lgen_nil :
-      ListGenStep [] None
-  | lgen_cons : forall te t,
-      ListGenStep (te :: t) (Some (t, te)).
-
-  Global Instance listGenerator : Generator A G :=
-    { gen_step := ListGenStep }.
-
-  Lemma list_gen_correct : forall l l',
-      GenEnsemble l l' ->
-      l = l'.
-  Proof.
-    intros.
-    induction H.
-    - now inversion H.
-    - subst. now inversion_clear H.
-  Qed.
-End list_defn.
-
-Section process.
-  Section defn.
-    Context {Request : Type} {Reply : Request -> Type} {Return : Type}.
-
-    Let TE := IOp Request Reply.
-    Let t := @Program Request Reply Return.
-
-    Definition ThreadGenStep (gen : t) (next : option (t * TE)) : Prop :=
-      match gen with
-      | p_dead _ =>
-          next = None
-      | p_cont req cont =>
-          exists (ret : Reply req),
-          next = Some (cont ret, ret <~ req)
-      end.
-
-    Global Instance processGen : Generator TE t :=
-    { gen_step := ThreadGenStep }.
-  End defn.
-
-  Section tests.
-    Let Req := bool.
-    Let Rep req :=
-      match req with
-      | true => nat
-      | false => bool
-      end.
-
-    Let my_prog : @Program Req Rep True :=
-      do x <- true;
-      match x with
-      | 0 =>
-        do _ <- false;
-        return I
-      | _ =>
-        do _ <- true;
-        return I
-      end.
-
-    Goal forall t,
-        GenEnsemble my_prog t ->
-        exists x y z,
-          t = [0 <~ true; x <~ false] \/
-          t = [S y <~ true; z <~ true].
-    Proof.
-      intros. subst my_prog. simpl.
-      sauto.
-    Qed.
-  End tests.
-End process.
-
-Section singleton_process.
-  Context {Gen State Event} `{StateSpace State (ProcessEvent Event)} `{Generator Event Gen}.
-
-  Record SingletonProcess :=
-    singleton_process { _ : Gen }.
-
-  Inductive SingletonStep : SingletonProcess -> option (SingletonProcess * (ProcessEvent Event)) -> Prop :=
-  | wrs_nil : forall g,
-      g ~~>x ->
-      SingletonStep (singleton_process g) None
-  | wrp_cons : forall g g' evt,
-      g ~~> g' & evt ->
-      SingletonStep (singleton_process g) (Some (singleton_process g', 0 @ evt)).
-
-  Global Instance singletonGen : Generator (ProcessEvent Event) SingletonProcess :=
-    { gen_step := SingletonStep }.
-
-  Lemma singleton_gen_comm :
-    generator_events_commute SingletonProcess.
-  Proof.
-    intros g g' g'' te1 te2 Hpids Hg Hg'.
-    exfalso.
-    inversion Hg; inversion Hg'; subst.
-    sauto.
-  Qed.
-End singleton_process.
-
-#[export] Hint Resolve singleton_gen_comm : slot.
-
-Section parallel_defn.
-  Context {TE G__l G__r : Type} `{Generator TE G__l} `{Generator (ProcessEvent TE) G__r}.
-
-  Record Parallel :=
-    parallel
-      { gp_l : G__l;
-        gp_r : G__r
-      }.
-
-  Inductive ParallelStep : Parallel -> option (Parallel * (ProcessEvent TE)) -> Prop :=
-  | g_left : forall te g__l g__l' g__r,
-      g__l ~~> g__l' & te ->
-      ParallelStep (parallel g__l g__r) (Some (parallel g__l' g__r, 0 @ te))
-  | g_right : forall te pid g__l g__r g__r',
-      g__r ~~> g__r' & (pid @ te) ->
-      ParallelStep (parallel g__l g__r) (Some (parallel g__l g__r', S pid @ te))
-  | g_nil : forall g__l g__r,
-      g__l ~~>x ->
-      g__r ~~>x ->
-      ParallelStep (parallel g__l g__r) None.
-
-  Global Instance genPairGen : Generator (ProcessEvent TE) Parallel :=
-    { gen_step := ParallelStep }.
-End parallel_defn.
-
-Infix "<||>" := parallel (right associativity, at level 101) : slot_scope.
-Notation "[| x |]" := (singleton_process x) : slot_scope.
-Notation "[| x ; .. ; y ; z |]" := (parallel x (.. (parallel y (singleton_process z)) ..)) : slot_scope.
-
-Section parallel_tests.
-  (* Check that all interleavings created by the ensemble are valid: *)
-  Goal forall t,
-      GenEnsemble [| [1; 2]; [3] |] t ->
-      t = [0 @ 1; 0 @ 2; 1 @ 3] \/
-      t = [0 @ 1; 1 @ 3; 0 @ 2] \/
-      t = [1 @ 3; 0 @ 1; 0 @ 2].
-  Proof.
-    intros. sauto.
-  Qed.
-
-  (* Check that it creates every interleaving: *)
-  Goal GenEnsemble [| [1; 2]; [3] |] [0 @ 1; 0 @ 2; 1 @ 3].
-  Proof.
-    constructor 2 with (g' := [| [2]; [3] |]).
-    - sauto.
-    - constructor 2 with (g' := [| []; [3] |]); sauto.
-  Qed.
-
-  Goal GenEnsemble [| [1; 2]; [3] |] [0 @ 1; 1 @ 3; 0 @ 2].
-  Proof.
-    constructor 2 with (g' := [| [2]; [3] |]).
-    - sauto.
-    - constructor 2 with (g' := [| [2] ; [] |] ); sauto.
-  Qed.
-
-  Goal GenEnsemble [| [1; 2] ; [3] |] [1 @ 3; 0 @ 1; 0 @ 2].
-  Proof.
-    constructor 2 with (g' := [| [1; 2] ; [] |]).
-    - sauto.
-    - constructor 2 with (g' := [| [2] ; [] |]); sauto.
-  Qed.
-
-  Goal forall t,
-      GenEnsemble [| [3] ; [1; 2] |] t ->
-      t = [1 @ 1; 1 @ 2; 0 @ 3] \/
-      t = [1 @ 1; 0 @ 3; 1 @ 2] \/
-      t = [0 @ 3; 1 @ 1; 1 @ 2].
-  Proof.
-    intros. sauto.
-  Qed.
-
-  (* Test interleavings of larger system *)
-  Goal forall t,
-      GenEnsemble [| [1; 2]; [3; 4] |] t ->
-      t = [0 @ 1; 0 @ 2; 1 @ 3; 1 @ 4] \/
-      t = [0 @ 1; 1 @ 3; 0 @ 2; 1 @ 4] \/
-      t = [0 @ 1; 1 @ 3; 1 @ 4; 0 @ 2] \/
-
-      t = [1 @ 3; 0 @ 1; 0 @ 2; 1 @ 4] \/
-      t = [1 @ 3; 0 @ 1; 1 @ 4; 0 @ 2] \/
-      t = [1 @ 3; 1 @ 4; 0 @ 1; 0 @ 2].
-  Proof.
-    intros. sauto.
-  Qed.
-
-  (* Test interleavings of a system with 3 processes *)
-  Goal forall t,
-      GenEnsemble [| [0]; [1]; [2] |] t ->
-      t = [0 @ 0; 1 @ 1; 2 @ 2] \/
-      t = [0 @ 0; 2 @ 2; 1 @ 1] \/
-
-      t = [1 @ 1; 0 @ 0; 2 @ 2] \/
-      t = [1 @ 1; 2 @ 2; 0 @ 0] \/
-
-      t = [2 @ 2; 1 @ 1; 0 @ 0] \/
-      t = [2 @ 2; 0 @ 0; 1 @ 1].
-  Proof.
-    intros. sauto.
-  Qed.
-End parallel_tests.
-
-Module better_parallel.
-  Section defn.
-    Context `{Hhan : IOHandler}.
-
-    Record Runnable :=
-      { pid : PID;
-        req : Request;
-        ret_t : Type;
-        cont : Reply req -> @Program Request Reply ret_t;
-      }.
-
-    Definition Processes := list Runnable.
-
-    Record Parallel :=
-      parallel
-        { last_pid : PID;
-          processes : Processes;
-        }.
-
-    Let TE := ProcessEvent (@IOp Request Reply).
-
-    Definition run_one (next : option (Parallel * TE)) (last_pid : PID) (r : Runnable) (remaining visited : Processes) : Prop :=
-      match r with
-        {| pid := pid; req := req; cont := cont |} =>
-          exists (rep : Reply req),
-          let r' := cont rep in
-          let pp' := match r' with
-                     | p_dead _ => visited ++ remaining
-                     | p_cont req cont => visited ++ ({| pid := pid; req := req; cont := cont |} :: remaining)
-                     end in
-          let g := {| last_pid := last_pid; processes := pp' |} in
-          next = Some (g, (pid @ rep <~ req))
-      end.
-
-    Fixpoint runit (next : option (Parallel * TE)) (last_pid : PID) (remaining visited : Processes) (acc : Prop) {struct remaining} :=
-      match remaining with
-      | [] => acc
-      | (r :: rest) =>
-          let acc := run_one next last_pid r rest visited \/ acc in
-          runit next last_pid rest (r :: visited) acc
-      end.
-
-    Definition ParallelStep (p : Parallel) (next : option (Parallel * TE)) : Prop :=
-      match p with
-        {| last_pid := last_pid; processes := pp |} =>
-          match p.(processes) with
-          | [] =>
-              next = None
-          | f :: rest =>
-              let acc := run_one next last_pid f rest [] in
-              runit next last_pid rest [f] acc
-          end
-      end.
-
-    Global Instance parGen : Generator TE Parallel :=
-      {| gen_step := ParallelStep |}.
-
-    Definition spawn {ret_t : Type} (prog : @Program Request Reply ret_t) (par : Parallel) : Parallel :=
-      match prog with
-      | p_dead _ => par
-      | p_cont req cont =>
-          match par with
-            {| last_pid := pid; processes := processes |} =>
-              let runnable := {| pid := pid; req := req; cont := cont |} in
-              {| last_pid := S pid;
-                processes := runnable :: processes
-              |}
-          end
-      end.
-
-    Definition empty := {| last_pid := 0; processes := [] |}.
-
-    Definition of_progs {Return : Type} (progs : list (@Program Request Reply Return)) : Parallel :=
-      fold_left (fun par prog => spawn prog par) progs empty.
-  End defn.
-
-  Section test.
-    Require Import Deterministic Handlers.
-    Let H := @Var.t nat.
-
-
-    Let prog : @Program (handler_request_t H) (handler_reply_t H) True :=
-          do r <- Var.read;
-          do _ <- Var.write 1;
-          return I.
-
-    Let pp := (spawn prog (spawn prog empty)).
-
-    Eval cbn in fun next => ParallelStep pp next.
-  End test.
-End better_parallel.
-
-From SLOT Require Import
-     Properties.
-
-From Coq Require Import
-     Classical_Prop.
-
-Section optimize.
-  Context {Gen State Event : Type}.
-  Let TE := (ProcessEvent Event).
-  Context `{Hssp : StateSpace State TE} `{Hgen : Generator TE Gen}.
-
-  Definition can_follow (te1 te2 : TE) : Prop :=
-    let (pid1, _) := te1 in
-    let (pid2, _) := te2 in
-    pid1 <= pid2 \/ not (events_commute te1 te2).
-
-  Definition can_follow_hd (te : TE) (t : list TE) : Prop :=
-    match t with
-    | [] => True
-    | hd :: _ => can_follow te hd
-    end.
-
-  Inductive GenEnsembleOpt (g : Gen) : @TraceEnsemble TE :=
-  | og_ens_nil :
-      g  ~~>x ->
-      GenEnsembleOpt g []
-  | og_ens_cons : forall g' te t,
-      g ~~> g' & te ->
-      can_follow_hd te t ->
-      GenEnsembleOpt g' t ->
-      GenEnsembleOpt g (te :: t).
-
-  Lemma can_follow_hd_eq {te t1 t2} (Hfoll : can_follow_hd te t1) (Hhd : hd_error t1 = hd_error t2) :
-    can_follow_hd te t2.
-  Proof.
-    intros.
-    unfold can_follow_hd in *.
-    destruct t1, t2; try reflexivity.
-    - exfalso. inversion Hhd.
-    - simpl in Hhd. injection Hhd as H. now subst.
-  Qed.
-
-  Fixpoint gen_ens_opt_add g g' te t (Hte : g ~~> g' & te)
-           (Ht : GenEnsembleOpt g' t)
-           (HG : generator_events_commute Gen)
-           (Hfoll : ~ can_follow_hd te t) {struct Ht} :
-    exists t', GenEnsembleOpt g t' /\ Permutation events_commute (te :: t) (t') /\
-            hd_error t = hd_error t'.
-  Proof with auto with slot.
-    destruct te as [pid evt].
-    inversion Ht as [ |g'' te' t' Hg'' Hte' Ht']; subst; clear Ht.
-    - exfalso. (* Hfoll cannot hold for an empty list *)
-      clear gen_ens_opt_add.
-      simpl in Hfoll. contradiction.
-    - destruct te' as [pid' evt'].
-      simpl in Hfoll. firstorder. apply NNPP in H0. rename H0 into Hcomm.
-      assert (Hpids : pid <> pid') by lia.
-      specialize (HG g g' g'' (pid @ evt) (pid' @ evt') Hpids) as Hgen_comm.
-      destruct Hgen_comm as [g_ [Hg_ Hg_']]...
-      destruct (classic (can_follow_hd (pid @ evt) t')) as [Hfoll' | Hfoll'].
-      + clear gen_ens_opt_add.
-        exists (pid' @ evt' :: pid @ evt :: t'). repeat split.
-        * constructor 2 with g_... sauto. constructor 2 with g''...
-        * now constructor.
-      + specialize (gen_ens_opt_add g_ g'' (pid @ evt) t' Hg_' Ht') as IH. clear gen_ens_opt_add.
-        destruct IH as [t'' [Ht'' [Hperm'' Hhd]]]...
-        exists (pid' @ evt' :: t''). repeat split.
-        * constructor 2 with g_...
-          eapply can_follow_hd_eq; eauto.
-        * apply perm_trans with (l' := pid' @ evt' :: pid @ evt :: t')...
-  Qed.
-
-  Fixpoint gen_ens_opt (g : Gen) (t : list TE) (Ht : GenEnsemble g t)
-           (HG : generator_events_commute Gen)
-           {struct Ht} :
-    exists t' : list TE, GenEnsembleOpt g t' /\ Permutation events_commute t t'.
-  Proof with auto with slot.
-    destruct Ht as [Hnil | g' te t Hte Ht].
-    - exists []. split; now constructor.
-    - apply gen_ens_opt in Ht. destruct Ht as [t' [Ht' Hperm]]; clear gen_ens_opt.
-      destruct (classic (can_follow_hd te t')).
-      + exists (te :: t'). split.
-        * constructor 2 with g'...
-        * now repeat constructor.
-      + eapply gen_ens_opt_add in Ht'; eauto.
-        destruct Ht' as [t'' [Ht'' [Hperm'' Hhd]]].
-        exists t''. split.
-        * assumption.
-        * apply perm_trans with (te :: t')...
-      + assumption.
-  Qed.
-
-  Theorem optimize_gen_p g
-    (HG : generator_events_commute Gen) :
-    sufficient_replacement_p (GenEnsemble g) (GenEnsembleOpt g).
-  Proof.
-    intros t Ht.
-    now apply gen_ens_opt.
-  Qed.
-
-  Theorem optimize_gen (g : Gen) P Q (HG : generator_events_commute Gen) :
-    -{{ P }} GenEnsembleOpt g {{ Q }} ->
-    -{{ P }} GenEnsemble g {{ Q }}.
-  Proof.
-    now apply ht_sufficient_replacement, comm_perm_sufficient_replacement, optimize_gen_p.
-  Qed.
-End optimize.
-
-Section parallel_gen_comm.
-  Context {State Event} `{StateSpace State (ProcessEvent Event)} {G1 G2}
-          `{Generator Event G1}
-          `{Generator (ProcessEvent Event) G2}.
-
-  Lemma parallel_gen_comm :
-    generator_events_commute G2 ->
-    generator_events_commute (@Parallel G1 G2).
-  Proof.
-    intros HG2 g g' g'' te1 te2 Hpids Hg Hg'.
-    destruct te1 as [pid1 evt1]. set (te1 := pid1 @ evt1).
-    destruct te2 as [pid2 evt2]. set (te2 := pid2 @ evt2).
-    simpl in Hpids.
-    inversion Hg; inversion Hg'; subst.
-    - exfalso. lia.
-    - sauto.
-    - sauto.
-    - assert (Hpids' : different_processes (pid @ evt1) (pid0 @ evt2)).
-      { simpl. lia. }
-      inversion H8; subst.
-      specialize (HG2 g__r g__r' g__r'0).
-      specialize (HG2 (pid @ evt1) (pid0 @ evt2) Hpids').
-      specialize (HG2 H4 H9).
-      sauto.
-  Qed.
-
-  Theorem parallel_processes_ht :
-    forall (P Q : State -> Prop) (g1 : G1) (g2 : G2),
-      generator_events_commute G2 ->
-      -{{ P }} GenEnsembleOpt (g1 <||> g2) {{ Q }} ->
-      -{{ P }} GenEnsemble (g1 <||> g2) {{ Q }}.
-  Proof.
-    intros *. intros HG2 Hht.
-    apply parallel_gen_comm in HG2.
-    specialize (optimize_gen (g1 <||> g2) P Q HG2 Hht) as Hopt.
-    assumption.
-  Qed.
-End parallel_gen_comm.
-
-#[export] Hint Unfold can_follow : slot.
-#[export] Hint Resolve singleton_gen_comm : slot.
-#[export] Hint Resolve parallel_gen_comm : slot.
diff --git a/theories/Handlers/Mutex.v b/theories/Handlers/Mutex.v
index e9dbd7e..ee10fb8 100644
--- a/theories/Handlers/Mutex.v
+++ b/theories/Handlers/Mutex.v
@@ -1,5 +1,5 @@
 (* SLOT, a formally verified model checker
-   Copyright (C) 2019-2023  k32
+   Copyright (C) 2019-2024  k32
 
    This program is free software: you can redistribute it and/or modify
    it under the terms of the GNU General Public License as published by
@@ -20,9 +20,7 @@ From Coq Require Import
 Import ListNotations.
 
 From SLOT Require Import
-     Foundations
-     Properties
-     Tactics.
+     Foundations.
 
 Section defs.
   Open Scope slot_scope.