1module Runtime.NativePointwisePlan
2
3import Component.Pointwise
4import Runtime.NativeFloatPlan
5import Runtime.NativeLaunchRecipeLoad
6import Runtime.NativeMemoryPlan
7import Runtime.NativePhysicalProgram
8import Data.Bytes
9import Model.Word64
10import Std.Fin
11import Std.List
12import Std.Foundation
13import Std.Natural
14import Std.Word
15
16family NativePointwiseFragment : Type 0
17constructor NativePointwiseFragmentOf
18field unrestricted nativePointwiseFragmentCommands : (pi unrestricted tail : (family NativePhysicalCommands) . (family NativePhysicalCommands))
19field unrestricted nativePointwiseFragmentResult : Nat
20field unrestricted nativePointwiseFragmentEnd : Nat
21
22end-family
23
24-- This is an explicitly selected native host realization. The state occupies
25-- a contiguous word region followed by derived expression scratch. No GPU
26-- operation can choose these commands as a fallback. Arithmetic is finite,
27-- separately rounded binary64; refusal prevents publication of a partial step.
28def nativePointwiseWordBytes : Nat =
29 (bytes-length (dataBytesWord64LE modelWord64Zero))
30
31def nativePointwiseAt =
32 (lambda unrestricted base : Nat .
33 (lambda unrestricted index : Nat .
34 (naturalAdd base (naturalMultiply nativePointwiseWordBytes index))))
35
36def nativePointwiseExtent =
37 (lambda unrestricted slots : Nat .
38 (lambda unrestricted program : (family StdList (family PointwiseAssignment StdU64 slots)) .
39 (lambda unrestricted base : Nat .
40 (nativePointwiseAt
41 base
42 (naturalAdd slots (pointwiseProgramTemporaryValues StdU64 slots program))))))
43
44def nativePointwiseCode =
45 (lambda unrestricted fragment : (family NativePointwiseFragment) .
46 (eliminate
47 NativePointwiseFragment
48 (lambda unrestricted current : (family NativePointwiseFragment) .
49 (pi unrestricted tail : (family NativePhysicalCommands) . (family NativePhysicalCommands)))
50 fragment
51 (branch NativePointwiseFragmentOf code result end . code)))
52
53def nativePointwiseResult =
54 (lambda unrestricted fragment : (family NativePointwiseFragment) .
55 (eliminate
56 NativePointwiseFragment
57 (lambda unrestricted current : (family NativePointwiseFragment) . Nat)
58 fragment
59 (branch NativePointwiseFragmentOf code result end . result)))
60
61def nativePointwiseEnd =
62 (lambda unrestricted fragment : (family NativePointwiseFragment) .
63 (eliminate
64 NativePointwiseFragment
65 (lambda unrestricted current : (family NativePointwiseFragment) . Nat)
66 fragment
67 (branch NativePointwiseFragmentOf code result end . end)))
68
69def nativePointwiseUnarySupported =
70 (lambda unrestricted operation : (family PointwiseUnary) .
71 (eliminate
72 PointwiseUnary
73 (lambda unrestricted current : (family PointwiseUnary) . Nat)
74 operation
75 (branch PointwiseNegate . 1)
76 (branch PointwiseSquare . 1)
77 (branch PointwiseRoundBF16 . 0)
78 (branch PointwiseReciprocal . 1)
79 (branch PointwiseReciprocalSquareRoot . 0)
80 (branch PointwiseSquareRoot . 1)
81 (branch PointwiseTanh . 0)
82 (branch PointwiseExponentialBase2 . 0)))
83
84def nativePointwiseBinarySupported =
85 (lambda unrestricted operation : (family PointwiseBinary) .
86 (eliminate
87 PointwiseBinary
88 (lambda unrestricted current : (family PointwiseBinary) . Nat)
89 operation
90 (branch PointwiseAdd . 1)
91 (branch PointwiseMultiply . 1)
92 (branch PointwiseSubtract . 1)
93 (branch PointwisePositiveGate . 0)))
94
95def nativePointwiseSupported =
96 (lambda unrestricted slots : Nat .
97 (lambda unrestricted program : (family StdList (family PointwiseAssignment StdU64 slots)) .
98 (stdListFold
99 (family PointwiseAssignment StdU64 slots)
100 Nat
101 (lambda unrestricted assignment : (family PointwiseAssignment StdU64 slots) .
102 (lambda unrestricted rest : Nat .
103 (eliminate
104 PointwiseAssignment
105 (lambda unrestricted current : (family PointwiseAssignment StdU64 slots) . Nat)
106 assignment
107 (branch
108 PointwiseAssign
109 destination
110 expression
111 .
112 (naturalAnd
113 rest
114 (pointwiseFold
115 StdU64
116 Nat
117 slots
118 (lambda unrestricted operation : (family PointwiseUnary) .
119 (lambda unrestricted child : Nat .
120 (naturalAnd (nativePointwiseUnarySupported operation) child)))
121 (lambda unrestricted operation : (family PointwiseBinary) .
122 (lambda unrestricted left : Nat .
123 (lambda unrestricted right : Nat .
124 (naturalAnd
125 (nativePointwiseBinarySupported operation)
126 (naturalAnd left right)))))
127 (lambda unrestricted word : StdU64 . 1)
128 expression
129 (lambda unrestricted index : (family StdFin slots) . 1)))))))
130 1
131 program)))
132
133def nativePointwiseAdmitted =
134 (lambda unrestricted slots : Nat .
135 (lambda unrestricted program : (family StdList (family PointwiseAssignment StdU64 slots)) .
136 (lambda unrestricted base : Nat .
137 (lambda unrestricted available : Nat .
138 (naturalAnd
139 (nativePointwiseSupported slots program)
140 (naturalAnd
141 (naturalIsZero (naturalModuloUnchecked base nativePointwiseWordBytes))
142 (naturalAnd
143 (naturalLessOrEqual (nativePointwiseExtent slots program base) available)
144 (naturalBelowTwoPower 64 (nativePointwiseExtent slots program base)))))))))
145
146-- Adding the sign bit modulo 2^64 flips it without rounding and preserves both
147-- zero signs. Subtracting from +0 would not implement negation of +0 correctly.
148def nativePointwiseNegate =
149 (lambda unrestricted scratch : Nat .
150 (lambda unrestricted destination : Nat .
151 (lambda unrestricted source : Nat .
152 (lambda unrestricted tail : (family NativePhysicalCommands) .
153 (nativeFloat64RequireFinite
154 (nativeMemoryLoad source)
155 scratch
156 b"pointwise-nonfinite"
157 (nativeLaunchRecipeCommand
158 (constructor
159 NativePhysicalOperation
160 NativePhysicalAddWord64
161 (nativeMemoryState destination)
162 (nativeMemoryLoad source)
163 (nativeLaunchRecipeImmediate (naturalPowerOfTwo 63)))
164 b"pointwise-negate"
165 tail))))))
166
167-- binary64 1.0, the dividend of a reciprocal
168def nativePointwiseOneBits : Nat =
169 0x3ff0000000000000
170
171-- Binary64 under the native finite profile (Runtime.NativeFloatPlan):
172-- negation flips the sign bit; square, reciprocal (1 / x) and square root are
173-- single correctly rounded operations; any nonfinite operand or result
174-- refuses. A reciprocal square root would be two roundings here, unlike the
175-- device profiles' single approximate operation, so it is not admitted.
176def nativePointwiseUnary =
177 (lambda unrestricted scratch : Nat .
178 (lambda unrestricted operation : (family PointwiseUnary) .
179 (lambda unrestricted destination : Nat .
180 (lambda unrestricted source : Nat .
181 (lambda unrestricted tail : (family NativePhysicalCommands) .
182 (eliminate
183 PointwiseUnary
184 (lambda unrestricted current : (family PointwiseUnary) .
185 (family NativePhysicalCommands))
186 operation
187 (branch PointwiseNegate . (nativePointwiseNegate scratch destination source tail))
188 (branch
189 PointwiseSquare
190 .
191 (nativeFiniteFloat64Binary
192 b"pointwise-nonfinite"
193 scratch
194 (constructor NativePhysicalFloat64Operation NativePhysicalFloat64Multiply)
195 destination
196 source
197 source
198 tail))
199 (branch PointwiseRoundBF16 . tail)
200 (branch
201 PointwiseReciprocal
202 .
203 (nativeMemoryStoreWord64
204 b"pointwise-one"
205 destination
206 (nativeLaunchRecipeImmediate nativePointwiseOneBits)
207 (nativeFiniteFloat64Binary
208 b"pointwise-nonfinite"
209 scratch
210 (constructor NativePhysicalFloat64Operation NativePhysicalFloat64Divide)
211 destination
212 destination
213 source
214 tail)))
215 (branch PointwiseReciprocalSquareRoot . tail)
216 (branch
217 PointwiseSquareRoot
218 .
219 (nativeFiniteFloat64Binary
220 b"pointwise-nonfinite"
221 scratch
222 (constructor NativePhysicalFloat64Operation NativePhysicalFloat64SquareRoot)
223 destination
224 source
225 source
226 tail))
227 (branch PointwiseTanh . tail)
228 (branch PointwiseExponentialBase2 . tail)))))))
229
230def nativePointwiseBinary =
231 (lambda unrestricted scratch : Nat .
232 (lambda unrestricted operation : (family PointwiseBinary) .
233 (lambda unrestricted destination : Nat .
234 (lambda unrestricted left : Nat .
235 (lambda unrestricted right : Nat .
236 (lambda unrestricted tail : (family NativePhysicalCommands) .
237 (eliminate
238 PointwiseBinary
239 (lambda unrestricted current : (family PointwiseBinary) .
240 (family NativePhysicalCommands))
241 operation
242 (branch
243 PointwiseAdd
244 .
245 (nativeFiniteFloat64Binary
246 b"pointwise-nonfinite"
247 scratch
248 (constructor NativePhysicalFloat64Operation NativePhysicalFloat64Add)
249 destination
250 left
251 right
252 tail))
253 (branch
254 PointwiseMultiply
255 .
256 (nativeFiniteFloat64Binary
257 b"pointwise-nonfinite"
258 scratch
259 (constructor NativePhysicalFloat64Operation NativePhysicalFloat64Multiply)
260 destination
261 left
262 right
263 tail))
264 (branch
265 PointwiseSubtract
266 .
267 (nativeFiniteFloat64Binary
268 b"pointwise-nonfinite"
269 scratch
270 (constructor NativePhysicalFloat64Operation NativePhysicalFloat64Subtract)
271 destination
272 left
273 right
274 tail))
275 (branch PointwisePositiveGate . tail))))))))
276
277-- Unsupported branches above are excluded by nativePointwiseProgram's erased
278-- admission proof. Inputs name existing slots; every other node materializes a
279-- fresh temporary. Explicit assignments then make their result visible to the
280-- next expression, using the same dependency order as the SM86 realization.
281def nativePointwiseExpression =
282 (lambda unrestricted slots : Nat .
283 (lambda unrestricted base : Nat .
284 (lambda unrestricted scratch : Nat .
285 (lambda unrestricted expression : (family PointwiseExpression StdU64 slots) .
286 (pointwiseFold
287 StdU64
288 (pi unrestricted next : Nat . (family NativePointwiseFragment))
289 slots
290 (lambda unrestricted operation : (family PointwiseUnary) .
291 (lambda unrestricted operand : (pi unrestricted next : Nat . (family NativePointwiseFragment)) .
292 (lambda unrestricted next : Nat .
293 (let unrestricted child =
294 (operand next)
295 in
296 (constructor
297 NativePointwiseFragment
298 NativePointwiseFragmentOf
299 (lambda unrestricted tail : (family NativePhysicalCommands) .
300 (nativePointwiseCode
301 child
302 (nativePointwiseUnary
303 scratch
304 operation
305 (nativePointwiseEnd child)
306 (nativePointwiseResult child)
307 tail)))
308 (nativePointwiseEnd child)
309 (nativePointwiseAt (nativePointwiseEnd child) 1))))))
310 (lambda unrestricted operation : (family PointwiseBinary) .
311 (lambda unrestricted left : (pi unrestricted next : Nat . (family NativePointwiseFragment)) .
312 (lambda unrestricted right : (pi unrestricted next : Nat . (family NativePointwiseFragment)) .
313 (lambda unrestricted next : Nat .
314 (let unrestricted l =
315 (left next)
316 in
317 (let unrestricted r =
318 (right (nativePointwiseEnd l))
319 in
320 (constructor
321 NativePointwiseFragment
322 NativePointwiseFragmentOf
323 (lambda unrestricted tail : (family NativePhysicalCommands) .
324 (nativePointwiseCode
325 l
326 (nativePointwiseCode
327 r
328 (nativePointwiseBinary
329 scratch
330 operation
331 (nativePointwiseEnd r)
332 (nativePointwiseResult l)
333 (nativePointwiseResult r)
334 tail))))
335 (nativePointwiseEnd r)
336 (nativePointwiseAt (nativePointwiseEnd r) 1))))))))
337 (lambda unrestricted bits : StdU64 .
338 (lambda unrestricted next : Nat .
339 (constructor
340 NativePointwiseFragment
341 NativePointwiseFragmentOf
342 (nativeMemoryStoreWord64
343 b"pointwise-literal"
344 next
345 (nativeLaunchRecipeImmediate (modelWord64Natural bits)))
346 next
347 (nativePointwiseAt next 1))))
348 expression
349 (lambda unrestricted index : (family StdFin slots) .
350 (lambda unrestricted next : Nat .
351 (constructor
352 NativePointwiseFragment
353 NativePointwiseFragmentOf
354 (lambda unrestricted tail : (family NativePhysicalCommands) . tail)
355 (nativePointwiseAt base (stdFinToNatural slots index))
356 next))))))))
357
358def nativePointwiseCommands =
359 (lambda unrestricted slots : Nat .
360 (lambda unrestricted program : (family StdList (family PointwiseAssignment StdU64 slots)) .
361 (lambda unrestricted base : Nat .
362 (lambda unrestricted available : Nat .
363 (lambda unrestricted scratch : Nat .
364 (lambda unrestricted tail : (family NativePhysicalCommands) .
365 (stdListFold
366 (family PointwiseAssignment StdU64 slots)
367 (family NativePhysicalCommands)
368 (lambda unrestricted assignment : (family PointwiseAssignment StdU64 slots) .
369 (lambda unrestricted rest : (family NativePhysicalCommands) .
370 (eliminate
371 PointwiseAssignment
372 (lambda unrestricted current : (family PointwiseAssignment StdU64 slots) .
373 (family NativePhysicalCommands))
374 assignment
375 (branch
376 PointwiseAssign
377 destination
378 expression
379 .
380 (let unrestricted fragment =
381 (nativePointwiseExpression
382 slots
383 base
384 scratch
385 expression
386 (nativePointwiseAt base slots))
387 in
388 (nativePointwiseCode
389 fragment
390 (nativeFloat64RequireFinite
391 (nativeMemoryLoad (nativePointwiseResult fragment))
392 scratch
393 b"pointwise-nonfinite"
394 (nativeMemoryStoreWord64
395 b"pointwise-assignment"
396 (nativePointwiseAt base (stdFinToNatural slots destination))
397 (nativeMemoryLoad (nativePointwiseResult fragment))
398 rest))))))))
399 tail
400 program)))))))
401
402-- The raw command fold above is internal to these two admission entries.
403def nativePointwiseProgram =
404 (lambda unrestricted slots : Nat .
405 (lambda unrestricted program : (family StdList (family PointwiseAssignment StdU64 slots)) .
406 (lambda unrestricted base : Nat .
407 (lambda unrestricted available : Nat .
408 (lambda unrestricted scratch : Nat .
409 (lambda erased admitted : (equal Nat (nativePointwiseAdmitted slots program base available) 1) .
410 (nativePointwiseCommands slots program base available scratch)))))))
411
412def planNativePointwiseProgram =
413 (lambda unrestricted slots : Nat .
414 (lambda unrestricted program : (family StdList (family PointwiseAssignment StdU64 slots)) .
415 (lambda unrestricted base : Nat .
416 (lambda unrestricted available : Nat .
417 (lambda unrestricted scratch : Nat .
418 (lambda unrestricted tail : (family NativePhysicalCommands) .
419 (nat-eliminate
420 (lambda unrestricted valid : Nat .
421 (family StdResult Bytes (family NativePhysicalCommands)))
422 (constructor
423 StdResult
424 StdFailure
425 Bytes
426 (family NativePhysicalCommands)
427 b"pointwise-program-admission")
428 (lambda unrestricted previous : Nat .
429 (lambda unrestricted ignored : (family StdResult Bytes (family NativePhysicalCommands)) .
430 (constructor
431 StdResult
432 StdSuccess
433 Bytes
434 (family NativePhysicalCommands)
435 (nativePointwiseCommands slots program base available scratch tail))))
436 (nativePointwiseAdmitted slots program base available))))))))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.