A supplied binding is three binary roles, already loaded into the identity
arena. Epoch initialization retains those bytes and acquires only the last
role. Admission proves the count/shape decision, not coordinator authority
or entropy provenance. The native initializer validates the binding before
asking the kernel for entropy and validates all four roles afterwards.
79def telemetryEpochAdmission =
80 (lambda unrestricted version : Nat .
81 (lambda unrestricted extent : Nat .
82 (lambda unrestricted received : Nat .
83 (lambda unrestricted valid : Nat .
84 (aosChoose
85 Nat
86 (naturalAnd (naturalEqual version 1) (naturalLessOrEqual valid 1))
87 (aosChoose
88 Nat
89 (naturalLessOrEqual telemetryIdentitySetBytes extent)
90 (aosChoose
91 Nat
92 (naturalEqual received telemetryIdentityBytes)
93 (aosChoose Nat valid 0 3)
94 2)
95 1)
96 4)))))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.