Check by subtraction before concatenation. In particular no sum of lengths
may wrap and turn an oversized header into a seemingly small allocation.
79def regionFrameJoinWithin =
80 (lambda unrestricted chunks : (family StdList Bytes) .
81 (eliminate
82 StdList
83 (lambda unrestricted current : (family StdList Bytes) .
84 (pi unrestricted budget : Nat . (family StdResult (family RegionFrameFailure) Bytes)))
85 chunks
86 (branch StdListEmpty . (lambda unrestricted budget : Nat . (regionFrameSuccess b"")))
87 (branch
88 StdListCons
89 head
90 tail
91 induction
92 .
93 (lambda unrestricted budget : Nat .
94 (regionFrameRequire
95 (naturalLessOrEqual (bytes-length head) budget)
96 (constructor RegionFrameFailure RegionFrameBounds)
97 (lambda unrestricted delayed : Nat .
98 (regionFrameThen
99 (induction (naturalSaturatingSubtract budget (bytes-length head)))
100 (lambda unrestricted rest : Bytes . (regionFrameSuccess (bytes-append head rest))))))))))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.