module Runtime.OrderedCombine import Runtime.Protocol import Runtime.RegionTransfer import Runtime.RegionFrame import Learning.Transition import Learning.Numerics import Representation.ParticipantGroup import Representation.Partition import Data.SHA256 import Data.SHA256Padding import Data.SHA256Digest import Std.List import Std.Foundation import Std.Natural -- This is the numerical expression tree, not a network-algorithm label. -- A leaf contributes once. A branch combines left then right at its named -- owner; no associativity or commutativity is assumed. Placement may change -- only through an explicit new tree/identity. Leaf values may carry numerators -- and weight masses together; normalization is a separate learning operation. -- Explicit ordered members retain the original exact leaf-order contract. -- A compact group specifies a set: the numerical tree still fixes its own -- operand order, and must cover every group member exactly once. family CombineCoverage : Type 0 constructor CombineOrderedMembers field unrestricted combineOrderedMembers : (family StdList Nat) constructor CombineParticipantGroup field unrestricted combineParticipantGroup : (family ParticipantGroup) field unrestricted combineGroupNodeBudget : Nat field unrestricted combineGroupDepthBudget : Nat end-family family OrderedCombineTree : Type 0 constructor OrderedCombineLeaf field unrestricted combineLeafOwner : Nat constructor OrderedCombineBranch field unrestricted combineBranchOwner : Nat recursive unrestricted combineLeftTree recursive unrestricted combineRightTree end-family family CombineReference : Type 0 constructor CombineReferenceOf field unrestricted combineReferenceOwnerValue : Nat field unrestricted combineReferenceSlotValue : Nat end-family family CombineStage : Type 0 constructor CombineReduce constructor CombineReplicate end-family family OrderedCombineOperation : Type 0 parameter erased combinePayload : Type 0 constructor CombineReadLeaf field unrestricted combineReadDestination : (family CombineReference) constructor CombineCopy field unrestricted combineCopySource : (family CombineReference) field unrestricted combineCopyDestination : (family CombineReference) constructor CombineApply field unrestricted combineApplyLeft : (family CombineReference) field unrestricted combineApplyRight : (family CombineReference) field unrestricted combineApplyDestination : (family CombineReference) constructor CombinePrepare field unrestricted combinePrepareSource : (family CombineReference) field unrestricted combinePreparePayload : combinePayload constructor CombineConsume field unrestricted combineConsumePayload : combinePayload field unrestricted combineConsumeDestination : (family CombineReference) end-family family OrderedCombineFailure : Type 0 constructor CombineMembershipBounds constructor CombineDuplicateLeaf constructor CombineOwnerOutsideChildren constructor CombineReferenceBounds constructor CombineCoverageMismatch constructor CombineIdentityUnavailable constructor CombineNumericalRefused field unrestricted combineNumericalReason : (family NumericalFailure) constructor CombineProtocolRefused field unrestricted combineProtocolReason : (family ProtocolFailure) end-family def combineOwner = (lambda unrestricted tree : (family OrderedCombineTree) . (eliminate OrderedCombineTree (lambda unrestricted current : (family OrderedCombineTree) . Nat) tree (branch OrderedCombineLeaf owner . owner) (branch OrderedCombineBranch owner left right leftResult rightResult . owner))) def combineNodeCount = (lambda unrestricted tree : (family OrderedCombineTree) . (eliminate OrderedCombineTree (lambda unrestricted current : (family OrderedCombineTree) . Nat) tree (branch OrderedCombineLeaf owner . 1) (branch OrderedCombineBranch owner left right leftResult rightResult . (naturalAdd 1 (naturalAdd leftResult rightResult))))) def combineLeaves = (lambda unrestricted tree : (family OrderedCombineTree) . (eliminate OrderedCombineTree (lambda unrestricted current : (family OrderedCombineTree) . (family StdList Nat)) tree (branch OrderedCombineLeaf owner . (constructor StdList StdListCons Nat owner (constructor StdList StdListEmpty Nat))) (branch OrderedCombineBranch owner left right leftResult rightResult . (stdListAppend Nat leftResult rightResult)))) def combineReferenceOwner = (lambda unrestricted reference : (family CombineReference) . (eliminate CombineReference (lambda unrestricted current : (family CombineReference) . Nat) reference (branch CombineReferenceOf owner slot . owner))) def combineReferenceSlot = (lambda unrestricted reference : (family CombineReference) . (eliminate CombineReference (lambda unrestricted current : (family CombineReference) . Nat) reference (branch CombineReferenceOf owner slot . slot))) def combineReference = (lambda unrestricted owner : Nat . (lambda unrestricted node : Nat . (lambda unrestricted field : Nat . (constructor CombineReference CombineReferenceOf owner (naturalAdd (naturalMultiply 3 node) field))))) def combineTreeReference = (lambda unrestricted tree : (family OrderedCombineTree) . (lambda unrestricted base : Nat . (combineReference (combineOwner tree) (naturalSaturatingSubtract (naturalAdd base (combineNodeCount tree)) 1) 0))) def combineStageCode = (lambda unrestricted stage : (family CombineStage) . (eliminate CombineStage (lambda unrestricted current : (family CombineStage) . Nat) stage (branch CombineReduce . 0) (branch CombineReplicate . 1))) -- Canonical prefix encoding includes the numerical tree, leaf order and -- execution owners. The enclosing anchor supplies the operation/schema/run -- semantics; changing only a route cannot disguise a different collective. def combineTreeBytes = (lambda unrestricted tree : (family OrderedCombineTree) . (eliminate OrderedCombineTree (lambda unrestricted current : (family OrderedCombineTree) . Bytes) tree (branch OrderedCombineLeaf owner . (bytes-append b"L" (regionFrameWord owner))) (branch OrderedCombineBranch owner left right leftResult rightResult . (bytes-append b"B" (bytes-append (regionFrameWord owner) (bytes-append leftResult (bytes-append rightResult b""))))))) def combineTreeDigest = (lambda unrestricted tree : (family OrderedCombineTree) . (sha256RawDigestOrEmpty (bytes-append b"alpha-ordered-combine-v1" (combineTreeBytes tree)))) -- Edge scopes retain the admitted plan digest and length-delimited region -- with fixed-width stage/reference coordinates. They require no additional -- hash invocation; the frame schema checks their final bounded byte extent. -- All node references use postorder ordinals. Three fields per node are -- output, left operand and right operand. They are logical references, never -- host addresses. A target is free to pack only its reachable references. def combineTransferIdentity = (lambda unrestricted anchor : (family RegionTransferIdentity) . (lambda unrestricted digest : Bytes . (lambda unrestricted stage : (family CombineStage) . (lambda unrestricted source : (family CombineReference) . (lambda unrestricted destination : (family CombineReference) . (eliminate RegionTransferIdentity (lambda unrestricted current : (family RegionTransferIdentity) . (family RegionTransferIdentity)) anchor (branch RegionTransferIdentityOf composition run region representation round operation sender receiver interval . (constructor RegionTransferIdentity RegionTransferIdentityOf composition run (bytes-append b"alpha-combine-edge-v1" (bytes-append (regionFrameWord (bytes-length region)) (bytes-append region (bytes-append digest (bytes-append (regionFrameWord (combineStageCode stage)) (bytes-append (regionFrameWord (combineReferenceSlot source)) (bytes-append (regionFrameWord (combineReferenceSlot destination)) b""))))))) representation round operation (combineReferenceOwner source) (combineReferenceOwner destination) interval)))))))) -- Prefix composition is shared by numerical and membership commitments. -- Preserve the caller's representation as a sized suffix; neither commitment -- may erase the original payload schema. def combineRepresentationAnchor = (lambda unrestricted prefix : Bytes . (lambda unrestricted anchor : (family RegionTransferIdentity) . (eliminate RegionTransferIdentity (lambda unrestricted current : (family RegionTransferIdentity) . (family RegionTransferIdentity)) anchor (branch RegionTransferIdentityOf composition run region representation round operation sender receiver interval . (constructor RegionTransferIdentity RegionTransferIdentityOf composition run region (bytes-append prefix (bytes-append (regionFrameWord (bytes-length representation)) representation)) round operation sender receiver interval))))) def combineNumericalAnchor = (lambda unrestricted contract : (family NumericalContract) . (lambda unrestricted anchor : (family RegionTransferIdentity) . (combineRepresentationAnchor (bytes-append b"numeric-contract-v1" (numericalExactContractDigest contract)) anchor))) -- Compact group identity binds logical universe, membership epoch and the -- entire coordinate relation. Budgets constrain admission, not membership. def combineCoverageAnchor = (lambda unrestricted coverage : (family CombineCoverage) . (lambda unrestricted anchor : (family RegionTransferIdentity) . (eliminate CombineCoverage (lambda unrestricted current : (family CombineCoverage) . (family RegionTransferIdentity)) coverage (branch CombineOrderedMembers members . anchor) (branch CombineParticipantGroup group nodes depth . (combineRepresentationAnchor (bytes-append b"group-contract-v1" (participantGroupDigest group)) anchor)))))