169def checkGlobalProtocol =
170 (lambda erased operation : Type 0 .
171 (lambda erased payload : Type 0 .
172 (lambda erased decision : Type 0 .
173 (lambda unrestricted participants : Nat .
174 (lambda unrestricted local : (pi unrestricted owner : Nat . (pi unrestricted value : operation . Nat)) .
175 (lambda unrestricted transfer : (pi unrestricted identity : (family RegionTransferIdentity) . (pi unrestricted value : payload . Nat)) .
176 (lambda unrestricted choice : (pi unrestricted owner : Nat . (pi unrestricted selector : decision . (pi unrestricted announcements : (family ProtocolAnnouncements payload) . Nat))) .
177 (lambda unrestricted program : (family GlobalProtocol operation payload decision) .
178 (protocolRequire
179 (naturalAnd
180 (naturalNonzero participants)
181 (naturalLessOrEqual participants regionFrameWordLimit))
182 (constructor ProtocolFailure ProtocolMembershipBounds)
183 (eliminate
184 GlobalProtocol
185 (lambda unrestricted current : (family GlobalProtocol operation payload decision) .
186 (family StdResult (family ProtocolFailure) Nat))
187 program
188 (branch GlobalProtocolEnd . protocolAccepted)
189 (branch
190 GlobalProtocolLocal
191 participant
192 value
193 rest
194 induction
195 .
196 (protocolRequire
197 (naturalLess participant participants)
198 (constructor ProtocolFailure ProtocolParticipantBounds)
199 (protocolRequire
200 (local participant value)
201 (constructor ProtocolFailure ProtocolLocalUnavailable)
202 induction)))
203 (branch
204 GlobalProtocolTransfer
205 identity
206 value
207 rest
208 induction
209 .
210 (protocolRequire
211 (naturalLess (regionTransferSender identity) participants)
212 (constructor ProtocolFailure ProtocolSenderBounds)
213 (protocolRequire
214 (naturalLess (regionTransferReceiver identity) participants)
215 (constructor ProtocolFailure ProtocolReceiverBounds)
216 (protocolRequire
217 (naturalEqual
218 (naturalEqual
219 (regionTransferSender identity)
220 (regionTransferReceiver identity))
221 0)
222 (constructor ProtocolFailure ProtocolSelfTransfer)
223 (protocolRequire
224 (transfer identity value)
225 (constructor ProtocolFailure ProtocolTransferUnavailable)
226 induction)))))
227 (branch
228 GlobalProtocolRepeat
229 count
230 body
231 rest
232 bodyCheck
233 restCheck
234 .
235 (protocolRequire
236 (naturalLessOrEqual count regionFrameWordLimit)
237 (constructor ProtocolFailure ProtocolRepeatBounds)
238 (protocolCheckThen
239 bodyCheck
240 (protocolCheckThen restCheck protocolAccepted))))
241 (branch
242 GlobalProtocolChoice
243 identity
244 selector
245 announcements
246 zeroBody
247 oneBody
248 rest
249 zeroCheck
250 oneCheck
251 restCheck
252 .
253 (protocolRequire
254 (naturalAnd
255 (naturalLess (regionTransferSender identity) participants)
256 (naturalEqual
257 (regionTransferSender identity)
258 (regionTransferReceiver identity)))
259 (constructor ProtocolFailure ProtocolChoiceAuthority)
260 (protocolRequire
261 (protocolAnnouncementsAdmitted
262 payload
263 participants
264 identity
265 transfer
266 announcements)
267 (constructor ProtocolFailure ProtocolChoiceRoutes)
268 (protocolRequire
269 (naturalAnd
270 (globalProtocolCovered
271 operation
272 payload
273 decision
274 (protocolInformed payload identity announcements)
275 zeroBody)
276 (globalProtocolCovered
277 operation
278 payload
279 decision
280 (protocolInformed payload identity announcements)
281 oneBody))
282 (constructor ProtocolFailure ProtocolChoiceUninformed)
283 (protocolRequire
284 (choice (regionTransferSender identity) selector announcements)
285 (constructor ProtocolFailure ProtocolChoiceUnavailable)
286 (protocolCheckThen
287 zeroCheck
288 (protocolCheckThen
289 oneCheck
290 (protocolCheckThen restCheck protocolAccepted))))))))))))))))))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.