From cgraphs.locks.lambdalock Require Export langtools.
(* Expressions and values *)
(* ---------------------- *)
Inductive expr := (* https://apndx.org/pub/thesis/thesis.pdf#nameddest=bd741f98 *)
| Val : val -> expr (* https://apndx.org/pub/thesis/thesis.pdf#nameddest=e1ac3346 *)
| Var : string -> expr
| Fun : string -> expr -> expr (* https://apndx.org/pub/thesis/thesis.pdf#nameddest=1b7faaef *)
| App : expr -> expr -> expr (* https://apndx.org/pub/thesis/thesis.pdf#nameddest=1a84c0b8 *)
| Unit : expr
| Pair : expr -> expr -> expr (* https://apndx.org/pub/thesis/thesis.pdf#nameddest=f76d493b *)
| LetPair : expr -> expr -> expr (* https://apndx.org/pub/thesis/thesis.pdf#nameddest=0cab1eef *)
| Sum : nat -> expr -> expr (* https://apndx.org/pub/thesis/thesis.pdf#nameddest=aa2c4dee *)
| MatchSum n : expr -> (fin n -> expr) -> expr (* https://apndx.org/pub/thesis/thesis.pdf#nameddest=dbbfbbb9 *)
(* Barriers *)
| ForkBarrier : expr -> expr (* https://apndx.org/pub/thesis/thesis.pdf#nameddest=0b0c64bd *)
(* Locks *)
| NewLock : expr -> expr (* https://apndx.org/pub/thesis/thesis.pdf#nameddest=8b3d344e *)
| ForkLock : expr -> expr -> expr (* https://apndx.org/pub/thesis/thesis.pdf#nameddest=117cde28 *)
| Acquire : expr -> expr (* https://apndx.org/pub/thesis/thesis.pdf#nameddest=e7363af4 *)
| Release : expr -> expr -> expr (* https://apndx.org/pub/thesis/thesis.pdf#nameddest=5a1132d4 *)
| Wait : expr -> expr (* https://apndx.org/pub/thesis/thesis.pdf#nameddest=29daa364 *)
| Drop : expr -> expr (* https://apndx.org/pub/thesis/thesis.pdf#nameddest=52880547 *)
with val := (* https://apndx.org/pub/thesis/thesis.pdf#nameddest=351fafd5 *)
| FunV : string -> expr -> val (* https://apndx.org/pub/thesis/thesis.pdf#nameddest=39d38956 *)
| UnitV : val
| PairV : val -> val -> val (* https://apndx.org/pub/thesis/thesis.pdf#nameddest=1c670e18 *)
| SumV : nat -> val -> val (* https://apndx.org/pub/thesis/thesis.pdf#nameddest=c1cc32bf *)
| BarrierV : nat -> val
| LockV : nat -> val.
(* Type system *)
(* ----------- *)
Inductive linearity := Lin | Unr.
Inductive lockstate := Opened | Closed.
Inductive lockownership := Owner | Client.
Definition lockcap : Type := lockownership * lockstate.
Inductive lockownership_split : lockownership -> lockownership -> lockownership -> Prop :=
| lo_split_1 : lockownership_split Owner Client Owner
| lo_split_2 : lockownership_split Owner Owner Client
| lo_split_3 : lockownership_split Client Client Client.
Inductive lockstate_split : lockstate -> lockstate -> lockstate -> Prop :=
| ls_split_1 : lockstate_split Opened Closed Opened
| ls_split_2 : lockstate_split Opened Opened Closed
| ls_split_3 : lockstate_split Closed Closed Closed.
Definition lockcap_split l1 l2 l3 :=
lockownership_split l1.1 l2.1 l3.1 ∧ lockstate_split l1.2 l2.2 l3.2.
CoInductive type := (* https://apndx.org/pub/thesis/thesis.pdf#nameddest=4e6c37ed *)
| FunT : linearity -> type -> type -> type (* https://apndx.org/pub/thesis/thesis.pdf#nameddest=68d56eeb *)
| UnitT : type
| PairT : type -> type -> type (* https://apndx.org/pub/thesis/thesis.pdf#nameddest=748f0a3a *)
| SumT n : (fin n -> type) -> type
| LockT : lockcap -> type -> type. (* https://apndx.org/pub/thesis/thesis.pdf#nameddest=d3e805ce *)
CoInductive unr : type -> Prop := (* https://apndx.org/pub/thesis/thesis.pdf#nameddest=5e71ad23 *)
| Fun_unr t1 t2 : unr (FunT Unr t1 t2)
| Unit_unr : unr UnitT
| Pair_unr t1 t2 : unr t1 -> unr t2 -> unr (PairT t1 t2)
| Sum_unr n ts : (∀ i, unr (ts i)) -> unr (SumT n ts).
(* We define linear environment splitting here.
On paper this is implicit in Γ1,Γ2 ⊢ e : A.
In Coq we have to explicitly say env_split Γ Γ1 Γ2, and typed Γ e A. *) (* https://apndx.org/pub/thesis/thesis.pdf#nameddest=f9fbd460 *)
Definition env := gmap string type.
Definition env_unr (Γ : env) :=
∀ x t, Γ !! x = Some t -> unr t.
Definition disj (Γ1 Γ2 : env) :=
∀ i t1 t2, Γ1 !! i = Some t1 -> Γ2 !! i = Some t2 -> t1 = t2 ∧ unr t1.
Definition env_split (Γ : env) (Γ1 : env) (Γ2 : env) :=
Γ = Γ1 ∪ Γ2 ∧ disj Γ1 Γ2.
Definition env_bind (Γ' : env) (x : string) (t : type) (Γ : env) :=
Γ' = <[ x := t ]> Γ ∧ ∀ t', Γ !! x = Some t' -> unr t'.
Definition env_var (Γ : env) (x : string) (t : type) :=
∃ Γ', Γ = <[ x := t ]> Γ' ∧ env_unr Γ'.
Inductive typed : env -> expr -> type -> Prop := (* https://apndx.org/pub/thesis/thesis.pdf#nameddest=063ac77d *)
(* Base language *)
| Var_typed Γ x t : (* https://apndx.org/pub/thesis/thesis.pdf#nameddest=d918f0e3 *)
env_var Γ x t ->
typed Γ (Var x) t (* https://apndx.org/pub/thesis/thesis.pdf#nameddest=18ff1edd *)
| Fun_typed Γ Γ' x e t1 t2 l : (* https://apndx.org/pub/thesis/thesis.pdf#nameddest=7de0a9fa *)
env_bind Γ' x t1 Γ ->
(l = Unr -> env_unr Γ) ->
typed Γ' e t2 -> (* https://apndx.org/pub/thesis/thesis.pdf#nameddest=cd8f4fae *)
typed Γ (Fun x e) (FunT l t1 t2) (* https://apndx.org/pub/thesis/thesis.pdf#nameddest=c897994a *)
| App_typed Γ Γ1 Γ2 e1 e2 t1 t2 l : (* https://apndx.org/pub/thesis/thesis.pdf#nameddest=cac20a51 *)
env_split Γ Γ1 Γ2 ->
typed Γ1 e1 (FunT l t1 t2) -> (* https://apndx.org/pub/thesis/thesis.pdf#nameddest=b329b0e9 *)
typed Γ2 e2 t1 -> (* https://apndx.org/pub/thesis/thesis.pdf#nameddest=9c6cfb05 *)
typed Γ (App e1 e2) t2 (* https://apndx.org/pub/thesis/thesis.pdf#nameddest=8016fa2f *)
| Unit_typed Γ : (* https://apndx.org/pub/thesis/thesis.pdf#nameddest=82fafc4b *)
env_unr Γ ->
typed Γ Unit UnitT (* https://apndx.org/pub/thesis/thesis.pdf#nameddest=128a62ec *)
| Pair_typed Γ Γ1 Γ2 e1 e2 t1 t2 : (* https://apndx.org/pub/thesis/thesis.pdf#nameddest=2061b613 *)
env_split Γ Γ1 Γ2 ->
typed Γ1 e1 t1 -> (* https://apndx.org/pub/thesis/thesis.pdf#nameddest=21da7a1b *)
typed Γ2 e2 t2 -> (* https://apndx.org/pub/thesis/thesis.pdf#nameddest=88bc53c3 *)
typed Γ (Pair e1 e2) (PairT t1 t2) (* https://apndx.org/pub/thesis/thesis.pdf#nameddest=bf73e6d5 *)
| LetPair_typed Γ Γ1 Γ2 e1 e2 t1 t2 t : (* https://apndx.org/pub/thesis/thesis.pdf#nameddest=0d21d03e *)
env_split Γ Γ1 Γ2 ->
typed Γ1 e1 (PairT t1 t2) -> (* https://apndx.org/pub/thesis/thesis.pdf#nameddest=3be318ad *)
typed Γ2 e2 (FunT Lin t1 (FunT Lin t2 t)) -> (* https://apndx.org/pub/thesis/thesis.pdf#nameddest=7f704c9a *)
typed Γ (LetPair e1 e2) t (* https://apndx.org/pub/thesis/thesis.pdf#nameddest=047dc82a *)
| Sum_typed Γ n (ts : fin n -> type) i e : (* https://apndx.org/pub/thesis/thesis.pdf#nameddest=f9a9c616 *)
typed Γ e (ts i) -> (* https://apndx.org/pub/thesis/thesis.pdf#nameddest=2a908df3 *)
typed Γ (Sum i e) (SumT n ts) (* https://apndx.org/pub/thesis/thesis.pdf#nameddest=567d9852 *)
| MatchSumN_typed n Γ Γ1 Γ2 t (ts : fin n -> type) es e : (* https://apndx.org/pub/thesis/thesis.pdf#nameddest=18af6e5d *)
env_split Γ Γ1 Γ2 ->
(n = 0 -> env_unr Γ2) ->
typed Γ1 e (SumT n ts) -> (* https://apndx.org/pub/thesis/thesis.pdf#nameddest=615b3c77 *)
(∀ i, typed Γ2 (es i) (FunT Lin (ts i) t)) -> (* https://apndx.org/pub/thesis/thesis.pdf#nameddest=e6ec31e8 *)
typed Γ (MatchSum n e es) t (* https://apndx.org/pub/thesis/thesis.pdf#nameddest=64e6af3a *)
(* Barriers *)
| Fork_typed Γ e t1 t2 : (* https://apndx.org/pub/thesis/thesis.pdf#nameddest=cbbc5d81 *)
typed Γ e (FunT Lin (FunT Lin t2 t1) UnitT) -> (* https://apndx.org/pub/thesis/thesis.pdf#nameddest=e3cc4b96 *)
typed Γ (ForkBarrier e) (FunT Lin t1 t2) (* https://apndx.org/pub/thesis/thesis.pdf#nameddest=f9774561 *)
(* Locks *)
| NewLock_typed Γ e t : (* https://apndx.org/pub/thesis/thesis.pdf#nameddest=ebd2f6f8 *)
typed Γ e t -> (* https://apndx.org/pub/thesis/thesis.pdf#nameddest=ca554905 *)
typed Γ (NewLock e) (LockT (Owner,Closed) t) (* https://apndx.org/pub/thesis/thesis.pdf#nameddest=37f69353 *)
| ForkLock_typed Γ Γ1 Γ2 e1 e2 t l1 l2 l3 : (* https://apndx.org/pub/thesis/thesis.pdf#nameddest=c38f8bf9 *)
env_split Γ Γ1 Γ2 ->
lockcap_split l1 l2 l3 ->
typed Γ1 e1 (LockT l1 t) -> (* https://apndx.org/pub/thesis/thesis.pdf#nameddest=86353a2a *)
typed Γ2 e2 (FunT Lin (LockT l2 t) UnitT) -> (* https://apndx.org/pub/thesis/thesis.pdf#nameddest=3edc7e2f *)
typed Γ (ForkLock e1 e2) (LockT l3 t) (* https://apndx.org/pub/thesis/thesis.pdf#nameddest=349435dc *)
| Acquire_typed Γ e t lo : (* https://apndx.org/pub/thesis/thesis.pdf#nameddest=73e233f6 *)
typed Γ e (LockT (lo,Closed) t) -> (* https://apndx.org/pub/thesis/thesis.pdf#nameddest=72503952 *)
typed Γ (Acquire e) (PairT (LockT (lo,Opened) t) t) (* https://apndx.org/pub/thesis/thesis.pdf#nameddest=d0d05905 *)
| Release_typed Γ Γ1 Γ2 e1 e2 t lo : (* https://apndx.org/pub/thesis/thesis.pdf#nameddest=6bf3e805 *)
env_split Γ Γ1 Γ2 ->
typed Γ1 e1 (LockT (lo,Opened) t) -> (* https://apndx.org/pub/thesis/thesis.pdf#nameddest=6bbc86f7 *)
typed Γ2 e2 t -> (* https://apndx.org/pub/thesis/thesis.pdf#nameddest=f8239a8e *)
typed Γ (Release e1 e2) (LockT (lo,Closed) t) (* https://apndx.org/pub/thesis/thesis.pdf#nameddest=bfb4ed07 *)
| Wait_typed Γ e t : (* https://apndx.org/pub/thesis/thesis.pdf#nameddest=e562fe59 *)
typed Γ e (LockT (Owner,Closed) t) -> (* https://apndx.org/pub/thesis/thesis.pdf#nameddest=5e317ac8 *)
typed Γ (Wait e) t (* https://apndx.org/pub/thesis/thesis.pdf#nameddest=56f2ff83 *)
| Drop_typed Γ e t : (* https://apndx.org/pub/thesis/thesis.pdf#nameddest=bf6563c1 *)
typed Γ e (LockT (Client,Closed) t) -> (* https://apndx.org/pub/thesis/thesis.pdf#nameddest=513db587 *)
typed Γ (Drop e) UnitT. (* https://apndx.org/pub/thesis/thesis.pdf#nameddest=087d77ec *)
(* Operational semantics *)
(* --------------------- *)
Definition subst (x:string) (a:val) := fix rec e :=
match e with
| Val _ => e
| Var x' => if decide (x = x') then Val a else e
| Fun x' e => Fun x' (if decide (x = x') then e else rec e)
| App e1 e2 => App (rec e1) (rec e2)
| Unit => Unit
| Pair e1 e2 => Pair (rec e1) (rec e2)
| LetPair e1 e2 => LetPair (rec e1) (rec e2)
| Sum n e => Sum n (rec e)
| MatchSum n e1 e2 => MatchSum n (rec e1) (rec ∘ e2)
| ForkBarrier e => ForkBarrier (rec e)
| NewLock e => NewLock (rec e)
| ForkLock e1 e2 => ForkLock (rec e1) (rec e2)
| Acquire e => Acquire (rec e)
| Release e1 e2 => Release (rec e1) (rec e2)
| Wait e => Wait (rec e)
| Drop e => Drop (rec e)
end.
Inductive pure_step : expr -> expr -> Prop := (* https://apndx.org/pub/thesis/thesis.pdf#nameddest=b8792a06 *)
| Fun_step x e : (* https://apndx.org/pub/thesis/thesis.pdf#nameddest=bd6ae9d6 *)
pure_step (Fun x e) (Val $ FunV x e) (* https://apndx.org/pub/thesis/thesis.pdf#nameddest=04bc1cc3 *)
| App_step x e a : (* https://apndx.org/pub/thesis/thesis.pdf#nameddest=1e38bd60 *)
pure_step (App (Val $ FunV x e) (Val a)) (subst x a e) (* https://apndx.org/pub/thesis/thesis.pdf#nameddest=5153b71b *)
| Unit_step : (* https://apndx.org/pub/thesis/thesis.pdf#nameddest=4a598e99 *)
pure_step Unit (Val $ UnitV) (* https://apndx.org/pub/thesis/thesis.pdf#nameddest=b7c9a7e4 *)
| Pair_step v1 v2 : (* https://apndx.org/pub/thesis/thesis.pdf#nameddest=72df8128 *)
pure_step (Pair (Val v1) (Val v2)) (Val $ PairV v1 v2) (* https://apndx.org/pub/thesis/thesis.pdf#nameddest=28bfc65e *)
| LetPair_step v1 v2 e: (* https://apndx.org/pub/thesis/thesis.pdf#nameddest=49850352 *)
pure_step (LetPair (Val $ PairV v1 v2) e) (App (App e (Val v1)) (Val v2)) (* https://apndx.org/pub/thesis/thesis.pdf#nameddest=eb58d82a *)
| Sum_step n v : (* https://apndx.org/pub/thesis/thesis.pdf#nameddest=157b308c *)
pure_step (Sum n (Val v)) (Val $ SumV n v) (* https://apndx.org/pub/thesis/thesis.pdf#nameddest=e4d91ea6 *)
| MatchSum_step n (i : fin n) v es : (* https://apndx.org/pub/thesis/thesis.pdf#nameddest=b9865a73 *)
pure_step (MatchSum n (Val $ SumV i v) es) (App (es i) (Val v)). (* https://apndx.org/pub/thesis/thesis.pdf#nameddest=5478ba63 *)
Inductive ctx1 : (expr -> expr) -> Prop := (* https://apndx.org/pub/thesis/thesis.pdf#nameddest=1c630008 *)
| Ctx_App_l e : ctx1 (λ x, App x e)
| Ctx_App_r e : ctx1 (λ x, App e x)
| Ctx_Pair_l e : ctx1 (λ x, Pair x e)
| Ctx_Pair_r e : ctx1 (λ x, Pair e x)
| Ctx_LetPair e : ctx1 (λ x, LetPair x e)
| Ctx_Sum i : ctx1 (λ x, Sum i x)
| Ctx_MatchSum n es : ctx1 (λ x, MatchSum n x es)
| Ctx_ForkBarrier : ctx1 (λ x, ForkBarrier x)
| Ctx_NewLock : ctx1 (λ x, NewLock x)
| Ctx_ForkLock_l e : ctx1 (λ x, ForkLock x e)
| Ctx_ForkLock_r e : ctx1 (λ x, ForkLock e x)
| Ctx_Acquire : ctx1 (λ x, Acquire x)
| Ctx_Release_l e : ctx1 (λ x, Release x e)
| Ctx_Release_r e : ctx1 (λ x, Release e x)
| Ctx_Wait : ctx1 (λ x, Wait x)
| Ctx_Drop : ctx1 (λ x, Drop x).
Inductive ctx : (expr -> expr) -> Prop := (* https://apndx.org/pub/thesis/thesis.pdf#nameddest=873c29d5 *)
| Ctx_id : ctx id (* https://apndx.org/pub/thesis/thesis.pdf#nameddest=5a04aa1e *)
| Ctx_comp k1 k2 : ctx1 k1 -> ctx k2 -> ctx (k1 ∘ k2). (* https://apndx.org/pub/thesis/thesis.pdf#nameddest=d0be05a9 *)
Inductive obj := Thread (e : expr) | Barrier | Lock (refcnt : nat) (o : option val).
Definition cfg := gmap nat obj.
Inductive local_step : nat -> cfg -> cfg -> Prop := (* https://apndx.org/pub/thesis/thesis.pdf#nameddest=36a090da *)
(* Base language *)
| Pure_step i k e e' : (* https://apndx.org/pub/thesis/thesis.pdf#nameddest=235e16a1 *)
ctx k -> pure_step e e' -> (* https://apndx.org/pub/thesis/thesis.pdf#nameddest=e0aa097e *)
local_step i {[ i := Thread (k e) ]} {[ i := Thread (k e') ]} (* https://apndx.org/pub/thesis/thesis.pdf#nameddest=9356889e *)
| Exit_step i : (* https://apndx.org/pub/thesis/thesis.pdf#nameddest=127169a0 *)
local_step i {[ i := Thread (Val UnitV) ]} ∅ (* https://apndx.org/pub/thesis/thesis.pdf#nameddest=f52aa0ec *)
(* Barriers *)
| Fork_step i j n k v : (* https://apndx.org/pub/thesis/thesis.pdf#nameddest=509888ad *)
i ≠ j -> i ≠ n -> j ≠ n -> ctx k -> (* https://apndx.org/pub/thesis/thesis.pdf#nameddest=5c3c2291 *)
local_step i {[ i := Thread (k (ForkBarrier (Val v))) ]} (* https://apndx.org/pub/thesis/thesis.pdf#nameddest=76c407c1 *)
{[ i := Thread (k (Val $ BarrierV n));
j := Thread (App (Val v) (Val $ BarrierV n));
n := Barrier ]}
| Sync_step i j n k1 k2 v1 v2 : (* https://apndx.org/pub/thesis/thesis.pdf#nameddest=0329b62d *)
i ≠ j -> i ≠ n -> j ≠ n -> ctx k1 -> ctx k2 -> (* https://apndx.org/pub/thesis/thesis.pdf#nameddest=2bddcfa4 *)
local_step n {[ i := Thread (k1 (App (Val $ BarrierV n) (Val v1))); (* https://apndx.org/pub/thesis/thesis.pdf#nameddest=11c6b589 *)
j := Thread (k2 (App (Val $ BarrierV n) (Val v2)));
n := Barrier ]}
{[ i := Thread (k1 $ Val v2);
j := Thread (k2 $ Val v1) ]}
(* Locks *)
| NewLock_step v k n i: (* https://apndx.org/pub/thesis/thesis.pdf#nameddest=081f2786 *)
i ≠ n -> ctx k -> (* https://apndx.org/pub/thesis/thesis.pdf#nameddest=99d5e9d1 *)
local_step i {[ i := Thread (k (NewLock (Val v))) ]} (* https://apndx.org/pub/thesis/thesis.pdf#nameddest=0e688e7e *)
{[ i := Thread (k (Val $ LockV n));
n := Lock 0 (Some v) ]}
| ForkLock_step v o k i j n refcnt : (* https://apndx.org/pub/thesis/thesis.pdf#nameddest=df365013 *)
i ≠ j -> i ≠ n -> j ≠ n -> ctx k -> (* https://apndx.org/pub/thesis/thesis.pdf#nameddest=330a8d8b *)
local_step n {[ i := Thread (k (ForkLock (Val $ LockV n) (Val v))); (* https://apndx.org/pub/thesis/thesis.pdf#nameddest=c6a00b4e *)
n := Lock refcnt o ]}
{[ i := Thread (k (Val $ LockV n));
j := Thread (App (Val v) (Val $ LockV n));
n := Lock (S refcnt) o ]}
| Acquire_step v k i n refcnt : (* https://apndx.org/pub/thesis/thesis.pdf#nameddest=a81ba248 *)
i ≠ n -> ctx k -> (* https://apndx.org/pub/thesis/thesis.pdf#nameddest=b13eb335 *)
local_step n {[ i := Thread (k (Acquire (Val $ LockV n))); (* https://apndx.org/pub/thesis/thesis.pdf#nameddest=c0ba1a27 *)
n := Lock refcnt (Some v) ]}
{[ i := Thread (k (Val $ PairV (LockV n) v));
n := Lock refcnt None ]}
| Release_step v k i n refcnt : (* https://apndx.org/pub/thesis/thesis.pdf#nameddest=2681b789 *)
i ≠ n -> ctx k -> (* https://apndx.org/pub/thesis/thesis.pdf#nameddest=c3c9c600 *)
local_step n {[ i := Thread (k (Release (Val $ LockV n) (Val v))); (* https://apndx.org/pub/thesis/thesis.pdf#nameddest=82b2c726 *)
n := Lock refcnt None ]}
{[ i := Thread (k (Val $ LockV n));
n := Lock refcnt (Some v) ]}
| Wait_step v k i n : (* https://apndx.org/pub/thesis/thesis.pdf#nameddest=aad9b1c4 *)
i ≠ n -> ctx k -> (* https://apndx.org/pub/thesis/thesis.pdf#nameddest=0d8e601a *)
local_step n {[ i := Thread (k (Wait (Val $ LockV n))); (* https://apndx.org/pub/thesis/thesis.pdf#nameddest=85b138b6 *)
n := Lock 0 (Some v) ]}
{[ i := Thread (k (Val v)) ]}
| Drop_step o k i n refcnt : (* https://apndx.org/pub/thesis/thesis.pdf#nameddest=8b3d3a51 *)
i ≠ n -> ctx k -> (* https://apndx.org/pub/thesis/thesis.pdf#nameddest=aa71107b *)
local_step n {[ i := Thread (k (Drop (Val $ LockV n))); (* https://apndx.org/pub/thesis/thesis.pdf#nameddest=0e5ffcaf *)
n := Lock (S refcnt) o ]}
{[ i := Thread (k (Val $ UnitV));
n := Lock refcnt o ]}.
Inductive step : nat -> cfg -> cfg -> Prop := (* https://apndx.org/pub/thesis/thesis.pdf#nameddest=98db5a22 *)
| Frame_step ρ ρ' ρf i : (* https://apndx.org/pub/thesis/thesis.pdf#nameddest=9f10f2a7 *)
ρ ##ₘ ρf -> ρ' ##ₘ ρf ->
local_step i ρ ρ' -> step i (ρ ∪ ρf) (ρ' ∪ ρf). (* https://apndx.org/pub/thesis/thesis.pdf#nameddest=90a734ae *)
Definition step' ρ ρ' := ∃ i, step i ρ ρ'. (* https://apndx.org/pub/thesis/thesis.pdf#nameddest=edb7be03 *)
Definition steps := rtc step'.