argv for n owners (positions after the program name): 1 the previous root
manifest; 1 + r the previous group manifest of role r >= 1; n + 1 + r the
previous shard of role r; 2n + 1 + 2r and 2n + 2 + 2r the candidate and
committed group manifest of role r (role 0's is the published root);
4n + 1 + 2r and 4n + 2 + 2r role r's candidate and committed shard; 6n + 1
the generation directory. Every owner receives the same argv and reads
only its own entries and its ancestors'.
297def nitPaths =
298 (lambda unrestricted owners : Nat .
299 (lambda unrestricted role : Nat .
300 (let unrestricted groups =
301 (succ (naturalMultiply 2 owners))
302 in
303 (let unrestricted shards =
304 (succ (naturalMultiply 4 owners))
305 in
306 (constructor
307 NativeTreePaths
308 NativeTreePathsOf
309 (lambda unrestricted at : Nat . (succ at))
310 (lambda unrestricted index : Nat . (succ (naturalAdd owners role)))
311 (naturalAdd groups (naturalMultiply 2 role))
312 (succ (naturalAdd groups (naturalMultiply 2 role)))
313 (lambda unrestricted index : Nat . (naturalAdd shards (naturalMultiply 2 role)))
314 (lambda unrestricted index : Nat . (succ (naturalAdd shards (naturalMultiply 2 role))))
315 (succ (naturalMultiply 6 owners)))))))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.