module Representation.ParticipantGroup import Std.Foundation import Std.Natural import Data.Bytes import Model.Word64 import Data.SHA256 import Data.SHA256Digest import Data.SHA256Padding -- Membership is a coordinate relation, independent of device capability and -- numerical evaluation order. Repetition shares one subgroup description; -- joining ordered, disjoint ranges indexes irregular populations. These are -- logical role IDs, not a claim that any physical devices executed. family ParticipantSelection : Type 0 constructor ParticipantStride field unrestricted participantFirst : Nat field unrestricted participantStride : Nat field unrestricted participantCount : Nat constructor ParticipantRepeat field unrestricted participantRepeats : Nat field unrestricted participantRepeatStride : Nat recursive unrestricted participantRepeatedSelection constructor ParticipantJoin recursive unrestricted participantLeftSelection recursive unrestricted participantRightSelection end-family family ParticipantGroup : Type 0 constructor ParticipantGroupOf field unrestricted participantUniverse : Nat field unrestricted participantEpoch : Nat field unrestricted participantIdentity : Bytes field unrestricted participantSelection : (family ParticipantSelection) end-family family ParticipantBounds : Type 0 constructor ParticipantBoundsOf field unrestricted participantLower : Nat field unrestricted participantUpper : Nat field unrestricted participantCardinality : Nat field unrestricted participantIndexNodes : Nat field unrestricted participantIndexDepth : Nat end-family -- Derived caches belong to the admitted compiler index. The unchecked selectors -- below must consume participantAdmit's result; arbitrary hand-built indexes -- are not certificates. A worker retains only its projected roles/edges, not -- this entire index. Lookup follows one structural path, never a rank list. family ParticipantIndex : Type 0 constructor ParticipantStrideIndex field unrestricted participantStrideBounds : (family ParticipantBounds) field unrestricted participantIndexStride : Nat constructor ParticipantRepeatIndex field unrestricted participantRepeatBounds : (family ParticipantBounds) field unrestricted participantIndexRepeatStride : Nat recursive unrestricted participantInnerIndex constructor ParticipantJoinIndex field unrestricted participantJoinBounds : (family ParticipantBounds) recursive unrestricted participantLeftIndex recursive unrestricted participantRightIndex end-family family ParticipantGroupFailure : Type 0 constructor ParticipantEmptyIdentity constructor ParticipantUniverseBounds constructor ParticipantEpochBounds constructor ParticipantEmptySelection constructor ParticipantZeroStride constructor ParticipantCoordinateOverflow constructor ParticipantRepeatedOverlap constructor ParticipantUnorderedJoin constructor ParticipantOutsideUniverse constructor ParticipantIndexBudget end-family -- Cardinalities and encoded identities use unsigned 64-bit words. Arithmetic -- is checked as mathematical Nat before any fixed-width identity is emitted. def participantWordLimit = 18446744073709551615 def participantRequire = (lambda erased value : Type 0 . (lambda unrestricted condition : Nat . (lambda unrestricted failure : (family ParticipantGroupFailure) . (lambda unrestricted next : (family StdResult (family ParticipantGroupFailure) value) . (nat-eliminate (lambda unrestricted flag : Nat . (family StdResult (family ParticipantGroupFailure) value)) (constructor StdResult StdFailure (family ParticipantGroupFailure) value failure) (lambda unrestricted prior : Nat . (lambda unrestricted ignored : (family StdResult (family ParticipantGroupFailure) value) . next)) condition))))) def participantBoundsLower = (lambda unrestricted bounds : (family ParticipantBounds) . (eliminate ParticipantBounds (lambda unrestricted current : (family ParticipantBounds) . Nat) bounds (branch ParticipantBoundsOf lower upper count nodes depth . lower))) def participantBoundsUpper = (lambda unrestricted bounds : (family ParticipantBounds) . (eliminate ParticipantBounds (lambda unrestricted current : (family ParticipantBounds) . Nat) bounds (branch ParticipantBoundsOf lower upper count nodes depth . upper))) def participantBoundsOf = (lambda unrestricted index : (family ParticipantIndex) . (eliminate ParticipantIndex (lambda unrestricted current : (family ParticipantIndex) . (family ParticipantBounds)) index (branch ParticipantStrideIndex bounds stride . bounds) (branch ParticipantRepeatIndex bounds stride inner induction . bounds) (branch ParticipantJoinIndex bounds left right leftResult rightResult . bounds))) def participantLowerOf = (lambda unrestricted index : (family ParticipantIndex) . (eliminate ParticipantBounds (lambda unrestricted current : (family ParticipantBounds) . Nat) (participantBoundsOf index) (branch ParticipantBoundsOf lower upper count nodes depth . lower))) def participantUpperOf = (lambda unrestricted index : (family ParticipantIndex) . (eliminate ParticipantBounds (lambda unrestricted current : (family ParticipantBounds) . Nat) (participantBoundsOf index) (branch ParticipantBoundsOf lower upper count nodes depth . upper))) def participantCountOf = (lambda unrestricted index : (family ParticipantIndex) . (eliminate ParticipantBounds (lambda unrestricted current : (family ParticipantBounds) . Nat) (participantBoundsOf index) (branch ParticipantBoundsOf lower upper count nodes depth . count))) def participantNodesOf = (lambda unrestricted index : (family ParticipantIndex) . (eliminate ParticipantBounds (lambda unrestricted current : (family ParticipantBounds) . Nat) (participantBoundsOf index) (branch ParticipantBoundsOf lower upper count nodes depth . nodes))) def participantDepthOf = (lambda unrestricted index : (family ParticipantIndex) . (eliminate ParticipantBounds (lambda unrestricted current : (family ParticipantBounds) . Nat) (participantBoundsOf index) (branch ParticipantBoundsOf lower upper count nodes depth . depth))) def participantUniverseOf = (lambda unrestricted group : (family ParticipantGroup) . (eliminate ParticipantGroup (lambda unrestricted current : (family ParticipantGroup) . Nat) group (branch ParticipantGroupOf universe epoch identity selection . universe))) def participantEpochOf = (lambda unrestricted group : (family ParticipantGroup) . (eliminate ParticipantGroup (lambda unrestricted current : (family ParticipantGroup) . Nat) group (branch ParticipantGroupOf universe epoch identity selection . epoch))) def participantIdentityOf = (lambda unrestricted group : (family ParticipantGroup) . (eliminate ParticipantGroup (lambda unrestricted current : (family ParticipantGroup) . Bytes) group (branch ParticipantGroupOf universe epoch identity selection . identity))) def participantSelectionOf = (lambda unrestricted group : (family ParticipantGroup) . (eliminate ParticipantGroup (lambda unrestricted current : (family ParticipantGroup) . (family ParticipantSelection)) group (branch ParticipantGroupOf universe epoch identity selection . selection))) def participantCompileStride = (lambda unrestricted first : Nat . (lambda unrestricted stride : Nat . (lambda unrestricted count : Nat . (participantRequire (family ParticipantIndex) (naturalNonzero count) (constructor ParticipantGroupFailure ParticipantEmptySelection) (participantRequire (family ParticipantIndex) (naturalAnd (naturalNonzero stride) (naturalLessOrEqual stride participantWordLimit)) (constructor ParticipantGroupFailure ParticipantZeroStride) (let unrestricted last = (naturalAdd first (naturalMultiply (naturalSaturatingSubtract count 1) stride)) in (participantRequire (family ParticipantIndex) (naturalAnd (naturalLessOrEqual count participantWordLimit) (naturalLessOrEqual last participantWordLimit)) (constructor ParticipantGroupFailure ParticipantCoordinateOverflow) (constructor StdResult StdSuccess (family ParticipantGroupFailure) (family ParticipantIndex) (constructor ParticipantIndex ParticipantStrideIndex (constructor ParticipantBounds ParticipantBoundsOf first last count 1 1) stride))))))))) def participantCompileRepeat = (lambda unrestricted count : Nat . (lambda unrestricted stride : Nat . (lambda unrestricted inner : (family ParticipantIndex) . (participantRequire (family ParticipantIndex) (naturalNonzero count) (constructor ParticipantGroupFailure ParticipantEmptySelection) (participantRequire (family ParticipantIndex) (naturalAnd (naturalLessOrEqual stride participantWordLimit) (naturalLess (naturalSaturatingSubtract (participantUpperOf inner) (participantLowerOf inner)) stride)) (constructor ParticipantGroupFailure ParticipantRepeatedOverlap) (let unrestricted last = (naturalAdd (participantUpperOf inner) (naturalMultiply (naturalSaturatingSubtract count 1) stride)) in (let unrestricted size = (naturalMultiply count (participantCountOf inner)) in (participantRequire (family ParticipantIndex) (naturalAnd (naturalLessOrEqual last participantWordLimit) (naturalLessOrEqual size participantWordLimit)) (constructor ParticipantGroupFailure ParticipantCoordinateOverflow) (constructor StdResult StdSuccess (family ParticipantGroupFailure) (family ParticipantIndex) (constructor ParticipantIndex ParticipantRepeatIndex (constructor ParticipantBounds ParticipantBoundsOf (participantLowerOf inner) last size (naturalAdd 1 (participantNodesOf inner)) (naturalAdd 1 (participantDepthOf inner))) stride inner)))))))))) def participantCompileJoin = (lambda unrestricted left : (family ParticipantIndex) . (lambda unrestricted right : (family ParticipantIndex) . (participantRequire (family ParticipantIndex) (naturalLess (participantUpperOf left) (participantLowerOf right)) (constructor ParticipantGroupFailure ParticipantUnorderedJoin) (let unrestricted size = (naturalAdd (participantCountOf left) (participantCountOf right)) in (participantRequire (family ParticipantIndex) (naturalLessOrEqual size participantWordLimit) (constructor ParticipantGroupFailure ParticipantCoordinateOverflow) (constructor StdResult StdSuccess (family ParticipantGroupFailure) (family ParticipantIndex) (constructor ParticipantIndex ParticipantJoinIndex (constructor ParticipantBounds ParticipantBoundsOf (participantLowerOf left) (participantUpperOf right) size (naturalAdd 1 (naturalAdd (participantNodesOf left) (participantNodesOf right))) (naturalAdd 1 (naturalSelect (naturalLess (participantDepthOf left) (participantDepthOf right)) (participantDepthOf right) (participantDepthOf left)))) left right))))))) def participantCompileSelection = (lambda unrestricted selection : (family ParticipantSelection) . (eliminate ParticipantSelection (lambda unrestricted current : (family ParticipantSelection) . (family StdResult (family ParticipantGroupFailure) (family ParticipantIndex))) selection (branch ParticipantStride first stride count . (participantCompileStride first stride count)) (branch ParticipantRepeat count stride inner induction . (stdResultBind (family ParticipantGroupFailure) (family ParticipantIndex) (family ParticipantIndex) induction (lambda unrestricted indexed : (family ParticipantIndex) . (participantCompileRepeat count stride indexed)))) (branch ParticipantJoin left right leftResult rightResult . (stdResultBind (family ParticipantGroupFailure) (family ParticipantIndex) (family ParticipantIndex) leftResult (lambda unrestricted leftIndex : (family ParticipantIndex) . (stdResultBind (family ParticipantGroupFailure) (family ParticipantIndex) (family ParticipantIndex) rightResult (lambda unrestricted rightIndex : (family ParticipantIndex) . (participantCompileJoin leftIndex rightIndex)))))))) -- Admission is linear in the compact description, not its cardinality. -- A budget limits index structure and lookup depth, not the number of roles. -- Empty, overlapping, wrapped or padded membership never enters a plan. def participantAdmit = (lambda unrestricted group : (family ParticipantGroup) . (lambda unrestricted nodeBudget : Nat . (lambda unrestricted depthBudget : Nat . (participantRequire (family ParticipantIndex) (naturalNonzero (bytes-length (participantIdentityOf group))) (constructor ParticipantGroupFailure ParticipantEmptyIdentity) (participantRequire (family ParticipantIndex) (naturalAnd (naturalNonzero (participantUniverseOf group)) (naturalLessOrEqual (participantUniverseOf group) participantWordLimit)) (constructor ParticipantGroupFailure ParticipantUniverseBounds) (participantRequire (family ParticipantIndex) (naturalLessOrEqual (participantEpochOf group) participantWordLimit) (constructor ParticipantGroupFailure ParticipantEpochBounds) (stdResultBind (family ParticipantGroupFailure) (family ParticipantIndex) (family ParticipantIndex) (participantCompileSelection (participantSelectionOf group)) (lambda unrestricted indexed : (family ParticipantIndex) . (participantRequire (family ParticipantIndex) (naturalLess (participantUpperOf indexed) (participantUniverseOf group)) (constructor ParticipantGroupFailure ParticipantOutsideUniverse) (participantRequire (family ParticipantIndex) (naturalAnd (naturalLessOrEqual (participantNodesOf indexed) nodeBudget) (naturalLessOrEqual (participantDepthOf indexed) depthBudget)) (constructor ParticipantGroupFailure ParticipantIndexBudget) (constructor StdResult StdSuccess (family ParticipantGroupFailure) (family ParticipantIndex) indexed))))))))))) def participantSelectUnchecked = (lambda unrestricted index : (family ParticipantIndex) . (eliminate ParticipantIndex (lambda unrestricted current : (family ParticipantIndex) . (pi unrestricted ordinal : Nat . Nat)) index (branch ParticipantStrideIndex bounds stride . (lambda unrestricted ordinal : Nat . (naturalAdd (participantBoundsLower bounds) (naturalMultiply ordinal stride)))) (branch ParticipantRepeatIndex bounds stride inner induction . (lambda unrestricted ordinal : Nat . (naturalAdd (naturalMultiply (naturalDivideUnchecked ordinal (participantCountOf inner)) stride) (induction (naturalModuloUnchecked ordinal (participantCountOf inner)))))) (branch ParticipantJoinIndex bounds left right leftResult rightResult . (lambda unrestricted ordinal : Nat . (nat-eliminate (lambda unrestricted flag : Nat . Nat) (rightResult (naturalSaturatingSubtract ordinal (participantCountOf left))) (lambda unrestricted prior : Nat . (lambda unrestricted ignored : Nat . (leftResult ordinal))) (naturalLess ordinal (participantCountOf left))))))) def participantMember = (lambda unrestricted index : (family ParticipantIndex) . (lambda unrestricted ordinal : Nat . (nat-eliminate (lambda unrestricted flag : Nat . (family StdOption Nat)) (constructor StdOption StdNone Nat) (lambda unrestricted prior : Nat . (lambda unrestricted ignored : (family StdOption Nat) . (constructor StdOption StdSome Nat (participantSelectUnchecked index ordinal)))) (naturalLess ordinal (participantCountOf index))))) def participantContains = (lambda unrestricted index : (family ParticipantIndex) . (eliminate ParticipantIndex (lambda unrestricted current : (family ParticipantIndex) . (pi unrestricted role : Nat . Nat)) index (branch ParticipantStrideIndex bounds stride . (lambda unrestricted role : Nat . (naturalAnd (naturalLessOrEqual (participantBoundsLower bounds) role) (naturalAnd (naturalLessOrEqual role (participantBoundsUpper bounds)) (naturalIsZero (naturalModuloUnchecked (naturalSaturatingSubtract role (participantBoundsLower bounds)) stride)))))) (branch ParticipantRepeatIndex bounds stride inner induction . (lambda unrestricted role : Nat . (naturalAnd (naturalLessOrEqual (participantBoundsLower bounds) role) (naturalAnd (naturalLessOrEqual role (participantBoundsUpper bounds)) (induction (naturalAdd (participantLowerOf inner) (naturalModuloUnchecked (naturalSaturatingSubtract role (participantBoundsLower bounds)) stride))))))) (branch ParticipantJoinIndex bounds left right leftResult rightResult . (lambda unrestricted role : Nat . (nat-eliminate (lambda unrestricted flag : Nat . Nat) (rightResult role) (lambda unrestricted prior : Nat . (lambda unrestricted ignored : Nat . (leftResult role))) (naturalLessOrEqual role (participantUpperOf left))))))) -- Identity binds the relation, namespace and membership epoch. Different -- equivalent decompositions may intentionally have different commitments; -- no optimizer may silently rewrite one after peers have agreed its identity. def participantWord = (lambda unrestricted value : Nat . (dataBytesWord64LE (modelWord64FromNaturalTruncated value))) def participantSelectionBytes = (lambda unrestricted selection : (family ParticipantSelection) . (eliminate ParticipantSelection (lambda unrestricted current : (family ParticipantSelection) . Bytes) selection (branch ParticipantStride first stride count . (bytes-append b"S" (bytes-append (participantWord first) (bytes-append (participantWord stride) (participantWord count))))) (branch ParticipantRepeat count stride inner induction . (bytes-append b"R" (bytes-append (participantWord count) (bytes-append (participantWord stride) induction)))) (branch ParticipantJoin left right leftResult rightResult . (bytes-append b"J" (bytes-append leftResult rightResult))))) def participantGroupBytes = (lambda unrestricted group : (family ParticipantGroup) . (bytes-append b"alpha-participant-group-v1" (bytes-append (participantWord (participantUniverseOf group)) (bytes-append (participantWord (participantEpochOf group)) (bytes-append (participantWord (bytes-length (participantIdentityOf group))) (bytes-append (participantIdentityOf group) (participantSelectionBytes (participantSelectionOf group)))))))) def participantGroupDigest = (lambda unrestricted group : (family ParticipantGroup) . (sha256RawDigestOrEmpty (participantGroupBytes group)))