First round uses the initialized version. Only later rounds rearm completed
slots, so finishing at u64 max does not require an impossible next version.
The up-front checked sum rejects an unrepresentable run before any transfer.
451def peerUpdatesWith =
452 (lambda unrestricted local : (pi unrestricted tail : (family NativePhysicalCommands) . (family NativePhysicalCommands)) .
453 (lambda unrestricted descriptor : (family NativePhysicalOperand) .
454 (lambda unrestricted worker : Nat .
455 (lambda unrestricted wrongMean : Nat .
456 (lambda unrestricted steps : Nat .
457 (lambda unrestricted epoch : (family NativePhysicalOperand) .
458 (lambda unrestricted version : (family NativePhysicalOperand) .
459 (lambda unrestricted initial : (family RegionFrameLayout) .
460 (lambda unrestricted contribution : (family RegionFrameLayout) .
461 (lambda unrestricted updated : (family RegionFrameLayout) .
462 (lambda unrestricted acknowledged : (family RegionFrameLayout) .
463 (lambda unrestricted work : Nat .
464 (lambda unrestricted finish : (family NativePhysicalCommands) .
465 (nativeCheckedWordAdd
466 (frameNativeState work)
467 version
468 (nativeLaunchRecipeImmediate steps)
469 0
470 b"peer-run-version-overflow"
471 (nat-eliminate
472 (lambda unrestricted count : Nat . (family NativePhysicalCommands))
473 finish
474 (lambda unrestricted previous : Nat .
475 (lambda unrestricted ignored : (family NativePhysicalCommands) .
476 (nativeCheckedWordAdd
477 (frameNativeState work)
478 version
479 (nativeLaunchRecipeImmediate 1)
480 0
481 b"peer-initial-version-overflow"
482 (nativeFrameInitializeRound
483 initial
484 epoch
485 version
486 (nativeFrameInitializeRound
487 contribution
488 epoch
489 version
490 (nativeFrameInitializeRound
491 updated
492 epoch
493 (frameNativeLoad work)
494 (nativeFrameInitializeRound
495 acknowledged
496 epoch
497 (frameNativeLoad work)
498 (peerRoundWith
499 local
500 descriptor
501 worker
502 wrongMean
503 initial
504 contribution
505 updated
506 acknowledged
507 work
508 (nativeLaunchRecipeCommand
509 (constructor
510 NativePhysicalOperation
511 NativePhysicalRepeatBeginCounted
512 (nativeLaunchRecipeImmediate previous))
513 b"peer-repeat"
514 (peerAdvance
515 worker
516 initial
517 contribution
518 updated
519 acknowledged
520 (peerRoundWith
521 local
522 descriptor
523 worker
524 wrongMean
525 initial
526 contribution
527 updated
528 acknowledged
529 work
530 (nativeLaunchRecipeCommand
531 (constructor
532 NativePhysicalOperation
533 NativePhysicalRepeatEnd)
534 b"peer-repeat-end"
535 finish))))))))))))
536 steps)))))))))))))))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.