This decoder is for a bounded scheduled frame, not a discovery protocol.
It rejects trailing bytes as well as truncation and binds the digest to the
complete scope. Native framing reads the expected header and body extents
separately; this pure boundary validates the completed immutable bytes.
269def decodeRegionFrame =
270 (lambda unrestricted identity : (family RegionTransferIdentity) .
271 (lambda unrestricted expectedBytes : Nat .
272 (lambda unrestricted headerBudget : Nat .
273 (lambda unrestricted frame : Bytes .
274 (regionFrameThen
275 (regionFrameHeader identity expectedBytes headerBudget)
276 (lambda unrestricted header : Bytes .
277 (regionFrameRequire
278 (naturalAnd
279 (naturalLessOrEqual regionFrameDigestBytes (bytes-length frame))
280 (naturalAnd
281 (naturalLessOrEqual
282 (bytes-length header)
283 (naturalSaturatingSubtract (bytes-length frame) regionFrameDigestBytes))
284 (naturalEqual
285 expectedBytes
286 (naturalSaturatingSubtract
287 (naturalSaturatingSubtract (bytes-length frame) regionFrameDigestBytes)
288 (bytes-length header)))))
289 (constructor RegionFrameFailure RegionFrameWrongExtent)
290 (lambda unrestricted delayed : Nat .
291 (regionFrameRequire
292 (bytes-equal header (dataBytesTakeValidated (bytes-length header) frame))
293 (constructor RegionFrameFailure RegionFrameWrongHeader)
294 (lambda unrestricted delayed : Nat .
295 (let unrestricted contentBytes =
296 (naturalSaturatingSubtract (bytes-length frame) regionFrameDigestBytes)
297 in
298 (regionFrameThen
299 (regionFrameHash (dataBytesTakeValidated contentBytes frame))
300 (lambda unrestricted digest : Bytes .
301 (regionFrameRequire
302 (bytes-equal digest (dataBytesDropValidated contentBytes frame))
303 (constructor RegionFrameFailure RegionFrameWrongDigest)
304 (lambda unrestricted delayed : Nat .
305 (regionFrameSuccess
306 (dataBytesTakeValidated
307 expectedBytes
308 (dataBytesDropValidated (bytes-length header) frame))))))))))))))))))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.