261def planNativeCheckpointNonempty =
262 (lambda unrestricted contract : (family CheckpointEnvelopeContract) .
263 (lambda unrestricted base : Nat .
264 (lambda unrestricted updates : Nat .
265 (lambda unrestricted invocations : Nat .
266 (lambda unrestricted available : Nat .
267 (nat-eliminate
268 (lambda unrestricted admitted : Nat .
269 (family StdResult (family NativeCheckpointFailure) (family NativeCheckpointLayout)))
270 (constructor
271 StdResult
272 StdFailure
273 (family NativeCheckpointFailure)
274 (family NativeCheckpointLayout)
275 (constructor NativeCheckpointFailure NativeCheckpointBounds))
276 (lambda unrestricted previous : Nat .
277 (lambda unrestricted ignored : (family StdResult (family NativeCheckpointFailure) (family NativeCheckpointLayout)) .
278 (eliminate
279 StdResult
280 (lambda unrestricted r : (family StdResult (family SHA256ErrorCode) Bytes) .
281 (family
282 StdResult
283 (family NativeCheckpointFailure)
284 (family NativeCheckpointLayout)))
285 (sha256PaddingSuffix (checkpointEnvelopeContractChunk contract))
286 (branch
287 StdFailure
288 error
289 .
290 (constructor
291 StdResult
292 StdFailure
293 (family NativeCheckpointFailure)
294 (family NativeCheckpointLayout)
295 (constructor NativeCheckpointFailure NativeCheckpointBounds)))
296 (branch
297 StdSuccess
298 fullPadding
299 .
300 (eliminate
301 StdResult
302 (lambda unrestricted r : (family StdResult (family SHA256ErrorCode) Bytes) .
303 (family
304 StdResult
305 (family NativeCheckpointFailure)
306 (family NativeCheckpointLayout)))
307 (sha256PaddingSuffix (checkpointEnvelopeTailBytes contract))
308 (branch
309 StdFailure
310 error
311 .
312 (constructor
313 StdResult
314 StdFailure
315 (family NativeCheckpointFailure)
316 (family NativeCheckpointLayout)
317 (constructor NativeCheckpointFailure NativeCheckpointBounds)))
318 (branch
319 StdSuccess
320 tailPadding
321 .
322 (let unrestricted layout =
323 (constructor
324 NativeCheckpointLayout
325 NativeCheckpointLayoutOf
326 contract
327 base
328 updates
329 invocations
330 fullPadding
331 tailPadding
332 (nativeCheckpointHeaderFor contract))
333 in
334 (nat-eliminate
335 (lambda unrestricted fits : Nat .
336 (family
337 StdResult
338 (family NativeCheckpointFailure)
339 (family NativeCheckpointLayout)))
340 (constructor
341 StdResult
342 StdFailure
343 (family NativeCheckpointFailure)
344 (family NativeCheckpointLayout)
345 (constructor NativeCheckpointFailure NativeCheckpointBounds))
346 (lambda unrestricted previousFit : Nat .
347 (lambda unrestricted ignoredFit : (family StdResult (family NativeCheckpointFailure) (family NativeCheckpointLayout)) .
348 (constructor
349 StdResult
350 StdSuccess
351 (family NativeCheckpointFailure)
352 (family NativeCheckpointLayout)
353 layout)))
354 (naturalAnd
355 (naturalLessOrEqual (nativeCheckpointEnd layout) available)
356 (naturalLessOrEqual
357 (nativeCheckpointEnd layout)
358 18446744073709551615))))))))))
359 (naturalAnd
360 (naturalEqual (naturalModuloUnchecked base digestWorkAlignment) 0)
361 (naturalAnd
362 (naturalLessOrEqual 1 (checkpointEnvelopeContractChunk contract))
363 (naturalAnd
364 (naturalLessOrEqual
365 (checkpointEnvelopeContractChunk contract)
366 (checkpointEnvelopeContractPayload contract))
367 (naturalAnd
368 (naturalLessOrEqual (checkpointEnvelopeFileBytes contract) 2147479552)
369 (naturalAnd
370 (naturalLessOrEqual
371 nativeCheckpointWordBytes
372 (checkpointEnvelopeContractPayload contract))
373 (naturalAnd
374 (naturalLessOrEqual
375 updates
376 (naturalSaturatingSubtract
377 (checkpointEnvelopeContractPayload contract)
378 nativeCheckpointWordBytes))
379 (naturalAnd
380 (naturalLessOrEqual
381 invocations
382 (naturalSaturatingSubtract
383 (checkpointEnvelopeContractPayload contract)
384 nativeCheckpointWordBytes))
385 (naturalAnd
386 (naturalEqual
387 (naturalModuloUnchecked updates nativeCheckpointWordBytes)
388 0)
389 (naturalAnd
390 (naturalEqual
391 (naturalModuloUnchecked invocations nativeCheckpointWordBytes)
392 0)
393 (naturalEqual (naturalEqual updates invocations) 0))))))))))))))))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.