Runtime.NativePeerTree

1module Runtime.NativePeerTree
2
3import Representation.ParticipantTree
4import Runtime.NativePeerEndpoint
5import Data.Bytes
6import Std.Foundation
7import Std.List
8import Std.Natural
9
10-- A participant's edges in a bounded-fan-out hierarchy
11-- (Representation.ParticipantTree). Every non-root role has exactly one
12-- parent, so the edge (parent(c), c) is named by c and its address is
13-- `address c`. A role's edges are its parent (a lower role: this role
14-- connects) followed by its children in role order (higher roles: this role
15-- listens), which is the ascending order Runtime.NativePeerEndpoint requires.
16-- A participant holds at most fanout + 1 edges and never the membership of
17-- the whole hierarchy: its control state is bounded by the fan-out.
18def nativePeerTreeEdges =
19  (lambda unrestricted fanout : Nat .
20    (lambda unrestricted count : Nat .
21      (lambda unrestricted role : Nat .
22        (lambda unrestricted address : (pi unrestricted child : Nat . Bytes) .
23          (let unrestricted node =
24            (participantTreeNode fanout count role)
25            in
26            (let unrestricted children =
27              (stdListMap
28                (family ParticipantTreeNode)
29                (family NativePeerEdge)
30                (lambda unrestricted child : (family ParticipantTreeNode) .
31                  (constructor
32                    NativePeerEdge
33                    NativePeerEdgeOf
34                    (participantTreeRoleOf child)
35                    (address (participantTreeRoleOf child))))
36                (participantTreeChildren fanout node))
37              in
38              (nat-eliminate
39                (lambda unrestricted root : Nat . (family StdList (family NativePeerEdge)))
40                (constructor
41                  StdList
42                  StdListCons
43                  (family NativePeerEdge)
44                  (constructor
45                    NativePeerEdge
46                    NativePeerEdgeOf
47                    (participantTreeParentOf node)
48                    (address role))
49                  children)
50                (lambda unrestricted predecessor : Nat .
51                  (lambda unrestricted ignored : (family StdList (family NativePeerEdge)) .
52                    children))
53                (participantTreeIsRoot node))))))))
54
55-- The connection slot to this role's parent (its first edge).
56def nativePeerTreeParentConnection : Nat =
57  (nativePeerEdgeConnectionSlot 0)
58
59-- A tree is admitted for this role when the hierarchy admits it and its
60-- edges are admitted endpoints (distinct ascending peers, IPv4 addresses).
61def nativePeerTreeAdmitted =
62  (lambda unrestricted fanout : Nat .
63    (lambda unrestricted count : Nat .
64      (lambda unrestricted role : Nat .
65        (lambda unrestricted address : (pi unrestricted child : Nat . Bytes) .
66          (naturalAnd
67            (participantTreeAdmitted fanout count role)
68            (nativePeerEdgesAdmitted role (nativePeerTreeEdges fanout count role address)))))))
69
70-- The role's edges with addresses listed in the hierarchy's edge order
71-- (parent first unless root, then children in role order): the form a
72-- caller that compiles each role's own addresses supplies.
73def nativePeerTreeEdgesListed =
74  (lambda unrestricted fanout : Nat .
75    (lambda unrestricted owners : Nat .
76      (lambda unrestricted role : Nat .
77        (lambda unrestricted addresses : (family StdList Bytes) .
78          (stdListFold
79            (family NativePeerEdge)
80            (pi unrestricted index : Nat . (family StdList (family NativePeerEdge)))
81            (lambda unrestricted edge : (family NativePeerEdge) .
82              (lambda unrestricted next : (pi unrestricted index : Nat . (family StdList (family NativePeerEdge))) .
83                (lambda unrestricted index : Nat .
84                  (constructor
85                    StdList
86                    StdListCons
87                    (family NativePeerEdge)
88                    (constructor
89                      NativePeerEdge
90                      NativePeerEdgeOf
91                      (nativePeerEdgePeerOf edge)
92                      (stdListHeadOr Bytes b"" (stdListDrop Bytes index addresses)))
93                    (next (succ index))))))
94            (lambda unrestricted index : Nat .
95              (constructor StdList StdListEmpty (family NativePeerEdge)))
96            (nativePeerTreeEdges fanout owners role (lambda unrestricted child : Nat . b""))
97            0)))))
98
99def nativePeerTreeListedAdmitted =
100  (lambda unrestricted fanout : Nat .
101    (lambda unrestricted owners : Nat .
102      (lambda unrestricted role : Nat .
103        (lambda unrestricted addresses : (family StdList Bytes) .
104          (naturalAnd
105            (participantTreeAdmitted fanout owners role)
106            (naturalAnd
107              (naturalEqual
108                (stdListLength Bytes addresses)
109                (stdListLength
110                  (family NativePeerEdge)
111                  (nativePeerTreeEdges fanout owners role (lambda unrestricted child : Nat . b""))))
112              (nativePeerEdgesAdmitted
113                role
114                (nativePeerTreeEdgesListed fanout owners role addresses))))))))