ParticipantGroupLaws

1module ParticipantGroupLaws
2
3import Representation.ParticipantGroup
4import Std.Foundation
5import Std.Natural
6import Model.Parameter
7import Model.Word64
8import Data.Bytes
9
10def stride =
11  (lambda unrestricted first : Nat .
12    (lambda unrestricted step : Nat .
13      (lambda unrestricted count : Nat .
14        (constructor ParticipantSelection ParticipantStride first step count))))
15
16def repeat =
17  (lambda unrestricted count : Nat .
18    (lambda unrestricted step : Nat .
19      (lambda unrestricted inner : (family ParticipantSelection) .
20        (constructor ParticipantSelection ParticipantRepeat count step inner))))
21
22def join =
23  (lambda unrestricted left : (family ParticipantSelection) .
24    (lambda unrestricted right : (family ParticipantSelection) .
25      (constructor ParticipantSelection ParticipantJoin left right)))
26
27def group =
28  (lambda unrestricted selection : (family ParticipantSelection) .
29    (constructor ParticipantGroup ParticipantGroupOf 200000 3 b"fleet-members" selection))
30
31def regular =
32  (group (repeat 625 320 (repeat 8 40 (repeat 2 20 (stride 0 1 20)))))
33
34def fixedAxes =
35  (group (repeat 625 320 (stride 127 20 2)))
36
37def irregular =
38  (group (join (stride 0 2 3) (repeat 3 11 (stride 10 3 2))))
39
40def unequalCoverage =
41  (group (join (stride 0 1 131072) (stride 131072 1 68928)))
42
43def failureCode =
44  (lambda unrestricted failure : (family ParticipantGroupFailure) .
45    (eliminate
46      ParticipantGroupFailure
47      (lambda unrestricted current : (family ParticipantGroupFailure) . Nat)
48      failure
49      (branch ParticipantEmptyIdentity . 1)
50      (branch ParticipantUniverseBounds . 2)
51      (branch ParticipantEpochBounds . 3)
52      (branch ParticipantEmptySelection . 4)
53      (branch ParticipantZeroStride . 5)
54      (branch ParticipantCoordinateOverflow . 6)
55      (branch ParticipantRepeatedOverlap . 7)
56      (branch ParticipantUnorderedJoin . 8)
57      (branch ParticipantOutsideUniverse . 9)
58      (branch ParticipantIndexBudget . 10)))
59
60def verdict =
61  (lambda unrestricted group : (family ParticipantGroup) .
62    (lambda unrestricted nodes : Nat .
63      (lambda unrestricted depth : Nat .
64        (eliminate
65          StdResult
66          (lambda unrestricted result : (family StdResult (family ParticipantGroupFailure) (family ParticipantIndex)) .
67            Nat)
68          (participantAdmit group nodes depth)
69          (branch StdFailure reason . (failureCode reason))
70          (branch StdSuccess index . 0)))))
71
72-- These probes consume the admitted index. The result 0 distinguishes refusal
73-- or an absent ordinal; present role r encodes as r+1, including role zero.
74def member =
75  (lambda unrestricted group : (family ParticipantGroup) .
76    (lambda unrestricted ordinal : Nat .
77      (eliminate
78        StdResult
79        (lambda unrestricted result : (family StdResult (family ParticipantGroupFailure) (family ParticipantIndex)) .
80          Nat)
81        (participantAdmit group 16 8)
82        (branch StdFailure reason . 0)
83        (branch
84          StdSuccess
85          index
86          .
87          (eliminate
88            StdOption
89            (lambda unrestricted value : (family StdOption Nat) . Nat)
90            (participantMember index ordinal)
91            (branch StdNone . 0)
92            (branch StdSome role . (naturalAdd role 1)))))))
93
94def count =
95  (lambda unrestricted group : (family ParticipantGroup) .
96    (eliminate
97      StdResult
98      (lambda unrestricted result : (family StdResult (family ParticipantGroupFailure) (family ParticipantIndex)) .
99        Nat)
100      (participantAdmit group 16 8)
101      (branch StdFailure reason . 0)
102      (branch StdSuccess index . (participantCountOf index))))
103
104def contains =
105  (lambda unrestricted group : (family ParticipantGroup) .
106    (lambda unrestricted role : Nat .
107      (eliminate
108        StdResult
109        (lambda unrestricted result : (family StdResult (family ParticipantGroupFailure) (family ParticipantIndex)) .
110          Nat)
111        (participantAdmit group 16 8)
112        (branch StdFailure reason . 0)
113        (branch StdSuccess index . (participantContains index role)))))
114
115def summary =
116  (lambda unrestricted group : (family ParticipantGroup) .
117    (eliminate
118      StdResult
119      (lambda unrestricted result : (family StdResult (family ParticipantGroupFailure) (family ParticipantIndex)) .
120        Bytes)
121      (participantAdmit group 16 8)
122      (branch StdFailure reason . b"")
123      (branch
124        StdSuccess
125        index
126        .
127        (bytes-append
128          (participantWord (participantCountOf index))
129          (bytes-append
130            (participantWord (participantNodesOf index))
131            (bytes-append
132              (participantWord (participantDepthOf index))
133              (bytes-append
134                (participantWord (participantLowerOf index))
135                (participantWord (participantUpperOf index)))))))))
136
137def regularAdmitted : (equal Nat (verdict regular 4 4) 0) =
138  (refl Nat 0)
139
140def regularCount : (equal Nat (count regular) 200000) =
141  (refl Nat 200000)
142
143def regularFirst : (equal Nat (member regular 0) 1) =
144  (refl Nat 1)
145
146def regularLast : (equal Nat (member regular 199999) 200000) =
147  (refl Nat 200000)
148
149def regularOutside : (equal Nat (member regular 200000) 0) =
150  (refl Nat 0)
151
152def fixedCount : (equal Nat (count fixedAxes) 1250) =
153  (refl Nat 1250)
154
155def fixedFirst : (equal Nat (member fixedAxes 0) 128) =
156  (refl Nat 128)
157
158def fixedInner : (equal Nat (member fixedAxes 1) 148) =
159  (refl Nat 148)
160
161def fixedNext : (equal Nat (member fixedAxes 2) 448) =
162  (refl Nat 448)
163
164def fixedLast : (equal Nat (member fixedAxes 1249) 199828) =
165  (refl Nat 199828)
166
167def fixedGap : (equal Nat (contains fixedAxes 128) 0) =
168  (refl Nat 0)
169
170def fixedPresent : (equal Nat (contains fixedAxes 147) 1) =
171  (refl Nat 1)
172
173def irregularCount : (equal Nat (count irregular) 9) =
174  (refl Nat 9)
175
176def irregularLast : (equal Nat (member irregular 8) 36) =
177  (refl Nat 36)
178
179def irregularMiddle : (equal Nat (member irregular 5) 22) =
180  (refl Nat 22)
181
182def irregularGap : (equal Nat (contains irregular 23) 0) =
183  (refl Nat 0)
184
185def irregularPresent : (equal Nat (contains irregular 24) 1) =
186  (refl Nat 1)
187
188def irregularJoinGap : (equal Nat (contains irregular 6) 0) =
189  (refl Nat 0)
190
191def unequalCount : (equal Nat (count unequalCoverage) 200000) =
192  (refl Nat 200000)
193
194def unequalBoundary : (equal Nat (member unequalCoverage 131072) 131073) =
195  (refl Nat 131073)
196
197def unequalLast : (equal Nat (member unequalCoverage 199999) 200000) =
198  (refl Nat 200000)
199
200def nodeBudget : (equal Nat (verdict regular 3 4) 10) =
201  (refl Nat 10)
202
203def depthBudget : (equal Nat (verdict regular 4 3) 10) =
204  (refl Nat 10)
205
206def emptyRefused : (equal Nat (verdict (group (stride 0 1 0)) 16 8) 4) =
207  (refl Nat 4)
208
209def zeroStride : (equal Nat (verdict (group (stride 0 0 1)) 16 8) 5) =
210  (refl Nat 5)
211
212def wrappedStride : (equal Nat (verdict (group (stride 0 18446744073709551616 1)) 16 8) 5) =
213  (refl Nat 5)
214
215def repeatedOverlap : (equal Nat (verdict (group (repeat 2 20 (stride 0 20 2))) 16 8) 7) =
216  (refl Nat 7)
217
218def repeatedStrideOverflow :
219  (equal Nat (verdict (group (repeat 1 18446744073709551616 (stride 0 1 1))) 16 8) 7) =
220  (refl Nat 7)
221
222def joinOverlap : (equal Nat (verdict (group (join (stride 0 1 2) (stride 1 1 2))) 16 8) 8) =
223  (refl Nat 8)
224
225def outsideUniverse : (equal Nat (verdict (group (stride 199999 1 2)) 16 8) 9) =
226  (refl Nat 9)
227
228def coordinateOverflow : (equal Nat (verdict (group (stride 18446744073709551615 1 2)) 16 8) 6) =
229  (refl Nat 6)
230
231def wrongIdentity :
232  (equal
233    Nat
234    (verdict (constructor ParticipantGroup ParticipantGroupOf 200000 0 b"" (stride 0 1 1)) 16 8)
235    1) =
236  (refl Nat 1)
237
238def epochOverflow :
239  (equal
240    Nat
241    (verdict
242      (constructor
243        ParticipantGroup
244        ParticipantGroupOf
245        200000
246        18446744073709551616
247        b"members"
248        (stride 0 1 1))
249      16
250      8)
251    3) =
252  (refl Nat 3)
253
254def universeZero :
255  (equal
256    Nat
257    (verdict (constructor ParticipantGroup ParticipantGroupOf 0 0 b"members" (stride 0 1 1)) 16 8)
258    2) =
259  (refl Nat 2)
260
261def main : Nat =
262  0