Remaining Shelley features/proofs

[williamdemeo]

This issue itemizes features and proofs that are missing (i.e., not yet formalized and/or described in the full cardano-ledger.pdf) from the Shelley era:

• [ ] CHAIN: incomplete (out of scope)

  • Dependencies:
    • PRTCL: missing - now part of Consensus
    • TICKN: missing - now part of Consensus
    • TICK: partially missing (not missing anymore since #869)
      • The NEWEPOCH logic is partially inlined in CHAIN (it has been moved to TICK)
      • CHAIN is missing the logic of RUPD (implemented in TICK since #869)
  • Functions:
    • chainChecks: missing - now part of Consensus
    • prtlSeqChecks: missing - now part of Consensus
    • adoptGenesisDelegs: missing - deprecated

• [x] BBODY: partially missing. Done in #884

  • LEDGERS: logic is inlined
  • CHAIN is missing preconditions:
    • bBodySize txs = hBbsize bhb
    • bbodyhash txs = bhash
  • CHAIN is missing the logic to update the block via incrBlocks

• [x] TICK: missing (5 days) Done in #869

  • Dependencies:
    • RUPD: missing
    • NEWEPOCH: partially inlined in CHAIN
  • Functions:
    • adoptGenesisDelegs: missing - deprecated

• [x] RUPD: missing (10 days) Done in #869

  • Dependencies:
  • Functions:
    • createRUpd: missing (#706)
    • monetary and treasury expansion parameters (#707)

• [x] NEWEPOCH: incomplete. Done in #854

  • Dependencies:
    • EPOCH:
    • MIR: missing - deprecated
  • Functions:
    • calculatePoolDistr: missing - used by Consensus (10 days)

• [x] EPOCH: incomplete. Done in #852

  • Dependencies:
    • SNAP:
    • POOLREAP:
      • Some of the POOLREAP logic (remove retired StakePools) is inlined in EPOCH
    • NEWPP: missing - deprecated
  • Functions:
    • votedValue: missing - deprecated (used by NEWPP)

• [x] POOLREAP: missing (15 days) (#719) Done in #852

  • Dependencies:
  • Functions
  • Notes: See issue #455 This is missing the logic to refund deposits

EDITED: Remove part that belongs to Consensus

[carlostome]

Moved the list to description.

[williamdemeo]

Here are some items not already covered by the lists above.

• [ ] Transitions from one era to the next.
  • [ ] Byron to Shelley (Fig 77 of shelley-ledger.pdf)
  • [ ] Shelley to Alonzo (Fig 16 of alonzo-ledger.pdf)
  • [ ] Alonzo to Babbage (not mentioned in babbage-ledger.pdf)
• [ ] ~DELPL: missing (Delegation and Pool Combined Environment)~ (deprecated)
• [ ] ~DELEGS: missing (Delegation sequence transition type)~

[HeinrichApfelmus]

DELPL: missing (Delegation and Pool Combined Environment)

It looks like this rule has already been incorporated: The new CERT rule (see Figure 46: CERTS rules) subsumes the old DELPL rule.

DELEGS: missing (Delegation sequence transition type)

It looks like this rule is to be replaced by the new CERTS rule (see Figure 46: CERTS rules). However, at the time of this comment, CERTS has not been added yet.

[williamdemeo]

Thanks @HeinrichApfelmus! You're right, DELPL is deprecated and DELEGS behavior is part of CERTS, so I've crossed those out.

Not sure what you mean by "CERTS has not been added yet." Agda code for the CERTS rule is here.

[HeinrichApfelmus]

Not sure what you mean by "CERTS has not been added yet." Agda code for the CERTS rule is here

Ah. What I meant was that the PDF rendering indicates that CERTS exists (Figure 32), but never gives a definition, e.g. Figure 35 "CERTS rules" doesn't mention it.

The Agda code for the CERTS uses ReflexiveTransitiveClosureᵇ', which saves space and potentially allows for proof reuse, but has the unfortunate side effect that it's harder to explain in the PDF. 🤔

[WhatisRT]

I think we do have an explanation of ReflexiveTransitiveClosure somewhere in the introduction, but the ᵇ' part doesn't help of course. Some cleanup might be necessary here.

[facundominguez]

I moved the BBODY item to the top level on recommendation by @WhatisRT. The other tasks in CHAIN are really out of scope apparently, except for TICK, which was already listed at the top level.