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