Platform.Linux.Nvidia.ProgramReadback

1module Platform.Linux.Nvidia.ProgramReadback
2
3import Platform.Linux.Nvidia.PlanHost
4import Platform.Linux.Nvidia.PlanHostRequest
5import Runtime.NativePhysicalEmbeddedArtifact
6import Runtime.NativeFilePlan
7import Runtime.NativePhysicalProgram
8import Model.Word64
9import Model.Parameter
10import Data.Bytes
11import Std.Natural
12
13-- A bounded, versioned capture of one retired native program session. The
14-- payload's interpretation belongs to the system; this owner records its byte
15-- extent, contiguous semaphore slots and fresh-channel issue count. No clock
16-- subtraction occurs here. Reads happen only after the caller's final fence.
17-- v1: magic[8], version:u64, dataBytes:u64, semaphoreCount:u64, payload,
18-- semaphoreCount * prSemaphoreStride bytes, then issueCount:u64; little-endian.
19def nvidiaProgramReadbackMagic : Bytes =
20  b"ALPHAPRD"
21
22def nvidiaProgramReadbackVersion : Nat =
23  1
24
25def nvidiaProgramReadbackHeader =
26  (lambda unrestricted dataBytes : Nat .
27    (lambda unrestricted semaphores : Nat .
28      (bytes-append
29        nvidiaProgramReadbackMagic
30        (bytes-append
31          (dataBytesWord64LE (modelWord64FromNaturalTruncated nvidiaProgramReadbackVersion))
32          (bytes-append
33            (dataBytesWord64LE (modelWord64FromNaturalTruncated dataBytes))
34            (dataBytesWord64LE (modelWord64FromNaturalTruncated semaphores)))))))
35
36def nvidiaProgramReadbackHeaderBytes : Nat =
37  (bytes-length (nvidiaProgramReadbackHeader 0 0))
38
39-- Envelope identity validation has retired before device execution begins.
40-- Reuse that full identity buffer, not prExpected's single-word allocation.
41def nvidiaProgramReadbackHeaderFits :
42  (equal
43    Nat
44    (naturalLessOrEqual nvidiaProgramReadbackHeaderBytes nativePhysicalEmbeddedIdentityLength)
45    1) =
46  (refl Nat 1)
47
48def nvidiaProgramReadback =
49  (lambda unrestricted path : (family NativePhysicalOperand) .
50    (lambda unrestricted semaphoreHost : Nat .
51      (lambda unrestricted dataHost : Nat .
52        (lambda unrestricted dataBytes : Nat .
53          (lambda unrestricted semaphores : Nat .
54            (lambda unrestricted counter : Nat .
55              (lambda unrestricted tail : (family NativePhysicalCommands) .
56                (let unrestricted semBytes =
57                  (naturalMultiply semaphores prSemaphoreStride)
58                  in
59                  (let unrestricted semOffset =
60                    (naturalAdd nvidiaProgramReadbackHeaderBytes dataBytes)
61                    in
62                    (let unrestricted counterOffset =
63                      (naturalAdd semOffset semBytes)
64                      in
65                      (phCopy
66                        prIdentityScratch
67                        (nvidiaProgramReadbackHeader dataBytes semaphores)
68                        (nativeFileOpen
69                          path
70                          nativeFileCandidateFlags
71                          prSlotResult
72                          prSlotStatus
73                          b"program-readback-open"
74                          (nativeFileWrite
75                            (phSlot prSlotResult)
76                            (phState prIdentityScratch)
77                            nvidiaProgramReadbackHeaderBytes
78                            (phImm 0)
79                            prSlotStatus
80                            b"program-readback-header"
81                            (nativeFileWrite
82                              (phSlot prSlotResult)
83                              (phImm dataHost)
84                              dataBytes
85                              (phImm nvidiaProgramReadbackHeaderBytes)
86                              prSlotStatus
87                              b"program-readback-data"
88                              (nativeFileWrite
89                                (phSlot prSlotResult)
90                                (phImm semaphoreHost)
91                                semBytes
92                                (phImm semOffset)
93                                prSlotStatus
94                                b"program-readback-fences"
95                                (nativeFileWrite
96                                  (phSlot prSlotResult)
97                                  (phState counter)
98                                  (bytes-length
99                                    (dataBytesWord64LE (modelWord64FromNaturalTruncated 0)))
100                                  (phImm counterOffset)
101                                  prSlotStatus
102                                  b"program-readback-issues"
103                                  (nativeFileClose
104                                    (phSlot prSlotResult)
105                                    prSlotStatus
106                                    b"program-readback-close"
107                                    tail)))))))))))))))))