Splitting system calls into two transitions

.gitignore

@@ -4,3 +4,4 @@ _build
 *~
 .lia.cache
 .aux
+rocq-ctree.opam

rocq-ctree.opam

@@ -0,0 +1,52 @@
+# This file is generated by dune, edit dune-project instead
+opam-version: "2.0"
+version: "2.0-dev"
+synopsis:
+  "Library for representing recursive, non-deterministic and impure programs with equational reasoning"
+maintainer: ["Yannick Zakowski"]
+authors: [
+  "Nicolas Chappe"
+  "Paul He"
+  "Ludovic Henrio"
+  "Yannick Zakowski"
+  "Steve Zdancewic"
+]
+license: "MIT"
+tags: [
+  "category:CS/Semantics and Compilation/Semantics"
+  "category:CS/Concurrency/Theory of concurrent systems"
+  "keyword:simulation"
+  "keyword:bisimilarity"
+  "keyword:coinduction up-to"
+  "keyword:process algebra"
+  "keyword:cooperative multithreading"
+  "logpath:CTree"
+]
+homepage: "https://github.com/vellvm/ctrees"
+bug-reports: "https://github.com/vellvm/ctrees/issues"
+depends: [
+  "dune" {>= "3.8"}
+  "rocq-core" {>= "9.0"}
+  "rocq-stdlib" {>= "9.0"}
+  "coq-ext-lib" {>= "0.11.3"}
+  "rocq-coinduction" {>= "1.21"}
+  "rocq-relation-algebra" {>= "1.8.0"}
+  "rocq-equations" {>= "1.3.1"}
+  "coq-itree" {>= "5.0"}
+  "odoc" {with-doc}
+]
+build: [
+  ["dune" "subst"] {dev}
+  [
+    "dune"
+    "build"
+    "-p"
+    name
+    "-j"
+    jobs
+    "@install"
+    "@runtest" {with-test}
+    "@doc" {with-doc}
+  ]
+]
+dev-repo: "git+https://github.com/vellvm/ctrees.git"

theories/CTree.v

@@ -5,8 +5,10 @@ From ITree Require Export
      Indexed.Function
      Indexed.Sum.
 
+From CTree.Utils Require Export
+     Utils.
+
 From CTree.Core Require Export
-     Utils
      Index
      CTreeDefinitions.
 

theories/Core/CTreeDefinitions.v

@@ -25,8 +25,9 @@ br.
 
 From ITree Require Import Basics.Basics Core.Subevent Indexed.Sum.
 
-From CTree Require Import
-	   Core.Utils Core.Index.
+From CTree Require Export
+	   Utils.Utils.
+From CTree Require Import Core.Index.
 
 From ExtLib Require Import
 	   Structures.Functor

theories/Core/Index.v

@@ -1,5 +1,5 @@
 From ITree Require Import Basics Indexed.Sum.
-From CTree Require Import Core.Utils.
+From CTree Require Import Utils.Utils.
 
 Section Index.
 

theories/Eq.v

@@ -67,23 +67,23 @@ The upto [Vis] context principle for [sbisim]
 |*)
 (* #[global] Tactic Notation "upto_vis" := __upto_vis_sbisim. *)
 
-(*|
-The upto [bind] context principle for [equ] and [sbisim] ---
-the same tactic covers both cases, whether in front of a [gfp], [t _] or [bt _].
-The three variants are:
-- [upto_bind]: leave you with both proof obligations, introducing an evar for the intermediate relation in the case of [equ]
-- [upto_bind_eq]: meant to be use when the prefixes of the computations
-are identical: assumes [reflexivity] will solve the first goal, and proceed to substitute the equality
-- [upto_bind with SS]: for [equ], provides explicitly the intermediate relation
-|*)
-#[global] Tactic Notation "upto_bind" :=
-  __eupto_bind_equ || __eupto_bind_sbisim.
-
-#[global] Tactic Notation "upto_bind_eq" :=
-  __upto_bind_equ_eq || __upto_bind_sbisim_eq.
-
-#[global] Tactic Notation "upto_bind" "with" uconstr(SS) :=
-  __upto_bind_equ SS || __upto_bind_sbisim SS.
+(* (*| *)
+(* The upto [bind] context principle for [equ] and [sbisim] --- *)
+(* the same tactic covers both cases, whether in front of a [gfp], [t _] or [bt _]. *)
+(* The three variants are: *)
+(* - [upto_bind]: leave you with both proof obligations, introducing an evar for the intermediate relation in the case of [equ] *)
+(* - [upto_bind_eq]: meant to be use when the prefixes of the computations *)
+(* are identical: assumes [reflexivity] will solve the first goal, and proceed to substitute the equality *)
+(* - [upto_bind with SS]: for [equ], provides explicitly the intermediate relation *)
+(* |*) *)
+(* #[global] Tactic Notation "upto_bind" := *)
+(*   __eupto_bind_equ || __eupto_bind_sbisim. *)
+
+(* #[global] Tactic Notation "upto_bind_eq" := *)
+(*   __upto_bind_equ_eq || __upto_bind_sbisim_eq. *)
+
+(* #[global] Tactic Notation "upto_bind" "with" uconstr(SS) := *)
+(*   __upto_bind_equ SS || __upto_bind_sbisim SS. *)
 
 (*|
 Weakens equalities into respectively [equ] and [sbisim] equations ---
@@ -96,7 +96,7 @@ Ltac eq2equ H :=
 
 Ltac eq2sb H :=
   match type of H with
-  | ?u = ?t => let eq := fresh "EQ" in assert (eq : u ~ t) by (rewrite H; reflexivity); clear H
+  | ?u = ?t => let eq := fresh "EQ" in assert (eq : u ≃ t) by (rewrite H; reflexivity); clear H
   end.
 
 #[global] Opaque wtrans.