Combine storage (the sum, the assembly, this owner's offer and read
replica), then the edge frames, the tree checkpoint and the root's
replicated shard layouts, then the owner state.
494def dpotWithLayout =
495 (lambda unrestricted c : Nat .
496 (lambda unrestricted u : Nat .
497 (lambda unrestricted system : (family DataParallelSystem c u) .
498 (lambda unrestricted q : Nat .
499 (lambda unrestricted p : Nat .
500 (lambda unrestricted g : Nat .
501 (lambda unrestricted fanout : Nat .
502 (lambda unrestricted role : Nat .
503 (lambda unrestricted epoch : Nat .
504 (lambda unrestricted available : Nat .
505 (lambda unrestricted emit : (pi unrestricted layout : (family NativeDataParallelOwnedLayout) . (pi unrestricted tree : (family NativeDataParallelOwnedTreeLayout) . Bytes)) .
506 (let unrestricted digest =
507 (dpIdentityDigest c u system)
508 in
509 (let unrestricted contextDigest =
510 (dpoContextDigest c u system p digest)
511 in
512 (let unrestricted sum =
513 (dpPlacementFor c u system digest (dpotTopology fanout) role)
514 in
515 (let unrestricted assemble =
516 (dpoAssemblePlacementFor
517 c
518 u
519 system
520 digest
521 (dpotTopology fanout)
522 role
523 sum)
524 in
525 (let unrestricted gradients =
526 (dpoGradientsFor
527 c
528 u
529 system
530 g
531 digest
532 (dpotTopology fanout)
533 role
534 (dpoPublicationStart c u system p assemble))
535 in
536 (eliminate
537 StdResult
538 (lambda unrestricted result : (family StdResult (family RegionFrameLayoutFailure) (family RegionFrameLayout)) .
539 Bytes)
540 (planRegionFrameLayout
541 (dpotIdentity c u system digest q p 2 1 0)
542 (dpotCommitmentBytes c u system q p)
543 512
544 (dpoGradientsEnd
545 c
546 u
547 system
548 gradients
549 (dpoPublicationStart c u system p assemble))
550 available)
551 (branch StdFailure error . b"")
552 (branch
553 StdSuccess
554 commitment
555 .
556 (eliminate
557 StdResult
558 (lambda unrestricted result : (family StdResult (family RegionFrameLayoutFailure) (family RegionFrameLayout)) .
559 Bytes)
560 (planRegionFrameLayout
561 (dpotIdentity c u system digest q p 3 0 1)
562 dpWord
563 512
564 (frameAlign (frameEnd commitment))
565 available)
566 (branch StdFailure error . b"")
567 (branch
568 StdSuccess
569 release
570 .
571 (eliminate
572 StdResult
573 (lambda unrestricted result : (family StdResult (family NativeCheckpointFailure) (family NativeTreeCheckpoint)) .
574 Bytes)
575 (planNativeTreeCheckpoint
576 (dpoContext
577 c
578 u
579 system
580 q
581 p
582 (dpotTopology fanout)
583 contextDigest)
584 (dpoRegions c u system q)
585 fanout
586 (dpOwners c u system)
587 role
588 (dpotOwnOf c u system q p)
589 epoch
590 (frameAlign (frameEnd release))
591 available)
592 (branch StdFailure error . b"")
593 (branch
594 StdSuccess
595 checkpoint
596 .
597 (eliminate
598 StdResult
599 (lambda unrestricted result : (family StdResult (family NativeCheckpointFailure) (family NativeRegionCheckpoint)) .
600 Bytes)
601 (dpotPlanRootShards
602 c
603 u
604 system
605 contextDigest
606 q
607 p
608 fanout
609 role
610 checkpoint
611 available)
612 (branch StdFailure error . b"")
613 (branch
614 StdSuccess
615 root
616 .
617 (emit
618 (constructor
619 NativeDataParallelOwnedLayout
620 NativeDataParallelOwnedLayoutOf
621 sum
622 assemble
623 (nativeCheckpointAlign (nativeRegionEnd root))
624 (nativeTreeEpoch checkpoint)
625 digest
626 gradients)
627 (constructor
628 NativeDataParallelOwnedTreeLayout
629 NativeDataParallelOwnedTreeLayoutOf
630 commitment
631 release
632 checkpoint
633 root))))))))))))))))))))))))))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.