module Runtime.LaunchRecipe import Std.Foundation -- One bounded ALXR v1 expansion algorithm shared by host instruction emitters. -- The wire format and argument contract are documented by NativeLaunchRecipeRoutine. -- All pointers/extents are machine words; supplied input/output ranges must be -- valid, nonoverlapping and nonwrapping. Every read/write is checked against -- those ranges. This is a decoder for compiler-emitted bounded table recipes, -- not an OS mapping or pointer-validity checker. -- Immediates/displacements below are signed 32-bit bit patterns; loads are -- little-endian and permit unaligned access. Compare is unsigned left-right. -- Load8/32 zero-extend; Store8 truncates. Only explicit compares/tests supply -- branch flags, so other emitters need not reproduce unused arithmetic flags. -- SP denotes a private 64-byte scratch frame addressed by negative offsets. -- Each emitter supplies its ABI-compliant frame allocation and return sequence. -- A complete recipe consumes every input byte, fills the declared output and -- has a zero reserved header word. Accepting only its valid prefix would hide -- truncated operation counts or concatenated/corrupt tables. family LaunchRecipeCondition : Type 0 constructor LaunchRecipeBelow constructor LaunchRecipeAbove constructor LaunchRecipeZero constructor LaunchRecipeNotZero end-family family LaunchRecipeBackend : Type 0 parameter erased recipeAssembly : Type 0 parameter erased recipeRegister : Type 0 constructor LaunchRecipeBackendValue field unrestricted backendRecipeMove : (pi unrestricted a0 : recipeRegister . (pi unrestricted a1 : recipeRegister . (pi unrestricted a2 : recipeAssembly . recipeAssembly))) field unrestricted backendRecipeAdd : (pi unrestricted a0 : recipeRegister . (pi unrestricted a1 : recipeRegister . (pi unrestricted a2 : recipeAssembly . recipeAssembly))) field unrestricted backendRecipeSubtract : (pi unrestricted a0 : recipeRegister . (pi unrestricted a1 : recipeRegister . (pi unrestricted a2 : recipeAssembly . recipeAssembly))) field unrestricted backendRecipeAddImmediate : (pi unrestricted a0 : recipeRegister . (pi unrestricted a1 : Nat . (pi unrestricted a2 : recipeAssembly . recipeAssembly))) field unrestricted backendRecipeCompare : (pi unrestricted a0 : recipeRegister . (pi unrestricted a1 : recipeRegister . (pi unrestricted a2 : recipeAssembly . recipeAssembly))) field unrestricted backendRecipeCompareImmediate : (pi unrestricted a0 : recipeRegister . (pi unrestricted a1 : Nat . (pi unrestricted a2 : recipeAssembly . recipeAssembly))) field unrestricted backendRecipeTest : (pi unrestricted a0 : recipeRegister . (pi unrestricted a1 : recipeAssembly . recipeAssembly)) field unrestricted backendRecipeLoad64 : (pi unrestricted a0 : recipeRegister . (pi unrestricted a1 : recipeRegister . (pi unrestricted a2 : Nat . (pi unrestricted a3 : recipeAssembly . recipeAssembly)))) field unrestricted backendRecipeLoad32 : (pi unrestricted a0 : recipeRegister . (pi unrestricted a1 : recipeRegister . (pi unrestricted a2 : Nat . (pi unrestricted a3 : recipeAssembly . recipeAssembly)))) field unrestricted backendRecipeLoad8 : (pi unrestricted a0 : recipeRegister . (pi unrestricted a1 : recipeRegister . (pi unrestricted a2 : recipeAssembly . recipeAssembly))) field unrestricted backendRecipeStore64 : (pi unrestricted a0 : recipeRegister . (pi unrestricted a1 : Nat . (pi unrestricted a2 : recipeRegister . (pi unrestricted a3 : recipeAssembly . recipeAssembly)))) field unrestricted backendRecipeStore8 : (pi unrestricted a0 : recipeRegister . (pi unrestricted a1 : recipeRegister . (pi unrestricted a2 : recipeAssembly . recipeAssembly))) field unrestricted backendRecipeClear : (pi unrestricted a0 : recipeRegister . (pi unrestricted a1 : recipeAssembly . recipeAssembly)) field unrestricted backendRecipeMultiplyImmediate : (pi unrestricted a0 : recipeRegister . (pi unrestricted a1 : Nat . (pi unrestricted a2 : recipeAssembly . recipeAssembly))) field unrestricted backendRecipeLabel : (pi unrestricted a0 : Bytes . (pi unrestricted a1 : recipeAssembly . recipeAssembly)) field unrestricted backendRecipeJump : (pi unrestricted a0 : Bytes . (pi unrestricted a1 : recipeAssembly . recipeAssembly)) field unrestricted backendRecipeJumpIf : (pi unrestricted a0 : (family LaunchRecipeCondition) . (pi unrestricted a1 : Bytes . (pi unrestricted a2 : recipeAssembly . recipeAssembly))) field unrestricted backendRecipeReturn : (pi unrestricted a0 : recipeAssembly . recipeAssembly) field unrestricted backendRecipeEnd : recipeAssembly field unrestricted backendRecipeRAX : recipeRegister field unrestricted backendRecipeRCX : recipeRegister field unrestricted backendRecipeRDX : recipeRegister field unrestricted backendRecipeRSI : recipeRegister field unrestricted backendRecipeRDI : recipeRegister field unrestricted backendRecipeRSP : recipeRegister field unrestricted backendRecipeR8 : recipeRegister field unrestricted backendRecipeR9 : recipeRegister field unrestricted backendRecipeR10 : recipeRegister field unrestricted backendRecipeR11 : recipeRegister end-family def lrLabelEntry : Bytes = b"alxr-entry" def lrLabelLoop : Bytes = b"alxr-loop" def lrLabelLiteral : Bytes = b"alxr-literal" def lrLabelLiteralLoop : Bytes = b"alxr-literal-loop" def lrLabelZero : Bytes = b"alxr-zero" def lrLabelZeroLoop : Bytes = b"alxr-zero-loop" def lrLabelRepeat : Bytes = b"alxr-repeat" def lrLabelUnitLoop : Bytes = b"alxr-unit-loop" def lrLabelNext : Bytes = b"alxr-next" def lrLabelCopyLoop : Bytes = b"alxr-copy-loop" def lrLabelPatchLoop : Bytes = b"alxr-patch-loop" def lrLabelPatchDone : Bytes = b"alxr-patch-done" def lrLabelRepeatDone : Bytes = b"alxr-repeat-done" def lrLabelDone : Bytes = b"alxr-done" def lrLabelFailed : Bytes = b"alxr-failed" def lrMagic : Nat = 0x52584c41 def lrMinusEight : Nat = 0xfffffff8 def lrSlotOutputStart : Nat = 0xfffffff8 def lrSlotUnit : Nat = 0xfffffff0 def lrSlotUnitLength : Nat = 0xffffffe8 def lrSlotPatchCursor : Nat = 0xffffffe0 def lrSlotPatchCount : Nat = 0xffffffd8 def lrSlotRemaining : Nat = 0xffffffd0 def lrSlotResume : Nat = 0xffffffc8 def lrSlotPatchBase : Nat = 0xffffffc0 def launchRecipeAssemblyFor = (lambda erased A : Type 0 . (lambda erased R : Type 0 . (lambda unrestricted backend : (family LaunchRecipeBackend A R) . (eliminate LaunchRecipeBackend (lambda unrestricted current : (family LaunchRecipeBackend A R) . A) backend (branch LaunchRecipeBackendValue lrMove lrAdd lrSubtract lrAddImmediate lrCompare lrCompareImmediate lrTest lrLoad64 lrLoad32 lrLoad8 lrStore64 lrStore8 lrClear lrMultiplyImmediate lrLabel lrJump lrJumpIf lrReturn lrEnd lrRAX lrRCX lrRDX lrRSI lrRDI lrRSP lrR8 lrR9 lrR10 lrR11 . (let unrestricted lrBelow = (constructor LaunchRecipeCondition LaunchRecipeBelow) in (let unrestricted lrAbove = (constructor LaunchRecipeCondition LaunchRecipeAbove) in (let unrestricted lrZero = (constructor LaunchRecipeCondition LaunchRecipeZero) in (let unrestricted lrNotZero = (constructor LaunchRecipeCondition LaunchRecipeNotZero) in (let unrestricted lrEntryBlock = (lambda unrestricted tail : A . (lrLabel lrLabelEntry (lrStore64 lrRSP lrSlotOutputStart lrRDX (lrAdd lrRSI lrRDI (lrAdd lrRCX lrRDX (lrMove lrRAX lrRDI (lrAddImmediate lrRAX 24 (lrCompare lrRAX lrRSI (lrJumpIf lrAbove lrLabelFailed (lrLoad32 lrR9 lrRDI 0 (lrCompareImmediate lrR9 lrMagic (lrJumpIf lrNotZero lrLabelFailed (lrLoad32 lrR9 lrRDI 4 (lrCompareImmediate lrR9 1 (lrJumpIf lrNotZero lrLabelFailed (lrLoad64 lrR9 lrRDI 8 (lrAdd lrR9 lrRDX (lrCompare lrR9 lrRCX (lrJumpIf lrNotZero lrLabelFailed (lrLoad32 lrR8 lrRDI 16 (lrLoad32 lrR9 lrRDI 20 (lrTest lrR9 (lrJumpIf lrNotZero lrLabelFailed (lrAddImmediate lrRDI 24 (lrJump lrLabelLoop tail))))))))))))))))))))))))) in -- Op dispatch: r8 ops remain; the op byte selects the block. (let unrestricted lrLoopBlock = (lambda unrestricted tail : A . (lrLabel lrLabelLoop (lrTest lrR8 (lrJumpIf lrZero lrLabelDone (lrAddImmediate lrR8 0xffffffff (lrCompare lrRDI lrRSI (lrJumpIf lrAbove lrLabelFailed (lrJumpIf lrZero lrLabelFailed (lrLoad8 lrR9 lrRDI (lrCompareImmediate lrR9 1 (lrJumpIf lrZero lrLabelLiteral (lrCompareImmediate lrR9 2 (lrJumpIf lrZero lrLabelZero (lrCompareImmediate lrR9 3 (lrJumpIf lrZero lrLabelRepeat (lrJump lrLabelFailed tail)))))))))))))))) in -- Reads the u32 length after the op byte into r10, advances rdi past it, and -- checks the output has room; the caller checks the input. (let unrestricted lrOperandLength = (lambda unrestricted tail : A . (lrMove lrRAX lrRDI (lrAddImmediate lrRAX 5 (lrCompare lrRAX lrRSI (lrJumpIf lrAbove lrLabelFailed (lrLoad32 lrR10 lrRDI 1 (lrAddImmediate lrRDI 5 (lrMove lrRAX lrRDX (lrAdd lrRAX lrR10 (lrCompare lrRAX lrRCX (lrJumpIf lrAbove lrLabelFailed tail))))))))))) in (let unrestricted lrLiteralBlock = (lambda unrestricted tail : A . (lrLabel lrLabelLiteral (lrOperandLength (lrMove lrRAX lrRDI (lrAdd lrRAX lrR10 (lrCompare lrRAX lrRSI (lrJumpIf lrAbove lrLabelFailed (lrLabel lrLabelLiteralLoop (lrTest lrR10 (lrJumpIf lrZero lrLabelLoop (lrLoad8 lrR11 lrRDI (lrStore8 lrRDX lrR11 (lrAddImmediate lrRDI 1 (lrAddImmediate lrRDX 1 (lrAddImmediate lrR10 0xffffffff (lrJump lrLabelLiteralLoop tail)))))))))))))))) in (let unrestricted lrZeroBlock = (lambda unrestricted tail : A . (lrLabel lrLabelZero (lrOperandLength (lrClear lrR11 (lrLabel lrLabelZeroLoop (lrTest lrR10 (lrJumpIf lrZero lrLabelLoop (lrStore8 lrRDX lrR11 (lrAddImmediate lrRDX 1 (lrAddImmediate lrR10 0xffffffff (lrJump lrLabelZeroLoop tail))))))))))) in -- REPEAT header: count (r9), unit length (r10), patch count (r11); the unit -- and patch table must lie inside the recipe. The first copy is the unit -- itself; the remaining count is saved for the copy loop. (let unrestricted lrRepeatBlock = (lambda unrestricted tail : A . (lrLabel lrLabelRepeat (lrMove lrRAX lrRDI (lrAddImmediate lrRAX 13 (lrCompare lrRAX lrRSI (lrJumpIf lrAbove lrLabelFailed (lrLoad32 lrR9 lrRDI 1 (lrLoad32 lrR10 lrRDI 5 (lrLoad32 lrR11 lrRDI 9 (lrAddImmediate lrRDI 13 (lrTest lrR9 (lrJumpIf lrZero lrLabelFailed (lrStore64 lrRSP lrSlotUnit lrRDI (lrStore64 lrRSP lrSlotUnitLength lrR10 (lrStore64 lrRSP lrSlotPatchCount lrR11 (lrMove lrRAX lrRDI (lrAdd lrRAX lrR10 (lrCompare lrRAX lrRSI (lrJumpIf lrAbove lrLabelFailed (lrStore64 lrRSP lrSlotPatchBase lrRAX (lrMultiplyImmediate lrR11 12 (lrAdd lrRAX lrR11 (lrCompare lrRAX lrRSI (lrJumpIf lrAbove lrLabelFailed (lrStore64 lrRSP lrSlotResume lrRAX (lrAddImmediate lrR9 0xffffffff (lrStore64 lrRSP lrSlotRemaining lrR9 (lrMove lrRAX lrRDX (lrAdd lrRAX lrR10 (lrCompare lrRAX lrRCX (lrJumpIf lrAbove lrLabelFailed (lrLabel lrLabelUnitLoop (lrTest lrR10 (lrJumpIf lrZero lrLabelNext (lrLoad8 lrR11 lrRDI (lrStore8 lrRDX lrR11 (lrAddImmediate lrRDI 1 (lrAddImmediate lrRDX 1 (lrAddImmediate lrR10 0xffffffff (lrJump lrLabelUnitLoop tail)))))))))))))))))))))))))))))))))))))))) in -- Each further copy duplicates the previous copy (rax reads, rdx writes), -- then adds the patch strides to the new copy at r11. (let unrestricted lrNextBlock = (lambda unrestricted tail : A . (lrLabel lrLabelNext (lrLoad64 lrR9 lrRSP lrSlotRemaining (lrTest lrR9 (lrJumpIf lrZero lrLabelRepeatDone (lrAddImmediate lrR9 0xffffffff (lrStore64 lrRSP lrSlotRemaining lrR9 (lrLoad64 lrR10 lrRSP lrSlotUnitLength (lrMove lrRAX lrRDX (lrAdd lrRAX lrR10 (lrCompare lrRAX lrRCX (lrJumpIf lrAbove lrLabelFailed (lrMove lrR11 lrRDX (lrMove lrRAX lrRDX (lrSubtract lrRAX lrR10 (lrLabel lrLabelCopyLoop (lrTest lrR10 (lrJumpIf lrZero lrLabelPatchLoop (lrLoad8 lrR9 lrRAX (lrStore8 lrRDX lrR9 (lrAddImmediate lrRAX 1 (lrAddImmediate lrRDX 1 (lrAddImmediate lrR10 0xffffffff (lrJump lrLabelCopyLoop tail)))))))))))))))))))))))) in -- Patches: r10 counts down, the cursor slot walks the table; r9 is the word -- address, rdi (free inside a repeat) the word, rax the stride. (let unrestricted lrPatchBlock = (lambda unrestricted tail : A . (lrLabel lrLabelPatchLoop (lrLoad64 lrR9 lrRSP lrSlotPatchBase (lrStore64 lrRSP lrSlotPatchCursor lrR9 (lrLoad64 lrR10 lrRSP lrSlotPatchCount (lrLabel lrLabelPatchDone (lrTest lrR10 (lrJumpIf lrZero lrLabelNext (lrLoad64 lrR9 lrRSP lrSlotPatchCursor (lrLoad32 lrRDI lrR9 0 (lrLoad64 lrRAX lrR9 4 (lrAddImmediate lrR9 12 (lrStore64 lrRSP lrSlotPatchCursor lrR9 (lrMove lrR9 lrRDI (lrAddImmediate lrR9 8 (lrLoad64 lrRDI lrRSP lrSlotUnitLength (lrCompare lrR9 lrRDI (lrJumpIf lrAbove lrLabelFailed (lrAddImmediate lrR9 lrMinusEight (lrAdd lrR9 lrR11 (lrLoad64 lrRDI lrR9 0 (lrAdd lrRDI lrRAX (lrStore64 lrR9 0 lrRDI (lrAddImmediate lrR10 0xffffffff (lrJump lrLabelPatchDone tail))))))))))))))))))))))))) in (let unrestricted lrRepeatDoneBlock = (lambda unrestricted tail : A . (lrLabel lrLabelRepeatDone (lrLoad64 lrRDI lrRSP lrSlotResume (lrJump lrLabelLoop tail)))) in (let unrestricted lrDoneBlock = (lambda unrestricted tail : A . (lrLabel lrLabelDone (lrCompare lrRDX lrRCX (lrJumpIf lrNotZero lrLabelFailed (lrCompare lrRDI lrRSI (lrJumpIf lrNotZero lrLabelFailed (lrMove lrRAX lrRDX (lrLoad64 lrR9 lrRSP lrSlotOutputStart (lrSubtract lrRAX lrR9 (lrReturn tail)))))))))) in (let unrestricted lrFailedBlock = (lambda unrestricted tail : A . (lrLabel lrLabelFailed (lrClear lrRAX (lrReturn tail)))) in (lrEntryBlock (lrLoopBlock (lrLiteralBlock (lrZeroBlock (lrRepeatBlock (lrNextBlock (lrPatchBlock (lrRepeatDoneBlock (lrDoneBlock (lrFailedBlock lrEnd))))))))))))))))))))))))))))))