1module Runtime.NativePhysicalMemory
2
3import Data.Bytes
4import Model.Parameter
5import Model.Word64
6import Std.Foundation
7import Std.Natural
8
9-- The interpreter's allocation contains program state, result words, then
10-- repeat and wait state. Both native hosts implement this same layout.
11-- Keep this ABI independent of the program/target owners so admission, memory
12-- reservations and machine emitters share one calculation.
13family NativePhysicalMemoryLayout : Type 0
14constructor NativePhysicalMemoryLayoutOf
15field unrestricted nativePhysicalMemoryStateBytes : Nat
16field unrestricted nativePhysicalMemorySlotBytes : Nat
17field unrestricted nativePhysicalMemoryScratchOffset : Nat
18field unrestricted nativePhysicalMemoryAllocationBytes : Nat
19
20end-family
21
22family NativePhysicalMemoryFailure : Type 0
23constructor NativePhysicalMemoryEmpty
24constructor NativePhysicalMemoryOverflow
25constructor NativePhysicalMemoryPageInvalid
26
27end-family
28
29def nativePhysicalMemoryWordLimit =
30 18446744073709551615
31
32def nativePhysicalMemoryWordBytes =
33 (bytes-length (dataBytesWord64LE (modelWord64FromNaturalTruncated 0)))
34
35-- The ISA shift implementing multiplication by one ABI word; checked below.
36def nativePhysicalMemoryWordShift =
37 3
38
39def nativePhysicalMemoryIterationOffset =
40 0
41
42def nativePhysicalMemoryCountOffset =
43 (naturalAdd nativePhysicalMemoryIterationOffset nativePhysicalMemoryWordBytes)
44
45def nativePhysicalMemoryBodyOffset =
46 (naturalAdd nativePhysicalMemoryCountOffset nativePhysicalMemoryWordBytes)
47
48def nativePhysicalMemoryBodyCountOffset =
49 (naturalAdd nativePhysicalMemoryBodyOffset nativePhysicalMemoryWordBytes)
50
51def nativePhysicalMemoryWaitSecondsOffset =
52 (naturalAdd nativePhysicalMemoryBodyCountOffset nativePhysicalMemoryWordBytes)
53
54def nativePhysicalMemoryWaitNanosOffset =
55 (naturalAdd nativePhysicalMemoryWaitSecondsOffset nativePhysicalMemoryWordBytes)
56
57def nativePhysicalMemoryScratchBytes =
58 (naturalAdd nativePhysicalMemoryWaitNanosOffset nativePhysicalMemoryWordBytes)
59
60def nativePhysicalMemoryAdmitted =
61 (lambda unrestricted state : Nat .
62 (lambda unrestricted slots : Nat .
63 (naturalAnd
64 (naturalNonzero state)
65 (naturalAnd
66 (naturalLessOrEqual
67 state
68 (naturalSaturatingSubtract
69 nativePhysicalMemoryWordLimit
70 nativePhysicalMemoryScratchBytes))
71 (naturalLessOrEqual
72 slots
73 (naturalDivideUnchecked
74 (naturalSaturatingSubtract
75 (naturalSaturatingSubtract
76 nativePhysicalMemoryWordLimit
77 nativePhysicalMemoryScratchBytes)
78 state)
79 nativePhysicalMemoryWordBytes))))))
80
81def planNativePhysicalMemory =
82 (lambda unrestricted state : Nat .
83 (lambda unrestricted slots : Nat .
84 (eliminate
85 StdBool
86 (lambda unrestricted flag : (family StdBool) .
87 (family
88 StdResult
89 (family NativePhysicalMemoryFailure)
90 (family NativePhysicalMemoryLayout)))
91 (stdBoolFromNatural (naturalNonzero state))
92 (branch
93 StdTrue
94 .
95 (eliminate
96 StdBool
97 (lambda unrestricted flag : (family StdBool) .
98 (family
99 StdResult
100 (family NativePhysicalMemoryFailure)
101 (family NativePhysicalMemoryLayout)))
102 (stdBoolFromNatural (nativePhysicalMemoryAdmitted state slots))
103 (branch
104 StdTrue
105 .
106 (let unrestricted slotBytes =
107 (naturalMultiply slots nativePhysicalMemoryWordBytes)
108 in
109 (let unrestricted scratch =
110 (naturalAdd state slotBytes)
111 in
112 (constructor
113 StdResult
114 StdSuccess
115 (family NativePhysicalMemoryFailure)
116 (family NativePhysicalMemoryLayout)
117 (constructor
118 NativePhysicalMemoryLayout
119 NativePhysicalMemoryLayoutOf
120 state
121 slotBytes
122 scratch
123 (naturalAdd scratch nativePhysicalMemoryScratchBytes))))))
124 (branch
125 StdFalse
126 .
127 (constructor
128 StdResult
129 StdFailure
130 (family NativePhysicalMemoryFailure)
131 (family NativePhysicalMemoryLayout)
132 (constructor NativePhysicalMemoryFailure NativePhysicalMemoryOverflow)))))
133 (branch
134 StdFalse
135 .
136 (constructor
137 StdResult
138 StdFailure
139 (family NativePhysicalMemoryFailure)
140 (family NativePhysicalMemoryLayout)
141 (constructor NativePhysicalMemoryFailure NativePhysicalMemoryEmpty))))))
142
143def nativePhysicalMemoryBytes =
144 (lambda unrestricted layout : (family NativePhysicalMemoryLayout) .
145 (eliminate
146 NativePhysicalMemoryLayout
147 (lambda unrestricted current : (family NativePhysicalMemoryLayout) . Nat)
148 layout
149 (branch NativePhysicalMemoryLayoutOf state slots scratch bytes . bytes)))
150
151-- Mapping granularity is a platform/deployment fact, never guessed from a
152-- neighboring host. This accepts a positive declared quantum; its provenance
153-- and agreement with the actual OS mapping remain the target's responsibility.
154def nativeMemoryMappedBytes =
155 (lambda unrestricted quantum : Nat .
156 (lambda unrestricted bytes : Nat .
157 (eliminate
158 StdBool
159 (lambda unrestricted flag : (family StdBool) .
160 (family StdResult (family NativePhysicalMemoryFailure) Nat))
161 (stdBoolFromNatural
162 (naturalAnd
163 (naturalNonzero quantum)
164 (naturalAnd
165 (naturalLessOrEqual quantum nativePhysicalMemoryWordLimit)
166 (naturalAnd
167 (naturalNonzero bytes)
168 (naturalLessOrEqual bytes nativePhysicalMemoryWordLimit)))))
169 (branch
170 StdTrue
171 .
172 (let unrestricted pages =
173 (naturalAdd (naturalDivideUnchecked (naturalSaturatingSubtract bytes 1) quantum) 1)
174 in
175 (eliminate
176 StdBool
177 (lambda unrestricted flag : (family StdBool) .
178 (family StdResult (family NativePhysicalMemoryFailure) Nat))
179 (stdBoolFromNatural
180 (naturalLessOrEqual
181 pages
182 (naturalDivideUnchecked nativePhysicalMemoryWordLimit quantum)))
183 (branch
184 StdTrue
185 .
186 (constructor
187 StdResult
188 StdSuccess
189 (family NativePhysicalMemoryFailure)
190 Nat
191 (naturalMultiply pages quantum)))
192 (branch
193 StdFalse
194 .
195 (constructor
196 StdResult
197 StdFailure
198 (family NativePhysicalMemoryFailure)
199 Nat
200 (constructor NativePhysicalMemoryFailure NativePhysicalMemoryOverflow))))))
201 (branch
202 StdFalse
203 .
204 (constructor
205 StdResult
206 StdFailure
207 (family NativePhysicalMemoryFailure)
208 Nat
209 (constructor NativePhysicalMemoryFailure NativePhysicalMemoryPageInvalid))))))
210
211def nativePhysicalMemoryMappedBytes =
212 (lambda unrestricted quantum : Nat .
213 (lambda unrestricted layout : (family NativePhysicalMemoryLayout) .
214 (nativeMemoryMappedBytes quantum (nativePhysicalMemoryBytes layout))))
215
216def nativePhysicalMemoryWordShiftLaw :
217 (equal Nat (naturalPowerOfTwo nativePhysicalMemoryWordShift) nativePhysicalMemoryWordBytes) =
218 (refl Nat 8)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.