The choice payload is a single canonical word. Admission checks every
declared announcement binding before either participant artifact is emitted.
The decision word must be disjoint from frame storage: framing/hash work may
overwrite its scratch/header bytes while an authority is still forwarding.
The complete host arena and result-slot capacities remain outer admission facts.
109def nativeProtocolDecisionAdmitted =
110 (lambda erased decision : Type 0 .
111 (lambda erased payload : Type 0 .
112 (lambda unrestricted binding : (family NativeProtocolDecisionBinding decision payload) .
113 (lambda unrestricted owner : Nat .
114 (lambda unrestricted selector : decision .
115 (lambda unrestricted announcements : (family ProtocolAnnouncements payload) .
116 (let unrestricted state =
117 (nativeProtocolDecisionState decision payload binding selector)
118 in
119 (let unrestricted wordBytes =
120 (bytes-length (regionFrameWord 0))
121 in
122 (naturalAnd
123 (naturalLessOrEqual
124 state
125 (naturalSaturatingSubtract regionFrameWordLimit wordBytes))
126 (eliminate
127 ProtocolAnnouncements
128 (lambda unrestricted current : (family ProtocolAnnouncements payload) . Nat)
129 announcements
130 (branch ProtocolAnnouncementsEnd . 1)
131 (branch
132 ProtocolAnnouncementsNext
133 identity
134 value
135 rest
136 induction
137 .
138 (let unrestricted frame =
139 (nativeProtocolDecisionFrame decision payload binding value)
140 in
141 (naturalAnd
142 (nativeProtocolFrameAdmitted identity frame)
143 (naturalAnd
144 (naturalEqual (framePayloadBytes frame) wordBytes)
145 (naturalAnd
146 (naturalOr
147 (naturalLessOrEqual
148 (naturalAdd state wordBytes)
149 (frameBase frame))
150 (naturalLessOrEqual (frameEnd frame) state))
151 (naturalAnd induction 1))))))))))))))))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.