1module Observe.Interchange
2
3import Data.UTF8
4import Model.Word32
5import Std.Byte
6import Std.Flag
7import Data.JSON
8import Data.JSONAccess
9import Observe.Value
10import Std.Natural
11
12-- AOS-JSON/1 RECORDS (docs/standards/AOS-1.0-draft-1.md §24): one line of a
13-- stream -- a header, descriptor, event, artifact, coverage or footer
14-- record, or a record of a type this reader does not know (retained and
15-- skipped, AOS-JSON-003) -- and the verdict code that says whether it is a
16-- valid record and, if not, the first rule it breaks.
17--
18-- THE CODES ARE A CONTRACT (docs/observability/README.md §"Validation
19-- contract"): the bootstrap tool's reader (tool/Aos.hs `LineCode`) returns
20-- the same number for the same line, and scripts/ci/observability.sh holds
21-- the two to it on every fixture. Never renumber one.
22--
23-- 0 valid 1 json 2 duplicate-key 3 limit
24-- 4 not-object 5 format 6 type 7 missing-field
25-- 8 integer 9 identity 10 value 11 availability
26-- 12 enum 13 field-type 14 required-extension
27--
28-- The checks run in a fixed order and the first that fails decides the
29-- code; the order is part of the contract.
30family AosLine : Type 0
31constructor AosLineInvalid
32field unrestricted aosLineInvalidCode : Nat
33constructor AosLineValid
34field unrestricted aosLineRecord : (family JSON)
35
36end-family
37
38-- The limits every AOS-JSON/1 stream declares in its header (a line of
39-- 1 MiB, 64 levels, a string of 256 KiB, 65,536 members), stated with
40-- Data.JSON's bounds.
41def aosLimits : (family JSONLimits) =
42 (constructor
43 JSONLimits
44 JSONLimitsValue
45 (constructor JSONBound JSONBoundAtMost 1048576)
46 (constructor JSONBound JSONBoundAtMost 64)
47 (constructor JSONBound JSONBoundAtMost 262144)
48 (constructor JSONBound JSONBoundAtMost 1024)
49 (constructor JSONBound JSONBoundAtMost 65536)
50 (constructor JSONBound JSONBoundBelowTwoPower 24))
51
52-- a parse failure's code: a duplicate name 2, a limit 3, anything else 1
53def aosParseErrorCode =
54 (lambda unrestricted error : (family JSONErrorCode) .
55 (eliminate
56 JSONErrorCode
57 (lambda unrestricted current : (family JSONErrorCode) . Nat)
58 error
59 (branch JSONInvalidUTF8 . 1)
60 (branch JSONUnexpectedEnd . 1)
61 (branch JSONTrailingBytes . 1)
62 (branch JSONInvalidValue . 1)
63 (branch JSONObjectKeyNotString . 1)
64 (branch JSONObjectColonMissing . 1)
65 (branch JSONObjectDelimiterMissing . 1)
66 (branch JSONObjectDuplicateKey . 2)
67 (branch JSONArrayDelimiterMissing . 1)
68 (branch JSONStringUnterminated . 1)
69 (branch JSONStringControlCharacter . 1)
70 (branch JSONEscapeInvalid . 1)
71 (branch JSONUnicodeEscapeInvalid . 1)
72 (branch JSONUnicodeLowWithoutHigh . 1)
73 (branch JSONUnicodeHighWithoutLow . 1)
74 (branch JSONNumberIntegerInvalid . 1)
75 (branch JSONNumberFractionDigitsMissing . 1)
76 (branch JSONNumberExponentDigitsMissing . 1)
77 (branch JSONExpectedObject . 1)
78 (branch JSONMissingMember . 1)
79 (branch JSONDuplicateMember . 2)
80 (branch JSONExpectedString . 1)
81 (branch JSONExpectedArray . 1)
82 (branch JSONExpectedNumber . 1)
83 (branch JSONExpectedInteger . 1)
84 (branch JSONExpectedBoolean . 1)
85 (branch JSONExpectedNull . 1)
86 (branch JSONInputLimitExceeded . 3)
87 (branch JSONDepthLimitExceeded . 3)
88 (branch JSONStringLimitExceeded . 3)
89 (branch JSONNumberLimitExceeded . 3)
90 (branch JSONContainerLimitExceeded . 3)
91 (branch JSONOutputLimitExceeded . 3)
92 (branch JSONNumericRangeUnsupported . 1)
93 (branch JSONMalformedTree . 1)))
94
95-- ---------------------------------------------------------------------------
96-- Field rules (each 0 when it holds, else its code)
97def aosTextCode =
98 (lambda unrestricted name : Bytes .
99 (lambda unrestricted value : (family JSON) .
100 (naturalSelect
101 (naturalIsZero (aosHas name value))
102 7
103 (naturalSelect (naturalIsZero (aosMemberIsString name value)) 13 0))))
104
105def aosNonEmptyTextCode =
106 (lambda unrestricted name : Bytes .
107 (lambda unrestricted value : (family JSON) .
108 (aosThen
109 (aosTextCode name value)
110 (naturalSelect (naturalIsZero (bytes-length (aosMemberBytes name value))) 13 0))))
111
112def aosIdentityCode =
113 (lambda unrestricted name : Bytes .
114 (lambda unrestricted value : (family JSON) .
115 (naturalSelect
116 (naturalIsZero (aosHas name value))
117 7
118 (naturalSelect
119 (naturalAnd (aosMemberIsString name value) (aosIsIdentity (aosMemberBytes name value)))
120 0
121 9))))
122
123def aosU64Code =
124 (lambda unrestricted name : Bytes .
125 (lambda unrestricted value : (family JSON) .
126 (naturalSelect
127 (naturalIsZero (aosHas name value))
128 7
129 (naturalSelect
130 (naturalAnd (aosMemberIsString name value) (aosIsU64Text (aosMemberBytes name value)))
131 0
132 8))))
133
134def aosObjectCode =
135 (lambda unrestricted name : Bytes .
136 (lambda unrestricted value : (family JSON) .
137 (naturalSelect
138 (naturalIsZero (aosHas name value))
139 7
140 (naturalSelect (aosIsObject (aosMemberValue name value)) 0 13))))
141
142def aosBooleanCode =
143 (lambda unrestricted name : Bytes .
144 (lambda unrestricted value : (family JSON) .
145 (naturalSelect
146 (naturalIsZero (aosHas name value))
147 7
148 (naturalSelect (aosIsBoolean (aosMemberValue name value)) 0 13))))
149
150-- 1 when every element of an array is a string (1 for a chain's end)
151def aosArrayAllStrings =
152 (lambda unrestricted value : (family JSON) .
153 (eliminate
154 JSON
155 (lambda unrestricted current : (family JSON) . Nat)
156 value
157 (branch JSONObject members membersInduction . 0)
158 (branch JSONObjectEnd . 0)
159 (branch JSONObjectMember key member tail memberInduction tailInduction . 0)
160 (branch JSONArray values valuesInduction . valuesInduction)
161 (branch JSONArrayEnd . 1)
162 (branch
163 JSONArrayNext
164 head
165 tail
166 headInduction
167 tailInduction
168 .
169 (naturalAnd (aosIsString head) tailInduction))
170 (branch JSONString text . 0)
171 (branch JSONNumber digits . 0)
172 (branch JSONBoolean flag . 0)
173 (branch JSONNull . 0)))
174
175def aosStringArrayCode =
176 (lambda unrestricted name : Bytes .
177 (lambda unrestricted value : (family JSON) .
178 (naturalSelect
179 (naturalIsZero (aosHas name value))
180 7
181 (let unrestricted member =
182 (aosMemberValue name value)
183 in
184 (naturalSelect (naturalAnd (aosIsArray member) (aosArrayAllStrings member)) 0 13)))))
185
186def aosArrayIsEmpty =
187 (lambda unrestricted value : (family JSON) .
188 (eliminate
189 JSON
190 (lambda unrestricted current : (family JSON) . Nat)
191 value
192 (branch JSONObject members membersInduction . 0)
193 (branch JSONObjectEnd . 0)
194 (branch JSONObjectMember key member tail memberInduction tailInduction . 0)
195 (branch JSONArray values valuesInduction . valuesInduction)
196 (branch JSONArrayEnd . 1)
197 (branch JSONArrayNext head tail headInduction tailInduction . 0)
198 (branch JSONString text . 0)
199 (branch JSONNumber digits . 0)
200 (branch JSONBoolean flag . 0)
201 (branch JSONNull . 0)))
202
203-- A required feature is interpretable only with its structural AND stream
204-- state handlers. Unknown requirements continue to refuse full validation.
205def aosKnownRequirements =
206 (lambda unrestricted value : (family JSON) .
207 (eliminate
208 JSON
209 (lambda unrestricted current : (family JSON) . Nat)
210 value
211 (branch JSONObject members membersInduction . 0)
212 (branch JSONObjectEnd . 0)
213 (branch JSONObjectMember key member tail memberInduction tailInduction . 0)
214 (branch JSONArray values valuesInduction . valuesInduction)
215 (branch JSONArrayEnd . 1)
216 (branch
217 JSONArrayNext
218 head
219 tail
220 headInduction
221 tailInduction
222 .
223 (naturalAnd headInduction tailInduction))
224 (branch JSONString text . (bytes-equal text b"aos.coverage.cumulative@1"))
225 (branch JSONNumber digits . 0)
226 (branch JSONBoolean flag . 0)
227 (branch JSONNull . 0)))
228
229def aosContainsCumulativeRequirement =
230 (lambda unrestricted value : (family JSON) .
231 (eliminate
232 JSON
233 (lambda unrestricted current : (family JSON) . Nat)
234 value
235 (branch JSONObject members membersInduction . 0)
236 (branch JSONObjectEnd . 0)
237 (branch JSONObjectMember key member tail memberInduction tailInduction . 0)
238 (branch JSONArray values valuesInduction . valuesInduction)
239 (branch JSONArrayEnd . 0)
240 (branch
241 JSONArrayNext
242 head
243 tail
244 headInduction
245 tailInduction
246 .
247 (naturalOr headInduction tailInduction))
248 (branch JSONString text . (bytes-equal text b"aos.coverage.cumulative@1"))
249 (branch JSONNumber digits . 0)
250 (branch JSONBoolean flag . 0)
251 (branch JSONNull . 0)))
252
253def aosCriticalExtensionCode =
254 (lambda unrestricted record : (family JSON) .
255 (naturalSelect
256 (aosHas b"required_extensions" record)
257 (aosThen
258 (aosStringArrayCode b"required_extensions" record)
259 (naturalSelect (aosKnownRequirements (aosMemberValue b"required_extensions" record)) 0 14))
260 0))
261
262-- 0 when the member (a present string) is one of the names, else 12
263def aosEnumCode =
264 (lambda unrestricted found : Nat . (naturalSelect found 0 12))
265
266-- an availability slot (AOS-JSON-006): {state: present, value} with the
267-- present value's own rule, or a non-present state, an optional structured
268-- reason, and no value
269def aosSlotCode =
270 (lambda unrestricted slot : (family JSON) .
271 (lambda unrestricted present : (pi unrestricted value : (family JSON) . Nat) .
272 (let unrestricted state =
273 (aosMemberBytes b"state" slot)
274 in
275 (naturalSelect
276 (naturalIsZero (aosMemberIsString b"state" slot))
277 11
278 (naturalSelect
279 (bytes-equal state b"present")
280 (naturalSelect
281 (aosHasExactly2 b"state" b"value" slot)
282 (present (aosMemberValue b"value" slot))
283 11)
284 (naturalSelect
285 (aosIsAbsenceState state)
286 (naturalSelect
287 (aosHasExactly1 b"state" slot)
288 0
289 (naturalSelect
290 (aosHasExactly2 b"state" b"reason" slot)
291 (naturalSelect (aosIsObject (aosMemberValue b"reason" slot)) 0 11)
292 11))
293 11))))))
294
295-- a present time: exactly clock_id, clock_epoch and ticks
296def aosTimeCode =
297 (lambda unrestricted value : (family JSON) .
298 (naturalSelect
299 (aosHasExactly3 b"clock_id" b"clock_epoch" b"ticks" value)
300 (aosThen
301 (aosIdentityCode b"clock_id" value)
302 (aosThen (aosIdentityCode b"clock_epoch" value) (aosU64Code b"ticks" value)))
303 11))
304
305-- a present context: exactly id
306def aosContextCode =
307 (lambda unrestricted value : (family JSON) .
308 (naturalSelect (aosHasExactly1 b"id" value) (aosIdentityCode b"id" value) 11))
309
310def aosValueCode =
311 (lambda unrestricted value : (family JSON) . (naturalSelect (aosIsValue value) 0 10))
312
313-- a payload member: a tagged value, or an availability slot of one
314def aosPayloadMemberCode =
315 (lambda unrestricted member : (family JSON) .
316 (naturalSelect
317 (aosHas b"t" member)
318 (aosValueCode member)
319 (naturalSelect (aosHas b"state" member) (aosSlotCode member aosValueCode) 10)))
320
321-- every payload member, in order: the first failure's code
322def aosPayloadCode =
323 (lambda unrestricted payload : (family JSON) .
324 (eliminate
325 JSON
326 (lambda unrestricted current : (family JSON) . Nat)
327 payload
328 (branch JSONObject members membersInduction . membersInduction)
329 (branch JSONObjectEnd . 0)
330 (branch
331 JSONObjectMember
332 key
333 member
334 tail
335 memberInduction
336 tailInduction
337 .
338 (aosThen (aosPayloadMemberCode member) tailInduction))
339 (branch JSONArray values valuesInduction . 0)
340 (branch JSONArrayEnd . 0)
341 (branch JSONArrayNext head tail headInduction tailInduction . 0)
342 (branch JSONString text . 0)
343 (branch JSONNumber digits . 0)
344 (branch JSONBoolean flag . 0)
345 (branch JSONNull . 0)))
346
347def aosIsRecordClass =
348 (lambda unrestricted text : Bytes .
349 (naturalOr
350 (bytes-equal text b"event")
351 (naturalOr
352 (bytes-equal text b"diagnostic")
353 (naturalOr
354 (bytes-equal text b"activity")
355 (naturalOr
356 (bytes-equal text b"state")
357 (naturalOr
358 (bytes-equal text b"metric")
359 (naturalOr
360 (bytes-equal text b"relation")
361 (naturalOr
362 (bytes-equal text b"artifact")
363 (naturalOr
364 (bytes-equal text b"receipt")
365 (naturalOr
366 (bytes-equal text b"descriptor")
367 (bytes-equal text b"capture-control")))))))))))
368
369def aosIsOriginKind =
370 (lambda unrestricted text : Bytes .
371 (naturalOr
372 (bytes-equal text b"direct")
373 (naturalOr
374 (bytes-equal text b"reported")
375 (naturalOr
376 (bytes-equal text b"derived")
377 (naturalOr (bytes-equal text b"simulated") (bytes-equal text b"estimated"))))))
378
379-- ---------------------------------------------------------------------------
380-- Records
381def aosHeaderCode =
382 (lambda unrestricted record : (family JSON) .
383 (aosThen
384 (aosNonEmptyTextCode b"aos_version" record)
385 (aosThen
386 (aosIdentityCode b"bundle_id" record)
387 (aosThen
388 (aosNonEmptyTextCode b"exporter" record)
389 (aosStringArrayCode b"required_extensions" record)))))
390
391def aosDescriptorCode =
392 (lambda unrestricted record : (family JSON) .
393 (aosThen
394 (aosNonEmptyTextCode b"descriptor_id" record)
395 (aosThen
396 (naturalSelect
397 (naturalLessOrEqual (bytes-length (aosMemberBytes b"descriptor_id" record)) 256)
398 0
399 13)
400 (aosThen (aosNonEmptyTextCode b"kind" record) (aosObjectCode b"body" record)))))
401
402def aosEventCode =
403 (lambda unrestricted record : (family JSON) .
404 (let unrestricted identity =
405 (aosMemberValue b"event_id" record)
406 in
407 (let unrestricted origin =
408 (aosMemberValue b"origin" record)
409 in
410 (aosThen
411 (aosNonEmptyTextCode b"aos_version" record)
412 (aosThen
413 (aosObjectCode b"event_id" record)
414 (aosThen
415 (aosIdentityCode b"attempt_id" identity)
416 (aosThen
417 (aosIdentityCode b"producer_id" identity)
418 (aosThen
419 (aosIdentityCode b"producer_epoch" identity)
420 (aosThen
421 (aosU64Code b"sequence" identity)
422 (aosThen
423 (aosNonEmptyTextCode b"schema_id" record)
424 (aosThen
425 (aosTextCode b"record_class" record)
426 (aosThen
427 (aosEnumCode (aosIsRecordClass (aosMemberBytes b"record_class" record)))
428 (aosThen
429 (aosIdentityCode b"policy_id" record)
430 (aosThen
431 (aosObjectCode b"origin" record)
432 (aosThen
433 (aosTextCode b"kind" origin)
434 (aosThen
435 (aosEnumCode (aosIsOriginKind (aosMemberBytes b"kind" origin)))
436 (aosThen
437 (naturalSelect (aosHas b"time" record) 0 7)
438 (aosThen
439 (aosSlotCode (aosMemberValue b"time" record) aosTimeCode)
440 (aosThen
441 (naturalSelect (aosHas b"context" record) 0 7)
442 (aosThen
443 (aosSlotCode
444 (aosMemberValue b"context" record)
445 aosContextCode)
446 (aosThen
447 (aosObjectCode b"payload" record)
448 (aosThen
449 (aosPayloadCode (aosMemberValue b"payload" record))
450 (aosThen
451 (naturalSelect
452 (aosHas b"extensions" record)
453 (naturalSelect
454 (aosIsArray (aosMemberValue b"extensions" record))
455 0
456 13)
457 7)
458 (aosStringArrayCode b"required_extensions" record))))))))))))))))))))))))
459
460-- `input` begins with `prefix`
461def aosHasPrefix =
462 (lambda unrestricted prefix : Bytes .
463 (lambda unrestricted input : Bytes .
464 (app
465 (bytes-eliminate
466 (lambda unrestricted current : Bytes . (pi unrestricted rest : Bytes . Nat))
467 (lambda unrestricted rest : Bytes . 1)
468 (lambda unrestricted head : Byte .
469 (lambda unrestricted tail : Bytes .
470 (lambda unrestricted induction : (pi unrestricted rest : Bytes . Nat) .
471 (lambda unrestricted rest : Bytes .
472 (naturalAnd
473 (naturalNonzero (bytes-length rest))
474 (naturalAnd (byte-equal head (bytes-head rest)) (induction (bytes-tail rest))))))))
475 prefix)
476 input)))
477
478-- `input` without its first `count` bytes
479def aosDropBytes =
480 (lambda unrestricted count : Nat .
481 (lambda unrestricted input : Bytes .
482 (app
483 (nat-eliminate
484 (lambda unrestricted current : Nat . (pi unrestricted rest : Bytes . Bytes))
485 (lambda unrestricted rest : Bytes . rest)
486 (lambda unrestricted predecessor : Nat .
487 (lambda unrestricted induction : (pi unrestricted rest : Bytes . Bytes) .
488 (lambda unrestricted rest : Bytes . (induction (bytes-tail rest)))))
489 count)
490 input)))
491
492-- `sha256:` then 64 lowercase hex digits
493def aosIsArtifactIdentity =
494 (lambda unrestricted text : Bytes .
495 (naturalAnd (aosHasPrefix b"sha256:" text) (aosIsHexOfWidth 64 (aosDropBytes 7 text))))
496
497def aosIsPublicationState =
498 (lambda unrestricted text : Bytes .
499 (naturalOr
500 (bytes-equal text b"requested")
501 (naturalOr
502 (bytes-equal text b"writing")
503 (naturalOr
504 (bytes-equal text b"complete")
505 (naturalOr (bytes-equal text b"verified") (bytes-equal text b"published"))))))
506
507def aosArtifactCode =
508 (lambda unrestricted record : (family JSON) .
509 (aosThen
510 (aosTextCode b"artifact_id" record)
511 (aosThen
512 (naturalSelect (aosIsArtifactIdentity (aosMemberBytes b"artifact_id" record)) 0 9)
513 (aosThen
514 (aosNonEmptyTextCode b"media" record)
515 (aosThen
516 (aosU64Code b"logical_size" record)
517 (aosThen
518 (aosTextCode b"state" record)
519 (aosThen
520 (aosEnumCode (aosIsPublicationState (aosMemberBytes b"state" record)))
521 (aosIdentityCode b"attempt_id" record))))))))
522
523-- A cumulative snapshot is exact and must announce its critical semantics
524-- on the record itself, so an older line reader cannot silently add totals.
525def aosCoverageModeCode =
526 (lambda unrestricted record : (family JSON) .
527 (naturalSelect
528 (aosHas b"coverage_mode" record)
529 (naturalSelect
530 (naturalAnd
531 (aosMemberIsString b"coverage_mode" record)
532 (naturalAnd
533 (bytes-equal (aosMemberBytes b"coverage_mode" record) b"cumulative")
534 (naturalAnd
535 (aosBooleanFlag (aosMemberValue b"dropped_exact" record))
536 (naturalAnd
537 (aosIsArray (aosMemberValue b"required_extensions" record))
538 (aosContainsCumulativeRequirement (aosMemberValue b"required_extensions" record))))))
539 0
540 12)
541 0))
542
543def aosCoverageCode =
544 (lambda unrestricted record : (family JSON) .
545 (aosThen
546 (aosIdentityCode b"attempt_id" record)
547 (aosThen
548 (aosIdentityCode b"producer_id" record)
549 (aosThen
550 (aosIdentityCode b"producer_epoch" record)
551 (aosThen
552 (aosU64Code b"next_sequence" record)
553 (aosThen
554 (aosU64Code b"records_accepted" record)
555 (aosThen
556 (aosU64Code b"records_dropped" record)
557 (aosThen
558 (aosU64Code b"records_excluded" record)
559 (aosThen (aosBooleanCode b"dropped_exact" record) (aosCoverageModeCode record))))))))))
560
561def aosIsTermination =
562 (lambda unrestricted text : Bytes .
563 (naturalOr
564 (bytes-equal text b"clean")
565 (naturalOr (bytes-equal text b"error") (bytes-equal text b"interrupted"))))
566
567def aosFooterCode =
568 (lambda unrestricted record : (family JSON) .
569 (aosThen
570 (aosU64Code b"records" record)
571 (aosThen
572 (aosTextCode b"termination" record)
573 (aosThen
574 (aosEnumCode (aosIsTermination (aosMemberBytes b"termination" record)))
575 (aosThen (aosBooleanCode b"complete" record) (aosStringArrayCode b"omissions" record))))))
576
577-- a parsed line's code: an object with the right format and a string type,
578-- then its type's rules (an unknown type is valid and skipped)
579def aosRecordCode =
580 (lambda unrestricted record : (family JSON) .
581 (let unrestricted kind =
582 (aosMemberBytes b"type" record)
583 in
584 (naturalSelect
585 (naturalIsZero (aosIsObject record))
586 4
587 (aosThen
588 (naturalSelect
589 (naturalAnd
590 (aosMemberIsString b"format" record)
591 (bytes-equal (aosMemberBytes b"format" record) b"AOS-JSON/1"))
592 0
593 5)
594 (aosThen
595 (naturalSelect (aosMemberIsString b"type" record) 0 6)
596 (aosThen
597 (naturalSelect
598 (bytes-equal kind b"header")
599 (aosHeaderCode record)
600 (naturalSelect
601 (bytes-equal kind b"descriptor")
602 (aosDescriptorCode record)
603 (naturalSelect
604 (bytes-equal kind b"event")
605 (aosEventCode record)
606 (naturalSelect
607 (bytes-equal kind b"artifact")
608 (aosArtifactCode record)
609 (naturalSelect
610 (bytes-equal kind b"coverage")
611 (aosCoverageCode record)
612 (naturalSelect (bytes-equal kind b"footer") (aosFooterCode record) 0))))))
613 (aosCriticalExtensionCode record)))))))
614
615-- ---------------------------------------------------------------------------
616-- Lines
617-- a line: parsed within the stream limits, then checked
618def aosClassifyLine =
619 (lambda unrestricted line : Bytes .
620 (eliminate
621 JSONDocumentResult
622 (lambda unrestricted current : (family JSONDocumentResult) . (family AosLine))
623 (parseJSONWithLimits aosLimits line)
624 (branch
625 JSONDocumentParsed
626 record
627 .
628 (let unrestricted code =
629 (aosRecordCode record)
630 in
631 (nat-eliminate
632 (lambda unrestricted current : Nat . (family AosLine))
633 (constructor AosLine AosLineValid record)
634 (lambda unrestricted predecessor : Nat .
635 (lambda unrestricted induction : (family AosLine) .
636 (constructor AosLine AosLineInvalid code)))
637 code)))
638 (branch
639 JSONDocumentFailed
640 error
641 offset
642 .
643 (constructor AosLine AosLineInvalid (aosParseErrorCode error)))))
644
645-- the line's verdict code (0: a valid record)
646def aosLineCode =
647 (lambda unrestricted line : Bytes .
648 (eliminate
649 AosLine
650 (lambda unrestricted current : (family AosLine) . Nat)
651 (aosClassifyLine line)
652 (branch AosLineInvalid code . code)
653 (branch AosLineValid record . 0)))
654
655-- A descriptor is source-declared data. Constructing this tree grants no
656-- validity or authority; renderJSON and the normal AOS readers still check it.
657def aosDescriptorRecord =
658 (lambda unrestricted kind : Bytes .
659 (lambda unrestricted identity : Bytes .
660 (lambda unrestricted body : (family JSON) .
661 (constructor
662 JSON
663 JSONObject
664 (constructor
665 JSON
666 JSONObjectMember
667 b"format"
668 (constructor JSON JSONString b"AOS-JSON/1")
669 (constructor
670 JSON
671 JSONObjectMember
672 b"type"
673 (constructor JSON JSONString b"descriptor")
674 (constructor
675 JSON
676 JSONObjectMember
677 b"kind"
678 (constructor JSON JSONString kind)
679 (constructor
680 JSON
681 JSONObjectMember
682 b"descriptor_id"
683 (constructor JSON JSONString identity)
684 (constructor JSON JSONObjectMember b"body" body (constructor JSON JSONObjectEnd))))))))))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.