1module Representation.ParticipantTree
2
3import Std.Foundation
4import Std.List
5import Std.Natural
6
7-- A bounded-fan-out hierarchy over logical roles 0..count-1, numbered in
8-- preorder so that every subtree is one contiguous role range [role,
9-- role + size). Role 0 is the root. A node's descendants (its range minus
10-- itself) are split into at most `fanout` contiguous chunks whose sizes differ
11-- by at most one, larger chunks first; each chunk is one child's subtree and
12-- its first role is that child.
13--
14-- Why preorder ranges: a parent certifies its children's coverage with O(fan-
15-- out) checks -- consecutive child ranges must tile (role, role + size) -- so
16-- a checkpoint or collective rooted here never collects the complete
17-- membership or every shard descriptor at one participant
18-- (docs/multi-device-learning/22-fleet-scale.md, "Distributed checkpoint data,
19-- bounded publication metadata"). Locating a role descends one path from the
20-- root, so its cost is depth x fan-out, not the participant count.
21--
22-- These are logical roles. Which device holds a role, and whether a
23-- particular placement keeps parent and child in one failure domain, are
24-- separate decisions (Execution.ResourceGraph); this relation only fixes who
25-- exchanges with whom.
26family ParticipantTreeNode : Type 0
27constructor ParticipantTreeNodeOf
28-- the node's role: the first role of its subtree
29field unrestricted participantTreeRole : Nat
30-- roles in the subtree, the node included
31field unrestricted participantTreeSize : Nat
32-- the parent's role; the root names itself
33field unrestricted participantTreeParent : Nat
34-- edges from the root to this node
35field unrestricted participantTreeDepth : Nat
36
37end-family
38
39def participantTreeRoleOf =
40 (lambda unrestricted node : (family ParticipantTreeNode) .
41 (eliminate
42 ParticipantTreeNode
43 (lambda unrestricted current : (family ParticipantTreeNode) . Nat)
44 node
45 (branch ParticipantTreeNodeOf role size parent depth . role)))
46
47def participantTreeSizeOf =
48 (lambda unrestricted node : (family ParticipantTreeNode) .
49 (eliminate
50 ParticipantTreeNode
51 (lambda unrestricted current : (family ParticipantTreeNode) . Nat)
52 node
53 (branch ParticipantTreeNodeOf role size parent depth . size)))
54
55def participantTreeParentOf =
56 (lambda unrestricted node : (family ParticipantTreeNode) .
57 (eliminate
58 ParticipantTreeNode
59 (lambda unrestricted current : (family ParticipantTreeNode) . Nat)
60 node
61 (branch ParticipantTreeNodeOf role size parent depth . parent)))
62
63def participantTreeDepthOf =
64 (lambda unrestricted node : (family ParticipantTreeNode) .
65 (eliminate
66 ParticipantTreeNode
67 (lambda unrestricted current : (family ParticipantTreeNode) . Nat)
68 node
69 (branch ParticipantTreeNodeOf role size parent depth . depth)))
70
71-- The children of a node with `size` roles: min(fanout, size - 1).
72def participantTreeChildCount =
73 (lambda unrestricted fanout : Nat .
74 (lambda unrestricted size : Nat . (naturalMinimum fanout (naturalPredecessor size))))
75
76-- The size of child `index` (from 0): the descendants divided as evenly as
77-- possible, the remainder going to the first children.
78def participantTreeChildSize =
79 (lambda unrestricted fanout : Nat .
80 (lambda unrestricted size : Nat .
81 (lambda unrestricted index : Nat .
82 (let unrestricted below =
83 (naturalPredecessor size)
84 in
85 (let unrestricted children =
86 (participantTreeChildCount fanout size)
87 in
88 (naturalAdd
89 (naturalDivideUnchecked below children)
90 (naturalSelect (naturalLess index (naturalModuloUnchecked below children)) 1 0)))))))
91
92-- The first role of child `index`: the node, then every earlier child.
93def participantTreeChildStart =
94 (lambda unrestricted fanout : Nat .
95 (lambda unrestricted role : Nat .
96 (lambda unrestricted size : Nat .
97 (lambda unrestricted index : Nat .
98 (let unrestricted below =
99 (naturalPredecessor size)
100 in
101 (let unrestricted children =
102 (participantTreeChildCount fanout size)
103 in
104 (let unrestricted base =
105 (naturalDivideUnchecked below children)
106 in
107 (naturalAdd
108 (succ role)
109 (naturalAdd
110 (naturalMultiply index base)
111 (naturalMinimum index (naturalModuloUnchecked below children)))))))))))
112
113def participantTreeChildNode =
114 (lambda unrestricted fanout : Nat .
115 (lambda unrestricted node : (family ParticipantTreeNode) .
116 (lambda unrestricted index : Nat .
117 (constructor
118 ParticipantTreeNode
119 ParticipantTreeNodeOf
120 (participantTreeChildStart
121 fanout
122 (participantTreeRoleOf node)
123 (participantTreeSizeOf node)
124 index)
125 (participantTreeChildSize fanout (participantTreeSizeOf node) index)
126 (participantTreeRoleOf node)
127 (succ (participantTreeDepthOf node))))))
128
129def participantTreeRoot =
130 (lambda unrestricted count : Nat .
131 (constructor ParticipantTreeNode ParticipantTreeNodeOf 0 count 0 0))
132
133-- The index of the child whose range holds `target` (a descendant of node).
134def participantTreeChildHolding =
135 (lambda unrestricted fanout : Nat .
136 (lambda unrestricted node : (family ParticipantTreeNode) .
137 (lambda unrestricted target : Nat .
138 (stdListFold
139 Nat
140 Nat
141 (lambda unrestricted index : Nat .
142 (lambda unrestricted rest : Nat .
143 (naturalSelect
144 (naturalLess
145 target
146 (participantTreeChildStart
147 fanout
148 (participantTreeRoleOf node)
149 (participantTreeSizeOf node)
150 (succ index)))
151 index
152 rest)))
153 0
154 (stdListNaturalsBelow (participantTreeChildCount fanout (participantTreeSizeOf node)))))))
155
156-- Descend from `node` toward `target`, at most `fuel` edges. Fan-out of at
157-- least two bounds the depth by log2 of the count, so 64 levels cover every
158-- role a 64-bit count names; a chain (fan-out one) needs fuel = count.
159def participantTreeDescend =
160 (lambda unrestricted fanout : Nat .
161 (lambda unrestricted fuel : Nat .
162 (nat-eliminate
163 (lambda unrestricted remaining : Nat .
164 (pi unrestricted node : (family ParticipantTreeNode) .
165 (pi unrestricted target : Nat . (family ParticipantTreeNode))))
166 (lambda unrestricted node : (family ParticipantTreeNode) .
167 (lambda unrestricted target : Nat . node))
168 (lambda unrestricted previous : Nat .
169 (lambda unrestricted deeper : (pi unrestricted node : (family ParticipantTreeNode) . (pi unrestricted target : Nat . (family ParticipantTreeNode))) .
170 (lambda unrestricted node : (family ParticipantTreeNode) .
171 (lambda unrestricted target : Nat .
172 (nat-eliminate
173 (lambda unrestricted found : Nat . (family ParticipantTreeNode))
174 (deeper
175 (participantTreeChildNode
176 fanout
177 node
178 (participantTreeChildHolding fanout node target))
179 target)
180 (lambda unrestricted predecessor : Nat .
181 (lambda unrestricted ignored : (family ParticipantTreeNode) . node))
182 (naturalEqual (participantTreeRoleOf node) target))))))
183 fuel)))
184
185def participantTreeFuel =
186 (lambda unrestricted fanout : Nat .
187 (lambda unrestricted count : Nat . (naturalSelect (naturalLess fanout 2) count 64)))
188
189-- The node of `role`. Admission (participantTreeAdmitted) must hold.
190def participantTreeNode =
191 (lambda unrestricted fanout : Nat .
192 (lambda unrestricted count : Nat .
193 (lambda unrestricted role : Nat .
194 (participantTreeDescend
195 fanout
196 (participantTreeFuel fanout count)
197 (participantTreeRoot count)
198 role))))
199
200-- The node's children, as nodes, in role order.
201def participantTreeChildren =
202 (lambda unrestricted fanout : Nat .
203 (lambda unrestricted node : (family ParticipantTreeNode) .
204 (stdListMap
205 Nat
206 (family ParticipantTreeNode)
207 (participantTreeChildNode fanout node)
208 (stdListNaturalsBelow (participantTreeChildCount fanout (participantTreeSizeOf node))))))
209
210def participantTreeIsRoot =
211 (lambda unrestricted node : (family ParticipantTreeNode) .
212 (naturalIsZero (participantTreeDepthOf node)))
213
214-- A hierarchy exists for a nonempty count with a nonzero fan-out, and the
215-- role must be one of its participants.
216def participantTreeAdmitted =
217 (lambda unrestricted fanout : Nat .
218 (lambda unrestricted count : Nat .
219 (lambda unrestricted role : Nat .
220 (naturalAnd
221 (naturalNonzero fanout)
222 (naturalAnd (naturalNonzero count) (naturalLess role count))))))
223
224-- The deepest node: the largest subtree's chain of first children reaches it,
225-- because sizes are nonincreasing in child order.
226def participantTreeHeight =
227 (lambda unrestricted fanout : Nat .
228 (lambda unrestricted count : Nat .
229 (participantTreeDepthOf
230 (nat-eliminate
231 (lambda unrestricted remaining : Nat . (family ParticipantTreeNode))
232 (participantTreeRoot count)
233 (lambda unrestricted previous : Nat .
234 (lambda unrestricted node : (family ParticipantTreeNode) .
235 (nat-eliminate
236 (lambda unrestricted leaf : Nat . (family ParticipantTreeNode))
237 node
238 (lambda unrestricted predecessor : Nat .
239 (lambda unrestricted ignored : (family ParticipantTreeNode) .
240 (participantTreeChildNode fanout node 0)))
241 (naturalLess 1 (participantTreeSizeOf node)))))
242 (participantTreeFuel fanout count)))))
243
244-- The nodes from the root down to (excluding) `role`'s node: the ancestors
245-- a participant consults to verify that its own subtree is part of one
246-- published root, in root-first order. At most the hierarchy's height.
247def participantTreeAncestors =
248 (lambda unrestricted fanout : Nat .
249 (lambda unrestricted count : Nat .
250 (lambda unrestricted role : Nat .
251 (app
252 (nat-eliminate
253 (lambda unrestricted remaining : Nat .
254 (pi unrestricted node : (family ParticipantTreeNode) .
255 (family StdList (family ParticipantTreeNode))))
256 (lambda unrestricted node : (family ParticipantTreeNode) .
257 (constructor StdList StdListEmpty (family ParticipantTreeNode)))
258 (lambda unrestricted previous : Nat .
259 (lambda unrestricted deeper : (pi unrestricted node : (family ParticipantTreeNode) . (family StdList (family ParticipantTreeNode))) .
260 (lambda unrestricted node : (family ParticipantTreeNode) .
261 (nat-eliminate
262 (lambda unrestricted found : Nat .
263 (family StdList (family ParticipantTreeNode)))
264 (constructor
265 StdList
266 StdListCons
267 (family ParticipantTreeNode)
268 node
269 (deeper
270 (participantTreeChildNode
271 fanout
272 node
273 (participantTreeChildHolding fanout node role))))
274 (lambda unrestricted predecessor : Nat .
275 (lambda unrestricted ignored : (family StdList (family ParticipantTreeNode)) .
276 (constructor StdList StdListEmpty (family ParticipantTreeNode))))
277 (naturalEqual (participantTreeRoleOf node) role)))))
278 (participantTreeFuel fanout count))
279 (participantTreeRoot count)))))
280
281-- The index, among `node`'s children, of the child whose subtree holds `role`.
282def participantTreeChildIndex =
283 participantTreeChildHoldingThe compiler supplied declaration spans and resolved links from this source snapshot. This page does not assert that this file belongs to a checked closure.