1module Observe.Stream
2
3import Data.UTF8
4import Model.Word32
5import Std.Byte
6import Std.Flag
7import Data.JSON
8import Data.JSONAccess
9import Observe.Value
10import Observe.Interchange
11import Std.List
12import Std.Natural
13
14-- AOS-JSON/1 STREAMS (docs/standards/AOS-1.0-draft-1.md §24.1, §10): a
15-- stream's verdict -- complete, incomplete or invalid -- and the reason.
16--
17-- invalid a line that is not a valid record; a first record that is
18-- not a header; a record after the footer; a footer whose
19-- count is not the number of lines before it; an event whose
20-- sequence does not increase within its producer epoch
21-- incomplete bytes after the last LF (a torn write: AOS-REC-001's valid
22-- prefix with an incomplete tail); no footer (AOS-JSON-002);
23-- a footer that says incomplete; sequences missing beyond
24-- the drops the producer's coverage record declares
25-- (AOS-COV-004 .. 005)
26-- complete none of these: complete for what the stream declares, not
27-- a claim that every physical event was observed (AOS-COV-001)
28--
29-- An incomplete stream is not an invalid one: its records remain
30-- individually valid evidence (AOS-OBS-004). Status and problem numbers are
31-- a contract with the bootstrap reader (tool/Aos.hs `StreamStatus`,
32-- `StreamProblem`); never renumber one.
33--
34-- status 0 complete, 1 incomplete, 2 invalid
35-- problem 0 none, 1 empty, 2 invalid-line, 3 header-missing,
36-- 4 after-footer, 5 footer-count, 6 sequence-order, 7 no-footer,
37-- 8 footer-incomplete, 9 truncated-tail, 10 unaccounted-gap,
38-- 11 coverage-cumulative
39-- ---------------------------------------------------------------------------
40-- Lines
41family AosStreamVerdict : Type 0
42constructor AosStreamVerdictValue
43field unrestricted aosVerdictStatus : Nat
44field unrestricted aosVerdictProblem : Nat
45field unrestricted aosVerdictLine : Nat
46field unrestricted aosVerdictLineCode : Nat
47field unrestricted aosVerdictLines : Nat
48field unrestricted aosVerdictEvents : Nat
49field unrestricted aosVerdictUnknownRecords : Nat
50field unrestricted aosVerdictTruncatedBytes : Nat
51field unrestricted aosVerdictGaps : Nat
52field unrestricted aosVerdictDeclaredDrops : Nat
53
54end-family
55
56-- one producer epoch's sequence state: the next sequence not yet seen (the
57-- last seen plus one; 0 before any), the events seen, the drops declared
58family AosProducer : Type 0
59constructor AosProducerValue
60field unrestricted aosProducerKey : Bytes
61field unrestricted aosProducerNext : Nat
62field unrestricted aosProducerEvents : Nat
63field unrestricted aosProducerDrops : Nat
64field unrestricted aosProducerCoveredNext : Nat
65field unrestricted aosProducerExcluded : Nat
66field unrestricted aosProducerCoverageMode : Nat
67
68end-family
69
70family AosWalk : Type 0
71constructor AosWalkValue
72field unrestricted aosWalkProblem : Nat
73field unrestricted aosWalkProblemLine : Nat
74field unrestricted aosWalkLineCode : Nat
75field unrestricted aosWalkProducers : (family StdList (family AosProducer))
76field unrestricted aosWalkFooter : Nat
77field unrestricted aosWalkFooterComplete : Nat
78field unrestricted aosWalkEvents : Nat
79field unrestricted aosWalkUnknown : Nat
80
81end-family
82
83family AosFound : Type 0
84constructor AosFoundNone
85constructor AosFoundSome
86field unrestricted aosFoundProducer : (family AosProducer)
87
88end-family
89
90def aosBytesCons =
91 (lambda unrestricted head : Bytes .
92 (lambda unrestricted rest : (family StdList Bytes) .
93 (constructor StdList StdListCons Bytes head rest)))
94
95def aosListHead =
96 (lambda unrestricted list : (family StdList Bytes) .
97 (eliminate
98 StdList
99 (lambda unrestricted current : (family StdList Bytes) . Bytes)
100 list
101 (branch StdListEmpty . b"")
102 (branch StdListCons head tail induction . head)))
103
104def aosListTail =
105 (lambda unrestricted list : (family StdList Bytes) .
106 (eliminate
107 StdList
108 (lambda unrestricted current : (family StdList Bytes) . (family StdList Bytes))
109 list
110 (branch StdListEmpty . (constructor StdList StdListEmpty Bytes))
111 (branch StdListCons head tail induction . tail)))
112
113-- The stream split at every LF: n LFs give n + 1 segments, the last the
114-- bytes after the final LF (empty for a stream that ends with one).
115def aosSegments =
116 (lambda unrestricted stream : Bytes .
117 (bytes-eliminate
118 (lambda unrestricted current : Bytes . (family StdList Bytes))
119 (aosBytesCons b"" (constructor StdList StdListEmpty Bytes))
120 (lambda unrestricted head : Byte .
121 (lambda unrestricted tail : Bytes .
122 (lambda unrestricted induction : (family StdList Bytes) .
123 (nat-eliminate
124 (lambda unrestricted current : Nat . (family StdList Bytes))
125 (aosBytesCons (bytes-cons head (aosListHead induction)) (aosListTail induction))
126 (lambda unrestricted predecessor : Nat .
127 (lambda unrestricted inner : (family StdList Bytes) . (aosBytesCons b"" induction)))
128 (byte-equal head (byte 10))))))
129 stream))
130
131def aosListLength =
132 (lambda unrestricted list : (family StdList Bytes) .
133 (eliminate
134 StdList
135 (lambda unrestricted current : (family StdList Bytes) . Nat)
136 list
137 (branch StdListEmpty . 0)
138 (branch StdListCons head tail induction . (succ induction))))
139
140def aosListLast =
141 (lambda unrestricted list : (family StdList Bytes) .
142 (eliminate
143 StdList
144 (lambda unrestricted current : (family StdList Bytes) . Bytes)
145 list
146 (branch StdListEmpty . b"")
147 (branch
148 StdListCons
149 head
150 tail
151 induction
152 .
153 (aosChoose Bytes (naturalIsZero (aosListLength tail)) head induction))))
154
155-- ---------------------------------------------------------------------------
156-- Producers
157-- the producer epoch an event or a coverage record belongs to
158def aosProducerKeyOf =
159 (lambda unrestricted identity : (family JSON) .
160 (bytes-append
161 (aosMemberBytes b"attempt_id" identity)
162 (bytes-append
163 b"/"
164 (bytes-append
165 (aosMemberBytes b"producer_id" identity)
166 (bytes-append b"/" (aosMemberBytes b"producer_epoch" identity))))))
167
168def aosKeyOf =
169 (lambda unrestricted producer : (family AosProducer) .
170 (eliminate
171 AosProducer
172 (lambda unrestricted current : (family AosProducer) . Bytes)
173 producer
174 (branch AosProducerValue key next events drops covered excluded mode . key)))
175
176def aosFind =
177 (lambda unrestricted key : Bytes .
178 (lambda unrestricted producers : (family StdList (family AosProducer)) .
179 (eliminate
180 StdList
181 (lambda unrestricted current : (family StdList (family AosProducer)) . (family AosFound))
182 producers
183 (branch StdListEmpty . (constructor AosFound AosFoundNone))
184 (branch
185 StdListCons
186 head
187 tail
188 induction
189 .
190 (aosChoose
191 (family AosFound)
192 (bytes-equal (aosKeyOf head) key)
193 (constructor AosFound AosFoundSome head)
194 induction)))))
195
196-- the list with the producer of `key` replaced by `update` of what was there
197-- (appended when absent)
198def aosUpsert =
199 (lambda unrestricted key : Bytes .
200 (lambda unrestricted update : (pi unrestricted found : (family AosFound) . (family AosProducer)) .
201 (lambda unrestricted producers : (family StdList (family AosProducer)) .
202 (eliminate
203 StdList
204 (lambda unrestricted current : (family StdList (family AosProducer)) .
205 (family StdList (family AosProducer)))
206 producers
207 (branch
208 StdListEmpty
209 .
210 (constructor
211 StdList
212 StdListCons
213 (family AosProducer)
214 (update (constructor AosFound AosFoundNone))
215 (constructor StdList StdListEmpty (family AosProducer))))
216 (branch
217 StdListCons
218 head
219 tail
220 induction
221 .
222 (aosChoose
223 (family StdList (family AosProducer))
224 (bytes-equal (aosKeyOf head) key)
225 (constructor
226 StdList
227 StdListCons
228 (family AosProducer)
229 (update (constructor AosFound AosFoundSome head))
230 tail)
231 (constructor StdList StdListCons (family AosProducer) head induction)))))))
232
233-- ---------------------------------------------------------------------------
234-- The walk
235def aosWalkInitial : (family AosWalk) =
236 (constructor
237 AosWalk
238 AosWalkValue
239 0
240 0
241 0
242 (constructor StdList StdListEmpty (family AosProducer))
243 0
244 0
245 0
246 0)
247
248-- the walk with a problem found at line n (it stops the walk)
249def aosWalkFail =
250 (lambda unrestricted walk : (family AosWalk) .
251 (lambda unrestricted problem : Nat .
252 (lambda unrestricted n : Nat .
253 (lambda unrestricted code : Nat .
254 (eliminate
255 AosWalk
256 (lambda unrestricted current : (family AosWalk) . (family AosWalk))
257 walk
258 (branch
259 AosWalkValue
260 oldProblem
261 oldLine
262 oldCode
263 producers
264 footer
265 complete
266 events
267 unknown
268 .
269 (constructor
270 AosWalk
271 AosWalkValue
272 problem
273 n
274 code
275 producers
276 footer
277 complete
278 events
279 unknown)))))))
280
281def aosDecimalOf =
282 (lambda unrestricted name : Bytes .
283 (lambda unrestricted value : (family JSON) . (aosDigitsValue (aosMemberBytes name value))))
284
285-- an event: its sequence must exceed every earlier one of its producer epoch
286def aosWalkEvent =
287 (lambda unrestricted walk : (family AosWalk) .
288 (lambda unrestricted n : Nat .
289 (lambda unrestricted record : (family JSON) .
290 (let unrestricted identity =
291 (aosMemberValue b"event_id" record)
292 in
293 (let unrestricted key =
294 (aosProducerKeyOf identity)
295 in
296 (let unrestricted sequence =
297 (aosDecimalOf b"sequence" identity)
298 in
299 (eliminate
300 AosWalk
301 (lambda unrestricted current : (family AosWalk) . (family AosWalk))
302 walk
303 (branch
304 AosWalkValue
305 problem
306 line
307 code
308 producers
309 footer
310 complete
311 events
312 unknown
313 .
314 (let unrestricted outOfOrder =
315 (eliminate
316 AosFound
317 (lambda unrestricted current : (family AosFound) . Nat)
318 (aosFind key producers)
319 (branch AosFoundNone . 0)
320 (branch
321 AosFoundSome
322 producer
323 .
324 (eliminate
325 AosProducer
326 (lambda unrestricted current : (family AosProducer) . Nat)
327 producer
328 (branch
329 AosProducerValue
330 k
331 next
332 seen
333 drops
334 covered
335 excluded
336 mode
337 .
338 (naturalOr (naturalLess sequence next) (naturalLess sequence covered))))))
339 in
340 (aosChoose
341 (family AosWalk)
342 outOfOrder
343 (aosWalkFail walk 6 n 0)
344 (constructor
345 AosWalk
346 AosWalkValue
347 problem
348 line
349 code
350 (aosUpsert
351 key
352 (lambda unrestricted found : (family AosFound) .
353 (eliminate
354 AosFound
355 (lambda unrestricted current : (family AosFound) .
356 (family AosProducer))
357 found
358 (branch
359 AosFoundNone
360 .
361 (constructor
362 AosProducer
363 AosProducerValue
364 key
365 (succ sequence)
366 1
367 0
368 0
369 0
370 0))
371 (branch
372 AosFoundSome
373 producer
374 .
375 (eliminate
376 AosProducer
377 (lambda unrestricted current : (family AosProducer) .
378 (family AosProducer))
379 producer
380 (branch
381 AosProducerValue
382 k
383 next
384 seen
385 drops
386 covered
387 excluded
388 mode
389 .
390 (constructor
391 AosProducer
392 AosProducerValue
393 key
394 (succ sequence)
395 (succ seen)
396 drops
397 covered
398 excluded
399 mode))))))
400 producers)
401 footer
402 complete
403 (succ events)
404 unknown)))))))))))
405
406-- Legacy coverage adds interval counts. Critical cumulative coverage is an
407-- exact prefix snapshot: repeated checkpoints replace totals, never add them.
408-- One selected sequence is either accepted or dropped; policy exclusions
409-- consume no sequence. Shared by cumulative coverage and live observer views.
410def aosSequenceAccounting =
411 (lambda unrestricted next : Nat . (lambda unrestricted accepted : Nat .
412 (lambda unrestricted dropped : Nat .
413 (naturalEqual next (naturalAdd accepted dropped)))))
414
415-- Accepted observations must equal the actual seen population; next includes
416-- trailing selected losses. A producer cannot mix the two coverage meanings.
417def aosCoverageConsistent =
418 (lambda unrestricted producer : (family AosProducer) .
419 (lambda unrestricted record : (family JSON) .
420 (eliminate
421 AosProducer
422 (lambda unrestricted current : (family AosProducer) . Nat)
423 producer
424 (branch
425 AosProducerValue
426 key
427 next
428 seen
429 drops
430 covered
431 excluded
432 mode
433 .
434 (aosChoose
435 Nat
436 (bytes-equal (aosMemberBytes b"coverage_mode" record) b"cumulative")
437 (naturalAnd
438 (naturalIsZero (naturalEqual mode 1))
439 (naturalAnd
440 (naturalLessOrEqual next (aosDecimalOf b"next_sequence" record))
441 (naturalAnd
442 (naturalLessOrEqual covered (aosDecimalOf b"next_sequence" record))
443 (naturalAnd
444 (naturalLessOrEqual drops (aosDecimalOf b"records_dropped" record))
445 (naturalAnd
446 (naturalLessOrEqual excluded (aosDecimalOf b"records_excluded" record))
447 (naturalAnd
448 (naturalEqual seen (aosDecimalOf b"records_accepted" record))
449 (aosSequenceAccounting
450 (aosDecimalOf b"next_sequence" record)
451 seen (aosDecimalOf b"records_dropped" record))))))))
452 (naturalIsZero (naturalEqual mode 2)))))))
453
454def aosCoverageUpdate =
455 (lambda unrestricted producer : (family AosProducer) .
456 (lambda unrestricted record : (family JSON) .
457 (eliminate
458 AosProducer
459 (lambda unrestricted current : (family AosProducer) . (family AosProducer))
460 producer
461 (branch
462 AosProducerValue
463 key
464 next
465 seen
466 drops
467 covered
468 excluded
469 mode
470 .
471 (aosChoose
472 (family AosProducer)
473 (bytes-equal (aosMemberBytes b"coverage_mode" record) b"cumulative")
474 (constructor
475 AosProducer
476 AosProducerValue
477 key
478 next
479 seen
480 (aosDecimalOf b"records_dropped" record)
481 (aosDecimalOf b"next_sequence" record)
482 (aosDecimalOf b"records_excluded" record)
483 2)
484 (constructor
485 AosProducer
486 AosProducerValue
487 key
488 next
489 seen
490 (naturalAdd drops (aosDecimalOf b"records_dropped" record))
491 covered
492 excluded
493 1))))))
494
495def aosCoveragePrior =
496 (lambda unrestricted key : Bytes .
497 (lambda unrestricted found : (family AosFound) .
498 (eliminate
499 AosFound
500 (lambda unrestricted current : (family AosFound) . (family AosProducer))
501 found
502 (branch AosFoundNone . (constructor AosProducer AosProducerValue key 0 0 0 0 0 0))
503 (branch AosFoundSome producer . producer))))
504
505def aosWalkCoverage =
506 (lambda unrestricted walk : (family AosWalk) .
507 (lambda unrestricted n : Nat .
508 (lambda unrestricted record : (family JSON) .
509 (let unrestricted key =
510 (aosProducerKeyOf record)
511 in
512 (eliminate
513 AosWalk
514 (lambda unrestricted current : (family AosWalk) . (family AosWalk))
515 walk
516 (branch
517 AosWalkValue
518 problem
519 line
520 code
521 producers
522 footer
523 complete
524 events
525 unknown
526 .
527 (aosChoose
528 (family AosWalk)
529 (aosCoverageConsistent (aosCoveragePrior key (aosFind key producers)) record)
530 (constructor
531 AosWalk
532 AosWalkValue
533 problem
534 line
535 code
536 (aosUpsert
537 key
538 (lambda unrestricted found : (family AosFound) .
539 (aosCoverageUpdate (aosCoveragePrior key found) record))
540 producers)
541 footer
542 complete
543 events
544 unknown)
545 (aosWalkFail walk 11 n 0))))))))
546
547-- the footer: it counts the lines before it
548def aosWalkFooter =
549 (lambda unrestricted walk : (family AosWalk) .
550 (lambda unrestricted n : Nat .
551 (lambda unrestricted record : (family JSON) .
552 (eliminate
553 AosWalk
554 (lambda unrestricted current : (family AosWalk) . (family AosWalk))
555 walk
556 (branch
557 AosWalkValue
558 problem
559 line
560 code
561 producers
562 footer
563 complete
564 events
565 unknown
566 .
567 (aosChoose
568 (family AosWalk)
569 (naturalEqual (aosDecimalOf b"records" record) (naturalSaturatingSubtract n 1))
570 (constructor
571 AosWalk
572 AosWalkValue
573 problem
574 line
575 code
576 producers
577 1
578 (aosBooleanFlag (aosMemberValue b"complete" record))
579 events
580 unknown)
581 (aosWalkFail walk 5 n 0)))))))
582
583def aosWalkUnknownRecord =
584 (lambda unrestricted walk : (family AosWalk) .
585 (eliminate
586 AosWalk
587 (lambda unrestricted current : (family AosWalk) . (family AosWalk))
588 walk
589 (branch
590 AosWalkValue
591 problem
592 line
593 code
594 producers
595 footer
596 complete
597 events
598 unknown
599 .
600 (constructor
601 AosWalk
602 AosWalkValue
603 problem
604 line
605 code
606 producers
607 footer
608 complete
609 events
610 (succ unknown)))))
611
612def aosWalkProblemOf =
613 (lambda unrestricted walk : (family AosWalk) .
614 (eliminate
615 AosWalk
616 (lambda unrestricted current : (family AosWalk) . Nat)
617 walk
618 (branch AosWalkValue problem line code producers footer complete events unknown . problem)))
619
620def aosWalkFooterOf =
621 (lambda unrestricted walk : (family AosWalk) .
622 (eliminate
623 AosWalk
624 (lambda unrestricted current : (family AosWalk) . Nat)
625 walk
626 (branch AosWalkValue problem line code producers footer complete events unknown . footer)))
627
628-- a valid record at line n
629def aosWalkRecord =
630 (lambda unrestricted walk : (family AosWalk) .
631 (lambda unrestricted n : Nat .
632 (lambda unrestricted record : (family JSON) .
633 (let unrestricted kind =
634 (aosMemberBytes b"type" record)
635 in
636 (aosChoose
637 (family AosWalk)
638 (naturalEqual n 1)
639 (aosChoose (family AosWalk) (bytes-equal kind b"header") walk (aosWalkFail walk 3 1 0))
640 (aosChoose
641 (family AosWalk)
642 (bytes-equal kind b"event")
643 (aosWalkEvent walk n record)
644 (aosChoose
645 (family AosWalk)
646 (bytes-equal kind b"coverage")
647 (aosWalkCoverage walk n record)
648 (aosChoose
649 (family AosWalk)
650 (bytes-equal kind b"footer")
651 (aosWalkFooter walk n record)
652 (aosChoose
653 (family AosWalk)
654 (naturalOr
655 (bytes-equal kind b"header")
656 (naturalOr (bytes-equal kind b"descriptor") (bytes-equal kind b"artifact")))
657 walk
658 (aosWalkUnknownRecord walk))))))))))
659
660-- line n of the stream: stops at the first problem
661def aosWalkLine =
662 (lambda unrestricted walk : (family AosWalk) .
663 (lambda unrestricted n : Nat .
664 (lambda unrestricted line : Bytes .
665 (aosChoose
666 (family AosWalk)
667 (aosWalkProblemOf walk)
668 walk
669 (eliminate
670 AosLine
671 (lambda unrestricted current : (family AosLine) . (family AosWalk))
672 (aosClassifyLine line)
673 (branch AosLineInvalid code . (aosWalkFail walk 2 n code))
674 (branch
675 AosLineValid
676 record
677 .
678 (aosChoose
679 (family AosWalk)
680 (aosWalkFooterOf walk)
681 (aosWalkFail walk 4 n 0)
682 (aosWalkRecord walk n record))))))))
683
684-- the complete lines (every segment but the last), walked in order from
685-- line 1: a left fold, the walk threaded through the right fold's functions
686def aosWalkLinesFrom =
687 (lambda unrestricted initial : (family AosWalk) .
688 (lambda unrestricted firstLine : Nat .
689 (lambda unrestricted segments : (family StdList Bytes) .
690 (app
691 (eliminate
692 StdList
693 (lambda unrestricted current : (family StdList Bytes) .
694 (pi unrestricted walk : (family AosWalk) .
695 (pi unrestricted n : Nat . (family AosWalk))))
696 segments
697 (branch
698 StdListEmpty
699 .
700 (lambda unrestricted walk : (family AosWalk) . (lambda unrestricted n : Nat . walk)))
701 (branch
702 StdListCons
703 line
704 rest
705 induction
706 .
707 (lambda unrestricted walk : (family AosWalk) .
708 (lambda unrestricted n : Nat .
709 -- the last segment is not a line: it is the tail after the last LF
710 (aosChoose
711 (family AosWalk)
712 (naturalIsZero (aosListLength rest))
713 walk
714 (induction (aosWalkLine walk n line) (succ n)))))))
715 initial
716 firstLine))))
717
718def aosWalkLines =
719 (lambda unrestricted segments : (family StdList Bytes) .
720 (aosWalkLinesFrom aosWalkInitial 1 segments))
721
722-- ---------------------------------------------------------------------------
723-- The verdict
724def aosSumGaps =
725 (lambda unrestricted producers : (family StdList (family AosProducer)) .
726 (lambda unrestricted withDrops : Nat .
727 (eliminate
728 StdList
729 (lambda unrestricted current : (family StdList (family AosProducer)) . Nat)
730 producers
731 (branch StdListEmpty . 0)
732 (branch
733 StdListCons
734 head
735 tail
736 induction
737 .
738 (naturalAdd
739 induction
740 (eliminate
741 AosProducer
742 (lambda unrestricted current : (family AosProducer) . Nat)
743 head
744 (branch
745 AosProducerValue
746 key
747 next
748 seen
749 drops
750 covered
751 excluded
752 mode
753 .
754 (naturalSaturatingSubtract
755 (naturalSaturatingSubtract
756 (aosChoose Nat (naturalLess next covered) covered next)
757 seen)
758 (naturalSelect withDrops drops 0)))))))))
759
760def aosSumDrops =
761 (lambda unrestricted producers : (family StdList (family AosProducer)) .
762 (eliminate
763 StdList
764 (lambda unrestricted current : (family StdList (family AosProducer)) . Nat)
765 producers
766 (branch StdListEmpty . 0)
767 (branch
768 StdListCons
769 head
770 tail
771 induction
772 .
773 (naturalAdd
774 induction
775 (eliminate
776 AosProducer
777 (lambda unrestricted current : (family AosProducer) . Nat)
778 head
779 (branch AosProducerValue key next seen drops covered excluded mode . drops))))))
780
781-- Finalization is separate from feeding so segment boundaries cannot reset
782-- sequence state, footer count, or the first diagnostic. Tail is its original
783-- byte extent, including a deliberately opaque oversized unfinished frame.
784def aosFinishStreamScan =
785 (lambda unrestricted lines : Nat .
786 (lambda unrestricted tailBytes : Nat .
787 (lambda unrestricted walk : (family AosWalk) .
788 (eliminate
789 AosWalk
790 (lambda unrestricted current : (family AosWalk) . (family AosStreamVerdict))
791 walk
792 (branch
793 AosWalkValue
794 problem
795 line
796 code
797 producers
798 footer
799 complete
800 events
801 unknown
802 .
803 (let unrestricted gaps =
804 (aosSumGaps producers 0)
805 in
806 (let unrestricted unaccounted =
807 (aosSumGaps producers 1)
808 in
809 (let unrestricted drops =
810 (aosSumDrops producers)
811 in
812 (let unrestricted verdict =
813 (lambda unrestricted status : Nat .
814 (lambda unrestricted found : Nat .
815 (constructor
816 AosStreamVerdict
817 AosStreamVerdictValue
818 status
819 found
820 line
821 code
822 lines
823 events
824 unknown
825 tailBytes
826 gaps
827 drops)))
828 in
829 (aosChoose
830 (family AosStreamVerdict)
831 problem
832 (verdict 2 problem)
833 (aosChoose
834 (family AosStreamVerdict)
835 (naturalIsZero lines)
836 (verdict 2 1)
837 (aosChoose
838 (family AosStreamVerdict)
839 tailBytes
840 (verdict 1 9)
841 (aosChoose
842 (family AosStreamVerdict)
843 (naturalIsZero footer)
844 (verdict 1 7)
845 (aosChoose
846 (family AosStreamVerdict)
847 (naturalIsZero complete)
848 (verdict 1 8)
849 (aosChoose
850 (family AosStreamVerdict)
851 unaccounted
852 (verdict 1 10)
853 (verdict 0 0))))))))))))))))
854
855def aosStreamVerdict =
856 (lambda unrestricted stream : Bytes .
857 (let unrestricted segments =
858 (aosSegments stream)
859 in
860 (aosFinishStreamScan
861 (naturalSaturatingSubtract (aosListLength segments) 1)
862 (bytes-length (aosListLast segments))
863 (aosWalkLines segments))))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.