module Checkpoint.NativeEnvelope

import Checkpoint.Envelope
import Runtime.NativeFilePlan
import Runtime.NativeMemoryPlan
import Runtime.NativeMemoryRoutine
import Runtime.NativePhysicalProgram
import Runtime.NativeLaunchRecipeLoad
import Runtime.NativeWordDigest
import Runtime.WordDigest
import Runtime.ArenaCertificate
import Model.Word64
import Data.Bytes
import Data.SHA256
import Data.SHA256Padding
import Std.Foundation
import Std.Natural

-- A bounded in-memory realization of the shared checkpoint envelope. It is
-- suitable for a replicated state or an admitted shard, not a fleet gather.
-- Logical updates/invocations occupy explicit, distinct words in the hashed
-- payload. Header counters are checked against them before restore exposes any
-- state. No peer/file-provided extent controls allocation or pointer arithmetic.
family NativeCheckpointLayout : Type 0
constructor NativeCheckpointLayoutOf
field unrestricted nativeCheckpointLayoutContract : (family CheckpointEnvelopeContract)
field unrestricted nativeCheckpointLayoutBase : Nat
field unrestricted nativeCheckpointLayoutUpdates : Nat
field unrestricted nativeCheckpointLayoutInvocations : Nat
field unrestricted nativeCheckpointLayoutFullPadding : Bytes
field unrestricted nativeCheckpointLayoutTailPadding : Bytes
field unrestricted nativeCheckpointLayoutHeader : Bytes

end-family

family NativeCheckpointFailure : Type 0
constructor NativeCheckpointBounds

end-family

def nativeCheckpointContract =
  (lambda unrestricted layout : (family NativeCheckpointLayout) .
    (eliminate
      NativeCheckpointLayout
      (lambda unrestricted current : (family NativeCheckpointLayout) .
        (family CheckpointEnvelopeContract))
      layout
      (branch
        NativeCheckpointLayoutOf
        contract
        base
        updates
        invocations
        fullPadding
        tailPadding
        header
        .
        contract)))

def nativeCheckpointBase =
  (lambda unrestricted layout : (family NativeCheckpointLayout) .
    (eliminate
      NativeCheckpointLayout
      (lambda unrestricted current : (family NativeCheckpointLayout) . Nat)
      layout
      (branch
        NativeCheckpointLayoutOf
        contract
        base
        updates
        invocations
        fullPadding
        tailPadding
        header
        .
        base)))

def nativeCheckpointUpdatesOffset =
  (lambda unrestricted layout : (family NativeCheckpointLayout) .
    (eliminate
      NativeCheckpointLayout
      (lambda unrestricted current : (family NativeCheckpointLayout) . Nat)
      layout
      (branch
        NativeCheckpointLayoutOf
        contract
        base
        updates
        invocations
        fullPadding
        tailPadding
        header
        .
        updates)))

def nativeCheckpointInvocationsOffset =
  (lambda unrestricted layout : (family NativeCheckpointLayout) .
    (eliminate
      NativeCheckpointLayout
      (lambda unrestricted current : (family NativeCheckpointLayout) . Nat)
      layout
      (branch
        NativeCheckpointLayoutOf
        contract
        base
        updates
        invocations
        fullPadding
        tailPadding
        header
        .
        invocations)))

def nativeCheckpointFullPadding =
  (lambda unrestricted layout : (family NativeCheckpointLayout) .
    (eliminate
      NativeCheckpointLayout
      (lambda unrestricted current : (family NativeCheckpointLayout) . Bytes)
      layout
      (branch
        NativeCheckpointLayoutOf
        contract
        base
        updates
        invocations
        fullPadding
        tailPadding
        header
        .
        fullPadding)))

def nativeCheckpointTailPadding =
  (lambda unrestricted layout : (family NativeCheckpointLayout) .
    (eliminate
      NativeCheckpointLayout
      (lambda unrestricted current : (family NativeCheckpointLayout) . Bytes)
      layout
      (branch
        NativeCheckpointLayoutOf
        contract
        base
        updates
        invocations
        fullPadding
        tailPadding
        header
        .
        tailPadding)))

def nativeCheckpointWordBytes =
  (bytes-length (checkpointEnvelopeWord 0))

-- Header identities are immutable for a planned layout. Keep their derived
-- bytes in that layout so preparation, validation and command inspection
-- share the SHA computations. A suspended constructor field leaves bounds
-- admission cheap when no executable consumes the header. This is the same
-- canonical envelope, not a saved hash or a second digest implementation.
def nativeCheckpointHeaderFor =
  (lambda unrestricted contract : (family CheckpointEnvelopeContract) .
    (bytes-append
      (checkpointEnvelopeFixed contract)
      (bytes-append
        (dataBytesRepeatByte (byte 0) (naturalMultiply 2 nativeCheckpointWordBytes))
        (bytes-append
          (checkpointEnvelopeIdentityDigests contract)
          (dataBytesRepeatByte
            (byte 0)
            (naturalSaturatingSubtract
              (checkpointEnvelopeHeaderBytes contract)
              checkpointEnvelopeDigestsAt))))))

def nativeCheckpointHeader =
  (lambda unrestricted layout : (family NativeCheckpointLayout) .
    (eliminate
      NativeCheckpointLayout
      (lambda unrestricted current : (family NativeCheckpointLayout) . Bytes)
      layout
      (branch
        NativeCheckpointLayoutOf
        contract
        base
        updates
        invocations
        fullPadding
        tailPadding
        header
        .
        header)))

def nativeCheckpointAlign =
  (lambda unrestricted n : Nat .
    (naturalMultiply
      digestWorkAlignment
      (naturalDivideUnchecked
        (naturalAdd n (naturalSaturatingSubtract digestWorkAlignment 1))
        digestWorkAlignment)))

def nativeCheckpointFileBytes =
  (lambda unrestricted layout : (family NativeCheckpointLayout) .
    (checkpointEnvelopeFileBytes (nativeCheckpointContract layout)))

def nativeCheckpointHeaderBytes =
  (lambda unrestricted layout : (family NativeCheckpointLayout) .
    (checkpointEnvelopeHeaderBytes (nativeCheckpointContract layout)))

def nativeCheckpointPayloadAt =
  (lambda unrestricted layout : (family NativeCheckpointLayout) .
    (naturalAdd (nativeCheckpointBase layout) (nativeCheckpointHeaderBytes layout)))

def nativeCheckpointUpdatesAt =
  (lambda unrestricted layout : (family NativeCheckpointLayout) .
    (naturalAdd (nativeCheckpointPayloadAt layout) (nativeCheckpointUpdatesOffset layout)))

def nativeCheckpointInvocationsAt =
  (lambda unrestricted layout : (family NativeCheckpointLayout) .
    (naturalAdd (nativeCheckpointPayloadAt layout) (nativeCheckpointInvocationsOffset layout)))

def nativeCheckpointReadbackAt =
  (lambda unrestricted layout : (family NativeCheckpointLayout) .
    (naturalAdd (nativeCheckpointBase layout) (nativeCheckpointFileBytes layout)))

def nativeCheckpointProbeAt =
  (lambda unrestricted layout : (family NativeCheckpointLayout) .
    (naturalAdd (nativeCheckpointReadbackAt layout) (nativeCheckpointFileBytes layout)))

def nativeCheckpointChunkAt =
  (lambda unrestricted layout : (family NativeCheckpointLayout) .
    (nativeCheckpointAlign (succ (nativeCheckpointProbeAt layout))))

def nativeCheckpointChunkBytes =
  (lambda unrestricted layout : (family NativeCheckpointLayout) .
    (naturalAdd
      (checkpointEnvelopeContractChunk (nativeCheckpointContract layout))
      (bytes-length (nativeCheckpointFullPadding layout))))

def nativeCheckpointMetadataAt =
  (lambda unrestricted layout : (family NativeCheckpointLayout) .
    (naturalAdd (nativeCheckpointChunkAt layout) (nativeCheckpointChunkBytes layout)))

def nativeCheckpointDigestAt =
  (lambda unrestricted layout : (family NativeCheckpointLayout) .
    (naturalAdd (nativeCheckpointMetadataAt layout) (nativeCheckpointHeaderBytes layout)))

def nativeCheckpointWorkAt =
  (lambda unrestricted layout : (family NativeCheckpointLayout) .
    (nativeCheckpointAlign
      (naturalAdd (nativeCheckpointDigestAt layout) checkpointEnvelopeDigestBytes)))

def nativeCheckpointSourcePointerAt =
  (lambda unrestricted layout : (family NativeCheckpointLayout) .
    (naturalAdd (nativeCheckpointWorkAt layout) digestWorkBytes))

def nativeCheckpointDigestPointerAt =
  (lambda unrestricted layout : (family NativeCheckpointLayout) .
    (naturalAdd (nativeCheckpointSourcePointerAt layout) nativeCheckpointWordBytes))

def nativeCheckpointEnd =
  (lambda unrestricted layout : (family NativeCheckpointLayout) .
    (naturalAdd (nativeCheckpointDigestPointerAt layout) nativeCheckpointWordBytes))

def planNativeCheckpointNonempty =
  (lambda unrestricted contract : (family CheckpointEnvelopeContract) .
    (lambda unrestricted base : Nat .
      (lambda unrestricted updates : Nat .
        (lambda unrestricted invocations : Nat .
          (lambda unrestricted available : Nat .
            (nat-eliminate
              (lambda unrestricted admitted : Nat .
                (family StdResult (family NativeCheckpointFailure) (family NativeCheckpointLayout)))
              (constructor
                StdResult
                StdFailure
                (family NativeCheckpointFailure)
                (family NativeCheckpointLayout)
                (constructor NativeCheckpointFailure NativeCheckpointBounds))
              (lambda unrestricted previous : Nat .
                (lambda unrestricted ignored : (family StdResult (family NativeCheckpointFailure) (family NativeCheckpointLayout)) .
                  (eliminate
                    StdResult
                    (lambda unrestricted r : (family StdResult (family SHA256ErrorCode) Bytes) .
                      (family
                        StdResult
                        (family NativeCheckpointFailure)
                        (family NativeCheckpointLayout)))
                    (sha256PaddingSuffix (checkpointEnvelopeContractChunk contract))
                    (branch
                      StdFailure
                      error
                      .
                      (constructor
                        StdResult
                        StdFailure
                        (family NativeCheckpointFailure)
                        (family NativeCheckpointLayout)
                        (constructor NativeCheckpointFailure NativeCheckpointBounds)))
                    (branch
                      StdSuccess
                      fullPadding
                      .
                      (eliminate
                        StdResult
                        (lambda unrestricted r : (family StdResult (family SHA256ErrorCode) Bytes) .
                          (family
                            StdResult
                            (family NativeCheckpointFailure)
                            (family NativeCheckpointLayout)))
                        (sha256PaddingSuffix (checkpointEnvelopeTailBytes contract))
                        (branch
                          StdFailure
                          error
                          .
                          (constructor
                            StdResult
                            StdFailure
                            (family NativeCheckpointFailure)
                            (family NativeCheckpointLayout)
                            (constructor NativeCheckpointFailure NativeCheckpointBounds)))
                        (branch
                          StdSuccess
                          tailPadding
                          .
                          (let unrestricted layout =
                            (constructor
                              NativeCheckpointLayout
                              NativeCheckpointLayoutOf
                              contract
                              base
                              updates
                              invocations
                              fullPadding
                              tailPadding
                              (nativeCheckpointHeaderFor contract))
                            in
                            (nat-eliminate
                              (lambda unrestricted fits : Nat .
                                (family
                                  StdResult
                                  (family NativeCheckpointFailure)
                                  (family NativeCheckpointLayout)))
                              (constructor
                                StdResult
                                StdFailure
                                (family NativeCheckpointFailure)
                                (family NativeCheckpointLayout)
                                (constructor NativeCheckpointFailure NativeCheckpointBounds))
                              (lambda unrestricted previousFit : Nat .
                                (lambda unrestricted ignoredFit : (family StdResult (family NativeCheckpointFailure) (family NativeCheckpointLayout)) .
                                  (constructor
                                    StdResult
                                    StdSuccess
                                    (family NativeCheckpointFailure)
                                    (family NativeCheckpointLayout)
                                    layout)))
                              (naturalAnd
                                (naturalLessOrEqual (nativeCheckpointEnd layout) available)
                                (naturalLessOrEqual
                                  (nativeCheckpointEnd layout)
                                  18446744073709551615))))))))))
              (naturalAnd
                (naturalEqual (naturalModuloUnchecked base digestWorkAlignment) 0)
                (naturalAnd
                  (naturalLessOrEqual 1 (checkpointEnvelopeContractChunk contract))
                  (naturalAnd
                    (naturalLessOrEqual
                      (checkpointEnvelopeContractChunk contract)
                      (checkpointEnvelopeContractPayload contract))
                    (naturalAnd
                      (naturalLessOrEqual (checkpointEnvelopeFileBytes contract) 2147479552)
                      (naturalAnd
                        (naturalLessOrEqual
                          nativeCheckpointWordBytes
                          (checkpointEnvelopeContractPayload contract))
                        (naturalAnd
                          (naturalLessOrEqual
                            updates
                            (naturalSaturatingSubtract
                              (checkpointEnvelopeContractPayload contract)
                              nativeCheckpointWordBytes))
                          (naturalAnd
                            (naturalLessOrEqual
                              invocations
                              (naturalSaturatingSubtract
                                (checkpointEnvelopeContractPayload contract)
                                nativeCheckpointWordBytes))
                            (naturalAnd
                              (naturalEqual
                                (naturalModuloUnchecked updates nativeCheckpointWordBytes)
                                0)
                              (naturalAnd
                                (naturalEqual
                                  (naturalModuloUnchecked invocations nativeCheckpointWordBytes)
                                  0)
                                (naturalEqual (naturalEqual updates invocations) 0))))))))))))))))

-- Avoid evaluating chunk division even in strict artifact realization when
-- the proposed contract has a zero chunk width.
def planNativeCheckpoint =
  (lambda unrestricted contract : (family CheckpointEnvelopeContract) .
    (lambda unrestricted base : Nat .
      (lambda unrestricted updates : Nat .
        (lambda unrestricted invocations : Nat .
          (lambda unrestricted available : Nat .
            (nat-eliminate
              (lambda unrestricted valid : Nat .
                (family StdResult (family NativeCheckpointFailure) (family NativeCheckpointLayout)))
              (constructor
                StdResult
                StdFailure
                (family NativeCheckpointFailure)
                (family NativeCheckpointLayout)
                (constructor NativeCheckpointFailure NativeCheckpointBounds))
              (lambda unrestricted previous : Nat .
                (lambda unrestricted ignored : (family StdResult (family NativeCheckpointFailure) (family NativeCheckpointLayout)) .
                  (planNativeCheckpointNonempty contract base updates invocations available)))
              (naturalNonzero (checkpointEnvelopeContractChunk contract))))))))

def nativeCheckpointStore =
  (lambda unrestricted at : Nat .
    (lambda unrestricted value : (family NativePhysicalOperand) .
      (nativeLaunchRecipeCommand
        (constructor NativePhysicalOperation NativePhysicalStoreWord64 (nativeMemoryState at) value)
        b"checkpoint-state")))

def nativeCheckpointAffine =
  (lambda unrestricted base : Nat .
    (lambda unrestricted stride : Nat .
      (constructor
        NativePhysicalOperand
        NativePhysicalLoopAffine
        (modelWord64FromNaturalTruncated base)
        (modelWord64FromNaturalTruncated stride))))

def nativeCheckpointPointer =
  (lambda unrestricted at : Nat .
    (lambda unrestricted base : Nat .
      (lambda unrestricted stride : Nat .
        (lambda unrestricted tail : (family NativePhysicalCommands) .
          (nativeLaunchRecipeCommand
            (constructor
              NativePhysicalOperation
              NativePhysicalAddWord64
              (nativeMemoryState at)
              (nativeMemoryState base)
              (nativeCheckpointAffine 0 stride))
            b"checkpoint-chunk-pointer"
            tail)))))

-- 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.
def nativeCheckpointHashChunk =
  (lambda unrestricted layout : (family NativeCheckpointLayout) .
    (lambda unrestricted extent : Nat .
      (lambda unrestricted padding : Bytes .
        (lambda unrestricted generate : Nat .
          (lambda unrestricted slot : Nat .
            (lambda unrestricted tail : (family NativePhysicalCommands) .
              (nativeMemoryCopyOperands
                (nativeMemoryState (nativeCheckpointChunkAt layout))
                (nativeMemoryLoad (nativeCheckpointSourcePointerAt layout))
                extent
                slot
                b"checkpoint-chunk-copy"
                (nativeMemoryCopyPayload
                  (naturalAdd (nativeCheckpointChunkAt layout) extent)
                  padding
                  (nativeLaunchRecipeCommand
                    (constructor
                      NativePhysicalOperation
                      NativePhysicalMachineRoutine
                      nativeWordDigestRoutine
                      (constructor
                        NativePhysicalArguments
                        NativePhysicalArgumentsValue
                        (nativeMemoryState (nativeCheckpointChunkAt layout))
                        (nativeLaunchRecipeImmediate
                          (naturalDivideUnchecked
                            (naturalAdd extent (bytes-length padding))
                            digestBlockBytes))
                        (nativeMemoryState (nativeCheckpointDigestAt layout))
                        (nativeLaunchRecipeImmediate 0)
                        (nativeLaunchRecipeImmediate 0)
                        (nativeMemoryState (nativeCheckpointWorkAt layout)))
                      (nativeLaunchRecipeStore slot))
                    b"checkpoint-hash"
                    (nativeLaunchRecipeAssertEqual
                      (nativeLaunchRecipeSlotValue slot)
                      (nativeLaunchRecipeImmediate checkpointEnvelopeDigestBytes)
                      b"checkpoint-hash-count"
                      (nat-eliminate
                        (lambda unrestricted mode : Nat . (family NativePhysicalCommands))
                        (nativeMemoryCompareOperands
                          (nativeMemoryState (nativeCheckpointDigestAt layout))
                          (nativeMemoryLoad (nativeCheckpointDigestPointerAt layout))
                          checkpointEnvelopeDigestBytes
                          slot
                          b"checkpoint-chunk"
                          tail)
                        (lambda unrestricted previous : Nat .
                          (lambda unrestricted ignored : (family NativePhysicalCommands) .
                            (nativeMemoryCopyOperands
                              (nativeMemoryLoad (nativeCheckpointDigestPointerAt layout))
                              (nativeMemoryState (nativeCheckpointDigestAt layout))
                              checkpointEnvelopeDigestBytes
                              slot
                              b"checkpoint-digest-copy"
                              tail)))
                        generate)))))))))))

def nativeCheckpointDigests =
  (lambda unrestricted layout : (family NativeCheckpointLayout) .
    (lambda unrestricted generate : Nat .
      (lambda unrestricted slot : Nat .
        (lambda unrestricted tail : (family NativePhysicalCommands) .
          (let unrestricted contract =
            (nativeCheckpointContract layout)
            in
            (let unrestricted full =
              (checkpointEnvelopeFullChunks contract)
              in
              (let unrestricted chunk =
                (checkpointEnvelopeContractChunk contract)
                in
                (let unrestricted last =
                  (checkpointEnvelopeTailBytes contract)
                  in
                  (nativeLaunchRecipeCommand
                    (constructor
                      NativePhysicalOperation
                      NativePhysicalRepeatBeginCounted
                      (nativeLaunchRecipeImmediate full))
                    b"checkpoint-chunks"
                    (nativeCheckpointPointer
                      (nativeCheckpointSourcePointerAt layout)
                      (nativeCheckpointPayloadAt layout)
                      chunk
                      (nativeCheckpointPointer
                        (nativeCheckpointDigestPointerAt layout)
                        (naturalAdd (nativeCheckpointBase layout) checkpointEnvelopeDigestsAt)
                        checkpointEnvelopeDigestBytes
                        (nativeCheckpointHashChunk
                          layout
                          chunk
                          (nativeCheckpointFullPadding layout)
                          generate
                          slot
                          (nativeLaunchRecipeCommand
                            (constructor NativePhysicalOperation NativePhysicalRepeatEnd)
                            b"checkpoint-chunks-end"
                            (nativeFileWhen
                              (naturalNonzero last)
                              (lambda unrestricted after : (family NativePhysicalCommands) .
                                (nativeCheckpointStore
                                  (nativeCheckpointSourcePointerAt layout)
                                  (nativeMemoryState
                                    (naturalAdd
                                      (nativeCheckpointPayloadAt layout)
                                      (naturalMultiply full chunk)))
                                  (nativeCheckpointStore
                                    (nativeCheckpointDigestPointerAt layout)
                                    (nativeMemoryState
                                      (naturalAdd
                                        (naturalAdd
                                        (nativeCheckpointBase layout)
                                        checkpointEnvelopeDigestsAt)
                                        (naturalMultiply full checkpointEnvelopeDigestBytes)))
                                    (nativeCheckpointHashChunk
                                      layout
                                      last
                                      (nativeCheckpointTailPadding layout)
                                      generate
                                      slot
                                      after))))
                              tail))))))))))))))

def nativeCheckpointRequireCounters =
  (lambda unrestricted layout : (family NativeCheckpointLayout) .
    (lambda unrestricted tail : (family NativePhysicalCommands) .
      (nativeLaunchRecipeAssertEqual
        (nativeMemoryLoad (naturalAdd (nativeCheckpointBase layout) checkpointEnvelopeUpdatesAt))
        (nativeMemoryLoad (nativeCheckpointUpdatesAt layout))
        b"checkpoint-update-counter"
        (nativeLaunchRecipeAssertEqual
          (nativeMemoryLoad
            (naturalAdd (nativeCheckpointBase layout) checkpointEnvelopeInvocationsAt))
          (nativeMemoryLoad (nativeCheckpointInvocationsAt layout))
          b"checkpoint-invocation-counter"
          tail))))

def nativeCheckpointPrepare =
  (lambda unrestricted layout : (family NativeCheckpointLayout) .
    (lambda unrestricted slot : Nat .
      (lambda unrestricted tail : (family NativePhysicalCommands) .
        (nativeMemoryCopyPayload
          (nativeCheckpointBase layout)
          (nativeCheckpointHeader layout)
          (nativeCheckpointStore
            (naturalAdd (nativeCheckpointBase layout) checkpointEnvelopeUpdatesAt)
            (nativeMemoryLoad (nativeCheckpointUpdatesAt layout))
            (nativeCheckpointStore
              (naturalAdd (nativeCheckpointBase layout) checkpointEnvelopeInvocationsAt)
              (nativeMemoryLoad (nativeCheckpointInvocationsAt layout))
              (nativeCheckpointDigests layout 1 slot tail)))))))

-- Canonical zero padding is part of version one's envelope, not an extension
-- area whose arbitrary bytes may survive integrity checks unnoticed.
def nativeCheckpointRequirePadding =
  (lambda unrestricted layout : (family NativeCheckpointLayout) .
    (lambda unrestricted slot : Nat .
      (lambda unrestricted tail : (family NativePhysicalCommands) .
        (let unrestricted start =
          (naturalAdd
            checkpointEnvelopeDigestsAt
            (naturalMultiply
              checkpointEnvelopeDigestBytes
              (checkpointEnvelopeChunkCount (nativeCheckpointContract layout))))
          in
          (nativeMemoryCompareRegions
            (naturalAdd (nativeCheckpointBase layout) start)
            (naturalAdd (nativeCheckpointMetadataAt layout) start)
            (naturalSaturatingSubtract (nativeCheckpointHeaderBytes layout) start)
            slot
            b"checkpoint-padding"
            tail)))))

def nativeCheckpointValidate =
  (lambda unrestricted layout : (family NativeCheckpointLayout) .
    (lambda unrestricted slot : Nat .
      (lambda unrestricted tail : (family NativePhysicalCommands) .
        (nativeMemoryCopyPayload
          (nativeCheckpointMetadataAt layout)
          (nativeCheckpointHeader layout)
          (nativeMemoryCompareRegions
            (nativeCheckpointBase layout)
            (nativeCheckpointMetadataAt layout)
            checkpointEnvelopeFixedBytes
            slot
            b"checkpoint-layout"
            (nativeMemoryCompareRegions
              (naturalAdd (nativeCheckpointBase layout) checkpointEnvelopeSchemaAt)
              (naturalAdd (nativeCheckpointMetadataAt layout) checkpointEnvelopeSchemaAt)
              (naturalSaturatingSubtract checkpointEnvelopeDigestsAt checkpointEnvelopeSchemaAt)
              slot
              b"checkpoint-identity"
              (nativeCheckpointRequirePadding
                layout
                slot
                (nativeCheckpointDigests
                  layout
                  0
                  slot
                  (nativeCheckpointRequireCounters layout tail)))))))))

def nativeCheckpointRestore =
  (lambda unrestricted layout : (family NativeCheckpointLayout) .
    (lambda unrestricted path : (family NativePhysicalOperand) .
      (lambda unrestricted descriptor : Nat .
        (lambda unrestricted slot : Nat .
          (lambda unrestricted tail : (family NativePhysicalCommands) .
            (nativeFileOpen
              path
              nativeFileReadFlags
              descriptor
              slot
              b"checkpoint-open"
              (nativeFileRead
                (nativeLaunchRecipeSlotValue descriptor)
                (nativeMemoryState (nativeCheckpointBase layout))
                (nativeCheckpointFileBytes layout)
                (nativeLaunchRecipeImmediate 0)
                slot
                b"checkpoint-read"
                (nativeFileRequireEOF
                  (nativeLaunchRecipeSlotValue descriptor)
                  (nativeMemoryState (nativeCheckpointProbeAt layout))
                  (nativeCheckpointFileBytes layout)
                  slot
                  (nativeFileClose
                    (nativeLaunchRecipeSlotValue descriptor)
                    slot
                    b"checkpoint-read-close"
                    (nativeCheckpointValidate layout slot tail))))))))))

def nativeCheckpointPublish =
  (lambda unrestricted layout : (family NativeCheckpointLayout) .
    (lambda unrestricted candidate : (family NativePhysicalOperand) .
      (lambda unrestricted committed : (family NativePhysicalOperand) .
        (lambda unrestricted directory : (family NativePhysicalOperand) .
          (lambda unrestricted descriptor : Nat .
            (lambda unrestricted slot : Nat .
              (lambda unrestricted stages : Nat .
                (lambda unrestricted tail : (family NativePhysicalCommands) .
                  (nativeCheckpointPrepare
                    layout
                    slot
                    (nativeFileOpen
                      candidate
                      nativeFileCandidateFlags
                      descriptor
                      slot
                      b"checkpoint-candidate-open"
                      (nativeFileWrite
                        (nativeLaunchRecipeSlotValue descriptor)
                        (nativeMemoryState (nativeCheckpointBase layout))
                        (nativeCheckpointFileBytes layout)
                        (nativeLaunchRecipeImmediate 0)
                        slot
                        b"checkpoint-write"
                        (nativeFileRead
                          (nativeLaunchRecipeSlotValue descriptor)
                          (nativeMemoryState (nativeCheckpointReadbackAt layout))
                          (nativeCheckpointFileBytes layout)
                          (nativeLaunchRecipeImmediate 0)
                          slot
                          b"checkpoint-readback"
                          (nativeFileRequireEOF
                            (nativeLaunchRecipeSlotValue descriptor)
                            (nativeMemoryState (nativeCheckpointProbeAt layout))
                            (nativeCheckpointFileBytes layout)
                            slot
                            (nativeMemoryCompareRegions
                              (nativeCheckpointBase layout)
                              (nativeCheckpointReadbackAt layout)
                              (nativeCheckpointFileBytes layout)
                              slot
                              b"checkpoint-readback-mismatch"
                              (nativeFileCommitStages
                                stages
                                0
                                descriptor
                                slot
                                candidate
                                committed
                                directory
                                tail)))))))))))))))

def nativeCheckpointResidents =
  (lambda unrestricted layout : (family NativeCheckpointLayout) .
    (constructor
      ArenaResidents
      ArenaResidentsNext
      (constructor
        ArenaResident
        ArenaResidentValue
        b"checkpoint-file"
        (nativeCheckpointBase layout)
        (nativeCheckpointFileBytes layout)
        1)
      (constructor
        ArenaResidents
        ArenaResidentsNext
        (constructor
          ArenaResident
          ArenaResidentValue
          b"checkpoint-readback"
          (nativeCheckpointReadbackAt layout)
          (succ (nativeCheckpointFileBytes layout))
          1)
        (constructor
          ArenaResidents
          ArenaResidentsNext
          (constructor
            ArenaResident
            ArenaResidentValue
            b"checkpoint-chunk"
            (nativeCheckpointChunkAt layout)
            (nativeCheckpointChunkBytes layout)
            1)
          (constructor
            ArenaResidents
            ArenaResidentsNext
            (constructor
              ArenaResident
              ArenaResidentValue
              b"checkpoint-metadata"
              (nativeCheckpointMetadataAt layout)
              (nativeCheckpointHeaderBytes layout)
              1)
            (constructor
              ArenaResidents
              ArenaResidentsNext
              (constructor
                ArenaResident
                ArenaResidentValue
                b"checkpoint-digest"
                (nativeCheckpointDigestAt layout)
                checkpointEnvelopeDigestBytes
                1)
              (constructor
                ArenaResidents
                ArenaResidentsNext
                (constructor
                  ArenaResident
                  ArenaResidentValue
                  b"checkpoint-hash-work"
                  (nativeCheckpointWorkAt layout)
                  digestWorkBytes
                  1)
                (constructor
                  ArenaResidents
                  ArenaResidentsNext
                  (constructor
                    ArenaResident
                    ArenaResidentValue
                    b"checkpoint-pointers"
                    (nativeCheckpointSourcePointerAt layout)
                    (naturalMultiply 2 nativeCheckpointWordBytes)
                    1)
                  (constructor ArenaResidents ArenaResidentsEnd)))))))))