1module Runtime.NativeObservedJournal
2
3import Data.Bytes
4import Model.Word64
5import Observe.Value
6import Runtime.NativeFileStatus
7import Runtime.NativeLaunchRecipeLoad
8import Runtime.NativePhysicalProgram
9import Runtime.NativeTelemetryPolicy
10import Runtime.NativeTelemetryValue
11import Runtime.TelemetryCapture
12import Runtime.TelemetryDrain
13import Runtime.TelemetryIdentity
14import Runtime.TelemetryPolicy
15import Runtime.TelemetryValue
16import Std.Natural
17
18-- One journal per actual producer epoch. Rendering reads the recorder-owned
19-- identity only after initialization; application source never receives access
20-- to that private arena. Exclusive creation prevents overwriting another run.
21-- The quoted hex formatter supplies the digits; openat skips the opening quote
22-- and a constant suffix replaces the closing quote. No second entropy draw or
23-- PID/time-derived identity is introduced merely to choose a filename.
24def nativeObservedJournalSuffix : Bytes =
25 b".alphatel\x00"
26
27def nativeObservedJournalNameBytes : Nat =
28 (naturalAdd
29 (naturalSaturatingSubtract (telemetryHexCellBytes telemetryIdentityBytes) 1)
30 (bytes-length nativeObservedJournalSuffix))
31
32-- fstat's result is not interpreted. This is the conservative Linux scratch
33-- extent already used by both maintained host ABIs; it is kept disjoint from
34-- the filename and recorder storage even when an open fails.
35def nativeObservedJournalStatBytes : Nat =
36 nativeFileStatusScratchBytes
37
38def nativeObservedJournalStatAt =
39 (lambda unrestricted pathAt : Nat . (naturalAdd pathAt nativeObservedJournalNameBytes))
40
41def nativeObservedJournalBytes : Nat =
42 (naturalAdd nativeObservedJournalNameBytes nativeObservedJournalStatBytes)
43
44def nativeObservedJournalAdmission =
45 (lambda unrestricted applicationBytes : Nat .
46 (lambda unrestricted applicationSlots : Nat .
47 (lambda unrestricted pathAt : Nat .
48 (lambda unrestricted fileSlot : Nat .
49 (lambda unrestricted directorySlot : Nat .
50 (naturalAnd
51 (telemetryRangeFits pathAt nativeObservedJournalBytes applicationBytes)
52 (naturalAnd
53 (naturalLess fileSlot applicationSlots)
54 (naturalAnd
55 (naturalLess directorySlot applicationSlots)
56 (naturalIsZero (naturalEqual fileSlot directorySlot))))))))))
57
58def nativeObservedJournalCall =
59 (lambda unrestricted syscall : Nat .
60 (lambda unrestricted arguments : (family NativePhysicalArguments) .
61 (lambda unrestricted payload : Bytes .
62 (lambda unrestricted resultSlot : Nat .
63 (lambda unrestricted error : Bytes .
64 (nativeLaunchRecipeCommand
65 (constructor
66 NativePhysicalOperation
67 NativePhysicalSystemCall
68 (nativeLaunchRecipeImmediate syscall)
69 arguments
70 payload
71 (nativeLaunchRecipeStore resultSlot))
72 error))))))
73
74def nativeObservedJournalCheckDescriptor =
75 (lambda unrestricted descriptorSlot : Nat .
76 (lambda unrestricted pathAt : Nat .
77 (lambda unrestricted workSlot : Nat .
78 (lambda unrestricted error : Bytes .
79 (lambda unrestricted tail : (family NativePhysicalCommands) .
80 (nativeObservedJournalCall
81 5
82 (nativeLaunchRecipeArguments
83 (nativeLaunchRecipeSlotValue descriptorSlot)
84 (nativeTelemetryPolicyState (nativeObservedJournalStatAt pathAt))
85 (nativeLaunchRecipeImmediate 0)
86 (nativeLaunchRecipeImmediate 0))
87 b""
88 workSlot
89 error
90 (nativeLaunchRecipeAssertEqual
91 (nativeLaunchRecipeSlotValue workSlot)
92 (nativeLaunchRecipeImmediate 0)
93 error
94 tail)))))))
95
96def nativeObservedJournalForCapacities =
97 (lambda unrestricted applicationBytes : Nat .
98 (lambda unrestricted ordinary : Nat .
99 (lambda unrestricted reserved : Nat .
100 (lambda unrestricted pathAt : Nat .
101 (lambda unrestricted fileSlot : Nat .
102 (lambda unrestricted directorySlot : Nat .
103 (lambda unrestricted workSlot : Nat .
104 (lambda unrestricted identity : Bytes .
105 (lambda unrestricted tail : (family NativePhysicalCommands) .
106 (nativeLaunchRecipeCommand
107 (constructor
108 NativePhysicalOperation
109 NativePhysicalMachineRoutine
110 (nativeTelemetryHexCellRoutine telemetryIdentityBytes 0)
111 (nativeLaunchRecipeArguments
112 (nativeTelemetryPolicyState
113 (naturalAdd
114 (captureIdentityAt applicationBytes ordinary reserved)
115 (telemetryIdentityOffset telemetryProducerEpochIndex)))
116 (nativeTelemetryPolicyState pathAt)
117 (nativeLaunchRecipeImmediate telemetryIdentityBytes)
118 (nativeLaunchRecipeImmediate
119 (telemetryHexCellBytes telemetryIdentityBytes)))
120 (nativeLaunchRecipeStore workSlot))
121 identity
122 (nativeLaunchRecipeAssertEqual
123 (nativeLaunchRecipeSlotValue workSlot)
124 (nativeLaunchRecipeImmediate 0)
125 b"telemetry:journal-name-refused"
126 (nativeLaunchRecipeCommand
127 (constructor
128 NativePhysicalOperation
129 NativePhysicalCopyPayloadToState
130 (modelWord64FromNaturalTruncated
131 (naturalAdd
132 pathAt
133 (naturalSaturatingSubtract
134 (telemetryHexCellBytes telemetryIdentityBytes)
135 1)))
136 (modelWord64FromNaturalTruncated
137 (bytes-length nativeObservedJournalSuffix))
138 nativeObservedJournalSuffix)
139 identity
140 (nativeObservedJournalCall
141 257
142 (nativeLaunchRecipeArguments
143 (nativeLaunchRecipeImmediate 18446744073709551516)
144 (constructor
145 NativePhysicalOperand
146 NativePhysicalPayloadAddress
147 modelWord64Zero)
148 (nativeLaunchRecipeImmediate 65536)
149 (nativeLaunchRecipeImmediate 0))
150 b".\x00"
151 directorySlot
152 identity
153 (nativeObservedJournalCheckDescriptor
154 directorySlot
155 pathAt
156 workSlot
157 b"telemetry:journal-directory-open"
158 (nativeObservedJournalCall
159 257
160 (nativeLaunchRecipeArguments
161 (nativeLaunchRecipeSlotValue directorySlot)
162 (nativeTelemetryPolicyState (succ pathAt))
163 (nativeLaunchRecipeImmediate 1217)
164 (nativeLaunchRecipeImmediate 384))
165 b""
166 fileSlot
167 identity
168 (nativeObservedJournalCheckDescriptor
169 fileSlot
170 pathAt
171 workSlot
172 b"telemetry:journal-open"
173 tail))))))))))))))))
174
175def nativeObservedJournalCommands =
176 (lambda unrestricted applicationBytes : Nat .
177 (lambda unrestricted plan : (family TelemetryRoutedPolicyPlan) .
178 (lambda unrestricted pathAt : Nat .
179 (lambda unrestricted fileSlot : Nat .
180 (lambda unrestricted directorySlot : Nat .
181 (lambda unrestricted workSlot : Nat .
182 (lambda unrestricted identity : Bytes .
183 (lambda unrestricted tail : (family NativePhysicalCommands) .
184 (eliminate
185 TelemetryRoutedPolicyPlan
186 (lambda unrestricted current : (family TelemetryRoutedPolicyPlan) .
187 (family NativePhysicalCommands))
188 plan
189 (branch
190 TelemetryRoutedPolicyReady
191 policy
192 sites
193 drain
194 .
195 (eliminate
196 TelemetryDispatchPlan
197 (lambda unrestricted current : (family TelemetryDispatchPlan) .
198 (family NativePhysicalCommands))
199 drain
200 (branch
201 TelemetryDispatchReady
202 ordinary
203 reserved
204 ordinaryRoutes
205 reservedRoutes
206 ordinaryPlan
207 reservedPlan
208 descriptors
209 bound
210 .
211 (nativeObservedJournalForCapacities
212 applicationBytes
213 ordinary
214 reserved
215 pathAt
216 fileSlot
217 directorySlot
218 workSlot
219 identity
220 tail))
221 (branch
222 TelemetryDispatchRefused
223 reason
224 .
225 (constructor NativePhysicalCommands NativePhysicalCommandsEnd))))
226 (branch
227 TelemetryRoutedPolicyRefused
228 reason
229 .
230 (constructor NativePhysicalCommands NativePhysicalCommandsEnd)))))))))))
231
232-- The caller supplies a public scratch result slot for cleanup; private
233-- recorder work slots are never exposed as application capabilities.
234def nativeObservedJournalClose =
235 (lambda unrestricted descriptorSlot : Nat .
236 (lambda unrestricted workSlot : Nat .
237 (lambda unrestricted error : Bytes .
238 (lambda unrestricted tail : (family NativePhysicalCommands) .
239 (nativeObservedJournalCall
240 3
241 (nativeLaunchRecipeArguments
242 (nativeLaunchRecipeSlotValue descriptorSlot)
243 (nativeLaunchRecipeImmediate 0)
244 (nativeLaunchRecipeImmediate 0)
245 (nativeLaunchRecipeImmediate 0))
246 b""
247 workSlot
248 error
249 (nativeLaunchRecipeAssertEqual
250 (nativeLaunchRecipeSlotValue workSlot)
251 (nativeLaunchRecipeImmediate 0)
252 error
253 tail))))))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.