the checkpoint a contract's host writes: the header -- fixed bytes,
`updates` and `invocations`, the identity digests, each chunk's digest
-- and the payload
261def checkpointEnvelopeWrite =
262 (lambda unrestricted contract : (family CheckpointEnvelopeContract) .
263 (lambda unrestricted updates : Nat .
264 (lambda unrestricted invocations : Nat .
265 (lambda unrestricted payload : Bytes .
266 (let unrestricted chunk = (checkpointEnvelopeContractChunk contract) in
267 (let unrestricted digests =
268 (bytes-builder-build
269 (app (nat-eliminate
270 (lambda unrestricted remaining : Nat . (pi unrestricted index : Nat . BytesBuilder))
271 (lambda unrestricted index : Nat . (bytes-builder-chunk b""))
272 (lambda unrestricted p : Nat .
273 (lambda unrestricted induction : (pi unrestricted index : Nat . BytesBuilder) .
274 (lambda unrestricted index : Nat .
275 (bytes-builder-append
276 (bytes-builder-chunk (sha256RawDigestOrEmpty (checkpointEnvelopeSlice payload (naturalMultiply chunk index) (checkpointEnvelopeChunkExtent contract index))))
277 (induction (succ index))))))
278 (checkpointEnvelopeChunkCount contract))
279 0)) in
280 (let unrestricted body =
281 (bytes-append (checkpointEnvelopeFixed contract)
282 (bytes-append (checkpointEnvelopeWord updates)
283 (bytes-append (checkpointEnvelopeWord invocations)
284 (bytes-append (checkpointEnvelopeIdentityDigests contract) digests)))) in
285 (bytes-append body
286 (bytes-append (checkpointEnvelopeZeros (naturalSaturatingSubtract (checkpointEnvelopeHeaderBytes contract) (bytes-length body)))
287 payload)))))))))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.