module Runtime.NativeHostTarget

import Runtime.NativePhysicalProgram
import Runtime.NativePhysicalNativeELF
import Runtime.NativeResourcePlan
import Data.Bytes

-- A native host executable target: the instruction set, Linux ABI and
-- physical-command interpreter that turn one target-neutral
-- NativePhysicalProgram into a self-contained executable.
--
-- Shared execution owners (learners, protocols, checkpoint publication)
-- derive the program once from the system; the pairing chooses the target.
-- This is what lets participants of one learning system run on different
-- host architectures: their programs come from the same derivation, and the
-- bytes they exchange and publish are defined by that program, not by the
-- target (the wire and checkpoint encodings are little-endian, fixed-width
-- and identical on every admitted host).
--
-- A target that cannot realize some command refuses the whole program by
-- returning empty bytes, which the compiler's ELF writer rejects. No
-- executable mixes instruction sets, and nothing is silently dropped or run
-- through another target. New targets are instances beside their platform
-- owners (Platform.AArch64.HostTarget), never a branch in this module.
family NativeHostTarget : Type 0
constructor NativeHostTargetOf
field unrestricted nativeHostTargetEmit : (pi unrestricted program : (family NativePhysicalProgram) . Bytes)

end-family

def nativeHostTargetProgramBytes =
  (lambda unrestricted target : (family NativeHostTarget) .
    (lambda unrestricted program : (family NativePhysicalProgram) .
      (eliminate
        NativeHostTarget
        (lambda unrestricted current : (family NativeHostTarget) . Bytes)
        target
        (branch NativeHostTargetOf emit . (emit program)))))

-- Linux x86-64: the native runtime and image of Runtime.NativePhysicalNativeELF.
def nativeHostTargetX86_64Linux : (family NativeHostTarget) =
  (constructor NativeHostTarget NativeHostTargetOf nativePhysicalGenerateNativeELFBytesDirect)

-- Deployment capacity admission precedes emission on every target. The
-- program remains the only source of state, result-slot and scratch sizes;
-- the caller cannot substitute a smaller declared interpreter allocation.
def nativeHostTargetResourceArtifact =
  (lambda unrestricted target : (family NativeHostTarget) .
    (lambda unrestricted resources : (family NativeResourceContext) .
      (lambda unrestricted program : (family NativePhysicalProgram) .
        (nat-eliminate
          (lambda unrestricted valid : Nat . Bytes)
          b""
          (lambda unrestricted prior : Nat .
            (lambda unrestricted ignored : Bytes . (nativeHostTargetProgramBytes target program)))
          (nativePhysicalResourcesAdmitted resources program)))))