21def nativeTelemetryIdentitySourceAdmission =
22 (lambda unrestricted applicationBytes : Nat .
23 (lambda unrestricted applicationSlots : Nat .
24 (lambda unrestricted source : (family NativeTelemetryIdentitySource) .
25 (eliminate
26 NativeTelemetryIdentitySource
27 (lambda unrestricted current : (family NativeTelemetryIdentitySource) . Nat)
28 source
29 (branch NativeTelemetryFreshIdentity . 1)
30 (branch NativeTelemetryAssignedFile path .
31 -- Initialization precedes application steps. Only an incoming argv
32 -- path exists at this point; application state/results are future
33 -- values and may not be read as an already-initialized pathname.
34 (eliminate
35 NativePhysicalOperand
36 (lambda unrestricted current : (family NativePhysicalOperand) . Nat)
37 path
38 (branch NativePhysicalImmediate value . 0)
39 (branch NativePhysicalResultValue slot . 0)
40 (branch NativePhysicalResultAddress slot offset . 0)
41 (branch NativePhysicalStateAddress offset . 0)
42 (branch NativePhysicalStateLoad64 offset . 0)
43 (branch NativePhysicalPayloadAddress offset . 0)
44 (branch NativePhysicalPayloadLoad64 offset . 0)
45 (branch NativePhysicalProcessArgument index . 1)
46 (branch NativePhysicalLoopAffine base stride . 0)))))))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.