225def checkpointEnvelopeVerdictOf =
226 (lambda unrestricted contract : (family CheckpointEnvelopeContract) .
227 (lambda unrestricted file : Bytes .
228 (let unrestricted digests = (checkpointEnvelopeIdentityDigests contract) in
229 (let unrestricted identity = (lambda unrestricted index : Nat . (lambda unrestricted at : Nat .
230 (bytes-equal (checkpointEnvelopeSlice file at checkpointEnvelopeDigestBytes)
231 (checkpointEnvelopeSlice digests (naturalMultiply index checkpointEnvelopeDigestBytes) checkpointEnvelopeDigestBytes)))) in
232 (let unrestricted bad = (checkpointEnvelopeFirstBadChunk contract file) in
233 (checkpointEnvelopeIf
234 (naturalEqual (bytes-length file) (checkpointEnvelopeFileBytes contract))
235 (checkpointEnvelopeIf
236 (bytes-equal (checkpointEnvelopeSlice file 0 checkpointEnvelopeFixedBytes) (checkpointEnvelopeFixed contract))
237 (checkpointEnvelopeIf (identity 0 checkpointEnvelopeSchemaAt)
238 (checkpointEnvelopeIf (identity 1 checkpointEnvelopeLearnerAt)
239 (checkpointEnvelopeIf (identity 2 checkpointEnvelopeDataAt)
240 (checkpointEnvelopeIf (identity 3 checkpointEnvelopeSeedAt)
241 (checkpointEnvelopeIf (naturalEqual bad (checkpointEnvelopeChunkCount contract))
242 (constructor CheckpointEnvelopeVerdict CheckpointEnvelopeAccepted)
243 (constructor CheckpointEnvelopeVerdict CheckpointEnvelopeChunkMismatch bad))
244 (constructor CheckpointEnvelopeVerdict CheckpointEnvelopeForeignSeed))
245 (constructor CheckpointEnvelopeVerdict CheckpointEnvelopeForeignData))
246 (constructor CheckpointEnvelopeVerdict CheckpointEnvelopeForeignLearner))
247 (constructor CheckpointEnvelopeVerdict CheckpointEnvelopeForeignSchema))
248 (constructor CheckpointEnvelopeVerdict CheckpointEnvelopeLayout))
249 (constructor CheckpointEnvelopeVerdict CheckpointEnvelopeTruncated)))))))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.