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.
2307def sm86RepeatedProgramBytesBuilder =
2308 (lambda unrestricted payload : Bytes .
2309 (lambda unrestricted count : Nat .
2310 (nat-eliminate
2311 (lambda unrestricted current : Nat . BytesBuilder)
2312 (bytes-builder-empty)
2313 (lambda unrestricted predecessor : Nat .
2314 (lambda unrestricted induction : BytesBuilder .
2315 (bytes-builder-append (bytes-builder-chunk payload) induction)))
2316 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.