module Platform.AArch64.NativePhysicalRuntime

import Runtime.NativePhysicalImage
import Runtime.NativePhysicalMemory
import Compiler.MachineAArch64
import Compiler.MachineAArch64Assembly
import Data.Bytes
import Model.Config
import Model.Word32
import Std.Byte
import Std.Natural

-- The AArch64 Linux twin of Runtime.NativePhysicalNative: one fixed program
-- that interprets an ALPXPHY3 command image appended after its code. The V3
-- layout aligns every record; see Runtime.NativePhysicalImagePlan. V2's packed
-- records can put an inline routine at an unaligned instruction address even
-- when syscall payloads are padded. This reader explicitly rejects that format.
-- Block for block it is the x86-64 runtime, under this register map:
--
--   x86-64          A64    role
--   RAX             x6     accumulator, resolver result
--   RDI RSI RDX     x0 x1 x2   system-call arguments 0-2
--   RCX/R10 R8 R9   x3 x4 x5   system-call arguments 3-5 (x86 moves RCX to R10; A64 needs no move)
--   R10 R11         x9 x10 temporaries
--   R12 R13 R14 R15 x12 x13 x14 x15   image end, remaining commands, command pointer, image base
--   RBX RBP         x19 x20 result-slot base, mapped state base
--   -               x21    the process entry stack pointer (argc, argv)
--   -               x11    the resolver's address, for blr
--   [rsp-248/-240/-232]    [sp,#8] [sp,#16] [sp,#24] in a derived aligned frame
--
-- The system-call number travels in x8 and the result returns in x0; the
-- runtime's own calls use the asm-generic numbers (mmap 222, openat 56,
-- write 64, fsync 82, close 57, munmap 215, exit_group 94, exit 93).  The
-- numbers a program's commands carry are the program's data, so an A64
-- program supplies A64 numbers.  Calls into the resolver and into machine
-- routines use blr/ret through x30; the runtime itself never returns.
def nprtX0 : (family AArch64Register) =
  (constructor AArch64Register AArch64X0)

def nprtX1 : (family AArch64Register) =
  (constructor AArch64Register AArch64X1)

def nprtX2 : (family AArch64Register) =
  (constructor AArch64Register AArch64X2)

def nprtX3 : (family AArch64Register) =
  (constructor AArch64Register AArch64X3)

def nprtX4 : (family AArch64Register) =
  (constructor AArch64Register AArch64X4)

def nprtX5 : (family AArch64Register) =
  (constructor AArch64Register AArch64X5)

def nprtX6 : (family AArch64Register) =
  (constructor AArch64Register AArch64X6)

def nprtX7 : (family AArch64Register) =
  (constructor AArch64Register AArch64X7)

def nprtX8 : (family AArch64Register) =
  (constructor AArch64Register AArch64X8)

def nprtX9 : (family AArch64Register) =
  (constructor AArch64Register AArch64X9)

def nprtX10 : (family AArch64Register) =
  (constructor AArch64Register AArch64X10)

def nprtX11 : (family AArch64Register) =
  (constructor AArch64Register AArch64X11)

def nprtX12 : (family AArch64Register) =
  (constructor AArch64Register AArch64X12)

def nprtX13 : (family AArch64Register) =
  (constructor AArch64Register AArch64X13)

def nprtX14 : (family AArch64Register) =
  (constructor AArch64Register AArch64X14)

def nprtX15 : (family AArch64Register) =
  (constructor AArch64Register AArch64X15)

def nprtX19 : (family AArch64Register) =
  (constructor AArch64Register AArch64X19)

def nprtX20 : (family AArch64Register) =
  (constructor AArch64Register AArch64X20)

def nprtX21 : (family AArch64Register) =
  (constructor AArch64Register AArch64X21)

def nprtShift0 : (family AArch64HalfwordShift) =
  (constructor AArch64HalfwordShift AArch64Shift0)

def nprtEqual : (family AArch64Condition) =
  (constructor AArch64Condition AArch64Equal)

def nprtNotEqual : (family AArch64Condition) =
  (constructor AArch64Condition AArch64NotEqual)

def nprtMinus : (family AArch64Condition) =
  (constructor AArch64Condition AArch64Minus)

def nprtBelow : (family AArch64Condition) =
  (constructor AArch64Condition AArch64CarryClear)

def nprtAbove : (family AArch64Condition) =
  (constructor AArch64Condition AArch64UnsignedHigher)

-- Frame slots standing in for the x86 runtime's [rsp-248], [rsp-240], [rsp-232].
def nprtSlotA : Nat =
  8

def nprtSlotB : Nat =
  16

def nprtSlotC : Nat =
  24

-- x12-x15 carry live VM state but are volatile in AAPCS64. Save them at
-- the caller boundary around every user routine. Depending on an incidental
-- routine register allocation corrupts the image cursor after a legal call.
-- These slots follow the existing temporary slots in the VM's private frame.
def nprtStackWordBytes =
  (bytes-length (nativePhysicalImageWord64Bytes nativePhysicalImageZeroWord64))

def nprtSaveImageEnd =
  (naturalAdd nprtSlotC nprtStackWordBytes)

def nprtSaveRemaining =
  (naturalAdd nprtSaveImageEnd nprtStackWordBytes)

def nprtSaveCommand =
  (naturalAdd nprtSaveRemaining nprtStackWordBytes)

def nprtSaveImage =
  (naturalAdd nprtSaveCommand nprtStackWordBytes)

def nprtStackBytes =
  (naturalMultiply
    16
    (naturalDivideUnchecked (naturalAdd 15 (naturalAdd nprtSaveImage nprtStackWordBytes)) 16))

-- Labels.
def nprtLabelEntry : Bytes =
  b"np-entry"

def nprtLabelLoop : Bytes =
  b"np-loop"

def nprtLabelDone : Bytes =
  b"np-done"

def nprtLabelAdvance : Bytes =
  b"np-advance"

def nprtLabelResolve : Bytes =
  b"np-resolve"

def nprtLabelResolveImmediate : Bytes =
  b"np-res-imm"

def nprtLabelResolveResult : Bytes =
  b"np-res-res"

def nprtLabelResolveResultAddress : Bytes =
  b"np-res-raddr"

def nprtLabelResolveStateAddress : Bytes =
  b"np-res-saddr"

def nprtLabelResolveStateLoad : Bytes =
  b"np-res-sload"

def nprtLabelResolvePayloadAddress : Bytes =
  b"np-res-paddr"

def nprtLabelResolvePayloadLoad : Bytes =
  b"np-res-pload"

def nprtLabelResolveProcessArgument : Bytes =
  b"np-res-argv"

def nprtLabelResolveSlotValid : Bytes =
  b"np-res-sv"

def nprtLabelResolveResultAddressSlotValid : Bytes =
  b"np-res-rasv"

def nprtLabelResolveStateAddressValid : Bytes =
  b"np-res-sav"

def nprtLabelResolveStateLoadValid : Bytes =
  b"np-res-slv"

def nprtLabelResolvePayloadAddressValid : Bytes =
  b"np-res-pav"

def nprtLabelResolvePayloadLoadValid : Bytes =
  b"np-res-plv"

def nprtLabelDispatchSystemCall : Bytes =
  b"np-syscall"

def nprtLabelDispatchCopy : Bytes =
  b"np-copy"

def nprtLabelDispatchRoutine : Bytes =
  b"np-routine"

def nprtLabelDispatchFence : Bytes =
  b"np-fence"

def nprtLabelDispatchTelemetry : Bytes =
  b"np-telemetry"

def nprtLabelDispatchAssert : Bytes =
  b"np-assert"

def nprtLabelDispatchAssertOneOf : Bytes =
  b"np-assert-one"

def nprtLabelDispatchHalt : Bytes =
  b"np-halt"

def nprtLabelBindResult : Bytes =
  b"np-bind"

def nprtLabelBindStore : Bytes =
  b"np-bind-s"

def nprtLabelBindSlotValid : Bytes =
  b"np-bind-sv"

def nprtLabelCopyLoop : Bytes =
  b"np-copy-l"

def nprtLabelCopyDone : Bytes =
  b"np-copy-d"

def nprtLabelFenceLoop : Bytes =
  b"np-fence-l"

def nprtLabelFenceDone : Bytes =
  b"np-fence-d"

def nprtLabelTelemetryCopyLoop : Bytes =
  b"np-tel-cl"

def nprtLabelTelemetryWriteLoop : Bytes =
  b"np-tel-wl"

def nprtLabelRecordExtentValid : Bytes =
  b"np-rec-ev"

def nprtLabelRecordEndValid : Bytes =
  b"np-rec-bv"

def nprtLabelFatalFormat : Bytes =
  b"np-fatal-format"

def nprtLabelFatalBounds : Bytes =
  b"np-fatal-bounds"

def nprtLabelFatalOperand : Bytes =
  b"np-fatal-operand"

def nprtLabelFatalSystemCall : Bytes =
  b"np-fatal-syscall"

def nprtLabelFatalAssertion : Bytes =
  b"np-fatal-assert"

def nprtLabelFatalFence : Bytes =
  b"np-fatal-fence"

def nprtLabelFatalTelemetry : Bytes =
  b"np-fatal-tel"

def nprtLabelFatalRecord : Bytes =
  b"np-fatal-record"

def nprtLabelCommandFailure : Bytes =
  b"np-command-fail"

def nprtLabelExit : Bytes =
  b"np-exit"

def nprtLabelImage : Bytes =
  b"np-image"

-- Assembly item builders.
def nprtEmit =
  (lambda unrestricted instruction : (family AArch64Instruction) .
    (lambda unrestricted tail : (family AArch64Assembly) .
      (constructor AArch64Assembly AArch64AssemblyEmit instruction tail)))

def nprtLabel =
  (lambda unrestricted name : Bytes .
    (lambda unrestricted tail : (family AArch64Assembly) .
      (constructor AArch64Assembly AArch64AssemblyLabel name tail)))

def nprtB =
  (lambda unrestricted target : Bytes .
    (lambda unrestricted tail : (family AArch64Assembly) .
      (constructor AArch64Assembly AArch64AssemblyBranch target tail)))

def nprtBIf =
  (lambda unrestricted condition : (family AArch64Condition) .
    (lambda unrestricted target : Bytes .
      (lambda unrestricted tail : (family AArch64Assembly) .
        (constructor AArch64Assembly AArch64AssemblyBranchIf condition target tail))))

def nprtAdr =
  (lambda unrestricted destination : (family AArch64Register) .
    (lambda unrestricted target : Bytes .
      (lambda unrestricted tail : (family AArch64Assembly) .
        (constructor AArch64Assembly AArch64AssemblyAddressOf destination target tail))))

-- Instructions.  `nprtCompare a b` is the x86 runtime's `Compare a b`, which
-- computes b - a: on A64 that is `cmp b, a`, so Below means b < a unsigned.
def nprtMovz =
  (lambda unrestricted destination : (family AArch64Register) .
    (lambda unrestricted value : Nat .
      (constructor AArch64Instruction AArch64MoveWideZero destination value nprtShift0)))

def nprtMov =
  (lambda unrestricted destination : (family AArch64Register) .
    (lambda unrestricted source : (family AArch64Register) .
      (constructor AArch64Instruction AArch64MoveRegister destination source)))

def nprtAdd =
  (lambda unrestricted destination : (family AArch64Register) .
    (lambda unrestricted source : (family AArch64Register) .
      (constructor AArch64Instruction AArch64AddRegister destination destination source)))

def nprtSub =
  (lambda unrestricted destination : (family AArch64Register) .
    (lambda unrestricted source : (family AArch64Register) .
      (constructor AArch64Instruction AArch64SubtractRegister destination destination source)))

def nprtAddImm =
  (lambda unrestricted destination : (family AArch64Register) .
    (lambda unrestricted value : Nat .
      (constructor AArch64Instruction AArch64AddImmediate destination destination value)))

def nprtSubImm =
  (lambda unrestricted destination : (family AArch64Register) .
    (lambda unrestricted value : Nat .
      (constructor AArch64Instruction AArch64SubtractImmediate destination destination value)))

def nprtCompare =
  (lambda unrestricted a : (family AArch64Register) .
    (lambda unrestricted b : (family AArch64Register) .
      (constructor AArch64Instruction AArch64CompareRegister b a)))

def nprtCmpImm =
  (lambda unrestricted register : (family AArch64Register) .
    (lambda unrestricted value : Nat .
      (constructor AArch64Instruction AArch64CompareImmediate register value)))

def nprtTest =
  (lambda unrestricted register : (family AArch64Register) .
    (constructor AArch64Instruction AArch64CompareImmediate register 0))

def nprtLsl =
  (lambda unrestricted register : (family AArch64Register) .
    (lambda unrestricted amount : Nat .
      (constructor AArch64Instruction AArch64ShiftLeftImmediate register register amount)))

def nprtLdr =
  (lambda unrestricted destination : (family AArch64Register) .
    (lambda unrestricted base : (family AArch64Register) .
      (lambda unrestricted offset : Nat .
        (constructor AArch64Instruction AArch64LoadMemory64 destination base offset))))

def nprtStr =
  (lambda unrestricted base : (family AArch64Register) .
    (lambda unrestricted offset : Nat .
      (lambda unrestricted source : (family AArch64Register) .
        (constructor AArch64Instruction AArch64StoreMemory64 base offset source))))

def nprtLdrb =
  (lambda unrestricted destination : (family AArch64Register) .
    (lambda unrestricted base : (family AArch64Register) .
      (constructor AArch64Instruction AArch64LoadMemory8ZeroExtend destination base 0)))

def nprtStrb =
  (lambda unrestricted base : (family AArch64Register) .
    (lambda unrestricted source : (family AArch64Register) .
      (constructor AArch64Instruction AArch64StoreMemory8 base 0 source)))

def nprtLdrSlot =
  (lambda unrestricted destination : (family AArch64Register) .
    (lambda unrestricted slot : Nat .
      (constructor AArch64Instruction AArch64LoadMemory64FromStack destination slot)))

def nprtStrSlot =
  (lambda unrestricted slot : Nat .
    (lambda unrestricted source : (family AArch64Register) .
      (constructor AArch64Instruction AArch64StoreMemory64ToStack slot source)))

def nprtSvc : (family AArch64Instruction) =
  (constructor AArch64Instruction AArch64SupervisorCall)

def nprtRet : (family AArch64Instruction) =
  (constructor AArch64Instruction AArch64Return)

def nprtBlr =
  (lambda unrestricted target : (family AArch64Register) .
    (constructor AArch64Instruction AArch64BranchLinkRegister target))

-- A 64-bit constant from eight little-endian bytes: movz then three movk.
def nprtHalf =
  (lambda unrestricted low : Byte .
    (lambda unrestricted high : Byte .
      (naturalAdd (byte-to-nat low) (naturalMultiply 256 (byte-to-nat high)))))

def nprtMovImm64 =
  (lambda unrestricted destination : (family AArch64Register) .
    (lambda unrestricted b0 : Byte .
      (lambda unrestricted b1 : Byte .
        (lambda unrestricted b2 : Byte .
          (lambda unrestricted b3 : Byte .
            (lambda unrestricted b4 : Byte .
              (lambda unrestricted b5 : Byte .
                (lambda unrestricted b6 : Byte .
                  (lambda unrestricted b7 : Byte .
                    (lambda unrestricted tail : (family AArch64Assembly) .
                      (nprtEmit
                        (constructor
                          AArch64Instruction
                          AArch64MoveWideZero
                          destination
                          (nprtHalf b0 b1)
                          nprtShift0)
                        (nprtEmit
                          (constructor
                            AArch64Instruction
                            AArch64MoveWideKeep
                            destination
                            (nprtHalf b2 b3)
                            (constructor AArch64HalfwordShift AArch64Shift16))
                          (nprtEmit
                            (constructor
                              AArch64Instruction
                              AArch64MoveWideKeep
                              destination
                              (nprtHalf b4 b5)
                              (constructor AArch64HalfwordShift AArch64Shift32))
                            (nprtEmit
                              (constructor
                                AArch64Instruction
                                AArch64MoveWideKeep
                                destination
                                (nprtHalf b6 b7)
                                (constructor AArch64HalfwordShift AArch64Shift48))
                              tail))))))))))))))

def nprtMovNegativeOne =
  (lambda unrestricted destination : (family AArch64Register) .
    (lambda unrestricted tail : (family AArch64Assembly) .
      (nprtMovImm64
        destination
        (byte 255)
        (byte 255)
        (byte 255)
        (byte 255)
        (byte 255)
        (byte 255)
        (byte 255)
        (byte 255)
        tail)))

-- The system call with the given asm-generic number: movz x8, svc.
def nprtSyscall =
  (lambda unrestricted number : Nat .
    (lambda unrestricted tail : (family AArch64Assembly) .
      (nprtEmit (nprtMovz nprtX8 number) (nprtEmit nprtSvc tail))))

-- Resolve the operand descriptor at [x14 + offset] into a register:
-- x0 = x14 + offset ; adr x11, resolve ; blr x11 ; mov dest, x6.
def nprtResolveCall =
  (lambda unrestricted descriptorOffset : Nat .
    (lambda unrestricted destination : (family AArch64Register) .
      (lambda unrestricted tail : (family AArch64Assembly) .
        (nprtEmit
          (nprtMov nprtX0 nprtX14)
          (nprtEmit
            (nprtAddImm nprtX0 descriptorOffset)
            (nprtAdr
              nprtX11
              nprtLabelResolve
              (nprtEmit (nprtBlr nprtX11) (nprtEmit (nprtMov destination nprtX6) tail))))))))

-- Exit with the code in x0.
def nprtExitWith =
  (lambda unrestricted code : Nat .
    (lambda unrestricted tail : (family AArch64Assembly) .
      (nprtEmit (nprtMovz nprtX0 code) (nprtB nprtLabelExit tail))))

-- ---------------------------------------------------------------------------
-- The commands Runtime.NativePhysicalNative gained after this twin was
-- written (Repeat, StoreWord64, the LoopAffine operand, FenceWait, AddWord64
-- and the Float64 family), block for block under the same register map.  The
-- resolver scratches x6, x9 and x10 and reads x0, and `svc` returns in x0, so
-- x1 .. x5 carry values across a resolve and a system call.
def nprtLabelDispatchSkip : Bytes =
  b"np-skip"

def nprtLabelDispatchRepeatBegin : Bytes =
  b"np-repeat-begin"

def nprtLabelDispatchRepeatEnd : Bytes =
  b"np-repeat-end"

def nprtLabelDispatchStore : Bytes =
  b"np-store"

def nprtLabelDispatchAdd : Bytes =
  b"np-add"

def nprtLabelDispatchFloat64 : Bytes =
  b"np-float64-"

def nprtLabelDispatchFenceWait : Bytes =
  b"np-fence-wait"

def nprtLabelFenceWaitLoop : Bytes =
  b"np-fence-wait-l"

def nprtLabelFenceWaitDone : Bytes =
  b"np-fence-wait-d"

def nprtLabelRepeatScan : Bytes =
  b"np-repeat-scan"

def nprtLabelRepeatScanNext : Bytes =
  b"np-repeat-scan-n"

def nprtLabelRepeatFound : Bytes =
  b"np-repeat-found"

def nprtLabelRepeatAgain : Bytes =
  b"np-repeat-again"

def nprtLabelResolveLoopAffine : Bytes =
  b"np-res-affine"

def nprtLabelResolveLoopAffineStep : Bytes =
  b"np-res-affine-s"

def nprtLabelResolveLoopAffineDone : Bytes =
  b"np-res-affine-d"

-- the scratch after the result slots: [+0] repeat iteration, [+8] count,
-- [+16] first body record, [+24] body record count, [+32] a timespec
-- (seconds, nanoseconds) for the fence wait's nanosleep
def nprtScratchBytes : Nat =
  nativePhysicalMemoryScratchBytes

-- argv[0]'s offset from the entry stack pointer x21 holds ([sp] is argc).
-- The x86 runtime reads [rsp + 16] because its resolver runs one call deep,
-- with the return address on the stack; x21 is the entry value itself.
def nprtArgvOffset : Nat =
  8

-- the asm-generic nanosleep
def nprtNanosleep : Nat =
  101

def nprtD0 : (family AArch64FloatRegister) =
  (constructor AArch64FloatRegister AArch64S0)

def nprtD1 : (family AArch64FloatRegister) =
  (constructor AArch64FloatRegister AArch64S1)

-- in the command dispatch: `tag` to `target`
def nprtDispatchTag =
  (lambda unrestricted tag : Nat .
    (lambda unrestricted target : Bytes .
      (lambda unrestricted tail : (family AArch64Assembly) .
        (nprtEmit (nprtCmpImm nprtX6 tag) (nprtBIf nprtEqual target tail)))))

-- in the resolver's dispatch: operand kind `kind` to `target`
def nprtDispatchKind =
  (lambda unrestricted kind : Nat .
    (lambda unrestricted target : Bytes .
      (lambda unrestricted tail : (family AArch64Assembly) .
        (nprtEmit (nprtCmpImm nprtX9 kind) (nprtBIf nprtEqual target tail)))))

-- the scratch's address, x19 + 8 * resultSlots, into `register`
def nprtScratchInto =
  (lambda unrestricted register : (family AArch64Register) .
    (lambda unrestricted tail : (family AArch64Assembly) .
      (nprtEmit
        (nprtLdr register nprtX15 32)
        (nprtEmit (nprtLsl register 3) (nprtEmit (nprtAdd register nprtX19) tail)))))

-- RepeatBegin (tag 9): iteration 0, the count from operand 0, the first body
-- record, and the number of body records found by scanning forward to the
-- matching RepeatEnd (tag 10).  A nested RepeatBegin or running off the image
-- is a malformed record.  A count of zero skips the body.
-- Shared by repeat search and branch skipping. Extents are checked before
-- reading or advancing, including the V3 alignment/padding contract.
def nprtScanRecord =
  (lambda unrestricted pointer : (family AArch64Register) .
    (lambda unrestricted extent : (family AArch64Register) .
      (lambda unrestricted scratch : (family AArch64Register) .
        (lambda unrestricted field : (family AArch64Register) .
          (lambda unrestricted tail : (family AArch64Assembly) .
            (nprtEmit
              (nprtCompare pointer nprtX12)
              (nprtBIf
                nprtBelow
                nprtLabelFatalBounds
                (nprtEmit
                  (nprtMov scratch nprtX12)
                  (nprtEmit
                    (nprtSub scratch pointer)
                    (nprtEmit
                      (nprtCmpImm scratch nativePhysicalImageCommandFixedBytes)
                      (nprtBIf
                        nprtBelow
                        nprtLabelFatalRecord
                        (nprtEmit
                          (nprtLdr extent pointer 8)
                          (nprtEmit
                            (nprtCmpImm extent nativePhysicalImageCommandFixedBytes)
                            (nprtBIf
                              nprtBelow
                              nprtLabelFatalRecord
                              (nprtEmit
                                (nprtCompare extent scratch)
                                (nprtBIf
                                  nprtBelow
                                  nprtLabelFatalBounds
                                  (nprtEmit
                                    (nprtMovz
                                      field
                                      (naturalSaturatingSubtract
                                        nativePhysicalImageRecordAlignment
                                        1))
                                    (nprtEmit
                                      (constructor
                                        AArch64Instruction
                                        AArch64AndRegister
                                        field
                                        extent
                                        field)
                                      (nprtEmit
                                        (nprtCmpImm field 0)
                                        (nprtBIf
                                        nprtNotEqual
                                        nprtLabelFatalRecord
                                        (nprtEmit
                                        (nprtMov scratch extent)
                                        (nprtEmit
                                        (nprtSubImm scratch nativePhysicalImageCommandFixedBytes)
                                        (nprtEmit
                                        (nprtLdr field pointer 32)
                                        (nprtEmit
                                        (nprtCompare field scratch)
                                        (nprtBIf
                                        nprtBelow
                                        nprtLabelFatalRecord
                                        (nprtEmit
                                        (nprtSub scratch field)
                                        (nprtEmit
                                        (nprtLdr field pointer 40)
                                        (nprtEmit
                                        (nprtCompare field scratch)
                                        (nprtBIf
                                        nprtBelow
                                        nprtLabelFatalRecord
                                        (nprtEmit
                                        (nprtSub scratch field)
                                        (nprtEmit
                                        (nprtLdr field pointer 48)
                                        (nprtEmit
                                        (nprtCompare field scratch)
                                        (nprtBIf
                                        nprtBelow
                                        nprtLabelFatalRecord
                                        (nprtEmit
                                        (nprtSub scratch field)
                                        (nprtEmit
                                        (nprtCmpImm
                                        scratch
                                        (naturalSaturatingSubtract
                                        nativePhysicalImageRecordAlignment
                                        1))
                                        (nprtBIf
                                        nprtAbove
                                        nprtLabelFatalRecord
                                        (nprtEmit
                                        (nprtLdr field pointer 0)
                                        (nprtEmit
                                        (nprtCmpImm field 1)
                                        (nprtBIf
                                        nprtBelow
                                        nprtLabelFatalRecord
                                        (nprtEmit
                                        (nprtCmpImm field 23)
                                        (nprtBIf nprtAbove nprtLabelFatalRecord tail)))))))))))))))))))))))))))))))))))))))))

-- X9 owns the loop-frame address and X10 its record count throughout this
-- scan. The record validator uses X0/X4/X5 so those live values survive.
def nprtRepeatBeginBlock =
  (lambda unrestricted tail : (family AArch64Assembly) .
    (nprtLabel
      nprtLabelDispatchRepeatBegin
      (nprtResolveCall
        64
        nprtX6
        (nprtScratchInto
          nprtX9
          (nprtEmit
            (nprtStr nprtX9 8 nprtX6)
            (nprtEmit
              (nprtMovz nprtX10 0)
              (nprtEmit
                (nprtStr nprtX9 0 nprtX10)
                (nprtEmit
                  (nprtLdr nprtX6 nprtX14 8)
                  (nprtEmit
                    (nprtAdd nprtX6 nprtX14)
                    (nprtEmit
                      (nprtStr nprtX9 16 nprtX6)
                      (nprtLabel
                        nprtLabelRepeatScan
                        (nprtScanRecord
                          nprtX6
                          nprtX0
                          nprtX4
                          nprtX5
                          (nprtEmit
                            (nprtCompare nprtX12 nprtX6)
                            (nprtBIf
                              nprtBelow
                              nprtLabelRepeatScanNext
                              (nprtB
                                nprtLabelFatalRecord
                                (nprtLabel
                                  nprtLabelRepeatScanNext
                                  (nprtEmit
                                    (nprtLdr nprtX0 nprtX6 0)
                                    (nprtEmit
                                      (nprtCmpImm nprtX0 10)
                                      (nprtBIf
                                        nprtEqual
                                        nprtLabelRepeatFound
                                        (nprtEmit
                                        (nprtCmpImm nprtX0 9)
                                        (nprtBIf
                                        nprtEqual
                                        nprtLabelFatalRecord
                                        (nprtEmit
                                        (nprtAddImm nprtX10 1)
                                        (nprtEmit
                                        (nprtLdr nprtX0 nprtX6 8)
                                        (nprtEmit
                                        (nprtAdd nprtX6 nprtX0)
                                        (nprtB
                                        nprtLabelRepeatScan
                                        (nprtLabel
                                        nprtLabelRepeatFound
                                        (nprtEmit
                                        (nprtStr nprtX9 24 nprtX10)
                                        (nprtEmit
                                        (nprtLdr nprtX0 nprtX9 8)
                                        (nprtEmit
                                        (nprtTest nprtX0)
                                        (nprtBIf
                                        nprtNotEqual
                                        nprtLabelAdvance
                                        (nprtEmit
                                        (nprtSub nprtX13 nprtX10)
                                        (nprtEmit
                                        (nprtSubImm nprtX13 1)
                                        (nprtEmit
                                        (nprtMov nprtX14 nprtX6)
                                        (nprtB nprtLabelAdvance tail))))))))))))))))))))))))))))))))))

-- RepeatEnd (tag 10): one more iteration done; while iterations remain,
-- continue at the first body record with the body's records still to count,
-- otherwise advance past the end.
def nprtRepeatEndBlock =
  (lambda unrestricted tail : (family AArch64Assembly) .
    (nprtLabel
      nprtLabelDispatchRepeatEnd
      (nprtScratchInto
        nprtX9
        (nprtEmit
          (nprtLdr nprtX10 nprtX9 0)
          (nprtEmit
            (nprtAddImm nprtX10 1)
            (nprtEmit
              (nprtStr nprtX9 0 nprtX10)
              (nprtEmit
                (nprtLdr nprtX6 nprtX9 8)
                (nprtEmit
                  (nprtCompare nprtX6 nprtX10)
                  (nprtBIf
                    nprtBelow
                    nprtLabelRepeatAgain
                    (nprtB
                      nprtLabelAdvance
                      (nprtLabel
                        nprtLabelRepeatAgain
                        (nprtEmit
                          (nprtLdr nprtX14 nprtX9 16)
                          (nprtEmit
                            (nprtLdr nprtX6 nprtX9 24)
                            (nprtEmit (nprtAdd nprtX13 nprtX6) (nprtB nprtLabelLoop tail)))))))))))))))

-- StoreWord64 (tag 11): the value of operand 1 into the address operand 0
-- resolves to.
def nprtStoreBlock =
  (lambda unrestricted tail : (family AArch64Assembly) .
    (nprtLabel
      nprtLabelDispatchStore
      (nprtResolveCall
        64
        nprtX1
        (nprtResolveCall
          88
          nprtX2
          (nprtEmit (nprtStr nprtX1 0 nprtX2) (nprtB nprtLabelAdvance tail))))))

-- AddWord64 (tag 13): operand 1 plus operand 2, modulo 2^64, into the
-- address operand 0 resolves to.
def nprtAddBlock =
  (lambda unrestricted tail : (family AArch64Assembly) .
    (nprtLabel
      nprtLabelDispatchAdd
      (nprtResolveCall
        64
        nprtX1
        (nprtResolveCall
          88
          nprtX2
          (nprtResolveCall
            112
            nprtX3
            (nprtEmit
              (nprtAdd nprtX2 nprtX3)
              (nprtEmit (nprtStr nprtX1 0 nprtX2) (nprtB nprtLabelAdvance tail))))))))

-- Float64 (tags 14 .. 21, Runtime.NativePhysicalImage.
-- nativePhysicalImageFloat64Tag): operand 1's and operand 2's words into d0
-- and d1, the operation, the result's word (binary32: the low word,
-- zero-extended) into the address operand 0 resolves to.  Each operation
-- leaves its word in x6.
def nprtFloat64Word =
  (lambda unrestricted instruction : (family AArch64Instruction) .
    (lambda unrestricted tail : (family AArch64Assembly) .
      (nprtEmit
        instruction
        (nprtEmit (constructor AArch64Instruction AArch64FloatMoveToGeneral64 nprtX6 nprtD0) tail))))

def nprtFloat64Binary =
  (lambda unrestricted operation : (pi unrestricted d : (family AArch64FloatRegister) . (pi unrestricted l : (family AArch64FloatRegister) . (pi unrestricted r : (family AArch64FloatRegister) . (family AArch64Instruction)))) .
    (nprtFloat64Word (operation nprtD0 nprtD0 nprtD1)))

-- `each tag operation rest` for every tag, in order
def nprtFloat64Entries =
  (lambda unrestricted each : (pi unrestricted tag : Nat . (pi unrestricted operation : (pi unrestricted after : (family AArch64Assembly) . (family AArch64Assembly)) . (pi unrestricted rest : (family AArch64Assembly) . (family AArch64Assembly)))) .
    (lambda unrestricted tail : (family AArch64Assembly) .
      (each
        14
        (nprtFloat64Binary
          (lambda unrestricted d : (family AArch64FloatRegister) .
            (lambda unrestricted l : (family AArch64FloatRegister) .
              (lambda unrestricted r : (family AArch64FloatRegister) .
                (constructor AArch64Instruction AArch64FloatAdd64 d l r)))))
        (each
          15
          (nprtFloat64Binary
            (lambda unrestricted d : (family AArch64FloatRegister) .
              (lambda unrestricted l : (family AArch64FloatRegister) .
                (lambda unrestricted r : (family AArch64FloatRegister) .
                  (constructor AArch64Instruction AArch64FloatSubtract64 d l r)))))
          (each
            16
            (nprtFloat64Binary
              (lambda unrestricted d : (family AArch64FloatRegister) .
                (lambda unrestricted l : (family AArch64FloatRegister) .
                  (lambda unrestricted r : (family AArch64FloatRegister) .
                    (constructor AArch64Instruction AArch64FloatMultiply64 d l r)))))
            (each
              17
              (nprtFloat64Binary
                (lambda unrestricted d : (family AArch64FloatRegister) .
                  (lambda unrestricted l : (family AArch64FloatRegister) .
                    (lambda unrestricted r : (family AArch64FloatRegister) .
                      (constructor AArch64Instruction AArch64FloatDivide64 d l r)))))
              -- the square root of operand 2, as the x86 lane's sqrtsd xmm0, xmm1
              (each
                18
                (nprtFloat64Word
                  (constructor AArch64Instruction AArch64FloatSquareRoot64 nprtD0 nprtD1))
                -- operand 1 as a signed 64-bit integer
                (each
                  19
                  (nprtFloat64Word
                    (constructor AArch64Instruction AArch64FloatFromSigned64 nprtD0 nprtX2))
                  -- operand 1 rounded to binary32, its word zero-extended
                  (each
                    20
                    (lambda unrestricted after : (family AArch64Assembly) .
                      (nprtEmit
                        (constructor AArch64Instruction AArch64FloatNarrow64To32 nprtD0 nprtD0)
                        (nprtEmit
                          (constructor AArch64Instruction AArch64FloatMoveToGeneral32 nprtX6 nprtD0)
                          after)))
                    -- operand 1's low word read as binary32, widened
                    (each
                      21
                      (nprtFloat64Word
                        (constructor AArch64Instruction AArch64FloatWiden32To64 nprtD0 nprtD0))
                      tail))))))))))

def nprtFloat64Label =
  (lambda unrestricted tag : Nat .
    (bytes-append nprtLabelDispatchFloat64 (bytes (nat-to-byte tag))))

def nprtFloat64Dispatch =
  (nprtFloat64Entries
    (lambda unrestricted tag : Nat .
      (lambda unrestricted operation : (pi unrestricted after : (family AArch64Assembly) . (family AArch64Assembly)) .
        (lambda unrestricted rest : (family AArch64Assembly) .
          (nprtDispatchTag tag (nprtFloat64Label tag) rest)))))

def nprtFloat64Block =
  (nprtFloat64Entries
    (lambda unrestricted tag : Nat .
      (lambda unrestricted operation : (pi unrestricted after : (family AArch64Assembly) . (family AArch64Assembly)) .
        (lambda unrestricted rest : (family AArch64Assembly) .
          (nprtLabel
            (nprtFloat64Label tag)
            (nprtResolveCall
              64
              nprtX1
              (nprtResolveCall
                88
                nprtX2
                (nprtResolveCall
                  112
                  nprtX3
                  (nprtEmit
                    (constructor AArch64Instruction AArch64FloatMoveFromGeneral64 nprtD0 nprtX2)
                    (nprtEmit
                      (constructor AArch64Instruction AArch64FloatMoveFromGeneral64 nprtD1 nprtX3)
                      (operation (nprtEmit (nprtStr nprtX1 0 nprtX6) (nprtB nprtLabelAdvance rest)))))))))))))

-- LoopAffine (operand kind 8): base + iteration * stride, the product by
-- repeated addition.  x0 holds the descriptor.
def nprtResolveLoopAffineBlock =
  (lambda unrestricted tail : (family AArch64Assembly) .
    (nprtLabel
      nprtLabelResolveLoopAffine
      (nprtEmit
        (nprtLdr nprtX6 nprtX0 8)
        (nprtEmit
          (nprtLdr nprtX10 nprtX0 16)
          (nprtScratchInto
            nprtX9
            (nprtEmit
              (nprtLdr nprtX9 nprtX9 0)
              (nprtLabel
                nprtLabelResolveLoopAffineStep
                (nprtEmit
                  (nprtTest nprtX9)
                  (nprtBIf
                    nprtEqual
                    nprtLabelResolveLoopAffineDone
                    (nprtEmit
                      (nprtAdd nprtX6 nprtX10)
                      (nprtEmit
                        (nprtSubImm nprtX9 1)
                        (nprtB
                          nprtLabelResolveLoopAffineStep
                          (nprtLabel nprtLabelResolveLoopAffineDone (nprtEmit nprtRet tail))))))))))))))

-- FenceWait (tag 12): the address into x3, the expected value into x4, the
-- poll bound into x5 and the interval into the scratch timespec, then load,
-- compare, nanosleep, count down.  A timeout is a command failure; only
-- equality advances.
def nprtFenceWaitBlock =
  (lambda unrestricted tail : (family AArch64Assembly) .
    (nprtLabel
      nprtLabelDispatchFenceWait
      (nprtResolveCall
        64
        nprtX3
        (nprtResolveCall
          88
          nprtX4
          (nprtResolveCall
            112
            nprtX5
            (nprtResolveCall
              136
              nprtX6
              (nprtScratchInto
                nprtX9
                (nprtEmit
                  (nprtMovz nprtX10 0)
                  (nprtEmit
                    (nprtStr nprtX9 32 nprtX10)
                    (nprtEmit
                      (nprtStr nprtX9 40 nprtX6)
                      (nprtLabel
                        nprtLabelFenceWaitLoop
                        (nprtEmit
                          (nprtLdr nprtX6 nprtX3 0)
                          (nprtEmit
                            (nprtCompare nprtX4 nprtX6)
                            (nprtBIf
                              nprtEqual
                              nprtLabelFenceWaitDone
                              (nprtEmit
                                (nprtMov nprtX0 nprtX9)
                                (nprtEmit
                                  (nprtAddImm nprtX0 32)
                                  (nprtEmit
                                    (nprtMovz nprtX1 0)
                                    (nprtSyscall
                                      nprtNanosleep
                                      (nprtEmit
                                        (nprtSubImm nprtX5 1)
                                        (nprtEmit
                                        (nprtTest nprtX5)
                                        (nprtBIf
                                        nprtNotEqual
                                        nprtLabelFenceWaitLoop
                                        (nprtB
                                        nprtLabelCommandFailure
                                        (nprtLabel
                                        nprtLabelFenceWaitDone
                                        (nprtB nprtLabelAdvance tail))))))))))))))))))))))))

-- entry: x21 = sp ; sp -= 256 ; x15 = &image ; check magic and version ;
-- x13 = command count ; x14 = x15 + 176 ; x12 = x14 + body extent ;
-- x1 = state extent (must be nonzero) ; result slots = count << 3 + extent ;
-- mmap(0, x1, 3, 0x22, -1, 0) -> x20 = state base ; x19 = x20 + state extent.
-- X1 is state extent, X6 result count. X10 holds the remaining word bound.
-- Check before shifting or adding so a damaged image cannot wrap mmap length.
def nprtMemoryGuard =
  (lambda unrestricted tail : (family AArch64Assembly) .
    (nprtMovNegativeOne
      nprtX10
      (nprtEmit
        (nprtSubImm nprtX10 nativePhysicalMemoryScratchBytes)
        (nprtEmit
          (nprtCompare nprtX10 nprtX1)
          (nprtBIf
            nprtAbove
            nprtLabelFatalFormat
            (nprtEmit
              (nprtSub nprtX10 nprtX1)
              (nprtEmit
                (constructor
                  AArch64Instruction
                  AArch64ShiftRightImmediate
                  nprtX10
                  nprtX10
                  nativePhysicalMemoryWordShift)
                (nprtEmit
                  (nprtCompare nprtX10 nprtX6)
                  (nprtBIf nprtAbove nprtLabelFatalFormat tail)))))))))

def nprtMainBlock =
  (lambda unrestricted tail : (family AArch64Assembly) .
    (nprtLabel
      nprtLabelEntry
      (nprtEmit
        (constructor AArch64Instruction AArch64AddImmediateFromStackPointer nprtX21 0)
        (nprtEmit
          (constructor
            AArch64Instruction
            AArch64SubtractStackPointer
            nprtStackBytes
            (constructor AArch64ImmediateShift AArch64Unshifted))
          (nprtAdr
            nprtX15
            nprtLabelImage
            (nprtEmit
              (nprtLdr nprtX6 nprtX15 0)
              (nprtMovImm64
                nprtX10
                (byte 65)
                (byte 76)
                (byte 80)
                (byte 88)
                (byte 80)
                (byte 72)
                (byte 89)
                (byte 51)
                (nprtEmit
                  (nprtCompare nprtX10 nprtX6)
                  (nprtBIf
                    nprtNotEqual
                    nprtLabelFatalFormat
                    (nprtEmit
                      (nprtLdr nprtX6 nprtX15 8)
                      (nprtEmit
                        (nprtCmpImm nprtX6 3)
                        (nprtBIf
                          nprtNotEqual
                          nprtLabelFatalFormat
                          (nprtEmit
                            (nprtLdr nprtX13 nprtX15 16)
                            (nprtEmit
                              (nprtMov nprtX14 nprtX15)
                              (nprtEmit
                                (nprtAddImm nprtX14 176)
                                (nprtEmit
                                  (nprtMov nprtX12 nprtX14)
                                  (nprtEmit
                                    (nprtLdr nprtX6 nprtX15 40)
                                    (nprtEmit
                                      (nprtAdd nprtX12 nprtX6)
                                      (nprtEmit
                                        (nprtLdr nprtX1 nprtX15 24)
                                        (nprtEmit
                                        (nprtTest nprtX1)
                                        (nprtBIf
                                        nprtEqual
                                        nprtLabelFatalFormat
                                        (nprtEmit
                                        (nprtLdr nprtX6 nprtX15 32)
                                        (nprtMemoryGuard
                                        (nprtEmit
                                        (nprtLsl nprtX6 nativePhysicalMemoryWordShift)
                                        (nprtEmit
                                        (nprtAdd nprtX1 nprtX6)
                                        (nprtEmit
                                        (nprtAddImm nprtX1 nprtScratchBytes)
                                        (nprtEmit
                                        (nprtMovz nprtX0 0)
                                        (nprtEmit
                                        (nprtMovz nprtX2 3)
                                        (nprtEmit
                                        (nprtMovz nprtX3 34)
                                        (nprtMovNegativeOne
                                        nprtX4
                                        (nprtEmit
                                        (nprtMovz nprtX5 0)
                                        (nprtSyscall
                                        222
                                        (nprtEmit
                                        (nprtTest nprtX0)
                                        (nprtBIf
                                        nprtMinus
                                        nprtLabelFatalSystemCall
                                        (nprtEmit
                                        (nprtMov nprtX20 nprtX0)
                                        (nprtEmit
                                        (nprtMov nprtX19 nprtX20)
                                        (nprtEmit
                                        (nprtLdr nprtX6 nprtX15 24)
                                        (nprtEmit
                                        (nprtAdd nprtX19 nprtX6)
                                        (nprtB nprtLabelLoop tail)))))))))))))))))))))))))))))))))))))))

-- V3's declared record extent includes only the minimum tail padding. Rounding
-- the sum of the content extents (rather than any individual field) keeps their
-- lengths and the diagnostic output intact. Every advance preserves alignment.
def nprtRoundRecordExtent =
  (lambda unrestricted register : (family AArch64Register) .
    (lambda unrestricted tail : (family AArch64Assembly) .
      (nprtEmit
        (nprtAddImm register 3)
        (nprtEmit
          (constructor AArch64Instruction AArch64ShiftRightImmediate register register 2)
          (nprtEmit (nprtLsl register 2) tail)))))

-- loop: while x13 != 0: bounds-check the record at x14, dispatch on kind.
def nprtLoopBlock =
  (lambda unrestricted tail : (family AArch64Assembly) .
    (nprtLabel
      nprtLabelLoop
      (nprtEmit
        (nprtTest nprtX13)
        (nprtBIf
          nprtEqual
          nprtLabelDone
          (nprtEmit
            (nprtCompare nprtX12 nprtX14)
            (nprtBIf
              nprtBelow
              nprtLabelRecordEndValid
              (nprtB
                nprtLabelFatalBounds
                (nprtLabel
                  nprtLabelRecordEndValid
                  (nprtEmit
                    (nprtLdr nprtX6 nprtX14 8)
                    (nprtEmit
                      (nprtCmpImm nprtX6 232)
                      (nprtBIf
                        nprtBelow
                        nprtLabelFatalRecord
                        (nprtLabel
                          nprtLabelRecordExtentValid
                          (nprtEmit
                            (nprtMov nprtX10 nprtX14)
                            (nprtEmit
                              (nprtAdd nprtX10 nprtX6)
                              (nprtEmit
                                (nprtCompare nprtX12 nprtX10)
                                (nprtBIf
                                  nprtAbove
                                  nprtLabelFatalBounds
                                  (nprtEmit
                                    (nprtLdr nprtX9 nprtX14 32)
                                    (nprtEmit
                                      (nprtLdr nprtX10 nprtX14 40)
                                      (nprtEmit
                                        (nprtAdd nprtX9 nprtX10)
                                        (nprtEmit
                                        (nprtLdr nprtX10 nprtX14 48)
                                        (nprtEmit
                                        (nprtAdd nprtX9 nprtX10)
                                        (nprtEmit
                                        (nprtAddImm nprtX9 232)
                                        (nprtRoundRecordExtent
                                        nprtX9
                                        (nprtEmit
                                        (nprtCompare nprtX6 nprtX9)
                                        (nprtBIf
                                        nprtNotEqual
                                        nprtLabelFatalRecord
                                        (nprtEmit
                                        (nprtLdr nprtX9 nprtX14 48)
                                        (nprtEmit
                                        (nprtTest nprtX9)
                                        (nprtBIf
                                        nprtEqual
                                        nprtLabelFatalRecord
                                        (nprtEmit
                                        (nprtLdr nprtX6 nprtX14 0)
                                        (nprtEmit
                                        (nprtCmpImm nprtX6 1)
                                        (nprtBIf
                                        nprtEqual
                                        nprtLabelDispatchSystemCall
                                        (nprtEmit
                                        (nprtCmpImm nprtX6 2)
                                        (nprtBIf
                                        nprtEqual
                                        nprtLabelDispatchCopy
                                        (nprtEmit
                                        (nprtCmpImm nprtX6 3)
                                        (nprtBIf
                                        nprtEqual
                                        nprtLabelDispatchRoutine
                                        (nprtEmit
                                        (nprtCmpImm nprtX6 4)
                                        (nprtBIf
                                        nprtEqual
                                        nprtLabelDispatchFence
                                        (nprtEmit
                                        (nprtCmpImm nprtX6 5)
                                        (nprtBIf
                                        nprtEqual
                                        nprtLabelDispatchTelemetry
                                        (nprtEmit
                                        (nprtCmpImm nprtX6 6)
                                        (nprtBIf
                                        nprtEqual
                                        nprtLabelDispatchAssert
                                        (nprtEmit
                                        (nprtCmpImm nprtX6 7)
                                        (nprtBIf
                                        nprtEqual
                                        nprtLabelDispatchHalt
                                        (nprtEmit
                                        (nprtCmpImm nprtX6 8)
                                        (nprtBIf
                                        nprtEqual
                                        nprtLabelDispatchAssertOneOf
                                        (nprtDispatchTag
                                        23
                                        nprtLabelDispatchSkip
                                        (nprtDispatchTag
                                        9
                                        nprtLabelDispatchRepeatBegin
                                        (nprtDispatchTag
                                        10
                                        nprtLabelDispatchRepeatEnd
                                        (nprtDispatchTag
                                        11
                                        nprtLabelDispatchStore
                                        (nprtDispatchTag
                                        12
                                        nprtLabelDispatchFenceWait
                                        (nprtDispatchTag
                                        13
                                        nprtLabelDispatchAdd
                                        (nprtFloat64Dispatch (nprtB nprtLabelFatalRecord tail)))))))))))))))))))))))))))))))))))))))))))))))))))))

-- syscall: resolve number (slot B) and six arguments, svc, result to x2, bind.
def nprtSystemCallBlock =
  (lambda unrestricted tail : (family AArch64Assembly) .
    (nprtLabel
      nprtLabelDispatchSystemCall
      (nprtResolveCall
        64
        nprtX6
        (nprtEmit
          (nprtStrSlot nprtSlotB nprtX6)
          (nprtResolveCall
            112
            nprtX1
            (nprtResolveCall
              136
              nprtX2
              (nprtResolveCall
                160
                nprtX3
                (nprtResolveCall
                  184
                  nprtX4
                  (nprtResolveCall
                    208
                    nprtX5
                    (nprtResolveCall
                      88
                      nprtX0
                      (nprtEmit
                        (nprtLdrSlot nprtX8 nprtSlotB)
                        (nprtEmit
                          nprtSvc
                          (nprtEmit (nprtMov nprtX2 nprtX0) (nprtB nprtLabelBindResult tail))))))))))))))

-- bind: binding kind at [x14+16]: 0 discard, 1 store x2 into result slot [x14+24].
def nprtBindBlock =
  (lambda unrestricted tail : (family AArch64Assembly) .
    (nprtLabel
      nprtLabelBindResult
      (nprtEmit
        (nprtLdr nprtX6 nprtX14 16)
        (nprtEmit
          (nprtCmpImm nprtX6 0)
          (nprtBIf
            nprtEqual
            nprtLabelAdvance
            (nprtEmit
              (nprtCmpImm nprtX6 1)
              (nprtBIf
                nprtEqual
                nprtLabelBindStore
                (nprtB
                  nprtLabelFatalRecord
                  (nprtLabel
                    nprtLabelBindStore
                    (nprtEmit
                      (nprtLdr nprtX6 nprtX14 24)
                      (nprtEmit
                        (nprtLdr nprtX10 nprtX15 32)
                        (nprtEmit
                          (nprtCompare nprtX10 nprtX6)
                          (nprtBIf
                            nprtBelow
                            nprtLabelBindSlotValid
                            (nprtB
                              nprtLabelFatalOperand
                              (nprtLabel
                                nprtLabelBindSlotValid
                                (nprtEmit
                                  (nprtLsl nprtX6 3)
                                  (nprtEmit
                                    (nprtAdd nprtX6 nprtX19)
                                    (nprtEmit
                                      (nprtStr nprtX6 0 nprtX2)
                                      (nprtB nprtLabelAdvance tail)))))))))))))))))))

-- copy: payload [x14+232 ..) of extent (resolved 88, must equal [x14+32]) into
-- state at resolved destination (64), bounded by the state extent.
def nprtCopyBlock =
  (lambda unrestricted tail : (family AArch64Assembly) .
    (nprtLabel
      nprtLabelDispatchCopy
      (nprtResolveCall
        88
        nprtX3
        (nprtEmit
          (nprtLdr nprtX10 nprtX14 32)
          (nprtEmit
            (nprtCompare nprtX10 nprtX3)
            (nprtBIf
              nprtNotEqual
              nprtLabelCommandFailure
              (nprtEmit
                (nprtMov nprtX5 nprtX3)
                (nprtResolveCall
                  64
                  nprtX6
                  (nprtEmit
                    (nprtMov nprtX9 nprtX6)
                    (nprtEmit
                      (nprtAdd nprtX9 nprtX5)
                      (nprtEmit
                        (nprtLdr nprtX10 nprtX15 24)
                        (nprtEmit
                          (nprtCompare nprtX10 nprtX9)
                          (nprtBIf
                            nprtAbove
                            nprtLabelCommandFailure
                            (nprtEmit
                              (nprtAdd nprtX6 nprtX20)
                              (nprtEmit
                                (nprtMov nprtX0 nprtX6)
                                (nprtEmit
                                  (nprtMov nprtX1 nprtX14)
                                  (nprtEmit
                                    (nprtAddImm nprtX1 232)
                                    (nprtEmit
                                      (nprtTest nprtX3)
                                      (nprtBIf
                                        nprtEqual
                                        nprtLabelCopyDone
                                        (nprtLabel
                                        nprtLabelCopyLoop
                                        (nprtEmit
                                        (nprtLdrb nprtX6 nprtX1)
                                        (nprtEmit
                                        (nprtStrb nprtX0 nprtX6)
                                        (nprtEmit
                                        (nprtAddImm nprtX1 1)
                                        (nprtEmit
                                        (nprtAddImm nprtX0 1)
                                        (nprtEmit
                                        (nprtSubImm nprtX3 1)
                                        (nprtEmit
                                        (nprtTest nprtX3)
                                        (nprtBIf
                                        nprtNotEqual
                                        nprtLabelCopyLoop
                                        (nprtLabel nprtLabelCopyDone (nprtB nprtLabelAdvance tail)))))))))))))))))))))))))))))

def nprtRoutineCall =
  (lambda unrestricted target : (family AArch64Register) .
    (lambda unrestricted tail : (family AArch64Assembly) .
      (nprtEmit
        (nprtStrSlot nprtSaveImageEnd nprtX12)
        (nprtEmit
          (nprtStrSlot nprtSaveRemaining nprtX13)
          (nprtEmit
            (nprtStrSlot nprtSaveCommand nprtX14)
            (nprtEmit
              (nprtStrSlot nprtSaveImage nprtX15)
              (nprtEmit
                (nprtBlr target)
                (nprtEmit
                  (nprtLdrSlot nprtX12 nprtSaveImageEnd)
                  (nprtEmit
                    (nprtLdrSlot nprtX13 nprtSaveRemaining)
                    (nprtEmit
                      (nprtLdrSlot nprtX14 nprtSaveCommand)
                      (nprtEmit (nprtLdrSlot nprtX15 nprtSaveImage) tail)))))))))))

-- routine: call the machine code at [x14+232] with six resolved arguments.
def nprtRoutineBlock =
  (lambda unrestricted tail : (family AArch64Assembly) .
    (nprtLabel
      nprtLabelDispatchRoutine
      (nprtEmit
        (nprtMov nprtX6 nprtX14)
        (nprtEmit
          (nprtAddImm nprtX6 232)
          (nprtEmit
            (nprtStrSlot nprtSlotB nprtX6)
            (nprtResolveCall
              88
              nprtX1
              (nprtResolveCall
                112
                nprtX2
                (nprtResolveCall
                  136
                  nprtX3
                  (nprtResolveCall
                    160
                    nprtX4
                    (nprtResolveCall
                      184
                      nprtX5
                      (nprtResolveCall
                        64
                        nprtX0
                        (nprtEmit
                          (nprtLdrSlot nprtX10 nprtSlotB)
                          (nprtRoutineCall
                            nprtX10
                            (nprtEmit (nprtMov nprtX2 nprtX0) (nprtB nprtLabelBindResult tail)))))))))))))))

-- fence: poll [address] (64) for expected (88), at most maximumPolls (112) times.
def nprtFenceBlock =
  (lambda unrestricted tail : (family AArch64Assembly) .
    (nprtLabel
      nprtLabelDispatchFence
      (nprtResolveCall
        112
        nprtX3
        (nprtEmit
          (nprtStrSlot nprtSlotB nprtX3)
          (nprtResolveCall
            88
            nprtX1
            (nprtEmit
              (nprtStrSlot nprtSlotA nprtX1)
              (nprtResolveCall
                64
                nprtX0
                (nprtEmit
                  (nprtLdrSlot nprtX1 nprtSlotA)
                  (nprtEmit
                    (nprtLdrSlot nprtX3 nprtSlotB)
                    (nprtEmit
                      (nprtTest nprtX3)
                      (nprtBIf
                        nprtEqual
                        nprtLabelCommandFailure
                        (nprtLabel
                          nprtLabelFenceLoop
                          (nprtEmit
                            (nprtLdr nprtX6 nprtX0 0)
                            (nprtEmit
                              (nprtCompare nprtX1 nprtX6)
                              (nprtBIf
                                nprtEqual
                                nprtLabelFenceDone
                                (nprtEmit
                                  (nprtSubImm nprtX3 1)
                                  (nprtEmit
                                    (nprtTest nprtX3)
                                    (nprtBIf
                                      nprtNotEqual
                                      nprtLabelFenceLoop
                                      (nprtB
                                        nprtLabelCommandFailure
                                        (nprtLabel nprtLabelFenceDone (nprtB nprtLabelAdvance tail)))))))))))))))))))))

-- assert: resolved (88) must equal resolved (64).
def nprtAssertBlock =
  (lambda unrestricted tail : (family AArch64Assembly) .
    (nprtLabel
      nprtLabelDispatchAssert
      (nprtResolveCall
        88
        nprtX1
        (nprtEmit
          (nprtStrSlot nprtSlotB nprtX1)
          (nprtResolveCall
            64
            nprtX6
            (nprtEmit
              (nprtLdrSlot nprtX1 nprtSlotB)
              (nprtEmit
                (nprtCompare nprtX1 nprtX6)
                (nprtBIf nprtNotEqual nprtLabelCommandFailure (nprtB nprtLabelAdvance tail)))))))))

-- assert-one-of: resolved (64) must equal resolved (88) or resolved (112).
def nprtAssertOneOfBlock =
  (lambda unrestricted tail : (family AArch64Assembly) .
    (nprtLabel
      nprtLabelDispatchAssertOneOf
      (nprtResolveCall
        112
        nprtX1
        (nprtEmit
          (nprtStrSlot nprtSlotC nprtX1)
          (nprtResolveCall
            88
            nprtX1
            (nprtEmit
              (nprtStrSlot nprtSlotB nprtX1)
              (nprtResolveCall
                64
                nprtX6
                (nprtEmit
                  (nprtLdrSlot nprtX1 nprtSlotB)
                  (nprtEmit
                    (nprtCompare nprtX1 nprtX6)
                    (nprtBIf
                      nprtEqual
                      nprtLabelAdvance
                      (nprtEmit
                        (nprtLdrSlot nprtX1 nprtSlotC)
                        (nprtEmit
                          (nprtCompare nprtX1 nprtX6)
                          (nprtBIf
                            nprtNotEqual
                            nprtLabelCommandFailure
                            (nprtB nprtLabelAdvance tail))))))))))))))

-- telemetry: mmap a buffer of path length + 1, copy the path (payload) in,
-- openat(AT_FDCWD, path, O_WRONLY|O_CREAT|O_APPEND, 0644), write the record
-- (payload after the path) in a loop, fsync, close, munmap.
def nprtTelemetryBlock =
  (lambda unrestricted tail : (family AArch64Assembly) .
    (nprtLabel
      nprtLabelDispatchTelemetry
      (nprtEmit
        (nprtLdr nprtX3 nprtX14 32)
        (nprtEmit
          (nprtTest nprtX3)
          (nprtBIf
            nprtEqual
            nprtLabelCommandFailure
            (nprtEmit
              (nprtMov nprtX1 nprtX3)
              (nprtEmit
                (nprtAddImm nprtX1 1)
                (nprtEmit
                  (nprtStrSlot nprtSlotC nprtX1)
                  (nprtEmit
                    (nprtMovz nprtX0 0)
                    (nprtEmit
                      (nprtMovz nprtX2 3)
                      (nprtEmit
                        (nprtMovz nprtX3 34)
                        (nprtMovNegativeOne
                          nprtX4
                          (nprtEmit
                            (nprtMovz nprtX5 0)
                            (nprtSyscall
                              222
                              (nprtEmit
                                (nprtTest nprtX0)
                                (nprtBIf
                                  nprtMinus
                                  nprtLabelCommandFailure
                                  (nprtEmit
                                    (nprtStrSlot nprtSlotA nprtX0)
                                    (nprtEmit
                                      (nprtLdr nprtX3 nprtX14 32)
                                      (nprtEmit
                                        (nprtMov nprtX1 nprtX14)
                                        (nprtEmit
                                        (nprtAddImm nprtX1 232)
                                        (nprtLabel
                                        nprtLabelTelemetryCopyLoop
                                        (nprtEmit
                                        (nprtLdrb nprtX6 nprtX1)
                                        (nprtEmit
                                        (nprtStrb nprtX0 nprtX6)
                                        (nprtEmit
                                        (nprtAddImm nprtX1 1)
                                        (nprtEmit
                                        (nprtAddImm nprtX0 1)
                                        (nprtEmit
                                        (nprtSubImm nprtX3 1)
                                        (nprtEmit
                                        (nprtTest nprtX3)
                                        (nprtBIf
                                        nprtNotEqual
                                        nprtLabelTelemetryCopyLoop
                                        (nprtMovNegativeOne
                                        nprtX0
                                        (nprtEmit
                                        (nprtAddImm nprtX0 0)
                                        (nprtEmit
                                        (nprtMovz nprtX9 99)
                                        (nprtEmit
                                        (nprtSub nprtX0 nprtX9)
                                        (nprtEmit
                                        (nprtLdrSlot nprtX1 nprtSlotA)
                                        (nprtEmit
                                        (nprtMovz nprtX2 1089)
                                        (nprtEmit
                                        (nprtMovz nprtX3 420)
                                        (nprtSyscall
                                        56
                                        (nprtEmit
                                        (nprtTest nprtX0)
                                        (nprtBIf
                                        nprtMinus
                                        nprtLabelCommandFailure
                                        (nprtEmit
                                        (nprtStrSlot nprtSlotB nprtX0)
                                        (nprtEmit
                                        (nprtMov nprtX1 nprtX14)
                                        (nprtEmit
                                        (nprtAddImm nprtX1 232)
                                        (nprtEmit
                                        (nprtLdr nprtX3 nprtX14 32)
                                        (nprtEmit
                                        (nprtAdd nprtX1 nprtX3)
                                        (nprtEmit
                                        (nprtLdr nprtX2 nprtX14 40)
                                        (nprtEmit
                                        (nprtLdrSlot nprtX0 nprtSlotB)
                                        (nprtLabel
                                        nprtLabelTelemetryWriteLoop
                                        (nprtSyscall
                                        64
                                        (nprtEmit
                                        (nprtTest nprtX0)
                                        (nprtBIf
                                        nprtMinus
                                        nprtLabelCommandFailure
                                        (nprtBIf
                                        nprtEqual
                                        nprtLabelCommandFailure
                                        (nprtEmit
                                        (nprtAdd nprtX1 nprtX0)
                                        (nprtEmit
                                        (nprtSub nprtX2 nprtX0)
                                        (nprtEmit
                                        (nprtLdrSlot nprtX0 nprtSlotB)
                                        (nprtEmit
                                        (nprtTest nprtX2)
                                        (nprtBIf
                                        nprtNotEqual
                                        nprtLabelTelemetryWriteLoop
                                        (nprtSyscall
                                        82
                                        (nprtEmit
                                        (nprtTest nprtX0)
                                        (nprtBIf
                                        nprtMinus
                                        nprtLabelCommandFailure
                                        (nprtEmit
                                        (nprtLdrSlot nprtX0 nprtSlotB)
                                        (nprtSyscall
                                        57
                                        (nprtEmit
                                        (nprtTest nprtX0)
                                        (nprtBIf
                                        nprtMinus
                                        nprtLabelCommandFailure
                                        (nprtEmit
                                        (nprtLdrSlot nprtX0 nprtSlotA)
                                        (nprtEmit
                                        (nprtLdrSlot nprtX1 nprtSlotC)
                                        (nprtSyscall
                                        215
                                        (nprtEmit
                                        (nprtTest nprtX0)
                                        (nprtBIf
                                        nprtMinus
                                        nprtLabelCommandFailure
                                        (nprtB nprtLabelAdvance tail))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))

-- advance: x14 += record extent ; x13 -= 1 ; loop.
def nprtAdvanceBlock =
  (lambda unrestricted tail : (family AArch64Assembly) .
    (nprtLabel
      nprtLabelAdvance
      (nprtEmit
        (nprtLdr nprtX6 nprtX14 8)
        (nprtEmit
          (nprtAdd nprtX14 nprtX6)
          (nprtEmit (nprtSubImm nprtX13 1) (nprtB nprtLabelLoop tail))))))

-- done: the command pointer must have reached the image end exactly.
def nprtDoneBlock =
  (lambda unrestricted tail : (family AArch64Assembly) .
    (nprtLabel
      nprtLabelDone
      (nprtEmit
        (nprtCompare nprtX12 nprtX14)
        (nprtBIf nprtNotEqual nprtLabelFatalBounds (nprtExitWith 0 tail)))))

def nprtHaltBlock =
  (lambda unrestricted tail : (family AArch64Assembly) .
    (nprtLabel nprtLabelDispatchHalt (nprtExitWith 0 tail)))

-- command failure: write the command's error identity ([x14+48] bytes at
-- payload + [x14+32] + [x14+40]) to stderr, exit 120.
def nprtCommandFailureBlock =
  (lambda unrestricted tail : (family AArch64Assembly) .
    (nprtLabel
      nprtLabelCommandFailure
      (nprtEmit
        (nprtMov nprtX1 nprtX14)
        (nprtEmit
          (nprtAddImm nprtX1 232)
          (nprtEmit
            (nprtLdr nprtX6 nprtX14 32)
            (nprtEmit
              (nprtAdd nprtX1 nprtX6)
              (nprtEmit
                (nprtLdr nprtX6 nprtX14 40)
                (nprtEmit
                  (nprtAdd nprtX1 nprtX6)
                  (nprtEmit
                    (nprtLdr nprtX2 nprtX14 48)
                    (nprtEmit (nprtMovz nprtX0 2) (nprtSyscall 64 (nprtExitWith 120 tail))))))))))))

-- The resolver: x0 points at an operand descriptor (kind at +0, value at +8,
-- extra at +16); the value lands in x6; ret.
def nprtResolveBlock =
  (lambda unrestricted tail : (family AArch64Assembly) .
    (nprtLabel
      nprtLabelResolve
      (nprtEmit
        (nprtLdr nprtX9 nprtX0 0)
        (nprtEmit
          (nprtCmpImm nprtX9 0)
          (nprtBIf
            nprtEqual
            nprtLabelResolveImmediate
            (nprtEmit
              (nprtCmpImm nprtX9 1)
              (nprtBIf
                nprtEqual
                nprtLabelResolveResult
                (nprtEmit
                  (nprtCmpImm nprtX9 2)
                  (nprtBIf
                    nprtEqual
                    nprtLabelResolveResultAddress
                    (nprtEmit
                      (nprtCmpImm nprtX9 3)
                      (nprtBIf
                        nprtEqual
                        nprtLabelResolveStateAddress
                        (nprtEmit
                          (nprtCmpImm nprtX9 4)
                          (nprtBIf
                            nprtEqual
                            nprtLabelResolveStateLoad
                            (nprtEmit
                              (nprtCmpImm nprtX9 5)
                              (nprtBIf
                                nprtEqual
                                nprtLabelResolvePayloadAddress
                                (nprtEmit
                                  (nprtCmpImm nprtX9 6)
                                  (nprtBIf
                                    nprtEqual
                                    nprtLabelResolvePayloadLoad
                                    (nprtEmit
                                      (nprtCmpImm nprtX9 7)
                                      (nprtBIf
                                        nprtEqual
                                        nprtLabelResolveProcessArgument
                                        (nprtDispatchKind
                                        8
                                        nprtLabelResolveLoopAffine
                                        (nprtB
                                        nprtLabelFatalOperand
                                        (nprtLabel
                                        nprtLabelResolveImmediate
                                        (nprtEmit
                                        (nprtLdr nprtX6 nprtX0 8)
                                        (nprtEmit
                                        nprtRet
                                        (nprtLabel
                                        nprtLabelResolveResult
                                        (nprtEmit
                                        (nprtLdr nprtX6 nprtX0 8)
                                        (nprtEmit
                                        (nprtLdr nprtX10 nprtX15 32)
                                        (nprtEmit
                                        (nprtCompare nprtX10 nprtX6)
                                        (nprtBIf
                                        nprtBelow
                                        nprtLabelResolveSlotValid
                                        (nprtB
                                        nprtLabelFatalOperand
                                        (nprtLabel
                                        nprtLabelResolveSlotValid
                                        (nprtEmit
                                        (nprtLsl nprtX6 3)
                                        (nprtEmit
                                        (nprtAdd nprtX6 nprtX19)
                                        (nprtEmit
                                        (nprtLdr nprtX6 nprtX6 0)
                                        (nprtEmit
                                        nprtRet
                                        (nprtLabel
                                        nprtLabelResolveResultAddress
                                        (nprtEmit
                                        (nprtLdr nprtX6 nprtX0 8)
                                        (nprtEmit
                                        (nprtLdr nprtX10 nprtX15 32)
                                        (nprtEmit
                                        (nprtCompare nprtX10 nprtX6)
                                        (nprtBIf
                                        nprtBelow
                                        nprtLabelResolveResultAddressSlotValid
                                        (nprtB
                                        nprtLabelFatalOperand
                                        (nprtLabel
                                        nprtLabelResolveResultAddressSlotValid
                                        (nprtEmit
                                        (nprtLsl nprtX6 3)
                                        (nprtEmit
                                        (nprtAdd nprtX6 nprtX19)
                                        (nprtEmit
                                        (nprtLdr nprtX6 nprtX6 0)
                                        (nprtEmit
                                        (nprtLdr nprtX10 nprtX0 16)
                                        (nprtEmit
                                        (nprtAdd nprtX6 nprtX10)
                                        (nprtEmit
                                        nprtRet
                                        (nprtLabel
                                        nprtLabelResolveStateAddress
                                        (nprtEmit
                                        (nprtLdr nprtX6 nprtX0 8)
                                        (nprtEmit
                                        (nprtLdr nprtX10 nprtX15 24)
                                        (nprtEmit
                                        (nprtCompare nprtX10 nprtX6)
                                        (nprtBIf
                                        nprtBelow
                                        nprtLabelResolveStateAddressValid
                                        (nprtB
                                        nprtLabelFatalOperand
                                        (nprtLabel
                                        nprtLabelResolveStateAddressValid
                                        (nprtEmit
                                        (nprtAdd nprtX6 nprtX20)
                                        (nprtEmit
                                        nprtRet
                                        (nprtLabel
                                        nprtLabelResolveStateLoad
                                        (nprtEmit
                                        (nprtLdr nprtX6 nprtX0 8)
                                        (nprtEmit
                                        (nprtMov nprtX9 nprtX6)
                                        (nprtEmit
                                        (nprtAddImm nprtX9 8)
                                        (nprtEmit
                                        (nprtLdr nprtX10 nprtX15 24)
                                        (nprtEmit
                                        (nprtCompare nprtX10 nprtX9)
                                        (nprtBIf
                                        nprtAbove
                                        nprtLabelFatalOperand
                                        (nprtLabel
                                        nprtLabelResolveStateLoadValid
                                        (nprtEmit
                                        (nprtAdd nprtX6 nprtX20)
                                        (nprtEmit
                                        (nprtLdr nprtX6 nprtX6 0)
                                        (nprtEmit
                                        nprtRet
                                        (nprtLabel
                                        nprtLabelResolvePayloadAddress
                                        (nprtEmit
                                        (nprtLdr nprtX6 nprtX0 8)
                                        (nprtEmit
                                        (nprtLdr nprtX10 nprtX14 32)
                                        (nprtEmit
                                        (nprtCompare nprtX10 nprtX6)
                                        (nprtBIf
                                        nprtBelow
                                        nprtLabelResolvePayloadAddressValid
                                        (nprtB
                                        nprtLabelFatalOperand
                                        (nprtLabel
                                        nprtLabelResolvePayloadAddressValid
                                        (nprtEmit
                                        (nprtAdd nprtX6 nprtX14)
                                        (nprtEmit
                                        (nprtAddImm nprtX6 232)
                                        (nprtEmit
                                        nprtRet
                                        (nprtLabel
                                        nprtLabelResolvePayloadLoad
                                        (nprtEmit
                                        (nprtLdr nprtX6 nprtX0 8)
                                        (nprtEmit
                                        (nprtMov nprtX9 nprtX6)
                                        (nprtEmit
                                        (nprtAddImm nprtX9 8)
                                        (nprtEmit
                                        (nprtLdr nprtX10 nprtX14 32)
                                        (nprtEmit
                                        (nprtCompare nprtX10 nprtX9)
                                        (nprtBIf
                                        nprtAbove
                                        nprtLabelFatalOperand
                                        (nprtLabel
                                        nprtLabelResolvePayloadLoadValid
                                        (nprtEmit
                                        (nprtAdd nprtX6 nprtX14)
                                        (nprtEmit
                                        (nprtAddImm nprtX6 232)
                                        (nprtEmit
                                        (nprtLdr nprtX6 nprtX6 0)
                                        (nprtEmit
                                        nprtRet
                                        (nprtLabel
                                        nprtLabelResolveProcessArgument
                                        (nprtEmit
                                        (nprtLdr nprtX6 nprtX0 8)
                                        (nprtEmit
                                        (nprtLsl nprtX6 3)
                                        (nprtEmit
                                        (nprtAdd nprtX6 nprtX21)
                                        (nprtEmit
                                        (nprtLdr nprtX6 nprtX6 nprtArgvOffset)
                                        (nprtEmit nprtRet tail))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))

-- fatal exits, and the shared exit: exit_group(x0).
def nprtFatalBlock =
  (lambda unrestricted tail : (family AArch64Assembly) .
    (nprtLabel
      nprtLabelFatalFormat
      (nprtExitWith
        101
        (nprtLabel
          nprtLabelFatalBounds
          (nprtExitWith
            102
            (nprtLabel
              nprtLabelFatalOperand
              (nprtExitWith
                103
                (nprtLabel
                  nprtLabelFatalSystemCall
                  (nprtExitWith
                    104
                    (nprtLabel
                      nprtLabelFatalAssertion
                      (nprtExitWith
                        105
                        (nprtLabel
                          nprtLabelFatalFence
                          (nprtExitWith
                            106
                            (nprtLabel
                              nprtLabelFatalTelemetry
                              (nprtExitWith
                                107
                                (nprtLabel
                                  nprtLabelFatalRecord
                                  (nprtExitWith 108 (nprtLabel nprtLabelExit (nprtSyscall 94 tail)))))))))))))))))))

-- Same record-count and repeat-frame contract as the x86-64 executor.
-- Skip traversal uses temporary registers, preserving the current loop frame.
def nprtSkipBlock =
  (lambda unrestricted tail : (family AArch64Assembly) .
    (nprtLabel
      nprtLabelDispatchSkip
      (nprtResolveCall
        88
        nprtX1
        (nprtEmit
          (nprtStrSlot nprtSlotB nprtX1)
          (nprtResolveCall
            64
            nprtX6
            (nprtEmit
              (nprtLdrSlot nprtX1 nprtSlotB)
              (nprtEmit
                (nprtCompare nprtX1 nprtX6)
                (nprtBIf
                  nprtEqual
                  nprtLabelAdvance
                  (nprtResolveCall
                    112
                    nprtX8
                    (nprtEmit
                      (nprtMov nprtX6 nprtX13)
                      (nprtEmit
                        (nprtSubImm nprtX6 1)
                        (nprtEmit
                          (nprtCompare nprtX8 nprtX6)
                          (nprtBIf
                            nprtBelow
                            nprtLabelFatalRecord
                            (nprtEmit
                              (nprtMovz nprtX7 0)
                              (nprtLabel
                                b"np-skip-scan"
                                (nprtEmit
                                  (nprtLdr nprtX6 nprtX14 8)
                                  (nprtEmit
                                    (nprtAdd nprtX14 nprtX6)
                                    (nprtEmit
                                      (nprtSubImm nprtX13 1)
                                      (nprtEmit
                                        (nprtCmpImm nprtX8 0)
                                        (nprtBIf
                                        nprtEqual
                                        b"np-skip-done"
                                        (nprtScanRecord
                                        nprtX14
                                        nprtX9
                                        nprtX6
                                        nprtX10
                                        (nprtEmit
                                        (nprtLdr nprtX6 nprtX14 0)
                                        (nprtEmit
                                        (nprtCmpImm nprtX6 1)
                                        (nprtBIf
                                        nprtBelow
                                        nprtLabelFatalRecord
                                        (nprtEmit
                                        (nprtCmpImm nprtX6 23)
                                        (nprtBIf
                                        nprtAbove
                                        nprtLabelFatalRecord
                                        (nprtEmit
                                        (nprtCmpImm nprtX6 9)
                                        (nprtBIf
                                        nprtEqual
                                        b"np-skip-begin"
                                        (nprtEmit
                                        (nprtCmpImm nprtX6 10)
                                        (nprtBIf
                                        nprtEqual
                                        b"np-skip-end"
                                        (nprtEmit
                                        (nprtCmpImm nprtX6 22)
                                        (nprtBIf
                                        nprtEqual
                                        b"np-skip-end"
                                        (nprtB
                                        b"np-skip-next"
                                        (nprtLabel
                                        b"np-skip-begin"
                                        (nprtEmit
                                        (nprtCmpImm nprtX7 0)
                                        (nprtBIf
                                        nprtNotEqual
                                        nprtLabelFatalRecord
                                        (nprtEmit
                                        (nprtMovz nprtX7 1)
                                        (nprtB
                                        b"np-skip-next"
                                        (nprtLabel
                                        b"np-skip-end"
                                        (nprtEmit
                                        (nprtCmpImm nprtX7 0)
                                        (nprtBIf
                                        nprtEqual
                                        nprtLabelFatalRecord
                                        (nprtEmit
                                        (nprtMovz nprtX7 0)
                                        (nprtLabel
                                        b"np-skip-next"
                                        (nprtEmit
                                        (nprtSubImm nprtX8 1)
                                        (nprtB
                                        b"np-skip-scan"
                                        (nprtLabel
                                        b"np-skip-done"
                                        (nprtEmit
                                        (nprtCmpImm nprtX7 0)
                                        (nprtBIf
                                        nprtNotEqual
                                        nprtLabelFatalRecord
                                        (nprtB nprtLabelLoop tail)))))))))))))))))))))))))))))))))))))))))))))))))

def aarch64NativePhysicalRuntimeAssembly : (family AArch64Assembly) =
  (nprtMainBlock
    (nprtLoopBlock
      (nprtSystemCallBlock
        (nprtBindBlock
          (nprtCopyBlock
            (nprtRoutineBlock
              (nprtFenceBlock
                (nprtTelemetryBlock
                  (nprtAssertBlock
                    (nprtAssertOneOfBlock
                      (nprtAdvanceBlock
                        (nprtDoneBlock
                          (nprtHaltBlock
                            (nprtCommandFailureBlock
                              (nprtResolveBlock
                                (nprtSkipBlock
                                  (nprtFatalBlock
                                    (nprtRepeatBeginBlock
                                      (nprtRepeatEndBlock
                                        (nprtStoreBlock
                                        (nprtAddBlock
                                        (nprtFloat64Block
                                        (nprtResolveLoopAffineBlock
                                        (nprtFenceWaitBlock
                                        (constructor
                                        AArch64Assembly
                                        AArch64AssemblyLabel
                                        nprtLabelImage
                                        (constructor AArch64Assembly AArch64AssemblyEnd))))))))))))))))))))))))))

def aarch64NativePhysicalRuntime : (family AArch64AssemblyResult) =
  (aarch64Assemble aarch64NativePhysicalRuntimeAssembly)