This checks individual record binding and the bounded payload population.
Cross-record sequence uniqueness, cumulative conservation, descriptor
immutability and stream schema meaning are additional admission gates; a
successful result here is not a publication/durability acknowledgement.
561def publicationTypedPayloadAdmission =
562 (lambda unrestricted identities : Bytes .
563 (lambda unrestricted lower : Nat .
564 (lambda unrestricted upper : Nat .
565 (lambda unrestricted occupied : Nat .
566 (lambda unrestricted records : (family StdList Bytes) .
567 (naturalAnd
568 (publicationTypedIdentitiesValid identities)
569 (naturalAnd
570 (naturalEqual (publicationTypedEventCount records) occupied)
571 (naturalAnd
572 (naturalLessOrEqual (aosListLength records) 1024)
573 (naturalAnd
574 (naturalLessOrEqual
575 (publicationRecordBytes
576 (naturalAdd
577 publicationPayloadRecordsAt
578 (bytes-length (publicationTypedRecordBytes records))))
579 publicationMaximumFrameBytes)
580 (eliminate
581 StdList
582 (lambda unrestricted current : (family StdList Bytes) . Nat)
583 records
584 (branch StdListEmpty . 1)
585 (branch
586 StdListCons
587 head
588 tail
589 induction
590 .
591 (naturalAnd
592 induction
593 (publicationTypedLineAdmission
594 (publicationTypedRecordKey identities)
595 lower
596 upper
597 head)))))))))))))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.