module Platform.Linux.Nvidia.RequestCapture import Checkpoint.Envelope import Data.Bytes import Data.UTF8 import Data.JSON import Data.JSONAccess import Data.JSONRender import Model.Config import Model.Parameter import Model.Word32 import Model.Word64 import Observe.CapturePolicy import Observe.Interchange import Observe.Value import Platform.Linux.Nvidia.PlanHost import Platform.Linux.Nvidia.PlanHostRequest import Platform.Linux.Nvidia.ObservedRequest import Runtime.NativeLaunchRecipeLoad import Runtime.NativeObservedProgram import Runtime.NativeObservedJournal import Runtime.NativePhysicalProgram import Runtime.NativeTelemetry import Runtime.NativeTelemetryIdentity import Runtime.NativeTelemetryPolicy import Runtime.TelemetryCapture import Runtime.TelemetryDrain import Runtime.TelemetryIdentity import Runtime.TelemetryPolicy import Runtime.TelemetryPublication import Runtime.TelemetryRecord import Std.Byte import Std.Flag import Std.List import Std.Natural -- Protocol boundaries report only what the host reached. These are not loss, -- token, update or latency measurements. Names are static schema-bound values; -- phase IDs remain the request protocol's IDs. Source time stays unavailable. -- The encoded batch budget is the whole publication frame -- (Runtime.TelemetryPublication.publicationMaximumFrameBytes). Every batch of -- this policy carries the complete declared descriptor inventory: the shared -- request, checkpoint, driver-context, continuation, persistence and -- input-binding sites plus each system's own sites, schemas and metadata. -- Bob's inventory alone needs 35,276 bytes (32,193 of descriptors), so the -- former 32,768-byte budget refused the recorder declaration. The routed plan -- still refuses any program whose declared batch exceeds the frame. def nvidiaRequestCapturePolicy = (constructor CapturePolicy CapturePolicyValue 1 b"00000000000000000000000000000500" (constructor CaptureProfile CaptureLifecycleProfile) 0 0 2 publicationMaximumFrameBytes 8 1 1) def nvidiaRequestCaptureDeclaration = (lambda unrestricted name : Bytes . (constructor TelemetryRecordDeclaration TelemetryRecordDeclarationValue b"alpha.request.boundary@1" b"diagnostic" (capturePolicyIdentifier nvidiaRequestCapturePolicy) b"reported" b"maintained request lifecycle boundary reached" (constructor TelemetryCaptureValue TelemetryMembersNext b"phase" (constructor TelemetryCaptureValue TelemetryUnsigned 0) (constructor TelemetryCaptureValue TelemetryMembersNext b"name" (constructor TelemetryCaptureValue TelemetryConstant (constructor AosValue AosText name)) (constructor TelemetryCaptureValue TelemetryMembersEnd))))) def nvidiaRequestCaptureField = (lambda unrestricted kind : Bytes . (constructor JSON JSONObject (telemetryPolicyMember b"type" (constructor JSON JSONString kind) (constructor JSON JSONObjectEnd)))) def nvidiaRequestCaptureSchema = (telemetryRecordJSON (telemetryRecordSchemaJSON (nvidiaRequestCaptureDeclaration b"") b"Alpha request host protocol" (constructor JSON JSONObject (telemetryPolicyMember b"phase" (nvidiaRequestCaptureField b"u64") (telemetryPolicyMember b"name" (nvidiaRequestCaptureField b"text") (constructor JSON JSONObjectEnd)))))) def nvidiaRequestCaptureSite = (lambda unrestricted phase : Nat . (lambda unrestricted name : Bytes . (lambda unrestricted identifier : Bytes . (lambda unrestricted tail : (family TelemetryPolicySites) . (constructor TelemetryPolicySites TelemetryPolicySitesNext (succ phase) (constructor CaptureSite CaptureSiteValue identifier name (constructor CaptureClass CaptureLifecycleClass) 1 2 1) (nvidiaRequestCaptureDeclaration name) tail))))) def nvidiaRequestCaptureSites = (nvidiaRequestCaptureSite prTelemetryBegin b"request-host:begin" b"00000000000000000000000000000501" (nvidiaRequestCaptureSite prTelemetryChecked b"request-host:request-checked" b"00000000000000000000000000000502" (nvidiaRequestCaptureSite prTelemetryChannel b"request-host:channel-ready" b"00000000000000000000000000000503" (nvidiaRequestCaptureSite prTelemetryUploaded b"request-host:uploaded" b"00000000000000000000000000000504" (nvidiaRequestCaptureSite prTelemetryLearner b"request-host:learner-scalars" b"00000000000000000000000000000505" (nvidiaRequestCaptureSite prTelemetryPublished b"request-host:checkpoint-published" b"00000000000000000000000000000506" (nvidiaRequestCaptureSite prTelemetryDone b"request-host:done" b"00000000000000000000000000000507" (constructor TelemetryPolicySites TelemetryPolicySitesEnd)))))))) -- A companion to the lifecycle record, emitted only after the persistence -- owner has completed all publication stages, including directory fsync. Read -- the header it actually wrote: a custom schedule may publish a different -- number of updates/invocations from the contract's default. This is the -- checkpoint frontier, not per-update timing, loss or consumer receipt. def nvidiaRequestCheckpointCaptureTag : Nat = (succ (succ prTelemetryDone)) -- Input and output frontiers have the same header representation, while their -- schemas and capture sites keep admission separate from durable publication. def nvidiaRequestCheckpointFrontierDeclaration = (lambda unrestricted schema : Bytes . (lambda unrestricted method : Bytes . (constructor TelemetryRecordDeclaration TelemetryRecordDeclarationValue schema b"diagnostic" (capturePolicyIdentifier nvidiaRequestCapturePolicy) b"reported" method (constructor TelemetryCaptureValue TelemetryMembersNext b"completed_updates" (constructor TelemetryCaptureValue TelemetryUnsigned 0) (constructor TelemetryCaptureValue TelemetryMembersNext b"completed_invocations" (constructor TelemetryCaptureValue TelemetryUnsigned 1) (constructor TelemetryCaptureValue TelemetryMembersNext b"envelope_version" (constructor TelemetryCaptureValue TelemetryUnsigned 2) (constructor TelemetryCaptureValue TelemetryMembersEnd))))))) def nvidiaRequestCheckpointCaptureDeclaration = (nvidiaRequestCheckpointFrontierDeclaration b"alpha.checkpoint.published-frontier@1" b"published checkpoint header after file and directory synchronization") def nvidiaRequestCheckpointAdmittedDeclaration = (nvidiaRequestCheckpointFrontierDeclaration b"alpha.checkpoint.admitted-frontier@1" b"input checkpoint header after layout, identity and chunk admission; before device upload") def nvidiaRequestCheckpointInputDeclaration = (constructor TelemetryRecordDeclaration TelemetryRecordDeclarationValue b"alpha.checkpoint.input-admission@1" b"diagnostic" (capturePolicyIdentifier nvidiaRequestCapturePolicy) b"reported" b"admitted input envelope version: zero means empty input; one means validated checkpoint" (constructor TelemetryCaptureValue TelemetryMembersNext b"envelope_version" (constructor TelemetryCaptureValue TelemetryUnsigned 0) (constructor TelemetryCaptureValue TelemetryMembersEnd))) def nvidiaRequestCheckpointFrontierSchema = (lambda unrestricted declaration : (family TelemetryRecordDeclaration) . (lambda unrestricted name : Bytes . (telemetryRecordJSON (telemetryRecordSchemaJSON declaration name (constructor JSON JSONObject (telemetryPolicyMember b"completed_updates" (nvidiaRequestCaptureField b"u64") (telemetryPolicyMember b"completed_invocations" (nvidiaRequestCaptureField b"u64") (telemetryPolicyMember b"envelope_version" (nvidiaRequestCaptureField b"u64") (constructor JSON JSONObjectEnd))))))))) def nvidiaRequestCheckpointCaptureSchema = (nvidiaRequestCheckpointFrontierSchema nvidiaRequestCheckpointCaptureDeclaration b"Published native checkpoint frontier") def nvidiaRequestCheckpointAdmittedSchema = (nvidiaRequestCheckpointFrontierSchema nvidiaRequestCheckpointAdmittedDeclaration b"Admitted native checkpoint frontier") def nvidiaRequestCheckpointInputSchema = (telemetryRecordJSON (telemetryRecordSchemaJSON nvidiaRequestCheckpointInputDeclaration b"Native checkpoint input admission" (constructor JSON JSONObject (telemetryPolicyMember b"envelope_version" (nvidiaRequestCaptureField b"u64") (constructor JSON JSONObjectEnd))))) def nvidiaRequestCheckpointInputTag : Nat = (succ nvidiaRequestCheckpointCaptureTag) def nvidiaRequestCheckpointAdmittedTag : Nat = (succ nvidiaRequestCheckpointInputTag) def nvidiaRequestCheckpointSite = (lambda unrestricted tag : Nat . (lambda unrestricted identity : Bytes . (lambda unrestricted name : Bytes . (lambda unrestricted dimensions : Nat . (lambda unrestricted declaration : (family TelemetryRecordDeclaration) . (lambda unrestricted tail : (family TelemetryPolicySites) . (constructor TelemetryPolicySites TelemetryPolicySitesNext tag (constructor CaptureSite CaptureSiteValue identity name (constructor CaptureClass CaptureLifecycleClass) 1 dimensions 1) declaration tail))))))) -- A manifest commits the persisted composite learning state, including all -- payload chunk hashes and counters. The full digest remains alongside every -- truncated typed reference. Tensor bytes are not retained by these records. def nvidiaRequestCheckpointManifestDeclaration = (lambda unrestricted stage : Bytes . (constructor TelemetryRecordDeclaration TelemetryRecordDeclarationValue b"alpha.checkpoint.manifest@1" b"state" (capturePolicyIdentifier nvidiaRequestCapturePolicy) b"reported" b"SHA-256 of the complete checkpoint envelope header, including payload chunk hashes; not the whole file digest" (constructor TelemetryCaptureValue TelemetryMembersNext b"manifest_sha256" (constructor TelemetryCaptureValue TelemetryBytes 0 checkpointEnvelopeDigestBytes) (constructor TelemetryCaptureValue TelemetryMembersNext b"completed_updates" (constructor TelemetryCaptureValue TelemetryUnsigned 4) (constructor TelemetryCaptureValue TelemetryMembersNext b"completed_invocations" (constructor TelemetryCaptureValue TelemetryUnsigned 5) (constructor TelemetryCaptureValue TelemetryMembersNext b"manifest_header_bytes" (constructor TelemetryCaptureValue TelemetryUnsigned 6) (constructor TelemetryCaptureValue TelemetryMembersNext b"payload_bytes" (constructor TelemetryCaptureValue TelemetryUnsigned 7) (constructor TelemetryCaptureValue TelemetryMembersNext b"stage" (constructor TelemetryCaptureValue TelemetryConstant (constructor AosValue AosText stage)) (constructor TelemetryCaptureValue TelemetryMembersEnd))))))))) def nvidiaRequestCheckpointStateDeclaration = (constructor TelemetryRecordDeclaration TelemetryRecordDeclarationValue b"aos.state.declared@1" b"state" (capturePolicyIdentifier nvidiaRequestCapturePolicy) b"reported" b"checkpoint manifest SHA-256 first 16 bytes identify the composite checkpointed state" (constructor TelemetryCaptureValue TelemetryMembersNext b"state" (constructor TelemetryCaptureValue TelemetryReference b"state" 0) (constructor TelemetryCaptureValue TelemetryMembersNext b"name" (constructor TelemetryCaptureValue TelemetryConstant (constructor AosValue AosText b"Checkpointed learning-system state")) (constructor TelemetryCaptureValue TelemetryMembersNext b"domain" (constructor TelemetryCaptureValue TelemetryConstant (constructor AosValue AosText b"learning-system")) (constructor TelemetryCaptureValue TelemetryMembersNext b"owner" (constructor TelemetryCaptureValue TelemetryUnavailable b"not_recorded" b"checkpoint-owner-entity-not-recorded") (constructor TelemetryCaptureValue TelemetryMembersNext b"content" (constructor TelemetryCaptureValue TelemetryUnavailable b"not_recorded" b"checkpoint-payload-not-retained") (constructor TelemetryCaptureValue TelemetryMembersNext b"manifest_sha256" (constructor TelemetryCaptureValue TelemetryBytes 0 checkpointEnvelopeDigestBytes) (constructor TelemetryCaptureValue TelemetryMembersEnd)))))))) def nvidiaRequestCheckpointIdentityDeclaration = (lambda unrestricted phase : Bytes . (constructor TelemetryRecordDeclaration TelemetryRecordDeclarationValue b"aos.state.checkpoint@1" b"state" (capturePolicyIdentifier nvidiaRequestCapturePolicy) b"reported" b"persistence or restoration owner reached the named checkpoint boundary" (constructor TelemetryCaptureValue TelemetryMembersNext b"checkpoint" (constructor TelemetryCaptureValue TelemetryReference b"checkpoint" 0) (constructor TelemetryCaptureValue TelemetryMembersNext b"states" (constructor TelemetryCaptureValue TelemetryList (constructor TelemetryCaptureValue TelemetryItemsNext (constructor TelemetryCaptureValue TelemetryReference b"state" 0) (constructor TelemetryCaptureValue TelemetryItemsEnd))) (constructor TelemetryCaptureValue TelemetryMembersNext b"phase" (constructor TelemetryCaptureValue TelemetryConstant (constructor AosValue AosText phase)) (constructor TelemetryCaptureValue TelemetryMembersNext b"artifact" (constructor TelemetryCaptureValue TelemetryUnavailable b"not_recorded" b"checkpoint-file-content-not-retained-by-telemetry") (constructor TelemetryCaptureValue TelemetryMembersNext b"manifest_sha256" (constructor TelemetryCaptureValue TelemetryBytes 0 checkpointEnvelopeDigestBytes) (constructor TelemetryCaptureValue TelemetryMembersEnd)))))))) def nvidiaRequestCheckpointManifestSchema = (telemetryRecordJSON (telemetryRecordSchemaJSON (nvidiaRequestCheckpointManifestDeclaration b"") b"Native checkpoint manifest commitment" (constructor JSON JSONObject (aosField b"manifest_sha256" (nvidiaRequestCaptureField b"bytes") (aosField b"completed_updates" (nvidiaRequestCaptureField b"u64") (aosField b"completed_invocations" (nvidiaRequestCaptureField b"u64") (aosField b"manifest_header_bytes" (nvidiaRequestCaptureField b"u64") (aosField b"payload_bytes" (nvidiaRequestCaptureField b"u64") (aosField b"stage" (nvidiaRequestCaptureField b"text") aosObjectEnd))))))))) def nvidiaRequestCheckpointStateSchema = (telemetryRecordJSON (telemetryRecordSchemaJSON nvidiaRequestCheckpointStateDeclaration b"Composite checkpoint state" (constructor JSON JSONObject (aosField b"state" (nvidiaRequestCaptureField b"ref:state") (aosField b"name" (nvidiaRequestCaptureField b"text") (aosField b"domain" (nvidiaRequestCaptureField b"text") (aosField b"owner" (nvidiaRequestCaptureField b"text") (aosField b"content" (nvidiaRequestCaptureField b"text") (aosField b"manifest_sha256" (nvidiaRequestCaptureField b"bytes") aosObjectEnd))))))))) def nvidiaRequestCheckpointIdentitySchema = (telemetryRecordJSON (telemetryRecordSchemaJSON (nvidiaRequestCheckpointIdentityDeclaration b"") b"Native checkpoint persistence and restoration" (constructor JSON JSONObject (aosField b"checkpoint" (nvidiaRequestCaptureField b"ref:checkpoint") (aosField b"states" (nvidiaRequestCaptureField b"list:ref:state") (aosField b"phase" (nvidiaRequestCaptureField b"text") (aosField b"artifact" (nvidiaRequestCaptureField b"ref:artifact") (aosField b"manifest_sha256" (nvidiaRequestCaptureField b"bytes") aosObjectEnd)))))))) def nvidiaRequestCheckpointManifestInputTag : Nat = (succ nvidiaRequestCheckpointAdmittedTag) def nvidiaRequestCheckpointManifestOutputTag : Nat = (succ nvidiaRequestCheckpointManifestInputTag) def nvidiaRequestCheckpointStateTag : Nat = (succ nvidiaRequestCheckpointManifestOutputTag) def nvidiaRequestCheckpointCommittedTag : Nat = (succ nvidiaRequestCheckpointStateTag) def nvidiaRequestCheckpointRestoredTag : Nat = (succ nvidiaRequestCheckpointCommittedTag) -- These bytes come from the admitted driver's version-query response, not -- the target's expected ABI branch. No firmware or operating-state query is -- implied by reaching the channel boundary. def nvidiaRequestDriverDeclaration = (constructor TelemetryRecordDeclaration TelemetryRecordDeclarationValue b"alpha.device.driver-context@1" b"event" (capturePolicyIdentifier nvidiaRequestCapturePolicy) b"reported" b"Linux NVIDIA driver version query after branch admission" (constructor TelemetryCaptureValue TelemetryMembersNext b"version_query_bytes" (constructor TelemetryCaptureValue TelemetryBytes 0 phDriverVersionBytes) (constructor TelemetryCaptureValue TelemetryMembersNext b"firmware" (constructor TelemetryCaptureValue TelemetryUnavailable b"not_recorded" b"firmware-not-queried") (constructor TelemetryCaptureValue TelemetryMembersNext b"clocks" (constructor TelemetryCaptureValue TelemetryUnavailable b"not_recorded" b"clocks-not-queried") (constructor TelemetryCaptureValue TelemetryMembersNext b"power" (constructor TelemetryCaptureValue TelemetryUnavailable b"not_recorded" b"power-not-queried") (constructor TelemetryCaptureValue TelemetryMembersNext b"temperature" (constructor TelemetryCaptureValue TelemetryUnavailable b"not_recorded" b"temperature-not-queried") (constructor TelemetryCaptureValue TelemetryMembersEnd))))))) def nvidiaRequestDriverSchema = (telemetryRecordJSON (telemetryRecordSchemaJSON nvidiaRequestDriverDeclaration b"Admitted native driver context" (constructor JSON JSONObject (aosField b"version_query_bytes" (nvidiaRequestCaptureField b"bytes") (aosField b"firmware" (nvidiaRequestCaptureField b"text") (aosField b"clocks" (nvidiaRequestCaptureField b"text") (aosField b"power" (nvidiaRequestCaptureField b"text") (aosField b"temperature" (nvidiaRequestCaptureField b"text") aosObjectEnd)))))))) def nvidiaRequestDriverTag : Nat = (succ nvidiaRequestCheckpointRestoredTag) -- This edge covers the complete restored-to-published execution window. -- It does not infer intermediate update states or a transition from an -- unobserved fresh-initialization state. def nvidiaRequestContinuationDeclaration = (constructor TelemetryRecordDeclaration TelemetryRecordDeclarationValue b"aos.state.transition@1" b"state" (capturePolicyIdentifier nvidiaRequestCapturePolicy) b"reported" b"persistence owner's committed continuation window" (constructor TelemetryCaptureValue TelemetryMembersNext b"transition" (constructor TelemetryCaptureValue TelemetryReference b"transition" 2) (constructor TelemetryCaptureValue TelemetryMembersNext b"inputs" (constructor TelemetryCaptureValue TelemetryList (constructor TelemetryCaptureValue TelemetryItemsNext (constructor TelemetryCaptureValue TelemetryReference b"state" 0) (constructor TelemetryCaptureValue TelemetryItemsEnd))) (constructor TelemetryCaptureValue TelemetryMembersNext b"outputs" (constructor TelemetryCaptureValue TelemetryList (constructor TelemetryCaptureValue TelemetryItemsNext (constructor TelemetryCaptureValue TelemetryReference b"state" 2) (constructor TelemetryCaptureValue TelemetryItemsEnd))) (constructor TelemetryCaptureValue TelemetryMembersNext b"outcome" (constructor TelemetryCaptureValue TelemetryConstant (constructor AosValue AosText b"accepted")) (constructor TelemetryCaptureValue TelemetryMembersNext b"reason" (constructor TelemetryCaptureValue TelemetryUnavailable b"not_recorded" b"committed-continuation-window") (constructor TelemetryCaptureValue TelemetryMembersNext b"mechanism" (constructor TelemetryCaptureValue TelemetryConstant (constructor AosValue AosText b"restored checkpoint to committed checkpoint; cumulative window, not one learner update")) (constructor TelemetryCaptureValue TelemetryMembersNext b"coordinate" (constructor TelemetryCaptureValue TelemetryMap (constructor TelemetryCaptureValue TelemetryMembersNext b"input_completed_updates" (constructor TelemetryCaptureValue TelemetryUnsigned 4) (constructor TelemetryCaptureValue TelemetryMembersNext b"output_completed_updates" (constructor TelemetryCaptureValue TelemetryUnsigned 5) (constructor TelemetryCaptureValue TelemetryMembersNext b"output_completed_invocations" (constructor TelemetryCaptureValue TelemetryUnsigned 6) (constructor TelemetryCaptureValue TelemetryMembersEnd))))) (constructor TelemetryCaptureValue TelemetryMembersEnd))))))))) def nvidiaRequestContinuationSchema = (telemetryRecordJSON (telemetryRecordSchemaJSON nvidiaRequestContinuationDeclaration b"Committed checkpoint continuation" (constructor JSON JSONObject (aosField b"transition" (nvidiaRequestCaptureField b"ref:transition") (aosField b"inputs" (nvidiaRequestCaptureField b"list:ref:state") (aosField b"outputs" (nvidiaRequestCaptureField b"list:ref:state") (aosField b"outcome" (nvidiaRequestCaptureField b"text") (aosField b"reason" (nvidiaRequestCaptureField b"text") (aosField b"mechanism" (nvidiaRequestCaptureField b"text") (aosField b"coordinate" (nvidiaRequestCaptureField b"map") aosObjectEnd)))))))))) def nvidiaRequestContinuationTag : Nat = (succ nvidiaRequestDriverTag) def nvidiaRequestPersistenceDeclaration = (lambda unrestricted stage : Bytes . (constructor TelemetryRecordDeclaration TelemetryRecordDeclarationValue b"alpha.checkpoint.persistence@1" b"state" (capturePolicyIdentifier nvidiaRequestCapturePolicy) b"reported" b"persistence owner reached checkpoint preparation or writable temporary file" (constructor TelemetryCaptureValue TelemetryMembersNext b"phase" (constructor TelemetryCaptureValue TelemetryUnsigned 0) (constructor TelemetryCaptureValue TelemetryMembersNext b"stage" (constructor TelemetryCaptureValue TelemetryConstant (constructor AosValue AosText stage)) (constructor TelemetryCaptureValue TelemetryMembersEnd))))) def nvidiaRequestPersistenceSchema = (telemetryRecordJSON (telemetryRecordSchemaJSON (nvidiaRequestPersistenceDeclaration b"") b"Native checkpoint write lifecycle" (constructor JSON JSONObject (aosField b"phase" (nvidiaRequestCaptureField b"u64") (aosField b"stage" (nvidiaRequestCaptureField b"text") aosObjectEnd))))) def nvidiaRequestCheckpointPreparingTag : Nat = (succ nvidiaRequestContinuationTag) def nvidiaRequestCheckpointWritingTag : Nat = (succ nvidiaRequestCheckpointPreparingTag) -- Binding hashes the exact admitted prefix from file offset zero, without -- retaining input bytes. The operation owner supplies the extent it hashed; -- neither a filename nor a configured corpus name is a content identity. def nvidiaRequestInputDeclaration = (constructor TelemetryRecordDeclaration TelemetryRecordDeclarationValue b"alpha.execution.input-binding@1" b"event" (capturePolicyIdentifier nvidiaRequestCapturePolicy) b"reported" b"SHA-256 from the native input binding owner" (constructor TelemetryCaptureValue TelemetryMembersNext b"input_sha256" (constructor TelemetryCaptureValue TelemetryBytes 0 checkpointEnvelopeDigestBytes) (constructor TelemetryCaptureValue TelemetryMembersNext b"hashed_prefix_bytes" (constructor TelemetryCaptureValue TelemetryUnsigned 4) (constructor TelemetryCaptureValue TelemetryMembersNext b"basis" (constructor TelemetryCaptureValue TelemetryConstant (constructor AosValue AosText b"input descriptor byte prefix from offset zero")) (constructor TelemetryCaptureValue TelemetryMembersEnd))))) def nvidiaRequestInputSchema = (telemetryRecordJSON (telemetryRecordSchemaJSON nvidiaRequestInputDeclaration b"Bound execution input bytes" (constructor JSON JSONObject (aosField b"input_sha256" (nvidiaRequestCaptureField b"bytes") (aosField b"hashed_prefix_bytes" (nvidiaRequestCaptureField b"u64") (aosField b"basis" (nvidiaRequestCaptureField b"text") aosObjectEnd)))))) def nvidiaRequestInputTag : Nat = (succ nvidiaRequestCheckpointWritingTag) def nvidiaRequestCaptureLastTag : Nat = nvidiaRequestInputTag def nvidiaRequestCheckpointIdentitySites = (lambda unrestricted tail : (family TelemetryPolicySites) . (nvidiaRequestCheckpointSite nvidiaRequestCheckpointManifestInputTag b"00000000000000000000000000000600" b"request-host:manifest-admitted" 8 (nvidiaRequestCheckpointManifestDeclaration b"admitted") (nvidiaRequestCheckpointSite nvidiaRequestCheckpointManifestOutputTag b"00000000000000000000000000000601" b"request-host:manifest-published" 8 (nvidiaRequestCheckpointManifestDeclaration b"published") (nvidiaRequestCheckpointSite nvidiaRequestCheckpointStateTag b"00000000000000000000000000000602" b"request-host:state-declared" 4 nvidiaRequestCheckpointStateDeclaration (nvidiaRequestCheckpointSite nvidiaRequestCheckpointCommittedTag b"00000000000000000000000000000603" b"request-host:checkpoint-committed" 4 (nvidiaRequestCheckpointIdentityDeclaration b"committed") (nvidiaRequestCheckpointSite nvidiaRequestCheckpointRestoredTag b"00000000000000000000000000000604" b"request-host:checkpoint-restored" 4 (nvidiaRequestCheckpointIdentityDeclaration b"restored") tail)))))) def nvidiaRequestCaptureSitesWithCheckpoint = (nvidiaRequestCheckpointSite nvidiaRequestInputTag b"00000000000000000000000000000609" b"request-host:input-bound" 5 nvidiaRequestInputDeclaration (nvidiaRequestCheckpointSite nvidiaRequestCheckpointPreparingTag b"00000000000000000000000000000607" b"request-host:checkpoint-preparing" 1 (nvidiaRequestPersistenceDeclaration b"preparing") (nvidiaRequestCheckpointSite nvidiaRequestCheckpointWritingTag b"00000000000000000000000000000608" b"request-host:checkpoint-writing" 1 (nvidiaRequestPersistenceDeclaration b"writing") (nvidiaRequestCheckpointSite nvidiaRequestContinuationTag b"00000000000000000000000000000606" b"request-host:committed-continuation" 7 nvidiaRequestContinuationDeclaration (nvidiaRequestCheckpointSite nvidiaRequestDriverTag b"00000000000000000000000000000605" b"request-host:driver-context" 8 nvidiaRequestDriverDeclaration (nvidiaRequestCheckpointIdentitySites (nvidiaRequestCheckpointSite nvidiaRequestCheckpointCaptureTag b"00000000000000000000000000000508" b"request-host:published-checkpoint-frontier" 3 nvidiaRequestCheckpointCaptureDeclaration (nvidiaRequestCheckpointSite nvidiaRequestCheckpointInputTag b"00000000000000000000000000000509" b"request-host:checkpoint-input-admission" 1 nvidiaRequestCheckpointInputDeclaration (nvidiaRequestCheckpointSite nvidiaRequestCheckpointAdmittedTag b"0000000000000000000000000000050a" b"request-host:admitted-checkpoint-frontier" 3 nvidiaRequestCheckpointAdmittedDeclaration nvidiaRequestCaptureSites))))))))) -- Read only the declared header words. Neither frontier transports checkpoint -- payload bytes, paths, seed material or input data into the journal. def nvidiaRequestCheckpointFrontierCapture = (lambda unrestricted tag : Nat . (lambda unrestricted header : Nat . (lambda unrestricted phase : Nat . (lambda unrestricted after : (family NativeObservedSteps) . (let unrestricted missing = (constructor NativeTelemetrySourceWord NativeTelemetryWordOmitted) in (constructor NativeObservedSteps NativeObservedCaptureBoundary tag (constructor NativeTelemetrySourceValues NativeTelemetrySourceValuesValue (constructor NativeTelemetrySourceWord NativeTelemetryWordValue (phLoad (naturalAdd header checkpointEnvelopeUpdatesAt))) (constructor NativeTelemetrySourceWord NativeTelemetryWordValue (phLoad (naturalAdd header checkpointEnvelopeInvocationsAt))) (constructor NativeTelemetrySourceWord NativeTelemetryWordValue (phLoad (naturalAdd header checkpointEnvelopeVersionAt))) missing missing missing missing missing) (phImm phase) after)))))) def nvidiaRequestCheckpointIdentityCapture = (lambda unrestricted tag : Nat . (lambda unrestricted digest : Nat . (lambda unrestricted after : (family NativeObservedSteps) . (constructor NativeObservedSteps NativeObservedCaptureBoundary tag (constructor NativeTelemetrySourceValues NativeTelemetrySourceValuesValue (constructor NativeTelemetrySourceWord NativeTelemetryWordValue (phLoad (naturalAdd digest (naturalMultiply 0 nativePhysicalWordBytes)))) (constructor NativeTelemetrySourceWord NativeTelemetryWordValue (phLoad (naturalAdd digest (naturalMultiply 1 nativePhysicalWordBytes)))) (constructor NativeTelemetrySourceWord NativeTelemetryWordValue (phLoad (naturalAdd digest (naturalMultiply 2 nativePhysicalWordBytes)))) (constructor NativeTelemetrySourceWord NativeTelemetryWordValue (phLoad (naturalAdd digest (naturalMultiply 3 nativePhysicalWordBytes)))) (constructor NativeTelemetrySourceWord NativeTelemetryWordOmitted) (constructor NativeTelemetrySourceWord NativeTelemetryWordOmitted) (constructor NativeTelemetrySourceWord NativeTelemetryWordOmitted) (constructor NativeTelemetrySourceWord NativeTelemetryWordOmitted)) (phImm 0) after)))) def nvidiaRequestCheckpointManifestCapture = (lambda unrestricted tag : Nat . (lambda unrestricted digest : Nat . (lambda unrestricted header : Nat . (lambda unrestricted after : (family NativeObservedSteps) . (constructor NativeObservedSteps NativeObservedCaptureBoundary tag (constructor NativeTelemetrySourceValues NativeTelemetrySourceValuesValue (constructor NativeTelemetrySourceWord NativeTelemetryWordValue (phLoad (naturalAdd digest (naturalMultiply 0 nativePhysicalWordBytes)))) (constructor NativeTelemetrySourceWord NativeTelemetryWordValue (phLoad (naturalAdd digest (naturalMultiply 1 nativePhysicalWordBytes)))) (constructor NativeTelemetrySourceWord NativeTelemetryWordValue (phLoad (naturalAdd digest (naturalMultiply 2 nativePhysicalWordBytes)))) (constructor NativeTelemetrySourceWord NativeTelemetryWordValue (phLoad (naturalAdd digest (naturalMultiply 3 nativePhysicalWordBytes)))) (constructor NativeTelemetrySourceWord NativeTelemetryWordValue (phLoad (naturalAdd header checkpointEnvelopeUpdatesAt))) (constructor NativeTelemetrySourceWord NativeTelemetryWordValue (phLoad (naturalAdd header checkpointEnvelopeInvocationsAt))) (constructor NativeTelemetrySourceWord NativeTelemetryWordValue (phLoad (naturalAdd header checkpointEnvelopeHeaderBytesAt))) (constructor NativeTelemetrySourceWord NativeTelemetryWordValue (phLoad (naturalAdd header checkpointEnvelopePayloadBytesAt)))) (phLoad (naturalAdd header checkpointEnvelopeUpdatesAt)) after))))) def nvidiaRequestContinuationCapture = (lambda unrestricted after : (family NativeObservedSteps) . (constructor NativeObservedSteps NativeObservedOperation (constructor NativePhysicalOperation NativePhysicalRepeatBeginCounted (phLoad (naturalAdd prCheckpointHeaderIn checkpointEnvelopeVersionAt))) (constructor NativeObservedSteps NativeObservedCaptureBoundary nvidiaRequestContinuationTag (constructor NativeTelemetrySourceValues NativeTelemetrySourceValuesValue (constructor NativeTelemetrySourceWord NativeTelemetryWordValue (phLoad (naturalAdd prCheckpointInputManifest (naturalMultiply 0 nativePhysicalWordBytes)))) (constructor NativeTelemetrySourceWord NativeTelemetryWordValue (phLoad (naturalAdd prCheckpointInputManifest (naturalMultiply 1 nativePhysicalWordBytes)))) (constructor NativeTelemetrySourceWord NativeTelemetryWordValue (phLoad (naturalAdd prCheckpointOutputManifest (naturalMultiply 0 nativePhysicalWordBytes)))) (constructor NativeTelemetrySourceWord NativeTelemetryWordValue (phLoad (naturalAdd prCheckpointOutputManifest (naturalMultiply 1 nativePhysicalWordBytes)))) (constructor NativeTelemetrySourceWord NativeTelemetryWordValue (phLoad (naturalAdd prCheckpointHeaderIn checkpointEnvelopeUpdatesAt))) (constructor NativeTelemetrySourceWord NativeTelemetryWordValue (phLoad (naturalAdd prCheckpointHeaderOut checkpointEnvelopeUpdatesAt))) (constructor NativeTelemetrySourceWord NativeTelemetryWordValue (phLoad (naturalAdd prCheckpointHeaderOut checkpointEnvelopeInvocationsAt))) (constructor NativeTelemetrySourceWord NativeTelemetryWordOmitted)) (phLoad (naturalAdd prCheckpointHeaderOut checkpointEnvelopeUpdatesAt)) (constructor NativeObservedSteps NativeObservedOperation (constructor NativePhysicalOperation NativePhysicalRepeatEnd) after)))) def nvidiaRequestCheckpointCapture = (lambda unrestricted after : (family NativeObservedSteps) . (nvidiaRequestCheckpointFrontierCapture nvidiaRequestCheckpointCaptureTag prCheckpointHeaderOut prTelemetryPublished (nvidiaRequestCheckpointManifestCapture nvidiaRequestCheckpointManifestOutputTag prCheckpointOutputManifest prCheckpointHeaderOut (nvidiaRequestCheckpointIdentityCapture nvidiaRequestCheckpointStateTag prCheckpointOutputManifest (nvidiaRequestCheckpointIdentityCapture nvidiaRequestCheckpointCommittedTag prCheckpointOutputManifest (nvidiaRequestContinuationCapture after)))))) -- Fresh initialization has no input checkpoint to restore. Only an admitted -- checkpoint can reach this record, after the system's complete load schedule. def nvidiaRequestCheckpointRestoredCapture = (lambda unrestricted after : (family NativeObservedSteps) . (constructor NativeObservedSteps NativeObservedOperation (constructor NativePhysicalOperation NativePhysicalRepeatBeginCounted (phLoad (naturalAdd prCheckpointHeaderIn checkpointEnvelopeVersionAt))) (nvidiaRequestCheckpointIdentityCapture nvidiaRequestCheckpointRestoredTag prCheckpointInputManifest (constructor NativeObservedSteps NativeObservedOperation (constructor NativePhysicalOperation NativePhysicalRepeatEnd) after)))) -- Admission proves the version is either zero (empty input) or one (validated -- layout/identities/chunks). The owner's bounded repeat therefore emits one -- input frontier only for an actual checkpoint. Empty input carries its -- admission decision but has no invented restored counters. This boundary is -- before device upload: it does not claim that GPU restoration has occurred. def nvidiaRequestCheckpointInputCapture = (lambda unrestricted after : (family NativeObservedSteps) . (let unrestricted version = (phLoad (naturalAdd prCheckpointHeaderIn checkpointEnvelopeVersionAt)) in (let unrestricted missing = (constructor NativeTelemetrySourceWord NativeTelemetryWordOmitted) in (constructor NativeObservedSteps NativeObservedCaptureBoundary nvidiaRequestCheckpointInputTag (constructor NativeTelemetrySourceValues NativeTelemetrySourceValuesValue (constructor NativeTelemetrySourceWord NativeTelemetryWordValue version) missing missing missing missing missing missing missing) (phImm prTelemetryChecked) (constructor NativeObservedSteps NativeObservedOperation (constructor NativePhysicalOperation NativePhysicalRepeatBeginCounted version) (nvidiaRequestCheckpointFrontierCapture nvidiaRequestCheckpointAdmittedTag prCheckpointHeaderIn prTelemetryChecked (nvidiaRequestCheckpointManifestCapture nvidiaRequestCheckpointManifestInputTag prCheckpointInputManifest prCheckpointHeaderIn (nvidiaRequestCheckpointIdentityCapture nvidiaRequestCheckpointStateTag prCheckpointInputManifest (constructor NativeObservedSteps NativeObservedOperation (constructor NativePhysicalOperation NativePhysicalRepeatEnd) after))))))))) def nvidiaRequestCapturePlanWithSites = (lambda unrestricted sites : (family TelemetryPolicySites) . (lambda unrestricted metadata : (family StdList Bytes) . (telemetryRoutedPolicyPlan nvidiaRequestCapturePolicy sites (constructor StdList StdListCons Bytes nvidiaRequestCaptureSchema (constructor StdList StdListCons Bytes nvidiaRequestCheckpointCaptureSchema (constructor StdList StdListCons Bytes nvidiaRequestCheckpointInputSchema (constructor StdList StdListCons Bytes nvidiaRequestCheckpointAdmittedSchema (constructor StdList StdListCons Bytes nvidiaRequestCheckpointManifestSchema (constructor StdList StdListCons Bytes nvidiaRequestCheckpointStateSchema (constructor StdList StdListCons Bytes nvidiaRequestCheckpointIdentitySchema (constructor StdList StdListCons Bytes nvidiaRequestDriverSchema (constructor StdList StdListCons Bytes nvidiaRequestContinuationSchema (constructor StdList StdListCons Bytes nvidiaRequestPersistenceSchema (constructor StdList StdListCons Bytes nvidiaRequestInputSchema metadata)))))))))))))) def nvidiaRequestCapturePlan = (nvidiaRequestCapturePlanWithSites nvidiaRequestCaptureSitesWithCheckpoint) def nvidiaRequestCaptureName = (lambda unrestricted phase : Nat . (eliminate TelemetryPolicySites (lambda unrestricted current : (family TelemetryPolicySites) . Bytes) (telemetryPolicySiteLookup (succ phase) nvidiaRequestCaptureSites) (branch TelemetryPolicySitesEnd . b"") (branch TelemetryPolicySitesNext tag site record tail induction . (captureSiteName site)))) def nvidiaRequestCaptureBoundary = (lambda unrestricted phase : Nat . (lambda unrestricted name : Bytes . (lambda unrestricted after : (family NativeObservedSteps) . (let unrestricted missing = (constructor NativeTelemetrySourceWord NativeTelemetryWordOmitted) in (constructor NativeObservedSteps NativeObservedCaptureBoundary (aosChoose Nat (naturalAnd (naturalLessOrEqual phase prTelemetryDone) (bytes-equal (nvidiaRequestCaptureName phase) name)) (succ phase) 0) (constructor NativeTelemetrySourceValues NativeTelemetrySourceValuesValue (constructor NativeTelemetrySourceWord NativeTelemetryWordValue (phImm phase)) missing missing missing missing missing missing missing) (phImm phase) after))))) def nvidiaRequestDriverCapture = (lambda unrestricted after : (family NativeObservedSteps) . (constructor NativeObservedSteps NativeObservedCaptureBoundary nvidiaRequestDriverTag (constructor NativeTelemetrySourceValues NativeTelemetrySourceValuesValue (constructor NativeTelemetrySourceWord NativeTelemetryWordValue (phLoad (naturalAdd phDriverVersionAt (naturalMultiply 0 nativePhysicalWordBytes)))) (constructor NativeTelemetrySourceWord NativeTelemetryWordValue (phLoad (naturalAdd phDriverVersionAt (naturalMultiply 1 nativePhysicalWordBytes)))) (constructor NativeTelemetrySourceWord NativeTelemetryWordValue (phLoad (naturalAdd phDriverVersionAt (naturalMultiply 2 nativePhysicalWordBytes)))) (constructor NativeTelemetrySourceWord NativeTelemetryWordValue (phLoad (naturalAdd phDriverVersionAt (naturalMultiply 3 nativePhysicalWordBytes)))) (constructor NativeTelemetrySourceWord NativeTelemetryWordValue (phLoad (naturalAdd phDriverVersionAt (naturalMultiply 4 nativePhysicalWordBytes)))) (constructor NativeTelemetrySourceWord NativeTelemetryWordValue (phLoad (naturalAdd phDriverVersionAt (naturalMultiply 5 nativePhysicalWordBytes)))) (constructor NativeTelemetrySourceWord NativeTelemetryWordValue (phLoad (naturalAdd phDriverVersionAt (naturalMultiply 6 nativePhysicalWordBytes)))) (constructor NativeTelemetrySourceWord NativeTelemetryWordValue (phLoad (naturalAdd phDriverVersionAt (naturalMultiply 7 nativePhysicalWordBytes))))) (phImm prTelemetryChannel) after)) def nvidiaRequestCaptureBoundaryWithCheckpointPhases = (lambda unrestricted phase : Nat . (lambda unrestricted name : Bytes . (lambda unrestricted after : (family NativeObservedSteps) . (nvidiaRequestCaptureBoundary phase name (aosChoose (family NativeObservedSteps) (naturalEqual phase prTelemetryPublished) (nvidiaRequestCheckpointCapture after) (aosChoose (family NativeObservedSteps) (naturalEqual phase prTelemetryChecked) (nvidiaRequestCheckpointInputCapture after) (aosChoose (family NativeObservedSteps) (naturalEqual phase prTelemetryChannel) (nvidiaRequestDriverCapture after) after))))))) def nvidiaRequestPersistenceCapture = (lambda unrestricted tag : Nat . (lambda unrestricted phase : Nat . (lambda unrestricted after : (family NativeObservedSteps) . (let unrestricted missing = (constructor NativeTelemetrySourceWord NativeTelemetryWordOmitted) in (constructor NativeObservedSteps NativeObservedCaptureBoundary tag (constructor NativeTelemetrySourceValues NativeTelemetrySourceValuesValue (constructor NativeTelemetrySourceWord NativeTelemetryWordValue (phImm phase)) missing missing missing missing missing missing missing) (phImm phase) after))))) def nvidiaRequestCaptureBoundaryWithPersistence = (lambda unrestricted phase : Nat . (lambda unrestricted name : Bytes . (lambda unrestricted after : (family NativeObservedSteps) . (aosChoose (family NativeObservedSteps) (naturalAnd (naturalEqual phase prTelemetryStateRestored) (bytes-equal name b"request-host:checkpoint-restored")) (nvidiaRequestCheckpointRestoredCapture after) (aosChoose (family NativeObservedSteps) (naturalAnd (naturalEqual phase prTelemetryCheckpointPreparing) (bytes-equal name b"request-host:checkpoint-preparing")) (nvidiaRequestPersistenceCapture nvidiaRequestCheckpointPreparingTag phase after) (aosChoose (family NativeObservedSteps) (naturalAnd (naturalEqual phase prTelemetryCheckpointWriting) (bytes-equal name b"request-host:checkpoint-writing")) (nvidiaRequestPersistenceCapture nvidiaRequestCheckpointWritingTag phase after) (nvidiaRequestCaptureBoundaryWithCheckpointPhases phase name after))))))) def nvidiaRequestInputCapture = (lambda unrestricted after : (family NativeObservedSteps) . (let unrestricted missing = (constructor NativeTelemetrySourceWord NativeTelemetryWordOmitted) in (constructor NativeObservedSteps NativeObservedCaptureBoundary nvidiaRequestInputTag (constructor NativeTelemetrySourceValues NativeTelemetrySourceValuesValue (constructor NativeTelemetrySourceWord NativeTelemetryWordValue (phLoad (naturalAdd prInputIdentity (naturalMultiply 0 nativePhysicalWordBytes)))) (constructor NativeTelemetrySourceWord NativeTelemetryWordValue (phLoad (naturalAdd prInputIdentity (naturalMultiply 1 nativePhysicalWordBytes)))) (constructor NativeTelemetrySourceWord NativeTelemetryWordValue (phLoad (naturalAdd prInputIdentity (naturalMultiply 2 nativePhysicalWordBytes)))) (constructor NativeTelemetrySourceWord NativeTelemetryWordValue (phLoad (naturalAdd prInputIdentity (naturalMultiply 3 nativePhysicalWordBytes)))) (constructor NativeTelemetrySourceWord NativeTelemetryWordValue (phLoad prInputIdentityExtent)) missing missing missing) (phImm prTelemetryInputBound) after))) def nvidiaRequestCaptureBoundaryWithCheckpoint = (lambda unrestricted phase : Nat . (lambda unrestricted name : Bytes . (lambda unrestricted after : (family NativeObservedSteps) . (aosChoose (family NativeObservedSteps) (naturalAnd (naturalEqual phase prTelemetryInputBound) (bytes-equal name b"request-host:input-bound")) (nvidiaRequestInputCapture after) (nvidiaRequestCaptureBoundaryWithPersistence phase name after))))) -- The application owns the filename/stat buffer and descriptors, while the -- recorder owns identity bytes and journal construction. All extents/slots are -- derived after the maintained request host's original declarations. def nvidiaRequestCaptureScalarAt : Nat = phStateExtent def nvidiaRequestCapturePathAt : Nat = (naturalAdd nvidiaRequestCaptureScalarAt nativePhysicalWordBytes) def nvidiaRequestCaptureBytes : Nat = (naturalAdd nvidiaRequestCapturePathAt nativeObservedJournalBytes) def nvidiaRequestCaptureFileSlot : Nat = phSlots def nvidiaRequestCaptureDirectorySlot : Nat = (succ nvidiaRequestCaptureFileSlot) def nvidiaRequestCaptureWorkSlot : Nat = (succ nvidiaRequestCaptureDirectorySlot) def nvidiaRequestCaptureSlots : Nat = (succ nvidiaRequestCaptureWorkSlot) -- Read one exact binary32 cell at a declared safe host boundary. Public -- scratch is disjoint from application buffers and recorder-private state. -- A second word carries the caller's declared coordinate. Neither word is -- interpreted as a learning quantity by this transport mechanism. def nvidiaRequestCaptureMappedF32 = (lambda unrestricted tag : Nat . (lambda unrestricted address : Nat . (lambda unrestricted coordinate : (family NativePhysicalOperand) . (lambda unrestricted after : (family NativeObservedSteps) . (nativeObservedPrefixWith (phCopy nvidiaRequestCaptureScalarAt (phZeros nativePhysicalWordBytes)) (nativeObservedPrefixWith (phCopyMappedToState address nvidiaRequestCaptureScalarAt (bytes-length (dataBytesWord32LE (modelWord32FromNaturalTruncated 0)))) (let unrestricted missing = (constructor NativeTelemetrySourceWord NativeTelemetryWordOmitted) in (constructor NativeObservedSteps NativeObservedCaptureBoundary tag (constructor NativeTelemetrySourceValues NativeTelemetrySourceValuesValue (constructor NativeTelemetrySourceWord NativeTelemetryWordValue (phLoad nvidiaRequestCaptureScalarAt)) (constructor NativeTelemetrySourceWord NativeTelemetryWordValue coordinate) missing missing missing missing missing missing) coordinate after)))))))) def nvidiaRequestCaptureCleanup = (nativeObservedPrefixWith (nativeObservedJournalClose nvidiaRequestCaptureFileSlot nvidiaRequestCaptureWorkSlot b"telemetry:journal-close") (nativeObservedPrefixWith (nativeObservedJournalClose nvidiaRequestCaptureDirectorySlot nvidiaRequestCaptureWorkSlot b"telemetry:journal-directory-close") (constructor NativeObservedSteps NativeObservedStepsEnd))) def nvidiaPlanHostManagedRequestStepsWithBoundary = (lambda unrestricted boundary : (pi unrestricted phase : Nat . (pi unrestricted name : Bytes . (pi unrestricted rest : (family NativeObservedSteps) . (family NativeObservedSteps)))) . (nvidiaPlanHostRequestWith (family NativeObservedSteps) nativeObservedPrefixWith (lambda unrestricted after : (family NativeObservedSteps) . (constructor NativeObservedSteps NativeObservedOpenJournal nvidiaRequestCapturePathAt nvidiaRequestCaptureFileSlot nvidiaRequestCaptureDirectorySlot (nativeObservedPrefixWith phTelemetryOpen after))) boundary (constructor NativeObservedSteps NativeObservedFinish nvidiaRequestCaptureCleanup))) def nvidiaPlanHostManagedRequestSteps = (nvidiaPlanHostManagedRequestStepsWithBoundary nvidiaRequestCaptureBoundaryWithCheckpoint) -- Assignment is a declared input capability. The same source schedule and -- capture layout serve both fresh and caller-assigned run membership; the -- recorder still acquires its own producer epoch before opening its journal. -- The request ABI occupies argv[1]. Assigned request artifacts add one -- declared file input at argv[2], rather than interpreting environment state. def nvidiaRequestAssignedIdentitySource : (family NativeTelemetryIdentitySource) = (constructor NativeTelemetryIdentitySource NativeTelemetryAssignedFile (constructor NativePhysicalOperand NativePhysicalProcessArgument (phWord 2))) def nvidiaPlanHostManagedRequestProgramWithBoundary = (lambda unrestricted boundary : (pi unrestricted phase : Nat . (pi unrestricted name : Bytes . (pi unrestricted rest : (family NativeObservedSteps) . (family NativeObservedSteps)))) . (lambda unrestricted source : (family NativeTelemetryIdentitySource) . (lambda unrestricted capturePlan : (family TelemetryRoutedPolicyPlan) . (lambda unrestricted layout : (family NvidiaPlanHostLayout) . (lambda unrestricted hostIdentity : Bytes . (lambda unrestricted programIdentity : Bytes . (lambda unrestricted qmdIdentity : Bytes . (lambda unrestricted pushIdentity : Bytes . (lambda unrestricted gpfifoIdentity : Bytes . (lambda unrestricted programLength : Nat . (lambda unrestricted qmdLength : Nat . (lambda unrestricted pushLength : Nat . (lambda unrestricted gpfifoLength : Nat . (lambda unrestricted submissionCount : Nat . (lambda unrestricted input : (family NvidiaPlanHostInputContract) . (lambda unrestricted contract : (family CheckpointEnvelopeContract) . (lambda unrestricted fills : (family NvidiaPlanHostRecipeFills) . (lambda unrestricted learner : (pi unrestricted after : (family NativePhysicalCommands) . (family NativePhysicalCommands)) . (lambda unrestricted steps : (family NvidiaPlanHostSteps) . (nativeObservedRequireProgram (nativeObservedBuildProgramWithIdentitySource source nvidiaRequestCaptureBytes nvidiaRequestCaptureSlots capturePlan (phSlot nvidiaRequestCaptureFileSlot) (phSlot nvidiaRequestCaptureDirectorySlot) hostIdentity (nvidiaPlanHostManagedRequestStepsWithBoundary boundary layout hostIdentity programIdentity qmdIdentity pushIdentity gpfifoIdentity programLength qmdLength pushLength gpfifoLength submissionCount input contract fills learner steps)))))))))))))))))))))) def nvidiaPlanHostManagedRequestProgramWithIdentitySource = (nvidiaPlanHostManagedRequestProgramWithBoundary nvidiaRequestCaptureBoundaryWithCheckpoint) def nvidiaPlanHostManagedRequestProgram = (nvidiaPlanHostManagedRequestProgramWithIdentitySource (constructor NativeTelemetryIdentitySource NativeTelemetryFreshIdentity))