module Platform.AArch64.HostLowering import Compiler.ELF import Data.Bytes import Model.Config import Model.Parameter import Model.Word64 import Platform.AArch64.MemoryRoutine import Platform.AArch64.WordArithmetic import Platform.AArch64.SocketRoutine import Runtime.NativeMemoryRoutine import Runtime.NativeWordArithmetic import Runtime.NativeFloatPlan import Platform.AArch64.FloatRoutine import Runtime.NativeSocketRoutine import Runtime.NativeSocketEndpoint import Platform.AArch64.Descriptor import Platform.AArch64.CardInfo import Platform.Linux.Nvidia.DeviceBinding import Runtime.NativeDescriptor import Platform.AArch64.CyclicRecordOffset import Platform.AArch64.LaunchRecipeRoutine import Platform.AArch64.NativePhysicalELF import Platform.AArch64.NativePhysicalRuntime import Platform.Linux.Nvidia.PlanHost import Platform.AArch64.PublicationRoutine import Platform.AArch64.TelemetrySeal import Platform.AArch64.WordDigest import Runtime.NativeCyclicRecordOffset import Runtime.NativeTelemetrySeal import Runtime.NativeWordDigest import Compiler.MachineAArch64Assembly import Runtime.NativeLaunchRecipeRoutine import Runtime.NativePhysicalImage import Runtime.NativePhysicalImagePlan import Runtime.NativePhysicalProgram import Std.Natural -- A host program for Linux x86-64 lowered to Linux AArch64. -- -- The physical command language is the same on both machines and the -- runtimes interpret it block for block (Platform.AArch64. -- NativePhysicalRuntime). What differs is the Linux ABI the program's own -- commands speak and the machine code its routines carry, and this module is -- the one place both are translated: -- -- * a system call's number, from the x86-64 table to the asm-generic one -- AArch64 uses; -- * the three x86-64 calls AArch64 has only in their general form -- dup2, -- unlink and rename become dup3(old, new, 0), unlinkat(AT_FDCWD, path, -- 0) and renameat2(AT_FDCWD, old, AT_FDCWD, new, 0), the same calls on -- both kernels; -- * openat's flags, whose O_DIRECT, O_LARGEFILE, O_DIRECTORY and -- O_NOFOLLOW bits sit at different positions (see ahlOpenFlags); -- * a machine routine, by its exact x86-64 code, to its AArch64 twin -- -- including the endpoint routines (connect, accept), so a learner's -- participant establishes its own sessions on either host. -- -- Anything else -- a call this table does not know, a number or an openat -- flag word not given as an immediate, a routine without a twin -- is -- refused by name, never passed through. family AArch64SystemCallForm : Type 0 constructor AArch64SystemCallAbsent -- the same arguments under another number constructor AArch64SystemCallSame field unrestricted aarch64SystemCallSameNumber : Nat constructor AArch64SystemCallDup3 field unrestricted aarch64SystemCallDup3Number : Nat constructor AArch64SystemCallUnlinkat field unrestricted aarch64SystemCallUnlinkatNumber : Nat constructor AArch64SystemCallRenameat2 field unrestricted aarch64SystemCallRenameat2Number : Nat constructor AArch64SystemCallOpenat field unrestricted aarch64SystemCallOpenatNumber : Nat end-family family AArch64SystemCallTable : Type 0 constructor AArch64SystemCallTableEnd constructor AArch64SystemCallTableNext field unrestricted aarch64SystemCallTableX86 : Nat field unrestricted aarch64SystemCallTableForm : (family AArch64SystemCallForm) recursive unrestricted aarch64SystemCallTableRest end-family family AArch64HostOperation : Type 0 constructor AArch64HostOperationLowered field unrestricted aarch64HostOperationValue : (family NativePhysicalOperation) constructor AArch64HostOperationRefused field unrestricted aarch64HostOperationReason : Bytes -- two commands in place of one constructor AArch64HostOperationLoweredPair field unrestricted aarch64HostOperationFirst : (family NativePhysicalOperation) field unrestricted aarch64HostOperationSecond : (family NativePhysicalOperation) end-family family AArch64HostLowering : Type 0 constructor AArch64HostLowered field unrestricted aarch64HostLoweredProgram : (family NativePhysicalProgram) constructor AArch64HostRefused -- why, and the command (from 0) that was refused field unrestricted aarch64HostRefusedReason : Bytes field unrestricted aarch64HostRefusedCommand : Nat end-family family AArch64HostRoutines : Type 0 constructor AArch64HostRoutinesEnd constructor AArch64HostRoutinesNext field unrestricted aarch64HostRoutineX86 : Bytes field unrestricted aarch64HostRoutineAArch64 : Bytes recursive unrestricted aarch64HostRoutinesRest end-family family AArch64HostCommands : Type 0 constructor AArch64HostCommandsLowered field unrestricted aarch64HostCommandsValue : (family NativePhysicalCommands) constructor AArch64HostCommandsRefused field unrestricted aarch64HostCommandsReason : Bytes field unrestricted aarch64HostCommandsIndex : Nat end-family -- the asm-generic AT_FDCWD, the same -100 as x86-64's def ahlAtFdCwd : Nat = 18446744073709551516 def ahlEntry = (lambda unrestricted x86 : Nat . (lambda unrestricted form : (family AArch64SystemCallForm) . (lambda unrestricted rest : (family AArch64SystemCallTable) . (constructor AArch64SystemCallTable AArch64SystemCallTableNext x86 form rest)))) def ahlSame = (lambda unrestricted number : Nat . (constructor AArch64SystemCallForm AArch64SystemCallSame number)) -- Every call the plan hosts and the host-runtime contracts make: x86-64 -- (arch/x86/entry/syscalls/syscall_64.tbl) against asm-generic -- (include/uapi/asm-generic/unistd.h). def aarch64SystemCallTable : (family AArch64SystemCallTable) = (ahlEntry 0 (ahlSame 63) -- read (ahlEntry 1 (ahlSame 64) -- write (ahlEntry 3 (ahlSame 57) -- close (ahlEntry 5 (ahlSame 80) -- fstat (st_size at 48 in both layouts) (ahlEntry 8 (ahlSame 62) -- lseek (ahlEntry 9 (ahlSame 222) -- mmap (ahlEntry 11 (ahlSame 215) -- munmap (ahlEntry 16 (ahlSame 29) -- ioctl (ahlEntry 17 (ahlSame 67) -- pread64 (ahlEntry 18 (ahlSame 68) -- pwrite64 (ahlEntry 33 (constructor AArch64SystemCallForm AArch64SystemCallDup3 24) (ahlEntry 35 (ahlSame 101) -- nanosleep (ahlEntry 40 (ahlSame 71) -- sendfile (ahlEntry 41 (ahlSame 198) -- socket (ahlEntry 43 (ahlSame 202) -- accept (ahlEntry 49 (ahlSame 200) -- bind (ahlEntry 50 (ahlSame 201) -- listen (ahlEntry 51 (ahlSame 204) -- getsockname (ahlEntry 54 (ahlSame 208) -- setsockopt (level/option values shared, see Runtime.NativeSocketPlan) (ahlEntry 60 (ahlSame 93) -- exit (ahlEntry 74 (ahlSame 82) -- fsync (ahlEntry 75 (ahlSame 83) -- fdatasync (ahlEntry 82 (constructor AArch64SystemCallForm AArch64SystemCallRenameat2 276) (ahlEntry 87 (constructor AArch64SystemCallForm AArch64SystemCallUnlinkat 35) (ahlEntry 228 (ahlSame 113) -- clock_gettime (ahlEntry 231 (ahlSame 94) -- exit_group (ahlEntry 257 (constructor AArch64SystemCallForm AArch64SystemCallOpenat 56) (ahlEntry 293 (ahlSame 59) -- pipe2 (ahlEntry 316 (ahlSame 276) -- renameat2 (RENAME_* flags are asm-generic on both) (ahlEntry 324 (ahlSame 283) -- membarrier (constructor AArch64SystemCallTable AArch64SystemCallTableEnd))))))))))))))))))))))))))))))) def aarch64SystemCallFor = (lambda unrestricted x86 : Nat . (eliminate AArch64SystemCallTable (lambda unrestricted current : (family AArch64SystemCallTable) . (family AArch64SystemCallForm)) aarch64SystemCallTable (branch AArch64SystemCallTableEnd . (constructor AArch64SystemCallForm AArch64SystemCallAbsent)) (branch AArch64SystemCallTableNext key form rest induction . (nat-eliminate (lambda unrestricted current : Nat . (family AArch64SystemCallForm)) induction (lambda unrestricted predecessor : Nat . (lambda unrestricted ignored : (family AArch64SystemCallForm) . form)) (naturalEqual key x86))))) -- open(2) flag bits that sit at different positions in the two ABIs: -- include/uapi/asm-generic/fcntl.h (x86-64 uses it unchanged) against -- arch/arm64/include/uapi/asm/fcntl.h. -- O_DIRECT x86-64 0x4000 AArch64 0x10000 -- O_LARGEFILE x86-64 0x8000 AArch64 0x20000 -- O_DIRECTORY x86-64 0x10000 AArch64 0x4000 -- O_NOFOLLOW x86-64 0x20000 AArch64 0x8000 -- Every other flag bit has one value on both. The four positions are -- exchanged among themselves, so each is tested on the caller's x86-64 word, -- never on a partly translated one. Checkpoint restore and publication open -- with O_NOFOLLOW; moving it (not refusing it) is what lets an AArch64 -- participant restore the shards an x86-64 participant published. def ahlX86Direct : Nat = 0x4000 def ahlX86LargeFile : Nat = 0x8000 def ahlX86Directory : Nat = 0x10000 def ahlX86NoFollow : Nat = 0x20000 def ahlAArch64Direct : Nat = 0x10000 def ahlAArch64LargeFile : Nat = 0x20000 def ahlAArch64Directory : Nat = 0x4000 def ahlAArch64NoFollow : Nat = 0x8000 def ahlBit = (lambda unrestricted flags : Nat . (lambda unrestricted bit : Nat . (naturalModuloUnchecked (naturalDivideUnchecked flags bit) 2))) -- `bit` when the x86-64 word sets x86, else zero def ahlMovedBit = (lambda unrestricted flags : Nat . (lambda unrestricted x86 : Nat . (lambda unrestricted bit : Nat . (naturalMultiply (ahlBit flags x86) bit)))) -- ---- results ---- def ahlImm = (lambda unrestricted value : Nat . (constructor NativePhysicalOperand NativePhysicalImmediate (modelWord64FromNaturalTruncated value))) def ahlLowered = (lambda unrestricted operation : (family NativePhysicalOperation) . (constructor AArch64HostOperation AArch64HostOperationLowered operation)) def ahlRefuse = (lambda unrestricted reason : Bytes . (constructor AArch64HostOperation AArch64HostOperationRefused reason)) -- the natural an operand holds when it is an immediate, else `otherwise` def ahlImmediateOr = (lambda unrestricted operand : (family NativePhysicalOperand) . (lambda unrestricted continue : (pi unrestricted value : Nat . (family AArch64HostOperation)) . (lambda unrestricted otherwise : (family AArch64HostOperation) . (eliminate NativePhysicalOperand (lambda unrestricted current : (family NativePhysicalOperand) . (family AArch64HostOperation)) operand (branch NativePhysicalImmediate value . (continue (modelWord64Natural value))) (branch NativePhysicalResultValue slot . otherwise) (branch NativePhysicalResultAddress slot offset . otherwise) (branch NativePhysicalStateAddress offset . otherwise) (branch NativePhysicalStateLoad64 offset . otherwise) (branch NativePhysicalPayloadAddress offset . otherwise) (branch NativePhysicalPayloadLoad64 offset . otherwise) (branch NativePhysicalProcessArgument index . otherwise) (branch NativePhysicalLoopAffine base stride . otherwise))))) -- ... else refuse def ahlWithImmediate = (lambda unrestricted operand : (family NativePhysicalOperand) . (lambda unrestricted reason : Bytes . (lambda unrestricted continue : (pi unrestricted value : Nat . (family AArch64HostOperation)) . (ahlImmediateOr operand continue (ahlRefuse reason))))) -- openat's flags on AArch64: the four relocated bits moved, every other bit -- the same def ahlOpenFlags = (lambda unrestricted flags : Nat . (naturalAdd (naturalSaturatingSubtract flags (naturalAdd (ahlMovedBit flags ahlX86Direct ahlX86Direct) (naturalAdd (ahlMovedBit flags ahlX86LargeFile ahlX86LargeFile) (naturalAdd (ahlMovedBit flags ahlX86Directory ahlX86Directory) (ahlMovedBit flags ahlX86NoFollow ahlX86NoFollow))))) (naturalAdd (ahlMovedBit flags ahlX86Direct ahlAArch64Direct) (naturalAdd (ahlMovedBit flags ahlX86LargeFile ahlAArch64LargeFile) (naturalAdd (ahlMovedBit flags ahlX86Directory ahlAArch64Directory) (ahlMovedBit flags ahlX86NoFollow ahlAArch64NoFollow)))))) def ahlSystemCall = (lambda unrestricted number : Nat . (lambda unrestricted arguments : (family NativePhysicalArguments) . (lambda unrestricted payload : Bytes . (lambda unrestricted result : (family NativePhysicalResultBinding) . (eliminate NativePhysicalArguments (lambda unrestricted current : (family NativePhysicalArguments) . (family AArch64HostOperation)) arguments (branch NativePhysicalArgumentsValue a0 a1 a2 a3 a4 a5 . (let unrestricted call = (lambda unrestricted target : Nat . (lambda unrestricted argv : (family NativePhysicalArguments) . (ahlLowered (constructor NativePhysicalOperation NativePhysicalSystemCall (ahlImm target) argv payload result)))) in (eliminate AArch64SystemCallForm (lambda unrestricted current : (family AArch64SystemCallForm) . (family AArch64HostOperation)) (aarch64SystemCallFor number) (branch AArch64SystemCallAbsent . (ahlRefuse b"aarch64-host-system-call-unknown")) (branch AArch64SystemCallSame target . (call target arguments)) (branch AArch64SystemCallDup3 target . (call target (constructor NativePhysicalArguments NativePhysicalArgumentsValue a0 a1 (ahlImm 0) a3 a4 a5))) (branch AArch64SystemCallUnlinkat target . (call target (constructor NativePhysicalArguments NativePhysicalArgumentsValue (ahlImm ahlAtFdCwd) a0 (ahlImm 0) (ahlImm 0) (ahlImm 0) (ahlImm 0)))) (branch AArch64SystemCallRenameat2 target . (call target (constructor NativePhysicalArguments NativePhysicalArgumentsValue (ahlImm ahlAtFdCwd) a0 (ahlImm ahlAtFdCwd) a1 (ahlImm 0) (ahlImm 0)))) (branch AArch64SystemCallOpenat target . (ahlWithImmediate a2 b"aarch64-host-openat-flags-not-immediate" (lambda unrestricted flags : Nat . (call target (constructor NativePhysicalArguments NativePhysicalArgumentsValue a0 a1 (ahlImm (ahlOpenFlags flags)) a3 a4 a5))))))))))))) -- ---- a number read at run time ---- -- A system call whose number the program reads at run time (the text -- request's operation word is one: 39 continues, 231 stops) cannot be -- translated here. It is translated there, by a routine generated from the -- table above: x0 in, the AArch64 number of an entry of the same form out, -- and -1 -- a call the kernel refuses -- for any other. Its result is kept -- in one result slot this lowering adds after the program's own. def ahlTranslateLabel = (lambda unrestricted x86 : Nat . (bytes-append b"ahl-translate-" (bytes (nat-to-byte (naturalDivideUnchecked x86 256)) (nat-to-byte (naturalModuloUnchecked x86 256))))) def aarch64SystemCallTranslateAssembly : (family AArch64Assembly) = (eliminate AArch64SystemCallTable (lambda unrestricted current : (family AArch64SystemCallTable) . (family AArch64Assembly)) aarch64SystemCallTable (branch AArch64SystemCallTableEnd . (nprtMovNegativeOne nprtX0 (nprtEmit nprtRet (constructor AArch64Assembly AArch64AssemblyEnd)))) (branch AArch64SystemCallTableNext key form rest induction . (eliminate AArch64SystemCallForm (lambda unrestricted current : (family AArch64SystemCallForm) . (family AArch64Assembly)) form (branch AArch64SystemCallAbsent . induction) (branch AArch64SystemCallSame target . (nprtEmit (nprtCmpImm nprtX0 key) (nprtBIf nprtNotEqual (ahlTranslateLabel key) (nprtEmit (nprtMovz nprtX0 target) (nprtEmit nprtRet (nprtLabel (ahlTranslateLabel key) induction)))))) (branch AArch64SystemCallDup3 target . induction) (branch AArch64SystemCallUnlinkat target . induction) (branch AArch64SystemCallRenameat2 target . induction) (branch AArch64SystemCallOpenat target . induction)))) def aarch64SystemCallTranslateRoutine : Bytes = (eliminate AArch64AssemblyResult (lambda unrestricted current : (family AArch64AssemblyResult) . Bytes) (aarch64Assemble aarch64SystemCallTranslateAssembly) (branch AArch64AssemblyEncoded code . code) (branch AArch64AssemblyEncodeDuplicateLabel name . b"") (branch AArch64AssemblyMissingLabel name . b"") (branch AArch64AssemblyDisplacementOutOfRange name . b"") (branch AArch64AssemblyOperandRefused value . b"")) -- translate the number into `slot`, then call through it def ahlTranslatedSystemCall = (lambda unrestricted slot : Nat . (lambda unrestricted number : (family NativePhysicalOperand) . (lambda unrestricted arguments : (family NativePhysicalArguments) . (lambda unrestricted payload : Bytes . (lambda unrestricted result : (family NativePhysicalResultBinding) . (let unrestricted slotOf = (constructor NativePhysicalSlot NativePhysicalSlotValue (modelWord64FromNaturalTruncated slot)) in (constructor AArch64HostOperation AArch64HostOperationLoweredPair (constructor NativePhysicalOperation NativePhysicalMachineRoutine aarch64SystemCallTranslateRoutine (constructor NativePhysicalArguments NativePhysicalArgumentsValue number (ahlImm 0) (ahlImm 0) (ahlImm 0) (ahlImm 0) (ahlImm 0)) (constructor NativePhysicalResultBinding NativePhysicalStoreResult slotOf)) (constructor NativePhysicalOperation NativePhysicalSystemCall (constructor NativePhysicalOperand NativePhysicalResultValue slotOf) arguments payload result)))))))) -- ---- routines ---- -- Each x86-64 routine a plan host carries, with its AArch64 twin. -- Each twin realizes the same admitted semantic/ABI contract. Shared algorithms -- use Platform.AArch64.RoutineEmitter; memory, arithmetic and connected stream -- routines implement their target-local contracts with typed AArch64 assembly. def aarch64HostRoutines : (family AArch64HostRoutines) = (constructor AArch64HostRoutines AArch64HostRoutinesNext phPublishCode aarch64Publish32Routine (constructor AArch64HostRoutines AArch64HostRoutinesNext nativeTelemetrySealRoutine aarch64TelemetrySealRoutine (constructor AArch64HostRoutines AArch64HostRoutinesNext nativeLaunchRecipeRoutineBytes aarch64LaunchRecipeRoutine (constructor AArch64HostRoutines AArch64HostRoutinesNext nativeCyclicRecordOffsetRoutine aarch64CyclicRecordOffsetRoutine (constructor AArch64HostRoutines AArch64HostRoutinesNext nativeWordDigestRoutine aarch64WordDigestRoutine (constructor AArch64HostRoutines AArch64HostRoutinesNext nativeByteDigestRoutine aarch64ByteDigestRoutine (constructor AArch64HostRoutines AArch64HostRoutinesNext nvidiaCardInfoGPUIdCode aarch64CardInfoCode (constructor AArch64HostRoutines AArch64HostRoutinesNext nativeDescriptorStatusCode aarch64DescriptorCode (constructor AArch64HostRoutines AArch64HostRoutinesNext nativeFloat64FiniteCode aarch64Float64FiniteCode (constructor AArch64HostRoutines AArch64HostRoutinesNext nativeMemoryCopyCode aarch64MemoryCopyCode (constructor AArch64HostRoutines AArch64HostRoutinesNext nativeMemoryEqualCode aarch64MemoryEqualCode (constructor AArch64HostRoutines AArch64HostRoutinesNext nativeCheckedWordAddCode aarch64CheckedWordAddCode (constructor AArch64HostRoutines AArch64HostRoutinesNext nativeSocketReadCode aarch64SocketReadCode (constructor AArch64HostRoutines AArch64HostRoutinesNext nativeSocketWriteCode aarch64SocketWriteCode (constructor AArch64HostRoutines AArch64HostRoutinesNext nativeSocketConnectCode aarch64SocketConnectCode (constructor AArch64HostRoutines AArch64HostRoutinesNext nativeSocketAcceptCode aarch64SocketAcceptCode (constructor AArch64HostRoutines AArch64HostRoutinesNext nativeWordDigestContinueRoutine aarch64WordDigestContinueRoutine (constructor AArch64HostRoutines AArch64HostRoutinesNext nativeByteDigestStreamStartRoutine aarch64ByteDigestStreamStartRoutine (constructor AArch64HostRoutines AArch64HostRoutinesNext nativeByteDigestStreamFinishRoutine aarch64ByteDigestStreamFinishRoutine (constructor AArch64HostRoutines AArch64HostRoutinesEnd)))))))))))))))))))) def ahlRoutine = (lambda unrestricted code : Bytes . (lambda unrestricted arguments : (family NativePhysicalArguments) . (lambda unrestricted result : (family NativePhysicalResultBinding) . (eliminate AArch64HostRoutines (lambda unrestricted current : (family AArch64HostRoutines) . (family AArch64HostOperation)) aarch64HostRoutines (branch AArch64HostRoutinesEnd . (ahlRefuse b"aarch64-host-routine-without-twin")) (branch AArch64HostRoutinesNext x86 twin rest induction . (nat-eliminate (lambda unrestricted current : Nat . (family AArch64HostOperation)) induction (lambda unrestricted predecessor : Nat . (lambda unrestricted ignored : (family AArch64HostOperation) . (ahlLowered (constructor NativePhysicalOperation NativePhysicalMachineRoutine twin arguments result)))) (bytes-equal x86 code))))))) def aarch64LowerOperation = (lambda unrestricted translateSlot : Nat . (lambda unrestricted operation : (family NativePhysicalOperation) . (eliminate NativePhysicalOperation (lambda unrestricted current : (family NativePhysicalOperation) . (family AArch64HostOperation)) operation (branch NativePhysicalSystemCall number arguments payload result . (ahlImmediateOr number (lambda unrestricted value : Nat . (ahlSystemCall value arguments payload result)) (ahlTranslatedSystemCall translateSlot number arguments payload result))) (branch NativePhysicalCopyPayloadToState destination extent payload . (ahlLowered operation)) (branch NativePhysicalMachineRoutine code arguments result . (ahlRoutine code arguments result)) (branch NativePhysicalFencePoll address expected polls . (ahlLowered operation)) (branch NativePhysicalTelemetryAppend path record . (ahlLowered operation)) (branch NativePhysicalAssertEqual left right error . (ahlLowered operation)) (branch NativePhysicalAssertOneOf observed first second error . (ahlLowered operation)) (branch NativePhysicalHaltSuccess . (ahlLowered operation)) (branch NativePhysicalRepeatBegin count . (ahlLowered operation)) (branch NativePhysicalSkipUnlessEqual left right count . (ahlLowered operation)) (branch NativePhysicalRepeatEnd . (ahlLowered operation)) (branch NativePhysicalRepeatEndWhen observed expected . (ahlRefuse b"aarch64-repeat-end-when-unavailable")) (branch NativePhysicalStoreWord64 destination value . (ahlLowered operation)) (branch NativePhysicalFenceWait address expected polls interval . (ahlLowered operation)) (branch NativePhysicalRepeatBeginCounted count . (ahlLowered operation)) (branch NativePhysicalAddWord64 destination left right . (ahlLowered operation)) (branch NativePhysicalFloat64 kind destination left right . (ahlLowered operation))))) -- Lowering may expand one source operation into two commands (a dynamic -- syscall number is translated before the syscall). Relative branches refer -- to source records, so their distances must be derived again from the emitted -- prefix. Validate the source window first: truncating an invalid source skip -- to the available suffix would silently admit a malformed source program. def aarch64LoweredWindowCount = (lambda unrestricted translateSlot : Nat . (lambda unrestricted commands : (family NativePhysicalCommands) . (eliminate NativePhysicalCommands (lambda unrestricted current : (family NativePhysicalCommands) . Nat) commands (branch NativePhysicalCommandsEnd . 0) (branch NativePhysicalCommandsNext head rest induction . (naturalAdd (eliminate NativePhysicalCommand (lambda unrestricted current : (family NativePhysicalCommand) . Nat) head (branch NativePhysicalCommandValue operation identity . (eliminate AArch64HostOperation (lambda unrestricted current : (family AArch64HostOperation) . Nat) (aarch64LowerOperation translateSlot operation) (branch AArch64HostOperationLowered value . 1) (branch AArch64HostOperationRefused reason . 0) (branch AArch64HostOperationLoweredPair first second . 2)))) induction))))) def aarch64LowerCommandOperation = (lambda unrestricted translateSlot : Nat . (lambda unrestricted remaining : (family NativePhysicalCommands) . (lambda unrestricted operation : (family NativePhysicalOperation) . (let unrestricted lowered = (aarch64LowerOperation translateSlot operation) in (eliminate NativePhysicalOperation (lambda unrestricted current : (family NativePhysicalOperation) . (family AArch64HostOperation)) operation (branch NativePhysicalSystemCall field0 field1 field2 field3 . lowered) (branch NativePhysicalCopyPayloadToState field0 field1 field2 . lowered) (branch NativePhysicalMachineRoutine field0 field1 field2 . lowered) (branch NativePhysicalFencePoll field0 field1 field2 . lowered) (branch NativePhysicalTelemetryAppend field0 field1 . lowered) (branch NativePhysicalAssertEqual field0 field1 field2 . lowered) (branch NativePhysicalAssertOneOf field0 field1 field2 field3 . lowered) (branch NativePhysicalHaltSuccess . lowered) (branch NativePhysicalRepeatBegin field0 . lowered) (branch NativePhysicalSkipUnlessEqual field0 field1 field2 . (nat-eliminate (lambda unrestricted flag : Nat . (family AArch64HostOperation)) (ahlRefuse b"aarch64-host-branch-target-invalid") (lambda unrestricted prior : Nat . (lambda unrestricted ignored : (family AArch64HostOperation) . (ahlLowered (constructor NativePhysicalOperation NativePhysicalSkipUnlessEqual field0 field1 (modelWord64FromNaturalTruncated (aarch64LoweredWindowCount translateSlot (nativePhysicalCommandsTake remaining (modelWord64Natural field2)))))))) (nativePhysicalBranchWindowValid field2 remaining))) (branch NativePhysicalRepeatEnd . lowered) (branch NativePhysicalRepeatEndWhen field0 field1 . lowered) (branch NativePhysicalStoreWord64 field0 field1 . lowered) (branch NativePhysicalFenceWait field0 field1 field2 field3 . lowered) (branch NativePhysicalRepeatBeginCounted field0 . lowered) (branch NativePhysicalAddWord64 field0 field1 field2 . lowered) (branch NativePhysicalFloat64 field0 field1 field2 field3 . lowered)))))) -- the commands lowered in order; a refusal names the first refused command def aarch64LowerCommands = (lambda unrestricted translateSlot : Nat . (lambda unrestricted commands : (family NativePhysicalCommands) . (app (eliminate NativePhysicalCommands (lambda unrestricted current : (family NativePhysicalCommands) . (pi unrestricted index : Nat . (family AArch64HostCommands))) commands (branch NativePhysicalCommandsEnd . (lambda unrestricted index : Nat . (constructor AArch64HostCommands AArch64HostCommandsLowered (constructor NativePhysicalCommands NativePhysicalCommandsEnd)))) (branch NativePhysicalCommandsNext head tail induction . (lambda unrestricted index : Nat . (eliminate NativePhysicalCommand (lambda unrestricted current : (family NativePhysicalCommand) . (family AArch64HostCommands)) head (branch NativePhysicalCommandValue operation identity . (eliminate AArch64HostOperation (lambda unrestricted current : (family AArch64HostOperation) . (family AArch64HostCommands)) (aarch64LowerCommandOperation translateSlot tail operation) (branch AArch64HostOperationLowered lowered . (eliminate AArch64HostCommands (lambda unrestricted current : (family AArch64HostCommands) . (family AArch64HostCommands)) (induction (succ index)) (branch AArch64HostCommandsLowered rest . (constructor AArch64HostCommands AArch64HostCommandsLowered (constructor NativePhysicalCommands NativePhysicalCommandsNext (constructor NativePhysicalCommand NativePhysicalCommandValue lowered identity) rest))) (branch AArch64HostCommandsRefused reason at . (constructor AArch64HostCommands AArch64HostCommandsRefused reason at)))) (branch AArch64HostOperationRefused reason . (constructor AArch64HostCommands AArch64HostCommandsRefused reason index)) (branch AArch64HostOperationLoweredPair first second . (eliminate AArch64HostCommands (lambda unrestricted current : (family AArch64HostCommands) . (family AArch64HostCommands)) (induction (succ index)) (branch AArch64HostCommandsLowered rest . (constructor AArch64HostCommands AArch64HostCommandsLowered (constructor NativePhysicalCommands NativePhysicalCommandsNext (constructor NativePhysicalCommand NativePhysicalCommandValue first identity) (constructor NativePhysicalCommands NativePhysicalCommandsNext (constructor NativePhysicalCommand NativePhysicalCommandValue second identity) rest)))) (branch AArch64HostCommandsRefused reason at . (constructor AArch64HostCommands AArch64HostCommandsRefused reason at)))))))))) zero))) -- ---- routine alignment ---- -- -- A MachineRoutine's code runs in place, at its record + 232, and A64 -- fetches instructions only from 4-byte aligned addresses; a copy's payload, -- an assertion's error code and a telemetry record have observable lengths -- that need not be words. The image format this host is encoded in, -- NativePhysicalImageAlignedV3 (Runtime.NativePhysicalImagePlan), places -- every record on an aligned boundary, and the runtime refuses any other -- format (exit 101). def ahlCommandCount = (lambda unrestricted commands : (family NativePhysicalCommands) . (eliminate NativePhysicalCommands (lambda unrestricted current : (family NativePhysicalCommands) . Nat) commands (branch NativePhysicalCommandsEnd . zero) (branch NativePhysicalCommandsNext head tail induction . (succ induction)))) def aarch64LowerHostProgram = (lambda unrestricted program : (family NativePhysicalProgram) . (eliminate NativePhysicalProgram (lambda unrestricted current : (family NativePhysicalProgram) . (family AArch64HostLowering)) program (branch NativePhysicalProgramValue stateExtent slots commands expected identity fallbacks . (eliminate AArch64HostCommands (lambda unrestricted current : (family AArch64HostCommands) . (family AArch64HostLowering)) (aarch64LowerCommands (modelWord64Natural slots) commands) -- the program's slots plus the one a translated system call's number -- is written to; a translated call is two commands, so the count is -- the lowered program's. Routine code is placed on instruction -- boundaries by the image format (NativePhysicalImageAlignedV3), -- which the AArch64 runtime requires. (branch AArch64HostCommandsLowered lowered . (constructor AArch64HostLowering AArch64HostLowered (constructor NativePhysicalProgram NativePhysicalProgramValue stateExtent (modelWord64FromNaturalTruncated (succ (modelWord64Natural slots))) lowered (ahlCommandCount lowered) identity fallbacks))) (branch AArch64HostCommandsRefused reason index . (constructor AArch64HostLowering AArch64HostRefused reason index)))))) -- The AArch64 runtime's machine code, assembled once. def aarch64HostRuntimeBytes : Bytes = (eliminate AArch64AssemblyResult (lambda unrestricted current : (family AArch64AssemblyResult) . Bytes) aarch64NativePhysicalRuntime (branch AArch64AssemblyEncoded code . code) (branch AArch64AssemblyEncodeDuplicateLabel name . b"") (branch AArch64AssemblyMissingLabel name . b"") (branch AArch64AssemblyDisplacementOutOfRange name . b"") (branch AArch64AssemblyOperandRefused value . b"")) -- The x86-64 host program as an AArch64 executable: the program lowered, its -- image after the AArch64 runtime, in Compiler.ELF's container. A refusal is -- the empty value, which the direct artifact writer rejects as a non-ELF -- -- fail-closed, as Runtime.NativePhysicalNativeELF's direct path is. def aarch64HostELFBytes = (lambda unrestricted program : (family NativePhysicalProgram) . (eliminate AArch64HostLowering (lambda unrestricted current : (family AArch64HostLowering) . Bytes) (aarch64LowerHostProgram program) (branch AArch64HostLowered lowered . (aarch64WrapMachineCodeSparseLarge (bytes-append aarch64HostRuntimeBytes (compiler-native-encode (family NativePhysicalImagePlan) (constructor NativePhysicalImagePlan NativePhysicalImagePlanValue (constructor NativePhysicalImageFormat NativePhysicalImageAlignedV3) lowered))))) (branch AArch64HostRefused reason index . b"")))