Certs

{-# OPTIONS --safe #-}

open import Ledger.Prelude
open import Ledger.Conway.Specification.Abstract
open import Ledger.Conway.Specification.Transaction using (TransactionStructure)

open import Data.Product using (_×_; _,_)
open import Relation.Binary.PropositionalEquality

open import Ledger.Conway.Conformance.Equivalence.Convert

module Ledger.Conway.Conformance.Equivalence.Certs
  (txs : _) (open TransactionStructure txs)
  (abs : AbstractFunctions txs) (open AbstractFunctions abs)
  where

private
  module L where
    open import Ledger.Conway.Specification.Certs govStructure public

  module C where
    open import Ledger.Conway.Conformance.Certs govStructure public

instance

  DStateToConf : L.Deposits ⊢ L.DState ⭆ C.DState
  DStateToConf .convⁱ deposits stᵈ =
    let open L.DState stᵈ in
    $\begin{pmatrix} \,\href{Ledger.Conway.Specification.Certs.html#4480}{\htmlId{922}{\htmlClass{Field}{\text{voteDelegs}}}}\, \\ \,\href{Ledger.Conway.Specification.Certs.html#4510}{\htmlId{935}{\htmlClass{Field}{\text{stakeDelegs}}}}\, \\ \,\href{Ledger.Conway.Specification.Certs.html#4541}{\htmlId{949}{\htmlClass{Field}{\text{rewards}}}}\, \\ \,\href{Ledger.Conway.Conformance.Equivalence.Certs.html#872}{\htmlId{959}{\htmlClass{Bound}{\text{deposits}}}}\, \end{pmatrix}$

  DStateFromConf : C.DState ⭆ L.DState
  DStateFromConf .convⁱ _ dState =
    let open C.DState dState in
    $\begin{pmatrix} \,\href{Ledger.Conway.Conformance.Certs.html#761}{\htmlId{1083}{\htmlClass{Field}{\text{voteDelegs}}}}\, \\ \,\href{Ledger.Conway.Conformance.Certs.html#791}{\htmlId{1096}{\htmlClass{Field}{\text{stakeDelegs}}}}\, \\ \,\href{Ledger.Conway.Conformance.Certs.html#831}{\htmlId{1110}{\htmlClass{Field}{\text{rewards}}}}\, \end{pmatrix}$

  GStateToConf : L.Deposits ⊢ L.GState ⭆ C.GState
  GStateToConf .convⁱ deposits stᵍ =
    let open L.GState stᵍ in
    $\begin{pmatrix} \,\href{Ledger.Conway.Specification.Certs.html#4772}{\htmlId{1243}{\htmlClass{Field}{\text{dreps}}}}\, \\ \,\href{Ledger.Conway.Specification.Certs.html#4795}{\htmlId{1251}{\htmlClass{Field}{\text{ccHotKeys}}}}\, \\ \,\href{Ledger.Conway.Conformance.Equivalence.Certs.html#1193}{\htmlId{1263}{\htmlClass{Bound}{\text{deposits}}}}\, \end{pmatrix}$

  GStateFromConf : C.GState ⭆ L.GState
  GStateFromConf .convⁱ deposits gState =
    let open C.GState gState in
    $\begin{pmatrix} \,\href{Ledger.Conway.Conformance.Certs.html#945}{\htmlId{1394}{\htmlClass{Field}{\text{dreps}}}}\, \\ \,\href{Ledger.Conway.Conformance.Certs.html#981}{\htmlId{1402}{\htmlClass{Field}{\text{ccHotKeys}}}}\, \end{pmatrix}$

data ValidDepsᵈ (pp : PParams) (deps : L.Deposits) : List L.DCert → Set where
  []         : ValidDepsᵈ pp deps []
  delegate   : ∀ {c del kh v certs}
             → ValidDepsᵈ pp (C.updateCertDeposit pp (L.delegate c del kh v) deps) certs
             → ValidDepsᵈ pp deps (L.delegate c del kh v ∷ certs)
  dereg      : ∀ {c md d certs}
             → (L.CredentialDeposit c , d) ∈ deps
             → md ≡ nothing ⊎ md ≡ just d
             → ValidDepsᵈ pp (C.updateCertDeposit pp (L.dereg c md) deps) certs
             → ValidDepsᵈ pp deps (L.dereg c md ∷ certs)
  regdrep    : ∀ {c v a certs}
             → ValidDepsᵈ pp deps certs
             → ValidDepsᵈ pp deps (L.regdrep c v a ∷ certs)
  deregdrep  : ∀ {c d certs}
             → ValidDepsᵈ pp deps certs
             → ValidDepsᵈ pp deps (L.deregdrep c d ∷ certs)
  regpool    : ∀ {kh p certs}
             → ValidDepsᵈ pp deps certs
             → ValidDepsᵈ pp deps (L.regpool kh p ∷ certs)
  retirepool : ∀ {kh e certs}
             → ValidDepsᵈ pp deps certs
             → ValidDepsᵈ pp deps (L.retirepool kh e  ∷ certs)
  ccreghot   : ∀ {c v certs}
             → ValidDepsᵈ pp deps certs
             → ValidDepsᵈ pp deps (L.ccreghot c v ∷ certs)
  reg        : ∀ {c d certs}
             → ValidDepsᵈ pp (C.updateCertDeposit pp (L.reg c d) deps) certs
             → ValidDepsᵈ pp deps (L.reg c d ∷ certs)

data ValidDepsᵍ (pp : PParams) (deps : L.Deposits) : List L.DCert → Set where
  []         : ValidDepsᵍ pp deps []
  regdrep    : ∀ {c v a certs}
             → ValidDepsᵍ pp (C.updateCertDeposit pp (L.regdrep c v a) deps) certs
             → ValidDepsᵍ pp deps (L.regdrep c v a ∷ certs)
  deregdrep  : ∀ {c d certs}
             → (L.DRepDeposit c , d) ∈ deps
             → ValidDepsᵍ pp (C.updateCertDeposit pp (L.deregdrep c d) deps) certs
             → ValidDepsᵍ pp deps (L.deregdrep c d ∷ certs)
  delegate   : ∀ {c del kh v certs}
             → ValidDepsᵍ pp deps certs
             → ValidDepsᵍ pp deps (L.delegate c del kh v ∷ certs)
  dereg      : ∀ {c d certs}
             → ValidDepsᵍ pp deps certs
             → ValidDepsᵍ pp deps (L.dereg c d ∷ certs)
  regpool    : ∀ {kh p certs}
             → ValidDepsᵍ pp deps certs
             → ValidDepsᵍ pp deps (L.regpool kh p ∷ certs)
  retirepool : ∀ {kh e certs}
             → ValidDepsᵍ pp deps certs
             → ValidDepsᵍ pp deps (L.retirepool kh e  ∷ certs)
  ccreghot   : ∀ {c v certs}
             → ValidDepsᵍ pp deps certs
             → ValidDepsᵍ pp deps (L.ccreghot c v ∷ certs)
  reg        : ∀ {c d certs}
             → ValidDepsᵍ pp deps certs
             → ValidDepsᵍ pp deps (L.reg c d ∷ certs)

record CertDeps* (pp : PParams) (dcerts : List L.DCert) : Set where
  constructor ⟦_,_,_,_⟧*
  field
    depsᵈ : L.Deposits
    depsᵍ : L.Deposits
    -- Invariants
    validᵈ : ValidDepsᵈ pp depsᵈ dcerts
    validᵍ : ValidDepsᵍ pp depsᵍ dcerts

pattern delegate*    ddeps gdeps = $\begin{pmatrix} \,\htmlId{4362}{\htmlClass{Symbol}{\text{\_}}}\, \\ \,\htmlId{4366}{\htmlClass{Symbol}{\text{\_}}}\, \\ \,\htmlId{4370}{\htmlClass{InductiveConstructor}{\text{delegate}}}\,   \,\href{Ledger.Conway.Conformance.Equivalence.Certs.html#4381}{\htmlId{4381}{\htmlClass{Bound}{\text{ddeps}}}}\, \\ \,\htmlId{4389}{\htmlClass{InductiveConstructor}{\text{delegate}}}\,    \,\href{Ledger.Conway.Conformance.Equivalence.Certs.html#4401}{\htmlId{4401}{\htmlClass{Bound}{\text{gdeps}}}}\, \end{pmatrix}$
pattern dereg*  v w  ddeps gdeps = $\begin{pmatrix} \,\htmlId{4447}{\htmlClass{Symbol}{\text{\_}}}\, \\ \,\htmlId{4451}{\htmlClass{Symbol}{\text{\_}}}\, \\ \,\htmlId{4455}{\htmlClass{InductiveConstructor}{\text{dereg}}}\, \,\href{Ledger.Conway.Conformance.Equivalence.Certs.html#4461}{\htmlId{4461}{\htmlClass{Bound}{\text{v}}}}\, \,\href{Ledger.Conway.Conformance.Equivalence.Certs.html#4463}{\htmlId{4463}{\htmlClass{Bound}{\text{w}}}}\,  \,\href{Ledger.Conway.Conformance.Equivalence.Certs.html#4466}{\htmlId{4466}{\htmlClass{Bound}{\text{ddeps}}}}\, \\ \,\htmlId{4474}{\htmlClass{InductiveConstructor}{\text{dereg}}}\,       \,\href{Ledger.Conway.Conformance.Equivalence.Certs.html#4486}{\htmlId{4486}{\htmlClass{Bound}{\text{gdeps}}}}\, \end{pmatrix}$
pattern regpool*     ddeps gdeps = $\begin{pmatrix} \,\htmlId{4532}{\htmlClass{Symbol}{\text{\_}}}\, \\ \,\htmlId{4536}{\htmlClass{Symbol}{\text{\_}}}\, \\ \,\htmlId{4540}{\htmlClass{InductiveConstructor}{\text{regpool}}}\,    \,\href{Ledger.Conway.Conformance.Equivalence.Certs.html#4551}{\htmlId{4551}{\htmlClass{Bound}{\text{ddeps}}}}\, \\ \,\htmlId{4559}{\htmlClass{InductiveConstructor}{\text{regpool}}}\,     \,\href{Ledger.Conway.Conformance.Equivalence.Certs.html#4571}{\htmlId{4571}{\htmlClass{Bound}{\text{gdeps}}}}\, \end{pmatrix}$
pattern retirepool*  ddeps gdeps = $\begin{pmatrix} \,\htmlId{4617}{\htmlClass{Symbol}{\text{\_}}}\, \\ \,\htmlId{4621}{\htmlClass{Symbol}{\text{\_}}}\, \\ \,\htmlId{4625}{\htmlClass{InductiveConstructor}{\text{retirepool}}}\, \,\href{Ledger.Conway.Conformance.Equivalence.Certs.html#4636}{\htmlId{4636}{\htmlClass{Bound}{\text{ddeps}}}}\, \\ \,\htmlId{4644}{\htmlClass{InductiveConstructor}{\text{retirepool}}}\,  \,\href{Ledger.Conway.Conformance.Equivalence.Certs.html#4656}{\htmlId{4656}{\htmlClass{Bound}{\text{gdeps}}}}\, \end{pmatrix}$
pattern regdrep*     ddeps gdeps = $\begin{pmatrix} \,\htmlId{4702}{\htmlClass{Symbol}{\text{\_}}}\, \\ \,\htmlId{4706}{\htmlClass{Symbol}{\text{\_}}}\, \\ \,\htmlId{4710}{\htmlClass{InductiveConstructor}{\text{regdrep}}}\,    \,\href{Ledger.Conway.Conformance.Equivalence.Certs.html#4721}{\htmlId{4721}{\htmlClass{Bound}{\text{ddeps}}}}\, \\ \,\htmlId{4729}{\htmlClass{InductiveConstructor}{\text{regdrep}}}\,     \,\href{Ledger.Conway.Conformance.Equivalence.Certs.html#4741}{\htmlId{4741}{\htmlClass{Bound}{\text{gdeps}}}}\, \end{pmatrix}$
pattern deregdrep* v ddeps gdeps = $\begin{pmatrix} \,\htmlId{4787}{\htmlClass{Symbol}{\text{\_}}}\, \\ \,\htmlId{4791}{\htmlClass{Symbol}{\text{\_}}}\, \\ \,\htmlId{4795}{\htmlClass{InductiveConstructor}{\text{deregdrep}}}\,  \,\href{Ledger.Conway.Conformance.Equivalence.Certs.html#4806}{\htmlId{4806}{\htmlClass{Bound}{\text{ddeps}}}}\, \\ \,\htmlId{4814}{\htmlClass{InductiveConstructor}{\text{deregdrep}}}\, \,\href{Ledger.Conway.Conformance.Equivalence.Certs.html#4824}{\htmlId{4824}{\htmlClass{Bound}{\text{v}}}}\, \,\href{Ledger.Conway.Conformance.Equivalence.Certs.html#4826}{\htmlId{4826}{\htmlClass{Bound}{\text{gdeps}}}}\, \end{pmatrix}$
pattern ccreghot*    ddeps gdeps = $\begin{pmatrix} \,\htmlId{4872}{\htmlClass{Symbol}{\text{\_}}}\, \\ \,\htmlId{4876}{\htmlClass{Symbol}{\text{\_}}}\, \\ \,\htmlId{4880}{\htmlClass{InductiveConstructor}{\text{ccreghot}}}\,   \,\href{Ledger.Conway.Conformance.Equivalence.Certs.html#4891}{\htmlId{4891}{\htmlClass{Bound}{\text{ddeps}}}}\, \\ \,\htmlId{4899}{\htmlClass{InductiveConstructor}{\text{ccreghot}}}\,    \,\href{Ledger.Conway.Conformance.Equivalence.Certs.html#4911}{\htmlId{4911}{\htmlClass{Bound}{\text{gdeps}}}}\, \end{pmatrix}$
pattern reg*         ddeps gdeps = $\begin{pmatrix} \,\htmlId{4957}{\htmlClass{Symbol}{\text{\_}}}\, \\ \,\htmlId{4961}{\htmlClass{Symbol}{\text{\_}}}\, \\ \,\htmlId{4965}{\htmlClass{InductiveConstructor}{\text{reg}}}\,        \,\href{Ledger.Conway.Conformance.Equivalence.Certs.html#4976}{\htmlId{4976}{\htmlClass{Bound}{\text{ddeps}}}}\, \\ \,\htmlId{4984}{\htmlClass{InductiveConstructor}{\text{reg}}}\,         \,\href{Ledger.Conway.Conformance.Equivalence.Certs.html#4996}{\htmlId{4996}{\htmlClass{Bound}{\text{gdeps}}}}\, \end{pmatrix}$

open CertDeps*

getCertDeps* : ∀ {pp dcert} → CertDeps* pp dcert → L.Deposits × L.Deposits
getCertDeps* deps = deps .depsᵈ , deps .depsᵍ

updateCertDeps : ∀ {pp dcert dcerts} → CertDeps* pp (dcert ∷ dcerts) → CertDeps* pp dcerts
updateCertDeps (delegate*    ddeps gdeps) = $\begin{pmatrix} \,\htmlId{5281}{\htmlClass{Symbol}{\text{\_}}}\, \\ \,\htmlId{5285}{\htmlClass{Symbol}{\text{\_}}}\, \\ \,\href{Ledger.Conway.Conformance.Equivalence.Certs.html#5264}{\htmlId{5289}{\htmlClass{Bound}{\text{ddeps}}}}\, \\ \,\href{Ledger.Conway.Conformance.Equivalence.Certs.html#5270}{\htmlId{5297}{\htmlClass{Bound}{\text{gdeps}}}}\, \end{pmatrix}$
updateCertDeps (dereg* _ _   ddeps gdeps) = $\begin{pmatrix} \,\htmlId{5352}{\htmlClass{Symbol}{\text{\_}}}\, \\ \,\htmlId{5356}{\htmlClass{Symbol}{\text{\_}}}\, \\ \,\href{Ledger.Conway.Conformance.Equivalence.Certs.html#5335}{\htmlId{5360}{\htmlClass{Bound}{\text{ddeps}}}}\, \\ \,\href{Ledger.Conway.Conformance.Equivalence.Certs.html#5341}{\htmlId{5368}{\htmlClass{Bound}{\text{gdeps}}}}\, \end{pmatrix}$
updateCertDeps (regpool*     ddeps gdeps) = $\begin{pmatrix} \,\htmlId{5423}{\htmlClass{Symbol}{\text{\_}}}\, \\ \,\htmlId{5427}{\htmlClass{Symbol}{\text{\_}}}\, \\ \,\href{Ledger.Conway.Conformance.Equivalence.Certs.html#5406}{\htmlId{5431}{\htmlClass{Bound}{\text{ddeps}}}}\, \\ \,\href{Ledger.Conway.Conformance.Equivalence.Certs.html#5412}{\htmlId{5439}{\htmlClass{Bound}{\text{gdeps}}}}\, \end{pmatrix}$
updateCertDeps (retirepool*  ddeps gdeps) = $\begin{pmatrix} \,\htmlId{5494}{\htmlClass{Symbol}{\text{\_}}}\, \\ \,\htmlId{5498}{\htmlClass{Symbol}{\text{\_}}}\, \\ \,\href{Ledger.Conway.Conformance.Equivalence.Certs.html#5477}{\htmlId{5502}{\htmlClass{Bound}{\text{ddeps}}}}\, \\ \,\href{Ledger.Conway.Conformance.Equivalence.Certs.html#5483}{\htmlId{5510}{\htmlClass{Bound}{\text{gdeps}}}}\, \end{pmatrix}$
updateCertDeps (regdrep*     ddeps gdeps) = $\begin{pmatrix} \,\htmlId{5565}{\htmlClass{Symbol}{\text{\_}}}\, \\ \,\htmlId{5569}{\htmlClass{Symbol}{\text{\_}}}\, \\ \,\href{Ledger.Conway.Conformance.Equivalence.Certs.html#5548}{\htmlId{5573}{\htmlClass{Bound}{\text{ddeps}}}}\, \\ \,\href{Ledger.Conway.Conformance.Equivalence.Certs.html#5554}{\htmlId{5581}{\htmlClass{Bound}{\text{gdeps}}}}\, \end{pmatrix}$
updateCertDeps (deregdrep* _ ddeps gdeps) = $\begin{pmatrix} \,\htmlId{5636}{\htmlClass{Symbol}{\text{\_}}}\, \\ \,\htmlId{5640}{\htmlClass{Symbol}{\text{\_}}}\, \\ \,\href{Ledger.Conway.Conformance.Equivalence.Certs.html#5619}{\htmlId{5644}{\htmlClass{Bound}{\text{ddeps}}}}\, \\ \,\href{Ledger.Conway.Conformance.Equivalence.Certs.html#5625}{\htmlId{5652}{\htmlClass{Bound}{\text{gdeps}}}}\, \end{pmatrix}$
updateCertDeps (ccreghot*    ddeps gdeps) = $\begin{pmatrix} \,\htmlId{5707}{\htmlClass{Symbol}{\text{\_}}}\, \\ \,\htmlId{5711}{\htmlClass{Symbol}{\text{\_}}}\, \\ \,\href{Ledger.Conway.Conformance.Equivalence.Certs.html#5690}{\htmlId{5715}{\htmlClass{Bound}{\text{ddeps}}}}\, \\ \,\href{Ledger.Conway.Conformance.Equivalence.Certs.html#5696}{\htmlId{5723}{\htmlClass{Bound}{\text{gdeps}}}}\, \end{pmatrix}$
updateCertDeps (reg*         ddeps gdeps) = $\begin{pmatrix} \,\htmlId{5778}{\htmlClass{Symbol}{\text{\_}}}\, \\ \,\htmlId{5782}{\htmlClass{Symbol}{\text{\_}}}\, \\ \,\href{Ledger.Conway.Conformance.Equivalence.Certs.html#5761}{\htmlId{5786}{\htmlClass{Bound}{\text{ddeps}}}}\, \\ \,\href{Ledger.Conway.Conformance.Equivalence.Certs.html#5767}{\htmlId{5794}{\htmlClass{Bound}{\text{gdeps}}}}\, \end{pmatrix}$

updateCertDeps* : ∀ {pp} dcerts → CertDeps* pp dcerts → CertDeps* pp []
updateCertDeps* []               deps = deps
updateCertDeps* (dcert ∷ dcerts) deps = updateCertDeps* dcerts (updateCertDeps deps)

instance

  CertStToConf : L.Deposits × L.Deposits ⊢ L.CertState ⭆ C.CertState
  CertStToConf .convⁱ (ddeps , gdeps) certState =
    let open L.CertState certState in
    $\begin{pmatrix} \,\href{Ledger.Conway.Conformance.Equivalence.Certs.html#6109}{\htmlId{6180}{\htmlClass{Bound}{\text{ddeps}}}}\, \,\href{Ledger.Conway.Conformance.Equivalence.Convert.html#380}{\htmlId{6186}{\htmlClass{Function Operator}{\text{⊢conv}}}}\, \,\href{Ledger.Conway.Specification.Certs.html#4940}{\htmlId{6192}{\htmlClass{Field}{\text{dState}}}}\, \\ \,\href{Ledger.Conway.Specification.Certs.html#4960}{\htmlId{6201}{\htmlClass{Field}{\text{pState}}}}\, \\ \,\href{Ledger.Conway.Conformance.Equivalence.Certs.html#6117}{\htmlId{6210}{\htmlClass{Bound}{\text{gdeps}}}}\, \,\href{Ledger.Conway.Conformance.Equivalence.Convert.html#380}{\htmlId{6216}{\htmlClass{Function Operator}{\text{⊢conv}}}}\, \,\href{Ledger.Conway.Specification.Certs.html#4980}{\htmlId{6222}{\htmlClass{Field}{\text{gState}}}}\, \end{pmatrix}$

  CertStFromConf : C.CertState ⭆ L.CertState
  CertStFromConf .convⁱ _ certState =
    let open C.CertState certState in
    $\begin{pmatrix} \,\href{Ledger.Conway.Conformance.Equivalence.Convert.html#562}{\htmlId{6359}{\htmlClass{Function}{\text{conv}}}}\, \,\href{Ledger.Conway.Conformance.Certs.html#1117}{\htmlId{6364}{\htmlClass{Field}{\text{dState}}}}\, \\ \,\href{Ledger.Conway.Conformance.Certs.html#1137}{\htmlId{6373}{\htmlClass{Field}{\text{pState}}}}\, \\ \,\href{Ledger.Conway.Conformance.Equivalence.Convert.html#562}{\htmlId{6382}{\htmlClass{Function}{\text{conv}}}}\, \,\href{Ledger.Conway.Conformance.Certs.html#1157}{\htmlId{6387}{\htmlClass{Field}{\text{gState}}}}\, \end{pmatrix}$

  PRE-CERTToConf : ∀ {Γ s s'}
                 → L.Deposits × L.Deposits
                   ⊢ Γ L.⊢ s ⇀⦇ _ ,PRE-CERT⦈ s' ⭆ⁱ λ deposits _ →
                     Γ C.⊢ (deposits ⊢conv s) ⇀⦇ _ ,PRE-CERT⦈ (deposits ⊢conv s')
  PRE-CERTToConf .convⁱ deposits (L.CERT-pre h) = C.CERT-pre h

  POST-CERTToConf : ∀ {Γ s s'}
                 → L.Deposits × L.Deposits
                   ⊢ Γ L.⊢ s ⇀⦇ _ ,POST-CERT⦈ s' ⭆ⁱ λ deposits _ →
                     Γ C.⊢ (deposits ⊢conv s) ⇀⦇ _ ,POST-CERT⦈ (deposits ⊢conv s')
  POST-CERTToConf .convⁱ deposits L.CERT-post = C.CERT-post

  DELEGToConf : ∀ {Γ s dcert dcerts s'}
                  (open L.DelegEnv Γ renaming (pparams to pp))
              → CertDeps* pp (dcert ∷ dcerts) ⊢
                 Γ L.⊢ s ⇀⦇ dcert ,DELEG⦈ s' ⭆ⁱ λ deposits _ →
                 Γ C.⊢ (deposits .depsᵈ ⊢conv s) ⇀⦇ dcert ,DELEG⦈ (updateCertDeps deposits .depsᵈ ⊢conv s')
  DELEGToConf .convⁱ (delegate* _ _) (L.DELEG-delegate h) = C.DELEG-delegate h
  DELEGToConf .convⁱ (dereg* v w _ _)  (L.DELEG-dereg h)    = C.DELEG-dereg (h , v , w)
  DELEGToConf .convⁱ (reg* _ _) (L.DELEG-reg h) = C.DELEG-reg h

  POOLToConf : ∀ {pp s dcert s'} → pp L.⊢ s ⇀⦇ dcert ,POOL⦈ s' ⭆ pp C.⊢ s ⇀⦇ dcert ,POOL⦈ s'
  POOLToConf .convⁱ _ L.POOL-regpool = C.POOL-regpool
  POOLToConf .convⁱ _ L.POOL-retirepool  = C.POOL-retirepool

  GOVCERTToConf : ∀ {Γ s dcert dcerts s'}
                  (open L.CertEnv Γ using (pp))
                → CertDeps* pp (dcert ∷ dcerts) ⊢
                   Γ L.⊢ s ⇀⦇ dcert ,GOVCERT⦈ s' ⭆ⁱ λ deposits _ →
                   Γ C.⊢ (deposits .depsᵍ ⊢conv s) ⇀⦇ dcert ,GOVCERT⦈ (updateCertDeps deposits .depsᵍ ⊢conv s')
  GOVCERTToConf .convⁱ (regdrep* _ _)     (L.GOVCERT-regdrep h) = C.GOVCERT-regdrep h
  GOVCERTToConf .convⁱ (deregdrep* v _ _) (L.GOVCERT-deregdrep h) = C.GOVCERT-deregdrep (h , v)
  GOVCERTToConf .convⁱ (ccreghot* _ _)    (L.GOVCERT-ccreghot h)  = C.GOVCERT-ccreghot h

  CERTToConf : ∀ {Γ s dcert dcerts s'} (open L.CertEnv Γ using (pp))
             → CertDeps* pp (dcert ∷ dcerts) ⊢
                Γ L.⊢ s ⇀⦇ dcert ,CERT⦈ s' ⭆ⁱ λ deposits _ →
                Γ C.⊢ (getCertDeps* deposits ⊢conv s) ⇀⦇ dcert ,CERT⦈ (getCertDeps* (updateCertDeps deposits) ⊢conv s')
  CERTToConf .convⁱ deposits@(delegate* _ _)    (L.CERT-deleg deleg)  = C.CERT-deleg (deposits ⊢conv deleg)
  CERTToConf .convⁱ deposits@(dereg* _ _ _ _)   (L.CERT-deleg deleg)  = C.CERT-deleg (deposits ⊢conv deleg)
  CERTToConf .convⁱ deposits@(regpool* _ _)     (L.CERT-pool pool)    = C.CERT-pool (conv pool)
  CERTToConf .convⁱ deposits@(retirepool* _ _)  (L.CERT-pool pool)    = C.CERT-pool (conv pool)
  CERTToConf .convⁱ deposits@(regdrep* _ _)     (L.CERT-vdel govcert) = C.CERT-vdel (deposits ⊢conv govcert)
  CERTToConf .convⁱ deposits@(deregdrep* _ _ _) (L.CERT-vdel govcert) = C.CERT-vdel (deposits ⊢conv govcert)
  CERTToConf .convⁱ deposits@(ccreghot* _ _)    (L.CERT-vdel govcert) = C.CERT-vdel (deposits ⊢conv govcert)
  CERTToConf .convⁱ deposits@(reg* _ _)         (L.CERT-deleg deleg)  = C.CERT-deleg (deposits ⊢conv deleg)

  CERT-POST-CERTToConf : ∀ {Γ s dcerts s'} (let open L.CertEnv Γ)
    → CertDeps* pp dcerts
      ⊢ RunTraceAndThen L._⊢_⇀⦇_,CERT⦈_ L._⊢_⇀⦇_,POST-CERT⦈_ Γ s dcerts s'
        ⭆ⁱ λ deposits _ → RunTraceAndThen C._⊢_⇀⦇_,CERT⦈_ C._⊢_⇀⦇_,POST-CERT⦈_
                            Γ (getCertDeps* deposits ⊢conv s) dcerts
                              (getCertDeps* (updateCertDeps* dcerts deposits) ⊢conv s')
  CERT-POST-CERTToConf .convⁱ deposits (run-[] x) = run-[] ((deposits .depsᵈ , deposits .depsᵍ) ⊢conv x)
  CERT-POST-CERTToConf .convⁱ deposits (run-∷ x x₁) = run-∷ (deposits ⊢conv x) (updateCertDeps deposits ⊢conv x₁)


  CERTSToConf : ∀ {Γ s dcerts s'} (let open L.CertEnv Γ)
    → CertDeps* pp dcerts
      ⊢ RunTraceAfterAndThen L._⊢_⇀⦇_,PRE-CERT⦈_ L._⊢_⇀⦇_,CERT⦈_ L._⊢_⇀⦇_,POST-CERT⦈_ Γ s dcerts s'
      ⭆ⁱ λ deposits _ → RunTraceAfterAndThen C._⊢_⇀⦇_,PRE-CERT⦈_ C._⊢_⇀⦇_,CERT⦈_ C._⊢_⇀⦇_,POST-CERT⦈_
                          Γ (getCertDeps* deposits ⊢conv s) dcerts
                            (getCertDeps* (updateCertDeps* dcerts deposits) ⊢conv s')
  CERTSToConf .convⁱ deposits (run (pre , cert-post)) = run (getCertDeps* deposits ⊢conv pre , deposits ⊢conv cert-post)

-- Converting form Conformance is easier since the deposit tracking disappears.
instance
  DELEGFromConf : ∀ {Γ s dcert s'}
                → Γ C.⊢ s ⇀⦇ dcert ,DELEG⦈ s' ⭆
                  Γ L.⊢ conv s ⇀⦇ dcert ,DELEG⦈ conv s'
  DELEGFromConf .convⁱ _ (C.DELEG-delegate h)    = L.DELEG-delegate h
  DELEGFromConf .convⁱ _ (C.DELEG-dereg (h , _)) = L.DELEG-dereg h
  DELEGFromConf .convⁱ _ (C.DELEG-reg h)         = L.DELEG-reg h

  GOVCERTFromConf : ∀ {Γ s dcert s'}
                  → Γ C.⊢ s ⇀⦇ dcert ,GOVCERT⦈ s' ⭆
                    Γ L.⊢ conv s ⇀⦇ dcert ,GOVCERT⦈ conv s'
  GOVCERTFromConf .convⁱ _ (C.GOVCERT-regdrep h)   = C.GOVCERT-regdrep h
  GOVCERTFromConf .convⁱ _ (C.GOVCERT-deregdrep (h , _)) = C.GOVCERT-deregdrep h
  GOVCERTFromConf .convⁱ _ (C.GOVCERT-ccreghot h)  = C.GOVCERT-ccreghot h

  CERTFromConf : ∀ {Γ s dcert s'} → Γ C.⊢ s ⇀⦇ dcert ,CERT⦈ s' ⭆ Γ L.⊢ conv s ⇀⦇ dcert ,CERT⦈ conv s'
  CERTFromConf .convⁱ _ (C.CERT-deleg deleg)  = L.CERT-deleg (conv deleg)
  CERTFromConf .convⁱ _ (C.CERT-pool pool)    = L.CERT-pool (conv pool)
  CERTFromConf .convⁱ _ (C.CERT-vdel govcert) = L.CERT-vdel (conv govcert)

  PRE-CERTFromConf : ∀ {Γ s s'}
                   → Γ C.⊢ s ⇀⦇ _ ,PRE-CERT⦈ s' ⭆
                     Γ L.⊢ (conv s) ⇀⦇ _ ,PRE-CERT⦈ (conv s')
  PRE-CERTFromConf .convⁱ _ (C.CERT-pre h) = L.CERT-pre h

  POST-CERTFromConf : ∀ {Γ s s'}
                   → Γ C.⊢ s ⇀⦇ _ ,POST-CERT⦈ s' ⭆
                     Γ L.⊢ (conv s) ⇀⦇ _ ,POST-CERT⦈ (conv s')
  POST-CERTFromConf .convⁱ _ C.CERT-post = L.CERT-post


  CERT-POST-CERTFromConf : ∀ {Γ s dcerts s'}
    → RunTraceAndThen C._⊢_⇀⦇_,CERT⦈_ C._⊢_⇀⦇_,POST-CERT⦈_ Γ s dcerts s'
      ⭆ RunTraceAndThen L._⊢_⇀⦇_,CERT⦈_ L._⊢_⇀⦇_,POST-CERT⦈_ Γ (conv s) dcerts (conv s')
  CERT-POST-CERTFromConf .convⁱ _ (run-[] x) = run-[] (conv x)
  CERT-POST-CERTFromConf .convⁱ _ (run-∷ x xs) = run-∷ (conv x) (conv xs)


  CERTSFromConf : ∀ {Γ s dcerts s'}
                 → RunTraceAfterAndThen C._⊢_⇀⦇_,PRE-CERT⦈_ C._⊢_⇀⦇_,CERT⦈_ C._⊢_⇀⦇_,POST-CERT⦈_ Γ s dcerts s' ⭆
                   RunTraceAfterAndThen L._⊢_⇀⦇_,PRE-CERT⦈_ L._⊢_⇀⦇_,CERT⦈_ L._⊢_⇀⦇_,POST-CERT⦈_ Γ (conv s) dcerts (conv s')
  CERTSFromConf .convⁱ _ (run (pre , cert-post)) = run ((conv pre) , conv cert-post)