module ParticipantGroupLaws import Representation.ParticipantGroup import Std.Foundation import Std.Natural import Model.Parameter import Model.Word64 import Data.Bytes def stride = (lambda unrestricted first : Nat . (lambda unrestricted step : Nat . (lambda unrestricted count : Nat . (constructor ParticipantSelection ParticipantStride first step count)))) def repeat = (lambda unrestricted count : Nat . (lambda unrestricted step : Nat . (lambda unrestricted inner : (family ParticipantSelection) . (constructor ParticipantSelection ParticipantRepeat count step inner)))) def join = (lambda unrestricted left : (family ParticipantSelection) . (lambda unrestricted right : (family ParticipantSelection) . (constructor ParticipantSelection ParticipantJoin left right))) def group = (lambda unrestricted selection : (family ParticipantSelection) . (constructor ParticipantGroup ParticipantGroupOf 200000 3 b"fleet-members" selection)) def regular = (group (repeat 625 320 (repeat 8 40 (repeat 2 20 (stride 0 1 20))))) def fixedAxes = (group (repeat 625 320 (stride 127 20 2))) def irregular = (group (join (stride 0 2 3) (repeat 3 11 (stride 10 3 2)))) def unequalCoverage = (group (join (stride 0 1 131072) (stride 131072 1 68928))) def failureCode = (lambda unrestricted failure : (family ParticipantGroupFailure) . (eliminate ParticipantGroupFailure (lambda unrestricted current : (family ParticipantGroupFailure) . Nat) failure (branch ParticipantEmptyIdentity . 1) (branch ParticipantUniverseBounds . 2) (branch ParticipantEpochBounds . 3) (branch ParticipantEmptySelection . 4) (branch ParticipantZeroStride . 5) (branch ParticipantCoordinateOverflow . 6) (branch ParticipantRepeatedOverlap . 7) (branch ParticipantUnorderedJoin . 8) (branch ParticipantOutsideUniverse . 9) (branch ParticipantIndexBudget . 10))) def verdict = (lambda unrestricted group : (family ParticipantGroup) . (lambda unrestricted nodes : Nat . (lambda unrestricted depth : Nat . (eliminate StdResult (lambda unrestricted result : (family StdResult (family ParticipantGroupFailure) (family ParticipantIndex)) . Nat) (participantAdmit group nodes depth) (branch StdFailure reason . (failureCode reason)) (branch StdSuccess index . 0))))) -- These probes consume the admitted index. The result 0 distinguishes refusal -- or an absent ordinal; present role r encodes as r+1, including role zero. def member = (lambda unrestricted group : (family ParticipantGroup) . (lambda unrestricted ordinal : Nat . (eliminate StdResult (lambda unrestricted result : (family StdResult (family ParticipantGroupFailure) (family ParticipantIndex)) . Nat) (participantAdmit group 16 8) (branch StdFailure reason . 0) (branch StdSuccess index . (eliminate StdOption (lambda unrestricted value : (family StdOption Nat) . Nat) (participantMember index ordinal) (branch StdNone . 0) (branch StdSome role . (naturalAdd role 1))))))) def count = (lambda unrestricted group : (family ParticipantGroup) . (eliminate StdResult (lambda unrestricted result : (family StdResult (family ParticipantGroupFailure) (family ParticipantIndex)) . Nat) (participantAdmit group 16 8) (branch StdFailure reason . 0) (branch StdSuccess index . (participantCountOf index)))) def contains = (lambda unrestricted group : (family ParticipantGroup) . (lambda unrestricted role : Nat . (eliminate StdResult (lambda unrestricted result : (family StdResult (family ParticipantGroupFailure) (family ParticipantIndex)) . Nat) (participantAdmit group 16 8) (branch StdFailure reason . 0) (branch StdSuccess index . (participantContains index role))))) def summary = (lambda unrestricted group : (family ParticipantGroup) . (eliminate StdResult (lambda unrestricted result : (family StdResult (family ParticipantGroupFailure) (family ParticipantIndex)) . Bytes) (participantAdmit group 16 8) (branch StdFailure reason . b"") (branch StdSuccess index . (bytes-append (participantWord (participantCountOf index)) (bytes-append (participantWord (participantNodesOf index)) (bytes-append (participantWord (participantDepthOf index)) (bytes-append (participantWord (participantLowerOf index)) (participantWord (participantUpperOf index))))))))) def regularAdmitted : (equal Nat (verdict regular 4 4) 0) = (refl Nat 0) def regularCount : (equal Nat (count regular) 200000) = (refl Nat 200000) def regularFirst : (equal Nat (member regular 0) 1) = (refl Nat 1) def regularLast : (equal Nat (member regular 199999) 200000) = (refl Nat 200000) def regularOutside : (equal Nat (member regular 200000) 0) = (refl Nat 0) def fixedCount : (equal Nat (count fixedAxes) 1250) = (refl Nat 1250) def fixedFirst : (equal Nat (member fixedAxes 0) 128) = (refl Nat 128) def fixedInner : (equal Nat (member fixedAxes 1) 148) = (refl Nat 148) def fixedNext : (equal Nat (member fixedAxes 2) 448) = (refl Nat 448) def fixedLast : (equal Nat (member fixedAxes 1249) 199828) = (refl Nat 199828) def fixedGap : (equal Nat (contains fixedAxes 128) 0) = (refl Nat 0) def fixedPresent : (equal Nat (contains fixedAxes 147) 1) = (refl Nat 1) def irregularCount : (equal Nat (count irregular) 9) = (refl Nat 9) def irregularLast : (equal Nat (member irregular 8) 36) = (refl Nat 36) def irregularMiddle : (equal Nat (member irregular 5) 22) = (refl Nat 22) def irregularGap : (equal Nat (contains irregular 23) 0) = (refl Nat 0) def irregularPresent : (equal Nat (contains irregular 24) 1) = (refl Nat 1) def irregularJoinGap : (equal Nat (contains irregular 6) 0) = (refl Nat 0) def unequalCount : (equal Nat (count unequalCoverage) 200000) = (refl Nat 200000) def unequalBoundary : (equal Nat (member unequalCoverage 131072) 131073) = (refl Nat 131073) def unequalLast : (equal Nat (member unequalCoverage 199999) 200000) = (refl Nat 200000) def nodeBudget : (equal Nat (verdict regular 3 4) 10) = (refl Nat 10) def depthBudget : (equal Nat (verdict regular 4 3) 10) = (refl Nat 10) def emptyRefused : (equal Nat (verdict (group (stride 0 1 0)) 16 8) 4) = (refl Nat 4) def zeroStride : (equal Nat (verdict (group (stride 0 0 1)) 16 8) 5) = (refl Nat 5) def wrappedStride : (equal Nat (verdict (group (stride 0 18446744073709551616 1)) 16 8) 5) = (refl Nat 5) def repeatedOverlap : (equal Nat (verdict (group (repeat 2 20 (stride 0 20 2))) 16 8) 7) = (refl Nat 7) def repeatedStrideOverflow : (equal Nat (verdict (group (repeat 1 18446744073709551616 (stride 0 1 1))) 16 8) 7) = (refl Nat 7) def joinOverlap : (equal Nat (verdict (group (join (stride 0 1 2) (stride 1 1 2))) 16 8) 8) = (refl Nat 8) def outsideUniverse : (equal Nat (verdict (group (stride 199999 1 2)) 16 8) 9) = (refl Nat 9) def coordinateOverflow : (equal Nat (verdict (group (stride 18446744073709551615 1 2)) 16 8) 6) = (refl Nat 6) def wrongIdentity : (equal Nat (verdict (constructor ParticipantGroup ParticipantGroupOf 200000 0 b"" (stride 0 1 1)) 16 8) 1) = (refl Nat 1) def epochOverflow : (equal Nat (verdict (constructor ParticipantGroup ParticipantGroupOf 200000 18446744073709551616 b"members" (stride 0 1 1)) 16 8) 3) = (refl Nat 3) def universeZero : (equal Nat (verdict (constructor ParticipantGroup ParticipantGroupOf 0 0 b"members" (stride 0 1 1)) 16 8) 2) = (refl Nat 2) def main : Nat = 0