Encode structural repetition without first expanding the repeated program.
This is the physical-program analogue of a bytes builder: the segment is
validated and encoded once, while its already-checked image is retained as
a shared chunk until the final build. Large unrolled schedules therefore
remain linear in their output size instead of repeatedly normalizing the
same instruction terms.
2409def sm86RepeatedProgramBytesBuilder =
2410 (lambda unrestricted payload : Bytes .
2411 (lambda unrestricted count : Nat .
2412 (nat-eliminate
2413 (lambda unrestricted current : Nat . BytesBuilder)
2414 (bytes-builder-empty)
2415 (lambda unrestricted predecessor : Nat .
2416 (lambda unrestricted induction : BytesBuilder .
2417 (bytes-builder-append (bytes-builder-chunk payload) induction)))
2418 count)))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.