Macro operands may not read outputs this operation overwrites, its
values/decision scratch, or command-relative payloads that would move to a
different generated command. Caller-relative affine values are materialized
from a saved caller iteration instead of a conditional block's iteration.
Interval tests subtract from the admitted arena boundaries, never add to an
arbitrary input offset. Even an excluded out-of-range u64 operand must not
overflow while checking scratch aliasing. The VM owns actual address bounds.
255def nativeTelemetrySourceScopeAdmission =
256 (lambda unrestricted applicationBytes : Nat .
257 (lambda unrestricted ordinaryCapacity : Nat .
258 (lambda unrestricted reservedCapacity : Nat .
259 (lambda unrestricted decisionAt : Nat .
260 (lambda unrestricted resultSlot : Nat .
261 (lambda unrestricted workSlot : Nat .
262 (lambda unrestricted operand : (family NativePhysicalOperand) .
263 (eliminate
264 NativePhysicalOperand
265 (lambda unrestricted current : (family NativePhysicalOperand) . Nat)
266 operand
267 (branch NativePhysicalImmediate value . 1)
268 (branch
269 NativePhysicalResultValue
270 slot
271 .
272 (eliminate
273 NativePhysicalSlot
274 (lambda unrestricted current : (family NativePhysicalSlot) . Nat)
275 slot
276 (branch
277 NativePhysicalSlotValue
278 index
279 .
280 (naturalAnd
281 (naturalIsZero (naturalEqual (modelWord64Natural index) resultSlot))
282 (naturalIsZero (naturalEqual (modelWord64Natural index) workSlot))))))
283 (branch NativePhysicalResultAddress slot offset . 1)
284 (branch NativePhysicalStateAddress offset . 1)
285 (branch
286 NativePhysicalStateLoad64
287 offset
288 .
289 (naturalAnd
290 (naturalOr
291 (naturalAnd
292 (naturalLessOrEqual
293 captureWordBytes
294 (captureValuesScratchAt
295 applicationBytes
296 ordinaryCapacity
297 reservedCapacity))
298 (naturalLessOrEqual
299 (modelWord64Natural offset)
300 (naturalSaturatingSubtract
301 (captureValuesScratchAt
302 applicationBytes
303 ordinaryCapacity
304 reservedCapacity)
305 captureWordBytes)))
306 (naturalLessOrEqual
307 (naturalAdd
308 (captureValuesScratchAt
309 applicationBytes
310 ordinaryCapacity
311 reservedCapacity)
312 captureValuesBytes)
313 (modelWord64Natural offset)))
314 (naturalOr
315 (naturalAnd
316 (naturalLessOrEqual captureWordBytes decisionAt)
317 (naturalLessOrEqual
318 (modelWord64Natural offset)
319 (naturalSaturatingSubtract decisionAt captureWordBytes)))
320 (naturalLessOrEqual
321 (naturalAdd decisionAt (naturalMultiply 2 captureWordBytes))
322 (modelWord64Natural offset)))))
323 (branch NativePhysicalPayloadAddress offset . 0)
324 (branch NativePhysicalPayloadLoad64 offset . 0)
325 (branch NativePhysicalProcessArgument index . 1)
326 (branch NativePhysicalLoopAffine base stride . 1)))))))))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.