359def nativePeerPublicationAdmitted =
360 (lambda unrestricted publication : (family NativePeerRegionPublication) .
361 (lambda unrestricted available : Nat .
362 (lambda unrestricted role : Nat .
363 (eliminate
364 NativePeerRegionPublication
365 (lambda unrestricted current : (family NativePeerRegionPublication) . Nat)
366 publication
367 (branch
368 NativePeerRegionPublicationOf
369 plan
370 peers
371 capture
372 committed
373 connection
374 stateAt
375 stateBytes
376 agreed
377 ownerOf
378 offsetOf
379 paths
380 .
381 (naturalAnd
382 (naturalNonzero peers)
383 (naturalAnd
384 (naturalLessOrEqual role peers)
385 (naturalAnd
386 (naturalBelowTwoPower 64 available)
387 (naturalAnd
388 (nativePeerFramesShareStorage peers capture stateBytes)
389 (naturalAnd
390 (nativePeerFramesShareStorage peers committed nativeCheckpointWordBytes)
391 (naturalAnd
392 (naturalAnd
393 (naturalLess nativeRegionCaptureBytes stateBytes)
394 (naturalAnd
395 (naturalLessOrEqual nativeRegionCaptureBytes agreed)
396 (naturalLessOrEqual agreed stateBytes)))
397 (naturalAnd
398 (naturalEqual
399 (nativeRegionPathCountOf paths)
400 (stdListLength (family NativeRegionShard) (nativeRegionShards plan)))
401 (naturalAnd
402 (arenaCertificate
403 available
404 (constructor
405 ArenaResidents
406 ArenaResidentsNext
407 (constructor
408 ArenaResident
409 ArenaResidentValue
410 b"captured-local-state"
411 stateAt
412 stateBytes
413 nativeCheckpointWordBytes)
414 (constructor
415 ArenaResidents
416 ArenaResidentsNext
417 (constructor
418 ArenaResident
419 ArenaResidentValue
420 b"capture-frame"
421 (frameBase (capture 1))
422 (naturalSaturatingSubtract
423 (frameEnd (capture 1))
424 (frameBase (capture 1)))
425 1)
426 (constructor
427 ArenaResidents
428 ArenaResidentsNext
429 (constructor
430 ArenaResident
431 ArenaResidentValue
432 b"commit-frame"
433 (frameBase (committed 1))
434 (naturalSaturatingSubtract
435 (frameEnd (committed 1))
436 (frameBase (committed 1)))
437 1)
438 (nativeRegionResidents plan)))))
439 (stdListFold
440 (family NativeRegionShard)
441 Nat
442 (lambda unrestricted shard : (family NativeRegionShard) .
443 (lambda unrestricted rest : Nat .
444 (naturalAnd
445 rest
446 (naturalAnd
447 (naturalLessOrEqual (ownerOf shard) peers)
448 (nativePublicationSourceWithin
449 (offsetOf shard)
450 (intervalExtent (nativeRegionInterval shard))
451 0
452 stateBytes)))))
453 1
454 (nativeRegionShards plan)))))))))))))))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.