Each chunk is copied into a separate padded arena, so hashing cannot
overwrite following payload bytes or an expected digest. Loop-affine offsets
derive from the admitted file schema. This fragment is used outside learning
repeats, since the current native program admits non-nested bounded loops.
452def nativeCheckpointHashChunk =
453 (lambda unrestricted layout : (family NativeCheckpointLayout) .
454 (lambda unrestricted extent : Nat .
455 (lambda unrestricted padding : Bytes .
456 (lambda unrestricted generate : Nat .
457 (lambda unrestricted slot : Nat .
458 (lambda unrestricted tail : (family NativePhysicalCommands) .
459 (nativeMemoryCopyOperands
460 (nativeMemoryState (nativeCheckpointChunkAt layout))
461 (nativeMemoryLoad (nativeCheckpointSourcePointerAt layout))
462 extent
463 slot
464 b"checkpoint-chunk-copy"
465 (nativeMemoryCopyPayload
466 (naturalAdd (nativeCheckpointChunkAt layout) extent)
467 padding
468 (nativeLaunchRecipeCommand
469 (constructor
470 NativePhysicalOperation
471 NativePhysicalMachineRoutine
472 nativeWordDigestRoutine
473 (constructor
474 NativePhysicalArguments
475 NativePhysicalArgumentsValue
476 (nativeMemoryState (nativeCheckpointChunkAt layout))
477 (nativeLaunchRecipeImmediate
478 (naturalDivideUnchecked
479 (naturalAdd extent (bytes-length padding))
480 digestBlockBytes))
481 (nativeMemoryState (nativeCheckpointDigestAt layout))
482 (nativeLaunchRecipeImmediate 0)
483 (nativeLaunchRecipeImmediate 0)
484 (nativeMemoryState (nativeCheckpointWorkAt layout)))
485 (nativeLaunchRecipeStore slot))
486 b"checkpoint-hash"
487 (nativeLaunchRecipeAssertEqual
488 (nativeLaunchRecipeSlotValue slot)
489 (nativeLaunchRecipeImmediate checkpointEnvelopeDigestBytes)
490 b"checkpoint-hash-count"
491 (nat-eliminate
492 (lambda unrestricted mode : Nat . (family NativePhysicalCommands))
493 (nativeMemoryCompareOperands
494 (nativeMemoryState (nativeCheckpointDigestAt layout))
495 (nativeMemoryLoad (nativeCheckpointDigestPointerAt layout))
496 checkpointEnvelopeDigestBytes
497 slot
498 b"checkpoint-chunk"
499 tail)
500 (lambda unrestricted previous : Nat .
501 (lambda unrestricted ignored : (family NativePhysicalCommands) .
502 (nativeMemoryCopyOperands
503 (nativeMemoryLoad (nativeCheckpointDigestPointerAt layout))
504 (nativeMemoryState (nativeCheckpointDigestAt layout))
505 checkpointEnvelopeDigestBytes
506 slot
507 b"checkpoint-digest-copy"
508 tail)))
509 generate)))))))))))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.