2207def checkpointLoad =
2208 (lambda unrestricted schema : (family CheckpointSchema) .
2209 (lambda unrestricted image : (family CheckpointImage) .
2210 (eliminate
2211 CheckpointSchemaIdentityResult
2212 (lambda unrestricted current : (family CheckpointSchemaIdentityResult) .
2213 (family CheckpointLoadResult))
2214 (checkpointValidateSchemaIdentity schema)
2215 (branch
2216 CheckpointSchemaIdentityAccepted
2217 canonicalBytes
2218 .
2219 (eliminate
2220 CheckpointSchema
2221 (lambda unrestricted current : (family CheckpointSchema) .
2222 (family CheckpointLoadResult))
2223 schema
2224 (branch
2225 CheckpointSchemaValue
2226 policy
2227 expectedDigest
2228 fields
2229 parameterCount
2230 expectedPayload
2231 .
2232 (eliminate
2233 CheckpointImage
2234 (lambda unrestricted current : (family CheckpointImage) .
2235 (family CheckpointLoadResult))
2236 image
2237 (branch
2238 CheckpointImageValue
2239 actualDigest
2240 blocks
2241 .
2242 (app
2243 (lambda unrestricted expectedCount : Nat .
2244 (app
2245 (lambda unrestricted actualCount : Nat .
2246 (nat-eliminate
2247 (lambda unrestricted digestMatched : Nat .
2248 (family CheckpointLoadResult))
2249 (constructor
2250 CheckpointLoadResult
2251 CheckpointLoadRejected
2252 (checkpointFailure
2253 (constructor CheckpointErrorCode CheckpointSchemaIdentityMismatch)
2254 zero
2255 expectedDigest
2256 actualDigest)
2257 (checkpointValidationTelemetry
2258 expectedCount
2259 actualCount
2260 zero
2261 modelWord64Zero
2262 canonicalBytes))
2263 (lambda unrestricted digestPredecessor : Nat .
2264 (lambda unrestricted digestInduction : (family CheckpointLoadResult) .
2265 (nat-eliminate
2266 (lambda unrestricted countMatched : Nat .
2267 (family CheckpointLoadResult))
2268 (constructor
2269 CheckpointLoadResult
2270 CheckpointLoadRejected
2271 (checkpointSimpleFailure
2272 (constructor CheckpointErrorCode CheckpointFieldCountMismatch)
2273 zero)
2274 (checkpointValidationTelemetry
2275 expectedCount
2276 actualCount
2277 zero
2278 modelWord64Zero
2279 canonicalBytes))
2280 (lambda unrestricted countPredecessor : Nat .
2281 (lambda unrestricted countInduction : (family CheckpointLoadResult) .
2282 (eliminate
2283 CheckpointBlocksValidationResult
2284 (lambda unrestricted current : (family CheckpointBlocksValidationResult) .
2285 (family CheckpointLoadResult))
2286 (checkpointValidateBlocks fields blocks)
2287 (branch
2288 CheckpointBlocksAccepted
2289 typedBlocks
2290 actualPayload
2291 validatedCount
2292 .
2293 (nat-eliminate
2294 (lambda unrestricted payloadMatched : Nat .
2295 (family CheckpointLoadResult))
2296 (constructor
2297 CheckpointLoadResult
2298 CheckpointLoadRejected
2299 (checkpointFailure
2300 (constructor
2301 CheckpointErrorCode
2302 CheckpointPayloadExtentMismatch)
2303 zero
2304 (dataBytesWord64LE expectedPayload)
2305 (dataBytesWord64LE actualPayload))
2306 (checkpointValidationTelemetry
2307 expectedCount
2308 actualCount
2309 validatedCount
2310 actualPayload
2311 canonicalBytes))
2312 (lambda unrestricted payloadPredecessor : Nat .
2313 (lambda unrestricted payloadInduction : (family CheckpointLoadResult) .
2314 (constructor
2315 CheckpointLoadResult
2316 CheckpointLoaded
2317 (constructor
2318 CheckpointTypedCheckpoint
2319 CheckpointTypedCheckpointValue
2320 policy
2321 image
2322 typedBlocks)
2323 (checkpointValidationTelemetry
2324 expectedCount
2325 actualCount
2326 validatedCount
2327 actualPayload
2328 canonicalBytes))))
2329 (modelWord64Equal expectedPayload actualPayload)))
2330 (branch
2331 CheckpointBlocksRejected
2332 failure
2333 payloadBytes
2334 validatedCount
2335 .
2336 (constructor
2337 CheckpointLoadResult
2338 CheckpointLoadRejected
2339 failure
2340 (checkpointValidationTelemetry
2341 expectedCount
2342 actualCount
2343 validatedCount
2344 payloadBytes
2345 canonicalBytes))))))
2346 (naturalEqual expectedCount actualCount))))
2347 (bytes-equal expectedDigest actualDigest)))
2348 (checkpointBlocksCount blocks)))
2349 (checkpointFieldsCount fields)))))))
2350 (branch
2351 CheckpointSchemaIdentityRejected
2352 failure
2353 canonicalBytes
2354 .
2355 (constructor
2356 CheckpointLoadResult
2357 CheckpointLoadRejected
2358 failure
2359 (checkpointValidationTelemetry zero zero zero modelWord64Zero canonicalBytes))))))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.