module Runtime.NativePhysicalImagePlan

import Runtime.NativePhysicalProgram
import Std.Natural

-- Wire layout is a compiler decision, separate from the host command semantics.
-- V2 preserves the packed x86 image. V3 aligns every record to four bytes so
-- inline machine routines can execute on an ISA with aligned instruction fetch.
-- Both have a 176-byte header and 232-byte fixed record. V3 changes magic and
-- version to ALPXPHY3 / 3 and adds zero padding AFTER the error identity:
--   recordExtent = roundUp(232 + payloadExtent + auxiliaryExtent + errorExtent, 4)
-- The three content extents retain their exact meaning; padding is never a
-- syscall payload, copied data, telemetry field or diagnostic identity. The
-- reader checks the rounded extent before dispatch and advances by that extent.
-- The image base must itself be aligned. Compiler.ELF plus the AArch64 assembler
-- establish this for the maintained host. V2 readers must reject V3 and vice versa.
family NativePhysicalImageFormat : Type 0
constructor NativePhysicalImagePackedV2
constructor NativePhysicalImageAlignedV3
end-family

family NativePhysicalImagePlan : Type 0
constructor NativePhysicalImagePlanValue
field unrestricted nativePhysicalImagePlanFormat : (family NativePhysicalImageFormat)
field unrestricted nativePhysicalImagePlanProgram : (family NativePhysicalProgram)
end-family

def nativePhysicalImageAlignedExtent =
  (lambda unrestricted extent : Nat .
    (naturalMultiply (naturalDivideUnchecked (naturalAdd extent 3) 4) 4))