Skip to content

Made CERTBASE get applied at the end of CERTS #710

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Open
wants to merge 3 commits into
base: master
Choose a base branch
from
Open

Made CERTBASE get applied at the end of CERTS #710

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
3 commits
Select commit Hold shift + click to select a range
5109173
Made CERTBASE be called last in CERTS
Soupstraw Mar 12, 2025
4e33baf
moved a check from CERTS to LEDGER
Soupstraw Mar 14, 2025
57731ff
moved rewards check to LEDGER
Soupstraw Mar 14, 2025
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
1 change: 0 additions & 1 deletion default.nix
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -74,7 +74,6 @@ let

in rec
{

agdaWithDeps = agdaWithPkgs deps;

latex = texlive.combine {
Expand Down
7 changes: 2 additions & 5 deletions src/Ledger/Certs.lagda
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -320,7 +320,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}
Expand Down Expand Up @@ -466,15 +466,12 @@ data _⊢_⇀⦇_,CERTBASE⦈_ where
validVoteDelegs = voteDelegs ∣^ ( mapˢ (credVoter DRep) (dom dReps)
∪ fromList (noConfidenceRep ∷ abstainRep ∷ []) )
in
∙ filter isKeyHash wdrlCreds ⊆ dom voteDelegs
∙ mapˢ (map₁ stake) (wdrls ˢ) ⊆ rewards ˢ
Comment on lines -469 to -470
Copy link
Collaborator

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

@Soupstraw I see you moved these two premises to the LEDGER rule. Could you explain why they can't remain here? (I need them here for the proof of the CERTBASE-pov lemma, which is used in the proof of CERTS-pov.)

Copy link
Contributor Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

The problem with the first premise is that in the implementation we check it in the LEDGER rule. I guess we could keep it in the same place in the spec and change the implementation instead. The important part is that it's still checked before the certs are applied, like it was before this PR.

The thing that was wrong was that validVoteDelegs was applied before the certificates had been applied. This caused DRep delegations to not get removed when the transaction had a unregdrep certificate, because the filter function used the old dReps map, where the DRep was still registered.

I think the second one could actually stay here as well if we call CERTBASE at the start, but I think it makes way more sense to do anything related to withdrawals in the LEDGER rule. The fact that we do the withrawals logic in CERTS is because that's how it was done in Shelley, before we had a dedicated CERTS rule. The withdrawals don't really have anything to do with certificates, so I don't think it makes sense to keep it here, and I've talked with @WhatisRT and @lehins about this and they both agreed. I've already moved that check to LEDGER in the implementation, so I think it'd be good to do it here also.

I think the best solution would be to have two base cases in the CERTS rule, one that gets applied at the start and then another that gets applied at the end. That way we can do the checks before we apply the certificates, and then update the voteDelegs only once we have applied all the certificates.

Copy link
Collaborator

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Okay, I'll have to take a closer look at this to refresh my memory and really understand exactly what's going on. My impression was that the premises that were moved were required for the CERTS-pov proof... but it's possible the statement of that property turns out to be wrong and/or not actually what we want. I think you understand this issue better than anyone right now, so I trust your judgment on it, and would be grateful if you could take some time at the water cooler today to explain it. I will then help with this PR by fixing the CERTS-pov theorem statement and construct a new proof of it.

────────────────────────────────
⟦ e , pp , vs , wdrls , cc ⟧ ⊢
⟦ ⟦ voteDelegs , stakeDelegs , rewards ⟧
, stᵖ
, ⟦ dReps , ccHotKeys ⟧
⟧ ⇀⦇ _ ,CERTBASE⦈
⟦ ⟦ validVoteDelegs , stakeDelegs , constMap wdrlCreds 0 ∪ˡ rewards ⟧
⟦ ⟦ validVoteDelegs , stakeDelegs , rewards ⟧
, stᵖ
, ⟦ refreshedDReps , ccHotKeys ⟧
⟧
Expand Down
27 changes: 9 additions & 18 deletions src/Ledger/Certs/Properties.agda
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -148,15 +148,13 @@ instance
open GState (gState cs); open DState (dState cs)
refresh = mapPartial getDRepVote (fromList votes)
refreshedDReps = mapValueRestricted (const (CertEnv.epoch ce + drepActivity)) dreps refresh
in case ¿ filterˢ isKeyHash (mapˢ RwdAddr.stake (dom wdrls)) ⊆ dom voteDelegs
× mapˢ (map₁ RwdAddr.stake) (wdrls ˢ) ⊆ rewards ˢ ¿ of λ where
(yes p) → success (-, CERT-base p)
in case ¿ mapˢ (map₁ RwdAddr.stake) (wdrls ˢ) ⊆ rewards ˢ ¿ of λ where
(yes p) → success (-, CERT-base (p {_}))
(no ¬p) → failure (genErrors ¬p)
Computational-CERTBASE .completeness ce st _ st' (CERT-base p)
rewrite let dState = CertState.dState st; open DState dState in
dec-yes ¿ filterˢ isKeyHash (mapˢ RwdAddr.stake (dom (CertEnv.wdrls ce))) ⊆ dom voteDelegs
× mapˢ (map₁ RwdAddr.stake) (CertEnv.wdrls ce ˢ) ⊆ rewards ˢ ¿
p .proj₂ = refl
Computational-CERTBASE .completeness ce st _ st' (CERT-base p) with
¿ mapˢ (map₁ RwdAddr.stake) (CertEnv.wdrls ce ˢ) ⊆ (st .CertState.dState .DState.rewards) ˢ ¿
... | yes _ = refl
... | no ¬q = ⊥-elim (¬q p)

Computational-CERTS : Computational _⊢_⇀⦇_,CERTS⦈_ String
Computational-CERTS = it
Expand Down Expand Up @@ -256,7 +254,7 @@ module _ {Γ : CertEnv}

CERTBASE-pov {s = cs}
{s' = cs'}
(CERT-base {pp}{vs}{e}{dreps}{wdrls} (_ , wdrlsCC⊆rwds)) =
(CERT-base {pp}{vs}{e}{dreps}{wdrls} wdrlsCC⊆rwds) =
let
open DState (dState cs )
open DState (dState cs') renaming (rewards to rewards')
Expand Down Expand Up @@ -301,16 +299,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)
13 changes: 5 additions & 8 deletions src/Ledger/Conway/Conformance/Certs.agda
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -200,24 +200,21 @@ data _⊢_⇀⦇_,CERT⦈_ : CertEnv → CertState → DCert → CertState → T
data _⊢_⇀⦇_,CERTBASE⦈_ : CertEnv → CertState → ⊤ → CertState → Type where
CERT-base :
let open PParams pp
refresh = mapPartial getDRepVote (fromList vs)
refreshedDReps = mapValueRestricted (const (e + drepActivity)) dReps refresh
wdrlCreds = mapˢ stake (dom wdrls)
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 ∷ []))
in
∙ filterˢ isKeyHash wdrlCreds ⊆ dom voteDelegs
∙ mapˢ (map₁ stake) (wdrls ˢ) ⊆ rewards ˢ
────────────────────────────────
⟦ e , pp , vs , wdrls , cc ⟧ ⊢
⟦ ⟦ voteDelegs , stakeDelegs , rewards , ddep ⟧
, stᵖ
, ⟦ dReps , ccHotKeys , gdep ⟧
⟧
⇀⦇ _ ,CERTBASE⦈
⟦ ⟦ validVoteDelegs , stakeDelegs , constMap wdrlCreds 0 ∪ˡ rewards , ddep ⟧
⟦ ⟦ validVoteDelegs , stakeDelegs , rewards , ddep ⟧
, stᵖ
, ⟦ refreshedDReps , ccHotKeys , gdep ⟧
⟧

_⊢_⇀⦇_,CERTS⦈_ : CertEnv → CertState → List DCert → CertState → Type
_⊢_⇀⦇_,CERTS⦈_ = ReflexiveTransitiveClosureᵇ' {_⊢_⇀⟦_⟧ᵇ_ = _⊢_⇀⦇_,CERTBASE⦈_}{_⊢_⇀⦇_,CERT⦈_}
_⊢_⇀⦇_,CERTS⦈_ = ReflexiveTransitiveClosureᵇ {_⊢_⇀⟦_⟧ᵇ_ = _⊢_⇀⦇_,CERTBASE⦈_}{_⊢_⇀⦇_,CERT⦈_}
11 changes: 2 additions & 9 deletions src/Ledger/Conway/Conformance/Certs/Properties.agda
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -194,15 +194,8 @@ instance

goal : ComputationResult String
(∃-syntax (_⊢_⇀⦇_,CERTBASE⦈_ ⟦ CertEnv.epoch ce , pp , votes , wdrls , _ ⟧ st sig))
goal = case ¿ filterˢ isKeyHash (mapˢ RwdAddr.stake (dom wdrls)) ⊆ dom voteDelegs
× mapˢ (map₁ RwdAddr.stake) (wdrls ˢ) ⊆ rewards ˢ ¿ of λ where
(yes p) → success (-, CERT-base p)
(no ¬p) → failure (genErr ¬p)
Computational-CERTBASE .completeness ce st _ st' (CERT-base p)
rewrite let dState = CertState.dState st; open DState dState; open CertEnv ce in
dec-yes ¿ filterˢ isKeyHash (mapˢ RwdAddr.stake (dom wdrls)) ⊆ dom voteDelegs
× mapˢ (map₁ RwdAddr.stake) (wdrls ˢ) ⊆ rewards ˢ ¿
p .proj₂ = refl
goal = success (-, CERT-base)
Computational-CERTBASE .completeness ce st _ st' CERT-base = refl

Computational-CERTS : Computational _⊢_⇀⦇_,CERTS⦈_ String
Computational-CERTS = it
64 changes: 19 additions & 45 deletions src/Ledger/Conway/Conformance/Equivalence.agda
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -104,7 +104,7 @@ lem-cert-deposits-valid : ∀ {Γ s tx s'} (open L.LEnv Γ using (pparams))
→ isValid tx ≡ true
→ Γ L.⊢ s ⇀⦇ tx ,LEDGER⦈ s'
→ updateLedgerDeps pparams tx (certDeposits s) ≡ᵈ certDeposits s'
lem-cert-deposits-valid {Γ} {s} {tx} {s'} refl (L.LEDGER-V⋯ refl utxow certs gov) rewrite sym (lemUpdateDeposits refl utxow) =
lem-cert-deposits-valid {Γ} {s} {tx} {s'} refl (L.LEDGER-V⋯ refl utxow certs u gov) rewrite sym (lemUpdateDeposits refl utxow) =
lem-upd-ddeps pparams deps tx ,
lem-upd-gdeps pparams deps tx
where
Expand Down Expand Up @@ -137,7 +137,7 @@ instance
certDeposits-s' ≡ᵈ certDeposits s'
× Γ C.⊢ (certDeposits s ⊢conv s) ⇀⦇ tx ,LEDGER⦈ (certDeposits-s' ⊢conv s')
-- LEDGERToConf {Γ} {s} {tx} {s'} .convⁱ (cdeps , eq-cdeps) r@(L.LEDGER-V⋯ refl utxow certs gov) =
LEDGERToConf {Γ} {s} {tx} {s'} .convⁱ _ r@(L.LEDGER-V⋯ refl utxow certs gov) =
LEDGERToConf {Γ} {s} {tx} {s'} .convⁱ _ r@(L.LEDGER-V⋯ refl utxow certs u gov) =
updateLedgerDeps pparams tx (certDeposits s)
, lem-cert-deposits-valid refl r
, subst₂ (λ • ◆ → Γ C.⊢ getCertDeps* cdeposits ⊢conv s ⇀⦇ tx ,LEDGER⦈ ⟦ • , _ , ◆ ⟧)
Expand All @@ -157,7 +157,7 @@ instance
certs' : _ C.⊢ (getCertDeps* cdeposits ⊢conv certState) ⇀⦇ txcerts ,CERTS⦈ certStateC'
certs' = cdeposits ⊢conv certs
ledger' : Γ C.⊢ (getCertDeps* cdeposits ⊢conv s) ⇀⦇ tx ,LEDGER⦈ C.⟦ utxoStC' , govSt' , certStateC' ⟧ˡ
ledger' = C.LEDGER-V⋯ refl utxow' certs' gov
ledger' = C.LEDGER-V⋯ refl utxow' certs' u gov
utxoEq : utxoStC' ≡ utxoSt'
utxoEq = cong (λ • → ⟦ _ , _ , • , _ ⟧)
(lemUpdateDeposits refl utxow)
Expand Down Expand Up @@ -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) =
Expand All @@ -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
Expand All @@ -242,7 +228,7 @@ instance
⭆ Γ L.⊢ conv s ⇀⦇ tx ,LEDGER⦈ conv s'
LEDGERFromConf .convⁱ _ (C.LEDGER-I⋯ invalid utxow) with inj₁ invalid ⊢conv utxow
... | utxow' rewrite lemInvalidDepositsC invalid utxow = L.LEDGER-I⋯ invalid utxow'
LEDGERFromConf {Γ} {s} {tx} {s'} .convⁱ wf (C.LEDGER-V⋯ refl utxow certs gov) =
LEDGERFromConf {Γ} {s} {tx} {s'} .convⁱ wf (C.LEDGER-V⋯ refl utxow certs u gov) =
subst (λ • → Γ L.⊢ conv s ⇀⦇ tx ,LEDGER⦈ ⟦ • , govSt' , conv certSt' ⟧) eqUtxo ledger'
where
open C.LEnv Γ
Expand All @@ -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
Expand All @@ -265,14 +251,14 @@ instance
ledger' : Γ L.⊢ conv s ⇀⦇ tx ,LEDGER⦈ L.⟦ setDeposits (utxowDeposits utxow) utxoSt'
, govSt'
, conv certSt' ⟧ˡ
ledger' = L.LEDGER-V⋯ refl utxow' (conv certs) gov
ledger' = L.LEDGER-V⋯ refl utxow' (conv certs) u gov

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
Expand All @@ -282,13 +268,8 @@ 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
lemWellformed {Γ} {s = ls} {tx} {s' = ls'} wf (C.LEDGER-V⋯ refl utxo certs u gov) = goal
where
open C.LState ls renaming (certState to certSt)
open C.LState ls' renaming (utxoSt to utxoSt'; certState to certSt')
Expand All @@ -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')
Expand Down Expand Up @@ -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₁'
Expand Down Expand Up @@ -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⦈_}

Expand All @@ -403,9 +377,9 @@ opaque
→ deps₁ ≡ᵈ deps₂
→ Γ 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
in deps₂' , eqd' , C.LEDGER-V⋯ refl utxo certs' gov
castLEDGER {Γ} {tx} {s} {s'} deps₁ deps₂ deps₁' eqd (C.LEDGER-V⋯ refl utxo certs u gov) =
let deps₂' , eqd' , certs' = castCERTS' deps₁ deps₂ deps₁' eqd certs
in deps₂' , eqd' , C.LEDGER-V⋯ refl utxo certs' u gov
castLEDGER deps₁ deps₂ deps₁' eqd (C.LEDGER-I⋯ refl utxo) = _ , eqd , C.LEDGER-I⋯ refl utxo

---------------------------------------------------------------------------
Expand Down
Loading
Loading