ParticipantTreeLaws

1module ParticipantTreeLaws
2
3import Representation.ParticipantTree
4import Std.Foundation
5import Std.List
6import Std.Natural
7
8-- Hand-computed hierarchies (checked against an independent model of the
9-- same splitting rule). Each law is decided by normalization.
10-- Seven roles, fan-out two: 0 -> {1, 4}; 1 -> {2, 3}; 4 -> {5, 6}.
11def binaryRootChildren :
12  (equal
13    (family StdList Nat)
14    (stdListMap
15      (family ParticipantTreeNode)
16      Nat
17      participantTreeRoleOf
18      (participantTreeChildren 2 (participantTreeNode 2 7 0)))
19    (constructor
20      StdList
21      StdListCons
22      Nat
23      1
24      (constructor StdList StdListCons Nat 4 (constructor StdList StdListEmpty Nat)))) =
25  (refl
26    (family StdList Nat)
27    (constructor
28      StdList
29      StdListCons
30      Nat
31      1
32      (constructor StdList StdListCons Nat 4 (constructor StdList StdListEmpty Nat))))
33
34def binaryNodeThreeParent : (equal Nat (participantTreeParentOf (participantTreeNode 2 7 3)) 1) =
35  (refl Nat 1)
36
37def binaryNodeThreeDepth : (equal Nat (participantTreeDepthOf (participantTreeNode 2 7 3)) 2) =
38  (refl Nat 2)
39
40def binaryNodeOneSize : (equal Nat (participantTreeSizeOf (participantTreeNode 2 7 1)) 3) =
41  (refl Nat 3)
42
43def binaryHeight : (equal Nat (participantTreeHeight 2 7) 2) =
44  (refl Nat 2)
45
46-- Ten roles, fan-out four: the nine descendants split 3, 2, 2, 2.
47def quaternarySecondChildSize : (equal Nat (participantTreeChildSize 4 10 1) 2) =
48  (refl Nat 2)
49
50def quaternaryFirstChildSize : (equal Nat (participantTreeChildSize 4 10 0) 3) =
51  (refl Nat 3)
52
53def quaternaryNodeFiveParent :
54  (equal Nat (participantTreeParentOf (participantTreeNode 4 10 5)) 4) =
55  (refl Nat 4)
56
57def quaternaryNodeNineParent :
58  (equal Nat (participantTreeParentOf (participantTreeNode 4 10 9)) 8) =
59  (refl Nat 8)
60
61-- Children tile the node's range: the start after the last child is the end.
62def quaternaryTiling : (equal Nat (participantTreeChildStart 4 0 10 4) 10) =
63  (refl Nat 10)
64
65-- Fan-out one is a chain.
66def chainParent : (equal Nat (participantTreeParentOf (participantTreeNode 1 4 3)) 2) =
67  (refl Nat 2)
68
69def chainHeight : (equal Nat (participantTreeHeight 1 4) 3) =
70  (refl Nat 3)
71
72-- The PRD's fleet design point: 200,000 roles with fan-out 64 need three
73-- edge levels (64^2 < 200,000 <= 64^3). The root's 199,999 descendants split
74-- into 63 subtrees of 3,125 and one of 3,124; no padding roles exist.
75def fleetHeight : (equal Nat (participantTreeHeight 64 200000) 3) =
76  (refl Nat 3)
77
78def fleetRootChildren : (equal Nat (participantTreeChildCount 64 200000) 64) =
79  (refl Nat 64)
80
81def fleetFirstSubtree : (equal Nat (participantTreeChildSize 64 200000 0) 3125) =
82  (refl Nat 3125)
83
84def fleetLastSubtree : (equal Nat (participantTreeChildSize 64 200000 63) 3124) =
85  (refl Nat 3124)
86
87def fleetLastRoleParent :
88  (equal Nat (participantTreeParentOf (participantTreeNode 64 200000 199999)) 199952) =
89  (refl Nat 199952)
90
91def fleetLastRoleDepth :
92  (equal Nat (participantTreeDepthOf (participantTreeNode 64 200000 199999)) 3) =
93  (refl Nat 3)
94
95def fleetMiddleRoleParent :
96  (equal Nat (participantTreeParentOf (participantTreeNode 64 200000 100000)) 99953) =
97  (refl Nat 99953)
98
99def roleOutsideRefused : (equal Nat (participantTreeAdmitted 64 200000 200000) 0) =
100  (refl Nat 0)
101
102-- Ancestors, root first: role 3 of the seven-role binary tree descends 0, 1.
103def binaryAncestors :
104  (equal
105    (family StdList Nat)
106    (stdListMap
107      (family ParticipantTreeNode)
108      Nat
109      participantTreeRoleOf
110      (participantTreeAncestors 2 7 3))
111    (constructor
112      StdList
113      StdListCons
114      Nat
115      0
116      (constructor StdList StdListCons Nat 1 (constructor StdList StdListEmpty Nat)))) =
117  (refl
118    (family StdList Nat)
119    (constructor
120      StdList
121      StdListCons
122      Nat
123      0
124      (constructor StdList StdListCons Nat 1 (constructor StdList StdListEmpty Nat))))
125
126def rootHasNoAncestors :
127  (equal Nat (stdListLength (family ParticipantTreeNode) (participantTreeAncestors 2 7 0)) 0) =
128  (refl Nat 0)
129
130def fleetAncestorCount :
131  (equal
132    Nat
133    (stdListLength (family ParticipantTreeNode) (participantTreeAncestors 64 200000 199999))
134    3) =
135  (refl Nat 3)
136
137def main : Nat =
138  0