Map the staging area once, at a fixed address the artifact reserves for it.
Its extent must cover the longest recipe the host loads.
69def nativeLaunchRecipeStagingCommands =
70 (lambda unrestricted stagingAddress : Nat .
71 (lambda unrestricted stagingExtent : Nat .
72 (lambda unrestricted resultSlot : Nat .
73 (lambda unrestricted errorIdentity : Bytes .
74 (lambda unrestricted tail : (family NativePhysicalCommands) .
75 (nativeLaunchRecipeCommand
76 (constructor NativePhysicalOperation NativePhysicalSystemCall
77 (nativeLaunchRecipeImmediate 9)
78 (constructor NativePhysicalArguments NativePhysicalArgumentsValue
79 (nativeLaunchRecipeImmediate stagingAddress)
80 (nativeLaunchRecipeImmediate stagingExtent)
81 (nativeLaunchRecipeImmediate nativeLaunchRecipeMapProtection)
82 (nativeLaunchRecipeImmediate nativeLaunchRecipeMapFlags)
83 (nativeLaunchRecipeImmediate nativeLaunchRecipeNoDescriptor)
84 (nativeLaunchRecipeImmediate 0))
85 b""
86 (nativeLaunchRecipeStore resultSlot))
87 errorIdentity
88 (nativeLaunchRecipeAssertEqual
89 (nativeLaunchRecipeSlotValue resultSlot)
90 (nativeLaunchRecipeImmediate stagingAddress)
91 errorIdentity
92 tail)))))))The compiler supplied declaration spans and resolved links from this source snapshot. This page does not assert that this file belongs to a checked closure.