1module Representation.ParticipantGroup
2
3import Std.Foundation
4import Std.Natural
5import Data.Bytes
6import Model.Word64
7import Data.SHA256
8import Data.SHA256Digest
9import Data.SHA256Padding
10
11-- Membership is a coordinate relation, independent of device capability and
12-- numerical evaluation order. Repetition shares one subgroup description;
13-- joining ordered, disjoint ranges indexes irregular populations. These are
14-- logical role IDs, not a claim that any physical devices executed.
15family ParticipantSelection : Type 0
16constructor ParticipantStride
17field unrestricted participantFirst : Nat
18field unrestricted participantStride : Nat
19field unrestricted participantCount : Nat
20constructor ParticipantRepeat
21field unrestricted participantRepeats : Nat
22field unrestricted participantRepeatStride : Nat
23recursive unrestricted participantRepeatedSelection
24constructor ParticipantJoin
25recursive unrestricted participantLeftSelection
26recursive unrestricted participantRightSelection
27
28end-family
29
30family ParticipantGroup : Type 0
31constructor ParticipantGroupOf
32field unrestricted participantUniverse : Nat
33field unrestricted participantEpoch : Nat
34field unrestricted participantIdentity : Bytes
35field unrestricted participantSelection : (family ParticipantSelection)
36
37end-family
38
39family ParticipantBounds : Type 0
40constructor ParticipantBoundsOf
41field unrestricted participantLower : Nat
42field unrestricted participantUpper : Nat
43field unrestricted participantCardinality : Nat
44field unrestricted participantIndexNodes : Nat
45field unrestricted participantIndexDepth : Nat
46
47end-family
48
49-- Derived caches belong to the admitted compiler index. The unchecked selectors
50-- below must consume participantAdmit's result; arbitrary hand-built indexes
51-- are not certificates. A worker retains only its projected roles/edges, not
52-- this entire index. Lookup follows one structural path, never a rank list.
53family ParticipantIndex : Type 0
54constructor ParticipantStrideIndex
55field unrestricted participantStrideBounds : (family ParticipantBounds)
56field unrestricted participantIndexStride : Nat
57constructor ParticipantRepeatIndex
58field unrestricted participantRepeatBounds : (family ParticipantBounds)
59field unrestricted participantIndexRepeatStride : Nat
60recursive unrestricted participantInnerIndex
61constructor ParticipantJoinIndex
62field unrestricted participantJoinBounds : (family ParticipantBounds)
63recursive unrestricted participantLeftIndex
64recursive unrestricted participantRightIndex
65
66end-family
67
68family ParticipantGroupFailure : Type 0
69constructor ParticipantEmptyIdentity
70constructor ParticipantUniverseBounds
71constructor ParticipantEpochBounds
72constructor ParticipantEmptySelection
73constructor ParticipantZeroStride
74constructor ParticipantCoordinateOverflow
75constructor ParticipantRepeatedOverlap
76constructor ParticipantUnorderedJoin
77constructor ParticipantOutsideUniverse
78constructor ParticipantIndexBudget
79
80end-family
81
82-- Cardinalities and encoded identities use unsigned 64-bit words. Arithmetic
83-- is checked as mathematical Nat before any fixed-width identity is emitted.
84def participantWordLimit =
85 18446744073709551615
86
87def participantRequire =
88 (lambda erased value : Type 0 .
89 (lambda unrestricted condition : Nat .
90 (lambda unrestricted failure : (family ParticipantGroupFailure) .
91 (lambda unrestricted next : (family StdResult (family ParticipantGroupFailure) value) .
92 (nat-eliminate
93 (lambda unrestricted flag : Nat .
94 (family StdResult (family ParticipantGroupFailure) value))
95 (constructor StdResult StdFailure (family ParticipantGroupFailure) value failure)
96 (lambda unrestricted prior : Nat .
97 (lambda unrestricted ignored : (family StdResult (family ParticipantGroupFailure) value) .
98 next))
99 condition)))))
100
101def participantBoundsLower =
102 (lambda unrestricted bounds : (family ParticipantBounds) .
103 (eliminate
104 ParticipantBounds
105 (lambda unrestricted current : (family ParticipantBounds) . Nat)
106 bounds
107 (branch ParticipantBoundsOf lower upper count nodes depth . lower)))
108
109def participantBoundsUpper =
110 (lambda unrestricted bounds : (family ParticipantBounds) .
111 (eliminate
112 ParticipantBounds
113 (lambda unrestricted current : (family ParticipantBounds) . Nat)
114 bounds
115 (branch ParticipantBoundsOf lower upper count nodes depth . upper)))
116
117def participantBoundsOf =
118 (lambda unrestricted index : (family ParticipantIndex) .
119 (eliminate
120 ParticipantIndex
121 (lambda unrestricted current : (family ParticipantIndex) . (family ParticipantBounds))
122 index
123 (branch ParticipantStrideIndex bounds stride . bounds)
124 (branch ParticipantRepeatIndex bounds stride inner induction . bounds)
125 (branch ParticipantJoinIndex bounds left right leftResult rightResult . bounds)))
126
127def participantLowerOf =
128 (lambda unrestricted index : (family ParticipantIndex) .
129 (eliminate
130 ParticipantBounds
131 (lambda unrestricted current : (family ParticipantBounds) . Nat)
132 (participantBoundsOf index)
133 (branch ParticipantBoundsOf lower upper count nodes depth . lower)))
134
135def participantUpperOf =
136 (lambda unrestricted index : (family ParticipantIndex) .
137 (eliminate
138 ParticipantBounds
139 (lambda unrestricted current : (family ParticipantBounds) . Nat)
140 (participantBoundsOf index)
141 (branch ParticipantBoundsOf lower upper count nodes depth . upper)))
142
143def participantCountOf =
144 (lambda unrestricted index : (family ParticipantIndex) .
145 (eliminate
146 ParticipantBounds
147 (lambda unrestricted current : (family ParticipantBounds) . Nat)
148 (participantBoundsOf index)
149 (branch ParticipantBoundsOf lower upper count nodes depth . count)))
150
151def participantNodesOf =
152 (lambda unrestricted index : (family ParticipantIndex) .
153 (eliminate
154 ParticipantBounds
155 (lambda unrestricted current : (family ParticipantBounds) . Nat)
156 (participantBoundsOf index)
157 (branch ParticipantBoundsOf lower upper count nodes depth . nodes)))
158
159def participantDepthOf =
160 (lambda unrestricted index : (family ParticipantIndex) .
161 (eliminate
162 ParticipantBounds
163 (lambda unrestricted current : (family ParticipantBounds) . Nat)
164 (participantBoundsOf index)
165 (branch ParticipantBoundsOf lower upper count nodes depth . depth)))
166
167def participantUniverseOf =
168 (lambda unrestricted group : (family ParticipantGroup) .
169 (eliminate
170 ParticipantGroup
171 (lambda unrestricted current : (family ParticipantGroup) . Nat)
172 group
173 (branch ParticipantGroupOf universe epoch identity selection . universe)))
174
175def participantEpochOf =
176 (lambda unrestricted group : (family ParticipantGroup) .
177 (eliminate
178 ParticipantGroup
179 (lambda unrestricted current : (family ParticipantGroup) . Nat)
180 group
181 (branch ParticipantGroupOf universe epoch identity selection . epoch)))
182
183def participantIdentityOf =
184 (lambda unrestricted group : (family ParticipantGroup) .
185 (eliminate
186 ParticipantGroup
187 (lambda unrestricted current : (family ParticipantGroup) . Bytes)
188 group
189 (branch ParticipantGroupOf universe epoch identity selection . identity)))
190
191def participantSelectionOf =
192 (lambda unrestricted group : (family ParticipantGroup) .
193 (eliminate
194 ParticipantGroup
195 (lambda unrestricted current : (family ParticipantGroup) . (family ParticipantSelection))
196 group
197 (branch ParticipantGroupOf universe epoch identity selection . selection)))
198
199def participantCompileStride =
200 (lambda unrestricted first : Nat .
201 (lambda unrestricted stride : Nat .
202 (lambda unrestricted count : Nat .
203 (participantRequire
204 (family ParticipantIndex)
205 (naturalNonzero count)
206 (constructor ParticipantGroupFailure ParticipantEmptySelection)
207 (participantRequire
208 (family ParticipantIndex)
209 (naturalAnd (naturalNonzero stride) (naturalLessOrEqual stride participantWordLimit))
210 (constructor ParticipantGroupFailure ParticipantZeroStride)
211 (let unrestricted last =
212 (naturalAdd first (naturalMultiply (naturalSaturatingSubtract count 1) stride))
213 in
214 (participantRequire
215 (family ParticipantIndex)
216 (naturalAnd
217 (naturalLessOrEqual count participantWordLimit)
218 (naturalLessOrEqual last participantWordLimit))
219 (constructor ParticipantGroupFailure ParticipantCoordinateOverflow)
220 (constructor
221 StdResult
222 StdSuccess
223 (family ParticipantGroupFailure)
224 (family ParticipantIndex)
225 (constructor
226 ParticipantIndex
227 ParticipantStrideIndex
228 (constructor ParticipantBounds ParticipantBoundsOf first last count 1 1)
229 stride)))))))))
230
231def participantCompileRepeat =
232 (lambda unrestricted count : Nat .
233 (lambda unrestricted stride : Nat .
234 (lambda unrestricted inner : (family ParticipantIndex) .
235 (participantRequire
236 (family ParticipantIndex)
237 (naturalNonzero count)
238 (constructor ParticipantGroupFailure ParticipantEmptySelection)
239 (participantRequire
240 (family ParticipantIndex)
241 (naturalAnd
242 (naturalLessOrEqual stride participantWordLimit)
243 (naturalLess
244 (naturalSaturatingSubtract (participantUpperOf inner) (participantLowerOf inner))
245 stride))
246 (constructor ParticipantGroupFailure ParticipantRepeatedOverlap)
247 (let unrestricted last =
248 (naturalAdd
249 (participantUpperOf inner)
250 (naturalMultiply (naturalSaturatingSubtract count 1) stride))
251 in
252 (let unrestricted size =
253 (naturalMultiply count (participantCountOf inner))
254 in
255 (participantRequire
256 (family ParticipantIndex)
257 (naturalAnd
258 (naturalLessOrEqual last participantWordLimit)
259 (naturalLessOrEqual size participantWordLimit))
260 (constructor ParticipantGroupFailure ParticipantCoordinateOverflow)
261 (constructor
262 StdResult
263 StdSuccess
264 (family ParticipantGroupFailure)
265 (family ParticipantIndex)
266 (constructor
267 ParticipantIndex
268 ParticipantRepeatIndex
269 (constructor
270 ParticipantBounds
271 ParticipantBoundsOf
272 (participantLowerOf inner)
273 last
274 size
275 (naturalAdd 1 (participantNodesOf inner))
276 (naturalAdd 1 (participantDepthOf inner)))
277 stride
278 inner))))))))))
279
280def participantCompileJoin =
281 (lambda unrestricted left : (family ParticipantIndex) .
282 (lambda unrestricted right : (family ParticipantIndex) .
283 (participantRequire
284 (family ParticipantIndex)
285 (naturalLess (participantUpperOf left) (participantLowerOf right))
286 (constructor ParticipantGroupFailure ParticipantUnorderedJoin)
287 (let unrestricted size =
288 (naturalAdd (participantCountOf left) (participantCountOf right))
289 in
290 (participantRequire
291 (family ParticipantIndex)
292 (naturalLessOrEqual size participantWordLimit)
293 (constructor ParticipantGroupFailure ParticipantCoordinateOverflow)
294 (constructor
295 StdResult
296 StdSuccess
297 (family ParticipantGroupFailure)
298 (family ParticipantIndex)
299 (constructor
300 ParticipantIndex
301 ParticipantJoinIndex
302 (constructor
303 ParticipantBounds
304 ParticipantBoundsOf
305 (participantLowerOf left)
306 (participantUpperOf right)
307 size
308 (naturalAdd 1 (naturalAdd (participantNodesOf left) (participantNodesOf right)))
309 (naturalAdd
310 1
311 (naturalSelect
312 (naturalLess (participantDepthOf left) (participantDepthOf right))
313 (participantDepthOf right)
314 (participantDepthOf left))))
315 left
316 right)))))))
317
318def participantCompileSelection =
319 (lambda unrestricted selection : (family ParticipantSelection) .
320 (eliminate
321 ParticipantSelection
322 (lambda unrestricted current : (family ParticipantSelection) .
323 (family StdResult (family ParticipantGroupFailure) (family ParticipantIndex)))
324 selection
325 (branch ParticipantStride first stride count . (participantCompileStride first stride count))
326 (branch
327 ParticipantRepeat
328 count
329 stride
330 inner
331 induction
332 .
333 (stdResultBind
334 (family ParticipantGroupFailure)
335 (family ParticipantIndex)
336 (family ParticipantIndex)
337 induction
338 (lambda unrestricted indexed : (family ParticipantIndex) .
339 (participantCompileRepeat count stride indexed))))
340 (branch
341 ParticipantJoin
342 left
343 right
344 leftResult
345 rightResult
346 .
347 (stdResultBind
348 (family ParticipantGroupFailure)
349 (family ParticipantIndex)
350 (family ParticipantIndex)
351 leftResult
352 (lambda unrestricted leftIndex : (family ParticipantIndex) .
353 (stdResultBind
354 (family ParticipantGroupFailure)
355 (family ParticipantIndex)
356 (family ParticipantIndex)
357 rightResult
358 (lambda unrestricted rightIndex : (family ParticipantIndex) .
359 (participantCompileJoin leftIndex rightIndex))))))))
360
361-- Admission is linear in the compact description, not its cardinality.
362-- A budget limits index structure and lookup depth, not the number of roles.
363-- Empty, overlapping, wrapped or padded membership never enters a plan.
364def participantAdmit =
365 (lambda unrestricted group : (family ParticipantGroup) .
366 (lambda unrestricted nodeBudget : Nat .
367 (lambda unrestricted depthBudget : Nat .
368 (participantRequire
369 (family ParticipantIndex)
370 (naturalNonzero (bytes-length (participantIdentityOf group)))
371 (constructor ParticipantGroupFailure ParticipantEmptyIdentity)
372 (participantRequire
373 (family ParticipantIndex)
374 (naturalAnd
375 (naturalNonzero (participantUniverseOf group))
376 (naturalLessOrEqual (participantUniverseOf group) participantWordLimit))
377 (constructor ParticipantGroupFailure ParticipantUniverseBounds)
378 (participantRequire
379 (family ParticipantIndex)
380 (naturalLessOrEqual (participantEpochOf group) participantWordLimit)
381 (constructor ParticipantGroupFailure ParticipantEpochBounds)
382 (stdResultBind
383 (family ParticipantGroupFailure)
384 (family ParticipantIndex)
385 (family ParticipantIndex)
386 (participantCompileSelection (participantSelectionOf group))
387 (lambda unrestricted indexed : (family ParticipantIndex) .
388 (participantRequire
389 (family ParticipantIndex)
390 (naturalLess (participantUpperOf indexed) (participantUniverseOf group))
391 (constructor ParticipantGroupFailure ParticipantOutsideUniverse)
392 (participantRequire
393 (family ParticipantIndex)
394 (naturalAnd
395 (naturalLessOrEqual (participantNodesOf indexed) nodeBudget)
396 (naturalLessOrEqual (participantDepthOf indexed) depthBudget))
397 (constructor ParticipantGroupFailure ParticipantIndexBudget)
398 (constructor
399 StdResult
400 StdSuccess
401 (family ParticipantGroupFailure)
402 (family ParticipantIndex)
403 indexed)))))))))))
404
405def participantSelectUnchecked =
406 (lambda unrestricted index : (family ParticipantIndex) .
407 (eliminate
408 ParticipantIndex
409 (lambda unrestricted current : (family ParticipantIndex) .
410 (pi unrestricted ordinal : Nat . Nat))
411 index
412 (branch
413 ParticipantStrideIndex
414 bounds
415 stride
416 .
417 (lambda unrestricted ordinal : Nat .
418 (naturalAdd (participantBoundsLower bounds) (naturalMultiply ordinal stride))))
419 (branch
420 ParticipantRepeatIndex
421 bounds
422 stride
423 inner
424 induction
425 .
426 (lambda unrestricted ordinal : Nat .
427 (naturalAdd
428 (naturalMultiply (naturalDivideUnchecked ordinal (participantCountOf inner)) stride)
429 (induction (naturalModuloUnchecked ordinal (participantCountOf inner))))))
430 (branch
431 ParticipantJoinIndex
432 bounds
433 left
434 right
435 leftResult
436 rightResult
437 .
438 (lambda unrestricted ordinal : Nat .
439 (nat-eliminate
440 (lambda unrestricted flag : Nat . Nat)
441 (rightResult (naturalSaturatingSubtract ordinal (participantCountOf left)))
442 (lambda unrestricted prior : Nat .
443 (lambda unrestricted ignored : Nat . (leftResult ordinal)))
444 (naturalLess ordinal (participantCountOf left)))))))
445
446def participantMember =
447 (lambda unrestricted index : (family ParticipantIndex) .
448 (lambda unrestricted ordinal : Nat .
449 (nat-eliminate
450 (lambda unrestricted flag : Nat . (family StdOption Nat))
451 (constructor StdOption StdNone Nat)
452 (lambda unrestricted prior : Nat .
453 (lambda unrestricted ignored : (family StdOption Nat) .
454 (constructor StdOption StdSome Nat (participantSelectUnchecked index ordinal))))
455 (naturalLess ordinal (participantCountOf index)))))
456
457def participantContains =
458 (lambda unrestricted index : (family ParticipantIndex) .
459 (eliminate
460 ParticipantIndex
461 (lambda unrestricted current : (family ParticipantIndex) . (pi unrestricted role : Nat . Nat))
462 index
463 (branch
464 ParticipantStrideIndex
465 bounds
466 stride
467 .
468 (lambda unrestricted role : Nat .
469 (naturalAnd
470 (naturalLessOrEqual (participantBoundsLower bounds) role)
471 (naturalAnd
472 (naturalLessOrEqual role (participantBoundsUpper bounds))
473 (naturalIsZero
474 (naturalModuloUnchecked
475 (naturalSaturatingSubtract role (participantBoundsLower bounds))
476 stride))))))
477 (branch
478 ParticipantRepeatIndex
479 bounds
480 stride
481 inner
482 induction
483 .
484 (lambda unrestricted role : Nat .
485 (naturalAnd
486 (naturalLessOrEqual (participantBoundsLower bounds) role)
487 (naturalAnd
488 (naturalLessOrEqual role (participantBoundsUpper bounds))
489 (induction
490 (naturalAdd
491 (participantLowerOf inner)
492 (naturalModuloUnchecked
493 (naturalSaturatingSubtract role (participantBoundsLower bounds))
494 stride)))))))
495 (branch
496 ParticipantJoinIndex
497 bounds
498 left
499 right
500 leftResult
501 rightResult
502 .
503 (lambda unrestricted role : Nat .
504 (nat-eliminate
505 (lambda unrestricted flag : Nat . Nat)
506 (rightResult role)
507 (lambda unrestricted prior : Nat .
508 (lambda unrestricted ignored : Nat . (leftResult role)))
509 (naturalLessOrEqual role (participantUpperOf left)))))))
510
511-- Identity binds the relation, namespace and membership epoch. Different
512-- equivalent decompositions may intentionally have different commitments;
513-- no optimizer may silently rewrite one after peers have agreed its identity.
514def participantWord =
515 (lambda unrestricted value : Nat . (dataBytesWord64LE (modelWord64FromNaturalTruncated value)))
516
517def participantSelectionBytes =
518 (lambda unrestricted selection : (family ParticipantSelection) .
519 (eliminate
520 ParticipantSelection
521 (lambda unrestricted current : (family ParticipantSelection) . Bytes)
522 selection
523 (branch
524 ParticipantStride
525 first
526 stride
527 count
528 .
529 (bytes-append
530 b"S"
531 (bytes-append
532 (participantWord first)
533 (bytes-append (participantWord stride) (participantWord count)))))
534 (branch
535 ParticipantRepeat
536 count
537 stride
538 inner
539 induction
540 .
541 (bytes-append
542 b"R"
543 (bytes-append (participantWord count) (bytes-append (participantWord stride) induction))))
544 (branch
545 ParticipantJoin
546 left
547 right
548 leftResult
549 rightResult
550 .
551 (bytes-append b"J" (bytes-append leftResult rightResult)))))
552
553def participantGroupBytes =
554 (lambda unrestricted group : (family ParticipantGroup) .
555 (bytes-append
556 b"alpha-participant-group-v1"
557 (bytes-append
558 (participantWord (participantUniverseOf group))
559 (bytes-append
560 (participantWord (participantEpochOf group))
561 (bytes-append
562 (participantWord (bytes-length (participantIdentityOf group)))
563 (bytes-append
564 (participantIdentityOf group)
565 (participantSelectionBytes (participantSelectionOf group))))))))
566
567def participantGroupDigest =
568 (lambda unrestricted group : (family ParticipantGroup) .
569 (sha256RawDigestOrEmpty (participantGroupBytes group)))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.