46def telemetryRecordAssemblyFor =
47 (lambda erased A : Type 0 .
48 (lambda erased R : Type 0 .
49 (lambda unrestricted backend : (family TelemetryRecordBackend A R) .
50 (lambda unrestricted kind : (family TelemetryRecordRoutineKind) .
51 (eliminate
52 TelemetryRecordBackend
53 (lambda unrestricted current : (family TelemetryRecordBackend A R) . A)
54 backend
55 (branch
56 TelemetryRecordBackendValue
57 recordLoad64
58 recordOr
59 recordCompareImmediate
60 recordJumpZero
61 recordJumpBelow
62 recordSet
63 recordLabel
64 recordReturn
65 recordEnd
66 recordResult
67 recordScratch
68 recordSource
69 recordIdentities
70 recordSourceExtent
71 recordIdentityExtent
72 recordOutputExtent
73 .
74 (let unrestricted recordCheckNonzero =
75 (lambda unrestricted base : R .
76 (lambda unrestricted offset : Nat .
77 (lambda unrestricted tail : A .
78 (recordLoad64
79 recordResult
80 base
81 offset
82 (recordLoad64
83 recordScratch
84 base
85 (naturalAdd offset captureWordBytes)
86 (recordOr
87 recordResult
88 recordScratch
89 (recordCompareImmediate
90 recordResult
91 0
92 (recordJumpZero b"record-refused" tail))))))))
93 in
94 (let unrestricted recordCheckParts =
95 (lambda unrestricted parts : (family TelemetryRecordParts) .
96 (eliminate
97 TelemetryRecordParts
98 (lambda unrestricted current : (family TelemetryRecordParts) . A)
99 parts
100 (branch
101 TelemetryRecordEnd
102 .
103 (recordSet
104 recordResult
105 1
106 (recordReturn
107 (recordLabel
108 b"record-refused"
109 (recordSet recordResult 0 (recordReturn recordEnd))))))
110 (branch TelemetryRecordLiteral bytes tail induction . induction)
111 (branch TelemetryRecordDecimal signed offset tail induction . induction)
112 (branch
113 TelemetryRecordHex
114 source
115 offset
116 width
117 reverse
118 nonzero
119 tail
120 induction
121 .
122 (aosChoose
123 A
124 nonzero
125 (recordCheckNonzero
126 (aosChoose R source recordIdentities recordSource)
127 offset
128 induction)
129 induction))))
130 in
131 (let unrestricted recordAdmissionAssembly =
132 (lambda unrestricted parts : (family TelemetryRecordParts) .
133 (recordCompareImmediate
134 recordSourceExtent
135 captureRecordBytes
136 (recordJumpBelow
137 b"record-refused"
138 (recordCompareImmediate
139 recordIdentityExtent
140 telemetryIdentitySetBytes
141 (recordJumpBelow
142 b"record-refused"
143 (recordCompareImmediate
144 recordOutputExtent
145 (bytes-length (telemetryRecordPartBytes parts))
146 (recordJumpBelow
147 b"record-refused"
148 (nat-eliminate
149 (lambda unrestricted current : Nat . A)
150 (recordCheckParts parts)
151 (lambda unrestricted index : Nat .
152 (lambda unrestricted induction : A .
153 (recordCheckNonzero
154 recordIdentities
155 (telemetryIdentityOffset index)
156 induction)))
157 (succ telemetryProducerEpochIndex)))))))))
158 in
159 (eliminate
160 TelemetryRecordRoutineKind
161 (lambda unrestricted current : (family TelemetryRecordRoutineKind) . A)
162 kind
163 (branch
164 TelemetryRecordAdmissionRoutine
165 parts
166 .
167 (recordAdmissionAssembly parts))
168 (branch
169 TelemetryRecordStatusRoutine
170 .
171 (recordLoad64 recordResult recordSource 0 (recordReturn recordEnd)))))))))))))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.