1module Runtime.OrderedCombine
2
3import Runtime.Protocol
4import Runtime.RegionTransfer
5import Runtime.RegionFrame
6import Learning.Transition
7import Learning.Numerics
8import Representation.ParticipantGroup
9import Representation.Partition
10import Data.SHA256
11import Data.SHA256Padding
12import Data.SHA256Digest
13import Std.List
14import Std.Foundation
15import Std.Natural
16
17-- This is the numerical expression tree, not a network-algorithm label.
18-- A leaf contributes once. A branch combines left then right at its named
19-- owner; no associativity or commutativity is assumed. Placement may change
20-- only through an explicit new tree/identity. Leaf values may carry numerators
21-- and weight masses together; normalization is a separate learning operation.
22-- Explicit ordered members retain the original exact leaf-order contract.
23-- A compact group specifies a set: the numerical tree still fixes its own
24-- operand order, and must cover every group member exactly once.
25family CombineCoverage : Type 0
26constructor CombineOrderedMembers
27field unrestricted combineOrderedMembers : (family StdList Nat)
28constructor CombineParticipantGroup
29field unrestricted combineParticipantGroup : (family ParticipantGroup)
30field unrestricted combineGroupNodeBudget : Nat
31field unrestricted combineGroupDepthBudget : Nat
32
33end-family
34
35family OrderedCombineTree : Type 0
36constructor OrderedCombineLeaf
37field unrestricted combineLeafOwner : Nat
38constructor OrderedCombineBranch
39field unrestricted combineBranchOwner : Nat
40recursive unrestricted combineLeftTree
41recursive unrestricted combineRightTree
42
43end-family
44
45family CombineReference : Type 0
46constructor CombineReferenceOf
47field unrestricted combineReferenceOwnerValue : Nat
48field unrestricted combineReferenceSlotValue : Nat
49
50end-family
51
52family CombineStage : Type 0
53constructor CombineReduce
54constructor CombineReplicate
55
56end-family
57
58family OrderedCombineOperation : Type 0
59parameter erased combinePayload : Type 0
60constructor CombineReadLeaf
61field unrestricted combineReadDestination : (family CombineReference)
62constructor CombineCopy
63field unrestricted combineCopySource : (family CombineReference)
64field unrestricted combineCopyDestination : (family CombineReference)
65constructor CombineApply
66field unrestricted combineApplyLeft : (family CombineReference)
67field unrestricted combineApplyRight : (family CombineReference)
68field unrestricted combineApplyDestination : (family CombineReference)
69constructor CombinePrepare
70field unrestricted combinePrepareSource : (family CombineReference)
71field unrestricted combinePreparePayload : combinePayload
72constructor CombineConsume
73field unrestricted combineConsumePayload : combinePayload
74field unrestricted combineConsumeDestination : (family CombineReference)
75
76end-family
77
78family OrderedCombineFailure : Type 0
79constructor CombineMembershipBounds
80constructor CombineDuplicateLeaf
81constructor CombineOwnerOutsideChildren
82constructor CombineReferenceBounds
83constructor CombineCoverageMismatch
84constructor CombineIdentityUnavailable
85constructor CombineNumericalRefused
86field unrestricted combineNumericalReason : (family NumericalFailure)
87constructor CombineProtocolRefused
88field unrestricted combineProtocolReason : (family ProtocolFailure)
89
90end-family
91
92def combineOwner =
93 (lambda unrestricted tree : (family OrderedCombineTree) .
94 (eliminate
95 OrderedCombineTree
96 (lambda unrestricted current : (family OrderedCombineTree) . Nat)
97 tree
98 (branch OrderedCombineLeaf owner . owner)
99 (branch OrderedCombineBranch owner left right leftResult rightResult . owner)))
100
101def combineNodeCount =
102 (lambda unrestricted tree : (family OrderedCombineTree) .
103 (eliminate
104 OrderedCombineTree
105 (lambda unrestricted current : (family OrderedCombineTree) . Nat)
106 tree
107 (branch OrderedCombineLeaf owner . 1)
108 (branch
109 OrderedCombineBranch
110 owner
111 left
112 right
113 leftResult
114 rightResult
115 .
116 (naturalAdd 1 (naturalAdd leftResult rightResult)))))
117
118def combineLeaves =
119 (lambda unrestricted tree : (family OrderedCombineTree) .
120 (eliminate
121 OrderedCombineTree
122 (lambda unrestricted current : (family OrderedCombineTree) . (family StdList Nat))
123 tree
124 (branch
125 OrderedCombineLeaf
126 owner
127 .
128 (constructor StdList StdListCons Nat owner (constructor StdList StdListEmpty Nat)))
129 (branch
130 OrderedCombineBranch
131 owner
132 left
133 right
134 leftResult
135 rightResult
136 .
137 (stdListAppend Nat leftResult rightResult))))
138
139def combineReferenceOwner =
140 (lambda unrestricted reference : (family CombineReference) .
141 (eliminate
142 CombineReference
143 (lambda unrestricted current : (family CombineReference) . Nat)
144 reference
145 (branch CombineReferenceOf owner slot . owner)))
146
147def combineReferenceSlot =
148 (lambda unrestricted reference : (family CombineReference) .
149 (eliminate
150 CombineReference
151 (lambda unrestricted current : (family CombineReference) . Nat)
152 reference
153 (branch CombineReferenceOf owner slot . slot)))
154
155def combineReference =
156 (lambda unrestricted owner : Nat .
157 (lambda unrestricted node : Nat .
158 (lambda unrestricted field : Nat .
159 (constructor
160 CombineReference
161 CombineReferenceOf
162 owner
163 (naturalAdd (naturalMultiply 3 node) field)))))
164
165def combineTreeReference =
166 (lambda unrestricted tree : (family OrderedCombineTree) .
167 (lambda unrestricted base : Nat .
168 (combineReference
169 (combineOwner tree)
170 (naturalSaturatingSubtract (naturalAdd base (combineNodeCount tree)) 1)
171 0)))
172
173def combineStageCode =
174 (lambda unrestricted stage : (family CombineStage) .
175 (eliminate
176 CombineStage
177 (lambda unrestricted current : (family CombineStage) . Nat)
178 stage
179 (branch CombineReduce . 0)
180 (branch CombineReplicate . 1)))
181
182-- Canonical prefix encoding includes the numerical tree, leaf order and
183-- execution owners. The enclosing anchor supplies the operation/schema/run
184-- semantics; changing only a route cannot disguise a different collective.
185def combineTreeBytes =
186 (lambda unrestricted tree : (family OrderedCombineTree) .
187 (eliminate
188 OrderedCombineTree
189 (lambda unrestricted current : (family OrderedCombineTree) . Bytes)
190 tree
191 (branch OrderedCombineLeaf owner . (bytes-append b"L" (regionFrameWord owner)))
192 (branch
193 OrderedCombineBranch
194 owner
195 left
196 right
197 leftResult
198 rightResult
199 .
200 (bytes-append
201 b"B"
202 (bytes-append
203 (regionFrameWord owner)
204 (bytes-append leftResult (bytes-append rightResult b"")))))))
205
206def combineTreeDigest =
207 (lambda unrestricted tree : (family OrderedCombineTree) .
208 (sha256RawDigestOrEmpty (bytes-append b"alpha-ordered-combine-v1" (combineTreeBytes tree))))
209
210-- Edge scopes retain the admitted plan digest and length-delimited region
211-- with fixed-width stage/reference coordinates. They require no additional
212-- hash invocation; the frame schema checks their final bounded byte extent.
213-- All node references use postorder ordinals. Three fields per node are
214-- output, left operand and right operand. They are logical references, never
215-- host addresses. A target is free to pack only its reachable references.
216def combineTransferIdentity =
217 (lambda unrestricted anchor : (family RegionTransferIdentity) .
218 (lambda unrestricted digest : Bytes .
219 (lambda unrestricted stage : (family CombineStage) .
220 (lambda unrestricted source : (family CombineReference) .
221 (lambda unrestricted destination : (family CombineReference) .
222 (eliminate
223 RegionTransferIdentity
224 (lambda unrestricted current : (family RegionTransferIdentity) .
225 (family RegionTransferIdentity))
226 anchor
227 (branch
228 RegionTransferIdentityOf
229 composition
230 run
231 region
232 representation
233 round
234 operation
235 sender
236 receiver
237 interval
238 .
239 (constructor
240 RegionTransferIdentity
241 RegionTransferIdentityOf
242 composition
243 run
244 (bytes-append
245 b"alpha-combine-edge-v1"
246 (bytes-append
247 (regionFrameWord (bytes-length region))
248 (bytes-append
249 region
250 (bytes-append
251 digest
252 (bytes-append
253 (regionFrameWord (combineStageCode stage))
254 (bytes-append
255 (regionFrameWord (combineReferenceSlot source))
256 (bytes-append
257 (regionFrameWord (combineReferenceSlot destination))
258 b"")))))))
259 representation
260 round
261 operation
262 (combineReferenceOwner source)
263 (combineReferenceOwner destination)
264 interval))))))))
265
266-- Prefix composition is shared by numerical and membership commitments.
267-- Preserve the caller's representation as a sized suffix; neither commitment
268-- may erase the original payload schema.
269def combineRepresentationAnchor =
270 (lambda unrestricted prefix : Bytes .
271 (lambda unrestricted anchor : (family RegionTransferIdentity) .
272 (eliminate
273 RegionTransferIdentity
274 (lambda unrestricted current : (family RegionTransferIdentity) .
275 (family RegionTransferIdentity))
276 anchor
277 (branch
278 RegionTransferIdentityOf
279 composition
280 run
281 region
282 representation
283 round
284 operation
285 sender
286 receiver
287 interval
288 .
289 (constructor
290 RegionTransferIdentity
291 RegionTransferIdentityOf
292 composition
293 run
294 region
295 (bytes-append
296 prefix
297 (bytes-append (regionFrameWord (bytes-length representation)) representation))
298 round
299 operation
300 sender
301 receiver
302 interval)))))
303
304def combineNumericalAnchor =
305 (lambda unrestricted contract : (family NumericalContract) .
306 (lambda unrestricted anchor : (family RegionTransferIdentity) .
307 (combineRepresentationAnchor
308 (bytes-append b"numeric-contract-v1" (numericalExactContractDigest contract))
309 anchor)))
310
311-- Compact group identity binds logical universe, membership epoch and the
312-- entire coordinate relation. Budgets constrain admission, not membership.
313def combineCoverageAnchor =
314 (lambda unrestricted coverage : (family CombineCoverage) .
315 (lambda unrestricted anchor : (family RegionTransferIdentity) .
316 (eliminate
317 CombineCoverage
318 (lambda unrestricted current : (family CombineCoverage) . (family RegionTransferIdentity))
319 coverage
320 (branch CombineOrderedMembers members . anchor)
321 (branch
322 CombineParticipantGroup
323 group
324 nodes
325 depth
326 .
327 (combineRepresentationAnchor
328 (bytes-append b"group-contract-v1" (participantGroupDigest group))
329 anchor)))))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.