Runtime.NativeMemoryPlan

1module Runtime.NativeMemoryPlan
2
3import Runtime.NativeMemoryRoutine
4import Runtime.NativePhysicalProgram
5import Runtime.NativeLaunchRecipeLoad
6import Model.Word64
7import Std.Natural
8
9-- Native commands over admitted host regions. Allocation and nonoverlap are
10-- planner obligations; these are shared by frames and durable state staging.
11def nativeMemoryState =
12  (lambda unrestricted offset : Nat .
13    (constructor
14      NativePhysicalOperand
15      NativePhysicalStateAddress
16      (modelWord64FromNaturalTruncated offset)))
17
18def nativeMemoryLoad =
19  (lambda unrestricted offset : Nat .
20    (constructor
21      NativePhysicalOperand
22      NativePhysicalStateLoad64
23      (modelWord64FromNaturalTruncated offset)))
24
25def nativeMemoryCopyPayload =
26  (lambda unrestricted offset : Nat .
27    (lambda unrestricted bytes : Bytes .
28      (lambda unrestricted tail : (family NativePhysicalCommands) .
29        (nat-eliminate
30          (lambda unrestricted count : Nat . (family NativePhysicalCommands))
31          tail
32          (lambda unrestricted previous : Nat .
33            (lambda unrestricted ignored : (family NativePhysicalCommands) .
34              (nativeLaunchRecipeCommand
35                (constructor
36                  NativePhysicalOperation
37                  NativePhysicalCopyPayloadToState
38                  (modelWord64FromNaturalTruncated offset)
39                  (modelWord64FromNaturalTruncated (bytes-length bytes))
40                  bytes)
41                b"memory-copy"
42                tail)))
43          (naturalNonzero (bytes-length bytes))))))
44
45def nativeMemoryCopyOperands =
46  (lambda unrestricted destination : (family NativePhysicalOperand) .
47    (lambda unrestricted source : (family NativePhysicalOperand) .
48      (lambda unrestricted extent : Nat .
49        (lambda unrestricted slot : Nat .
50          (lambda unrestricted error : Bytes .
51            (lambda unrestricted tail : (family NativePhysicalCommands) .
52              (nativeLaunchRecipeCommand
53                (constructor
54                  NativePhysicalOperation
55                  NativePhysicalMachineRoutine
56                  nativeMemoryCopyCode
57                  (nativeLaunchRecipeArguments
58                    destination
59                    source
60                    (nativeLaunchRecipeImmediate extent)
61                    (nativeLaunchRecipeImmediate 0))
62                  (nativeLaunchRecipeStore slot))
63                error
64                (nativeLaunchRecipeAssertEqual
65                  (nativeLaunchRecipeSlotValue slot)
66                  (nativeLaunchRecipeImmediate 0)
67                  error
68                  tail))))))))
69
70def nativeMemoryCompareOperands =
71  (lambda unrestricted left : (family NativePhysicalOperand) .
72    (lambda unrestricted right : (family NativePhysicalOperand) .
73      (lambda unrestricted extent : Nat .
74        (lambda unrestricted slot : Nat .
75          (lambda unrestricted error : Bytes .
76            (lambda unrestricted tail : (family NativePhysicalCommands) .
77              (nativeLaunchRecipeCommand
78                (constructor
79                  NativePhysicalOperation
80                  NativePhysicalMachineRoutine
81                  nativeMemoryEqualCode
82                  (nativeLaunchRecipeArguments
83                    left
84                    right
85                    (nativeLaunchRecipeImmediate extent)
86                    (nativeLaunchRecipeImmediate 0))
87                  (nativeLaunchRecipeStore slot))
88                error
89                (nativeLaunchRecipeAssertEqual
90                  (nativeLaunchRecipeSlotValue slot)
91                  (nativeLaunchRecipeImmediate 1)
92                  error
93                  tail))))))))
94
95def nativeMemoryCompareRegions =
96  (lambda unrestricted left : Nat .
97    (lambda unrestricted right : Nat .
98      (lambda unrestricted extent : Nat .
99        (nativeMemoryCompareOperands (nativeMemoryState left) (nativeMemoryState right) extent))))
100
101-- Store one explicit runtime word; caller admission owns the destination.
102def nativeMemoryStoreWord64 =
103  (lambda unrestricted error : Bytes .
104    (lambda unrestricted destination : Nat .
105      (lambda unrestricted value : (family NativePhysicalOperand) .
106        (nativeLaunchRecipeCommand
107          (constructor
108            NativePhysicalOperation
109            NativePhysicalStoreWord64
110            (nativeMemoryState destination)
111            value)
112          error))))