Version two carries the existing eight control words. A changed control
shape requires its own admitted encoding, never silent field omission.
424def publicationArenaCertificate =
425 (lambda unrestricted applicationBytes : Nat .
426 (lambda unrestricted ordinaryCapacity : Nat .
427 (lambda unrestricted reservedCapacity : Nat .
428 (naturalAnd
429 (naturalEqual
430 captureControlBytes
431 (bytes-length (nativeTelemetryEncodeCounters publicationEmptyCounters)))
432 (publicationStorageCertificate applicationBytes ordinaryCapacity reservedCapacity)))))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.