Repository navigation
[FEAT] - Adapt the formal spec to include Linear Leios - #2278
javierdiaz72 wants to merge 9 commits into
Conversation
javierdiaz72
added
enhancement
Add two header-level checks to CHAINHEAD, derived from the certificate inclusion rules of CIP-164: a header may only set certifiedEB if the last applied block announced an endorser block, and if at least 3*leiosHeaderPeriod + leiosVotingPeriod + leiosDiffusionPeriod has elapsed since that block. The certifying header does not repeat the hash of the endorser block it certifies, so LastAppliedBlock gains an aeb field recording what the last block announced. The three Leios periods are protocol parameters on PParams, read through getPParams as maxHeaderSize already is, and named after their counterparts in the ledger specification. They are wall-clock durations rather than slot counts: constants in slots could be changed neither by governance nor by a change of slot length. Milliseconds accordingly joins Coin in Ledger.Prelude.Base, matching where the ledger specification defines it. Comparing a duration against two slots needs a way to place a slot in time, so EpochStructure gains slotToTime. Expressing the check as slotToTime sℓ + certificationDelay ps ≤ slotToTime s rather than converting the delay into a slot count keeps certificationDelay in the units CIP-164 states it in, and leaves the rounding implicit in the arithmetic instead of fixing a rounding policy the CIP does not specify. A function rather than a slot-length constant, so that an instantiation with era-varying slot lengths remains expressible. Note that the announced endorser block size is deliberately left unchecked: per CIP-164 an incorrect size invalidates neither the header nor the block, and only costs the producer the votes of honest nodes. Split the Chain Head types figure in two, as it no longer fits on a page, and give LastAppliedBlock and ChainHeadState separate AgdaSuppressSpace blocks: sharing one made Agda emit an alignment preamble anchored past the column of the ChainHeadState declaration, which LaTeX rejects. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
05383aa to
27e269a
Compare
The ledger specification's Leios design note settles how the summed periods become a slot bound (docs/leios/design-note.md, "Alignment with the consensus specification", item 2): CIP-164 converts them with the genesis slotLength, rounded up, and both specifications are to share one definition of the conversion and agree on the boundary sℓ + certificationDelay ≤ s. So SlotLengthᶜ, nonzero, joins GlobalConstants, and durationToSlots sits beside Milliseconds in Ledger.Prelude.Base. It takes the slot length as an argument rather than naming SlotLengthᶜ, because the note has the conversion travelling with Milliseconds and the constant travelling with the epoch structure when both move to the common library; naming the constant would fuse the two units. This replaces the slotToTime formulation, which compared wall-clock times instead of converting. That agreed with this one at every boundary, but it was a second shape for a quantity the two specifications are meant to share, which is what the note exists to prevent. EpochStructure keeps a field for the conversion, as Slot is abstract and only the structure can present durationToSlots' result as one. The ledger specification's Slot is abstract in the same way, so its certificationDelay will need the same; if it lands a different shape, this should follow. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
williamdemeo
left a comment
williamdemeo
left a comment
There was a problem hiding this comment.
Nice work @javierdiaz72! I approve with a few suggestions for you to consider.
| and rounding up. Because a header | ||
| that sets \afld{certifiedEB} obliges the corresponding body to carry a matching | ||
| certificate, this constraint can be checked on the header alone --- exactly the kind |
There was a problem hiding this comment.
This argument holds because of two things the ledger's block rule enforces and the header validator cannot see: that certifiedEB equals the presence of the certificate in the body (in both directions, otherwise a false bit skips this check while a certificate rides in the body), and that the body-side certificate check applies the same delay. Could the prose state these as obligations on the block rule rather than as a fact about headers? Both are being written into the ledger spec's block and chain rules now.
| bhTooEarly = bh { bhBody = certifyingBhbAt 2 } | ||
|
|
||
| -- Certifies at slot 10, comfortably past the delay. | ||
| bhInTime :: BHeader | ||
| bhInTime = bh { bhBody = certifyingBhbAt 10 } |
There was a problem hiding this comment.
The cases certify at slot 2 and slot 10 against a delay of exactly 8 slots, so the boundary is not exercised (slot 8 is the earliest permitted, slot 7 the latest rejected), and because 8000 ms is a multiple of the 1000 ms slot a conversion that rounded down would pass unchanged. Suggestion: set leiosDiffusionPeriod = 3500 in the fixture (delay ⌈8500/1000⌉ = 9) and add the two cases below; I ran them against this head and both pass.
bhOneShort, bhAtBoundary :: BHeader
bhOneShort = bh { bhBody = certifyingBhbAt 8 }
bhAtBoundary = bh { bhBody = certifyingBhbAt 9 }
chsAtBoundary :: ChainHeadState
chsAtBoundary = chs' { chsLab = Just lab' { labSℓ = 9 } }
it "chainheadStep rejects a header certifying one slot short of the delay" $
isFailure (chainheadStep dummyExternalFunctions che chs bhOneShort) @?= True
it "chainheadStep accepts a header certifying exactly at the delay" $
chainheadStep dummyExternalFunctions che chs bhAtBoundary @?= Success chsAtBoundary| -- The number of slots spanning a wall-clock duration, rounded up. Used | ||
| -- to interpret the Leios timing protocol parameters, which CIP-164 | ||
| -- specifies as durations rather than as slot counts. A field because | ||
| -- Slot is abstract here: `durationToSlots` yields a number, which only | ||
| -- the structure can present as a Slot. | ||
| slotsFromDuration : Milliseconds → Slot |
There was a problem hiding this comment.
As a field, any EpochStructure may implement this arbitrarily; only ℕEpochStructure rounds up, and the rounding is what the CIP's security argument relies on. A SlotLength : Milliseconds field with slotsFromDuration derived from it would make the law hold for every instance, and the shared quantity in the ledger alignment table would be the constant rather than the function. (This is just a suggestion/preference since the record already has unconstrained fields.)
| leiosPeriods pp = leiosHeaderPeriod , leiosVotingPeriod , leiosDiffusionPeriod | ||
| where open PParams pp | ||
|
|
||
| certificationDelay : LeiosPeriods → Slot |
There was a problem hiding this comment.
Consider certificationDelay : PParams → Slot, since the ledger spec will define certificationDelay over its PParams, and identical signatures keep the correspondence between the two specs trivial.
| \item The operational certificate issue number map \afld{cs}. | ||
| \item The epoch nonce \afld{η₀}. | ||
| \item The evolving nonce \afld{ηv}. | ||
| \item The candidate nonce \afld{ηc}. | ||
| \item The previous epoch hash nonce \afld{ηh}. | ||
| \item The last header hash \afld{h}. | ||
| \item The last slot \afld{sℓ}. | ||
| \item The last block number \afld{bℓ}. |
There was a problem hiding this comment.
Consider adding the endorser block announced by the last applied block to the list.
|
A status note from the ledger side. The ledger specification's chain rule (fls#1346) now reads the delay's parameters at the certifying block, as Since this PR's last commit, @javierdiaz72 do you plan to refresh this PR against |
I was confused about this PR, I thought I had already merged it. So, I will take the opportunity to address your review comments and refresh the PR against |
The dummy periods summed to 8000ms against a slot length of 1000ms, so the delay was a whole number of slots and rounding down would have given the same answer; the cases also certified at slots 2 and 10 against a delay of 8, leaving the boundary untested. leiosDiffusionPeriod becomes 3500ms, so the delay is ⌈8500/1000⌉ = 9 where rounding down would give 8, and two cases pin the boundary: slot 8 is rejected, slot 9 accepted. Replacing the ceiling with a floor now fails the first of those and nothing else. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
slotsFromDuration was a field, so only ℕEpochStructure rounded up and any other instance could shorten the delay, or ignore the duration entirely, without the specification noticing. The rounding is what CIP-164's Step 5 specifies and what its security argument depends on. EpochStructure now takes the genesis SlotLength as a constant and derives slotsFromDuration from it, so the rounding holds by construction. ℕtoSlot injects the resulting count into the slot semiring, as ℕtoEpoch already does for epochs; this relies on 1# denoting one slot, which addSlot and firstSlot assume too. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
The header's certifiedEB bit obliging the body to carry a matching certificate is enforced by the ledger, not here, so do not present it as a header-only check.
The ledger specification will define certificationDelay over its own PParams, so matching the signature keeps the correspondence between the two specifications a matter of reading, not translation. This also removes LeiosPeriods and the leiosPeriods accessor. The accessor existed only because spelling the three fields out at the call site overran the width of the figure, and passing the whole record is narrower than either form. What it costs is that the type of certChecks no longer records that it reads just three of the parameters. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
The subsection enumerates what the chain head state consists of, and adding the aeb field to LastAppliedBlock left that list describing a state one component smaller than the figure beside it shows. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
This branch has not been deployed
2 participants
This PR solves #2273.