Canonical zero padding is part of version one's envelope, not an extension
area whose arbitrary bytes may survive integrity checks unnoticed.
608def nativeCheckpointRequirePadding =
609 (lambda unrestricted layout : (family NativeCheckpointLayout) .
610 (lambda unrestricted slot : Nat .
611 (lambda unrestricted tail : (family NativePhysicalCommands) .
612 (let unrestricted start =
613 (naturalAdd
614 checkpointEnvelopeDigestsAt
615 (naturalMultiply
616 checkpointEnvelopeDigestBytes
617 (checkpointEnvelopeChunkCount (nativeCheckpointContract layout))))
618 in
619 (nativeMemoryCompareRegions
620 (naturalAdd (nativeCheckpointBase layout) start)
621 (naturalAdd (nativeCheckpointMetadataAt layout) start)
622 (naturalSaturatingSubtract (nativeCheckpointHeaderBytes layout) start)
623 slot
624 b"checkpoint-padding"
625 tail)))))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.