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-- V2 preserves the packed x86 image. V3 aligns every record to four bytes so
8-- inline machine routines can execute on an ISA with aligned instruction fetch.
9-- Both have a 176-byte header and 232-byte fixed record. V3 changes magic and
10-- version to ALPXPHY3 / 3 and adds zero padding AFTER the error identity:
11--   recordExtent = roundUp(232 + payloadExtent + auxiliaryExtent + errorExtent, 4)
12-- The three content extents retain their exact meaning; padding is never a
13-- syscall payload, copied data, telemetry field or diagnostic identity. The
14-- reader checks the rounded extent before dispatch and advances by that extent.
15-- The image base must itself be aligned. Compiler.ELF plus the AArch64 assembler
16-- establish this for the maintained host. V2 readers must reject V3 and vice versa.
17family NativePhysicalImageFormat : Type 0
18constructor NativePhysicalImagePackedV2
19constructor NativePhysicalImageAlignedV3
20end-family
21
22family NativePhysicalImagePlan : Type 0
23constructor NativePhysicalImagePlanValue
24field unrestricted nativePhysicalImagePlanFormat : (family NativePhysicalImageFormat)
25field unrestricted nativePhysicalImagePlanProgram : (family NativePhysicalProgram)
26end-family
27
28def nativePhysicalImageAlignedExtent =
29  (lambda unrestricted extent : Nat .
30    (naturalMultiply (naturalDivideUnchecked (naturalAdd extent 3) 4) 4))