Admission is checked before touching either buffer. Source and destination
disjointness is a caller layout obligation, certified alongside application
and publication storage. Codes: 0 admitted, 4 refused; no durability claim.
80def telemetryHexCellAdmission =
81 (lambda unrestricted width : Nat .
82 (lambda unrestricted reverse : Nat .
83 (lambda unrestricted sourceExtent : Nat .
84 (lambda unrestricted destinationExtent : Nat .
85 (aosChoose
86 Nat
87 (naturalAnd
88 (naturalNonzero width)
89 (naturalAnd
90 (naturalLessOrEqual width telemetryHexSourceMaximumBytes)
91 (naturalAnd
92 (naturalLessOrEqual reverse 1)
93 (naturalAnd
94 (naturalLessOrEqual width sourceExtent)
95 (naturalLessOrEqual
96 width
97 (naturalDivideUnchecked (naturalSaturatingSubtract destinationExtent 2) 2))))))
98 0
99 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.