Prove an equivalence between the two ledgers

[WhatisRT]

We have two models right now, one under Ledger and one under Ledger.Conway.Conformance. They differ by some logic being moved from CERTS into UTXO but are otherwise identical. This means that there should be a theorem of the form

Γ L.⊢ s ⇀⦇ tx ,LEDGER⦈ s' ⇔ Γ C.⊢ s ⇀⦇ tx ,LEDGER⦈ s'

except that we need to translate some of the types being involved (otherwise this won't type check). In the end, we need to prove this for CHAIN, but that should be trivial once we have it for LEDGER.

Our current strategy for maintenance is based on this being proven, otherwise these could drift out of sync. So the sooner this is done the better.

See also #512, which will actually make this provable once finished and #525.

Blocked by #512 and it would be a good idea to do #582 first.

[UlfNorell]

Is there a precise(ish) description of what the difference should be? I'm expecting there will be some places where Ledger has moved since Conformance was forked where the correct thing is to just update Conformance to match.

[WhatisRT]

If I'm not forgetting anything, the only actual difference should be in how the deposits are handled. Any other difference is probably unintentional drift between the two implementations.

I think you're right, it's probably more likely that in that case Conformance needs an update. I think in that case it'd be best to make a small separate PR just for that update so that the PR for this issue includes no logic changes after everything is rebased. That way the question 'which one is correct' becomes disentangled from this work.

[UlfNorell]

Getting deeper into the proof, I'm getting confused about how the conformance rules are supposed to work (and consequently what the precise equivalence statement should be).

In particular, in the Conformance rules, there are three separate Deposits in LState: two in CertState (in DState and GState) and one in UTxOState. The ones in CertState are updated independently in DELEG and GOVCERT respectively:

formal-ledger-specifications/src/Ledger/Conway/Conformance/Certs.agda

Lines 103 to 114 in d61bd38

	data _⊢_⇀⦇_,DELEG⦈_ where
	DELEG-delegate : let open PParams pp in
	∙ (c ∉ dom rwds → d ≡ keyDeposit)
	∙ (c ∈ dom rwds → d ≡ 0)
	∙ mv ∈ mapˢ (just ∘ credVoter DRep) delegatees ∪ ❴ nothing ❵
	∙ mkh ∈ mapˢ just (dom pools) ∪ ❴ nothing ❵
	────────────────────────────────
	⟦ pp , pools , delegatees ⟧ᵈᵉ ⊢
	⟦ vDelegs , sDelegs , rwds , dep ⟧ᵈ
	⇀⦇ delegate c mv mkh d ,DELEG⦈
	⟦ insertIfJust c mv vDelegs , insertIfJust c mkh sDelegs , rwds ∪ˡ ❴ c , 0 ❵
	, updateCertDeposit pp (delegate c mv mkh d) dep ⟧ᵈ

formal-ledger-specifications/src/Ledger/Conway/Conformance/Certs.agda

Lines 127 to 135 in d61bd38

	data _⊢_⇀⦇_,GOVCERT⦈_ : GovCertEnv → GState → DCert → GState → Type where
	GOVCERT-regdrep : ∀ {pp} → let open PParams pp in
	∙ (d ≡ drepDeposit × c ∉ dom dReps) ⊎ (d ≡ 0 × c ∈ dom dReps)
	────────────────────────────────
	⟦ e , pp , vs , wdrls ⟧ᶜ ⊢
	⟦ dReps , ccKeys , dep ⟧ᵛ
	⇀⦇ regdrep c d an ,GOVCERT⦈
	⟦ ❴ c , e + drepActivity ❵ ∪ˡ dReps , ccKeys
	, updateCertDeposit pp (regdrep c d an ) dep ⟧ᵛ

and never synced up

formal-ledger-specifications/src/Ledger/Conway/Conformance/Certs.agda

Lines 151 to 165 in d61bd38

	data _⊢_⇀⦇_,CERT⦈_ : CertEnv → CertState → DCert → CertState → Type where
	CERT-deleg :
	∙ ⟦ pp , PState.pools stᵖ , dom (GState.dreps stᵍ) ⟧ᵈᵉ ⊢ stᵈ ⇀⦇ dCert ,DELEG⦈ stᵈ'
	────────────────────────────────
	⟦ e , pp , vs , wdrls ⟧ᶜ ⊢ ⟦ stᵈ , stᵖ , stᵍ ⟧ᶜˢ ⇀⦇ dCert ,CERT⦈ ⟦ stᵈ' , stᵖ , stᵍ ⟧ᶜˢ
	CERT-pool :
	∙ pp ⊢ stᵖ ⇀⦇ dCert ,POOL⦈ stᵖ'
	────────────────────────────────
	⟦ e , pp , vs , wdrls ⟧ᶜ ⊢ ⟦ stᵈ , stᵖ , stᵍ ⟧ᶜˢ ⇀⦇ dCert ,CERT⦈ ⟦ stᵈ , stᵖ' , stᵍ ⟧ᶜˢ
	CERT-vdel :
	∙ Γ ⊢ stᵍ ⇀⦇ dCert ,GOVCERT⦈ stᵍ'
	────────────────────────────────
	Γ ⊢ ⟦ stᵈ , stᵖ , stᵍ ⟧ᶜˢ ⇀⦇ dCert ,CERT⦈ ⟦ stᵈ , stᵖ , stᵍ' ⟧ᶜˢ

The deposits in UTxOState are unaffected by the UTXOW/UTXO/UTXOS rules

formal-ledger-specifications/src/Ledger/Conway/Conformance/Utxo.agda

Lines 127 to 142 in d61bd38

	data _⊢_⇀⦇_,UTXOS⦈_ : UTxOEnv → UTxOState → Tx → UTxOState → Type where
	Scripts-Yes :
	∀ {Γ} {s} {tx}
	→ let open Tx tx renaming (body to txb); open TxBody txb
	open UTxOEnv Γ renaming (pparams to pp)
	open UTxOState s
	sLst = collectPhaseTwoScriptInputs pp tx utxo
	in
	∙ evalScripts tx sLst ≡ isValid
	∙ isValid ≡ true
	────────────────────────────────
	Γ ⊢ s ⇀⦇ tx ,UTXOS⦈ ⟦ (utxo ∣ txins ᶜ) ∪ˡ (outs txb)
	, fees + txfee
	, deposits
	, donations + txdonation
	⟧ᵘ

and updated after the fact in the LEDGER rule, without looking at the deposits in CertState:

formal-ledger-specifications/src/Ledger/Conway/Conformance/Ledger.agda

Lines 75 to 88 in d61bd38

	_⊢_⇀⦇_,LEDGER⦈_ : LEnv → LState → Tx → LState → Type
	where
	LEDGER-V :
	let open LState s; txb = tx .body; open TxBody txb; open LEnv Γ
	utxoSt'' = record utxoSt' { deposits = updateDeposits pparams txb (deposits utxoSt') }
	in
	∙ isValid tx ≡ true
	∙ record { LEnv Γ } ⊢ utxoSt ⇀⦇ tx ,UTXOW⦈ utxoSt'
	∙ ⟦ epoch slot , pparams , txvote , txwdrls ⟧ᶜ ⊢ certState ⇀⦇ txcerts ,CERTS⦈ certState'
	∙ ⟦ txid , epoch slot , pparams , ppolicy , enactState , certState' ⟧ᵍ ⊢ govSt |ᵒ certState' ⇀⦇ txgov txb ,GOV⦈ govSt'
	────────────────────────────────
	Γ ⊢ s ⇀⦇ tx ,LEDGER⦈ ⟦ utxoSt'' , govSt' , certState' ⟧ˡ

I think I can prove that the deposits in the UTxOState line up between Ledger and Conformance, and that when you construct a Conformance rule from a Ledger rule the deposits in CertState contains the deposits relevant to the particular rule (DELEG or GOVCERT), but it's not obvious what the precise relation is.

@WhatisRT @Soupstraw your input here would be welcome.

[WhatisRT]

Ah, it seems this is a bit of a mess. First, the preferred semantics of the deposits is that the union of all three deposit pots on the Conformance side equals the deposit pot on the Ledger side. They are split by DepositPurpose:

• all CredentialDeposits are in DState
• all DRepDeposits are in GState
• the other two are in UTxOState

However, it turns out that this split doesn't actually work! To compute things properly, UTxOState actually needs to contain all the deposits (technically Scripts-Yes just needs read access, so it could be provided via UTxOEnv, but that seems even more messy). This is why we have utxoSt'' in LEDGER-V: it updates all the deposits. I don't remember right now why this isn't in Scripts-Yes. Maybe it could be, in which case that'd probably be cleaner and the equivalence statement for UTXO would be nicer.

This data duplication also makes things a bit more annoying, since there is now an extra invariant that I don't know how to fit in the picture. Specifically, both deposits in CertState should be a subset of the one in UTxOState. So now, arguably the translation from a Conformance LState that doesn't satisfy this invariant should fail. I don't know if we want to represent this or not. It also means that to convert a Ledger CertState into a Conformance one, you also need to supply the deposits.

For UTXO equivalence, there are three cases:

• valid transaction => both final states should be equal (up to the utxoSt'' thing mentioned above)
• transaction has invalid certificates => Ledger fails, Conformance succeeds (but Conformance CERTS fails)
• otherwise invalid transaction => both fail

CERTS equivalence is analogous, and then the two failures of the 'transaction has invalid certificates' cases lead to a failure of LEDGER either way.

I hope this helps!