the index of the first chunk whose digest differs, or the chunk count
209def checkpointEnvelopeFirstBadChunk =
210 (lambda unrestricted contract : (family CheckpointEnvelopeContract) .
211 (lambda unrestricted file : Bytes .
212 (let unrestricted count = (checkpointEnvelopeChunkCount contract) in
213 (let unrestricted header = (checkpointEnvelopeHeaderBytes contract) in
214 (let unrestricted chunk = (checkpointEnvelopeContractChunk contract) in
215 (app
216 (nat-eliminate
217 (lambda unrestricted remaining : Nat . (pi unrestricted index : Nat . Nat))
218 (lambda unrestricted index : Nat . index)
219 (lambda unrestricted p : Nat .
220 (lambda unrestricted induction : (pi unrestricted index : Nat . Nat) .
221 (lambda unrestricted index : Nat .
222 (nat-eliminate
223 (lambda unrestricted same : Nat . Nat)
224 index
225 (lambda unrestricted q : Nat . (lambda unrestricted ignored : Nat . (induction (succ index))))
226 (bytes-equal
227 (checkpointEnvelopeSlice file (naturalAdd checkpointEnvelopeDigestsAt (naturalMultiply checkpointEnvelopeDigestBytes index)) checkpointEnvelopeDigestBytes)
228 (sha256RawDigestOrEmpty (checkpointEnvelopeSlice file (naturalAdd header (naturalMultiply chunk index)) (checkpointEnvelopeChunkExtent contract index))))))))
229 count)
230 0))))))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.