Audit/Compare the Conway spec to the implementation

[JaredCorduan]

Audit that the conway formal spec matches the implementation. (it would be better to have conformance tests against an executable model , but the new agda model will probably not be fully executable in time.)

---

Blocks branch

Level 1

• [ ] DELEG
• [ ] GOVCERT
• [ ] POOL

Level 2

• [ ] CERT
• [ ] CERTS
• [ ] GOV

Level 3

• [ ] UTXOS
• [ ] UTXO (babbage)
• [ ] UTXOW (babbage)

Level 4

• [ ] LEDGER

Ticks branch

Level 1

• [ ] ENACT
• [ ] POOLREAP (shelley)
• [ ] SNAP (shelley)

Level 2

• [ ] RATIFY

Level 3

• [ ] EPOCH

Level 4

• [ ] NEWEPOCH

[ltouro]

There is a link to conway formal spec?

[JaredCorduan]

There is a link to conway formal spec?

great question, there's not yet, unfortunately. CIP-1694 is the closest thing that we have so far. See this section for a loose understanding of what is in scope for conway.

Our goal for conway is to do something new and exciting with the spec: use the Agda model to produce a PDF with the relevant changes. When it is ready, I will add a link to it at the top of the table in the main README of this repo.

[lehins]

There is a link to conway formal spec?

Yes, the full spec is implemented in Agda: https://github.com/IntersectMBO/formal-ledger-specifications

There are links in the readme to PDF version as well.

[lehins]

My notes that came out of the audit with @WhatisRT and the final outcomes:

• ExUnits do not have an upper bound. Enforce to maxBound :: Word64 with well formed check on the intra-era hardfork.

  After further inspection this note turns out to be incorrect, since despite us using Natural for ExUnits we have always protected it at the deserialization level to be in the range [0, maxBound :: Int64]: https://github.com/IntersectMBO/cardano-ledger/blob/156f568d16a0a93f872438b519247b913584178f/libs/cardano-ledger-core/src/Cardano/Ledger/Plutus/ExUnits.hs#L193-L209

• Pass curEpoch instead of slotNo to POOL env.

  https://github.com/IntersectMBO/cardano-ledger/issues/4692

• Add comment that VState is GState in spec and/or implementation

  This is taken care of in https://github.com/IntersectMBO/cardano-ledger/pull/4697

• Move committeeUpdateContainsColdCred to the let binding for consistency.

  Done in https://github.com/IntersectMBO/cardano-ledger/commit/50c9329ee4bc087a4d735d39c7362ed9a8386346

• Remove GenDelegs and Irewards during translation to Conway

  Instead of clearing them out of the state we have a plan on making the CertState into a type family and using correct per era definitions: https://github.com/IntersectMBO/cardano-ledger/issues/4693

• For intra era HF prevent delegation to non-existent DRep and cleanup on DRep unreg. For next era remove non-existent delegations during translation

  https://github.com/IntersectMBO/cardano-ledger/issues/4598 We were able to cleanup the non-existent delegations for the intra-era HF as well.

• Avoid multiple lookups of stake credential in UMap for all checks

  Taken care of in #4600 and #4643

• Spec has a problem with handling deposits

  This has been solved by creating alternative rules for conformance. Some of it is addressed in https://github.com/IntersectMBO/cardano-ledger/pull/4665 on the ledger side but more work is underway on the spec side as well.

• unionR, (⨃) Fix deposit being ignored. This will affect drainWithdrawals

  https://github.com/IntersectMBO/cardano-ledger/issues/4694

• Allowing MutliAsset in collateral was done to allow wallets to pick inputs easier.

  Added a comment in https://github.com/IntersectMBO/cardano-ledger/pull/4697

• Figure out a consistent story about Tx for phase2: what should be validated what should not.

  https://github.com/IntersectMBO/cardano-ledger/issues/4695

• Add a special operator for x % 0 = 0

  https://github.com/IntersectMBO/cardano-ledger/issues/4696

• For PV10 cleanup dangling delegations for dreps unpon unregistration

  Taken care of in: https://github.com/IntersectMBO/cardano-ledger/pull/4652

• ConwayTreasuryValueMismatch is checked in LEDGER instead of UTXO. Also it is only checked for valid transactions.

  https://github.com/IntersectMBO/cardano-ledger/issues/4691

• Bug: GovInfoEvent reports also siblings that have been removed due to enactment, like if they were enacted.

  https://github.com/IntersectMBO/cardano-ledger/issues/4602 and fixed in https://github.com/IntersectMBO/cardano-ledger/pull/4604

• GovInfoEvent should report Map GovActionId Coin

  Taken care of in: https://github.com/IntersectMBO/cardano-ledger/pull/4623

• | otherwise = (um, Map.insertWith (<>) (gasId gas) (gasDeposit gas) unclaimed) - replace insertWith with insert

  Taken care of in https://github.com/IntersectMBO/cardano-ledger/pull/4697

[JaredCorduan]

:muscle: