Plan this role's group manifest, its own shards and its ancestors' group
manifests, in that order from `base`. `ownOf role` gives a role's own
partition (the regions and intervals it holds); every participant derives
every ancestor's contract from it and the hierarchy, never from a peer.
Memory is the role's own shards plus at most height + 1 manifests of at
most fan-out + own records each: independent of the participant count.
362def planNativeTreeAncestors =
363 (lambda unrestricted context : (family CheckpointEnvelopeContract) .
364 (lambda unrestricted logical : Bytes .
365 (lambda unrestricted fanout : Nat .
366 (lambda unrestricted count : Nat .
367 (lambda unrestricted ownOf : (pi unrestricted role : Nat . (family StdList (family CheckpointRegionPartition))) .
368 (lambda unrestricted available : Nat .
369 (lambda unrestricted ancestors : (family StdList (family ParticipantTreeNode)) .
370 (lambda unrestricted finish : (pi unrestricted at : Nat . (pi unrestricted planned : (family StdList (family NativeCheckpointLayout)) . (family StdResult (family NativeCheckpointFailure) (family NativeTreeCheckpoint)))) .
371 (stdListFold
372 (family ParticipantTreeNode)
373 (pi unrestricted at : Nat .
374 (pi unrestricted planned : (family StdList (family NativeCheckpointLayout)) .
375 (family
376 StdResult
377 (family NativeCheckpointFailure)
378 (family NativeTreeCheckpoint))))
379 (lambda unrestricted ancestor : (family ParticipantTreeNode) .
380 (lambda unrestricted next : (pi unrestricted at : Nat . (pi unrestricted planned : (family StdList (family NativeCheckpointLayout)) . (family StdResult (family NativeCheckpointFailure) (family NativeTreeCheckpoint)))) .
381 (lambda unrestricted at : Nat .
382 (lambda unrestricted planned : (family StdList (family NativeCheckpointLayout)) .
383 (eliminate
384 StdResult
385 (lambda unrestricted result : (family StdResult (family NativeCheckpointFailure) (family NativeCheckpointLayout)) .
386 (family
387 StdResult
388 (family NativeCheckpointFailure)
389 (family NativeTreeCheckpoint)))
390 (planNativeTreeGroup
391 context
392 logical
393 fanout
394 count
395 ancestor
396 (ownOf (participantTreeRoleOf ancestor))
397 at
398 available)
399 (branch
400 StdFailure
401 error
402 .
403 (constructor
404 StdResult
405 StdFailure
406 (family NativeCheckpointFailure)
407 (family NativeTreeCheckpoint)
408 error))
409 (branch
410 StdSuccess
411 layout
412 .
413 (next
414 (nativeCheckpointAlign (nativeCheckpointEnd layout))
415 (stdListAppend
416 (family NativeCheckpointLayout)
417 planned
418 (constructor
419 StdList
420 StdListCons
421 (family NativeCheckpointLayout)
422 layout
423 (constructor
424 StdList
425 StdListEmpty
426 (family NativeCheckpointLayout)))))))))))
427 finish
428 ancestors)))))))))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.