Every edge's frames share the template's storage exactly.
702def dpotFramesAdmitted =
703 (lambda unrestricted c : Nat .
704 (lambda unrestricted u : Nat .
705 (lambda unrestricted system : (family DataParallelSystem c u) .
706 (lambda unrestricted digest : Bytes .
707 (lambda unrestricted q : Nat .
708 (lambda unrestricted p : Nat .
709 (lambda unrestricted fanout : Nat .
710 (lambda unrestricted tree : (family NativeDataParallelOwnedTreeLayout) .
711 (stdListFold
712 Nat
713 Nat
714 (lambda unrestricted index : Nat .
715 (lambda unrestricted rest : Nat .
716 (naturalAnd
717 rest
718 (naturalAnd
719 (naturalEqual
720 (frameEnd
721 (dpotCommitmentFor c u system digest q p fanout tree (succ index)))
722 (frameEnd (dpotCommitment tree)))
723 (naturalEqual
724 (frameEnd
725 (dpotReleaseFor c u system digest q p fanout tree (succ index)))
726 (frameEnd (dpotRelease tree)))))))
727 1
728 (stdListNaturalsBelow (naturalPredecessor (dpOwners c u system))))))))))))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.