236def planRegionFrameLayout =
237 (lambda unrestricted identity : (family RegionTransferIdentity) .
238 (lambda unrestricted payloadBytes : Nat .
239 (lambda unrestricted headerBudget : Nat .
240 (lambda unrestricted base : Nat .
241 (lambda unrestricted available : Nat .
242 (eliminate
243 StdResult
244 (lambda unrestricted current : (family StdResult (family RegionFrameFailure) Bytes) .
245 (family StdResult (family RegionFrameLayoutFailure) (family RegionFrameLayout)))
246 (regionFrameHeader identity payloadBytes headerBudget)
247 (branch
248 StdFailure
249 code
250 .
251 (constructor
252 StdResult
253 StdFailure
254 (family RegionFrameLayoutFailure)
255 (family RegionFrameLayout)
256 (constructor RegionFrameLayoutFailure RegionFrameLayoutHeaderRejected)))
257 (branch
258 StdSuccess
259 header
260 .
261 (nat-eliminate
262 (lambda unrestricted valid : Nat .
263 (family StdResult (family RegionFrameLayoutFailure) (family RegionFrameLayout)))
264 (constructor
265 StdResult
266 StdFailure
267 (family RegionFrameLayoutFailure)
268 (family RegionFrameLayout)
269 (constructor RegionFrameLayoutFailure RegionFrameLayoutBoundsRejected))
270 (lambda unrestricted previous : Nat .
271 (lambda unrestricted ignored : (family StdResult (family RegionFrameLayoutFailure) (family RegionFrameLayout)) .
272 (eliminate
273 StdResult
274 (lambda unrestricted current : (family StdResult (family SHA256ErrorCode) Bytes) .
275 (family
276 StdResult
277 (family RegionFrameLayoutFailure)
278 (family RegionFrameLayout)))
279 (sha256PaddingSuffix (naturalAdd (bytes-length header) payloadBytes))
280 (branch
281 StdFailure
282 code
283 .
284 (constructor
285 StdResult
286 StdFailure
287 (family RegionFrameLayoutFailure)
288 (family RegionFrameLayout)
289 (constructor RegionFrameLayoutFailure RegionFrameLayoutPaddingRejected)))
290 (branch
291 StdSuccess
292 padding
293 .
294 (let unrestricted layout : (family RegionFrameLayout) =
295 (constructor
296 RegionFrameLayout
297 RegionFrameLayoutOf
298 header
299 payloadBytes
300 base
301 padding)
302 in
303 (nat-eliminate
304 (lambda unrestricted fits : Nat .
305 (family
306 StdResult
307 (family RegionFrameLayoutFailure)
308 (family RegionFrameLayout)))
309 (constructor
310 StdResult
311 StdFailure
312 (family RegionFrameLayoutFailure)
313 (family RegionFrameLayout)
314 (constructor
315 RegionFrameLayoutFailure
316 RegionFrameLayoutBoundsRejected))
317 (lambda unrestricted previous : Nat .
318 (lambda unrestricted ignored : (family StdResult (family RegionFrameLayoutFailure) (family RegionFrameLayout)) .
319 (constructor
320 StdResult
321 StdSuccess
322 (family RegionFrameLayoutFailure)
323 (family RegionFrameLayout)
324 layout)))
325 (frameLayoutFits available layout)))))))
326 (naturalAnd
327 (naturalLessOrEqual
328 (bytes-length header)
329 (modelWord64Natural sha256MaximumInputBytes))
330 (naturalLessOrEqual
331 payloadBytes
332 (naturalSaturatingSubtract
333 (modelWord64Natural sha256MaximumInputBytes)
334 (bytes-length header))))))))))))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.