Runtime.TelemetryIdentity

1module Runtime.TelemetryIdentity
2
3import Observe.Value
4import Runtime.ArenaCertificate
5import Runtime.TelemetryCapture
6import Std.Natural
7
8-- AOS-ID-003 fixes a 128-bit, nonzero identity (32 lowercase hex digits on
9-- interchange). Native memory retains its sixteen binary bytes, not text.
10-- Run/attempt/producer may be assigned by an admitted execution coordinator;
11-- only producer_epoch is renewed at every process start. Uploads mint none.
12def telemetryIdentityBytes : Nat =
13  (naturalDivideUnchecked 32 2)
14
15def telemetryRunIdentityIndex : Nat =
16  0
17
18def telemetryAttemptIdentityIndex : Nat =
19  (succ telemetryRunIdentityIndex)
20
21def telemetryProducerIdentityIndex : Nat =
22  (succ telemetryAttemptIdentityIndex)
23
24def telemetryProducerEpochIndex : Nat =
25  (succ telemetryProducerIdentityIndex)
26
27def telemetryIdentityOffset =
28  (lambda unrestricted index : Nat . (naturalMultiply index telemetryIdentityBytes))
29
30def telemetryIdentitySetBytes : Nat =
31  (telemetryIdentityOffset (succ telemetryProducerEpochIndex))
32
33def telemetryIdentityBindingBytes : Nat =
34  (telemetryIdentityOffset telemetryProducerEpochIndex)
35
36-- The supplied transport contains exactly the three assigned binary roles.
37-- A short read or any trailing byte refuses binding before epoch entropy is
38-- acquired. This proves framing, not the caller's coordinator authority.
39def telemetryAssignedBindingAdmission =
40  (lambda unrestricted received : Nat .
41    (lambda unrestricted trailing : Nat .
42      (naturalAnd
43        (naturalEqual received telemetryIdentityBindingBytes)
44        (naturalIsZero trailing))))
45
46def telemetryBinaryIdentityValid =
47  (lambda unrestricted value : Bytes .
48    (naturalAnd
49      (naturalEqual (bytes-length value) telemetryIdentityBytes)
50      (aosAnyByte (lambda unrestricted b : Byte . (naturalIsZero (byte-equal b (byte 0)))) value)))
51
52-- 0 admitted, 1 insufficient destination, 2 incomplete entropy, 3 zero
53-- identity, 4 unsupported contract. A successful byte count alone is not
54-- permission to publish; every role must meet the AOS identity contract.
55def telemetryIdentityAdmission =
56  (lambda unrestricted version : Nat .
57    (lambda unrestricted extent : Nat .
58      (lambda unrestricted received : Nat .
59        (lambda unrestricted valid : Nat .
60          (aosChoose
61            Nat
62            (naturalAnd (naturalEqual version 1) (naturalLessOrEqual valid 1))
63            (aosChoose
64              Nat
65              (naturalLessOrEqual telemetryIdentitySetBytes extent)
66              (aosChoose
67                Nat
68                (naturalEqual received telemetryIdentitySetBytes)
69                (aosChoose Nat valid 0 3)
70                2)
71              1)
72            4)))))
73
74-- A supplied binding is three binary roles, already loaded into the identity
75-- arena. Epoch initialization retains those bytes and acquires only the last
76-- role. Admission proves the count/shape decision, not coordinator authority
77-- or entropy provenance. The native initializer validates the binding before
78-- asking the kernel for entropy and validates all four roles afterwards.
79def telemetryEpochAdmission =
80  (lambda unrestricted version : Nat .
81    (lambda unrestricted extent : Nat .
82      (lambda unrestricted received : Nat .
83        (lambda unrestricted valid : Nat .
84          (aosChoose
85            Nat
86            (naturalAnd (naturalEqual version 1) (naturalLessOrEqual valid 1))
87            (aosChoose
88              Nat
89              (naturalLessOrEqual telemetryIdentitySetBytes extent)
90              (aosChoose
91                Nat
92                (naturalEqual received telemetryIdentityBytes)
93                (aosChoose Nat valid 0 3)
94                2)
95              1)
96            4)))))
97
98-- Extend the capture arena, rather than reserving an unrelated absolute
99-- address. The application and acquisition residents keep their owner.
100def captureIdentityAt =
101  (lambda unrestricted applicationBytes : Nat .
102    (lambda unrestricted ordinaryCapacity : Nat .
103      (lambda unrestricted reservedCapacity : Nat .
104        (captureAlign (captureArenaBytes applicationBytes ordinaryCapacity reservedCapacity)))))
105
106def captureWithIdentityArenaBytes =
107  (lambda unrestricted applicationBytes : Nat .
108    (lambda unrestricted ordinaryCapacity : Nat .
109      (lambda unrestricted reservedCapacity : Nat .
110        (naturalAdd
111          (captureIdentityAt applicationBytes ordinaryCapacity reservedCapacity)
112          telemetryIdentitySetBytes))))
113
114def captureWithIdentityArenaResidents =
115  (lambda unrestricted applicationBytes : Nat .
116    (lambda unrestricted ordinaryCapacity : Nat .
117      (lambda unrestricted reservedCapacity : Nat .
118        (constructor
119          ArenaResidents
120          ArenaResidentsNext
121          (constructor
122            ArenaResident
123            ArenaResidentValue
124            b"telemetry-identities"
125            (captureIdentityAt applicationBytes ordinaryCapacity reservedCapacity)
126            telemetryIdentitySetBytes
127            captureWordBytes)
128          (captureArenaResidents applicationBytes ordinaryCapacity reservedCapacity)))))
129
130def captureWithIdentityArenaCertificate =
131  (lambda unrestricted applicationBytes : Nat .
132    (lambda unrestricted ordinaryCapacity : Nat .
133      (lambda unrestricted reservedCapacity : Nat .
134        (naturalAnd
135          (captureArenaCertificate applicationBytes ordinaryCapacity reservedCapacity)
136          (naturalAnd
137            (naturalLessOrEqual
138              (captureWithIdentityArenaBytes applicationBytes ordinaryCapacity reservedCapacity)
139              captureExtentMaximum)
140            (arenaCertificate
141              (captureWithIdentityArenaBytes applicationBytes ordinaryCapacity reservedCapacity)
142              (captureWithIdentityArenaResidents applicationBytes ordinaryCapacity reservedCapacity)))))))