module Runtime.NativeLaunchRecipeLoad

import Model.Config
import Model.Parameter
import Model.Word64
import Runtime.NativeLaunchRecipeRoutine
import Runtime.NativePhysicalProgram
import Std.Natural

-- The host-program commands that bring one embedded launch-table recipe into
-- a mapped arena: read the recipe from the executable into a staging area,
-- expand it in place with the shared routine, and require the exact extent.
-- Every system's host program loads its program, QMD, pushbuffer and GPFIFO
-- components through this fragment; nothing here knows a system or a card.

def nativeLaunchRecipeWord =
  (lambda unrestricted value : Nat . (modelWord64FromNaturalTruncated value))

def nativeLaunchRecipeImmediate =
  (lambda unrestricted value : Nat .
    (constructor NativePhysicalOperand NativePhysicalImmediate (nativeLaunchRecipeWord value)))

def nativeLaunchRecipeSlot =
  (lambda unrestricted index : Nat .
    (constructor NativePhysicalSlot NativePhysicalSlotValue (nativeLaunchRecipeWord index)))

def nativeLaunchRecipeSlotValue =
  (lambda unrestricted index : Nat .
    (constructor NativePhysicalOperand NativePhysicalResultValue (nativeLaunchRecipeSlot index)))

def nativeLaunchRecipeStore =
  (lambda unrestricted index : Nat .
    (constructor NativePhysicalResultBinding NativePhysicalStoreResult (nativeLaunchRecipeSlot index)))

def nativeLaunchRecipeArguments =
  (lambda unrestricted a0 : (family NativePhysicalOperand) .
    (lambda unrestricted a1 : (family NativePhysicalOperand) .
      (lambda unrestricted a2 : (family NativePhysicalOperand) .
        (lambda unrestricted a3 : (family NativePhysicalOperand) .
          (constructor NativePhysicalArguments NativePhysicalArgumentsValue
            a0 a1 a2 a3 (nativeLaunchRecipeImmediate 0) (nativeLaunchRecipeImmediate 0))))))

def nativeLaunchRecipeCommand =
  (lambda unrestricted operation : (family NativePhysicalOperation) .
    (lambda unrestricted errorIdentity : Bytes .
      (lambda unrestricted tail : (family NativePhysicalCommands) .
        (constructor NativePhysicalCommands NativePhysicalCommandsNext
          (constructor NativePhysicalCommand NativePhysicalCommandValue operation errorIdentity)
          tail))))

def nativeLaunchRecipeAssertEqual =
  (lambda unrestricted left : (family NativePhysicalOperand) .
    (lambda unrestricted right : (family NativePhysicalOperand) .
      (lambda unrestricted errorIdentity : Bytes .
        (lambda unrestricted tail : (family NativePhysicalCommands) .
          (nativeLaunchRecipeCommand
            (constructor NativePhysicalOperation NativePhysicalAssertEqual left right
              (constructor NativePhysicalErrorCode NativePhysicalExecutionAssertionFailed))
            errorIdentity
            tail)))))

-- PROT_READ | PROT_WRITE and MAP_PRIVATE | MAP_FIXED | MAP_ANONYMOUS.
def nativeLaunchRecipeMapProtection : Nat = 3
def nativeLaunchRecipeMapFlags : Nat = 50
def nativeLaunchRecipeNoDescriptor : Nat = 18446744073709551615

-- Map the staging area once, at a fixed address the artifact reserves for it.
-- Its extent must cover the longest recipe the host loads.
def nativeLaunchRecipeStagingCommands =
  (lambda unrestricted stagingAddress : Nat .
    (lambda unrestricted stagingExtent : Nat .
      (lambda unrestricted resultSlot : Nat .
        (lambda unrestricted errorIdentity : Bytes .
          (lambda unrestricted tail : (family NativePhysicalCommands) .
            (nativeLaunchRecipeCommand
              (constructor NativePhysicalOperation NativePhysicalSystemCall
                (nativeLaunchRecipeImmediate 9)
                (constructor NativePhysicalArguments NativePhysicalArgumentsValue
                  (nativeLaunchRecipeImmediate stagingAddress)
                  (nativeLaunchRecipeImmediate stagingExtent)
                  (nativeLaunchRecipeImmediate nativeLaunchRecipeMapProtection)
                  (nativeLaunchRecipeImmediate nativeLaunchRecipeMapFlags)
                  (nativeLaunchRecipeImmediate nativeLaunchRecipeNoDescriptor)
                  (nativeLaunchRecipeImmediate 0))
                b""
                (nativeLaunchRecipeStore resultSlot))
              errorIdentity
              (nativeLaunchRecipeAssertEqual
                (nativeLaunchRecipeSlotValue resultSlot)
                (nativeLaunchRecipeImmediate stagingAddress)
                errorIdentity
                tail)))))))

-- Load one recipe: pread64 it from the executable at its component offset
-- into the staging area, expand it into the destination, and require the
-- routine to report exactly the table's extent.  `executable` is the operand
-- holding the /proc/self/exe descriptor.
def nativeLaunchRecipeLoadCommands =
  (lambda unrestricted executable : (family NativePhysicalOperand) .
    (lambda unrestricted stagingAddress : Nat .
      (lambda unrestricted recipeOffset : Nat .
        (lambda unrestricted recipeExtent : Nat .
          (lambda unrestricted destination : Nat .
            (lambda unrestricted tableExtent : Nat .
              (lambda unrestricted resultSlot : Nat .
                (lambda unrestricted errorIdentity : Bytes .
                  (lambda unrestricted tail : (family NativePhysicalCommands) .
                    (nativeLaunchRecipeCommand
                      (constructor NativePhysicalOperation NativePhysicalSystemCall
                        (nativeLaunchRecipeImmediate 17)
                        (nativeLaunchRecipeArguments
                          executable
                          (nativeLaunchRecipeImmediate stagingAddress)
                          (nativeLaunchRecipeImmediate recipeExtent)
                          (nativeLaunchRecipeImmediate recipeOffset))
                        b""
                        (nativeLaunchRecipeStore resultSlot))
                      errorIdentity
                      (nativeLaunchRecipeAssertEqual
                        (nativeLaunchRecipeSlotValue resultSlot)
                        (nativeLaunchRecipeImmediate recipeExtent)
                        errorIdentity
                        (nativeLaunchRecipeCommand
                          (constructor NativePhysicalOperation NativePhysicalMachineRoutine
                            nativeLaunchRecipeRoutineBytes
                            (nativeLaunchRecipeArguments
                              (nativeLaunchRecipeImmediate stagingAddress)
                              (nativeLaunchRecipeImmediate recipeExtent)
                              (nativeLaunchRecipeImmediate destination)
                              (nativeLaunchRecipeImmediate tableExtent))
                            (nativeLaunchRecipeStore resultSlot))
                          errorIdentity
                          (nativeLaunchRecipeAssertEqual
                            (nativeLaunchRecipeSlotValue resultSlot)
                            (nativeLaunchRecipeImmediate tableExtent)
                            errorIdentity
                            tail)))))))))))))

-- The same load with the offsets and extents already as machine words, for
-- host programs that carry their layout as ModelWord64 values.
def nativeLaunchRecipeWordImmediate =
  (lambda unrestricted value : (family ModelWord64) .
    (constructor NativePhysicalOperand NativePhysicalImmediate value))

def nativeLaunchRecipeLoadWords =
  (lambda unrestricted executable : (family NativePhysicalOperand) .
    (lambda unrestricted stagingAddress : Nat .
      (lambda unrestricted recipeOffset : (family ModelWord64) .
        (lambda unrestricted recipeExtent : (family ModelWord64) .
          (lambda unrestricted destination : Nat .
            (lambda unrestricted tableExtent : (family ModelWord64) .
              (lambda unrestricted resultSlot : Nat .
                (lambda unrestricted errorIdentity : Bytes .
                  (lambda unrestricted tail : (family NativePhysicalCommands) .
                    (nativeLaunchRecipeCommand
                      (constructor NativePhysicalOperation NativePhysicalSystemCall
                        (nativeLaunchRecipeImmediate 17)
                        (nativeLaunchRecipeArguments
                          executable
                          (nativeLaunchRecipeImmediate stagingAddress)
                          (nativeLaunchRecipeWordImmediate recipeExtent)
                          (nativeLaunchRecipeWordImmediate recipeOffset))
                        b""
                        (nativeLaunchRecipeStore resultSlot))
                      errorIdentity
                      (nativeLaunchRecipeAssertEqual
                        (nativeLaunchRecipeSlotValue resultSlot)
                        (nativeLaunchRecipeWordImmediate recipeExtent)
                        errorIdentity
                        (nativeLaunchRecipeCommand
                          (constructor NativePhysicalOperation NativePhysicalMachineRoutine
                            nativeLaunchRecipeRoutineBytes
                            (nativeLaunchRecipeArguments
                              (nativeLaunchRecipeImmediate stagingAddress)
                              (nativeLaunchRecipeWordImmediate recipeExtent)
                              (nativeLaunchRecipeImmediate destination)
                              (nativeLaunchRecipeWordImmediate tableExtent))
                            (nativeLaunchRecipeStore resultSlot))
                          errorIdentity
                          (nativeLaunchRecipeAssertEqual
                            (nativeLaunchRecipeSlotValue resultSlot)
                            (nativeLaunchRecipeWordImmediate tableExtent)
                            errorIdentity
                            tail)))))))))))))

-- The same load with the recipe's offset and extent as operands: the words a
-- host read from its own manifest at run time, so the host program needs no
-- build-time knowledge of where the linker put the recipe.
def nativeLaunchRecipeLoadOperands =
  (lambda unrestricted executable : (family NativePhysicalOperand) .
    (lambda unrestricted stagingAddress : Nat .
      (lambda unrestricted recipeOffset : (family NativePhysicalOperand) .
        (lambda unrestricted recipeExtent : (family NativePhysicalOperand) .
          (lambda unrestricted destination : Nat .
            (lambda unrestricted tableExtent : Nat .
              (lambda unrestricted resultSlot : Nat .
                (lambda unrestricted errorIdentity : Bytes .
                  (lambda unrestricted tail : (family NativePhysicalCommands) .
                    (nativeLaunchRecipeCommand
                      (constructor NativePhysicalOperation NativePhysicalSystemCall
                        (nativeLaunchRecipeImmediate 17)
                        (nativeLaunchRecipeArguments
                          executable
                          (nativeLaunchRecipeImmediate stagingAddress)
                          recipeExtent
                          recipeOffset)
                        b""
                        (nativeLaunchRecipeStore resultSlot))
                      errorIdentity
                      (nativeLaunchRecipeAssertEqual
                        (nativeLaunchRecipeSlotValue resultSlot)
                        recipeExtent
                        errorIdentity
                        (nativeLaunchRecipeCommand
                          (constructor NativePhysicalOperation NativePhysicalMachineRoutine
                            nativeLaunchRecipeRoutineBytes
                            (nativeLaunchRecipeArguments
                              (nativeLaunchRecipeImmediate stagingAddress)
                              recipeExtent
                              (nativeLaunchRecipeImmediate destination)
                              (nativeLaunchRecipeImmediate tableExtent))
                            (nativeLaunchRecipeStore resultSlot))
                          errorIdentity
                          (nativeLaunchRecipeAssertEqual
                            (nativeLaunchRecipeSlotValue resultSlot)
                            (nativeLaunchRecipeImmediate tableExtent)
                            errorIdentity
                            tail)))))))))))))