Made CERTBASE be called last in CERTS

Author: Soupstraw

src/Ledger/Certs.lagda

@@ -321,7 +321,7 @@ module _ where  -- achieves uniform (but perhaps misleading) alignment of type s
   _⊢_⇀⦇_,CERTS⦈_     : CertEnv     → CertState  → List DCert  → CertState  → Type
 \end{code}
 \begin{code}[hide]
-  _⊢_⇀⦇_,CERTS⦈_ = ReflexiveTransitiveClosureᵇ' {_⊢_⇀⟦_⟧ᵇ_ = _⊢_⇀⦇_,CERTBASE⦈_} {_⊢_⇀⦇_,CERT⦈_}
+  _⊢_⇀⦇_,CERTS⦈_ = ReflexiveTransitiveClosureᵇ {_⊢_⇀⟦_⟧ᵇ_ = _⊢_⇀⦇_,CERTBASE⦈_} {_⊢_⇀⦇_,CERT⦈_}
 \end{code}
 \end{AgdaMultiCode}
 \caption{Types for the transition systems relating to certificates}

src/Ledger/Certs/Properties.agda

@@ -301,16 +301,9 @@ module _  {Γ : CertEnv}
           getCoin (zeroMap ∪ˡ rewards) + getCoin wdrls
             ∎
 
-    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)))
+    CERTS-pov (BS-base x) = CERTBASE-pov x
+    CERTS-pov {s₁ = s₁} {sₙ} (BS-ind x y) = trans (CERT-pov x) (CERTS-pov y)
 
 -- TODO: Prove the following property.
 -- range vDelegs ⊆ map (credVoter DRep) (dom DReps)

src/Ledger/Conway/Conformance/Certs.agda

@@ -220,4 +220,4 @@ data _⊢_⇀⦇_,CERTBASE⦈_ : CertEnv → CertState → ⊤ → CertState →
       ⟧
 
 _⊢_⇀⦇_,CERTS⦈_     : CertEnv → CertState → List DCert → CertState → Type
-_⊢_⇀⦇_,CERTS⦈_ = ReflexiveTransitiveClosureᵇ' {_⊢_⇀⟦_⟧ᵇ_ = _⊢_⇀⦇_,CERTBASE⦈_}{_⊢_⇀⦇_,CERT⦈_}
+_⊢_⇀⦇_,CERTS⦈_ = ReflexiveTransitiveClosureᵇ {_⊢_⇀⟦_⟧ᵇ_ = _⊢_⇀⦇_,CERTBASE⦈_}{_⊢_⇀⦇_,CERT⦈_}

src/Ledger/Conway/Conformance/Equivalence.agda

@@ -190,9 +190,9 @@ WellformedLState s = certDepositsC (C.LState.certState s) ≡ᵈ certDeposits (c
 
 getValidCertDepositsCERTS : ∀ {Γ s certs s'} deposits (open L.CertEnv Γ using (pp))
                           → certDepositsC s ≡ᵈ (certDDeps deposits , certGDeps deposits)
-                          → ReflexiveTransitiveClosure {sts = C._⊢_⇀⦇_,CERT⦈_} Γ s certs s'
+                          → Γ C.⊢ s ⇀⦇ certs ,CERTS⦈ s'
                           → L.ValidCertDeposits pp deposits certs
-getValidCertDepositsCERTS deposits wf (BS-base Id-nop) = L.[]
+getValidCertDepositsCERTS deposits wf (BS-base _) = L.[]
 getValidCertDepositsCERTS {Γ} {s} {cert ∷ _} deposits wf (BS-ind (C.CERT-deleg (C.DELEG-delegate (a , b))) rs) =
   L.delegate (getValidCertDepositsCERTS _ (lemUpdCert (L.CertEnv.pp Γ) (certDepositsC s) deposits cert wf) rs)
 getValidCertDepositsCERTS {Γ} {s} {cert ∷ _} deposits wf (BS-ind (C.CERT-deleg (C.DELEG-dereg (_ , h , h'))) rs) =
@@ -212,20 +212,6 @@ getValidCertDepositsCERTS {Γ} {s} {cert ∷ _} deposits wf (BS-ind (C.CERT-vdel
 getValidCertDepositsCERTS {Γ} {s} {cert ∷ _} deposits wf (BS-ind (C.CERT-vdel (C.GOVCERT-ccreghot x)) rs) =
   L.ccreghot(getValidCertDepositsCERTS _ (lemUpdCert (L.CertEnv.pp Γ) (certDepositsC s) deposits cert wf) rs)
 
-getValidCertDepositsC : ∀ Γ s {s'} tx
-                     → (let open C.LEnv Γ using (pparams; slot; enactState)
-                            open TxBody (tx .Tx.body) using (txcerts; txvote; txwdrls)
-                            open C.LState s
-                            open C.UTxOState utxoSt using (deposits)
-                            cc = C.allColdCreds govSt enactState
-                       )
-                     → WellformedLState s
-                     → isValid tx ≡ true
-                     → ⟦ epoch slot , pparams , txvote , txwdrls , cc ⟧ C.⊢ certState ⇀⦇ txcerts ,CERTS⦈ s'
-                     → L.ValidCertDeposits pparams deposits txcerts
-getValidCertDepositsC Γ s tx wf refl (RTC (C.CERT-base _ , step)) =
-  getValidCertDepositsCERTS (C.UTxOState.deposits (C.LState.utxoSt s)) wf step
-
 lemUtxowDeposits : ∀ {Γ s s' tx}
                       (let open C.UTxOEnv Γ using (pparams))
                   → isValid tx ≡ true
@@ -254,7 +240,7 @@ instance
       open C.UTxOState utxoSt using (deposits)
 
       valid-deps : L.ValidCertDeposits pparams deposits txcerts
-      valid-deps = getValidCertDepositsC Γ s tx wf refl certs
+      valid-deps = getValidCertDepositsCERTS (C.UTxOState.deposits (C.LState.utxoSt s)) wf certs
 
       utxow' : _ L.⊢ utxoSt ⇀⦇ tx ,UTXOW⦈ (setDeposits (utxowDeposits utxow) utxoSt')
       utxow' = inj₂ valid-deps ⊢conv utxow
@@ -270,9 +256,9 @@ instance
 open IsEquivalence ≡ᵈ-isEquivalence renaming (refl to ≡ᵈ-refl; sym to ≡ᵈ-sym; trans to ≡ᵈ-trans)
 
 lemCERTS'DepositsC : ∀ {Γ s dcerts s'} (open C.CertEnv Γ using (pp))
-                   → ReflexiveTransitiveClosure {sts = C._⊢_⇀⦇_,CERT⦈_} Γ s dcerts s'
+                   → C._⊢_⇀⦇_,CERTS⦈_ Γ s dcerts s'
                    → certDepositsC s' ≡ ⟨ updateDDeps pp dcerts , updateGDeps pp dcerts ⟩ (certDepositsC s)
-lemCERTS'DepositsC (BS-base Id-nop)                                  = refl
+lemCERTS'DepositsC (BS-base (C._⊢_⇀⦇_,CERTBASE⦈_.CERT-base _))       = refl
 lemCERTS'DepositsC (BS-ind (C.CERT-deleg (C.DELEG-delegate   _)) rs) = lemCERTS'DepositsC rs
 lemCERTS'DepositsC (BS-ind (C.CERT-deleg (C.DELEG-dereg      _)) rs) = lemCERTS'DepositsC rs
 lemCERTS'DepositsC (BS-ind (C.CERT-deleg (C.DELEG-reg        _)) rs) = lemCERTS'DepositsC rs
@@ -282,11 +268,6 @@ lemCERTS'DepositsC (BS-ind (C.CERT-vdel (C.GOVCERT-regdrep   _)) rs) = lemCERTS'
 lemCERTS'DepositsC (BS-ind (C.CERT-vdel (C.GOVCERT-deregdrep _)) rs) = lemCERTS'DepositsC rs
 lemCERTS'DepositsC (BS-ind (C.CERT-vdel (C.GOVCERT-ccreghot  _)) rs) = lemCERTS'DepositsC rs
 
-lemCERTSDepositsC : ∀ {Γ s txcerts s'} (open C.CertEnv Γ using (pp))
-                  → Γ C.⊢ s ⇀⦇ txcerts ,CERTS⦈ s'
-                  → certDepositsC s' ≡ ⟨ updateDDeps pp txcerts , updateGDeps pp txcerts ⟩ (certDepositsC s)
-lemCERTSDepositsC (RTC (C.CERT-base _ , step)) = lemCERTS'DepositsC step
-
 lemWellformed : ∀ {Γ s tx s'} → WellformedLState s → Γ C.⊢ s ⇀⦇ tx ,LEDGER⦈ s' → WellformedLState s'
 lemWellformed {Γ} {s = ls} {tx} {s' = ls'} wf (C.LEDGER-V⋯ refl utxo certs gov) = goal
   where
@@ -310,7 +291,7 @@ lemWellformed {Γ} {s = ls} {tx} {s' = ls'} wf (C.LEDGER-V⋯ refl utxo certs go
     lem rewrite lemDepositsC utxo = refl
 
     lem₁ : (ddeps' , gdeps') ≡ (updateDDeps pparams txcerts ddeps , updateGDeps pparams txcerts gdeps)
-    lem₁ = lemCERTSDepositsC certs
+    lem₁ = lemCERTS'DepositsC certs
 
     lem₂ :  (updateDDeps pparams txcerts (certDDeps deposits) , updateGDeps pparams txcerts (certGDeps deposits))
          ≡ᵈ (certDDeps deposits' , certGDeps deposits')
@@ -342,9 +323,10 @@ updateCDep pp cert (ddep , gdep) = updateDDep pp cert ddep , updateGDep pp cert
 opaque
   castCERTS' : ∀ {Γ certs} {s s' : L.CertState} deps₁ deps₂ deps₁'
              → deps₁ ≡ᵈ deps₂
-             → Γ ⊢ deps₁ ⊢conv s ⇀⦇ certs ,CERTS'⦈ (deps₁' ⊢conv s')
-             → ∃[ deps₂' ] deps₁' ≡ᵈ deps₂' × Γ ⊢ deps₂ ⊢conv s ⇀⦇ certs ,CERTS'⦈ (deps₂' ⊢conv s')
-  castCERTS' deps₁ deps₂ deps₁' eqd (BS-base Id-nop) = deps₂ , eqd , BS-base Id-nop
+             → Γ C.⊢ deps₁ ⊢conv s ⇀⦇ certs ,CERTS⦈ (deps₁' ⊢conv s')
+             → ∃[ deps₂' ] deps₁' ≡ᵈ deps₂' × Γ C.⊢ deps₂ ⊢conv s ⇀⦇ certs ,CERTS⦈ (deps₂' ⊢conv s')
+  castCERTS' deps₁ deps₂ deps₁' eqd (BS-base (C._⊢_⇀⦇_,CERTBASE⦈_.CERT-base h)) = 
+    deps₂ , eqd , BS-base (C.CERT-base h)
   castCERTS' {Γ} deps₁ deps₂ deps₁' eqd (BS-ind (C.CERT-deleg {dCert = cert} (C.DELEG-delegate h))    rs) =
     let open C.CertEnv Γ using (pp)
         deps₂' , eqd' , rs' = castCERTS' (updateCDep pp cert deps₁) (updateCDep pp cert deps₂) deps₁'
@@ -387,14 +369,6 @@ opaque
     let deps₂' , eqd' , rs' = castCERTS' deps₁ deps₂ deps₁' eqd rs
     in  deps₂' , eqd' , BS-ind (C.CERT-vdel (C.GOVCERT-ccreghot h)) rs'
 
-  castCERTS : ∀ {Γ certs} {s s' : L.CertState} deps₁ deps₂ deps₁'
-            → deps₁ ≡ᵈ deps₂
-            → Γ C.⊢ deps₁ ⊢conv s ⇀⦇ certs ,CERTS⦈ (deps₁' ⊢conv s')
-            → ∃[ deps₂' ] deps₁' ≡ᵈ deps₂' × Γ C.⊢ deps₂ ⊢conv s ⇀⦇ certs ,CERTS⦈ (deps₂' ⊢conv s')
-  castCERTS deps₁ deps₂ deps₁' eqd (RTC (C.CERT-base h , step)) =
-    let deps₂' , eqd' , step' = castCERTS' deps₁ deps₂ deps₁' eqd step
-    in  deps₂' , eqd' , RTC (C.CERT-base h , step')
-
 _⊢_⇀⦇_,GOVn⦈_ : L.GovEnv × ℕ → L.GovState → List (GovVote ⊎ GovProposal) → L.GovState → Type
 _⊢_⇀⦇_,GOVn⦈_ = _⊢_⇀⟦_⟧ᵢ*'_ {_⊢_⇀⟦_⟧ᵇ_ = IdSTS} {_⊢_⇀⟦_⟧_ = L._⊢_⇀⦇_,GOV⦈_}
 
@@ -404,7 +378,7 @@ opaque
             → Γ C.⊢ deps₁ ⊢conv s ⇀⦇ tx ,LEDGER⦈ (deps₁' ⊢conv s')
             → ∃[ deps₂' ] deps₁' ≡ᵈ deps₂' × Γ C.⊢ deps₂ ⊢conv s ⇀⦇ tx ,LEDGER⦈ (deps₂' ⊢conv s')
   castLEDGER {Γ} {tx} {s} {s'} deps₁ deps₂ deps₁' eqd (C.LEDGER-V⋯ refl utxo certs gov) =
-    let deps₂' , eqd' , certs' = castCERTS deps₁ deps₂ deps₁' eqd certs
+    let deps₂' , eqd' , certs' = castCERTS' deps₁ deps₂ deps₁' eqd certs
     in  deps₂' , eqd' , C.LEDGER-V⋯ refl utxo certs' gov
   castLEDGER deps₁ deps₂ deps₁' eqd (C.LEDGER-I⋯ refl utxo) = _ , eqd , C.LEDGER-I⋯ refl utxo
 

src/Ledger/Conway/Conformance/Equivalence/Certs.agda

@@ -204,8 +204,8 @@ instance
                 ⊢ Γ L.⊢ s ⇀⦇ dcerts ,CERTS⦈ s' ⭆ⁱ λ deposits _ →
                   Γ C.⊢ (getCertDeps* deposits ⊢conv s) ⇀⦇ dcerts ,CERTS⦈
                         (getCertDeps* (updateCertDeps* dcerts deposits) ⊢conv s')
-  CERTSToConf .convⁱ deposits (RTC (base , step)) =
-    RTC (getCertDeps* deposits ⊢conv base , deposits ⊢conv step)
+  CERTSToConf .convⁱ ⟦ depsᵈ , depsᵍ , _ , _ ⟧* (BS-base x) = BS-base ((depsᵈ , depsᵍ) ⊢conv x)
+  CERTSToConf .convⁱ deposits (BS-ind x y) = BS-ind (deposits ⊢conv x) (updateCertDeps deposits ⊢conv y)
 
 -- Converting form Conformance is easier since the deposit tracking disappears.
 instance
@@ -246,4 +246,5 @@ instance
   CERTSFromConf : ∀ {Γ s dcerts s'}
                 → Γ C.⊢ s ⇀⦇ dcerts ,CERTS⦈ s' ⭆
                   Γ L.⊢ conv s ⇀⦇ dcerts ,CERTS⦈ conv s'
-  CERTSFromConf .convⁱ _ (RTC (base , step)) = RTC (conv base , conv step)
+  CERTSFromConf .convⁱ _ (BS-base x) = BS-base (conv x)
+  CERTSFromConf .convⁱ _ (BS-ind x x₁) = BS-ind (conv x) (conv x₁)