1module Runtime.NativePhysicalProgramComposer
2
3import Model.Word64
4import Runtime.NativePhysicalProgram
5import Std.Natural
6import Model.Parameter
7
8family NativePhysicalProgramComposeAddressClass : Type 0
9constructor NativePhysicalProgramComposeStateAddress
10constructor NativePhysicalProgramComposeResultSlot
11constructor NativePhysicalProgramComposePayloadAddress
12constructor NativePhysicalProgramComposeStateExtent
13constructor NativePhysicalProgramComposeResultExtent
14end-family
15
16family NativePhysicalProgramComposeErrorCode : Type 0
17constructor NativePhysicalProgramComposeIdentityInvalid
18constructor NativePhysicalProgramComposeTrainingRejected
19field unrestricted nativePhysicalProgramComposeTrainingError :
20 (family NativePhysicalErrorCode)
21constructor NativePhysicalProgramComposeInferenceRejected
22field unrestricted nativePhysicalProgramComposeInferenceError :
23 (family NativePhysicalErrorCode)
24constructor NativePhysicalProgramComposeArithmeticFailed
25field unrestricted nativePhysicalProgramComposeAddressClass :
26 (family NativePhysicalProgramComposeAddressClass)
27field unrestricted nativePhysicalProgramComposeArithmeticError :
28 (family ModelWord64ArithmeticErrorCode)
29constructor NativePhysicalProgramComposeTrainingHaltMissing
30constructor NativePhysicalProgramComposeTrainingHaltNotFinal
31constructor NativePhysicalProgramComposeCombinedRejected
32field unrestricted nativePhysicalProgramComposeCombinedError :
33 (family NativePhysicalErrorCode)
34end-family
35
36family NativePhysicalProgramComposeTelemetry : Type 0
37constructor NativePhysicalProgramComposeTelemetryValue
38field unrestricted nativePhysicalProgramComposeTrainingCommands : Nat
39field unrestricted nativePhysicalProgramComposeInferenceCommands : Nat
40field unrestricted nativePhysicalProgramComposeCombinedCommands : Nat
41field unrestricted nativePhysicalProgramComposeCommandsRelocated : Nat
42field unrestricted nativePhysicalProgramComposeOperationsRelocated : Nat
43field unrestricted nativePhysicalProgramComposeOperandsRelocated : Nat
44field unrestricted nativePhysicalProgramComposeArithmeticChecks : Nat
45field unrestricted nativePhysicalProgramComposeTrainingHaltsRemoved : Nat
46field unrestricted nativePhysicalProgramComposeProgramValidations : Nat
47field unrestricted nativePhysicalProgramComposeFailures : Nat
48field unrestricted nativePhysicalProgramComposeHostFallbacks : Nat
49field unrestricted nativePhysicalProgramComposeTrainingIdentity : Bytes
50field unrestricted nativePhysicalProgramComposeInferenceIdentity : Bytes
51field unrestricted nativePhysicalProgramComposeCombinedIdentity : Bytes
52field unrestricted nativePhysicalProgramComposeLastError : Bytes
53end-family
54
55family NativePhysicalProgramComposeOperandResult : Type 0
56constructor NativePhysicalProgramComposeOperandRelocated
57field unrestricted nativePhysicalProgramComposeRelocatedOperand :
58 (family NativePhysicalOperand)
59field unrestricted nativePhysicalProgramComposeOperandRelocations : Nat
60field unrestricted nativePhysicalProgramComposeOperandArithmeticChecks : Nat
61constructor NativePhysicalProgramComposeOperandRejected
62field unrestricted nativePhysicalProgramComposeOperandError :
63 (family NativePhysicalProgramComposeErrorCode)
64field unrestricted nativePhysicalProgramComposeRejectedOperandRelocations : Nat
65field unrestricted nativePhysicalProgramComposeRejectedOperandArithmeticChecks : Nat
66end-family
67
68family NativePhysicalProgramComposeArgumentsResult : Type 0
69constructor NativePhysicalProgramComposeArgumentsRelocated
70field unrestricted nativePhysicalProgramComposeRelocatedArguments :
71 (family NativePhysicalArguments)
72field unrestricted nativePhysicalProgramComposeArgumentsRelocations : Nat
73field unrestricted nativePhysicalProgramComposeArgumentsArithmeticChecks : Nat
74constructor NativePhysicalProgramComposeArgumentsRejected
75field unrestricted nativePhysicalProgramComposeArgumentsError :
76 (family NativePhysicalProgramComposeErrorCode)
77field unrestricted nativePhysicalProgramComposeRejectedArgumentsRelocations : Nat
78field unrestricted nativePhysicalProgramComposeRejectedArgumentsArithmeticChecks : Nat
79end-family
80
81family NativePhysicalProgramComposeBindingResult : Type 0
82constructor NativePhysicalProgramComposeBindingRelocated
83field unrestricted nativePhysicalProgramComposeRelocatedBinding :
84 (family NativePhysicalResultBinding)
85field unrestricted nativePhysicalProgramComposeBindingRelocations : Nat
86field unrestricted nativePhysicalProgramComposeBindingArithmeticChecks : Nat
87constructor NativePhysicalProgramComposeBindingRejected
88field unrestricted nativePhysicalProgramComposeBindingError :
89 (family NativePhysicalProgramComposeErrorCode)
90end-family
91
92family NativePhysicalProgramComposeOperationResult : Type 0
93constructor NativePhysicalProgramComposeOperationRelocated
94field unrestricted nativePhysicalProgramComposeRelocatedOperation :
95 (family NativePhysicalOperation)
96field unrestricted nativePhysicalProgramComposeOperationOperandRelocations : Nat
97field unrestricted nativePhysicalProgramComposeOperationArithmeticChecks : Nat
98constructor NativePhysicalProgramComposeOperationRejected
99field unrestricted nativePhysicalProgramComposeOperationError :
100 (family NativePhysicalProgramComposeErrorCode)
101field unrestricted nativePhysicalProgramComposeRejectedOperationRelocations : Nat
102field unrestricted nativePhysicalProgramComposeRejectedOperationArithmeticChecks : Nat
103end-family
104
105family NativePhysicalProgramComposeCommandsResult : Type 0
106constructor NativePhysicalProgramComposeCommandsRelocated
107field unrestricted nativePhysicalProgramComposeRelocatedCommands :
108 (family NativePhysicalCommands)
109field unrestricted nativePhysicalProgramComposeRelocatedCommandCount : Nat
110field unrestricted nativePhysicalProgramComposeRelocatedOperationCount : Nat
111field unrestricted nativePhysicalProgramComposeRelocatedOperandCount : Nat
112field unrestricted nativePhysicalProgramComposeCommandsArithmeticChecks : Nat
113constructor NativePhysicalProgramComposeCommandsRejected
114field unrestricted nativePhysicalProgramComposeCommandsError :
115 (family NativePhysicalProgramComposeErrorCode)
116field unrestricted nativePhysicalProgramComposeRejectedCommandCount : Nat
117field unrestricted nativePhysicalProgramComposeRejectedOperationCount : Nat
118field unrestricted nativePhysicalProgramComposeRejectedOperandCount : Nat
119field unrestricted nativePhysicalProgramComposeRejectedArithmeticChecks : Nat
120end-family
121
122family NativePhysicalProgramComposeStripResult : Type 0
123constructor NativePhysicalProgramComposeStripEmpty
124constructor NativePhysicalProgramComposeStripSucceeded
125field unrestricted nativePhysicalProgramComposeStrippedCommands :
126 (family NativePhysicalCommands)
127field unrestricted nativePhysicalProgramComposeStrippedCount : Nat
128constructor NativePhysicalProgramComposeStripRejected
129field unrestricted nativePhysicalProgramComposeStripError :
130 (family NativePhysicalProgramComposeErrorCode)
131field unrestricted nativePhysicalProgramComposeStripVisited : Nat
132end-family
133
134family NativePhysicalProgramComposeResult : Type 0
135constructor NativePhysicalProgramComposed
136field unrestricted nativePhysicalProgramComposeProgram :
137 (family NativePhysicalProgram)
138field unrestricted nativePhysicalProgramComposeValidation :
139 (family NativePhysicalProgramValidation)
140field unrestricted nativePhysicalProgramComposeSuccessTelemetry :
141 (family NativePhysicalProgramComposeTelemetry)
142constructor NativePhysicalProgramCompositionRejected
143field unrestricted nativePhysicalProgramCompositionError :
144 (family NativePhysicalProgramComposeErrorCode)
145field unrestricted nativePhysicalProgramComposeFailureTelemetry :
146 (family NativePhysicalProgramComposeTelemetry)
147end-family
148
149def nativePhysicalProgramComposeErrorCodeBytes =
150 (lambda unrestricted code : (family NativePhysicalProgramComposeErrorCode) .
151 (eliminate NativePhysicalProgramComposeErrorCode
152 (lambda unrestricted current :
153 (family NativePhysicalProgramComposeErrorCode) . Bytes)
154 code
155 (branch NativePhysicalProgramComposeIdentityInvalid .
156 b"ALPHA-PCOMP-001")
157 (branch NativePhysicalProgramComposeTrainingRejected error .
158 (bytes-append
159 b"ALPHA-PCOMP-002-"
160 (app nativePhysicalErrorCodeBytes error)))
161 (branch NativePhysicalProgramComposeInferenceRejected error .
162 (bytes-append
163 b"ALPHA-PCOMP-003-"
164 (app nativePhysicalErrorCodeBytes error)))
165 (branch NativePhysicalProgramComposeArithmeticFailed addressClass error .
166 (bytes-append
167 b"ALPHA-PCOMP-004-"
168 (app modelWord64ArithmeticErrorCodeBytes error)))
169 (branch NativePhysicalProgramComposeTrainingHaltMissing .
170 b"ALPHA-PCOMP-005")
171 (branch NativePhysicalProgramComposeTrainingHaltNotFinal .
172 b"ALPHA-PCOMP-006")
173 (branch NativePhysicalProgramComposeCombinedRejected error .
174 (bytes-append
175 b"ALPHA-PCOMP-007-"
176 (app nativePhysicalErrorCodeBytes error)))))
177
178def nativePhysicalProgramComposeTelemetry =
179 (lambda unrestricted trainingCommands : Nat .
180 (lambda unrestricted inferenceCommands : Nat .
181 (lambda unrestricted combinedCommands : Nat .
182 (lambda unrestricted relocatedCommands : Nat .
183 (lambda unrestricted relocatedOperations : Nat .
184 (lambda unrestricted relocatedOperands : Nat .
185 (lambda unrestricted arithmeticChecks : Nat .
186 (lambda unrestricted haltsRemoved : Nat .
187 (lambda unrestricted validations : Nat .
188 (lambda unrestricted failures : Nat .
189 (lambda unrestricted trainingIdentity : Bytes .
190 (lambda unrestricted inferenceIdentity : Bytes .
191 (lambda unrestricted combinedIdentity : Bytes .
192 (lambda unrestricted lastError : Bytes .
193 (constructor NativePhysicalProgramComposeTelemetry
194 NativePhysicalProgramComposeTelemetryValue
195 trainingCommands inferenceCommands combinedCommands
196 relocatedCommands relocatedOperations relocatedOperands
197 arithmeticChecks haltsRemoved validations failures zero
198 trainingIdentity inferenceIdentity combinedIdentity
199 lastError)))))))))))))))
200
201def nativePhysicalProgramComposeCommandsCount =
202 (lambda unrestricted commands : (family NativePhysicalCommands) .
203 (eliminate NativePhysicalCommands
204 (lambda unrestricted current : (family NativePhysicalCommands) . Nat)
205 commands
206 (branch NativePhysicalCommandsEnd . zero)
207 (branch NativePhysicalCommandsNext head tail induction .
208 (succ induction))))
209
210def nativePhysicalProgramComposeCommandsAppend =
211 (lambda unrestricted left : (family NativePhysicalCommands) .
212 (lambda unrestricted right : (family NativePhysicalCommands) .
213 (eliminate NativePhysicalCommands
214 (lambda unrestricted current : (family NativePhysicalCommands) .
215 (family NativePhysicalCommands))
216 left
217 (branch NativePhysicalCommandsEnd . right)
218 (branch NativePhysicalCommandsNext head tail induction .
219 (constructor NativePhysicalCommands NativePhysicalCommandsNext
220 head induction)))))
221
222def nativePhysicalProgramComposeProgramIdentity =
223 (lambda unrestricted program : (family NativePhysicalProgram) .
224 (eliminate NativePhysicalProgram
225 (lambda unrestricted current : (family NativePhysicalProgram) . Bytes)
226 program
227 (branch NativePhysicalProgramValue
228 stateExtent resultSlots commands expected identity fallbacks . identity)))
229
230def nativePhysicalProgramComposeProgramCommands =
231 (lambda unrestricted program : (family NativePhysicalProgram) .
232 (eliminate NativePhysicalProgram
233 (lambda unrestricted current : (family NativePhysicalProgram) .
234 (family NativePhysicalCommands))
235 program
236 (branch NativePhysicalProgramValue
237 stateExtent resultSlots commands expected identity fallbacks . commands)))
238
239def nativePhysicalProgramComposeProgramPayloadBytes =
240 (lambda unrestricted program : (family NativePhysicalProgram) .
241 (eliminate NativePhysicalProgram
242 (lambda unrestricted current : (family NativePhysicalProgram) . Nat)
243 program
244 (branch NativePhysicalProgramValue
245 stateExtent resultSlots commands expected identity fallbacks .
246 (eliminate NativePhysicalCounts
247 (lambda unrestricted current : (family NativePhysicalCounts) . Nat)
248 (app nativePhysicalCommandsCounts commands)
249 (branch NativePhysicalCountsValue
250 commandCount systemCalls copies routines polls telemetry assertions
251 halts payloadBytes . payloadBytes)))))
252
253def nativePhysicalProgramComposeWord64FromNatural =
254 (lambda unrestricted value : Nat .
255 (nat-eliminate
256 (lambda unrestricted current : Nat . (family ModelWord64CheckedResult))
257 (constructor ModelWord64CheckedResult
258 ModelWord64CheckedSucceeded modelWord64Zero)
259 (lambda unrestricted predecessor : Nat .
260 (lambda unrestricted induction : (family ModelWord64CheckedResult) .
261 (eliminate ModelWord64CheckedResult
262 (lambda unrestricted current : (family ModelWord64CheckedResult) .
263 (family ModelWord64CheckedResult))
264 induction
265 (branch ModelWord64CheckedSucceeded prior .
266 (app (app modelWord64AddChecked prior) modelWord64One))
267 (branch ModelWord64CheckedFailed error . induction))))
268 value))
269
270def nativePhysicalProgramComposeShiftOperandValue =
271 (lambda unrestricted addressClass :
272 (family NativePhysicalProgramComposeAddressClass) .
273 (lambda unrestricted base : (family ModelWord64) .
274 (lambda unrestricted value : (family ModelWord64) .
275 (eliminate ModelWord64CheckedResult
276 (lambda unrestricted current : (family ModelWord64CheckedResult) .
277 (family NativePhysicalProgramComposeOperandResult))
278 (app (app modelWord64AddChecked base) value)
279 (branch ModelWord64CheckedSucceeded shifted .
280 (constructor NativePhysicalProgramComposeOperandResult
281 NativePhysicalProgramComposeOperandRelocated
282 (constructor NativePhysicalOperand NativePhysicalImmediate shifted)
283 (succ zero) (succ zero)))
284 (branch ModelWord64CheckedFailed error .
285 (constructor NativePhysicalProgramComposeOperandResult
286 NativePhysicalProgramComposeOperandRejected
287 (constructor NativePhysicalProgramComposeErrorCode
288 NativePhysicalProgramComposeArithmeticFailed
289 addressClass error)
290 zero (succ zero)))))))
291
292def nativePhysicalProgramComposeRelocateOperand =
293 (lambda unrestricted operand : (family NativePhysicalOperand) .
294 (lambda unrestricted stateBase : (family ModelWord64) .
295 (lambda unrestricted resultBase : (family ModelWord64) .
296 (lambda unrestricted payloadBase : (family ModelWord64) .
297 (eliminate NativePhysicalOperand
298 (lambda unrestricted current : (family NativePhysicalOperand) .
299 (family NativePhysicalProgramComposeOperandResult))
300 operand
301 (branch NativePhysicalImmediate value .
302 (constructor NativePhysicalProgramComposeOperandResult
303 NativePhysicalProgramComposeOperandRelocated operand zero zero))
304 (branch NativePhysicalResultValue slot .
305 (eliminate NativePhysicalSlot
306 (lambda unrestricted current : (family NativePhysicalSlot) .
307 (family NativePhysicalProgramComposeOperandResult))
308 slot
309 (branch NativePhysicalSlotValue index .
310 (eliminate ModelWord64CheckedResult
311 (lambda unrestricted current : (family ModelWord64CheckedResult) .
312 (family NativePhysicalProgramComposeOperandResult))
313 (app (app modelWord64AddChecked resultBase) index)
314 (branch ModelWord64CheckedSucceeded shifted .
315 (constructor NativePhysicalProgramComposeOperandResult
316 NativePhysicalProgramComposeOperandRelocated
317 (constructor NativePhysicalOperand
318 NativePhysicalResultValue
319 (constructor NativePhysicalSlot
320 NativePhysicalSlotValue shifted))
321 (succ zero) (succ zero)))
322 (branch ModelWord64CheckedFailed error .
323 (constructor NativePhysicalProgramComposeOperandResult
324 NativePhysicalProgramComposeOperandRejected
325 (constructor NativePhysicalProgramComposeErrorCode
326 NativePhysicalProgramComposeArithmeticFailed
327 (constructor NativePhysicalProgramComposeAddressClass
328 NativePhysicalProgramComposeResultSlot)
329 error)
330 zero (succ zero)))))))
331 (branch NativePhysicalResultAddress slot offset .
332 (eliminate NativePhysicalSlot
333 (lambda unrestricted current : (family NativePhysicalSlot) .
334 (family NativePhysicalProgramComposeOperandResult))
335 slot
336 (branch NativePhysicalSlotValue index .
337 (eliminate ModelWord64CheckedResult
338 (lambda unrestricted current : (family ModelWord64CheckedResult) .
339 (family NativePhysicalProgramComposeOperandResult))
340 (app (app modelWord64AddChecked resultBase) index)
341 (branch ModelWord64CheckedSucceeded shifted .
342 (constructor NativePhysicalProgramComposeOperandResult
343 NativePhysicalProgramComposeOperandRelocated
344 (constructor NativePhysicalOperand
345 NativePhysicalResultAddress
346 (constructor NativePhysicalSlot NativePhysicalSlotValue shifted)
347 offset)
348 (succ zero) (succ zero)))
349 (branch ModelWord64CheckedFailed error .
350 (constructor NativePhysicalProgramComposeOperandResult
351 NativePhysicalProgramComposeOperandRejected
352 (constructor NativePhysicalProgramComposeErrorCode
353 NativePhysicalProgramComposeArithmeticFailed
354 (constructor NativePhysicalProgramComposeAddressClass
355 NativePhysicalProgramComposeResultSlot)
356 error)
357 zero (succ zero)))))))
358 (branch NativePhysicalStateAddress offset .
359 (eliminate ModelWord64CheckedResult
360 (lambda unrestricted current : (family ModelWord64CheckedResult) .
361 (family NativePhysicalProgramComposeOperandResult))
362 (app (app modelWord64AddChecked stateBase) offset)
363 (branch ModelWord64CheckedSucceeded shifted .
364 (constructor NativePhysicalProgramComposeOperandResult
365 NativePhysicalProgramComposeOperandRelocated
366 (constructor NativePhysicalOperand NativePhysicalStateAddress shifted)
367 (succ zero) (succ zero)))
368 (branch ModelWord64CheckedFailed error .
369 (constructor NativePhysicalProgramComposeOperandResult
370 NativePhysicalProgramComposeOperandRejected
371 (constructor NativePhysicalProgramComposeErrorCode
372 NativePhysicalProgramComposeArithmeticFailed
373 (constructor NativePhysicalProgramComposeAddressClass
374 NativePhysicalProgramComposeStateAddress)
375 error)
376 zero (succ zero)))))
377 (branch NativePhysicalStateLoad64 offset .
378 (eliminate ModelWord64CheckedResult
379 (lambda unrestricted current : (family ModelWord64CheckedResult) .
380 (family NativePhysicalProgramComposeOperandResult))
381 (app (app modelWord64AddChecked stateBase) offset)
382 (branch ModelWord64CheckedSucceeded shifted .
383 (constructor NativePhysicalProgramComposeOperandResult
384 NativePhysicalProgramComposeOperandRelocated
385 (constructor NativePhysicalOperand NativePhysicalStateLoad64 shifted)
386 (succ zero) (succ zero)))
387 (branch ModelWord64CheckedFailed error .
388 (constructor NativePhysicalProgramComposeOperandResult
389 NativePhysicalProgramComposeOperandRejected
390 (constructor NativePhysicalProgramComposeErrorCode
391 NativePhysicalProgramComposeArithmeticFailed
392 (constructor NativePhysicalProgramComposeAddressClass
393 NativePhysicalProgramComposeStateAddress)
394 error)
395 zero (succ zero)))))
396 (branch NativePhysicalPayloadAddress offset .
397 (eliminate ModelWord64CheckedResult
398 (lambda unrestricted current : (family ModelWord64CheckedResult) .
399 (family NativePhysicalProgramComposeOperandResult))
400 (app (app modelWord64AddChecked payloadBase) offset)
401 (branch ModelWord64CheckedSucceeded shifted .
402 (constructor NativePhysicalProgramComposeOperandResult
403 NativePhysicalProgramComposeOperandRelocated
404 (constructor NativePhysicalOperand NativePhysicalPayloadAddress shifted)
405 (succ zero) (succ zero)))
406 (branch ModelWord64CheckedFailed error .
407 (constructor NativePhysicalProgramComposeOperandResult
408 NativePhysicalProgramComposeOperandRejected
409 (constructor NativePhysicalProgramComposeErrorCode
410 NativePhysicalProgramComposeArithmeticFailed
411 (constructor NativePhysicalProgramComposeAddressClass
412 NativePhysicalProgramComposePayloadAddress)
413 error)
414 zero (succ zero)))))
415 (branch NativePhysicalPayloadLoad64 offset .
416 (eliminate ModelWord64CheckedResult
417 (lambda unrestricted current : (family ModelWord64CheckedResult) .
418 (family NativePhysicalProgramComposeOperandResult))
419 (app (app modelWord64AddChecked payloadBase) offset)
420 (branch ModelWord64CheckedSucceeded shifted .
421 (constructor NativePhysicalProgramComposeOperandResult
422 NativePhysicalProgramComposeOperandRelocated
423 (constructor NativePhysicalOperand NativePhysicalPayloadLoad64 shifted)
424 (succ zero) (succ zero)))
425 (branch ModelWord64CheckedFailed error .
426 (constructor NativePhysicalProgramComposeOperandResult
427 NativePhysicalProgramComposeOperandRejected
428 (constructor NativePhysicalProgramComposeErrorCode
429 NativePhysicalProgramComposeArithmeticFailed
430 (constructor NativePhysicalProgramComposeAddressClass
431 NativePhysicalProgramComposePayloadAddress)
432 error)
433 zero (succ zero)))))
434 (branch NativePhysicalProcessArgument index .
435 (constructor NativePhysicalProgramComposeOperandResult
436 NativePhysicalProgramComposeOperandRelocated operand zero zero))
437 (branch NativePhysicalLoopAffine base stride .
438 (constructor NativePhysicalProgramComposeOperandResult
439 NativePhysicalProgramComposeOperandRelocated operand zero zero)))))))
440
441def nativePhysicalProgramComposeRelocateArguments =
442 (lambda unrestricted arguments : (family NativePhysicalArguments) .
443 (lambda unrestricted stateBase : (family ModelWord64) .
444 (lambda unrestricted resultBase : (family ModelWord64) .
445 (lambda unrestricted payloadBase : (family ModelWord64) .
446 (eliminate NativePhysicalArguments
447 (lambda unrestricted current : (family NativePhysicalArguments) .
448 (family NativePhysicalProgramComposeArgumentsResult))
449 arguments
450 (branch NativePhysicalArgumentsValue a0 a1 a2 a3 a4 a5 .
451 (eliminate NativePhysicalProgramComposeOperandResult
452 (lambda unrestricted current :
453 (family NativePhysicalProgramComposeOperandResult) .
454 (family NativePhysicalProgramComposeArgumentsResult))
455 (app
456 (app
457 (app
458 (app nativePhysicalProgramComposeRelocateOperand a0)
459 stateBase)
460 resultBase)
461 payloadBase)
462 (branch NativePhysicalProgramComposeOperandRelocated
463 r0 n0 c0 .
464 (eliminate NativePhysicalProgramComposeOperandResult
465 (lambda unrestricted current :
466 (family NativePhysicalProgramComposeOperandResult) .
467 (family NativePhysicalProgramComposeArgumentsResult))
468 (app (app (app (app nativePhysicalProgramComposeRelocateOperand a1)
469 stateBase) resultBase) payloadBase)
470 (branch NativePhysicalProgramComposeOperandRelocated r1 n1 c1 .
471 (eliminate NativePhysicalProgramComposeOperandResult
472 (lambda unrestricted current :
473 (family NativePhysicalProgramComposeOperandResult) .
474 (family NativePhysicalProgramComposeArgumentsResult))
475 (app (app (app (app nativePhysicalProgramComposeRelocateOperand a2)
476 stateBase) resultBase) payloadBase)
477 (branch NativePhysicalProgramComposeOperandRelocated r2 n2 c2 .
478 (eliminate NativePhysicalProgramComposeOperandResult
479 (lambda unrestricted current :
480 (family NativePhysicalProgramComposeOperandResult) .
481 (family NativePhysicalProgramComposeArgumentsResult))
482 (app (app (app (app nativePhysicalProgramComposeRelocateOperand a3)
483 stateBase) resultBase) payloadBase)
484 (branch NativePhysicalProgramComposeOperandRelocated r3 n3 c3 .
485 (eliminate NativePhysicalProgramComposeOperandResult
486 (lambda unrestricted current :
487 (family NativePhysicalProgramComposeOperandResult) .
488 (family NativePhysicalProgramComposeArgumentsResult))
489 (app (app (app (app nativePhysicalProgramComposeRelocateOperand a4)
490 stateBase) resultBase) payloadBase)
491 (branch NativePhysicalProgramComposeOperandRelocated r4 n4 c4 .
492 (eliminate NativePhysicalProgramComposeOperandResult
493 (lambda unrestricted current :
494 (family NativePhysicalProgramComposeOperandResult) .
495 (family NativePhysicalProgramComposeArgumentsResult))
496 (app (app (app (app nativePhysicalProgramComposeRelocateOperand a5)
497 stateBase) resultBase) payloadBase)
498 (branch NativePhysicalProgramComposeOperandRelocated r5 n5 c5 .
499 (constructor NativePhysicalProgramComposeArgumentsResult
500 NativePhysicalProgramComposeArgumentsRelocated
501 (constructor NativePhysicalArguments
502 NativePhysicalArgumentsValue r0 r1 r2 r3 r4 r5)
503 (app (app naturalAdd
504 (app (app naturalAdd
505 (app (app naturalAdd
506 (app (app naturalAdd (app (app naturalAdd n0) n1)) n2)) n3)) n4)) n5)
507 (app (app naturalAdd
508 (app (app naturalAdd
509 (app (app naturalAdd
510 (app (app naturalAdd (app (app naturalAdd c0) c1)) c2)) c3)) c4)) c5)))
511 (branch NativePhysicalProgramComposeOperandRejected error n5 c5 .
512 (constructor NativePhysicalProgramComposeArgumentsResult
513 NativePhysicalProgramComposeArgumentsRejected error
514 (app (app naturalAdd
515 (app (app naturalAdd
516 (app (app naturalAdd
517 (app (app naturalAdd (app (app naturalAdd n0) n1)) n2)) n3)) n4)) n5)
518 (app (app naturalAdd
519 (app (app naturalAdd
520 (app (app naturalAdd
521 (app (app naturalAdd (app (app naturalAdd c0) c1)) c2)) c3)) c4)) c5)))))
522 (branch NativePhysicalProgramComposeOperandRejected error n4 c4 .
523 (constructor NativePhysicalProgramComposeArgumentsResult
524 NativePhysicalProgramComposeArgumentsRejected error
525 (app (app naturalAdd
526 (app (app naturalAdd
527 (app (app naturalAdd (app (app naturalAdd n0) n1)) n2)) n3)) n4)
528 (app (app naturalAdd
529 (app (app naturalAdd
530 (app (app naturalAdd (app (app naturalAdd c0) c1)) c2)) c3)) c4)))))
531 (branch NativePhysicalProgramComposeOperandRejected error n3 c3 .
532 (constructor NativePhysicalProgramComposeArgumentsResult
533 NativePhysicalProgramComposeArgumentsRejected error
534 (app (app naturalAdd
535 (app (app naturalAdd (app (app naturalAdd n0) n1)) n2)) n3)
536 (app (app naturalAdd
537 (app (app naturalAdd (app (app naturalAdd c0) c1)) c2)) c3)))))
538 (branch NativePhysicalProgramComposeOperandRejected error n2 c2 .
539 (constructor NativePhysicalProgramComposeArgumentsResult
540 NativePhysicalProgramComposeArgumentsRejected error
541 (app (app naturalAdd (app (app naturalAdd n0) n1)) n2)
542 (app (app naturalAdd (app (app naturalAdd c0) c1)) c2)))))
543 (branch NativePhysicalProgramComposeOperandRejected error n1 c1 .
544 (constructor NativePhysicalProgramComposeArgumentsResult
545 NativePhysicalProgramComposeArgumentsRejected error
546 (app (app naturalAdd n0) n1)
547 (app (app naturalAdd c0) c1)))))
548 (branch NativePhysicalProgramComposeOperandRejected
549 error relocations checks .
550 (constructor NativePhysicalProgramComposeArgumentsResult
551 NativePhysicalProgramComposeArgumentsRejected
552 error relocations checks)))))))))
553
554def nativePhysicalProgramComposeRelocateBinding =
555 (lambda unrestricted binding : (family NativePhysicalResultBinding) .
556 (lambda unrestricted resultBase : (family ModelWord64) .
557 (eliminate NativePhysicalResultBinding
558 (lambda unrestricted current : (family NativePhysicalResultBinding) .
559 (family NativePhysicalProgramComposeBindingResult))
560 binding
561 (branch NativePhysicalDiscardResult .
562 (constructor NativePhysicalProgramComposeBindingResult
563 NativePhysicalProgramComposeBindingRelocated binding zero zero))
564 (branch NativePhysicalStoreResult slot .
565 (eliminate NativePhysicalSlot
566 (lambda unrestricted current : (family NativePhysicalSlot) .
567 (family NativePhysicalProgramComposeBindingResult))
568 slot
569 (branch NativePhysicalSlotValue index .
570 (eliminate ModelWord64CheckedResult
571 (lambda unrestricted current : (family ModelWord64CheckedResult) .
572 (family NativePhysicalProgramComposeBindingResult))
573 (app (app modelWord64AddChecked resultBase) index)
574 (branch ModelWord64CheckedSucceeded shifted .
575 (constructor NativePhysicalProgramComposeBindingResult
576 NativePhysicalProgramComposeBindingRelocated
577 (constructor NativePhysicalResultBinding
578 NativePhysicalStoreResult
579 (constructor NativePhysicalSlot NativePhysicalSlotValue shifted))
580 (succ zero) (succ zero)))
581 (branch ModelWord64CheckedFailed error .
582 (constructor NativePhysicalProgramComposeBindingResult
583 NativePhysicalProgramComposeBindingRejected
584 (constructor NativePhysicalProgramComposeErrorCode
585 NativePhysicalProgramComposeArithmeticFailed
586 (constructor NativePhysicalProgramComposeAddressClass
587 NativePhysicalProgramComposeResultSlot)
588 error))))))))))
589
590def nativePhysicalProgramComposeRelocateOperation =
591 (lambda unrestricted operation : (family NativePhysicalOperation) .
592 (lambda unrestricted stateBase : (family ModelWord64) .
593 (lambda unrestricted resultBase : (family ModelWord64) .
594 (lambda unrestricted payloadBase : (family ModelWord64) .
595 (eliminate NativePhysicalOperation
596 (lambda unrestricted current : (family NativePhysicalOperation) .
597 (family NativePhysicalProgramComposeOperationResult))
598 operation
599 (branch NativePhysicalSystemCall number arguments payload binding .
600 (eliminate NativePhysicalProgramComposeOperandResult
601 (lambda unrestricted current :
602 (family NativePhysicalProgramComposeOperandResult) .
603 (family NativePhysicalProgramComposeOperationResult))
604 (app (app (app (app nativePhysicalProgramComposeRelocateOperand number)
605 stateBase) resultBase) payloadBase)
606 (branch NativePhysicalProgramComposeOperandRelocated relocatedNumber n0 c0 .
607 (eliminate NativePhysicalProgramComposeArgumentsResult
608 (lambda unrestricted current :
609 (family NativePhysicalProgramComposeArgumentsResult) .
610 (family NativePhysicalProgramComposeOperationResult))
611 (app (app (app (app nativePhysicalProgramComposeRelocateArguments arguments)
612 stateBase) resultBase) payloadBase)
613 (branch NativePhysicalProgramComposeArgumentsRelocated
614 relocatedArguments n1 c1 .
615 (eliminate NativePhysicalProgramComposeBindingResult
616 (lambda unrestricted current :
617 (family NativePhysicalProgramComposeBindingResult) .
618 (family NativePhysicalProgramComposeOperationResult))
619 (app
620 (app nativePhysicalProgramComposeRelocateBinding binding)
621 resultBase)
622 (branch NativePhysicalProgramComposeBindingRelocated
623 relocatedBinding n2 c2 .
624 (constructor NativePhysicalProgramComposeOperationResult
625 NativePhysicalProgramComposeOperationRelocated
626 (constructor NativePhysicalOperation
627 NativePhysicalSystemCall relocatedNumber
628 relocatedArguments payload relocatedBinding)
629 (app (app naturalAdd (app (app naturalAdd n0) n1)) n2)
630 (app (app naturalAdd (app (app naturalAdd c0) c1)) c2)))
631 (branch NativePhysicalProgramComposeBindingRejected error .
632 (constructor NativePhysicalProgramComposeOperationResult
633 NativePhysicalProgramComposeOperationRejected error
634 (app (app naturalAdd n0) n1)
635 (app (app naturalAdd c0) c1)))))
636 (branch NativePhysicalProgramComposeArgumentsRejected error n1 c1 .
637 (constructor NativePhysicalProgramComposeOperationResult
638 NativePhysicalProgramComposeOperationRejected error
639 (app (app naturalAdd n0) n1)
640 (app (app naturalAdd c0) c1)))))
641 (branch NativePhysicalProgramComposeOperandRejected error n c .
642 (constructor NativePhysicalProgramComposeOperationResult
643 NativePhysicalProgramComposeOperationRejected error n c))
644 ))
645 (branch NativePhysicalCopyPayloadToState destination extent payload .
646 (eliminate ModelWord64CheckedResult
647 (lambda unrestricted current : (family ModelWord64CheckedResult) .
648 (family NativePhysicalProgramComposeOperationResult))
649 (app (app modelWord64AddChecked stateBase) destination)
650 (branch ModelWord64CheckedSucceeded shifted .
651 (constructor NativePhysicalProgramComposeOperationResult
652 NativePhysicalProgramComposeOperationRelocated
653 (constructor NativePhysicalOperation
654 NativePhysicalCopyPayloadToState shifted extent payload)
655 (succ zero) (succ zero)))
656 (branch ModelWord64CheckedFailed error .
657 (constructor NativePhysicalProgramComposeOperationResult
658 NativePhysicalProgramComposeOperationRejected
659 (constructor NativePhysicalProgramComposeErrorCode
660 NativePhysicalProgramComposeArithmeticFailed
661 (constructor NativePhysicalProgramComposeAddressClass
662 NativePhysicalProgramComposeStateAddress)
663 error)
664 zero (succ zero)))))
665 (branch NativePhysicalMachineRoutine machineCode arguments binding .
666 (eliminate NativePhysicalProgramComposeArgumentsResult
667 (lambda unrestricted current :
668 (family NativePhysicalProgramComposeArgumentsResult) .
669 (family NativePhysicalProgramComposeOperationResult))
670 (app (app (app (app nativePhysicalProgramComposeRelocateArguments arguments)
671 stateBase) resultBase) payloadBase)
672 (branch NativePhysicalProgramComposeArgumentsRelocated relocatedArguments n1 c1 .
673 (eliminate NativePhysicalProgramComposeBindingResult
674 (lambda unrestricted current :
675 (family NativePhysicalProgramComposeBindingResult) .
676 (family NativePhysicalProgramComposeOperationResult))
677 (app (app nativePhysicalProgramComposeRelocateBinding binding) resultBase)
678 (branch NativePhysicalProgramComposeBindingRelocated relocatedBinding n2 c2 .
679 (constructor NativePhysicalProgramComposeOperationResult
680 NativePhysicalProgramComposeOperationRelocated
681 (constructor NativePhysicalOperation NativePhysicalMachineRoutine
682 machineCode relocatedArguments relocatedBinding)
683 (app (app naturalAdd n1) n2)
684 (app (app naturalAdd c1) c2)))
685 (branch NativePhysicalProgramComposeBindingRejected error .
686 (constructor NativePhysicalProgramComposeOperationResult
687 NativePhysicalProgramComposeOperationRejected error n1 c1))))
688 (branch NativePhysicalProgramComposeArgumentsRejected error n c .
689 (constructor NativePhysicalProgramComposeOperationResult
690 NativePhysicalProgramComposeOperationRejected error n c))
691 ))
692 (branch NativePhysicalFencePoll address expected maximumPolls .
693 (eliminate NativePhysicalProgramComposeOperandResult
694 (lambda unrestricted current :
695 (family NativePhysicalProgramComposeOperandResult) .
696 (family NativePhysicalProgramComposeOperationResult))
697 (app (app (app (app nativePhysicalProgramComposeRelocateOperand address)
698 stateBase) resultBase) payloadBase)
699 (branch NativePhysicalProgramComposeOperandRelocated relocatedAddress n0 c0 .
700 (eliminate NativePhysicalProgramComposeOperandResult
701 (lambda unrestricted current :
702 (family NativePhysicalProgramComposeOperandResult) .
703 (family NativePhysicalProgramComposeOperationResult))
704 (app (app (app (app nativePhysicalProgramComposeRelocateOperand expected)
705 stateBase) resultBase) payloadBase)
706 (branch NativePhysicalProgramComposeOperandRelocated relocatedExpected n1 c1 .
707 (constructor NativePhysicalProgramComposeOperationResult
708 NativePhysicalProgramComposeOperationRelocated
709 (constructor NativePhysicalOperation NativePhysicalFencePoll
710 relocatedAddress relocatedExpected maximumPolls)
711 (app (app naturalAdd n0) n1)
712 (app (app naturalAdd c0) c1)))
713 (branch NativePhysicalProgramComposeOperandRejected error n1 c1 .
714 (constructor NativePhysicalProgramComposeOperationResult
715 NativePhysicalProgramComposeOperationRejected error
716 (app (app naturalAdd n0) n1)
717 (app (app naturalAdd c0) c1)))))
718 (branch NativePhysicalProgramComposeOperandRejected error n c .
719 (constructor NativePhysicalProgramComposeOperationResult
720 NativePhysicalProgramComposeOperationRejected error n c))
721 ))
722 (branch NativePhysicalTelemetryAppend path record .
723 (constructor NativePhysicalProgramComposeOperationResult
724 NativePhysicalProgramComposeOperationRelocated operation zero zero))
725 (branch NativePhysicalAssertEqual left right errorCode .
726 (eliminate NativePhysicalProgramComposeOperandResult
727 (lambda unrestricted current :
728 (family NativePhysicalProgramComposeOperandResult) .
729 (family NativePhysicalProgramComposeOperationResult))
730 (app (app (app (app nativePhysicalProgramComposeRelocateOperand left)
731 stateBase) resultBase) payloadBase)
732 (branch NativePhysicalProgramComposeOperandRelocated relocatedLeft n0 c0 .
733 (eliminate NativePhysicalProgramComposeOperandResult
734 (lambda unrestricted current :
735 (family NativePhysicalProgramComposeOperandResult) .
736 (family NativePhysicalProgramComposeOperationResult))
737 (app (app (app (app nativePhysicalProgramComposeRelocateOperand right)
738 stateBase) resultBase) payloadBase)
739 (branch NativePhysicalProgramComposeOperandRelocated relocatedRight n1 c1 .
740 (constructor NativePhysicalProgramComposeOperationResult
741 NativePhysicalProgramComposeOperationRelocated
742 (constructor NativePhysicalOperation NativePhysicalAssertEqual
743 relocatedLeft relocatedRight errorCode)
744 (app (app naturalAdd n0) n1)
745 (app (app naturalAdd c0) c1)))
746 (branch NativePhysicalProgramComposeOperandRejected error n1 c1 .
747 (constructor NativePhysicalProgramComposeOperationResult
748 NativePhysicalProgramComposeOperationRejected error
749 (app (app naturalAdd n0) n1)
750 (app (app naturalAdd c0) c1)))))
751 (branch NativePhysicalProgramComposeOperandRejected error n c .
752 (constructor NativePhysicalProgramComposeOperationResult
753 NativePhysicalProgramComposeOperationRejected error n c))
754 ))
755 (branch NativePhysicalAssertOneOf observed first second errorCode .
756 (eliminate NativePhysicalProgramComposeOperandResult
757 (lambda unrestricted current :
758 (family NativePhysicalProgramComposeOperandResult) .
759 (family NativePhysicalProgramComposeOperationResult))
760 (app (app (app (app nativePhysicalProgramComposeRelocateOperand observed)
761 stateBase) resultBase) payloadBase)
762 (branch NativePhysicalProgramComposeOperandRelocated relocatedObserved n0 c0 .
763 (eliminate NativePhysicalProgramComposeOperandResult
764 (lambda unrestricted current :
765 (family NativePhysicalProgramComposeOperandResult) .
766 (family NativePhysicalProgramComposeOperationResult))
767 (app (app (app (app nativePhysicalProgramComposeRelocateOperand first)
768 stateBase) resultBase) payloadBase)
769 (branch NativePhysicalProgramComposeOperandRelocated relocatedFirst n1 c1 .
770 (eliminate NativePhysicalProgramComposeOperandResult
771 (lambda unrestricted current :
772 (family NativePhysicalProgramComposeOperandResult) .
773 (family NativePhysicalProgramComposeOperationResult))
774 (app (app (app (app nativePhysicalProgramComposeRelocateOperand second)
775 stateBase) resultBase) payloadBase)
776 (branch NativePhysicalProgramComposeOperandRelocated relocatedSecond n2 c2 .
777 (constructor NativePhysicalProgramComposeOperationResult
778 NativePhysicalProgramComposeOperationRelocated
779 (constructor NativePhysicalOperation NativePhysicalAssertOneOf
780 relocatedObserved relocatedFirst relocatedSecond errorCode)
781 (app (app naturalAdd n0) (app (app naturalAdd n1) n2))
782 (app (app naturalAdd c0) (app (app naturalAdd c1) c2))))
783 (branch NativePhysicalProgramComposeOperandRejected error n2 c2 .
784 (constructor NativePhysicalProgramComposeOperationResult
785 NativePhysicalProgramComposeOperationRejected error
786 (app (app naturalAdd n0) (app (app naturalAdd n1) n2))
787 (app (app naturalAdd c0) (app (app naturalAdd c1) c2))))))
788 (branch NativePhysicalProgramComposeOperandRejected error n1 c1 .
789 (constructor NativePhysicalProgramComposeOperationResult
790 NativePhysicalProgramComposeOperationRejected error
791 (app (app naturalAdd n0) n1)
792 (app (app naturalAdd c0) c1)))))
793 (branch NativePhysicalProgramComposeOperandRejected error n c .
794 (constructor NativePhysicalProgramComposeOperationResult
795 NativePhysicalProgramComposeOperationRejected error n c))
796 ))
797 (branch NativePhysicalHaltSuccess .
798 (constructor NativePhysicalProgramComposeOperationResult
799 NativePhysicalProgramComposeOperationRelocated operation zero zero))
800 (branch NativePhysicalRepeatBegin count .
801 (constructor NativePhysicalProgramComposeOperationResult
802 NativePhysicalProgramComposeOperationRelocated operation zero zero))
803 (branch
804 NativePhysicalSkipUnlessEqual
805 left
806 right
807 count
808 .
809 (eliminate
810 NativePhysicalProgramComposeOperandResult
811 (lambda unrestricted current : (family NativePhysicalProgramComposeOperandResult) .
812 (family NativePhysicalProgramComposeOperationResult))
813 (nativePhysicalProgramComposeRelocateOperand left stateBase resultBase payloadBase)
814 (branch
815 NativePhysicalProgramComposeOperandRelocated
816 relocatedLeft
817 n0
818 c0
819 .
820 (eliminate
821 NativePhysicalProgramComposeOperandResult
822 (lambda unrestricted current : (family NativePhysicalProgramComposeOperandResult) .
823 (family NativePhysicalProgramComposeOperationResult))
824 (nativePhysicalProgramComposeRelocateOperand
825 right
826 stateBase
827 resultBase
828 payloadBase)
829 (branch
830 NativePhysicalProgramComposeOperandRelocated
831 relocatedRight
832 n1
833 c1
834 .
835 (constructor
836 NativePhysicalProgramComposeOperationResult
837 NativePhysicalProgramComposeOperationRelocated
838 (constructor
839 NativePhysicalOperation
840 NativePhysicalSkipUnlessEqual
841 relocatedLeft
842 relocatedRight
843 count)
844 (naturalAdd n0 n1)
845 (naturalAdd c0 c1)))
846 (branch
847 NativePhysicalProgramComposeOperandRejected
848 error
849 n1
850 c1
851 .
852 (constructor
853 NativePhysicalProgramComposeOperationResult
854 NativePhysicalProgramComposeOperationRejected
855 error
856 (naturalAdd n0 n1)
857 (naturalAdd c0 c1)))))
858 (branch
859 NativePhysicalProgramComposeOperandRejected
860 error
861 n
862 c
863 .
864 (constructor
865 NativePhysicalProgramComposeOperationResult
866 NativePhysicalProgramComposeOperationRejected
867 error
868 n
869 c))))
870(branch NativePhysicalRepeatEnd .
871 (constructor NativePhysicalProgramComposeOperationResult
872 NativePhysicalProgramComposeOperationRelocated operation zero zero))
873 (branch NativePhysicalRepeatEndWhen observed expected .
874 (constructor NativePhysicalProgramComposeOperationResult
875 NativePhysicalProgramComposeOperationRelocated operation zero zero))
876 (branch NativePhysicalStoreWord64 destination value .
877 (constructor NativePhysicalProgramComposeOperationResult
878 NativePhysicalProgramComposeOperationRelocated operation zero zero))
879 (branch NativePhysicalFenceWait address expected polls interval .
880 (constructor NativePhysicalProgramComposeOperationResult
881 NativePhysicalProgramComposeOperationRelocated operation zero zero))
882 (branch NativePhysicalRepeatBeginCounted count .
883 (constructor NativePhysicalProgramComposeOperationResult
884 NativePhysicalProgramComposeOperationRelocated operation zero zero))
885 (branch NativePhysicalAddWord64 destination left right .
886 (constructor NativePhysicalProgramComposeOperationResult
887 NativePhysicalProgramComposeOperationRelocated operation zero zero))
888 (branch NativePhysicalFloat64 kind destination left right .
889 (constructor NativePhysicalProgramComposeOperationResult
890 NativePhysicalProgramComposeOperationRelocated operation zero zero)))))))
891
892def nativePhysicalProgramComposeRelocateCommands =
893 (lambda unrestricted commands : (family NativePhysicalCommands) .
894 (lambda unrestricted stateBase : (family ModelWord64) .
895 (lambda unrestricted resultBase : (family ModelWord64) .
896 (lambda unrestricted payloadBase : (family ModelWord64) .
897 (eliminate NativePhysicalCommands
898 (lambda unrestricted current : (family NativePhysicalCommands) .
899 (family NativePhysicalProgramComposeCommandsResult))
900 commands
901 (branch NativePhysicalCommandsEnd .
902 (constructor NativePhysicalProgramComposeCommandsResult
903 NativePhysicalProgramComposeCommandsRelocated
904 (constructor NativePhysicalCommands NativePhysicalCommandsEnd)
905 zero zero zero zero))
906 (branch NativePhysicalCommandsNext head tail induction .
907 (eliminate NativePhysicalCommand
908 (lambda unrestricted current : (family NativePhysicalCommand) .
909 (family NativePhysicalProgramComposeCommandsResult))
910 head
911 (branch NativePhysicalCommandValue operation errorIdentity .
912 (eliminate NativePhysicalProgramComposeOperationResult
913 (lambda unrestricted current :
914 (family NativePhysicalProgramComposeOperationResult) .
915 (family NativePhysicalProgramComposeCommandsResult))
916 (app (app (app (app nativePhysicalProgramComposeRelocateOperation operation)
917 stateBase) resultBase) payloadBase)
918 (branch NativePhysicalProgramComposeOperationRelocated
919 relocatedOperation n0 c0 .
920 (eliminate NativePhysicalProgramComposeCommandsResult
921 (lambda unrestricted current :
922 (family NativePhysicalProgramComposeCommandsResult) .
923 (family NativePhysicalProgramComposeCommandsResult))
924 induction
925 (branch NativePhysicalProgramComposeCommandsRelocated
926 relocatedTail commandsDone operationsDone operandsDone checksDone .
927 (constructor NativePhysicalProgramComposeCommandsResult
928 NativePhysicalProgramComposeCommandsRelocated
929 (constructor NativePhysicalCommands NativePhysicalCommandsNext
930 (constructor NativePhysicalCommand NativePhysicalCommandValue
931 relocatedOperation errorIdentity)
932 relocatedTail)
933 (succ commandsDone) (succ operationsDone)
934 (app (app naturalAdd n0) operandsDone)
935 (app (app naturalAdd c0) checksDone)))
936 (branch NativePhysicalProgramComposeCommandsRejected
937 error commandsDone operationsDone operandsDone checksDone .
938 (constructor NativePhysicalProgramComposeCommandsResult
939 NativePhysicalProgramComposeCommandsRejected error
940 (succ commandsDone) (succ operationsDone)
941 (app (app naturalAdd n0) operandsDone)
942 (app (app naturalAdd c0) checksDone)))))
943 (branch NativePhysicalProgramComposeOperationRejected error n c .
944 (constructor NativePhysicalProgramComposeCommandsResult
945 NativePhysicalProgramComposeCommandsRejected
946 error zero zero n c)))))))))))
947
948def nativePhysicalProgramComposeOperationIsHalt =
949 (lambda unrestricted operation : (family NativePhysicalOperation) .
950 (eliminate NativePhysicalOperation
951 (lambda unrestricted current : (family NativePhysicalOperation) . Nat)
952 operation
953 (branch NativePhysicalSystemCall number arguments payload binding . zero)
954 (branch NativePhysicalCopyPayloadToState destination extent payload . zero)
955 (branch NativePhysicalMachineRoutine code arguments binding . zero)
956 (branch NativePhysicalFencePoll address expected polls . zero)
957 (branch NativePhysicalTelemetryAppend path record . zero)
958 (branch NativePhysicalAssertEqual left right error . zero)
959 (branch NativePhysicalAssertOneOf observed first second error . zero)
960 (branch NativePhysicalHaltSuccess . (succ zero))
961 (branch NativePhysicalRepeatBegin count . zero)
962 (branch NativePhysicalSkipUnlessEqual left right count . zero)
963(branch NativePhysicalRepeatEnd . zero)
964 (branch NativePhysicalRepeatEndWhen observed expected . zero)
965 (branch NativePhysicalStoreWord64 destination value . zero)
966 (branch NativePhysicalFenceWait address expected polls interval . zero)
967 (branch NativePhysicalRepeatBeginCounted count . zero)
968 (branch NativePhysicalAddWord64 destination left right . zero)
969 (branch NativePhysicalFloat64 operation destination left right . zero)))
970
971def nativePhysicalProgramComposeCommandIsHalt =
972 (lambda unrestricted command : (family NativePhysicalCommand) .
973 (eliminate NativePhysicalCommand
974 (lambda unrestricted current : (family NativePhysicalCommand) . Nat)
975 command
976 (branch NativePhysicalCommandValue operation errorIdentity .
977 (app nativePhysicalProgramComposeOperationIsHalt operation))))
978
979-- Sequential composition removes the training program's final halt. A
980-- forward branch targeting the old end must now target the first inference
981-- command, not skip that command. Other relative record distances are stable.
982-- originalRestCount comes from the strip fold, avoiding a scan per command.
983def nativePhysicalProgramComposeRemoveFinalHaltJump =
984 (lambda unrestricted originalRestCount : Nat .
985 (lambda unrestricted command : (family NativePhysicalCommand) .
986 (eliminate NativePhysicalCommand
987 (lambda unrestricted current : (family NativePhysicalCommand) . (family NativePhysicalCommand))
988 command
989 (branch NativePhysicalCommandValue original identity .
990 (constructor NativePhysicalCommand NativePhysicalCommandValue
991 (eliminate NativePhysicalOperation
992 (lambda unrestricted current : (family NativePhysicalOperation) . (family NativePhysicalOperation))
993 original
994(branch NativePhysicalSystemCall number arguments payload binding . original)
995(branch NativePhysicalCopyPayloadToState destination extent payload . original)
996(branch NativePhysicalMachineRoutine code arguments binding . original)
997(branch NativePhysicalFencePoll address expected polls . original)
998(branch NativePhysicalTelemetryAppend path record . original)
999(branch NativePhysicalAssertEqual left right error . original)
1000(branch NativePhysicalAssertOneOf observed first second error . original)
1001(branch NativePhysicalHaltSuccess . original)
1002(branch NativePhysicalRepeatBegin count . original)
1003(branch NativePhysicalSkipUnlessEqual left right count . (constructor NativePhysicalOperation NativePhysicalSkipUnlessEqual left right
1004 (modelWord64FromNaturalTruncated
1005 (naturalSaturatingSubtract (modelWord64Natural count)
1006 (naturalEqual (modelWord64Natural count) originalRestCount)))))
1007(branch NativePhysicalRepeatEnd . original)
1008(branch NativePhysicalRepeatEndWhen observed expected . original)
1009(branch NativePhysicalStoreWord64 destination value . original)
1010(branch NativePhysicalFenceWait address expected polls interval . original)
1011(branch NativePhysicalRepeatBeginCounted count . original)
1012(branch NativePhysicalAddWord64 destination left right . original)
1013(branch NativePhysicalFloat64 operation destination left right . original)) identity)))))
1014
1015def nativePhysicalProgramComposeStripTrainingHalt =
1016 (lambda unrestricted commands : (family NativePhysicalCommands) .
1017 (eliminate NativePhysicalCommands
1018 (lambda unrestricted current : (family NativePhysicalCommands) .
1019 (family NativePhysicalProgramComposeStripResult))
1020 commands
1021 (branch NativePhysicalCommandsEnd .
1022 (constructor NativePhysicalProgramComposeStripResult
1023 NativePhysicalProgramComposeStripEmpty))
1024 (branch NativePhysicalCommandsNext head tail induction .
1025 (eliminate NativePhysicalProgramComposeStripResult
1026 (lambda unrestricted current :
1027 (family NativePhysicalProgramComposeStripResult) .
1028 (family NativePhysicalProgramComposeStripResult))
1029 induction
1030 (branch NativePhysicalProgramComposeStripEmpty .
1031 (nat-eliminate
1032 (lambda unrestricted isHalt : Nat .
1033 (family NativePhysicalProgramComposeStripResult))
1034 (constructor NativePhysicalProgramComposeStripResult
1035 NativePhysicalProgramComposeStripRejected
1036 (constructor NativePhysicalProgramComposeErrorCode
1037 NativePhysicalProgramComposeTrainingHaltMissing)
1038 (succ zero))
1039 (lambda unrestricted predecessor : Nat .
1040 (lambda unrestricted ignored :
1041 (family NativePhysicalProgramComposeStripResult) .
1042 (constructor NativePhysicalProgramComposeStripResult
1043 NativePhysicalProgramComposeStripSucceeded
1044 (constructor NativePhysicalCommands NativePhysicalCommandsEnd)
1045 zero)))
1046 (app nativePhysicalProgramComposeCommandIsHalt head)))
1047 (branch NativePhysicalProgramComposeStripSucceeded stripped count .
1048 (nat-eliminate
1049 (lambda unrestricted isHalt : Nat .
1050 (family NativePhysicalProgramComposeStripResult))
1051 (constructor NativePhysicalProgramComposeStripResult
1052 NativePhysicalProgramComposeStripSucceeded
1053 (constructor NativePhysicalCommands NativePhysicalCommandsNext
1054 (nativePhysicalProgramComposeRemoveFinalHaltJump (succ count) head) stripped)
1055 (succ count))
1056 (lambda unrestricted predecessor : Nat .
1057 (lambda unrestricted ignored :
1058 (family NativePhysicalProgramComposeStripResult) .
1059 (constructor NativePhysicalProgramComposeStripResult
1060 NativePhysicalProgramComposeStripRejected
1061 (constructor NativePhysicalProgramComposeErrorCode
1062 NativePhysicalProgramComposeTrainingHaltNotFinal)
1063 (succ count))))
1064 (app nativePhysicalProgramComposeCommandIsHalt head)))
1065 (branch NativePhysicalProgramComposeStripRejected error visited . induction)))))
1066
1067def nativePhysicalProgramComposeFailure =
1068 (lambda unrestricted error : (family NativePhysicalProgramComposeErrorCode) .
1069 (lambda unrestricted trainingCommands : Nat .
1070 (lambda unrestricted inferenceCommands : Nat .
1071 (lambda unrestricted combinedCommands : Nat .
1072 (lambda unrestricted relocatedCommands : Nat .
1073 (lambda unrestricted relocatedOperations : Nat .
1074 (lambda unrestricted relocatedOperands : Nat .
1075 (lambda unrestricted arithmeticChecks : Nat .
1076 (lambda unrestricted haltsRemoved : Nat .
1077 (lambda unrestricted validations : Nat .
1078 (lambda unrestricted trainingIdentity : Bytes .
1079 (lambda unrestricted inferenceIdentity : Bytes .
1080 (lambda unrestricted combinedIdentity : Bytes .
1081 (constructor NativePhysicalProgramComposeResult
1082 NativePhysicalProgramCompositionRejected error
1083 (app
1084 (app
1085 (app
1086 (app
1087 (app
1088 (app
1089 (app
1090 (app
1091 (app
1092 (app
1093 (app
1094 (app
1095 (app
1096 (app nativePhysicalProgramComposeTelemetry
1097 trainingCommands)
1098 inferenceCommands)
1099 combinedCommands)
1100 relocatedCommands)
1101 relocatedOperations)
1102 relocatedOperands)
1103 arithmeticChecks)
1104 haltsRemoved)
1105 validations)
1106 (succ zero))
1107 trainingIdentity)
1108 inferenceIdentity)
1109 combinedIdentity)
1110 (app nativePhysicalProgramComposeErrorCodeBytes error))))))))))))))))
1111
1112def nativePhysicalComposePrograms =
1113 (lambda unrestricted training : (family NativePhysicalProgram) .
1114 (lambda unrestricted inference : (family NativePhysicalProgram) .
1115 (lambda unrestricted combinedIdentity : Bytes .
1116 (app
1117 (lambda unrestricted trainingIdentity : Bytes .
1118 (app
1119 (lambda unrestricted inferenceIdentity : Bytes .
1120 (app
1121 (lambda unrestricted trainingCommands :
1122 (family NativePhysicalCommands) .
1123 (app
1124 (lambda unrestricted inferenceCommands :
1125 (family NativePhysicalCommands) .
1126 (nat-eliminate
1127 (lambda unrestricted identityValid : Nat .
1128 (family NativePhysicalProgramComposeResult))
1129 (app
1130 (app
1131 (app
1132 (app
1133 (app
1134 (app
1135 (app
1136 (app
1137 (app
1138 (app
1139 (app
1140 (app nativePhysicalProgramComposeFailure
1141 (constructor NativePhysicalProgramComposeErrorCode
1142 NativePhysicalProgramComposeIdentityInvalid))
1143 (app nativePhysicalProgramComposeCommandsCount trainingCommands))
1144 (app nativePhysicalProgramComposeCommandsCount inferenceCommands))
1145 zero)
1146 zero)
1147 zero)
1148 zero)
1149 zero)
1150 zero)
1151 zero)
1152 trainingIdentity)
1153 inferenceIdentity
1154 combinedIdentity)
1155 (lambda unrestricted identityPredecessor : Nat .
1156 (lambda unrestricted identityInduction :
1157 (family NativePhysicalProgramComposeResult) .
1158 (eliminate NativePhysicalProgramValidation
1159 (lambda unrestricted current :
1160 (family NativePhysicalProgramValidation) .
1161 (family NativePhysicalProgramComposeResult))
1162 (app nativePhysicalValidateProgram training)
1163 (branch NativePhysicalProgramValidated validatedTraining trainingTelemetry .
1164 (eliminate NativePhysicalProgramValidation
1165 (lambda unrestricted current :
1166 (family NativePhysicalProgramValidation) .
1167 (family NativePhysicalProgramComposeResult))
1168 (app nativePhysicalValidateProgram inference)
1169 (branch NativePhysicalProgramValidated validatedInference inferenceTelemetry .
1170 (eliminate NativePhysicalProgram
1171 (lambda unrestricted current :
1172 (family NativePhysicalProgram) .
1173 (family NativePhysicalProgramComposeResult))
1174 training
1175 (branch NativePhysicalProgramValue
1176 trainingState trainingResults ignoredTrainingCommands
1177 trainingExpected ignoredTrainingIdentity trainingFallbacks .
1178 (eliminate NativePhysicalProgram
1179 (lambda unrestricted current :
1180 (family NativePhysicalProgram) .
1181 (family NativePhysicalProgramComposeResult))
1182 inference
1183 (branch NativePhysicalProgramValue
1184 inferenceState inferenceResults ignoredInferenceCommands
1185 inferenceExpected ignoredInferenceIdentity inferenceFallbacks .
1186 (eliminate NativePhysicalProgramComposeStripResult
1187 (lambda unrestricted current :
1188 (family NativePhysicalProgramComposeStripResult) .
1189 (family NativePhysicalProgramComposeResult))
1190 (app nativePhysicalProgramComposeStripTrainingHalt trainingCommands)
1191 (branch NativePhysicalProgramComposeStripEmpty .
1192 (app
1193 (app
1194 (app
1195 (app
1196 (app
1197 (app
1198 (app
1199 (app
1200 (app
1201 (app
1202 (app
1203 (app nativePhysicalProgramComposeFailure
1204 (constructor NativePhysicalProgramComposeErrorCode
1205 NativePhysicalProgramComposeTrainingHaltMissing))
1206 (app nativePhysicalProgramComposeCommandsCount trainingCommands))
1207 (app nativePhysicalProgramComposeCommandsCount inferenceCommands))
1208 zero)
1209 zero)
1210 zero)
1211 zero)
1212 zero)
1213 zero)
1214 (byte-to-nat (byte 2)))
1215 trainingIdentity)
1216 inferenceIdentity
1217 combinedIdentity))
1218 (branch NativePhysicalProgramComposeStripSucceeded
1219 trainingPrefix trainingPrefixCount .
1220 (eliminate ModelWord64CheckedResult
1221 (lambda unrestricted current :
1222 (family ModelWord64CheckedResult) .
1223 (family NativePhysicalProgramComposeResult))
1224 (app nativePhysicalProgramComposeWord64FromNatural
1225 (app nativePhysicalProgramComposeProgramPayloadBytes training))
1226 (branch ModelWord64CheckedSucceeded payloadBase .
1227 (eliminate NativePhysicalProgramComposeCommandsResult
1228 (lambda unrestricted current :
1229 (family NativePhysicalProgramComposeCommandsResult) .
1230 (family NativePhysicalProgramComposeResult))
1231 (app
1232 (app
1233 (app
1234 (app nativePhysicalProgramComposeRelocateCommands inferenceCommands)
1235 trainingState)
1236 trainingResults)
1237 payloadBase)
1238 (branch NativePhysicalProgramComposeCommandsRelocated
1239 relocatedInference commandCount operationCount
1240 operandCount checks .
1241 (eliminate ModelWord64CheckedResult
1242 (lambda unrestricted current :
1243 (family ModelWord64CheckedResult) .
1244 (family NativePhysicalProgramComposeResult))
1245 (app (app modelWord64AddChecked trainingState) inferenceState)
1246 (branch ModelWord64CheckedSucceeded combinedState .
1247 (eliminate ModelWord64CheckedResult
1248 (lambda unrestricted current :
1249 (family ModelWord64CheckedResult) .
1250 (family NativePhysicalProgramComposeResult))
1251 (app (app modelWord64AddChecked trainingResults) inferenceResults)
1252 (branch ModelWord64CheckedSucceeded combinedResults .
1253 (app
1254 (lambda unrestricted combinedCommands :
1255 (family NativePhysicalCommands) .
1256 (app
1257 (lambda unrestricted combinedProgram :
1258 (family NativePhysicalProgram) .
1259 (eliminate NativePhysicalProgramValidation
1260 (lambda unrestricted current :
1261 (family NativePhysicalProgramValidation) .
1262 (family NativePhysicalProgramComposeResult))
1263 (app nativePhysicalValidateProgram combinedProgram)
1264 (branch NativePhysicalProgramValidated validated telemetry .
1265 (constructor NativePhysicalProgramComposeResult
1266 NativePhysicalProgramComposed combinedProgram
1267 (constructor NativePhysicalProgramValidation
1268 NativePhysicalProgramValidated validated telemetry)
1269 (app
1270 (app
1271 (app
1272 (app
1273 (app
1274 (app
1275 (app
1276 (app
1277 (app
1278 (app
1279 (app
1280 (app
1281 (app
1282 (app nativePhysicalProgramComposeTelemetry
1283 (app nativePhysicalProgramComposeCommandsCount trainingCommands))
1284 (app nativePhysicalProgramComposeCommandsCount inferenceCommands))
1285 (app nativePhysicalProgramComposeCommandsCount combinedCommands))
1286 commandCount)
1287 operationCount)
1288 operandCount)
1289 (app (app naturalAdd checks) (succ (succ zero))))
1290 (succ zero))
1291 (byte-to-nat (byte 3)))
1292 zero)
1293 trainingIdentity)
1294 inferenceIdentity)
1295 combinedIdentity)
1296 b"")))
1297 (branch NativePhysicalProgramRejected error telemetry .
1298 (app
1299 (app
1300 (app
1301 (app
1302 (app
1303 (app
1304 (app
1305 (app
1306 (app
1307 (app
1308 (app
1309 (app nativePhysicalProgramComposeFailure
1310 (constructor NativePhysicalProgramComposeErrorCode
1311 NativePhysicalProgramComposeCombinedRejected error))
1312 (app nativePhysicalProgramComposeCommandsCount trainingCommands))
1313 (app nativePhysicalProgramComposeCommandsCount inferenceCommands))
1314 (app nativePhysicalProgramComposeCommandsCount combinedCommands))
1315 commandCount)
1316 operationCount)
1317 operandCount)
1318 (app (app naturalAdd checks) (succ (succ zero))))
1319 (succ zero))
1320 (byte-to-nat (byte 3)))
1321 trainingIdentity)
1322 inferenceIdentity
1323 combinedIdentity))))
1324 (constructor NativePhysicalProgram
1325 NativePhysicalProgramValue
1326 combinedState combinedResults combinedCommands
1327 (app nativePhysicalProgramComposeCommandsCount combinedCommands)
1328 combinedIdentity
1329 (app
1330 (app naturalAdd trainingFallbacks)
1331 inferenceFallbacks))))
1332 (app
1333 (app nativePhysicalProgramComposeCommandsAppend trainingPrefix)
1334 relocatedInference)))
1335 (branch ModelWord64CheckedFailed error .
1336 (app
1337 (app
1338 (app
1339 (app
1340 (app
1341 (app
1342 (app
1343 (app
1344 (app
1345 (app
1346 (app
1347 (app nativePhysicalProgramComposeFailure
1348 (constructor NativePhysicalProgramComposeErrorCode
1349 NativePhysicalProgramComposeArithmeticFailed
1350 (constructor NativePhysicalProgramComposeAddressClass
1351 NativePhysicalProgramComposeResultExtent)
1352 error))
1353 (app nativePhysicalProgramComposeCommandsCount trainingCommands))
1354 (app nativePhysicalProgramComposeCommandsCount inferenceCommands))
1355 zero)
1356 commandCount)
1357 operationCount)
1358 operandCount)
1359 (app (app naturalAdd checks) (succ (succ zero))))
1360 (succ zero))
1361 (byte-to-nat (byte 2)))
1362 trainingIdentity)
1363 inferenceIdentity
1364 combinedIdentity))))
1365 (branch ModelWord64CheckedFailed error .
1366 (app
1367 (app
1368 (app
1369 (app
1370 (app
1371 (app
1372 (app
1373 (app
1374 (app
1375 (app
1376 (app
1377 (app nativePhysicalProgramComposeFailure
1378 (constructor NativePhysicalProgramComposeErrorCode
1379 NativePhysicalProgramComposeArithmeticFailed
1380 (constructor NativePhysicalProgramComposeAddressClass
1381 NativePhysicalProgramComposeStateExtent)
1382 error))
1383 (app nativePhysicalProgramComposeCommandsCount trainingCommands))
1384 (app nativePhysicalProgramComposeCommandsCount inferenceCommands))
1385 zero)
1386 commandCount)
1387 operationCount)
1388 operandCount)
1389 (succ checks))
1390 (succ zero))
1391 (byte-to-nat (byte 2)))
1392 trainingIdentity)
1393 inferenceIdentity
1394 combinedIdentity))))
1395 (branch NativePhysicalProgramComposeCommandsRejected
1396 error commandCount operationCount operandCount checks .
1397 (app
1398 (app
1399 (app
1400 (app
1401 (app
1402 (app
1403 (app
1404 (app
1405 (app
1406 (app
1407 (app
1408 (app nativePhysicalProgramComposeFailure error)
1409 (app nativePhysicalProgramComposeCommandsCount trainingCommands))
1410 (app nativePhysicalProgramComposeCommandsCount inferenceCommands))
1411 zero)
1412 commandCount)
1413 operationCount)
1414 operandCount)
1415 checks)
1416 (succ zero))
1417 (byte-to-nat (byte 2)))
1418 trainingIdentity)
1419 inferenceIdentity
1420 combinedIdentity))))
1421 (branch ModelWord64CheckedFailed error .
1422 (app
1423 (app
1424 (app
1425 (app
1426 (app
1427 (app
1428 (app
1429 (app
1430 (app
1431 (app
1432 (app
1433 (app nativePhysicalProgramComposeFailure
1434 (constructor NativePhysicalProgramComposeErrorCode
1435 NativePhysicalProgramComposeArithmeticFailed
1436 (constructor NativePhysicalProgramComposeAddressClass
1437 NativePhysicalProgramComposePayloadAddress)
1438 error))
1439 (app nativePhysicalProgramComposeCommandsCount trainingCommands))
1440 (app nativePhysicalProgramComposeCommandsCount inferenceCommands))
1441 zero)
1442 zero)
1443 zero)
1444 zero)
1445 zero)
1446 (succ zero))
1447 (byte-to-nat (byte 2)))
1448 trainingIdentity)
1449 inferenceIdentity
1450 combinedIdentity))))
1451 (branch NativePhysicalProgramComposeStripRejected error visited .
1452 (app
1453 (app
1454 (app
1455 (app
1456 (app
1457 (app
1458 (app
1459 (app
1460 (app
1461 (app
1462 (app
1463 (app nativePhysicalProgramComposeFailure error)
1464 (app nativePhysicalProgramComposeCommandsCount trainingCommands))
1465 (app nativePhysicalProgramComposeCommandsCount inferenceCommands))
1466 zero)
1467 zero)
1468 zero)
1469 zero)
1470 zero)
1471 zero)
1472 (byte-to-nat (byte 2)))
1473 trainingIdentity)
1474 inferenceIdentity
1475 combinedIdentity))))))))
1476 (branch NativePhysicalProgramRejected error telemetry .
1477 (app
1478 (app
1479 (app
1480 (app
1481 (app
1482 (app
1483 (app
1484 (app
1485 (app
1486 (app
1487 (app
1488 (app nativePhysicalProgramComposeFailure
1489 (constructor NativePhysicalProgramComposeErrorCode
1490 NativePhysicalProgramComposeInferenceRejected error))
1491 (app nativePhysicalProgramComposeCommandsCount trainingCommands))
1492 (app nativePhysicalProgramComposeCommandsCount inferenceCommands))
1493 zero)
1494 zero)
1495 zero)
1496 zero)
1497 zero)
1498 zero)
1499 (byte-to-nat (byte 2)))
1500 trainingIdentity)
1501 inferenceIdentity
1502 combinedIdentity))))
1503 (branch NativePhysicalProgramRejected error telemetry .
1504 (app
1505 (app
1506 (app
1507 (app
1508 (app
1509 (app
1510 (app
1511 (app
1512 (app
1513 (app
1514 (app
1515 (app nativePhysicalProgramComposeFailure
1516 (constructor NativePhysicalProgramComposeErrorCode
1517 NativePhysicalProgramComposeTrainingRejected error))
1518 (app nativePhysicalProgramComposeCommandsCount trainingCommands))
1519 (app nativePhysicalProgramComposeCommandsCount inferenceCommands))
1520 zero)
1521 zero)
1522 zero)
1523 zero)
1524 zero)
1525 zero)
1526 (succ zero))
1527 trainingIdentity)
1528 inferenceIdentity
1529 combinedIdentity)))))
1530
1531 (app naturalAnd
1532 (app
1533 (app naturalAnd
1534 (app
1535 (app naturalEqual (bytes-length trainingIdentity))
1536 (byte-to-nat (byte 64))))
1537 (app
1538 (app naturalEqual (bytes-length inferenceIdentity))
1539 (byte-to-nat (byte 64))))
1540 (app
1541 (app naturalEqual (bytes-length combinedIdentity))
1542 (byte-to-nat (byte 64))))))
1543 (app nativePhysicalProgramComposeProgramCommands inference)))
1544 (app nativePhysicalProgramComposeProgramCommands training)))
1545 (app nativePhysicalProgramComposeProgramIdentity inference)))
1546 (app nativePhysicalProgramComposeProgramIdentity training)))))
1547
1548def nativePhysicalProgramComposerHostFallbacks : Nat = zeroThe compiler supplied declaration spans and resolved links from this source snapshot. This page does not assert that this file belongs to a checked closure.