Runtime.NativePhysicalImagePlan

1module Runtime.NativePhysicalImagePlan
2
3import Runtime.NativePhysicalProgram
4import Std.Natural
5
6-- Wire layout is a compiler decision, separate from the host command semantics.
7-- Both formats have a 176-byte header.  A record is eight header words, its
8-- operand slots (24 bytes each, at most seven), then payload, auxiliary bytes
9-- and error identity.
10--
11-- V4 (ALPXPHY4 / 4, the x86-64 host) is compact: a record stores its operand
12-- slots only up to the last one that is not the zero immediate, and header
13-- word 7 holds the bytes it omitted (0, 24, ..., 168).  A slot it does not
14-- store reads as the zero immediate, so trimming never changes a value:
15--   recordExtent = 232 - omitted + payloadExtent + auxiliaryExtent + errorExtent
16-- and the payload begins at byte 232 - omitted.
17--
18-- V3 (ALPXPHY3 / 3, AArch64) stores all seven slots (word 7 is 0) and adds
19-- zero padding AFTER the error identity so inline machine routines can execute
20-- on an ISA with aligned instruction fetch:
21--   recordExtent = roundUp(232 + payloadExtent + auxiliaryExtent + errorExtent, 4)
22-- The image base must itself be aligned. Compiler.ELF plus the AArch64 assembler
23-- establish this for the maintained host.
24--
25-- In both, the three content extents retain their exact meaning; padding is
26-- never a syscall payload, copied data, telemetry field or diagnostic
27-- identity. The reader checks the extent before dispatch and advances by it.
28--
29-- Shared routine code (both formats): a machine routine whose code repeats an
30-- earlier routine's exactly, and which passes no operand into its own payload,
31-- stores a one-instruction branch to that earlier code instead of a copy (x86
32-- jmp rel32, AArch64 B).  The interpreter calls it like any routine; the branch
33-- reaches the same code with the same registers and return address.
34-- V4 readers must reject V3 and vice versa.
35family NativePhysicalImageFormat : Type 0
36constructor NativePhysicalImageCompactV4
37constructor NativePhysicalImageAlignedV3
38end-family
39
40-- A packed image: the x86-64 host's V4 image, compressed by the compiler and
41-- unpacked once by the interpreter (Runtime.NativePhysicalNative) when the
42-- executable starts. Container: magic ALPXLZ01, version 1 (u64), unpacked
43-- length (u64), packed length (u64), then LZ sequences. A sequence is a token
44-- (high nibble: literal count; low nibble: match length minus 4; either nibble
45-- 15 continues in bytes of 255 and a final remainder), the literals, a 16-bit
46-- little-endian distance 1 .. 65535 back into the bytes already produced, and
47-- the match length's continuation; matches may overlap their own output, and
48-- the last sequence carries literals only. The interpreter unpacks into the
49-- pages after the file's last page, which the executable's load segment
50-- reserves (Compiler.ELF), writable while it writes them and read+execute
51-- before anything in them runs. It refuses (exit 109) a wrong version, a
52-- literal or match past the stream or past the declared length, a distance
53-- reaching before the output, and an output that is not exactly the declared
54-- length. The unpacked image is byte-identical to the V4 image, so execution
55-- is unchanged; only its bytes on disk are compressed.
56family NativePhysicalPackedImage : Type 0
57constructor NativePhysicalPackedImageOf
58field unrestricted nativePhysicalPackedImageProgram : (family NativePhysicalProgram)
59end-family
60
61family NativePhysicalImagePlan : Type 0
62constructor NativePhysicalImagePlanValue
63field unrestricted nativePhysicalImagePlanFormat : (family NativePhysicalImageFormat)
64field unrestricted nativePhysicalImagePlanProgram : (family NativePhysicalProgram)
65end-family
66
67def nativePhysicalImageAlignedExtent =
68  (lambda unrestricted extent : Nat .
69    (naturalMultiply (naturalDivideUnchecked (naturalAdd extent 3) 4) 4))