Accepted observations must equal the actual seen population; next includes
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)))))))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.