233def encodeRegionFrame =
234 (lambda unrestricted identity : (family RegionTransferIdentity) .
235 (lambda unrestricted headerBudget : Nat .
236 (lambda unrestricted payloadBudget : Nat .
237 (lambda unrestricted payload : Bytes .
238 (regionFrameRequire
239 (naturalLessOrEqual (bytes-length payload) payloadBudget)
240 (constructor RegionFrameFailure RegionFrameBounds)
241 (lambda unrestricted delayed : Nat .
242 (regionFrameThen
243 (regionFrameHeader identity (bytes-length payload) headerBudget)
244 (lambda unrestricted header : Bytes .
245 (regionFrameRequire
246 (naturalAnd
247 (naturalLessOrEqual
248 (bytes-length header)
249 (naturalSaturatingSubtract regionFrameWordLimit regionFrameDigestBytes))
250 (naturalLessOrEqual
251 (bytes-length payload)
252 (naturalSaturatingSubtract
253 (naturalSaturatingSubtract regionFrameWordLimit regionFrameDigestBytes)
254 (bytes-length header))))
255 (constructor RegionFrameFailure RegionFrameBounds)
256 (lambda unrestricted delayed : Nat .
257 (let unrestricted content =
258 (bytes-append header payload)
259 in
260 (regionFrameThen
261 (regionFrameHash content)
262 (lambda unrestricted digest : Bytes .
263 (regionFrameSuccess (bytes-append content digest)))))))))))))))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.