The final digest covers only bytes present in the payload. The generic
byte-prefix operation zero-pads, so passing the full chunk extent for the
tail would disagree with native file hashing while still passing a codec
round trip that made the same mistake on both sides.
132def checkpointEnvelopeChunkExtent =
133 (lambda unrestricted contract : (family CheckpointEnvelopeContract) .
134 (lambda unrestricted index : Nat .
135 (naturalSelect (naturalLess index (checkpointEnvelopeFullChunks contract))
136 (checkpointEnvelopeContractChunk contract)
137 (naturalSelect (naturalEqual index (checkpointEnvelopeFullChunks contract))
138 (checkpointEnvelopeTailBytes contract) 0))))The compiler supplied declaration spans and resolved links from this source snapshot. This page does not assert that this file belongs to a checked closure.