372def planNativeRegionCheckpoint =
373 (lambda unrestricted context : (family CheckpointEnvelopeContract) .
374 (lambda unrestricted regions : (family StdList (family CheckpointLogicalRegion)) .
375 (lambda unrestricted parts : (family StdList (family CheckpointRegionPartition)) .
376 (lambda unrestricted epoch : Nat .
377 (lambda unrestricted base : Nat .
378 (lambda unrestricted available : Nat .
379 (lambda unrestricted fragmentLimit : Nat .
380 (nat-eliminate
381 (lambda unrestricted flag : Nat .
382 (family
383 StdResult
384 (family NativeCheckpointFailure)
385 (family NativeRegionCheckpoint)))
386 (constructor
387 StdResult
388 StdFailure
389 (family NativeCheckpointFailure)
390 (family NativeRegionCheckpoint)
391 (constructor NativeCheckpointFailure NativeCheckpointBounds))
392 (lambda unrestricted previous : Nat .
393 (lambda unrestricted ignored : (family StdResult (family NativeCheckpointFailure) (family NativeRegionCheckpoint)) .
394 (let unrestricted logical =
395 (checkpointLogicalSchemaBytes regions)
396 in
397 (eliminate
398 StdResult
399 (lambda unrestricted current : (family StdResult (family NativeCheckpointFailure) (family NativeCheckpointLayout)) .
400 (family
401 StdResult
402 (family NativeCheckpointFailure)
403 (family NativeRegionCheckpoint)))
404 (planNativeCheckpoint
405 (nativeRegionContract
406 context
407 (bytes-append
408 b"ALPHA-REGION-MANIFEST-1\x00"
409 (bytes-append logical (nativeRegionPartitionBytes parts)))
410 (naturalAdd
411 nativeRegionCaptureBytes
412 (naturalMultiply
413 (nativeRegionShardCount parts)
414 nativeRegionRecordBytes)))
415 base
416 0
417 nativeCheckpointWordBytes
418 available)
419 (branch
420 StdFailure
421 error
422 .
423 (constructor
424 StdResult
425 StdFailure
426 (family NativeCheckpointFailure)
427 (family NativeRegionCheckpoint)
428 error))
429 (branch
430 StdSuccess
431 manifest
432 .
433 (eliminate
434 StdResult
435 (lambda unrestricted current : (family StdResult (family NativeCheckpointFailure) (family NativeRegionCheckpoint)) .
436 (family
437 StdResult
438 (family NativeCheckpointFailure)
439 (family NativeRegionCheckpoint)))
440 (nativeRegionAppendParts
441 context
442 logical
443 available
444 parts
445 (constructor
446 StdResult
447 StdSuccess
448 (family NativeCheckpointFailure)
449 (family NativeRegionCheckpoint)
450 (constructor
451 NativeRegionCheckpoint
452 NativeRegionCheckpointOf
453 manifest
454 (constructor StdList StdListEmpty (family NativeRegionShard))
455 epoch
456 (nativeCheckpointEnd manifest))))
457 (branch
458 StdFailure
459 error
460 .
461 (constructor
462 StdResult
463 StdFailure
464 (family NativeCheckpointFailure)
465 (family NativeRegionCheckpoint)
466 error))
467 (branch
468 StdSuccess
469 plan
470 .
471 (constructor
472 StdResult
473 StdSuccess
474 (family NativeCheckpointFailure)
475 (family NativeRegionCheckpoint)
476 (constructor
477 NativeRegionCheckpoint
478 NativeRegionCheckpointOf
479 manifest
480 (stdListReverse
481 (family NativeRegionShard)
482 (nativeRegionShards plan))
483 epoch
484 (nativeRegionEnd plan))))))))))
485 (naturalAnd
486 (checkpointPartitionsValid regions parts)
487 (naturalAnd
488 (naturalNonzero epoch)
489 (naturalAnd
490 (checkpointManifestWordFits epoch)
491 (naturalLessOrEqual (nativeRegionShardCount parts) fragmentLimit))))))))))))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.