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.
2230def sm86RepeatedProgramBytesBuilder =
2231 (lambda unrestricted payload : Bytes .
2232 (lambda unrestricted count : Nat .
2233 (nat-eliminate
2234 (lambda unrestricted current : Nat . BytesBuilder)
2235 (bytes-builder-empty)
2236 (lambda unrestricted predecessor : Nat .
2237 (lambda unrestricted induction : BytesBuilder .
2238 (bytes-builder-append (bytes-builder-chunk payload) induction)))
2239 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.