289def checkpointPreparedShardValid =
290 (lambda unrestricted region : (family CheckpointLogicalRegion) .
291 (lambda unrestricted capture : (family CheckpointCapture) .
292 (lambda unrestricted shard : (family CheckpointPreparedShard) .
293 (naturalAnd
294 (checkpointCaptureEqual capture (checkpointShardCapture shard))
295 (naturalAnd
296 (bytes-equal (logicalCheckpointFormat region) (checkpointShardFormat shard))
297 (naturalAnd
298 (naturalEqual
299 (checkpointShardBytes shard)
300 (intervalExtent (checkpointShardInterval shard)))
301 (naturalAnd
302 (naturalEqual
303 (bytes-length (checkpointShardDigest shard))
304 checkpointEnvelopeDigestBytes)
305 (naturalAnd
306 (intervalWithin (logicalCheckpointExtent region) (checkpointShardInterval shard))
307 (naturalLess
308 (intervalBegin (checkpointShardInterval shard))
309 (intervalEnd (checkpointShardInterval shard)))))))))))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.