1module Checkpoint.RegionManifest
2
3import Checkpoint.Envelope
4import Checkpoint.Schema
5import Data.Bytes
6import Data.SHA256
7import Data.SHA256Digest
8import Learning.Transition
9import Model.Word64
10import Representation.Partition
11import Std.Foundation
12import Std.List
13import Std.Natural
14
15-- A logical region is (the complete logical schema digest, its declaration
16-- ordinal). Names/formats describe that region; no rank, path, stream offset or
17-- device address enters the identity. Byte coordinates preserve opaque state
18-- and permit splitting a serialized value provided restore joins it before use.
19-- Declaration order is semantic and stable across physical placements.
20family CheckpointLogicalRegion : Type 0
21constructor CheckpointLogicalRegionOf
22field unrestricted logicalCheckpointNameValue : Bytes
23field unrestricted logicalCheckpointFormatValue : Bytes
24field unrestricted logicalCheckpointExtentValue : Nat
25
26end-family
27
28family CheckpointCapture : Type 0
29constructor CheckpointCaptureOf
30field unrestricted checkpointCaptureRoundValue : (family LearningRound)
31field unrestricted checkpointCaptureCursorValue : Nat
32
33end-family
34
35family CheckpointRegionPartition : Type 0
36constructor CheckpointRegionPartitionOf
37field unrestricted checkpointPartitionOrdinalValue : Nat
38field unrestricted checkpointPartitionIntervalsValue : (family StdList (family LogicalInterval))
39
40end-family
41
42family CheckpointPreparedShard : Type 0
43constructor CheckpointPreparedShardOf
44field unrestricted checkpointShardIntervalValue : (family LogicalInterval)
45field unrestricted checkpointShardFormatValue : Bytes
46field unrestricted checkpointShardCaptureValue : (family CheckpointCapture)
47field unrestricted checkpointShardBytesValue : Nat
48field unrestricted checkpointShardDigestValue : Bytes
49
50end-family
51
52family CheckpointCapturedRegion : Type 0
53constructor CheckpointCapturedRegionOf
54field unrestricted checkpointCapturedOrdinalValue : Nat
55field unrestricted checkpointCapturedShardsValue : (family StdList (family CheckpointPreparedShard))
56
57end-family
58
59def logicalCheckpointName =
60 (lambda unrestricted value : (family CheckpointLogicalRegion) .
61 (eliminate
62 CheckpointLogicalRegion
63 (lambda unrestricted current : (family CheckpointLogicalRegion) . Bytes)
64 value
65 (branch CheckpointLogicalRegionOf name format extent . name)))
66
67def logicalCheckpointFormat =
68 (lambda unrestricted value : (family CheckpointLogicalRegion) .
69 (eliminate
70 CheckpointLogicalRegion
71 (lambda unrestricted current : (family CheckpointLogicalRegion) . Bytes)
72 value
73 (branch CheckpointLogicalRegionOf name format extent . format)))
74
75def logicalCheckpointExtent =
76 (lambda unrestricted value : (family CheckpointLogicalRegion) .
77 (eliminate
78 CheckpointLogicalRegion
79 (lambda unrestricted current : (family CheckpointLogicalRegion) . Nat)
80 value
81 (branch CheckpointLogicalRegionOf name format extent . extent)))
82
83def checkpointCaptureRound =
84 (lambda unrestricted value : (family CheckpointCapture) .
85 (eliminate
86 CheckpointCapture
87 (lambda unrestricted current : (family CheckpointCapture) . (family LearningRound))
88 value
89 (branch CheckpointCaptureOf round cursor . round)))
90
91def checkpointCaptureCursor =
92 (lambda unrestricted value : (family CheckpointCapture) .
93 (eliminate
94 CheckpointCapture
95 (lambda unrestricted current : (family CheckpointCapture) . Nat)
96 value
97 (branch CheckpointCaptureOf round cursor . cursor)))
98
99def checkpointPartitionOrdinal =
100 (lambda unrestricted value : (family CheckpointRegionPartition) .
101 (eliminate
102 CheckpointRegionPartition
103 (lambda unrestricted current : (family CheckpointRegionPartition) . Nat)
104 value
105 (branch CheckpointRegionPartitionOf ordinal intervals . ordinal)))
106
107def checkpointPartitionIntervals =
108 (lambda unrestricted value : (family CheckpointRegionPartition) .
109 (eliminate
110 CheckpointRegionPartition
111 (lambda unrestricted current : (family CheckpointRegionPartition) .
112 (family StdList (family LogicalInterval)))
113 value
114 (branch CheckpointRegionPartitionOf ordinal intervals . intervals)))
115
116def checkpointShardInterval =
117 (lambda unrestricted value : (family CheckpointPreparedShard) .
118 (eliminate
119 CheckpointPreparedShard
120 (lambda unrestricted current : (family CheckpointPreparedShard) . (family LogicalInterval))
121 value
122 (branch CheckpointPreparedShardOf interval format capture extent digest . interval)))
123
124def checkpointShardFormat =
125 (lambda unrestricted value : (family CheckpointPreparedShard) .
126 (eliminate
127 CheckpointPreparedShard
128 (lambda unrestricted current : (family CheckpointPreparedShard) . Bytes)
129 value
130 (branch CheckpointPreparedShardOf interval format capture extent digest . format)))
131
132def checkpointShardCapture =
133 (lambda unrestricted value : (family CheckpointPreparedShard) .
134 (eliminate
135 CheckpointPreparedShard
136 (lambda unrestricted current : (family CheckpointPreparedShard) . (family CheckpointCapture))
137 value
138 (branch CheckpointPreparedShardOf interval format capture extent digest . capture)))
139
140def checkpointShardBytes =
141 (lambda unrestricted value : (family CheckpointPreparedShard) .
142 (eliminate
143 CheckpointPreparedShard
144 (lambda unrestricted current : (family CheckpointPreparedShard) . Nat)
145 value
146 (branch CheckpointPreparedShardOf interval format capture extent digest . extent)))
147
148def checkpointShardDigest =
149 (lambda unrestricted value : (family CheckpointPreparedShard) .
150 (eliminate
151 CheckpointPreparedShard
152 (lambda unrestricted current : (family CheckpointPreparedShard) . Bytes)
153 value
154 (branch CheckpointPreparedShardOf interval format capture extent digest . digest)))
155
156def checkpointCapturedOrdinal =
157 (lambda unrestricted value : (family CheckpointCapturedRegion) .
158 (eliminate
159 CheckpointCapturedRegion
160 (lambda unrestricted current : (family CheckpointCapturedRegion) . Nat)
161 value
162 (branch CheckpointCapturedRegionOf ordinal shards . ordinal)))
163
164def checkpointCapturedShards =
165 (lambda unrestricted value : (family CheckpointCapturedRegion) .
166 (eliminate
167 CheckpointCapturedRegion
168 (lambda unrestricted current : (family CheckpointCapturedRegion) .
169 (family StdList (family CheckpointPreparedShard)))
170 value
171 (branch CheckpointCapturedRegionOf ordinal shards . shards)))
172
173def checkpointManifestVersion : Nat =
174 1
175
176def checkpointManifestWordFits =
177 (lambda unrestricted value : Nat . (naturalLessOrEqual value 18446744073709551615))
178
179def checkpointCaptureValid =
180 (lambda unrestricted capture : (family CheckpointCapture) .
181 (eliminate
182 LearningRound
183 (lambda unrestricted current : (family LearningRound) . Nat)
184 (checkpointCaptureRound capture)
185 (branch
186 LearningRoundOf
187 epoch
188 version
189 .
190 (naturalAnd
191 (naturalNonzero epoch)
192 (naturalAnd
193 (checkpointManifestWordFits epoch)
194 (naturalAnd
195 (checkpointManifestWordFits version)
196 (checkpointManifestWordFits (checkpointCaptureCursor capture))))))))
197
198def checkpointCaptureEqual =
199 (lambda unrestricted expected : (family CheckpointCapture) .
200 (lambda unrestricted actual : (family CheckpointCapture) .
201 (naturalAnd
202 (learningRoundEqual (checkpointCaptureRound expected) (checkpointCaptureRound actual))
203 (naturalEqual (checkpointCaptureCursor expected) (checkpointCaptureCursor actual)))))
204
205def checkpointLogicalRegionValid =
206 (lambda unrestricted region : (family CheckpointLogicalRegion) .
207 (naturalAnd
208 (naturalNonzero (bytes-length (logicalCheckpointName region)))
209 (naturalAnd
210 (naturalNonzero (bytes-length (logicalCheckpointFormat region)))
211 (naturalAnd
212 (checkpointManifestWordFits (bytes-length (logicalCheckpointName region)))
213 (naturalAnd
214 (checkpointManifestWordFits (bytes-length (logicalCheckpointFormat region)))
215 (checkpointManifestWordFits (logicalCheckpointExtent region)))))))
216
217def checkpointLogicalRegionsValid =
218 (stdListFold
219 (family CheckpointLogicalRegion)
220 Nat
221 (lambda unrestricted region : (family CheckpointLogicalRegion) .
222 (lambda unrestricted rest : Nat . (naturalAnd (checkpointLogicalRegionValid region) rest)))
223 1)
224
225-- Empty logical regions have an empty shard list. Empty shard records are
226-- refused: they add no ownership, and otherwise permit duplicate empty claims.
227def checkpointNonemptyIntervals =
228 (stdListFold
229 (family LogicalInterval)
230 Nat
231 (lambda unrestricted interval : (family LogicalInterval) .
232 (lambda unrestricted rest : Nat .
233 (naturalAnd (naturalLess (intervalBegin interval) (intervalEnd interval)) rest)))
234 1)
235
236-- One linear pass over regions and fragments, never over logical byte counts.
237-- A group ordinal identifies a field in this schema, not a participant.
238def checkpointPartitionsFrom =
239 (lambda unrestricted regions : (family StdList (family CheckpointLogicalRegion)) .
240 (eliminate
241 StdList
242 (lambda unrestricted current : (family StdList (family CheckpointLogicalRegion)) .
243 (pi unrestricted ordinal : Nat .
244 (pi unrestricted parts : (family StdList (family CheckpointRegionPartition)) . Nat)))
245 regions
246 (branch
247 StdListEmpty
248 .
249 (lambda unrestricted ordinal : Nat .
250 (lambda unrestricted parts : (family StdList (family CheckpointRegionPartition)) .
251 (stdBoolToNatural (stdListIsEmpty (family CheckpointRegionPartition) parts)))))
252 (branch
253 StdListCons
254 region
255 tail
256 induction
257 .
258 (lambda unrestricted ordinal : Nat .
259 (lambda unrestricted parts : (family StdList (family CheckpointRegionPartition)) .
260 (eliminate
261 StdList
262 (lambda unrestricted current : (family StdList (family CheckpointRegionPartition)) .
263 Nat)
264 parts
265 (branch StdListEmpty . 0)
266 (branch
267 StdListCons
268 part
269 after
270 ignored
271 .
272 (naturalAnd
273 (naturalEqual ordinal (checkpointPartitionOrdinal part))
274 (naturalAnd
275 (intervalPartitionValid
276 (logicalCheckpointExtent region)
277 (checkpointPartitionIntervals part))
278 (naturalAnd
279 (checkpointNonemptyIntervals (checkpointPartitionIntervals part))
280 (induction (succ ordinal) after)))))))))))
281
282def checkpointPartitionsValid =
283 (lambda unrestricted regions : (family StdList (family CheckpointLogicalRegion)) .
284 (lambda unrestricted parts : (family StdList (family CheckpointRegionPartition)) .
285 (naturalAnd
286 (checkpointLogicalRegionsValid regions)
287 (checkpointPartitionsFrom regions 0 parts))))
288
289def checkpointPreparedShardValid =
290 (lambda unrestricted region : (family CheckpointLogicalRegion) .
291 (lambda unrestricted capture : (family CheckpointCapture) .
292 (lambda unrestricted shard : (family CheckpointPreparedShard) .
293 (naturalAnd
294 (checkpointCaptureEqual capture (checkpointShardCapture shard))
295 (naturalAnd
296 (bytes-equal (logicalCheckpointFormat region) (checkpointShardFormat shard))
297 (naturalAnd
298 (naturalEqual
299 (checkpointShardBytes shard)
300 (intervalExtent (checkpointShardInterval shard)))
301 (naturalAnd
302 (naturalEqual
303 (bytes-length (checkpointShardDigest shard))
304 checkpointEnvelopeDigestBytes)
305 (naturalAnd
306 (intervalWithin (logicalCheckpointExtent region) (checkpointShardInterval shard))
307 (naturalLess
308 (intervalBegin (checkpointShardInterval shard))
309 (intervalEnd (checkpointShardInterval shard)))))))))))
310
311def checkpointCapturedRegionValid =
312 (lambda unrestricted region : (family CheckpointLogicalRegion) .
313 (lambda unrestricted ordinal : Nat .
314 (lambda unrestricted capture : (family CheckpointCapture) .
315 (lambda unrestricted group : (family CheckpointCapturedRegion) .
316 (let unrestricted shards =
317 (checkpointCapturedShards group)
318 in
319 (naturalAnd
320 (naturalEqual ordinal (checkpointCapturedOrdinal group))
321 (naturalAnd
322 (intervalPartitionValid
323 (logicalCheckpointExtent region)
324 (stdListMap
325 (family CheckpointPreparedShard)
326 (family LogicalInterval)
327 checkpointShardInterval
328 shards))
329 (stdListFold
330 (family CheckpointPreparedShard)
331 Nat
332 (lambda unrestricted shard : (family CheckpointPreparedShard) .
333 (lambda unrestricted rest : Nat .
334 (naturalAnd (checkpointPreparedShardValid region capture shard) rest)))
335 1
336 shards))))))))
337
338def checkpointManifestFrom =
339 (lambda unrestricted capture : (family CheckpointCapture) .
340 (lambda unrestricted regions : (family StdList (family CheckpointLogicalRegion)) .
341 (eliminate
342 StdList
343 (lambda unrestricted current : (family StdList (family CheckpointLogicalRegion)) .
344 (pi unrestricted ordinal : Nat .
345 (pi unrestricted groups : (family StdList (family CheckpointCapturedRegion)) . Nat)))
346 regions
347 (branch
348 StdListEmpty
349 .
350 (lambda unrestricted ordinal : Nat .
351 (lambda unrestricted groups : (family StdList (family CheckpointCapturedRegion)) .
352 (stdBoolToNatural (stdListIsEmpty (family CheckpointCapturedRegion) groups)))))
353 (branch
354 StdListCons
355 region
356 tail
357 induction
358 .
359 (lambda unrestricted ordinal : Nat .
360 (lambda unrestricted groups : (family StdList (family CheckpointCapturedRegion)) .
361 (eliminate
362 StdList
363 (lambda unrestricted current : (family StdList (family CheckpointCapturedRegion)) .
364 Nat)
365 groups
366 (branch StdListEmpty . 0)
367 (branch
368 StdListCons
369 group
370 after
371 ignored
372 .
373 (naturalAnd
374 (checkpointCapturedRegionValid region ordinal capture group)
375 (induction (succ ordinal) after))))))))))
376
377def checkpointManifestValid =
378 (lambda unrestricted version : Nat .
379 (lambda unrestricted regions : (family StdList (family CheckpointLogicalRegion)) .
380 (lambda unrestricted capture : (family CheckpointCapture) .
381 (lambda unrestricted groups : (family StdList (family CheckpointCapturedRegion)) .
382 (naturalAnd
383 (naturalEqual version checkpointManifestVersion)
384 (naturalAnd
385 (checkpointLogicalRegionsValid regions)
386 (naturalAnd
387 (checkpointCaptureValid capture)
388 (checkpointManifestFrom capture regions 0 groups))))))))
389
390-- Length-prefix every semantic byte string. Builders materialize once rather
391-- than repeatedly copying an ever-growing schema suffix. Physical offsets and
392-- participant identities are deliberately absent from these canonical bytes.
393def checkpointManifestSized =
394 (lambda unrestricted value : Bytes .
395 (bytes-builder-append
396 (bytes-builder-chunk (checkpointEnvelopeWord (bytes-length value)))
397 (bytes-builder-chunk value)))
398
399def checkpointRegionEncoding =
400 (lambda unrestricted region : (family CheckpointLogicalRegion) .
401 (bytes-builder-append
402 (checkpointManifestSized (logicalCheckpointName region))
403 (bytes-builder-append
404 (checkpointManifestSized (logicalCheckpointFormat region))
405 (bytes-builder-chunk (checkpointEnvelopeWord (logicalCheckpointExtent region))))))
406
407def checkpointLogicalSchemaBytes =
408 (lambda unrestricted regions : (family StdList (family CheckpointLogicalRegion)) .
409 (bytes-builder-build
410 (bytes-builder-append
411 (bytes-builder-chunk b"ALPHA-LOGICAL-CHECKPOINT-1\x00")
412 (bytes-builder-append
413 (bytes-builder-chunk
414 (checkpointEnvelopeWord (stdListLength (family CheckpointLogicalRegion) regions)))
415 (stdListFold
416 (family CheckpointLogicalRegion)
417 BytesBuilder
418 (lambda unrestricted region : (family CheckpointLogicalRegion) .
419 (lambda unrestricted rest : BytesBuilder .
420 (bytes-builder-append (checkpointRegionEncoding region) rest)))
421 (bytes-builder-empty)
422 regions)))))
423
424def checkpointLogicalSchemaDigest =
425 (lambda unrestricted regions : (family StdList (family CheckpointLogicalRegion)) .
426 (sha256RawDigestOrEmpty (checkpointLogicalSchemaBytes regions)))
427
428-- Adapt the maintained field schema without its storage or stream offsets.
429-- Field kind/name, element count, domain and initialization remain semantic.
430-- These regions use byte coordinates; a native consumer must reconstruct and
431-- validate its declared representation before exposing a partial typed value.
432def checkpointLogicalRegionFromField =
433 (lambda unrestricted field : (family CheckpointField) .
434 (eliminate
435 CheckpointField
436 (lambda unrestricted current : (family CheckpointField) . (family CheckpointLogicalRegion))
437 field
438 (branch
439 CheckpointFieldValue
440 kind
441 name
442 storage
443 stream
444 extent
445 elements
446 domain
447 initialization
448 .
449 (constructor
450 CheckpointLogicalRegion
451 CheckpointLogicalRegionOf
452 (bytes-builder-build
453 (bytes-builder-append
454 (checkpointManifestSized (checkpointFieldKindName kind))
455 (checkpointManifestSized name)))
456 (bytes-builder-build
457 (bytes-builder-append
458 (checkpointManifestSized domain)
459 (bytes-builder-append
460 (bytes-builder-chunk (checkpointEnvelopeWord (modelWord64Natural elements)))
461 (checkpointManifestSized initialization))))
462 (modelWord64Natural extent)))))
463
464def checkpointLogicalRegionsFromFields =
465 (lambda unrestricted fields : (family CheckpointFields) .
466 (eliminate
467 CheckpointFields
468 (lambda unrestricted current : (family CheckpointFields) .
469 (family StdList (family CheckpointLogicalRegion)))
470 fields
471 (branch
472 CheckpointFieldsEnd
473 .
474 (constructor StdList StdListEmpty (family CheckpointLogicalRegion)))
475 (branch
476 CheckpointFieldsNext
477 head
478 tail
479 induction
480 .
481 (constructor
482 StdList
483 StdListCons
484 (family CheckpointLogicalRegion)
485 (checkpointLogicalRegionFromField head)
486 induction))))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.