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#4729}{\htmlId{919}{\htmlClass{Field}{\text{voteDelegs}}}}\, \\ \,\href{Ledger.Conway.Specification.Certs.html#4759}{\htmlId{932}{\htmlClass{Field}{\text{stakeDelegs}}}}\, \\ \,\href{Ledger.Conway.Specification.Certs.html#4790}{\htmlId{946}{\htmlClass{Field}{\text{rewards}}}}\, \\ \,\href{Ledger.Conway.Conformance.Equivalence.Certs.html#869}{\htmlId{956}{\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#747}{\htmlId{1080}{\htmlClass{Field}{\text{voteDelegs}}}}\, \\ \,\href{Ledger.Conway.Conformance.Certs.html#777}{\htmlId{1093}{\htmlClass{Field}{\text{stakeDelegs}}}}\, \\ \,\href{Ledger.Conway.Conformance.Certs.html#817}{\htmlId{1107}{\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#5003}{\htmlId{1240}{\htmlClass{Field}{\text{dreps}}}}\, \\ \,\href{Ledger.Conway.Specification.Certs.html#5026}{\htmlId{1248}{\htmlClass{Field}{\text{ccHotKeys}}}}\, \\ \,\href{Ledger.Conway.Conformance.Equivalence.Certs.html#1190}{\htmlId{1260}{\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#931}{\htmlId{1391}{\htmlClass{Field}{\text{dreps}}}}\, \\ \,\href{Ledger.Conway.Conformance.Certs.html#967}{\htmlId{1399}{\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
validᵈ : ValidDepsᵈ pp depsᵈ dcerts
validᵍ : ValidDepsᵍ pp depsᵍ dcerts
pattern delegate* ddeps gdeps = $\begin{pmatrix} \,\htmlId{4359}{\htmlClass{Symbol}{\text{\_}}}\, \\ \,\htmlId{4363}{\htmlClass{Symbol}{\text{\_}}}\, \\ \,\htmlId{4367}{\htmlClass{InductiveConstructor}{\text{delegate}}}\, \,\href{Ledger.Conway.Conformance.Equivalence.Certs.html#4378}{\htmlId{4378}{\htmlClass{Bound}{\text{ddeps}}}}\, \\ \,\htmlId{4386}{\htmlClass{InductiveConstructor}{\text{delegate}}}\, \,\href{Ledger.Conway.Conformance.Equivalence.Certs.html#4398}{\htmlId{4398}{\htmlClass{Bound}{\text{gdeps}}}}\, \end{pmatrix}$
pattern dereg* v w ddeps gdeps = $\begin{pmatrix} \,\htmlId{4444}{\htmlClass{Symbol}{\text{\_}}}\, \\ \,\htmlId{4448}{\htmlClass{Symbol}{\text{\_}}}\, \\ \,\htmlId{4452}{\htmlClass{InductiveConstructor}{\text{dereg}}}\, \,\href{Ledger.Conway.Conformance.Equivalence.Certs.html#4458}{\htmlId{4458}{\htmlClass{Bound}{\text{v}}}}\, \,\href{Ledger.Conway.Conformance.Equivalence.Certs.html#4460}{\htmlId{4460}{\htmlClass{Bound}{\text{w}}}}\, \,\href{Ledger.Conway.Conformance.Equivalence.Certs.html#4463}{\htmlId{4463}{\htmlClass{Bound}{\text{ddeps}}}}\, \\ \,\htmlId{4471}{\htmlClass{InductiveConstructor}{\text{dereg}}}\, \,\href{Ledger.Conway.Conformance.Equivalence.Certs.html#4483}{\htmlId{4483}{\htmlClass{Bound}{\text{gdeps}}}}\, \end{pmatrix}$
pattern regpool* ddeps gdeps = $\begin{pmatrix} \,\htmlId{4529}{\htmlClass{Symbol}{\text{\_}}}\, \\ \,\htmlId{4533}{\htmlClass{Symbol}{\text{\_}}}\, \\ \,\htmlId{4537}{\htmlClass{InductiveConstructor}{\text{regpool}}}\, \,\href{Ledger.Conway.Conformance.Equivalence.Certs.html#4548}{\htmlId{4548}{\htmlClass{Bound}{\text{ddeps}}}}\, \\ \,\htmlId{4556}{\htmlClass{InductiveConstructor}{\text{regpool}}}\, \,\href{Ledger.Conway.Conformance.Equivalence.Certs.html#4568}{\htmlId{4568}{\htmlClass{Bound}{\text{gdeps}}}}\, \end{pmatrix}$
pattern retirepool* ddeps gdeps = $\begin{pmatrix} \,\htmlId{4614}{\htmlClass{Symbol}{\text{\_}}}\, \\ \,\htmlId{4618}{\htmlClass{Symbol}{\text{\_}}}\, \\ \,\htmlId{4622}{\htmlClass{InductiveConstructor}{\text{retirepool}}}\, \,\href{Ledger.Conway.Conformance.Equivalence.Certs.html#4633}{\htmlId{4633}{\htmlClass{Bound}{\text{ddeps}}}}\, \\ \,\htmlId{4641}{\htmlClass{InductiveConstructor}{\text{retirepool}}}\, \,\href{Ledger.Conway.Conformance.Equivalence.Certs.html#4653}{\htmlId{4653}{\htmlClass{Bound}{\text{gdeps}}}}\, \end{pmatrix}$
pattern regdrep* ddeps gdeps = $\begin{pmatrix} \,\htmlId{4699}{\htmlClass{Symbol}{\text{\_}}}\, \\ \,\htmlId{4703}{\htmlClass{Symbol}{\text{\_}}}\, \\ \,\htmlId{4707}{\htmlClass{InductiveConstructor}{\text{regdrep}}}\, \,\href{Ledger.Conway.Conformance.Equivalence.Certs.html#4718}{\htmlId{4718}{\htmlClass{Bound}{\text{ddeps}}}}\, \\ \,\htmlId{4726}{\htmlClass{InductiveConstructor}{\text{regdrep}}}\, \,\href{Ledger.Conway.Conformance.Equivalence.Certs.html#4738}{\htmlId{4738}{\htmlClass{Bound}{\text{gdeps}}}}\, \end{pmatrix}$
pattern deregdrep* v ddeps gdeps = $\begin{pmatrix} \,\htmlId{4784}{\htmlClass{Symbol}{\text{\_}}}\, \\ \,\htmlId{4788}{\htmlClass{Symbol}{\text{\_}}}\, \\ \,\htmlId{4792}{\htmlClass{InductiveConstructor}{\text{deregdrep}}}\, \,\href{Ledger.Conway.Conformance.Equivalence.Certs.html#4803}{\htmlId{4803}{\htmlClass{Bound}{\text{ddeps}}}}\, \\ \,\htmlId{4811}{\htmlClass{InductiveConstructor}{\text{deregdrep}}}\, \,\href{Ledger.Conway.Conformance.Equivalence.Certs.html#4821}{\htmlId{4821}{\htmlClass{Bound}{\text{v}}}}\, \,\href{Ledger.Conway.Conformance.Equivalence.Certs.html#4823}{\htmlId{4823}{\htmlClass{Bound}{\text{gdeps}}}}\, \end{pmatrix}$
pattern ccreghot* ddeps gdeps = $\begin{pmatrix} \,\htmlId{4869}{\htmlClass{Symbol}{\text{\_}}}\, \\ \,\htmlId{4873}{\htmlClass{Symbol}{\text{\_}}}\, \\ \,\htmlId{4877}{\htmlClass{InductiveConstructor}{\text{ccreghot}}}\, \,\href{Ledger.Conway.Conformance.Equivalence.Certs.html#4888}{\htmlId{4888}{\htmlClass{Bound}{\text{ddeps}}}}\, \\ \,\htmlId{4896}{\htmlClass{InductiveConstructor}{\text{ccreghot}}}\, \,\href{Ledger.Conway.Conformance.Equivalence.Certs.html#4908}{\htmlId{4908}{\htmlClass{Bound}{\text{gdeps}}}}\, \end{pmatrix}$
pattern reg* ddeps gdeps = $\begin{pmatrix} \,\htmlId{4954}{\htmlClass{Symbol}{\text{\_}}}\, \\ \,\htmlId{4958}{\htmlClass{Symbol}{\text{\_}}}\, \\ \,\htmlId{4962}{\htmlClass{InductiveConstructor}{\text{reg}}}\, \,\href{Ledger.Conway.Conformance.Equivalence.Certs.html#4973}{\htmlId{4973}{\htmlClass{Bound}{\text{ddeps}}}}\, \\ \,\htmlId{4981}{\htmlClass{InductiveConstructor}{\text{reg}}}\, \,\href{Ledger.Conway.Conformance.Equivalence.Certs.html#4993}{\htmlId{4993}{\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{5278}{\htmlClass{Symbol}{\text{\_}}}\, \\ \,\htmlId{5282}{\htmlClass{Symbol}{\text{\_}}}\, \\ \,\href{Ledger.Conway.Conformance.Equivalence.Certs.html#5261}{\htmlId{5286}{\htmlClass{Bound}{\text{ddeps}}}}\, \\ \,\href{Ledger.Conway.Conformance.Equivalence.Certs.html#5267}{\htmlId{5294}{\htmlClass{Bound}{\text{gdeps}}}}\, \end{pmatrix}$
updateCertDeps (dereg* _ _ ddeps gdeps) = $\begin{pmatrix} \,\htmlId{5349}{\htmlClass{Symbol}{\text{\_}}}\, \\ \,\htmlId{5353}{\htmlClass{Symbol}{\text{\_}}}\, \\ \,\href{Ledger.Conway.Conformance.Equivalence.Certs.html#5332}{\htmlId{5357}{\htmlClass{Bound}{\text{ddeps}}}}\, \\ \,\href{Ledger.Conway.Conformance.Equivalence.Certs.html#5338}{\htmlId{5365}{\htmlClass{Bound}{\text{gdeps}}}}\, \end{pmatrix}$
updateCertDeps (regpool* ddeps gdeps) = $\begin{pmatrix} \,\htmlId{5420}{\htmlClass{Symbol}{\text{\_}}}\, \\ \,\htmlId{5424}{\htmlClass{Symbol}{\text{\_}}}\, \\ \,\href{Ledger.Conway.Conformance.Equivalence.Certs.html#5403}{\htmlId{5428}{\htmlClass{Bound}{\text{ddeps}}}}\, \\ \,\href{Ledger.Conway.Conformance.Equivalence.Certs.html#5409}{\htmlId{5436}{\htmlClass{Bound}{\text{gdeps}}}}\, \end{pmatrix}$
updateCertDeps (retirepool* ddeps gdeps) = $\begin{pmatrix} \,\htmlId{5491}{\htmlClass{Symbol}{\text{\_}}}\, \\ \,\htmlId{5495}{\htmlClass{Symbol}{\text{\_}}}\, \\ \,\href{Ledger.Conway.Conformance.Equivalence.Certs.html#5474}{\htmlId{5499}{\htmlClass{Bound}{\text{ddeps}}}}\, \\ \,\href{Ledger.Conway.Conformance.Equivalence.Certs.html#5480}{\htmlId{5507}{\htmlClass{Bound}{\text{gdeps}}}}\, \end{pmatrix}$
updateCertDeps (regdrep* ddeps gdeps) = $\begin{pmatrix} \,\htmlId{5562}{\htmlClass{Symbol}{\text{\_}}}\, \\ \,\htmlId{5566}{\htmlClass{Symbol}{\text{\_}}}\, \\ \,\href{Ledger.Conway.Conformance.Equivalence.Certs.html#5545}{\htmlId{5570}{\htmlClass{Bound}{\text{ddeps}}}}\, \\ \,\href{Ledger.Conway.Conformance.Equivalence.Certs.html#5551}{\htmlId{5578}{\htmlClass{Bound}{\text{gdeps}}}}\, \end{pmatrix}$
updateCertDeps (deregdrep* _ ddeps gdeps) = $\begin{pmatrix} \,\htmlId{5633}{\htmlClass{Symbol}{\text{\_}}}\, \\ \,\htmlId{5637}{\htmlClass{Symbol}{\text{\_}}}\, \\ \,\href{Ledger.Conway.Conformance.Equivalence.Certs.html#5616}{\htmlId{5641}{\htmlClass{Bound}{\text{ddeps}}}}\, \\ \,\href{Ledger.Conway.Conformance.Equivalence.Certs.html#5622}{\htmlId{5649}{\htmlClass{Bound}{\text{gdeps}}}}\, \end{pmatrix}$
updateCertDeps (ccreghot* ddeps gdeps) = $\begin{pmatrix} \,\htmlId{5704}{\htmlClass{Symbol}{\text{\_}}}\, \\ \,\htmlId{5708}{\htmlClass{Symbol}{\text{\_}}}\, \\ \,\href{Ledger.Conway.Conformance.Equivalence.Certs.html#5687}{\htmlId{5712}{\htmlClass{Bound}{\text{ddeps}}}}\, \\ \,\href{Ledger.Conway.Conformance.Equivalence.Certs.html#5693}{\htmlId{5720}{\htmlClass{Bound}{\text{gdeps}}}}\, \end{pmatrix}$
updateCertDeps (reg* ddeps gdeps) = $\begin{pmatrix} \,\htmlId{5775}{\htmlClass{Symbol}{\text{\_}}}\, \\ \,\htmlId{5779}{\htmlClass{Symbol}{\text{\_}}}\, \\ \,\href{Ledger.Conway.Conformance.Equivalence.Certs.html#5758}{\htmlId{5783}{\htmlClass{Bound}{\text{ddeps}}}}\, \\ \,\href{Ledger.Conway.Conformance.Equivalence.Certs.html#5764}{\htmlId{5791}{\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#6106}{\htmlId{6177}{\htmlClass{Bound}{\text{ddeps}}}}\, \,\href{Ledger.Conway.Conformance.Equivalence.Convert.html#377}{\htmlId{6183}{\htmlClass{Function Operator}{\text{⊢conv}}}}\, \,\href{Ledger.Conway.Specification.Certs.html#5175}{\htmlId{6189}{\htmlClass{Field}{\text{dState}}}}\, \\ \,\href{Ledger.Conway.Specification.Certs.html#5195}{\htmlId{6198}{\htmlClass{Field}{\text{pState}}}}\, \\ \,\href{Ledger.Conway.Conformance.Equivalence.Certs.html#6114}{\htmlId{6207}{\htmlClass{Bound}{\text{gdeps}}}}\, \,\href{Ledger.Conway.Conformance.Equivalence.Convert.html#377}{\htmlId{6213}{\htmlClass{Function Operator}{\text{⊢conv}}}}\, \,\href{Ledger.Conway.Specification.Certs.html#5215}{\htmlId{6219}{\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#559}{\htmlId{6356}{\htmlClass{Function}{\text{conv}}}}\, \,\href{Ledger.Conway.Conformance.Certs.html#1103}{\htmlId{6361}{\htmlClass{Field}{\text{dState}}}}\, \\ \,\href{Ledger.Conway.Conformance.Certs.html#1123}{\htmlId{6370}{\htmlClass{Field}{\text{pState}}}}\, \\ \,\href{Ledger.Conway.Conformance.Equivalence.Convert.html#559}{\htmlId{6379}{\htmlClass{Function}{\text{conv}}}}\, \,\href{Ledger.Conway.Conformance.Certs.html#1143}{\htmlId{6384}{\htmlClass{Field}{\text{gState}}}}\, \end{pmatrix}$
CERTBASEToConf : ∀ {Γ s s'}
→ L.Deposits × L.Deposits
⊢ Γ L.⊢ s ⇀⦇ _ ,CERTBASE⦈ s' ⭆ⁱ λ deposits _ →
Γ C.⊢ (deposits ⊢conv s) ⇀⦇ _ ,CERTBASE⦈ (deposits ⊢conv s')
CERTBASEToConf .convⁱ deposits (L.CERT-base h) = C.CERT-base h
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 h) = C.POOL-regpool h
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)
CERTS'ToConf : ∀ {Γ s dcerts s'} (let open L.CertEnv Γ)
→ CertDeps* pp dcerts
⊢ ReflexiveTransitiveClosure {sts = L._⊢_⇀⦇_,CERT⦈_} Γ s dcerts s' ⭆ⁱ λ deposits _ →
ReflexiveTransitiveClosure {sts = C._⊢_⇀⦇_,CERT⦈_}
Γ (getCertDeps* deposits ⊢conv s) dcerts
(getCertDeps* (updateCertDeps* dcerts deposits) ⊢conv s')
CERTS'ToConf .convⁱ deposits (BS-base Id-nop) = BS-base Id-nop
CERTS'ToConf .convⁱ deposits (BS-ind r rs) = BS-ind (deposits ⊢conv r) (updateCertDeps deposits ⊢conv rs)
CERTSToConf : ∀ {Γ s dcerts s'} (let open L.CertEnv Γ)
→ CertDeps* pp dcerts
⊢ Γ 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)
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
POOLFromConf : ∀ {pp s dcert s'} → pp C.⊢ s ⇀⦇ dcert ,POOL⦈ s' ⭆ pp L.⊢ s ⇀⦇ dcert ,POOL⦈ s'
POOLFromConf .convⁱ _ (C.POOL-regpool h) = L.POOL-regpool h
POOLFromConf .convⁱ _ C.POOL-retirepool = L.POOL-retirepool
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)
CERTBASEFromConf : ∀ {Γ s s'}
→ Γ C.⊢ s ⇀⦇ _ ,CERTBASE⦈ s' ⭆
Γ L.⊢ (conv s) ⇀⦇ _ ,CERTBASE⦈ (conv s')
CERTBASEFromConf .convⁱ _ (C.CERT-base h) = L.CERT-base h
CERTS'FromConf : ∀ {Γ s dcerts s'}
→ ReflexiveTransitiveClosure {sts = C._⊢_⇀⦇_,CERT⦈_} Γ s dcerts s' ⭆
ReflexiveTransitiveClosure {sts = L._⊢_⇀⦇_,CERT⦈_} Γ (conv s) dcerts (conv s')
CERTS'FromConf .convⁱ _ (BS-base Id-nop) = BS-base Id-nop
CERTS'FromConf .convⁱ _ (BS-ind r rs) = BS-ind (conv r) (conv rs)
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)