CERTS should do the base case first (#604)

* CERTS should do the base case first This closes issue #545. * progress * implement Ulf's idea to split off base case * progress * task complete * cleanup: remove unused code; clean up some pdf figures * attempt at more abstract implementation of "base case first" mod * proof of computationality and completeness * cleanup
IntersectMBO · Nov 22, 2024 · d406853 · d406853
1 parent 363b1f6
commit d406853
Show file tree

Hide file tree

Showing 11 changed files with 82 additions and 48 deletions.
diff --git a/src/Interface/ComputationalRelation.agda b/src/Interface/ComputationalRelation.agda
@@ -40,7 +40,7 @@ instance
   Bifunctor-ComputationResult : ∀ {a : Level} → Bifunctor {_} {a} ComputationResult
   Bifunctor-ComputationResult .bimap _ f (success x) = success $ f x
   Bifunctor-ComputationResult .bimap f _ (failure x) = failure $ f x
-  
+
   Functor-ComputationResult : ∀ {E : Type} → Functor (ComputationResult E)
   Functor-ComputationResult ._<$>_ f (success x) = success $ f x
   Functor-ComputationResult ._<$>_ _ (failure x) = failure x
@@ -135,7 +135,7 @@ module _ {STS : C → S → Sig → S → Type} (comp : Computational STS Err) w
   ExtendedRel-rightUnique {s' = success x}  {success x'} h h'
     with trans (sym $ Equivalence.from ≡-success⇔STS h) (Equivalence.from ≡-success⇔STS h')
   ... | refl = refl
-    
+
   ExtendedRel-rightUnique {s' = success x} {failure _}  h h' = ⊥-elim $ h' x h
   ExtendedRel-rightUnique {s' = failure _} {success x'} h h' = ⊥-elim $ h x' h'
   ExtendedRel-rightUnique {s' = failure a} {failure b}  h h' = refl
@@ -190,9 +190,9 @@ instance
 module _ {BSTS : C → S → ⊤ → S → Type} ⦃ _ : Computational BSTS Err₁ ⦄ where
   module _ {STS : C → S → Sig → S → Type} ⦃ _ : Computational STS Err₂ ⦄
      ⦃ _ : InjectError Err₁ Err ⦄ ⦃ _ : InjectError Err₂ Err ⦄ where instance
-    Computational-ReflexiveTransitiveClosureᵇ : Computational (ReflexiveTransitiveClosureᵇ BSTS STS) (Err)
+    Computational-ReflexiveTransitiveClosureᵇ : Computational (ReflexiveTransitiveClosureᵇ {_⊢_⇀⟦_⟧ᵇ_ = BSTS}{STS}) (Err)
     Computational-ReflexiveTransitiveClosureᵇ .computeProof c s [] = bimap (injectError it) (map₂′ BS-base) (computeProof c s tt)
-    Computational-ReflexiveTransitiveClosureᵇ .computeProof c s (sig ∷ sigs) with computeProof c s sig 
+    Computational-ReflexiveTransitiveClosureᵇ .computeProof c s (sig ∷ sigs) with computeProof c s sig
     ... | success (s₁ , h) with computeProof c s₁ sigs
     ...   | success (s₂ , hs) = success (s₂ , BS-ind h hs)
     ...   | failure a = failure (injectError it a)
@@ -209,7 +209,7 @@ module _ {BSTS : C → S → ⊤ → S → Type} ⦃ _ : Computational BSTS Err
   module _ {STS : C × ℕ → S → Sig → S → Type} ⦃ Computational-STS : Computational STS Err₂ ⦄
     ⦃ InjectError-Err₁ : InjectError Err₁ Err ⦄ ⦃ InjectError-Err₂ : InjectError Err₂ Err ⦄
     where instance
-    Computational-ReflexiveTransitiveClosureᵢᵇ' : Computational (_⊢_⇀⟦_⟧ᵢ*'_ BSTS STS) Err
+    Computational-ReflexiveTransitiveClosureᵢᵇ' : Computational (_⊢_⇀⟦_⟧ᵢ*'_ {_⊢_⇀⟦_⟧ᵇ_ = BSTS}{STS}) Err
     Computational-ReflexiveTransitiveClosureᵢᵇ' .computeProof c s [] =
       bimap (injectError it) (map₂′ BS-base) (computeProof (proj₁ c) s tt)
     Computational-ReflexiveTransitiveClosureᵢᵇ' .computeProof c s (sig ∷ sigs) with computeProof c s sig
@@ -226,16 +226,35 @@ module _ {BSTS : C → S → ⊤ → S → Type} ⦃ _ : Computational BSTS Err
       with computeProof (proj₁ c , suc (proj₂ c)) s₁ sigs | completeness _ _ _ _ hs
     ...   | success (s₂ , _) | p = p
 
-    Computational-ReflexiveTransitiveClosureᵢᵇ : Computational (ReflexiveTransitiveClosureᵢᵇ BSTS STS) Err
+    Computational-ReflexiveTransitiveClosureᵢᵇ : Computational (ReflexiveTransitiveClosureᵢᵇ {_⊢_⇀⟦_⟧ᵇ_ = BSTS}{STS}) Err
     Computational-ReflexiveTransitiveClosureᵢᵇ .computeProof c =
       Computational-ReflexiveTransitiveClosureᵢᵇ' .computeProof (c , 0)
     Computational-ReflexiveTransitiveClosureᵢᵇ .completeness c =
       Computational-ReflexiveTransitiveClosureᵢᵇ' .completeness (c , 0)
 
+module _ {BSTS : C → S → ⊤ → S → Type} ⦃ _ : Computational BSTS Err₁ ⦄ where
+  module _ {STS : C → S → Sig → S → Type} ⦃ _ : Computational STS Err₂ ⦄
+     ⦃ _ : InjectError Err₁ Err ⦄ ⦃ _ : InjectError Err₂ Err ⦄ where instance
+    Computational-ReflexiveTransitiveClosureᵇ' : Computational (ReflexiveTransitiveClosureᵇ' {_⊢_⇀⟦_⟧ᵇ_ = BSTS} {STS}) (Err)
+    Computational-ReflexiveTransitiveClosureᵇ' .computeProof c s sigs with (computeProof{STS = BSTS} c s tt)
+    ... | failure a = failure (injectError it a)
+    ... | success (s' , h) with (computeProof{STS = ReflexiveTransitiveClosureᵇ {_⊢_⇀⟦_⟧ᵇ_ = IdSTS} {STS}} c s' sigs)
+    ... | failure a = failure a
+    ... | success (s' , hs) = success (s' , (RTC (h , hs)))
+
+    Computational-ReflexiveTransitiveClosureᵇ' .completeness c s sigs s'' (RTC (bsts , sts))
+      with (computeProof {STS = BSTS} c s tt) | completeness _ _ _ _ bsts
+    ... | success (s₁ , h) | refl
+      with  computeProof {STS = ReflexiveTransitiveClosureᵇ {_⊢_⇀⟦_⟧ᵇ_ = IdSTS} {STS}}{Err} c s₁ sigs
+         |  completeness {Err = Err} _ _ _ _ sts
+    ... | success (s₂ , _) | p = p
+
+
 Computational-ReflexiveTransitiveClosure : {STS : C → S → Sig → S → Type} → ⦃ Computational STS Err ⦄
-  → Computational (ReflexiveTransitiveClosure STS) Err
+  → Computational (ReflexiveTransitiveClosure {sts = STS}) Err
 Computational-ReflexiveTransitiveClosure = it
 
 Computational-ReflexiveTransitiveClosureᵢ : {STS : C × ℕ → S → Sig → S → Type} → ⦃ Computational STS Err ⦄
-  → Computational (ReflexiveTransitiveClosureᵢ STS) Err
+  → Computational (ReflexiveTransitiveClosureᵢ {sts = STS}) Err
 Computational-ReflexiveTransitiveClosureᵢ = it
+
diff --git a/src/Interface/STS.agda b/src/Interface/STS.agda
@@ -39,7 +39,7 @@ private
 
 -- small-step to big-step transformer
 
-module _ (_⊢_⇀⟦_⟧ᵇ_ : C → S → ⊤ → S → Type) (_⊢_⇀⟦_⟧_ : C → S → Sig → S → Type) where
+module _ {_⊢_⇀⟦_⟧ᵇ_ : C → S → ⊤ → S → Type} {_⊢_⇀⟦_⟧_ : C → S → Sig → S → Type} where
   data _⊢_⇀⟦_⟧*_ : C → S → List Sig → S → Type where
 
     BS-base :
@@ -53,7 +53,7 @@ module _ (_⊢_⇀⟦_⟧ᵇ_ : C → S → ⊤ → S → Type) (_⊢_⇀⟦_⟧
         ───────────────────────────────────────
         Γ ⊢ s  ⇀⟦ sig ∷ sigs ⟧* s''
 
-module _ (_⊢_⇀⟦_⟧ᵇ_ : C → S → ⊤ → S → Type) (_⊢_⇀⟦_⟧_ : C × ℕ → S → Sig → S → Type) where
+module _ {_⊢_⇀⟦_⟧ᵇ_ : C → S → ⊤ → S → Type} {_⊢_⇀⟦_⟧_ : C × ℕ → S → Sig → S → Type} where
   data _⊢_⇀⟦_⟧ᵢ*'_ : C × ℕ → S → List Sig → S → Type where
 
     BS-base :
@@ -73,29 +73,38 @@ module _ (_⊢_⇀⟦_⟧ᵇ_ : C → S → ⊤ → S → Type) (_⊢_⇀⟦_⟧
 data IdSTS {C S} : C → S → ⊤ → S → Type where
   Id-nop : IdSTS Γ s _ s
 
+module _ {_⊢_⇀⟦_⟧ᵇ_ : C → S → ⊤ → S → Type} {_⊢_⇀⟦_⟧_ : C → S → Sig → S → Type} where
+  data _⊢_⇀⟦_⟧*'_ : C → S → List Sig → S → Type where
+      RTC :
+          ∙ Γ ⊢ s ⇀⟦ _ ⟧ᵇ s'
+          ∙ _⊢_⇀⟦_⟧*_ {_⊢_⇀⟦_⟧ᵇ_ = IdSTS}{_⊢_⇀⟦_⟧_} Γ s' sigs s''
+          ───────────────────────────────────────
+          Γ ⊢ s ⇀⟦ sigs ⟧*' s''
+
+
 -- with a trivial base case
-ReflexiveTransitiveClosure : (C → S → Sig → S → Type) → C → S → List Sig → S → Type
-ReflexiveTransitiveClosure = _⊢_⇀⟦_⟧*_ IdSTS
+ReflexiveTransitiveClosure : {sts : C → S → Sig → S → Type} → C → S → List Sig → S → Type
+ReflexiveTransitiveClosure {sts = sts} = _⊢_⇀⟦_⟧*_ {_⊢_⇀⟦_⟧ᵇ_ = IdSTS}{sts}
 
 STS-total : (C → S → Sig → S → Type) → Type
 STS-total _⊢_⇀⟦_⟧_ = ∀ {Γ s sig} → ∃[ s' ] Γ ⊢ s ⇀⟦ sig ⟧ s'
 
 ReflexiveTransitiveClosure-total : {_⊢_⇀⟦_⟧_ : C → S → Sig → S → Type}
-  → STS-total _⊢_⇀⟦_⟧_ → STS-total (ReflexiveTransitiveClosure _⊢_⇀⟦_⟧_)
+  → STS-total _⊢_⇀⟦_⟧_ → STS-total (ReflexiveTransitiveClosure {sts = _⊢_⇀⟦_⟧_})
 ReflexiveTransitiveClosure-total SS-total {Γ} {s} {[]} = s , BS-base Id-nop
 ReflexiveTransitiveClosure-total SS-total {Γ} {s} {x ∷ sig} =
   case SS-total of λ where
     (s' , Ps') → map₂′ (BS-ind Ps') $ ReflexiveTransitiveClosure-total SS-total
 
-ReflexiveTransitiveClosureᵢ : (C × ℕ → S → Sig → S → Type) → C → S → List Sig → S → Type
-ReflexiveTransitiveClosureᵢ = _⊢_⇀⟦_⟧ᵢ*_ IdSTS
+ReflexiveTransitiveClosureᵢ : {sts : C × ℕ → S → Sig → S → Type} → C → S → List Sig → S → Type
+ReflexiveTransitiveClosureᵢ {sts = sts} = _⊢_⇀⟦_⟧ᵢ*_ {_⊢_⇀⟦_⟧ᵇ_ = IdSTS}{sts}
 
 ReflexiveTransitiveClosureᵢ-total : {_⊢_⇀⟦_⟧_ : C × ℕ → S → Sig → S → Type}
-  → STS-total _⊢_⇀⟦_⟧_ → STS-total (ReflexiveTransitiveClosureᵢ _⊢_⇀⟦_⟧_)
+  → STS-total _⊢_⇀⟦_⟧_ → STS-total (ReflexiveTransitiveClosureᵢ {sts = _⊢_⇀⟦_⟧_})
 ReflexiveTransitiveClosureᵢ-total SS-total = helper SS-total
   where
     helper : {_⊢_⇀⟦_⟧_ : C × ℕ → S → Sig → S → Type}
-      → STS-total _⊢_⇀⟦_⟧_ → STS-total (_⊢_⇀⟦_⟧ᵢ*'_ IdSTS _⊢_⇀⟦_⟧_)
+      → STS-total _⊢_⇀⟦_⟧_ → STS-total (_⊢_⇀⟦_⟧ᵢ*'_ {_⊢_⇀⟦_⟧ᵇ_ = IdSTS}{_⊢_⇀⟦_⟧_})
     helper SS-total {s = s} {[]} = s , BS-base Id-nop
     helper SS-total {s = s} {x ∷ sig} =
       case SS-total of λ where
@@ -104,11 +113,12 @@ ReflexiveTransitiveClosureᵢ-total SS-total = helper SS-total
 -- with a given base case
 ReflexiveTransitiveClosureᵢᵇ = _⊢_⇀⟦_⟧ᵢ*_
 ReflexiveTransitiveClosureᵇ  = _⊢_⇀⟦_⟧*_
+ReflexiveTransitiveClosureᵇ'  = _⊢_⇀⟦_⟧*'_
 
 LedgerInvariant : (C → S → Sig → S → Type) → (S → Type) → Type
 LedgerInvariant STS P = ∀ {c s sig s'} → STS c s sig s' → P s → P s'
 
 RTC-preserves-inv : ∀ {STS : C → S → Sig → S → Type} {P}
-                  → LedgerInvariant STS P → LedgerInvariant (ReflexiveTransitiveClosure STS) P
+                  → LedgerInvariant STS P → LedgerInvariant (ReflexiveTransitiveClosure {sts = STS}) P
 RTC-preserves-inv inv (BS-base Id-nop) = id
 RTC-preserves-inv inv (BS-ind p₁ p₂)   = RTC-preserves-inv inv p₂ ∘ inv p₁
diff --git a/src/Ledger/Certs.lagda b/src/Ledger/Certs.lagda
@@ -264,42 +264,41 @@ constitutional committee.
 \end{itemize}
 
 \begin{figure*}[h]
-\begin{AgdaSuppressSpace}
+\begin{AgdaMultiCode}
 \begin{code}[hide]
 data
 \end{code}
 \begin{code}
-  _⊢_⇀⦇_,DELEG⦈_     : DelegEnv → DState → DCert → DState → Type
+    _⊢_⇀⦇_,DELEG⦈_     : DelegEnv → DState → DCert → DState → Type
 \end{code}
 \begin{code}[hide]
 data
 \end{code}
 \begin{code}
-  _⊢_⇀⦇_,POOL⦈_      : PoolEnv → PState → DCert → PState → Type
+    _⊢_⇀⦇_,POOL⦈_      : PoolEnv → PState → DCert → PState → Type
 \end{code}
 \begin{code}[hide]
 data
 \end{code}
 \begin{code}
-  _⊢_⇀⦇_,GOVCERT⦈_   : GovCertEnv → GState → DCert → GState → Type
+    _⊢_⇀⦇_,GOVCERT⦈_   : GovCertEnv → GState → DCert → GState → Type
 \end{code}
 \begin{code}[hide]
 data
 \end{code}
 \begin{code}
-  _⊢_⇀⦇_,CERT⦈_      : CertEnv → CertState → DCert → CertState → Type
+    _⊢_⇀⦇_,CERT⦈_      : CertEnv → CertState → DCert → CertState → Type
 \end{code}
 \begin{code}[hide]
 data
 \end{code}
 \begin{code}
-  _⊢_⇀⦇_,CERTBASE⦈_  : CertEnv → CertState → ⊤ → CertState → Type
-\end{code}
-\begin{code}
-_⊢_⇀⦇_,CERTS⦈_     : CertEnv → CertState → List DCert → CertState → Type
-_⊢_⇀⦇_,CERTS⦈_ = ReflexiveTransitiveClosureᵇ _⊢_⇀⦇_,CERTBASE⦈_ _⊢_⇀⦇_,CERT⦈_
+    _⊢_⇀⦇_,CERTBASE⦈_  : CertEnv → CertState → ⊤ → CertState → Type
+
+_⊢_⇀⦇_,CERTS⦈_       : CertEnv → CertState → List DCert → CertState → Type
+_⊢_⇀⦇_,CERTS⦈_ = ReflexiveTransitiveClosureᵇ' {_⊢_⇀⟦_⟧ᵇ_ = _⊢_⇀⦇_,CERTBASE⦈_} {_⊢_⇀⦇_,CERT⦈_}
 \end{code}
-\end{AgdaSuppressSpace}
+\end{AgdaMultiCode}
 \caption{Types for the transition systems relating to certificates}
 \label{fig:sts:certs-types}
 \end{figure*}
@@ -318,15 +317,15 @@ data _⊢_⇀⦇_,DELEG⦈_ where
         fromList ( nothing ∷ just abstainRep ∷ just noConfidenceRep ∷ [] )
     ∙ mkh ∈ mapˢ just (dom pools) ∪ ❴ nothing ❵
       ────────────────────────────────
-      ⟦ pp , pools , delegatees ⟧ᵈᵉ ⊢
-        ⟦ vDelegs , sDelegs , rwds ⟧ᵈ ⇀⦇ delegate c mv mkh d ,DELEG⦈
+      ⟦ pp , pools , delegatees ⟧ᵈᵉ ⊢ ⟦ vDelegs , sDelegs , rwds ⟧ᵈ
+        ⇀⦇ delegate c mv mkh d ,DELEG⦈
         ⟦ insertIfJust c mv vDelegs , insertIfJust c mkh sDelegs , rwds ∪ˡ ❴ c , 0 ❵ ⟧ᵈ
 
   DELEG-dereg :
     ∙ (c , 0) ∈ rwds
       ────────────────────────────────
-      ⟦ pp , pools , delegatees ⟧ᵈᵉ ⊢  ⟦ vDelegs , sDelegs , rwds ⟧ᵈ ⇀⦇ dereg c d ,DELEG⦈
-                          ⟦ vDelegs ∣ ❴ c ❵ ᶜ , sDelegs ∣ ❴ c ❵ ᶜ , rwds ∣ ❴ c ❵ ᶜ ⟧ᵈ
+      ⟦ pp , pools , delegatees ⟧ᵈᵉ ⊢ ⟦ vDelegs , sDelegs , rwds ⟧ᵈ ⇀⦇ dereg c d ,DELEG⦈
+        ⟦ vDelegs ∣ ❴ c ❵ ᶜ , sDelegs ∣ ❴ c ❵ ᶜ , rwds ∣ ❴ c ❵ ᶜ ⟧ᵈ
 \end{code}
 \end{AgdaSuppressSpace}
 \caption{Auxiliary DELEG transition system}
@@ -430,7 +429,8 @@ data _⊢_⇀⦇_,CERTBASE⦈_ where
     refresh          = mapPartial getDRepVote (fromList vs)
     refreshedDReps   = mapValueRestricted (const (e + drepActivity)) dReps refresh
     wdrlCreds        = mapˢ stake (dom wdrls)
-    validVoteDelegs  = voteDelegs ∣^ (mapˢ (credVoter DRep) (dom dReps) ∪ fromList (noConfidenceRep ∷ abstainRep ∷ []))
+    validVoteDelegs  = voteDelegs ∣^ (  mapˢ (credVoter DRep) (dom dReps)
+                                        ∪ fromList (noConfidenceRep ∷ abstainRep ∷ []) )
     in
     ∙ filter isKeyHash wdrlCreds ⊆ dom voteDelegs
     ∙ mapˢ (map₁ stake) (wdrls ˢ) ⊆ rewards ˢ

diff --git a/src/Ledger/Certs/Properties.agda b/src/Ledger/Certs/Properties.agda
@@ -145,7 +145,6 @@ Computational-CERTS = it
 
 private variable
   dCert : DCert
-  Γ : CertEnv
   l : List DCert
   A A' B : Type
 instance
@@ -158,7 +157,8 @@ getCoin-singleton = indexedSum-singleton' {M = Coin} (finiteness _)
                 → a ∈ dom m → getCoin (m ∪ˡ ❴ (a , c) ❵ᵐ) ≡ getCoin m
 ∪ˡsingleton∈dom m {(a , c)} a∈dom = ≡ᵉ-getCoin (m ∪ˡ ❴ (a , c) ❵) m (singleton-∈-∪ˡ {m = m} a∈dom)
 
-module _  ( indexedSumᵛ'-∪ :  {A : Type} ⦃ _ : DecEq A ⦄ (m m' : A ⇀ Coin)
+module _  {Γ : CertEnv}
+          ( indexedSumᵛ'-∪ :  {A : Type} ⦃ _ : DecEq A ⦄ (m m' : A ⇀ Coin)
                               → disjoint (dom m) (dom m')
                               → getCoin (m ∪ˡ m') ≡ getCoin m + getCoin m' )
   where
@@ -281,11 +281,16 @@ module _  ( indexedSumᵛ'-∪ :  {A : Type} ⦃ _ : DecEq A ⦄ (m m' : A ⇀ C
           getCoin (zeroMap ∪ˡ rewards) + getCoin wdrls
             ∎
 
-    CERTS-pov : {stᵈ stᵈ' : DState} {stᵖ stᵖ' : PState} {stᵍ stᵍ' : GState}
-                → Γ ⊢ ⟦ stᵈ , stᵖ , stᵍ ⟧ᶜˢ ⇀⦇ l ,CERTS⦈ ⟦ stᵈ' , stᵖ' , stᵍ' ⟧ᶜˢ
-                → getCoin ⟦ stᵈ , stᵖ , stᵍ ⟧ᶜˢ ≡ getCoin ⟦ stᵈ' , stᵖ' , stᵍ' ⟧ᶜˢ + getCoin (CertEnv.wdrls Γ)
-    CERTS-pov (BS-base x) = CERTBASE-pov x
-    CERTS-pov (BS-ind  x xs) = trans (CERT-pov x) (CERTS-pov xs)
+    sts-pov  : {s₁ sₙ : CertState} → ReflexiveTransitiveClosure {sts = _⊢_⇀⦇_,CERT⦈_} Γ s₁ l sₙ
+             → getCoin s₁ ≡ getCoin sₙ
+    sts-pov (BS-base Id-nop) = refl
+    sts-pov (BS-ind x xs) = trans (CERT-pov x) (sts-pov xs)
+
+    CERTS-pov : {s₁ sₙ : CertState} → Γ ⊢ s₁ ⇀⦇ l ,CERTS⦈ sₙ → getCoin s₁ ≡ getCoin sₙ + getCoin (CertEnv.wdrls Γ)
+    CERTS-pov (RTC {s' = s'} {s'' = sₙ} (bsts , BS-base Id-nop)) = CERTBASE-pov bsts
+    CERTS-pov (RTC (bsts , BS-ind x sts)) = trans  (CERTBASE-pov bsts)
+                                                   (cong  (_+ getCoin (CertEnv.wdrls Γ))
+                                                          (trans (CERT-pov x) (sts-pov sts)))
 
 -- TODO: Prove the following property.
 -- range vDelegs ⊆ map (credVoter DRep) (dom DReps)
diff --git a/src/Ledger/Conway/Conformance/Certs.agda b/src/Ledger/Conway/Conformance/Certs.agda
@@ -200,4 +200,4 @@ data _⊢_⇀⦇_,CERTBASE⦈_ : CertEnv → CertState → ⊤ → CertState →
       ⟧ᶜˢ
 
 _⊢_⇀⦇_,CERTS⦈_     : CertEnv → CertState → List DCert → CertState → Type
-_⊢_⇀⦇_,CERTS⦈_ = ReflexiveTransitiveClosureᵇ _⊢_⇀⦇_,CERTBASE⦈_ _⊢_⇀⦇_,CERT⦈_
+_⊢_⇀⦇_,CERTS⦈_ = ReflexiveTransitiveClosureᵇ' {_⊢_⇀⟦_⟧ᵇ_ = _⊢_⇀⦇_,CERTBASE⦈_}{_⊢_⇀⦇_,CERT⦈_}
diff --git a/src/Ledger/Conway/Conformance/Gov.agda b/src/Ledger/Conway/Conformance/Gov.agda
@@ -268,4 +268,4 @@ data _⊢_⇀⦇_,GOV'⦈_ where
       ───────────────────────────────────────
       (Γ , k) ⊢ s ⇀⦇ inj₂ prop ,GOV'⦈ s'
 
-_⊢_⇀⦇_,GOV⦈_ = ReflexiveTransitiveClosureᵢ _⊢_⇀⦇_,GOV'⦈_
+_⊢_⇀⦇_,GOV⦈_ = ReflexiveTransitiveClosureᵢ {sts = _⊢_⇀⦇_,GOV'⦈_}
diff --git a/src/Ledger/Conway/Conformance/Ledger.agda b/src/Ledger/Conway/Conformance/Ledger.agda
@@ -90,4 +90,4 @@ pattern LEDGER-V⋯ w x y z = LEDGER-V (w , x , y , z)
 pattern LEDGER-I⋯ y z     = LEDGER-I (y , z)
 
 _⊢_⇀⦇_,LEDGERS⦈_ : LEnv → LState → List Tx → LState → Type
-_⊢_⇀⦇_,LEDGERS⦈_ = ReflexiveTransitiveClosure _⊢_⇀⦇_,LEDGER⦈_
+_⊢_⇀⦇_,LEDGERS⦈_ = ReflexiveTransitiveClosure {sts = _⊢_⇀⦇_,LEDGER⦈_}
diff --git a/src/Ledger/Gov.lagda b/src/Ledger/Gov.lagda
@@ -354,7 +354,7 @@ data _⊢_⇀⦇_,GOV'⦈_ where
       ───────────────────────────────────────
       (Γ , k) ⊢ s ⇀⦇ inj₂ prop ,GOV'⦈ s'
 
-_⊢_⇀⦇_,GOV⦈_ = ReflexiveTransitiveClosureᵢ _⊢_⇀⦇_,GOV'⦈_
+_⊢_⇀⦇_,GOV⦈_ = ReflexiveTransitiveClosureᵢ {sts = _⊢_⇀⦇_,GOV'⦈_}
 \end{code}
 \caption{Rules for the GOV transition system}
 \label{defs:gov-rules}

diff --git a/src/Ledger/Ledger.lagda b/src/Ledger/Ledger.lagda
@@ -137,7 +137,7 @@ pattern LEDGER-I⋯ y z     = LEDGER-I (y , z)
 \begin{figure*}[h]
 \begin{code}
 _⊢_⇀⦇_,LEDGERS⦈_ : LEnv → LState → List Tx → LState → Type
-_⊢_⇀⦇_,LEDGERS⦈_ = ReflexiveTransitiveClosure _⊢_⇀⦇_,LEDGER⦈_
+_⊢_⇀⦇_,LEDGERS⦈_ = ReflexiveTransitiveClosure {sts = _⊢_⇀⦇_,LEDGER⦈_}
 \end{code}
 \caption{LEDGERS transition system}
 \end{figure*}

diff --git a/src/Ledger/Ledger/Properties.agda b/src/Ledger/Ledger/Properties.agda
@@ -237,7 +237,7 @@ module LEDGER-PROPS (tx : Tx) (Γ : LEnv) (s : LState) where
   STS→GovSt≡ (LEDGER-V x) refl = STS→updateGovSt≡ (txgov txb) 0 (proj₂ (proj₂ (proj₂ x)))
     where
     STS→updateGovSt≡ : (vps : List (GovVote ⊎ GovProposal)) (k : ℕ) {certSt : CertState} {govSt govSt' : GovState}
-      → (_⊢_⇀⟦_⟧ᵢ*'_ IdSTS _⊢_⇀⦇_,GOV'⦈_ (⟦ txid , epoch slot , pp , ppolicy , enactState , certSt ⟧ᵍ , k) govSt vps govSt')
+      → (_⊢_⇀⟦_⟧ᵢ*'_ {_⊢_⇀⟦_⟧ᵇ_ = IdSTS}{_⊢_⇀⦇_,GOV'⦈_} (⟦ txid , epoch slot , pp , ppolicy , enactState , certSt ⟧ᵍ , k) govSt vps govSt')
       → govSt' ≡ updateGovStates vps k govSt
     STS→updateGovSt≡ [] _ (BS-base Id-nop) = refl
     STS→updateGovSt≡ (inj₁ v ∷ vps) k (BS-ind (GOV-Vote x) h)

diff --git a/src/Ledger/Ratify.lagda b/src/Ledger/Ratify.lagda
@@ -578,7 +578,7 @@ data _⊢_⇀⦇_,RATIFY'⦈_ : RatifyEnv → RatifyState → GovActionID × Gov
 
 _⊢_⇀⦇_,RATIFY⦈_  : RatifyEnv → RatifyState → List (GovActionID × GovActionState)
                  → RatifyState → Type
-_⊢_⇀⦇_,RATIFY⦈_ = ReflexiveTransitiveClosure _⊢_⇀⦇_,RATIFY'⦈_
+_⊢_⇀⦇_,RATIFY⦈_ = ReflexiveTransitiveClosure {sts = _⊢_⇀⦇_,RATIFY'⦈_}
 \end{code}
 \end{AgdaSuppressSpace}
 \caption{The RATIFY transition system}