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]:

  cardano-ledger/libs/cardano-ledger-core/src/Cardano/Ledger/Plutus/ExUnits.hs

  Lines 193 to 209 in 156f568

  	instance DecCBOR ExUnits where
  	decCBOR = decode $ RecD ExUnits <! D decNat <! D decNat
  	where
  	decNat :: Decoder s Natural
  	decNat = do
  	x <- decCBOR
  	when
  	(x > fromIntegral (Prelude.maxBound :: Int64))
  	( cborError $
  	DecoderErrorCustom "ExUnits field" "values must not exceed maxBound :: Int64"
  	)
  	pure $ wordToNatural x
  	{-# INLINE decNat #-}
  	wordToNatural :: Word64 -> Natural
  	wordToNatural = fromIntegral
  	{-# INLINE wordToNatural #-}
  	{-# INLINE decCBOR #-}

• Pass curEpoch instead of slotNo to POOL env.

  Pass curEpochNo instead of curSlotNo to all the rules that don't need SlotNo #4692

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

  This is taken care of in Minor fixups from internal audit #4697

• Move committeeUpdateContainsColdCred to the let binding for consistency.

  Done in 50c9329

• 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: Make CertState into a type family #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

  Ensure that dRep ID exists prior to delegation #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 Stop reporting invalid refund when stake credential is not registered #4600 and Improve certificate performance #4643

• Spec has a problem with handling deposits

  This has been solved by creating alternative rules for conformance. Some of it is addressed in Remove the proposals workaround from UTXO conformance, add LEDGER conformance #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

  Replace UMap with a better tailored representation and name #4694

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

  Added a comment in Minor fixups from internal audit #4697

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

  Clarify which phase1 validation is skipped for isValid == False transactions #4695

• Add a special operator for x % 0 = 0

  Add %? operator #4696

• For PV10 cleanup dangling delegations for dreps unpon unregistration

  Taken care of in: Ensure dreps exist prior to delegation #4652

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

  Move ConwayTreasuryValueMismatch into UTXO rule #4691

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

  GovInfoEvent incorrectly reports removed as enacted #4602 and fixed in Fix enacted Set in GovInfoEvent #4604

• GovInfoEvent should report Map GovActionId Coin

  Taken care of in: Change GovInfoEvent's "unclaimed" field from Set to a Map #4623

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

  Taken care of in Minor fixups from internal audit #4697

[JaredCorduan]

💪