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