1module Platform.Linux.Nvidia.RequestCapture
2
3import Checkpoint.Envelope
4import Data.Bytes
5import Data.UTF8
6import Data.JSON
7import Data.JSONAccess
8import Data.JSONRender
9import Model.Config
10import Model.Parameter
11import Model.Word32
12import Model.Word64
13import Observe.CapturePolicy
14import Observe.Interchange
15import Observe.Value
16import Platform.Linux.Nvidia.PlanHost
17import Platform.Linux.Nvidia.PlanHostRequest
18import Platform.Linux.Nvidia.ObservedRequest
19import Runtime.NativeLaunchRecipeLoad
20import Runtime.NativeObservedProgram
21import Runtime.NativeObservedJournal
22import Runtime.NativePhysicalProgram
23import Runtime.NativeTelemetry
24import Runtime.NativeTelemetryIdentity
25import Runtime.NativeTelemetryPolicy
26import Runtime.TelemetryCapture
27import Runtime.TelemetryDrain
28import Runtime.TelemetryIdentity
29import Runtime.TelemetryPolicy
30import Runtime.TelemetryPublication
31import Runtime.TelemetryRecord
32import Std.Byte
33import Std.Flag
34import Std.List
35import Std.Natural
36
37-- Protocol boundaries report only what the host reached. These are not loss,
38-- token, update or latency measurements. Names are static schema-bound values;
39-- phase IDs remain the request protocol's IDs. Source time stays unavailable.
40-- The encoded batch budget is the whole publication frame
41-- (Runtime.TelemetryPublication.publicationMaximumFrameBytes). Every batch of
42-- this policy carries the complete declared descriptor inventory: the shared
43-- request, checkpoint, driver-context, continuation, persistence and
44-- input-binding sites plus each system's own sites, schemas and metadata.
45-- Bob's inventory alone needs 35,276 bytes (32,193 of descriptors), so the
46-- former 32,768-byte budget refused the recorder declaration. The routed plan
47-- still refuses any program whose declared batch exceeds the frame.
48def nvidiaRequestCapturePolicy =
49 (constructor
50 CapturePolicy
51 CapturePolicyValue
52 1
53 b"00000000000000000000000000000500"
54 (constructor CaptureProfile CaptureLifecycleProfile)
55 0
56 0
57 2
58 publicationMaximumFrameBytes
59 8
60 1
61 1)
62
63def nvidiaRequestCaptureDeclaration =
64 (lambda unrestricted name : Bytes .
65 (constructor
66 TelemetryRecordDeclaration
67 TelemetryRecordDeclarationValue
68 b"alpha.request.boundary@1"
69 b"diagnostic"
70 (capturePolicyIdentifier nvidiaRequestCapturePolicy)
71 b"reported"
72 b"maintained request lifecycle boundary reached"
73 (constructor
74 TelemetryCaptureValue
75 TelemetryMembersNext
76 b"phase"
77 (constructor TelemetryCaptureValue TelemetryUnsigned 0)
78 (constructor
79 TelemetryCaptureValue
80 TelemetryMembersNext
81 b"name"
82 (constructor TelemetryCaptureValue TelemetryConstant (constructor AosValue AosText name))
83 (constructor TelemetryCaptureValue TelemetryMembersEnd)))))
84
85def nvidiaRequestCaptureField =
86 (lambda unrestricted kind : Bytes .
87 (constructor
88 JSON
89 JSONObject
90 (telemetryPolicyMember
91 b"type"
92 (constructor JSON JSONString kind)
93 (constructor JSON JSONObjectEnd))))
94
95def nvidiaRequestCaptureSchema =
96 (telemetryRecordJSON
97 (telemetryRecordSchemaJSON
98 (nvidiaRequestCaptureDeclaration b"")
99 b"Alpha request host protocol"
100 (constructor
101 JSON
102 JSONObject
103 (telemetryPolicyMember
104 b"phase"
105 (nvidiaRequestCaptureField b"u64")
106 (telemetryPolicyMember
107 b"name"
108 (nvidiaRequestCaptureField b"text")
109 (constructor JSON JSONObjectEnd))))))
110
111def nvidiaRequestCaptureSite =
112 (lambda unrestricted phase : Nat .
113 (lambda unrestricted name : Bytes .
114 (lambda unrestricted identifier : Bytes .
115 (lambda unrestricted tail : (family TelemetryPolicySites) .
116 (constructor
117 TelemetryPolicySites
118 TelemetryPolicySitesNext
119 (succ phase)
120 (constructor
121 CaptureSite
122 CaptureSiteValue
123 identifier
124 name
125 (constructor CaptureClass CaptureLifecycleClass)
126 1
127 2
128 1)
129 (nvidiaRequestCaptureDeclaration name)
130 tail)))))
131
132def nvidiaRequestCaptureSites =
133 (nvidiaRequestCaptureSite
134 prTelemetryBegin
135 b"request-host:begin"
136 b"00000000000000000000000000000501"
137 (nvidiaRequestCaptureSite
138 prTelemetryChecked
139 b"request-host:request-checked"
140 b"00000000000000000000000000000502"
141 (nvidiaRequestCaptureSite
142 prTelemetryChannel
143 b"request-host:channel-ready"
144 b"00000000000000000000000000000503"
145 (nvidiaRequestCaptureSite
146 prTelemetryUploaded
147 b"request-host:uploaded"
148 b"00000000000000000000000000000504"
149 (nvidiaRequestCaptureSite
150 prTelemetryLearner
151 b"request-host:learner-scalars"
152 b"00000000000000000000000000000505"
153 (nvidiaRequestCaptureSite
154 prTelemetryPublished
155 b"request-host:checkpoint-published"
156 b"00000000000000000000000000000506"
157 (nvidiaRequestCaptureSite
158 prTelemetryDone
159 b"request-host:done"
160 b"00000000000000000000000000000507"
161 (constructor TelemetryPolicySites TelemetryPolicySitesEnd))))))))
162
163-- A companion to the lifecycle record, emitted only after the persistence
164-- owner has completed all publication stages, including directory fsync. Read
165-- the header it actually wrote: a custom schedule may publish a different
166-- number of updates/invocations from the contract's default. This is the
167-- checkpoint frontier, not per-update timing, loss or consumer receipt.
168def nvidiaRequestCheckpointCaptureTag : Nat =
169 (succ (succ prTelemetryDone))
170
171-- Input and output frontiers have the same header representation, while their
172-- schemas and capture sites keep admission separate from durable publication.
173def nvidiaRequestCheckpointFrontierDeclaration =
174 (lambda unrestricted schema : Bytes .
175 (lambda unrestricted method : Bytes .
176 (constructor
177 TelemetryRecordDeclaration
178 TelemetryRecordDeclarationValue
179 schema
180 b"diagnostic"
181 (capturePolicyIdentifier nvidiaRequestCapturePolicy)
182 b"reported"
183 method
184 (constructor
185 TelemetryCaptureValue
186 TelemetryMembersNext
187 b"completed_updates"
188 (constructor TelemetryCaptureValue TelemetryUnsigned 0)
189 (constructor
190 TelemetryCaptureValue
191 TelemetryMembersNext
192 b"completed_invocations"
193 (constructor TelemetryCaptureValue TelemetryUnsigned 1)
194 (constructor
195 TelemetryCaptureValue
196 TelemetryMembersNext
197 b"envelope_version"
198 (constructor TelemetryCaptureValue TelemetryUnsigned 2)
199 (constructor TelemetryCaptureValue TelemetryMembersEnd)))))))
200
201def nvidiaRequestCheckpointCaptureDeclaration =
202 (nvidiaRequestCheckpointFrontierDeclaration
203 b"alpha.checkpoint.published-frontier@1"
204 b"published checkpoint header after file and directory synchronization")
205
206def nvidiaRequestCheckpointAdmittedDeclaration =
207 (nvidiaRequestCheckpointFrontierDeclaration
208 b"alpha.checkpoint.admitted-frontier@1"
209 b"input checkpoint header after layout, identity and chunk admission; before device upload")
210
211def nvidiaRequestCheckpointInputDeclaration =
212 (constructor
213 TelemetryRecordDeclaration
214 TelemetryRecordDeclarationValue
215 b"alpha.checkpoint.input-admission@1"
216 b"diagnostic"
217 (capturePolicyIdentifier nvidiaRequestCapturePolicy)
218 b"reported"
219 b"admitted input envelope version: zero means empty input; one means validated checkpoint"
220 (constructor
221 TelemetryCaptureValue
222 TelemetryMembersNext
223 b"envelope_version"
224 (constructor TelemetryCaptureValue TelemetryUnsigned 0)
225 (constructor TelemetryCaptureValue TelemetryMembersEnd)))
226
227def nvidiaRequestCheckpointFrontierSchema =
228 (lambda unrestricted declaration : (family TelemetryRecordDeclaration) .
229 (lambda unrestricted name : Bytes .
230 (telemetryRecordJSON
231 (telemetryRecordSchemaJSON
232 declaration
233 name
234 (constructor
235 JSON
236 JSONObject
237 (telemetryPolicyMember
238 b"completed_updates"
239 (nvidiaRequestCaptureField b"u64")
240 (telemetryPolicyMember
241 b"completed_invocations"
242 (nvidiaRequestCaptureField b"u64")
243 (telemetryPolicyMember
244 b"envelope_version"
245 (nvidiaRequestCaptureField b"u64")
246 (constructor JSON JSONObjectEnd)))))))))
247
248def nvidiaRequestCheckpointCaptureSchema =
249 (nvidiaRequestCheckpointFrontierSchema
250 nvidiaRequestCheckpointCaptureDeclaration
251 b"Published native checkpoint frontier")
252
253def nvidiaRequestCheckpointAdmittedSchema =
254 (nvidiaRequestCheckpointFrontierSchema
255 nvidiaRequestCheckpointAdmittedDeclaration
256 b"Admitted native checkpoint frontier")
257
258def nvidiaRequestCheckpointInputSchema =
259 (telemetryRecordJSON
260 (telemetryRecordSchemaJSON
261 nvidiaRequestCheckpointInputDeclaration
262 b"Native checkpoint input admission"
263 (constructor
264 JSON
265 JSONObject
266 (telemetryPolicyMember
267 b"envelope_version"
268 (nvidiaRequestCaptureField b"u64")
269 (constructor JSON JSONObjectEnd)))))
270
271def nvidiaRequestCheckpointInputTag : Nat =
272 (succ nvidiaRequestCheckpointCaptureTag)
273
274def nvidiaRequestCheckpointAdmittedTag : Nat =
275 (succ nvidiaRequestCheckpointInputTag)
276
277def nvidiaRequestCheckpointSite =
278 (lambda unrestricted tag : Nat .
279 (lambda unrestricted identity : Bytes .
280 (lambda unrestricted name : Bytes .
281 (lambda unrestricted dimensions : Nat .
282 (lambda unrestricted declaration : (family TelemetryRecordDeclaration) .
283 (lambda unrestricted tail : (family TelemetryPolicySites) .
284 (constructor
285 TelemetryPolicySites
286 TelemetryPolicySitesNext
287 tag
288 (constructor
289 CaptureSite
290 CaptureSiteValue
291 identity
292 name
293 (constructor CaptureClass CaptureLifecycleClass)
294 1
295 dimensions
296 1)
297 declaration
298 tail)))))))
299
300-- A manifest commits the persisted composite learning state, including all
301-- payload chunk hashes and counters. The full digest remains alongside every
302-- truncated typed reference. Tensor bytes are not retained by these records.
303def nvidiaRequestCheckpointManifestDeclaration =
304 (lambda unrestricted stage : Bytes .
305 (constructor
306 TelemetryRecordDeclaration
307 TelemetryRecordDeclarationValue
308 b"alpha.checkpoint.manifest@1"
309 b"state"
310 (capturePolicyIdentifier nvidiaRequestCapturePolicy)
311 b"reported"
312 b"SHA-256 of the complete checkpoint envelope header, including payload chunk hashes; not the whole file digest"
313 (constructor
314 TelemetryCaptureValue
315 TelemetryMembersNext
316 b"manifest_sha256"
317 (constructor TelemetryCaptureValue TelemetryBytes 0 checkpointEnvelopeDigestBytes)
318 (constructor
319 TelemetryCaptureValue
320 TelemetryMembersNext
321 b"completed_updates"
322 (constructor TelemetryCaptureValue TelemetryUnsigned 4)
323 (constructor
324 TelemetryCaptureValue
325 TelemetryMembersNext
326 b"completed_invocations"
327 (constructor TelemetryCaptureValue TelemetryUnsigned 5)
328 (constructor
329 TelemetryCaptureValue
330 TelemetryMembersNext
331 b"manifest_header_bytes"
332 (constructor TelemetryCaptureValue TelemetryUnsigned 6)
333 (constructor
334 TelemetryCaptureValue
335 TelemetryMembersNext
336 b"payload_bytes"
337 (constructor TelemetryCaptureValue TelemetryUnsigned 7)
338 (constructor
339 TelemetryCaptureValue
340 TelemetryMembersNext
341 b"stage"
342 (constructor
343 TelemetryCaptureValue
344 TelemetryConstant
345 (constructor AosValue AosText stage))
346 (constructor TelemetryCaptureValue TelemetryMembersEnd)))))))))
347
348def nvidiaRequestCheckpointStateDeclaration =
349 (constructor
350 TelemetryRecordDeclaration
351 TelemetryRecordDeclarationValue
352 b"aos.state.declared@1"
353 b"state"
354 (capturePolicyIdentifier nvidiaRequestCapturePolicy)
355 b"reported"
356 b"checkpoint manifest SHA-256 first 16 bytes identify the composite checkpointed state"
357 (constructor
358 TelemetryCaptureValue
359 TelemetryMembersNext
360 b"state"
361 (constructor TelemetryCaptureValue TelemetryReference b"state" 0)
362 (constructor
363 TelemetryCaptureValue
364 TelemetryMembersNext
365 b"name"
366 (constructor
367 TelemetryCaptureValue
368 TelemetryConstant
369 (constructor AosValue AosText b"Checkpointed learning-system state"))
370 (constructor
371 TelemetryCaptureValue
372 TelemetryMembersNext
373 b"domain"
374 (constructor
375 TelemetryCaptureValue
376 TelemetryConstant
377 (constructor AosValue AosText b"learning-system"))
378 (constructor
379 TelemetryCaptureValue
380 TelemetryMembersNext
381 b"owner"
382 (constructor
383 TelemetryCaptureValue
384 TelemetryUnavailable
385 b"not_recorded"
386 b"checkpoint-owner-entity-not-recorded")
387 (constructor
388 TelemetryCaptureValue
389 TelemetryMembersNext
390 b"content"
391 (constructor
392 TelemetryCaptureValue
393 TelemetryUnavailable
394 b"not_recorded"
395 b"checkpoint-payload-not-retained")
396 (constructor
397 TelemetryCaptureValue
398 TelemetryMembersNext
399 b"manifest_sha256"
400 (constructor TelemetryCaptureValue TelemetryBytes 0 checkpointEnvelopeDigestBytes)
401 (constructor TelemetryCaptureValue TelemetryMembersEnd))))))))
402
403def nvidiaRequestCheckpointIdentityDeclaration =
404 (lambda unrestricted phase : Bytes .
405 (constructor
406 TelemetryRecordDeclaration
407 TelemetryRecordDeclarationValue
408 b"aos.state.checkpoint@1"
409 b"state"
410 (capturePolicyIdentifier nvidiaRequestCapturePolicy)
411 b"reported"
412 b"persistence or restoration owner reached the named checkpoint boundary"
413 (constructor
414 TelemetryCaptureValue
415 TelemetryMembersNext
416 b"checkpoint"
417 (constructor TelemetryCaptureValue TelemetryReference b"checkpoint" 0)
418 (constructor
419 TelemetryCaptureValue
420 TelemetryMembersNext
421 b"states"
422 (constructor
423 TelemetryCaptureValue
424 TelemetryList
425 (constructor
426 TelemetryCaptureValue
427 TelemetryItemsNext
428 (constructor TelemetryCaptureValue TelemetryReference b"state" 0)
429 (constructor TelemetryCaptureValue TelemetryItemsEnd)))
430 (constructor
431 TelemetryCaptureValue
432 TelemetryMembersNext
433 b"phase"
434 (constructor
435 TelemetryCaptureValue
436 TelemetryConstant
437 (constructor AosValue AosText phase))
438 (constructor
439 TelemetryCaptureValue
440 TelemetryMembersNext
441 b"artifact"
442 (constructor
443 TelemetryCaptureValue
444 TelemetryUnavailable
445 b"not_recorded"
446 b"checkpoint-file-content-not-retained-by-telemetry")
447 (constructor
448 TelemetryCaptureValue
449 TelemetryMembersNext
450 b"manifest_sha256"
451 (constructor TelemetryCaptureValue TelemetryBytes 0 checkpointEnvelopeDigestBytes)
452 (constructor TelemetryCaptureValue TelemetryMembersEnd))))))))
453
454def nvidiaRequestCheckpointManifestSchema =
455 (telemetryRecordJSON
456 (telemetryRecordSchemaJSON
457 (nvidiaRequestCheckpointManifestDeclaration b"")
458 b"Native checkpoint manifest commitment"
459 (constructor
460 JSON
461 JSONObject
462 (aosField
463 b"manifest_sha256"
464 (nvidiaRequestCaptureField b"bytes")
465 (aosField
466 b"completed_updates"
467 (nvidiaRequestCaptureField b"u64")
468 (aosField
469 b"completed_invocations"
470 (nvidiaRequestCaptureField b"u64")
471 (aosField
472 b"manifest_header_bytes"
473 (nvidiaRequestCaptureField b"u64")
474 (aosField
475 b"payload_bytes"
476 (nvidiaRequestCaptureField b"u64")
477 (aosField b"stage" (nvidiaRequestCaptureField b"text") aosObjectEnd)))))))))
478
479def nvidiaRequestCheckpointStateSchema =
480 (telemetryRecordJSON
481 (telemetryRecordSchemaJSON
482 nvidiaRequestCheckpointStateDeclaration
483 b"Composite checkpoint state"
484 (constructor
485 JSON
486 JSONObject
487 (aosField
488 b"state"
489 (nvidiaRequestCaptureField b"ref:state")
490 (aosField
491 b"name"
492 (nvidiaRequestCaptureField b"text")
493 (aosField
494 b"domain"
495 (nvidiaRequestCaptureField b"text")
496 (aosField
497 b"owner"
498 (nvidiaRequestCaptureField b"text")
499 (aosField
500 b"content"
501 (nvidiaRequestCaptureField b"text")
502 (aosField b"manifest_sha256" (nvidiaRequestCaptureField b"bytes") aosObjectEnd)))))))))
503
504def nvidiaRequestCheckpointIdentitySchema =
505 (telemetryRecordJSON
506 (telemetryRecordSchemaJSON
507 (nvidiaRequestCheckpointIdentityDeclaration b"")
508 b"Native checkpoint persistence and restoration"
509 (constructor
510 JSON
511 JSONObject
512 (aosField
513 b"checkpoint"
514 (nvidiaRequestCaptureField b"ref:checkpoint")
515 (aosField
516 b"states"
517 (nvidiaRequestCaptureField b"list:ref:state")
518 (aosField
519 b"phase"
520 (nvidiaRequestCaptureField b"text")
521 (aosField
522 b"artifact"
523 (nvidiaRequestCaptureField b"ref:artifact")
524 (aosField b"manifest_sha256" (nvidiaRequestCaptureField b"bytes") aosObjectEnd))))))))
525
526def nvidiaRequestCheckpointManifestInputTag : Nat =
527 (succ nvidiaRequestCheckpointAdmittedTag)
528
529def nvidiaRequestCheckpointManifestOutputTag : Nat =
530 (succ nvidiaRequestCheckpointManifestInputTag)
531
532def nvidiaRequestCheckpointStateTag : Nat =
533 (succ nvidiaRequestCheckpointManifestOutputTag)
534
535def nvidiaRequestCheckpointCommittedTag : Nat =
536 (succ nvidiaRequestCheckpointStateTag)
537
538def nvidiaRequestCheckpointRestoredTag : Nat =
539 (succ nvidiaRequestCheckpointCommittedTag)
540
541-- These bytes come from the admitted driver's version-query response, not
542-- the target's expected ABI branch. No firmware or operating-state query is
543-- implied by reaching the channel boundary.
544def nvidiaRequestDriverDeclaration =
545 (constructor
546 TelemetryRecordDeclaration
547 TelemetryRecordDeclarationValue
548 b"alpha.device.driver-context@1"
549 b"event"
550 (capturePolicyIdentifier nvidiaRequestCapturePolicy)
551 b"reported"
552 b"Linux NVIDIA driver version query after branch admission"
553 (constructor
554 TelemetryCaptureValue
555 TelemetryMembersNext
556 b"version_query_bytes"
557 (constructor TelemetryCaptureValue TelemetryBytes 0 phDriverVersionBytes)
558 (constructor
559 TelemetryCaptureValue
560 TelemetryMembersNext
561 b"firmware"
562 (constructor
563 TelemetryCaptureValue
564 TelemetryUnavailable
565 b"not_recorded"
566 b"firmware-not-queried")
567 (constructor
568 TelemetryCaptureValue
569 TelemetryMembersNext
570 b"clocks"
571 (constructor
572 TelemetryCaptureValue
573 TelemetryUnavailable
574 b"not_recorded"
575 b"clocks-not-queried")
576 (constructor
577 TelemetryCaptureValue
578 TelemetryMembersNext
579 b"power"
580 (constructor
581 TelemetryCaptureValue
582 TelemetryUnavailable
583 b"not_recorded"
584 b"power-not-queried")
585 (constructor
586 TelemetryCaptureValue
587 TelemetryMembersNext
588 b"temperature"
589 (constructor
590 TelemetryCaptureValue
591 TelemetryUnavailable
592 b"not_recorded"
593 b"temperature-not-queried")
594 (constructor TelemetryCaptureValue TelemetryMembersEnd)))))))
595
596def nvidiaRequestDriverSchema =
597 (telemetryRecordJSON
598 (telemetryRecordSchemaJSON
599 nvidiaRequestDriverDeclaration
600 b"Admitted native driver context"
601 (constructor
602 JSON
603 JSONObject
604 (aosField
605 b"version_query_bytes"
606 (nvidiaRequestCaptureField b"bytes")
607 (aosField
608 b"firmware"
609 (nvidiaRequestCaptureField b"text")
610 (aosField
611 b"clocks"
612 (nvidiaRequestCaptureField b"text")
613 (aosField
614 b"power"
615 (nvidiaRequestCaptureField b"text")
616 (aosField b"temperature" (nvidiaRequestCaptureField b"text") aosObjectEnd))))))))
617
618def nvidiaRequestDriverTag : Nat =
619 (succ nvidiaRequestCheckpointRestoredTag)
620
621-- This edge covers the complete restored-to-published execution window.
622-- It does not infer intermediate update states or a transition from an
623-- unobserved fresh-initialization state.
624def nvidiaRequestContinuationDeclaration =
625 (constructor
626 TelemetryRecordDeclaration
627 TelemetryRecordDeclarationValue
628 b"aos.state.transition@1"
629 b"state"
630 (capturePolicyIdentifier nvidiaRequestCapturePolicy)
631 b"reported"
632 b"persistence owner's committed continuation window"
633 (constructor
634 TelemetryCaptureValue
635 TelemetryMembersNext
636 b"transition"
637 (constructor TelemetryCaptureValue TelemetryReference b"transition" 2)
638 (constructor
639 TelemetryCaptureValue
640 TelemetryMembersNext
641 b"inputs"
642 (constructor
643 TelemetryCaptureValue
644 TelemetryList
645 (constructor
646 TelemetryCaptureValue
647 TelemetryItemsNext
648 (constructor TelemetryCaptureValue TelemetryReference b"state" 0)
649 (constructor TelemetryCaptureValue TelemetryItemsEnd)))
650 (constructor
651 TelemetryCaptureValue
652 TelemetryMembersNext
653 b"outputs"
654 (constructor
655 TelemetryCaptureValue
656 TelemetryList
657 (constructor
658 TelemetryCaptureValue
659 TelemetryItemsNext
660 (constructor TelemetryCaptureValue TelemetryReference b"state" 2)
661 (constructor TelemetryCaptureValue TelemetryItemsEnd)))
662 (constructor
663 TelemetryCaptureValue
664 TelemetryMembersNext
665 b"outcome"
666 (constructor
667 TelemetryCaptureValue
668 TelemetryConstant
669 (constructor AosValue AosText b"accepted"))
670 (constructor
671 TelemetryCaptureValue
672 TelemetryMembersNext
673 b"reason"
674 (constructor
675 TelemetryCaptureValue
676 TelemetryUnavailable
677 b"not_recorded"
678 b"committed-continuation-window")
679 (constructor
680 TelemetryCaptureValue
681 TelemetryMembersNext
682 b"mechanism"
683 (constructor
684 TelemetryCaptureValue
685 TelemetryConstant
686 (constructor
687 AosValue
688 AosText
689 b"restored checkpoint to committed checkpoint; cumulative window, not one learner update"))
690 (constructor
691 TelemetryCaptureValue
692 TelemetryMembersNext
693 b"coordinate"
694 (constructor
695 TelemetryCaptureValue
696 TelemetryMap
697 (constructor
698 TelemetryCaptureValue
699 TelemetryMembersNext
700 b"input_completed_updates"
701 (constructor TelemetryCaptureValue TelemetryUnsigned 4)
702 (constructor
703 TelemetryCaptureValue
704 TelemetryMembersNext
705 b"output_completed_updates"
706 (constructor TelemetryCaptureValue TelemetryUnsigned 5)
707 (constructor
708 TelemetryCaptureValue
709 TelemetryMembersNext
710 b"output_completed_invocations"
711 (constructor TelemetryCaptureValue TelemetryUnsigned 6)
712 (constructor TelemetryCaptureValue TelemetryMembersEnd)))))
713 (constructor TelemetryCaptureValue TelemetryMembersEnd)))))))))
714
715def nvidiaRequestContinuationSchema =
716 (telemetryRecordJSON
717 (telemetryRecordSchemaJSON
718 nvidiaRequestContinuationDeclaration
719 b"Committed checkpoint continuation"
720 (constructor
721 JSON
722 JSONObject
723 (aosField
724 b"transition"
725 (nvidiaRequestCaptureField b"ref:transition")
726 (aosField
727 b"inputs"
728 (nvidiaRequestCaptureField b"list:ref:state")
729 (aosField
730 b"outputs"
731 (nvidiaRequestCaptureField b"list:ref:state")
732 (aosField
733 b"outcome"
734 (nvidiaRequestCaptureField b"text")
735 (aosField
736 b"reason"
737 (nvidiaRequestCaptureField b"text")
738 (aosField
739 b"mechanism"
740 (nvidiaRequestCaptureField b"text")
741 (aosField b"coordinate" (nvidiaRequestCaptureField b"map") aosObjectEnd))))))))))
742
743def nvidiaRequestContinuationTag : Nat =
744 (succ nvidiaRequestDriverTag)
745
746def nvidiaRequestPersistenceDeclaration =
747 (lambda unrestricted stage : Bytes .
748 (constructor
749 TelemetryRecordDeclaration
750 TelemetryRecordDeclarationValue
751 b"alpha.checkpoint.persistence@1"
752 b"state"
753 (capturePolicyIdentifier nvidiaRequestCapturePolicy)
754 b"reported"
755 b"persistence owner reached checkpoint preparation or writable temporary file"
756 (constructor
757 TelemetryCaptureValue
758 TelemetryMembersNext
759 b"phase"
760 (constructor TelemetryCaptureValue TelemetryUnsigned 0)
761 (constructor
762 TelemetryCaptureValue
763 TelemetryMembersNext
764 b"stage"
765 (constructor TelemetryCaptureValue TelemetryConstant (constructor AosValue AosText stage))
766 (constructor TelemetryCaptureValue TelemetryMembersEnd)))))
767
768def nvidiaRequestPersistenceSchema =
769 (telemetryRecordJSON
770 (telemetryRecordSchemaJSON
771 (nvidiaRequestPersistenceDeclaration b"")
772 b"Native checkpoint write lifecycle"
773 (constructor
774 JSON
775 JSONObject
776 (aosField
777 b"phase"
778 (nvidiaRequestCaptureField b"u64")
779 (aosField b"stage" (nvidiaRequestCaptureField b"text") aosObjectEnd)))))
780
781def nvidiaRequestCheckpointPreparingTag : Nat =
782 (succ nvidiaRequestContinuationTag)
783
784def nvidiaRequestCheckpointWritingTag : Nat =
785 (succ nvidiaRequestCheckpointPreparingTag)
786
787-- Binding hashes the exact admitted prefix from file offset zero, without
788-- retaining input bytes. The operation owner supplies the extent it hashed;
789-- neither a filename nor a configured corpus name is a content identity.
790def nvidiaRequestInputDeclaration =
791 (constructor
792 TelemetryRecordDeclaration
793 TelemetryRecordDeclarationValue
794 b"alpha.execution.input-binding@1"
795 b"event"
796 (capturePolicyIdentifier nvidiaRequestCapturePolicy)
797 b"reported"
798 b"SHA-256 from the native input binding owner"
799 (constructor
800 TelemetryCaptureValue
801 TelemetryMembersNext
802 b"input_sha256"
803 (constructor TelemetryCaptureValue TelemetryBytes 0 checkpointEnvelopeDigestBytes)
804 (constructor
805 TelemetryCaptureValue
806 TelemetryMembersNext
807 b"hashed_prefix_bytes"
808 (constructor TelemetryCaptureValue TelemetryUnsigned 4)
809 (constructor
810 TelemetryCaptureValue
811 TelemetryMembersNext
812 b"basis"
813 (constructor
814 TelemetryCaptureValue
815 TelemetryConstant
816 (constructor AosValue AosText b"input descriptor byte prefix from offset zero"))
817 (constructor TelemetryCaptureValue TelemetryMembersEnd)))))
818
819def nvidiaRequestInputSchema =
820 (telemetryRecordJSON
821 (telemetryRecordSchemaJSON
822 nvidiaRequestInputDeclaration
823 b"Bound execution input bytes"
824 (constructor
825 JSON
826 JSONObject
827 (aosField
828 b"input_sha256"
829 (nvidiaRequestCaptureField b"bytes")
830 (aosField
831 b"hashed_prefix_bytes"
832 (nvidiaRequestCaptureField b"u64")
833 (aosField b"basis" (nvidiaRequestCaptureField b"text") aosObjectEnd))))))
834
835def nvidiaRequestInputTag : Nat =
836 (succ nvidiaRequestCheckpointWritingTag)
837
838def nvidiaRequestCaptureLastTag : Nat =
839 nvidiaRequestInputTag
840
841def nvidiaRequestCheckpointIdentitySites =
842 (lambda unrestricted tail : (family TelemetryPolicySites) .
843 (nvidiaRequestCheckpointSite
844 nvidiaRequestCheckpointManifestInputTag
845 b"00000000000000000000000000000600"
846 b"request-host:manifest-admitted"
847 8
848 (nvidiaRequestCheckpointManifestDeclaration b"admitted")
849 (nvidiaRequestCheckpointSite
850 nvidiaRequestCheckpointManifestOutputTag
851 b"00000000000000000000000000000601"
852 b"request-host:manifest-published"
853 8
854 (nvidiaRequestCheckpointManifestDeclaration b"published")
855 (nvidiaRequestCheckpointSite
856 nvidiaRequestCheckpointStateTag
857 b"00000000000000000000000000000602"
858 b"request-host:state-declared"
859 4
860 nvidiaRequestCheckpointStateDeclaration
861 (nvidiaRequestCheckpointSite
862 nvidiaRequestCheckpointCommittedTag
863 b"00000000000000000000000000000603"
864 b"request-host:checkpoint-committed"
865 4
866 (nvidiaRequestCheckpointIdentityDeclaration b"committed")
867 (nvidiaRequestCheckpointSite
868 nvidiaRequestCheckpointRestoredTag
869 b"00000000000000000000000000000604"
870 b"request-host:checkpoint-restored"
871 4
872 (nvidiaRequestCheckpointIdentityDeclaration b"restored")
873 tail))))))
874
875def nvidiaRequestCaptureSitesWithCheckpoint =
876 (nvidiaRequestCheckpointSite
877 nvidiaRequestInputTag
878 b"00000000000000000000000000000609"
879 b"request-host:input-bound"
880 5
881 nvidiaRequestInputDeclaration
882 (nvidiaRequestCheckpointSite
883 nvidiaRequestCheckpointPreparingTag
884 b"00000000000000000000000000000607"
885 b"request-host:checkpoint-preparing"
886 1
887 (nvidiaRequestPersistenceDeclaration b"preparing")
888 (nvidiaRequestCheckpointSite
889 nvidiaRequestCheckpointWritingTag
890 b"00000000000000000000000000000608"
891 b"request-host:checkpoint-writing"
892 1
893 (nvidiaRequestPersistenceDeclaration b"writing")
894 (nvidiaRequestCheckpointSite
895 nvidiaRequestContinuationTag
896 b"00000000000000000000000000000606"
897 b"request-host:committed-continuation"
898 7
899 nvidiaRequestContinuationDeclaration
900 (nvidiaRequestCheckpointSite
901 nvidiaRequestDriverTag
902 b"00000000000000000000000000000605"
903 b"request-host:driver-context"
904 8
905 nvidiaRequestDriverDeclaration
906 (nvidiaRequestCheckpointIdentitySites
907 (nvidiaRequestCheckpointSite
908 nvidiaRequestCheckpointCaptureTag
909 b"00000000000000000000000000000508"
910 b"request-host:published-checkpoint-frontier"
911 3
912 nvidiaRequestCheckpointCaptureDeclaration
913 (nvidiaRequestCheckpointSite
914 nvidiaRequestCheckpointInputTag
915 b"00000000000000000000000000000509"
916 b"request-host:checkpoint-input-admission"
917 1
918 nvidiaRequestCheckpointInputDeclaration
919 (nvidiaRequestCheckpointSite
920 nvidiaRequestCheckpointAdmittedTag
921 b"0000000000000000000000000000050a"
922 b"request-host:admitted-checkpoint-frontier"
923 3
924 nvidiaRequestCheckpointAdmittedDeclaration
925 nvidiaRequestCaptureSites)))))))))
926
927-- Read only the declared header words. Neither frontier transports checkpoint
928-- payload bytes, paths, seed material or input data into the journal.
929def nvidiaRequestCheckpointFrontierCapture =
930 (lambda unrestricted tag : Nat .
931 (lambda unrestricted header : Nat .
932 (lambda unrestricted phase : Nat .
933 (lambda unrestricted after : (family NativeObservedSteps) .
934 (let unrestricted missing =
935 (constructor NativeTelemetrySourceWord NativeTelemetryWordOmitted)
936 in
937 (constructor
938 NativeObservedSteps
939 NativeObservedCaptureBoundary
940 tag
941 (constructor
942 NativeTelemetrySourceValues
943 NativeTelemetrySourceValuesValue
944 (constructor
945 NativeTelemetrySourceWord
946 NativeTelemetryWordValue
947 (phLoad (naturalAdd header checkpointEnvelopeUpdatesAt)))
948 (constructor
949 NativeTelemetrySourceWord
950 NativeTelemetryWordValue
951 (phLoad (naturalAdd header checkpointEnvelopeInvocationsAt)))
952 (constructor
953 NativeTelemetrySourceWord
954 NativeTelemetryWordValue
955 (phLoad (naturalAdd header checkpointEnvelopeVersionAt)))
956 missing
957 missing
958 missing
959 missing
960 missing)
961 (phImm phase)
962 after))))))
963
964def nvidiaRequestCheckpointIdentityCapture =
965 (lambda unrestricted tag : Nat .
966 (lambda unrestricted digest : Nat .
967 (lambda unrestricted after : (family NativeObservedSteps) .
968 (constructor
969 NativeObservedSteps
970 NativeObservedCaptureBoundary
971 tag
972 (constructor
973 NativeTelemetrySourceValues
974 NativeTelemetrySourceValuesValue
975 (constructor
976 NativeTelemetrySourceWord
977 NativeTelemetryWordValue
978 (phLoad (naturalAdd digest (naturalMultiply 0 nativePhysicalWordBytes))))
979 (constructor
980 NativeTelemetrySourceWord
981 NativeTelemetryWordValue
982 (phLoad (naturalAdd digest (naturalMultiply 1 nativePhysicalWordBytes))))
983 (constructor
984 NativeTelemetrySourceWord
985 NativeTelemetryWordValue
986 (phLoad (naturalAdd digest (naturalMultiply 2 nativePhysicalWordBytes))))
987 (constructor
988 NativeTelemetrySourceWord
989 NativeTelemetryWordValue
990 (phLoad (naturalAdd digest (naturalMultiply 3 nativePhysicalWordBytes))))
991 (constructor NativeTelemetrySourceWord NativeTelemetryWordOmitted)
992 (constructor NativeTelemetrySourceWord NativeTelemetryWordOmitted)
993 (constructor NativeTelemetrySourceWord NativeTelemetryWordOmitted)
994 (constructor NativeTelemetrySourceWord NativeTelemetryWordOmitted))
995 (phImm 0)
996 after))))
997
998def nvidiaRequestCheckpointManifestCapture =
999 (lambda unrestricted tag : Nat .
1000 (lambda unrestricted digest : Nat .
1001 (lambda unrestricted header : Nat .
1002 (lambda unrestricted after : (family NativeObservedSteps) .
1003 (constructor
1004 NativeObservedSteps
1005 NativeObservedCaptureBoundary
1006 tag
1007 (constructor
1008 NativeTelemetrySourceValues
1009 NativeTelemetrySourceValuesValue
1010 (constructor
1011 NativeTelemetrySourceWord
1012 NativeTelemetryWordValue
1013 (phLoad (naturalAdd digest (naturalMultiply 0 nativePhysicalWordBytes))))
1014 (constructor
1015 NativeTelemetrySourceWord
1016 NativeTelemetryWordValue
1017 (phLoad (naturalAdd digest (naturalMultiply 1 nativePhysicalWordBytes))))
1018 (constructor
1019 NativeTelemetrySourceWord
1020 NativeTelemetryWordValue
1021 (phLoad (naturalAdd digest (naturalMultiply 2 nativePhysicalWordBytes))))
1022 (constructor
1023 NativeTelemetrySourceWord
1024 NativeTelemetryWordValue
1025 (phLoad (naturalAdd digest (naturalMultiply 3 nativePhysicalWordBytes))))
1026 (constructor
1027 NativeTelemetrySourceWord
1028 NativeTelemetryWordValue
1029 (phLoad (naturalAdd header checkpointEnvelopeUpdatesAt)))
1030 (constructor
1031 NativeTelemetrySourceWord
1032 NativeTelemetryWordValue
1033 (phLoad (naturalAdd header checkpointEnvelopeInvocationsAt)))
1034 (constructor
1035 NativeTelemetrySourceWord
1036 NativeTelemetryWordValue
1037 (phLoad (naturalAdd header checkpointEnvelopeHeaderBytesAt)))
1038 (constructor
1039 NativeTelemetrySourceWord
1040 NativeTelemetryWordValue
1041 (phLoad (naturalAdd header checkpointEnvelopePayloadBytesAt))))
1042 (phLoad (naturalAdd header checkpointEnvelopeUpdatesAt))
1043 after)))))
1044
1045def nvidiaRequestContinuationCapture =
1046 (lambda unrestricted after : (family NativeObservedSteps) .
1047 (constructor
1048 NativeObservedSteps
1049 NativeObservedOperation
1050 (constructor
1051 NativePhysicalOperation
1052 NativePhysicalRepeatBeginCounted
1053 (phLoad (naturalAdd prCheckpointHeaderIn checkpointEnvelopeVersionAt)))
1054 (constructor
1055 NativeObservedSteps
1056 NativeObservedCaptureBoundary
1057 nvidiaRequestContinuationTag
1058 (constructor
1059 NativeTelemetrySourceValues
1060 NativeTelemetrySourceValuesValue
1061 (constructor
1062 NativeTelemetrySourceWord
1063 NativeTelemetryWordValue
1064 (phLoad
1065 (naturalAdd prCheckpointInputManifest (naturalMultiply 0 nativePhysicalWordBytes))))
1066 (constructor
1067 NativeTelemetrySourceWord
1068 NativeTelemetryWordValue
1069 (phLoad
1070 (naturalAdd prCheckpointInputManifest (naturalMultiply 1 nativePhysicalWordBytes))))
1071 (constructor
1072 NativeTelemetrySourceWord
1073 NativeTelemetryWordValue
1074 (phLoad
1075 (naturalAdd prCheckpointOutputManifest (naturalMultiply 0 nativePhysicalWordBytes))))
1076 (constructor
1077 NativeTelemetrySourceWord
1078 NativeTelemetryWordValue
1079 (phLoad
1080 (naturalAdd prCheckpointOutputManifest (naturalMultiply 1 nativePhysicalWordBytes))))
1081 (constructor
1082 NativeTelemetrySourceWord
1083 NativeTelemetryWordValue
1084 (phLoad (naturalAdd prCheckpointHeaderIn checkpointEnvelopeUpdatesAt)))
1085 (constructor
1086 NativeTelemetrySourceWord
1087 NativeTelemetryWordValue
1088 (phLoad (naturalAdd prCheckpointHeaderOut checkpointEnvelopeUpdatesAt)))
1089 (constructor
1090 NativeTelemetrySourceWord
1091 NativeTelemetryWordValue
1092 (phLoad (naturalAdd prCheckpointHeaderOut checkpointEnvelopeInvocationsAt)))
1093 (constructor NativeTelemetrySourceWord NativeTelemetryWordOmitted))
1094 (phLoad (naturalAdd prCheckpointHeaderOut checkpointEnvelopeUpdatesAt))
1095 (constructor
1096 NativeObservedSteps
1097 NativeObservedOperation
1098 (constructor NativePhysicalOperation NativePhysicalRepeatEnd)
1099 after))))
1100
1101def nvidiaRequestCheckpointCapture =
1102 (lambda unrestricted after : (family NativeObservedSteps) .
1103 (nvidiaRequestCheckpointFrontierCapture
1104 nvidiaRequestCheckpointCaptureTag
1105 prCheckpointHeaderOut
1106 prTelemetryPublished
1107 (nvidiaRequestCheckpointManifestCapture
1108 nvidiaRequestCheckpointManifestOutputTag
1109 prCheckpointOutputManifest
1110 prCheckpointHeaderOut
1111 (nvidiaRequestCheckpointIdentityCapture
1112 nvidiaRequestCheckpointStateTag
1113 prCheckpointOutputManifest
1114 (nvidiaRequestCheckpointIdentityCapture
1115 nvidiaRequestCheckpointCommittedTag
1116 prCheckpointOutputManifest
1117 (nvidiaRequestContinuationCapture after))))))
1118
1119-- Fresh initialization has no input checkpoint to restore. Only an admitted
1120-- checkpoint can reach this record, after the system's complete load schedule.
1121def nvidiaRequestCheckpointRestoredCapture =
1122 (lambda unrestricted after : (family NativeObservedSteps) .
1123 (constructor
1124 NativeObservedSteps
1125 NativeObservedOperation
1126 (constructor
1127 NativePhysicalOperation
1128 NativePhysicalRepeatBeginCounted
1129 (phLoad (naturalAdd prCheckpointHeaderIn checkpointEnvelopeVersionAt)))
1130 (nvidiaRequestCheckpointIdentityCapture
1131 nvidiaRequestCheckpointRestoredTag
1132 prCheckpointInputManifest
1133 (constructor
1134 NativeObservedSteps
1135 NativeObservedOperation
1136 (constructor NativePhysicalOperation NativePhysicalRepeatEnd)
1137 after))))
1138
1139-- Admission proves the version is either zero (empty input) or one (validated
1140-- layout/identities/chunks). The owner's bounded repeat therefore emits one
1141-- input frontier only for an actual checkpoint. Empty input carries its
1142-- admission decision but has no invented restored counters. This boundary is
1143-- before device upload: it does not claim that GPU restoration has occurred.
1144def nvidiaRequestCheckpointInputCapture =
1145 (lambda unrestricted after : (family NativeObservedSteps) .
1146 (let unrestricted version =
1147 (phLoad (naturalAdd prCheckpointHeaderIn checkpointEnvelopeVersionAt))
1148 in
1149 (let unrestricted missing =
1150 (constructor NativeTelemetrySourceWord NativeTelemetryWordOmitted)
1151 in
1152 (constructor
1153 NativeObservedSteps
1154 NativeObservedCaptureBoundary
1155 nvidiaRequestCheckpointInputTag
1156 (constructor
1157 NativeTelemetrySourceValues
1158 NativeTelemetrySourceValuesValue
1159 (constructor NativeTelemetrySourceWord NativeTelemetryWordValue version)
1160 missing
1161 missing
1162 missing
1163 missing
1164 missing
1165 missing
1166 missing)
1167 (phImm prTelemetryChecked)
1168 (constructor
1169 NativeObservedSteps
1170 NativeObservedOperation
1171 (constructor NativePhysicalOperation NativePhysicalRepeatBeginCounted version)
1172 (nvidiaRequestCheckpointFrontierCapture
1173 nvidiaRequestCheckpointAdmittedTag
1174 prCheckpointHeaderIn
1175 prTelemetryChecked
1176 (nvidiaRequestCheckpointManifestCapture
1177 nvidiaRequestCheckpointManifestInputTag
1178 prCheckpointInputManifest
1179 prCheckpointHeaderIn
1180 (nvidiaRequestCheckpointIdentityCapture
1181 nvidiaRequestCheckpointStateTag
1182 prCheckpointInputManifest
1183 (constructor
1184 NativeObservedSteps
1185 NativeObservedOperation
1186 (constructor NativePhysicalOperation NativePhysicalRepeatEnd)
1187 after)))))))))
1188
1189def nvidiaRequestCapturePlanWithSites =
1190 (lambda unrestricted sites : (family TelemetryPolicySites) .
1191 (lambda unrestricted metadata : (family StdList Bytes) .
1192 (telemetryRoutedPolicyPlan
1193 nvidiaRequestCapturePolicy
1194 sites
1195 (constructor
1196 StdList
1197 StdListCons
1198 Bytes
1199 nvidiaRequestCaptureSchema
1200 (constructor
1201 StdList
1202 StdListCons
1203 Bytes
1204 nvidiaRequestCheckpointCaptureSchema
1205 (constructor
1206 StdList
1207 StdListCons
1208 Bytes
1209 nvidiaRequestCheckpointInputSchema
1210 (constructor
1211 StdList
1212 StdListCons
1213 Bytes
1214 nvidiaRequestCheckpointAdmittedSchema
1215 (constructor
1216 StdList
1217 StdListCons
1218 Bytes
1219 nvidiaRequestCheckpointManifestSchema
1220 (constructor
1221 StdList
1222 StdListCons
1223 Bytes
1224 nvidiaRequestCheckpointStateSchema
1225 (constructor
1226 StdList
1227 StdListCons
1228 Bytes
1229 nvidiaRequestCheckpointIdentitySchema
1230 (constructor
1231 StdList
1232 StdListCons
1233 Bytes
1234 nvidiaRequestDriverSchema
1235 (constructor
1236 StdList
1237 StdListCons
1238 Bytes
1239 nvidiaRequestContinuationSchema
1240 (constructor
1241 StdList
1242 StdListCons
1243 Bytes
1244 nvidiaRequestPersistenceSchema
1245 (constructor
1246 StdList
1247 StdListCons
1248 Bytes
1249 nvidiaRequestInputSchema
1250 metadata))))))))))))))
1251
1252def nvidiaRequestCapturePlan =
1253 (nvidiaRequestCapturePlanWithSites nvidiaRequestCaptureSitesWithCheckpoint)
1254
1255def nvidiaRequestCaptureName =
1256 (lambda unrestricted phase : Nat .
1257 (eliminate
1258 TelemetryPolicySites
1259 (lambda unrestricted current : (family TelemetryPolicySites) . Bytes)
1260 (telemetryPolicySiteLookup (succ phase) nvidiaRequestCaptureSites)
1261 (branch TelemetryPolicySitesEnd . b"")
1262 (branch TelemetryPolicySitesNext tag site record tail induction . (captureSiteName site))))
1263
1264def nvidiaRequestCaptureBoundary =
1265 (lambda unrestricted phase : Nat .
1266 (lambda unrestricted name : Bytes .
1267 (lambda unrestricted after : (family NativeObservedSteps) .
1268 (let unrestricted missing =
1269 (constructor NativeTelemetrySourceWord NativeTelemetryWordOmitted)
1270 in
1271 (constructor
1272 NativeObservedSteps
1273 NativeObservedCaptureBoundary
1274 (aosChoose
1275 Nat
1276 (naturalAnd
1277 (naturalLessOrEqual phase prTelemetryDone)
1278 (bytes-equal (nvidiaRequestCaptureName phase) name))
1279 (succ phase)
1280 0)
1281 (constructor
1282 NativeTelemetrySourceValues
1283 NativeTelemetrySourceValuesValue
1284 (constructor NativeTelemetrySourceWord NativeTelemetryWordValue (phImm phase))
1285 missing
1286 missing
1287 missing
1288 missing
1289 missing
1290 missing
1291 missing)
1292 (phImm phase)
1293 after)))))
1294
1295def nvidiaRequestDriverCapture =
1296 (lambda unrestricted after : (family NativeObservedSteps) .
1297 (constructor
1298 NativeObservedSteps
1299 NativeObservedCaptureBoundary
1300 nvidiaRequestDriverTag
1301 (constructor
1302 NativeTelemetrySourceValues
1303 NativeTelemetrySourceValuesValue
1304 (constructor
1305 NativeTelemetrySourceWord
1306 NativeTelemetryWordValue
1307 (phLoad (naturalAdd phDriverVersionAt (naturalMultiply 0 nativePhysicalWordBytes))))
1308 (constructor
1309 NativeTelemetrySourceWord
1310 NativeTelemetryWordValue
1311 (phLoad (naturalAdd phDriverVersionAt (naturalMultiply 1 nativePhysicalWordBytes))))
1312 (constructor
1313 NativeTelemetrySourceWord
1314 NativeTelemetryWordValue
1315 (phLoad (naturalAdd phDriverVersionAt (naturalMultiply 2 nativePhysicalWordBytes))))
1316 (constructor
1317 NativeTelemetrySourceWord
1318 NativeTelemetryWordValue
1319 (phLoad (naturalAdd phDriverVersionAt (naturalMultiply 3 nativePhysicalWordBytes))))
1320 (constructor
1321 NativeTelemetrySourceWord
1322 NativeTelemetryWordValue
1323 (phLoad (naturalAdd phDriverVersionAt (naturalMultiply 4 nativePhysicalWordBytes))))
1324 (constructor
1325 NativeTelemetrySourceWord
1326 NativeTelemetryWordValue
1327 (phLoad (naturalAdd phDriverVersionAt (naturalMultiply 5 nativePhysicalWordBytes))))
1328 (constructor
1329 NativeTelemetrySourceWord
1330 NativeTelemetryWordValue
1331 (phLoad (naturalAdd phDriverVersionAt (naturalMultiply 6 nativePhysicalWordBytes))))
1332 (constructor
1333 NativeTelemetrySourceWord
1334 NativeTelemetryWordValue
1335 (phLoad (naturalAdd phDriverVersionAt (naturalMultiply 7 nativePhysicalWordBytes)))))
1336 (phImm prTelemetryChannel)
1337 after))
1338
1339def nvidiaRequestCaptureBoundaryWithCheckpointPhases =
1340 (lambda unrestricted phase : Nat .
1341 (lambda unrestricted name : Bytes .
1342 (lambda unrestricted after : (family NativeObservedSteps) .
1343 (nvidiaRequestCaptureBoundary
1344 phase
1345 name
1346 (aosChoose
1347 (family NativeObservedSteps)
1348 (naturalEqual phase prTelemetryPublished)
1349 (nvidiaRequestCheckpointCapture after)
1350 (aosChoose
1351 (family NativeObservedSteps)
1352 (naturalEqual phase prTelemetryChecked)
1353 (nvidiaRequestCheckpointInputCapture after)
1354 (aosChoose
1355 (family NativeObservedSteps)
1356 (naturalEqual phase prTelemetryChannel)
1357 (nvidiaRequestDriverCapture after)
1358 after)))))))
1359
1360def nvidiaRequestPersistenceCapture =
1361 (lambda unrestricted tag : Nat .
1362 (lambda unrestricted phase : Nat .
1363 (lambda unrestricted after : (family NativeObservedSteps) .
1364 (let unrestricted missing =
1365 (constructor NativeTelemetrySourceWord NativeTelemetryWordOmitted)
1366 in
1367 (constructor
1368 NativeObservedSteps
1369 NativeObservedCaptureBoundary
1370 tag
1371 (constructor
1372 NativeTelemetrySourceValues
1373 NativeTelemetrySourceValuesValue
1374 (constructor NativeTelemetrySourceWord NativeTelemetryWordValue (phImm phase))
1375 missing
1376 missing
1377 missing
1378 missing
1379 missing
1380 missing
1381 missing)
1382 (phImm phase)
1383 after)))))
1384
1385def nvidiaRequestCaptureBoundaryWithPersistence =
1386 (lambda unrestricted phase : Nat .
1387 (lambda unrestricted name : Bytes .
1388 (lambda unrestricted after : (family NativeObservedSteps) .
1389 (aosChoose
1390 (family NativeObservedSteps)
1391 (naturalAnd
1392 (naturalEqual phase prTelemetryStateRestored)
1393 (bytes-equal name b"request-host:checkpoint-restored"))
1394 (nvidiaRequestCheckpointRestoredCapture after)
1395 (aosChoose
1396 (family NativeObservedSteps)
1397 (naturalAnd
1398 (naturalEqual phase prTelemetryCheckpointPreparing)
1399 (bytes-equal name b"request-host:checkpoint-preparing"))
1400 (nvidiaRequestPersistenceCapture nvidiaRequestCheckpointPreparingTag phase after)
1401 (aosChoose
1402 (family NativeObservedSteps)
1403 (naturalAnd
1404 (naturalEqual phase prTelemetryCheckpointWriting)
1405 (bytes-equal name b"request-host:checkpoint-writing"))
1406 (nvidiaRequestPersistenceCapture nvidiaRequestCheckpointWritingTag phase after)
1407 (nvidiaRequestCaptureBoundaryWithCheckpointPhases phase name after)))))))
1408
1409def nvidiaRequestInputCapture =
1410 (lambda unrestricted after : (family NativeObservedSteps) .
1411 (let unrestricted missing =
1412 (constructor NativeTelemetrySourceWord NativeTelemetryWordOmitted)
1413 in
1414 (constructor
1415 NativeObservedSteps
1416 NativeObservedCaptureBoundary
1417 nvidiaRequestInputTag
1418 (constructor
1419 NativeTelemetrySourceValues
1420 NativeTelemetrySourceValuesValue
1421 (constructor
1422 NativeTelemetrySourceWord
1423 NativeTelemetryWordValue
1424 (phLoad (naturalAdd prInputIdentity (naturalMultiply 0 nativePhysicalWordBytes))))
1425 (constructor
1426 NativeTelemetrySourceWord
1427 NativeTelemetryWordValue
1428 (phLoad (naturalAdd prInputIdentity (naturalMultiply 1 nativePhysicalWordBytes))))
1429 (constructor
1430 NativeTelemetrySourceWord
1431 NativeTelemetryWordValue
1432 (phLoad (naturalAdd prInputIdentity (naturalMultiply 2 nativePhysicalWordBytes))))
1433 (constructor
1434 NativeTelemetrySourceWord
1435 NativeTelemetryWordValue
1436 (phLoad (naturalAdd prInputIdentity (naturalMultiply 3 nativePhysicalWordBytes))))
1437 (constructor
1438 NativeTelemetrySourceWord
1439 NativeTelemetryWordValue
1440 (phLoad prInputIdentityExtent))
1441 missing
1442 missing
1443 missing)
1444 (phImm prTelemetryInputBound)
1445 after)))
1446
1447def nvidiaRequestCaptureBoundaryWithCheckpoint =
1448 (lambda unrestricted phase : Nat .
1449 (lambda unrestricted name : Bytes .
1450 (lambda unrestricted after : (family NativeObservedSteps) .
1451 (aosChoose
1452 (family NativeObservedSteps)
1453 (naturalAnd
1454 (naturalEqual phase prTelemetryInputBound)
1455 (bytes-equal name b"request-host:input-bound"))
1456 (nvidiaRequestInputCapture after)
1457 (nvidiaRequestCaptureBoundaryWithPersistence phase name after)))))
1458
1459-- The application owns the filename/stat buffer and descriptors, while the
1460-- recorder owns identity bytes and journal construction. All extents/slots are
1461-- derived after the maintained request host's original declarations.
1462def nvidiaRequestCaptureScalarAt : Nat =
1463 phStateExtent
1464
1465def nvidiaRequestCapturePathAt : Nat =
1466 (naturalAdd nvidiaRequestCaptureScalarAt nativePhysicalWordBytes)
1467
1468def nvidiaRequestCaptureBytes : Nat =
1469 (naturalAdd nvidiaRequestCapturePathAt nativeObservedJournalBytes)
1470
1471def nvidiaRequestCaptureFileSlot : Nat =
1472 phSlots
1473
1474def nvidiaRequestCaptureDirectorySlot : Nat =
1475 (succ nvidiaRequestCaptureFileSlot)
1476
1477def nvidiaRequestCaptureWorkSlot : Nat =
1478 (succ nvidiaRequestCaptureDirectorySlot)
1479
1480def nvidiaRequestCaptureSlots : Nat =
1481 (succ nvidiaRequestCaptureWorkSlot)
1482
1483-- Read one exact binary32 cell at a declared safe host boundary. Public
1484-- scratch is disjoint from application buffers and recorder-private state.
1485-- A second word carries the caller's declared coordinate. Neither word is
1486-- interpreted as a learning quantity by this transport mechanism.
1487def nvidiaRequestCaptureMappedF32 =
1488 (lambda unrestricted tag : Nat .
1489 (lambda unrestricted address : Nat .
1490 (lambda unrestricted coordinate : (family NativePhysicalOperand) .
1491 (lambda unrestricted after : (family NativeObservedSteps) .
1492 (nativeObservedPrefixWith
1493 (phCopy nvidiaRequestCaptureScalarAt (phZeros nativePhysicalWordBytes))
1494 (nativeObservedPrefixWith
1495 (phCopyMappedToState
1496 address
1497 nvidiaRequestCaptureScalarAt
1498 (bytes-length (dataBytesWord32LE (modelWord32FromNaturalTruncated 0))))
1499 (let unrestricted missing =
1500 (constructor NativeTelemetrySourceWord NativeTelemetryWordOmitted)
1501 in
1502 (constructor
1503 NativeObservedSteps
1504 NativeObservedCaptureBoundary
1505 tag
1506 (constructor
1507 NativeTelemetrySourceValues
1508 NativeTelemetrySourceValuesValue
1509 (constructor
1510 NativeTelemetrySourceWord
1511 NativeTelemetryWordValue
1512 (phLoad nvidiaRequestCaptureScalarAt))
1513 (constructor NativeTelemetrySourceWord NativeTelemetryWordValue coordinate)
1514 missing
1515 missing
1516 missing
1517 missing
1518 missing
1519 missing)
1520 coordinate
1521 after))))))))
1522
1523def nvidiaRequestCaptureCleanup =
1524 (nativeObservedPrefixWith
1525 (nativeObservedJournalClose
1526 nvidiaRequestCaptureFileSlot
1527 nvidiaRequestCaptureWorkSlot
1528 b"telemetry:journal-close")
1529 (nativeObservedPrefixWith
1530 (nativeObservedJournalClose
1531 nvidiaRequestCaptureDirectorySlot
1532 nvidiaRequestCaptureWorkSlot
1533 b"telemetry:journal-directory-close")
1534 (constructor NativeObservedSteps NativeObservedStepsEnd)))
1535
1536def nvidiaPlanHostManagedRequestStepsWithBoundary =
1537 (lambda unrestricted boundary : (pi unrestricted phase : Nat . (pi unrestricted name : Bytes . (pi unrestricted rest : (family NativeObservedSteps) . (family NativeObservedSteps)))) .
1538 (nvidiaPlanHostRequestWith
1539 (family NativeObservedSteps)
1540 nativeObservedPrefixWith
1541 (lambda unrestricted after : (family NativeObservedSteps) .
1542 (constructor
1543 NativeObservedSteps
1544 NativeObservedOpenJournal
1545 nvidiaRequestCapturePathAt
1546 nvidiaRequestCaptureFileSlot
1547 nvidiaRequestCaptureDirectorySlot
1548 (nativeObservedPrefixWith phTelemetryOpen after)))
1549 boundary
1550 (constructor NativeObservedSteps NativeObservedFinish nvidiaRequestCaptureCleanup)))
1551
1552def nvidiaPlanHostManagedRequestSteps =
1553 (nvidiaPlanHostManagedRequestStepsWithBoundary nvidiaRequestCaptureBoundaryWithCheckpoint)
1554
1555-- Assignment is a declared input capability. The same source schedule and
1556-- capture layout serve both fresh and caller-assigned run membership; the
1557-- recorder still acquires its own producer epoch before opening its journal.
1558-- The request ABI occupies argv[1]. Assigned request artifacts add one
1559-- declared file input at argv[2], rather than interpreting environment state.
1560def nvidiaRequestAssignedIdentitySource : (family NativeTelemetryIdentitySource) =
1561 (constructor
1562 NativeTelemetryIdentitySource
1563 NativeTelemetryAssignedFile
1564 (constructor NativePhysicalOperand NativePhysicalProcessArgument (phWord 2)))
1565
1566def nvidiaPlanHostManagedRequestProgramWithBoundary =
1567 (lambda unrestricted boundary : (pi unrestricted phase : Nat . (pi unrestricted name : Bytes . (pi unrestricted rest : (family NativeObservedSteps) . (family NativeObservedSteps)))) .
1568 (lambda unrestricted source : (family NativeTelemetryIdentitySource) .
1569 (lambda unrestricted capturePlan : (family TelemetryRoutedPolicyPlan) .
1570 (lambda unrestricted layout : (family NvidiaPlanHostLayout) .
1571 (lambda unrestricted hostIdentity : Bytes .
1572 (lambda unrestricted programIdentity : Bytes .
1573 (lambda unrestricted qmdIdentity : Bytes .
1574 (lambda unrestricted pushIdentity : Bytes .
1575 (lambda unrestricted gpfifoIdentity : Bytes .
1576 (lambda unrestricted programLength : Nat .
1577 (lambda unrestricted qmdLength : Nat .
1578 (lambda unrestricted pushLength : Nat .
1579 (lambda unrestricted gpfifoLength : Nat .
1580 (lambda unrestricted submissionCount : Nat .
1581 (lambda unrestricted input : (family NvidiaPlanHostInputContract) .
1582 (lambda unrestricted contract : (family CheckpointEnvelopeContract) .
1583 (lambda unrestricted fills : (family NvidiaPlanHostRecipeFills) .
1584 (lambda unrestricted learner : (pi unrestricted after : (family NativePhysicalCommands) . (family NativePhysicalCommands)) .
1585 (lambda unrestricted steps : (family NvidiaPlanHostSteps) .
1586 (nativeObservedRequireProgram
1587 (nativeObservedBuildProgramWithIdentitySource
1588 source
1589 nvidiaRequestCaptureBytes
1590 nvidiaRequestCaptureSlots
1591 capturePlan
1592 (phSlot nvidiaRequestCaptureFileSlot)
1593 (phSlot nvidiaRequestCaptureDirectorySlot)
1594 hostIdentity
1595 (nvidiaPlanHostManagedRequestStepsWithBoundary
1596 boundary
1597 layout
1598 hostIdentity
1599 programIdentity
1600 qmdIdentity
1601 pushIdentity
1602 gpfifoIdentity
1603 programLength
1604 qmdLength
1605 pushLength
1606 gpfifoLength
1607 submissionCount
1608 input
1609 contract
1610 fills
1611 learner
1612 steps))))))))))))))))))))))
1613
1614def nvidiaPlanHostManagedRequestProgramWithIdentitySource =
1615 (nvidiaPlanHostManagedRequestProgramWithBoundary nvidiaRequestCaptureBoundaryWithCheckpoint)
1616
1617def nvidiaPlanHostManagedRequestProgram =
1618 (nvidiaPlanHostManagedRequestProgramWithIdentitySource
1619 (constructor NativeTelemetryIdentitySource NativeTelemetryFreshIdentity))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.