Runtime.NativeHostTarget

1module Runtime.NativeHostTarget
2
3import Runtime.NativePhysicalProgram
4import Runtime.NativePhysicalNativeELF
5import Runtime.NativeResourcePlan
6import Data.Bytes
7
8-- A native host executable target: the instruction set, Linux ABI and
9-- physical-command interpreter that turn one target-neutral
10-- NativePhysicalProgram into a self-contained executable.
11--
12-- Shared execution owners (learners, protocols, checkpoint publication)
13-- derive the program once from the system; the pairing chooses the target.
14-- This is what lets participants of one learning system run on different
15-- host architectures: their programs come from the same derivation, and the
16-- bytes they exchange and publish are defined by that program, not by the
17-- target (the wire and checkpoint encodings are little-endian, fixed-width
18-- and identical on every admitted host).
19--
20-- A target that cannot realize some command refuses the whole program by
21-- returning empty bytes, which the compiler's ELF writer rejects. No
22-- executable mixes instruction sets, and nothing is silently dropped or run
23-- through another target. New targets are instances beside their platform
24-- owners (Platform.AArch64.HostTarget), never a branch in this module.
25family NativeHostTarget : Type 0
26constructor NativeHostTargetOf
27field unrestricted nativeHostTargetEmit : (pi unrestricted program : (family NativePhysicalProgram) . Bytes)
28
29end-family
30
31def nativeHostTargetProgramBytes =
32  (lambda unrestricted target : (family NativeHostTarget) .
33    (lambda unrestricted program : (family NativePhysicalProgram) .
34      (eliminate
35        NativeHostTarget
36        (lambda unrestricted current : (family NativeHostTarget) . Bytes)
37        target
38        (branch NativeHostTargetOf emit . (emit program)))))
39
40-- Linux x86-64: the native runtime and image of Runtime.NativePhysicalNativeELF.
41def nativeHostTargetX86_64Linux : (family NativeHostTarget) =
42  (constructor NativeHostTarget NativeHostTargetOf nativePhysicalGenerateNativeELFBytesDirect)
43
44-- Deployment capacity admission precedes emission on every target. The
45-- program remains the only source of state, result-slot and scratch sizes;
46-- the caller cannot substitute a smaller declared interpreter allocation.
47def nativeHostTargetResourceArtifact =
48  (lambda unrestricted target : (family NativeHostTarget) .
49    (lambda unrestricted resources : (family NativeResourceContext) .
50      (lambda unrestricted program : (family NativePhysicalProgram) .
51        (nat-eliminate
52          (lambda unrestricted valid : Nat . Bytes)
53          b""
54          (lambda unrestricted prior : Nat .
55            (lambda unrestricted ignored : Bytes . (nativeHostTargetProgramBytes target program)))
56          (nativePhysicalResourcesAdmitted resources program)))))