Platform.Linux.Nvidia.ObservedRequest

1module Platform.Linux.Nvidia.ObservedRequest
2
3import Data.Bytes
4import Platform.Linux.Nvidia.PlanHost
5import Platform.Linux.Nvidia.PlanHostRequest
6import Std.Natural
7import Runtime.NativeObservedProgram
8
9-- Use the maintained request-step interpreter with source-declared effects.
10-- A boundary is reached only after the owning protocol has returned; recorder
11-- lowering owns required capture, drain/retry, storage and target bindings.
12-- Keeping this adapter beside the interpreter avoids making every unobserved
13-- host import the capture implementation merely to lower its ordinary steps.
14def nvidiaPlanHostObservedSteps =
15  (nvidiaPlanHostStepsWith (family NativeObservedSteps) nativeObservedPrefixWith)
16
17-- Complete request lifecycle, using the same envelope, request, channel,
18-- staging, learner and schedule owners as the physical instance. Embedded
19-- legacy command fragments may still emit v1 phase records: retain their
20-- recorder mapping until those declarations migrate to typed source effects.
21-- Top-level boundaries are supplied by the caller's declared capture policy.
22-- End closes the producer before cleanup; a failed earlier command never
23-- reaches this completion path and cannot fabricate a terminal acknowledgement.
24def nvidiaPlanHostObservedRequestSteps =
25  (lambda unrestricted boundary : (pi unrestricted phase : Nat . (pi unrestricted name : Bytes . (pi unrestricted after : (family NativeObservedSteps) . (family NativeObservedSteps)))) .
26    (lambda unrestricted cleanup : (family NativeObservedSteps) .
27      (nvidiaPlanHostRequestWith
28        (family NativeObservedSteps)
29        nativeObservedPrefixWith
30        (nativeObservedPrefixWith phTelemetryOpen)
31        boundary
32        (constructor NativeObservedSteps NativeObservedFinish cleanup))))