module Runtime.NativeIndependentState

import Learning.IndependentState
import Component.Pointwise
import Checkpoint.Envelope
import Checkpoint.NativeEnvelope
import Checkpoint.NativeRegions
import Checkpoint.NativePeerPublication
import Checkpoint.RegionManifest
import Compiler.Planning.RegionFrame
import Runtime.NativePointwisePlan
import Runtime.NativePhysicalProgram
import Runtime.NativePhysicalProgramComposer
import Runtime.NativePhysicalNativeELF
import Runtime.NativeHostTarget
import Runtime.NativeResourcePlan
import Runtime.NativeLaunchRecipeLoad
import Runtime.NativeMemoryPlan
import Runtime.NativeFloatPlan
import Runtime.NativeFilePlan
import Runtime.NativeSocketPlan
import Runtime.NativePeerEndpoint
import Runtime.NativeRegionFrame
import Runtime.NativeWordArithmetic
import Runtime.RegionTransfer
import Runtime.ArenaCertificate
import Learning.Transition
import Representation.Partition
import Data.Bytes
import Data.SHA256Padding
import Data.SHA256Digest
import Model.Word64
import Std.Byte
import Std.Foundation
import Std.List
import Std.Natural
import Std.Word

-- This realization compiles separately owned state transitions, one per
-- observation row of the system: owners 0..n-1 over a star. There is no
-- per-step collective because the admitted transition reads only local state
-- and immutable local inputs. The final capture joins every authority at
-- owner 0 (Checkpoint.NativePeerPublication); a missing or differently
-- advanced owner cannot publish a logical checkpoint.
-- Execution is selected explicitly: target callbacks supply local state work,
-- while this owner supplies versions, transport and durable publication.
family NativeIndependentLayout : Type 0
constructor NativeIndependentLayoutOf
field unrestricted independentCaptureFrame : (family RegionFrameLayout)
field unrestricted independentCommittedFrame : (family RegionFrameLayout)
field unrestricted independentCheckpointPlan : (family NativeRegionCheckpoint)
field unrestricted independentHostScratchWords : Nat
-- the system identity's digest, computed once per artifact: every frame
-- identity of the owner names it
field unrestricted independentDigest : Bytes

end-family

def niCapture =
  (lambda unrestricted layout : (family NativeIndependentLayout) .
    (eliminate
      NativeIndependentLayout
      (lambda unrestricted current : (family NativeIndependentLayout) . (family RegionFrameLayout))
      layout
      (branch NativeIndependentLayoutOf capture committed checkpoint scratchWords digest . capture)))

def niCommitted =
  (lambda unrestricted layout : (family NativeIndependentLayout) .
    (eliminate
      NativeIndependentLayout
      (lambda unrestricted current : (family NativeIndependentLayout) . (family RegionFrameLayout))
      layout
      (branch
        NativeIndependentLayoutOf
        capture
        committed
        checkpoint
        scratchWords
        digest
        .
        committed)))

def niCheckpoint =
  (lambda unrestricted layout : (family NativeIndependentLayout) .
    (eliminate
      NativeIndependentLayout
      (lambda unrestricted current : (family NativeIndependentLayout) .
        (family NativeRegionCheckpoint))
      layout
      (branch
        NativeIndependentLayoutOf
        capture
        committed
        checkpoint
        scratchWords
        digest
        .
        checkpoint)))

-- Scratch is selected by the realization. A GPU state program needs no host
-- arithmetic temporaries; its callback reserves only actual session state.
def niScratchWords =
  (lambda unrestricted layout : (family NativeIndependentLayout) .
    (eliminate
      NativeIndependentLayout
      (lambda unrestricted current : (family NativeIndependentLayout) . Nat)
      layout
      (branch
        NativeIndependentLayoutOf
        capture
        committed
        checkpoint
        scratchWords
        digest
        .
        scratchWords)))

def niDigest =
  (lambda unrestricted layout : (family NativeIndependentLayout) .
    (eliminate
      NativeIndependentLayout
      (lambda unrestricted current : (family NativeIndependentLayout) . Bytes)
      layout
      (branch NativeIndependentLayoutOf capture committed checkpoint scratchWords digest . digest)))

def niEnd =
  (constructor NativePhysicalCommands NativePhysicalCommandsEnd)

def niHalt =
  (nativeLaunchRecipeCommand
    (constructor NativePhysicalOperation NativePhysicalHaltSuccess)
    b"independent-done"
    niEnd)

-- The owners: one per observation row of the system.
def niOwners =
  (lambda unrestricted slots : Nat .
    (lambda unrestricted system : (family IndependentStateSystem slots) .
      (stdListLength (family StdList StdU64) (independentInitialValues slots system))))

-- argv: previous manifest, one previous shard per owner, then each owner's
-- candidate/committed output shard, the manifest pair and the directory.
def niPaths =
  (lambda unrestricted slots : Nat .
    (lambda unrestricted system : (family IndependentStateSystem slots) .
      (constructor NativeRegionPaths NativeRegionPathsOf 1 (niOwners slots system))))

def niStateAt =
  (lambda unrestricted layout : (family NativeIndependentLayout) .
    (nativeRegionEnd (niCheckpoint layout)))

def niValuesAt =
  (lambda unrestricted layout : (family NativeIndependentLayout) .
    (naturalAdd (niStateAt layout) nativeRegionCaptureBytes))

def niWidth =
  (lambda unrestricted slots : Nat .
    (lambda unrestricted system : (family IndependentStateSystem slots) .
      (nativePointwiseAt 0 (independentPersistentCount slots system))))

def niCaptureBytes =
  (lambda unrestricted slots : Nat .
    (lambda unrestricted system : (family IndependentStateSystem slots) .
      (naturalAdd nativeRegionCaptureBytes (niWidth slots system))))

def niEndpoint =
  (lambda unrestricted slots : Nat .
    (lambda unrestricted system : (family IndependentStateSystem slots) .
      (lambda unrestricted layout : (family NativeIndependentLayout) .
        (nativePointwiseAt (niValuesAt layout) (naturalAdd slots (niScratchWords layout))))))

-- The endpoint state holds one address entry per edge of this owner.
def niExtent =
  (lambda unrestricted slots : Nat .
    (lambda unrestricted system : (family IndependentStateSystem slots) .
      (lambda unrestricted layout : (family NativeIndependentLayout) .
        (lambda unrestricted edges : (family StdList (family NativePeerEdge)) .
          (nativePeerEdgesEnd (niEndpoint slots system layout) edges)))))

def niInterval =
  (lambda unrestricted slots : Nat .
    (lambda unrestricted system : (family IndependentStateSystem slots) .
      (lambda unrestricted owner : Nat .
        (constructor
          LogicalInterval
          LogicalIntervalOf
          (naturalMultiply owner (niWidth slots system))
          (naturalMultiply (succ owner) (niWidth slots system))))))

def niRegions =
  (lambda unrestricted slots : Nat .
    (lambda unrestricted system : (family IndependentStateSystem slots) .
      (constructor
        StdList
        StdListCons
        (family CheckpointLogicalRegion)
        (constructor
          CheckpointLogicalRegion
          CheckpointLogicalRegionOf
          b"owned-state"
          b"f64-le"
          (naturalMultiply (niOwners slots system) (niWidth slots system)))
        (constructor StdList StdListEmpty (family CheckpointLogicalRegion)))))

def niPartitions =
  (lambda unrestricted slots : Nat .
    (lambda unrestricted system : (family IndependentStateSystem slots) .
      (constructor
        StdList
        StdListCons
        (family CheckpointRegionPartition)
        (constructor
          CheckpointRegionPartition
          CheckpointRegionPartitionOf
          0
          (stdListMap
            Nat
            (family LogicalInterval)
            (niInterval slots system)
            (stdListNaturalsBelow (niOwners slots system))))
        (constructor StdList StdListEmpty (family CheckpointRegionPartition)))))

def niContext =
  (lambda unrestricted slots : Nat .
    (lambda unrestricted system : (family IndependentStateSystem slots) .
      (constructor
        CheckpointEnvelopeContract
        CheckpointEnvelopeContractValue
        (bytes-append
          b"independent-owner-state-f64-finite-rne-separate-v2;"
          (independentStateIdentity slots system))
        b"typed-sequential-local-transitions"
        b"immutable-local-inputs;one-input-round-per-update"
        b"declared-initial-state;no-randomness"
        1
        1
        1)))

def niIdentityDigest =
  (lambda unrestricted slots : Nat .
    (lambda unrestricted system : (family IndependentStateSystem slots) .
      (sha256RawDigestOrEmpty (independentStateIdentity slots system))))

def niIdentity =
  (lambda unrestricted slots : Nat .
    (lambda unrestricted system : (family IndependentStateSystem slots) .
      (lambda unrestricted digest : Bytes .
        (lambda unrestricted operation : Nat .
          (lambda unrestricted sender : Nat .
            (lambda unrestricted receiver : Nat .
              (constructor
                RegionTransferIdentity
                RegionTransferIdentityOf
                digest
                b"independent-state-v1"
                b"owned-state"
                b"finite-f64-rne-separate"
                (constructor LearningRound LearningRoundOf 1 0)
                operation
                sender
                receiver
                (constructor
                  LogicalInterval
                  LogicalIntervalOf
                  0
                  (naturalMultiply (niOwners slots system) (niWidth slots system))))))))))

-- One owner's frame in the storage the layout planned for owner 1. Frames
-- differ only in their identity-bound header. A frame that cannot be planned
-- there falls back to an empty header: its extent then differs from owner
-- 1's, and Checkpoint.NativePeerPublication's shared-storage admission
-- refuses the whole publication instead of using a misidentified frame.
def niFrameAt =
  (lambda unrestricted identity : (family RegionTransferIdentity) .
    (lambda unrestricted payload : Nat .
      (lambda unrestricted at : (family RegionFrameLayout) .
        (eliminate
          StdResult
          (lambda unrestricted result : (family StdResult (family RegionFrameLayoutFailure) (family RegionFrameLayout)) .
            (family RegionFrameLayout))
          (planRegionFrameLayout identity payload 512 (frameBase at) (frameEnd at))
          (branch
            StdFailure
            error
            .
            (constructor RegionFrameLayout RegionFrameLayoutOf b"" payload (frameBase at) b""))
          (branch StdSuccess frame . frame)))))

def niCaptureFor =
  (lambda unrestricted slots : Nat .
    (lambda unrestricted system : (family IndependentStateSystem slots) .
      (lambda unrestricted layout : (family NativeIndependentLayout) .
        (lambda unrestricted owner : Nat .
          (niFrameAt
            (niIdentity slots system (niDigest layout) 0 owner 0)
            (niCaptureBytes slots system)
            (niCapture layout))))))

def niCommittedFor =
  (lambda unrestricted slots : Nat .
    (lambda unrestricted system : (family IndependentStateSystem slots) .
      (lambda unrestricted layout : (family NativeIndependentLayout) .
        (lambda unrestricted owner : Nat .
          (niFrameAt
            (niIdentity slots system (niDigest layout) 1 0 owner)
            nativePointwiseWordBytes
            (niCommitted layout))))))

-- Owner 0 has an edge to every other owner, in order; every other owner has
-- one edge, to owner 0. `addresses` are those edges' addresses.
def niEdges =
  (lambda unrestricted slots : Nat .
    (lambda unrestricted system : (family IndependentStateSystem slots) .
      (lambda unrestricted owner : Nat .
        (lambda unrestricted addresses : (family StdList Bytes) .
          (nativePeerStarEdges owner addresses)))))

def niEdgesAdmitted =
  (lambda unrestricted slots : Nat .
    (lambda unrestricted system : (family IndependentStateSystem slots) .
      (lambda unrestricted owner : Nat .
        (lambda unrestricted addresses : (family StdList Bytes) .
          (nativePeerStarAdmitted (niOwners slots system) owner addresses)))))

def niPublication =
  (lambda unrestricted slots : Nat .
    (lambda unrestricted system : (family IndependentStateSystem slots) .
      (lambda unrestricted layout : (family NativeIndependentLayout) .
        (lambda unrestricted resume : Nat .
          (lambda unrestricted edges : (family StdList (family NativePeerEdge)) .
            (constructor
              NativePeerRegionPublication
              NativePeerRegionPublicationOf
              (constructor
                NativeRegionCheckpoint
                NativeRegionCheckpointOf
                (nativeRegionManifest (niCheckpoint layout))
                (nativeRegionShards (niCheckpoint layout))
                (naturalAdd (nativeRegionEpoch (niCheckpoint layout)) resume)
                (nativeRegionEnd (niCheckpoint layout)))
              (naturalPredecessor (niOwners slots system))
              (niCaptureFor slots system layout)
              (niCommittedFor slots system layout)
              (nativePeerEdgeConnectionTo edges)
              (niStateAt layout)
              (niCaptureBytes slots system)
              nativeRegionCaptureBytes
              (lambda unrestricted shard : (family NativeRegionShard) .
                (naturalDivideUnchecked
                  (intervalBegin (nativeRegionInterval shard))
                  (niWidth slots system)))
              (lambda unrestricted shard : (family NativeRegionShard) . nativeRegionCaptureBytes)
              (niPaths slots system)))))))

def niWithLayout =
  (lambda unrestricted slots : Nat .
    (lambda unrestricted system : (family IndependentStateSystem slots) .
      (lambda unrestricted epoch : Nat .
        (lambda unrestricted base : Nat .
          (lambda unrestricted scratchWords : Nat .
            (lambda unrestricted available : Nat .
              (lambda unrestricted emit : (pi unrestricted layout : (family NativeIndependentLayout) . Bytes) .
                (let unrestricted digest =
                  (niIdentityDigest slots system)
                  in
                  (eliminate
                    StdResult
                    (lambda unrestricted result : (family StdResult (family RegionFrameLayoutFailure) (family RegionFrameLayout)) .
                      Bytes)
                    (planRegionFrameLayout
                      (niIdentity slots system digest 0 1 0)
                      (niCaptureBytes slots system)
                      512
                      base
                      available)
                    (branch StdFailure error . b"")
                    (branch
                      StdSuccess
                      capture
                      .
                      (eliminate
                        StdResult
                        (lambda unrestricted result : (family StdResult (family RegionFrameLayoutFailure) (family RegionFrameLayout)) .
                          Bytes)
                        (planRegionFrameLayout
                          (niIdentity slots system digest 1 0 1)
                          nativePointwiseWordBytes
                          512
                          (frameAlign (frameEnd capture))
                          available)
                        (branch StdFailure error . b"")
                        (branch
                          StdSuccess
                          committed
                          .
                          (eliminate
                            StdResult
                            (lambda unrestricted result : (family StdResult (family NativeCheckpointFailure) (family NativeRegionCheckpoint)) .
                              Bytes)
                            (planNativeRegionCheckpoint
                              (niContext slots system)
                              (niRegions slots system)
                              (niPartitions slots system)
                              epoch
                              (frameAlign (frameEnd committed))
                              available
                              (niOwners slots system))
                            (branch StdFailure error . b"")
                            (branch
                              StdSuccess
                              checkpoint
                              .
                              (emit
                                (constructor
                                  NativeIndependentLayout
                                  NativeIndependentLayoutOf
                                  capture
                                  committed
                                  checkpoint
                                  scratchWords
                                  digest))))))))))))))))

def niDestinations =
  (lambda unrestricted slots : Nat .
    (lambda unrestricted system : (family IndependentStateSystem slots) .
      (lambda unrestricted layout : (family NativeIndependentLayout) .
        (lambda unrestricted owner : Nat .
          (constructor
            StdList
            StdListCons
            (family NativeRegionDestination)
            (constructor
              NativeRegionDestination
              NativeRegionDestinationOf
              0
              (niInterval slots system owner)
              (niValuesAt layout))
            (constructor StdList StdListEmpty (family NativeRegionDestination)))))))

def niOutput =
  (lambda unrestricted base : Nat .
    (lambda unrestricted size : Nat .
      (lambda unrestricted tail : (family NativePhysicalCommands) .
        (nativeFileCall
          1
          (nativeLaunchRecipeArguments
            (nativeLaunchRecipeImmediate 1)
            (nativeMemoryState base)
            (nativeLaunchRecipeImmediate size)
            (nativeLaunchRecipeImmediate 0))
          nativePeerScratchSlot
          size
          b"independent-result"
          tail))))

def niRow =
  (lambda unrestricted slots : Nat .
    (lambda unrestricted system : (family IndependentStateSystem slots) .
      (lambda unrestricted owner : Nat .
        (stdListHeadOr
          (family StdList StdU64)
          (constructor StdList StdListEmpty StdU64)
          (stdListDrop (family StdList StdU64) owner (independentInitialValues slots system))))))

def niInitializeAt =
  (lambda unrestricted slots : Nat .
    (lambda unrestricted system : (family IndependentStateSystem slots) .
      (lambda unrestricted valuesAt : Nat .
        (lambda unrestricted owner : Nat .
          (lambda unrestricted tail : (family NativePhysicalCommands) .
            (stdListFold
              StdU64
              (pi unrestricted index : Nat . (family NativePhysicalCommands))
              (lambda unrestricted word : StdU64 .
                (lambda unrestricted next : (pi unrestricted index : Nat . (family NativePhysicalCommands)) .
                  (lambda unrestricted index : Nat .
                    (nativeMemoryStoreWord64
                      b"independent-initial"
                      (nativePointwiseAt valuesAt index)
                      (nativeLaunchRecipeImmediate (modelWord64Natural word))
                      (next (succ index))))))
              (lambda unrestricted index : Nat . tail)
              (niRow slots system owner)
              0))))))

def niInitialize =
  (lambda unrestricted slots : Nat .
    (lambda unrestricted system : (family IndependentStateSystem slots) .
      (lambda unrestricted layout : (family NativeIndependentLayout) .
        (niInitializeAt slots system (niValuesAt layout)))))

def niFinite =
  (lambda unrestricted base : Nat .
    (lambda unrestricted count : Nat .
      (lambda unrestricted tail : (family NativePhysicalCommands) .
        (stdListFold
          Nat
          (family NativePhysicalCommands)
          (lambda unrestricted index : Nat .
            (lambda unrestricted rest : (family NativePhysicalCommands) .
              (nativeFloat64RequireFinite
                (nativeMemoryLoad (nativePointwiseAt base index))
                nativePeerScratchSlot
                b"independent-state-nonfinite"
                rest)))
          tail
          (stdListNaturalsBelow count)))))

-- Version and cursor advance only after the target's step returns. These
-- address-based owners serve every topology (star and hierarchy).
def niAdvanceAt =
  (lambda unrestricted stateAt : Nat .
    (lambda unrestricted tail : (family NativePhysicalCommands) .
      (nativeCheckedWordAdd
        (nativeMemoryState stateAt)
        (nativeMemoryLoad stateAt)
        (nativeLaunchRecipeImmediate 1)
        nativePeerScratchSlot
        b"independent-version-overflow"
        (nativeCheckedWordAdd
          (nativeMemoryState (nativePointwiseAt stateAt 1))
          (nativeMemoryLoad (nativePointwiseAt stateAt 1))
          (nativeLaunchRecipeImmediate 1)
          nativePeerScratchSlot
          b"independent-cursor-overflow"
          tail))))

def niAdvance =
  (lambda unrestricted layout : (family NativeIndependentLayout) . (niAdvanceAt (niStateAt layout)))

-- The target owns the step's arithmetic and refusal. Logical position advances
-- only after that callback returns successfully; capture occurs after all steps.
def niRoundsAt =
  (lambda unrestricted stateAt : Nat .
    (lambda unrestricted steps : Nat .
      (lambda unrestricted step : (pi unrestricted tail : (family NativePhysicalCommands) . (family NativePhysicalCommands)) .
        (lambda unrestricted tail : (family NativePhysicalCommands) .
          (nativeLaunchRecipeCommand
            (constructor
              NativePhysicalOperation
              NativePhysicalRepeatBeginCounted
              (nativeLaunchRecipeImmediate steps))
            b"independent-repeat"
            (step
              (niAdvanceAt
                stateAt
                (nativeLaunchRecipeCommand
                  (constructor NativePhysicalOperation NativePhysicalRepeatEnd)
                  b"independent-repeat-end"
                  tail))))))))

def niRoundsWith =
  (lambda unrestricted layout : (family NativeIndependentLayout) . (niRoundsAt (niStateAt layout)))

def niRestore =
  (lambda unrestricted slots : Nat .
    (lambda unrestricted system : (family IndependentStateSystem slots) .
      (lambda unrestricted layout : (family NativeIndependentLayout) .
        (lambda unrestricted owner : Nat .
          (lambda unrestricted extent : Nat .
            (lambda unrestricted tail : (family NativePhysicalCommands) .
              (planNativeRegionRestore
                (niCheckpoint layout)
                (nativeRegionPathArgument (nativeRegionPathFirst (niPaths slots system)))
                (lambda unrestricted index : Nat .
                  (nativeRegionPathArgument
                    (naturalAdd (nativeRegionInputShardBase (niPaths slots system)) index)))
                nativePeerListenerSlot
                nativePeerScratchSlot
                extent
                (niDestinations slots system layout owner)
                (nativeMemoryCopyOperands
                  (nativeMemoryState (niStateAt layout))
                  (nativeMemoryState (nativeRegionCaptureAt (niCheckpoint layout)))
                  nativeRegionCaptureBytes
                  nativePeerScratchSlot
                  b"independent-restore-capture"
                  (nativeLaunchRecipeAssertEqual
                    (nativeMemoryLoad (niStateAt layout))
                    (nativeMemoryLoad (nativePointwiseAt (niStateAt layout) 1))
                    b"independent-input-position"
                    (nativeCheckedWordAdd
                      (nativeMemoryState (nativePointwiseAt (niStateAt layout) 2))
                      (nativeMemoryLoad (nativePointwiseAt (niStateAt layout) 2))
                      (nativeLaunchRecipeImmediate 1)
                      nativePeerScratchSlot
                      b"independent-epoch-overflow"
                      tail))))))))))

def niStart =
  (lambda unrestricted slots : Nat .
    (lambda unrestricted system : (family IndependentStateSystem slots) .
      (lambda unrestricted layout : (family NativeIndependentLayout) .
        (lambda unrestricted owner : Nat .
          (lambda unrestricted extent : Nat .
            (lambda unrestricted resume : Nat .
              (lambda unrestricted tail : (family NativePhysicalCommands) .
                (nat-eliminate
                  (lambda unrestricted mode : Nat .
                    (family
                      StdResult
                      (family NativeCheckpointFailure)
                      (family NativePhysicalCommands)))
                  (constructor
                    StdResult
                    StdSuccess
                    (family NativeCheckpointFailure)
                    (family NativePhysicalCommands)
                    (nativeMemoryStoreWord64
                      b"independent-version"
                      (niStateAt layout)
                      (nativeLaunchRecipeImmediate 0)
                      (nativeMemoryStoreWord64
                        b"independent-cursor"
                        (nativePointwiseAt (niStateAt layout) 1)
                        (nativeLaunchRecipeImmediate 0)
                        (nativeMemoryStoreWord64
                          b"independent-epoch"
                          (nativePointwiseAt (niStateAt layout) 2)
                          (nativeLaunchRecipeImmediate (nativeRegionEpoch (niCheckpoint layout)))
                          tail))))
                  (lambda unrestricted previous : Nat .
                    (lambda unrestricted ignored : (family StdResult (family NativeCheckpointFailure) (family NativePhysicalCommands)) .
                      (niRestore slots system layout owner extent tail)))
                  resume))))))))

def niProgramFor =
  (lambda unrestricted resultSlots : Nat .
    (lambda unrestricted extent : Nat .
      (lambda unrestricted commands : (family NativePhysicalCommands) .
        (nativePhysicalProgramFromCommands
          (bytes-append
            b"independent-state-native-v1"
            (dataBytesRepeatByte
              (byte 0)
              (naturalSaturatingSubtract 64 (bytes-length b"independent-state-native-v1"))))
          extent
          resultSlots
          commands))))

-- At least two owners: a single owner has no peer to publish with.
def niOwnersAdmitted =
  (lambda unrestricted slots : Nat .
    (lambda unrestricted system : (family IndependentStateSystem slots) .
      (naturalAnd
        (independentStateAdmitted slots system)
        (naturalLessOrEqual 2 (niOwners slots system)))))

def niRunAdmitted =
  (lambda unrestricted slots : Nat .
    (lambda unrestricted system : (family IndependentStateSystem slots) .
      (lambda unrestricted owner : Nat .
        (lambda unrestricted resume : Nat .
          (lambda unrestricted epoch : Nat .
            (lambda unrestricted steps : Nat .
              (naturalAnd
                (niOwnersAdmitted slots system)
                (naturalAnd
                  (naturalLess owner (niOwners slots system))
                  (naturalAnd
                    (naturalLessOrEqual resume 1)
                    (naturalAnd
                      (naturalNonzero epoch)
                      (naturalAnd
                        (naturalBelowTwoPower 64 (naturalAdd epoch resume))
                        (naturalBelowTwoPower 64 steps))))))))))))

-- Preparation follows initial-state/checkpoint validation. A target uploads
-- that state once, executes its own local steps, and captures its authoritative
-- values before publication. The publisher never observes stale host shadows.
def niCommandsWith =
  (lambda unrestricted slots : Nat .
    (lambda unrestricted system : (family IndependentStateSystem slots) .
      (lambda unrestricted layout : (family NativeIndependentLayout) .
        (lambda unrestricted owner : Nat .
          (lambda unrestricted edges : (family StdList (family NativePeerEdge)) .
            (lambda unrestricted resume : Nat .
              (lambda unrestricted steps : Nat .
                (lambda unrestricted extent : Nat .
                  (lambda unrestricted prepare : (pi unrestricted tail : (family NativePhysicalCommands) . (family NativePhysicalCommands)) .
                    (lambda unrestricted step : (pi unrestricted tail : (family NativePhysicalCommands) . (family NativePhysicalCommands)) .
                      (lambda unrestricted capture : (pi unrestricted tail : (family NativePhysicalCommands) . (family NativePhysicalCommands)) .
                        (lambda unrestricted finish : (pi unrestricted tail : (family NativePhysicalCommands) . (family NativePhysicalCommands)) .
                          (stdResultBind
                            (family NativeCheckpointFailure)
                            (family NativePhysicalCommands)
                            (family NativePhysicalCommands)
                            (planNativePeerRegionPublish
                              (niPublication slots system layout resume edges)
                              extent
                              owner
                              (nativePeerEdgesFold
                                edges
                                (lambda unrestricted index : Nat .
                                  (lambda unrestricted edge : (family NativePeerEdge) .
                                    (nativeSocketCloseChecked
                                      (nativeLaunchRecipeSlotValue
                                        (nativePeerEdgeConnectionSlot index))
                                      nativePeerScratchSlot)))
                                (niOutput
                                  (niStateAt layout)
                                  (niCaptureBytes slots system)
                                  (finish niHalt))))
                            (lambda unrestricted published : (family NativePhysicalCommands) .
                              (stdResultBind
                                (family NativeCheckpointFailure)
                                (family NativePhysicalCommands)
                                (family NativePhysicalCommands)
                                (niStart
                                  slots
                                  system
                                  layout
                                  owner
                                  extent
                                  resume
                                  (niFinite
                                    (niValuesAt layout)
                                    slots
                                    (nativePeerEdgeSetup
                                      owner
                                      edges
                                      (niEndpoint slots system layout)
                                      (prepare (niRoundsWith layout steps step (capture published))))))
                                (lambda unrestricted commands : (family NativePhysicalCommands) .
                                  (constructor
                                    StdResult
                                    StdSuccess
                                    (family NativeCheckpointFailure)
                                    (family NativePhysicalCommands)
                                    (niInitialize slots system layout owner commands))))))))))))))))))

def nativeIndependentArtifact =
  (lambda unrestricted target : (family NativeHostTarget) .
    (lambda unrestricted resources : (family NativeResourceContext) .
      (lambda unrestricted slots : Nat .
        (lambda unrestricted system : (family IndependentStateSystem slots) .
          (lambda unrestricted owner : Nat .
            (lambda unrestricted addresses : (family StdList Bytes) .
              (lambda unrestricted resume : Nat .
                (lambda unrestricted epoch : Nat .
                  (lambda unrestricted steps : Nat .
                    (lambda unrestricted available : Nat .
                      (let unrestricted edges =
                        (niEdges slots system owner addresses)
                        in
                        (niWithLayout
                          slots
                          system
                          epoch
                          0
                          (pointwiseProgramTemporaryValues
                            StdU64
                            slots
                            (independentAssignments slots system))
                          available
                          (lambda unrestricted layout : (family NativeIndependentLayout) .
                            (nat-eliminate
                              (lambda unrestricted valid : Nat . Bytes)
                              b""
                              (lambda unrestricted previous : Nat .
                                (lambda unrestricted ignored : Bytes .
                                  (eliminate
                                    StdResult
                                    (lambda unrestricted result : (family StdResult Bytes (family NativePhysicalCommands)) .
                                      Bytes)
                                    (planNativePointwiseProgram
                                      slots
                                      (independentAssignments slots system)
                                      (niValuesAt layout)
                                      (niEndpoint slots system layout)
                                      nativePeerScratchSlot
                                      niEnd)
                                    (branch StdFailure error . b"")
                                    (branch
                                      StdSuccess
                                      step
                                      .
                                      (eliminate
                                        StdResult
                                        (lambda unrestricted result : (family StdResult (family NativeCheckpointFailure) (family NativePhysicalCommands)) .
                                        Bytes)
                                        (niCommandsWith
                                        slots
                                        system
                                        layout
                                        owner
                                        edges
                                        resume
                                        steps
                                        (niExtent slots system layout edges)
                                        (lambda unrestricted tail : (family NativePhysicalCommands) .
                                        tail)
                                        (nativePhysicalProgramComposeCommandsAppend step)
                                        (lambda unrestricted tail : (family NativePhysicalCommands) .
                                        tail)
                                        (lambda unrestricted tail : (family NativePhysicalCommands) .
                                        tail))
                                        (branch StdFailure error . b"")
                                        (branch
                                        StdSuccess
                                        commands
                                        .
                                        (nativeHostTargetResourceArtifact
                                        target
                                        resources
                                        (niProgramFor
                                        (nativePeerEdgeSlots edges)
                                        (niExtent slots system layout edges)
                                        commands))))))))
                              (naturalAnd
                                (niRunAdmitted slots system owner resume epoch steps)
                                (naturalAnd
                                  (niEdgesAdmitted slots system owner addresses)
                                  (naturalLessOrEqual
                                    (niExtent slots system layout edges)
                                    available)))))))))))))))))

-- Evaluation restores the joined logical state through the same checkpoint
-- owner. A target evaluates and captures before the public result is written.
def niEvaluationCommands =
  (lambda unrestricted paths : (family NativeRegionPaths) .
    (lambda unrestricted width : Nat .
      (lambda unrestricted checkpoint : (family NativeRegionCheckpoint) .
        (lambda unrestricted base : Nat .
          (lambda unrestricted extent : Nat .
            (lambda unrestricted prepare : (pi unrestricted tail : (family NativePhysicalCommands) . (family NativePhysicalCommands)) .
              (lambda unrestricted evaluate : (pi unrestricted tail : (family NativePhysicalCommands) . (family NativePhysicalCommands)) .
                (lambda unrestricted capture : (pi unrestricted tail : (family NativePhysicalCommands) . (family NativePhysicalCommands)) .
                  (lambda unrestricted finish : (pi unrestricted tail : (family NativePhysicalCommands) . (family NativePhysicalCommands)) .
                    (planNativeRegionRestore
                      checkpoint
                      (nativeRegionPathArgument (nativeRegionPathFirst paths))
                      (lambda unrestricted index : Nat .
                        (nativeRegionPathArgument
                          (naturalAdd (nativeRegionInputShardBase paths) index)))
                      nativePeerListenerSlot
                      nativePeerScratchSlot
                      extent
                      (constructor
                        StdList
                        StdListCons
                        (family NativeRegionDestination)
                        (constructor
                          NativeRegionDestination
                          NativeRegionDestinationOf
                          0
                          (constructor
                            LogicalInterval
                            LogicalIntervalOf
                            0
                            (nativePointwiseAt 0 width))
                          base)
                        (constructor StdList StdListEmpty (family NativeRegionDestination)))
                      (nativeLaunchRecipeAssertEqual
                        (nativeMemoryLoad (nativeRegionCaptureAt checkpoint))
                        (nativeMemoryLoad (nativePointwiseAt (nativeRegionCaptureAt checkpoint) 1))
                        b"independent-input-position"
                        (niFinite
                          base
                          width
                          (prepare
                            (evaluate
                              (capture (niOutput base nativePointwiseWordBytes (finish niHalt)))))))))))))))))

def nativeIndependentEvaluation =
  (lambda unrestricted target : (family NativeHostTarget) .
    (lambda unrestricted resources : (family NativeResourceContext) .
      (lambda unrestricted slots : Nat .
        (lambda unrestricted system : (family IndependentStateSystem slots) .
          (lambda unrestricted epoch : Nat .
            (lambda unrestricted program : (family StdList (family PointwiseAssignment StdU64 (naturalMultiply (niOwners slots system) (independentPersistentCount slots system)))) .
              (lambda unrestricted available : Nat .
                (eliminate
                  StdResult
                  (lambda unrestricted result : (family StdResult (family NativeCheckpointFailure) (family NativeRegionCheckpoint)) .
                    Bytes)
                  (planNativeRegionCheckpoint
                    (niContext slots system)
                    (niRegions slots system)
                    (niPartitions slots system)
                    epoch
                    0
                    available
                    (niOwners slots system))
                  (branch StdFailure error . b"")
                  (branch
                    StdSuccess
                    checkpoint
                    .
                    (let unrestricted width =
                      (naturalMultiply
                        (niOwners slots system)
                        (independentPersistentCount slots system))
                      in
                      (let unrestricted base =
                        (nativeRegionEnd checkpoint)
                        in
                        (let unrestricted extent =
                          (nativePointwiseExtent width program base)
                          in
                          (nat-eliminate
                            (lambda unrestricted valid : Nat . Bytes)
                            b""
                            (lambda unrestricted previous : Nat .
                              (lambda unrestricted ignored : Bytes .
                                (eliminate
                                  StdResult
                                  (lambda unrestricted result : (family StdResult Bytes (family NativePhysicalCommands)) .
                                    Bytes)
                                  (planNativePointwiseProgram
                                    width
                                    program
                                    base
                                    extent
                                    nativePeerScratchSlot
                                    niEnd)
                                  (branch StdFailure error . b"")
                                  (branch
                                    StdSuccess
                                    evaluated
                                    .
                                    (eliminate
                                      StdResult
                                      (lambda unrestricted result : (family StdResult (family NativeCheckpointFailure) (family NativePhysicalCommands)) .
                                        Bytes)
                                      (niEvaluationCommands
                                        (niPaths slots system)
                                        width
                                        checkpoint
                                        base
                                        extent
                                        (lambda unrestricted tail : (family NativePhysicalCommands) .
                                        tail)
                                        (nativePhysicalProgramComposeCommandsAppend evaluated)
                                        (lambda unrestricted tail : (family NativePhysicalCommands) .
                                        tail)
                                        (lambda unrestricted tail : (family NativePhysicalCommands) .
                                        tail))
                                      (branch StdFailure error . b"")
                                      (branch
                                        StdSuccess
                                        commands
                                        .
                                        (nativeHostTargetResourceArtifact
                                        target
                                        resources
                                        (niProgramFor nativePeerEndpointSlots extent commands))))))))
                            (naturalAnd
                              (independentStateAdmitted slots system)
                              (naturalAnd
                                (niOwnersAdmitted slots system)
                                (naturalLessOrEqual extent available))))))))))))))))