search

IntersectMBO / formal-ledger-specifications

Formal specifications of the cardano ledger
Apache License 2.0
38 stars 13 forks source link

Prove an equivalence between the two ledgers #585

Open WhatisRT opened 1 month ago

WhatisRT commented 1 month ago

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 commented 1 month ago

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 commented 1 month ago

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 commented 2 weeks ago

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:

https://github.com/IntersectMBO/formal-ledger-specifications/blob/d61bd383e54c7927798b6d2f7dcd946c0ac79384/src/Ledger/Conway/Conformance/Certs.agda#L103-L114

https://github.com/IntersectMBO/formal-ledger-specifications/blob/d61bd383e54c7927798b6d2f7dcd946c0ac79384/src/Ledger/Conway/Conformance/Certs.agda#L127-L135

and never synced up

https://github.com/IntersectMBO/formal-ledger-specifications/blob/d61bd383e54c7927798b6d2f7dcd946c0ac79384/src/Ledger/Conway/Conformance/Certs.agda#L151-L165

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

https://github.com/IntersectMBO/formal-ledger-specifications/blob/d61bd383e54c7927798b6d2f7dcd946c0ac79384/src/Ledger/Conway/Conformance/Utxo.agda#L127-L142

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

https://github.com/IntersectMBO/formal-ledger-specifications/blob/d61bd383e54c7927798b6d2f7dcd946c0ac79384/src/Ledger/Conway/Conformance/Ledger.agda#L75-L88

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 commented 2 weeks ago

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:

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:

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!