1module Data.Bytes
2
3import Model.Config
4import Model.Parameter
5import Std.Byte
6import Std.Natural
7
8-- Stable public failures. Assigned ALPHA-DATA-BYTES codes never change.
9family DataBytesErrorCode : Type 0
10constructor DataBytesWord32InputTooShort
11constructor DataBytesWord64InputTooShort
12constructor DataBytesLengthOverflow
13constructor DataBytesOffsetOverflow
14constructor DataBytesOffsetOutOfRange
15constructor DataBytesIndexOutOfRange
16constructor DataBytesSliceOutOfRange
17constructor DataBytesWord32MalformedLength
18constructor DataBytesWord64MalformedLength
19constructor DataBytesAllocationLimitExceeded
20constructor DataBytesBuilderInvariantViolation
21
22end-family
23
24family DataBytesOrdering : Type 0
25constructor DataBytesLess
26constructor DataBytesEqual
27constructor DataBytesGreater
28
29end-family
30
31family DataBytesTelemetry : Type 0
32constructor DataBytesTelemetryValue
33field unrestricted dataBytesTelemetryInputBytes : Nat
34field unrestricted dataBytesTelemetryRequestedBytes : Nat
35field unrestricted dataBytesTelemetryOutputBytes : Nat
36field unrestricted dataBytesTelemetryChunks : Nat
37field unrestricted dataBytesTelemetrySharedBytes : Nat
38field unrestricted dataBytesTelemetryPreparationCopiedBytes : Nat
39field unrestricted dataBytesTelemetryVisitedBytes : Nat
40field unrestricted dataBytesTelemetryAllocationLimit : Nat
41
42end-family
43
44family DataBytesResult : Type 0
45constructor DataBytesSucceeded
46field unrestricted dataBytesSucceededValue : Bytes
47field unrestricted dataBytesSucceededTelemetry : (family DataBytesTelemetry)
48constructor DataBytesFailed
49field unrestricted dataBytesFailureCode : (family DataBytesErrorCode)
50field unrestricted dataBytesFailureTelemetry : (family DataBytesTelemetry)
51
52end-family
53
54family DataBytesCheckedNaturalResult : Type 0
55constructor DataBytesCheckedNaturalSucceeded
56field unrestricted dataBytesCheckedNaturalValue : Nat
57constructor DataBytesCheckedNaturalFailed
58field unrestricted dataBytesCheckedNaturalError : (family DataBytesErrorCode)
59
60end-family
61
62-- A slice retains a suffix of its immutable source and a bounded visible length.
63family DataBytesSlice : Type 0
64constructor DataBytesSliceView
65field unrestricted dataBytesSliceSuffix : Bytes
66field unrestricted dataBytesSliceLength : Nat
67
68end-family
69
70family DataBytesSliceResult : Type 0
71constructor DataBytesSliceSucceeded
72field unrestricted dataBytesSliceSucceededValue : (family DataBytesSlice)
73field unrestricted dataBytesSliceSucceededTelemetry : (family DataBytesTelemetry)
74constructor DataBytesSliceFailed
75field unrestricted dataBytesSliceFailureCode : (family DataBytesErrorCode)
76field unrestricted dataBytesSliceFailureTelemetry : (family DataBytesTelemetry)
77
78end-family
79
80family DataBytesIndexResult : Type 0
81constructor DataBytesIndexSucceeded
82field unrestricted dataBytesIndexedByte : Byte
83field unrestricted dataBytesIndexTelemetry : (family DataBytesTelemetry)
84constructor DataBytesIndexFailed
85field unrestricted dataBytesIndexFailureCode : (family DataBytesErrorCode)
86field unrestricted dataBytesIndexFailureTelemetry : (family DataBytesTelemetry)
87
88end-family
89
90-- Appending builders creates runtime DAG nodes. No byte payload is copied until
91-- the one checked bytes-builder-build at the edge of the operation.
92family DataBytesBuilder : Type 0
93constructor DataBytesBuilderValue
94field unrestricted dataBytesBuilderRuntime : BytesBuilder
95field unrestricted dataBytesBuilderLength : Nat
96field unrestricted dataBytesBuilderChunks : Nat
97field unrestricted dataBytesBuilderSharedBytes : Nat
98field unrestricted dataBytesBuilderPreparationCopiedBytes : Nat
99
100end-family
101
102family DataBytesBuilderResult : Type 0
103constructor DataBytesBuilderSucceeded
104field unrestricted dataBytesBuilderSucceededValue : (family DataBytesBuilder)
105field unrestricted dataBytesBuilderSucceededTelemetry : (family DataBytesTelemetry)
106constructor DataBytesBuilderFailed
107field unrestricted dataBytesBuilderFailureCode : (family DataBytesErrorCode)
108field unrestricted dataBytesBuilderFailureTelemetry : (family DataBytesTelemetry)
109
110end-family
111
112family DataBytesWord32DecodeResult : Type 0
113constructor DataBytesWord32Decoded
114field unrestricted dataBytesDecodedWord32 : (family ModelWord32)
115field unrestricted dataBytesWord32Remaining : Bytes
116constructor DataBytesWord32DecodeFailed
117field unrestricted dataBytesWord32DecodeError : (family DataBytesErrorCode)
118
119end-family
120
121family DataBytesWord64DecodeResult : Type 0
122constructor DataBytesWord64Decoded
123field unrestricted dataBytesDecodedWord64 : (family ModelWord64)
124field unrestricted dataBytesWord64Remaining : Bytes
125constructor DataBytesWord64DecodeFailed
126field unrestricted dataBytesWord64DecodeError : (family DataBytesErrorCode)
127
128end-family
129
130family DataBytesWord32ExactDecodeResult : Type 0
131constructor DataBytesWord32ExactlyDecoded
132field unrestricted dataBytesExactlyDecodedWord32 : (family ModelWord32)
133field unrestricted dataBytesWord32ExactTelemetry : (family DataBytesTelemetry)
134constructor DataBytesWord32ExactDecodeFailed
135field unrestricted dataBytesWord32ExactDecodeError : (family DataBytesErrorCode)
136field unrestricted dataBytesWord32ExactFailureTelemetry : (family DataBytesTelemetry)
137
138end-family
139
140family DataBytesWord64ExactDecodeResult : Type 0
141constructor DataBytesWord64ExactlyDecoded
142field unrestricted dataBytesExactlyDecodedWord64 : (family ModelWord64)
143field unrestricted dataBytesWord64ExactTelemetry : (family DataBytesTelemetry)
144constructor DataBytesWord64ExactDecodeFailed
145field unrestricted dataBytesWord64ExactDecodeError : (family DataBytesErrorCode)
146field unrestricted dataBytesWord64ExactFailureTelemetry : (family DataBytesTelemetry)
147
148end-family
149
150def dataBytesNaturalOne =
151 (byte-to-nat (byte 1))
152
153def dataBytesNaturalTwo =
154 (byte-to-nat (byte 2))
155
156def dataBytesNaturalThree =
157 (byte-to-nat (byte 3))
158
159def dataBytesNaturalFour =
160 (byte-to-nat (byte 4))
161
162def dataBytesNaturalFive =
163 (byte-to-nat (byte 5))
164
165def dataBytesNaturalSix =
166 (byte-to-nat (byte 6))
167
168def dataBytesNaturalSeven =
169 (byte-to-nat (byte 7))
170
171def dataBytesNaturalEight =
172 (byte-to-nat (byte 8))
173
174def dataBytesNaturalTen =
175 (byte-to-nat (byte 10))
176
177def dataBytesNaturalSixteen =
178 (byte-to-nat (byte 16))
179
180def dataBytesNaturalSixtyFour =
181 (byte-to-nat (byte 64))
182
183def dataBytesNaturalOneThousandTwentyFour =
184 (naturalMultiply dataBytesNaturalSixteen dataBytesNaturalSixtyFour)
185
186-- 64 MiB. Callers handling larger artifacts must supply an explicit limit.
187def dataBytesDefaultAllocationLimit =
188 (naturalMultiply
189 dataBytesNaturalSixtyFour
190 (naturalMultiply dataBytesNaturalOneThousandTwentyFour dataBytesNaturalOneThousandTwentyFour))
191
192def dataBytesErrorCodeBytes =
193 (lambda unrestricted code : (family DataBytesErrorCode) .
194 (eliminate
195 DataBytesErrorCode
196 (lambda unrestricted current : (family DataBytesErrorCode) . Bytes)
197 code
198 (branch
199 DataBytesWord32InputTooShort
200 .
201 b"ALPHA-DATA-BYTES-001")
202 (branch
203 DataBytesWord64InputTooShort
204 .
205 b"ALPHA-DATA-BYTES-002")
206 (branch
207 DataBytesLengthOverflow
208 .
209 b"ALPHA-DATA-BYTES-003")
210 (branch
211 DataBytesOffsetOverflow
212 .
213 b"ALPHA-DATA-BYTES-004")
214 (branch
215 DataBytesOffsetOutOfRange
216 .
217 b"ALPHA-DATA-BYTES-005")
218 (branch
219 DataBytesIndexOutOfRange
220 .
221 b"ALPHA-DATA-BYTES-006")
222 (branch
223 DataBytesSliceOutOfRange
224 .
225 b"ALPHA-DATA-BYTES-007")
226 (branch
227 DataBytesWord32MalformedLength
228 .
229 b"ALPHA-DATA-BYTES-008")
230 (branch
231 DataBytesWord64MalformedLength
232 .
233 b"ALPHA-DATA-BYTES-009")
234 (branch
235 DataBytesAllocationLimitExceeded
236 .
237 b"ALPHA-DATA-BYTES-010")
238 (branch
239 DataBytesBuilderInvariantViolation
240 .
241 b"ALPHA-DATA-BYTES-011")))
242
243def dataBytesTelemetry =
244 (lambda unrestricted inputBytes : Nat .
245 (lambda unrestricted requestedBytes : Nat .
246 (lambda unrestricted outputBytes : Nat .
247 (lambda unrestricted chunks : Nat .
248 (lambda unrestricted sharedBytes : Nat .
249 (lambda unrestricted preparationCopiedBytes : Nat .
250 (lambda unrestricted visitedBytes : Nat .
251 (lambda unrestricted allocationLimit : Nat .
252 (constructor
253 DataBytesTelemetry
254 DataBytesTelemetryValue
255 inputBytes
256 requestedBytes
257 outputBytes
258 chunks
259 sharedBytes
260 preparationCopiedBytes
261 visitedBytes
262 allocationLimit)))))))))
263
264def dataBytesZeroTelemetry =
265 (lambda unrestricted allocationLimit : Nat .
266 (dataBytesTelemetry zero zero zero zero zero zero zero allocationLimit))
267
268-- Check before addition. Runtime Nat is machine-sized, so a post-add check could
269-- observe a wrapped value and is not acceptable.
270def dataBytesCheckedAddWithin =
271 (lambda unrestricted limit : Nat .
272 (lambda unrestricted failure : (family DataBytesErrorCode) .
273 (lambda unrestricted left : Nat .
274 (lambda unrestricted right : Nat .
275 (nat-eliminate
276 (lambda unrestricted current : Nat . (family DataBytesCheckedNaturalResult))
277 (constructor DataBytesCheckedNaturalResult DataBytesCheckedNaturalFailed failure)
278 (lambda unrestricted leftFitsPredecessor : Nat .
279 (lambda unrestricted leftFitsInduction : (family DataBytesCheckedNaturalResult) .
280 (nat-eliminate
281 (lambda unrestricted current : Nat . (family DataBytesCheckedNaturalResult))
282 (constructor DataBytesCheckedNaturalResult DataBytesCheckedNaturalFailed failure)
283 (lambda unrestricted rightFitsPredecessor : Nat .
284 (lambda unrestricted rightFitsInduction : (family DataBytesCheckedNaturalResult) .
285 (constructor
286 DataBytesCheckedNaturalResult
287 DataBytesCheckedNaturalSucceeded
288 (naturalAdd left right))))
289 (naturalLessOrEqual right (naturalSaturatingSubtract limit left)))))
290 (naturalLessOrEqual left limit))))))
291
292def dataBytesCheckedLengthAdd =
293 (dataBytesCheckedAddWithin
294 dataBytesDefaultAllocationLimit
295 (constructor DataBytesErrorCode DataBytesLengthOverflow))
296
297def dataBytesCheckedOffsetAdd =
298 (dataBytesCheckedAddWithin
299 dataBytesDefaultAllocationLimit
300 (constructor DataBytesErrorCode DataBytesOffsetOverflow))
301
302-- These helpers are called only after a public bounds proof.
303def dataBytesDropValidated =
304 (lambda unrestricted count : Nat .
305 (nat-eliminate
306 (lambda unrestricted current : Nat . (pi unrestricted input : Bytes . Bytes))
307 (lambda unrestricted input : Bytes . input)
308 (lambda unrestricted predecessor : Nat .
309 (lambda unrestricted induction : (pi unrestricted input : Bytes . Bytes) .
310 (lambda unrestricted input : Bytes . (induction (bytes-tail input)))))
311 count))
312
313-- Build the prefix once. Repeated bytes-cons copies every growing suffix in
314-- the native evaluator, making a large imported normalization table quadratic.
315-- A builder retains each byte as a chunk and materializes the prefix linearly.
316-- Keep the total helper's old zero-padding behavior past the end; public
317-- bounded slices reject those requests before calling this helper.
318def dataBytesTakeBuilder =
319 (lambda unrestricted count : Nat .
320 (nat-eliminate
321 (lambda unrestricted current : Nat . (pi unrestricted input : Bytes . BytesBuilder))
322 (lambda unrestricted input : Bytes . (bytes-builder-empty))
323 (lambda unrestricted predecessor : Nat .
324 (lambda unrestricted induction : (pi unrestricted input : Bytes . BytesBuilder) .
325 (lambda unrestricted input : Bytes .
326 (bytes-builder-append
327 (bytes-builder-chunk (bytes-cons (bytes-head input) b""))
328 (induction (bytes-tail input))))))
329 count))
330
331def dataBytesTakeValidated =
332 (lambda unrestricted count : Nat .
333 (lambda unrestricted input : Bytes .
334 (bytes-builder-build (dataBytesTakeBuilder count input))))
335
336def dataBytesByteAtValidated =
337 (lambda unrestricted input : Bytes .
338 (lambda unrestricted index : Nat . (bytes-head (dataBytesDropValidated index input))))
339
340-- Bytes is the runtime's project-owned immutable byte value.
341def dataBytesEmpty =
342 b""
343
344def dataBytesFromBytes =
345 (lambda unrestricted value : Bytes . value)
346
347def dataBytesToBytes =
348 (lambda unrestricted value : Bytes . value)
349
350-- Repeat a complete chunk, materializing once. This does not repeatedly
351-- copy a growing suffix as bytes-cons/bytes-append in a linear fold would.
352def dataBytesRepeat = (lambda unrestricted chunk : Bytes . (lambda unrestricted count : Nat .
353 (bytes-builder-build (nat-eliminate (lambda unrestricted n : Nat . BytesBuilder)
354 (bytes-builder-empty)
355 (lambda unrestricted index : Nat . (lambda unrestricted previous : BytesBuilder .
356 (bytes-builder-append previous (bytes-builder-chunk chunk)))) count))))
357
358-- Batch single-byte repetitions into 4096-byte chunks. This is a construction
359-- granularity, not a maximum extent: quotient and remainder cover all bytes.
360def dataBytesRepeatByte = (lambda unrestricted value : Byte . (lambda unrestricted count : Nat .
361 (let unrestricted single = (bytes-cons value b"") in
362 (nat-eliminate (lambda unrestricted small : Nat . Bytes)
363 (let unrestricted block = (dataBytesRepeat single 4096) in
364 (bytes-append (dataBytesRepeat block (naturalDivideUnchecked count 4096))
365 (dataBytesRepeat single (naturalModuloUnchecked count 4096))))
366 (lambda unrestricted predecessor : Nat . (lambda unrestricted unused : Bytes .
367 (dataBytesRepeat single count)))
368 (nat-less-than count 4096)))))
369
370def dataBytesLength =
371 (lambda unrestricted value : Bytes . (bytes-length value))
372
373def dataBytesEqual =
374 (lambda unrestricted left : Bytes .
375 (lambda unrestricted right : Bytes . (bytes-equal left right)))
376
377def dataBytesCompare =
378 (lambda unrestricted left : Bytes .
379 (bytes-eliminate
380 (lambda unrestricted current : Bytes .
381 (pi unrestricted right : Bytes . (family DataBytesOrdering)))
382 (lambda unrestricted right : Bytes .
383 (bytes-eliminate
384 (lambda unrestricted current : Bytes . (family DataBytesOrdering))
385 (constructor DataBytesOrdering DataBytesEqual)
386 (lambda unrestricted rightHead : Byte .
387 (lambda unrestricted rightTail : Bytes .
388 (lambda unrestricted rightInduction : (family DataBytesOrdering) .
389 (constructor DataBytesOrdering DataBytesLess))))
390 right))
391 (lambda unrestricted leftHead : Byte .
392 (lambda unrestricted leftTail : Bytes .
393 (lambda unrestricted leftInduction : (pi unrestricted right : Bytes . (family DataBytesOrdering)) .
394 (lambda unrestricted right : Bytes .
395 (bytes-eliminate
396 (lambda unrestricted current : Bytes . (family DataBytesOrdering))
397 (constructor DataBytesOrdering DataBytesGreater)
398 (lambda unrestricted rightHead : Byte .
399 (lambda unrestricted rightTail : Bytes .
400 (lambda unrestricted rightInduction : (family DataBytesOrdering) .
401 (nat-eliminate
402 (lambda unrestricted current : Nat . (family DataBytesOrdering))
403 (nat-eliminate
404 (lambda unrestricted current : Nat . (family DataBytesOrdering))
405 (constructor DataBytesOrdering DataBytesGreater)
406 (lambda unrestricted lessPredecessor : Nat .
407 (lambda unrestricted lessInduction : (family DataBytesOrdering) .
408 (constructor DataBytesOrdering DataBytesLess)))
409 (byte-less-than leftHead rightHead))
410 (lambda unrestricted equalPredecessor : Nat .
411 (lambda unrestricted equalInduction : (family DataBytesOrdering) .
412 (leftInduction rightTail)))
413 (byte-equal leftHead rightHead)))))
414 right)))))
415 left))
416
417def dataBytesIndex =
418 (lambda unrestricted input : Bytes .
419 (lambda unrestricted index : Nat .
420 (app
421 (lambda unrestricted inputLength : Nat .
422 (nat-eliminate
423 (lambda unrestricted current : Nat . (family DataBytesIndexResult))
424 (constructor
425 DataBytesIndexResult
426 DataBytesIndexFailed
427 (constructor DataBytesErrorCode DataBytesIndexOutOfRange)
428 (dataBytesTelemetry
429 inputLength
430 dataBytesNaturalOne
431 zero
432 zero
433 zero
434 zero
435 index
436 inputLength))
437 (lambda unrestricted fitsPredecessor : Nat .
438 (lambda unrestricted fitsInduction : (family DataBytesIndexResult) .
439 (constructor
440 DataBytesIndexResult
441 DataBytesIndexSucceeded
442 (dataBytesByteAtValidated input index)
443 (dataBytesTelemetry
444 inputLength
445 dataBytesNaturalOne
446 dataBytesNaturalOne
447 zero
448 dataBytesNaturalOne
449 zero
450 index
451 inputLength))))
452 (naturalLess index inputLength)))
453 (bytes-length input))))
454
455def dataBytesSlice =
456 (lambda unrestricted input : Bytes .
457 (lambda unrestricted offset : Nat .
458 (lambda unrestricted requestedLength : Nat .
459 (app
460 (lambda unrestricted inputLength : Nat .
461 (nat-eliminate
462 (lambda unrestricted current : Nat . (family DataBytesSliceResult))
463 (constructor
464 DataBytesSliceResult
465 DataBytesSliceFailed
466 (constructor DataBytesErrorCode DataBytesOffsetOutOfRange)
467 (dataBytesTelemetry
468 inputLength
469 requestedLength
470 zero
471 zero
472 zero
473 zero
474 zero
475 inputLength))
476 (lambda unrestricted offsetFitsPredecessor : Nat .
477 (lambda unrestricted offsetFitsInduction : (family DataBytesSliceResult) .
478 (nat-eliminate
479 (lambda unrestricted current : Nat . (family DataBytesSliceResult))
480 (constructor
481 DataBytesSliceResult
482 DataBytesSliceFailed
483 (constructor DataBytesErrorCode DataBytesSliceOutOfRange)
484 (dataBytesTelemetry
485 inputLength
486 requestedLength
487 zero
488 zero
489 zero
490 zero
491 offset
492 inputLength))
493 (lambda unrestricted lengthFitsPredecessor : Nat .
494 (lambda unrestricted lengthFitsInduction : (family DataBytesSliceResult) .
495 (constructor
496 DataBytesSliceResult
497 DataBytesSliceSucceeded
498 (constructor
499 DataBytesSlice
500 DataBytesSliceView
501 (dataBytesDropValidated offset input)
502 requestedLength)
503 (dataBytesTelemetry
504 inputLength
505 requestedLength
506 zero
507 zero
508 requestedLength
509 zero
510 offset
511 inputLength))))
512 (naturalLessOrEqual
513 requestedLength
514 (naturalSaturatingSubtract inputLength offset)))))
515 (naturalLessOrEqual offset inputLength)))
516 (bytes-length input)))))
517
518def dataBytesSliceToBytesWithin =
519 (lambda unrestricted allocationLimit : Nat .
520 (lambda unrestricted slice : (family DataBytesSlice) .
521 (eliminate
522 DataBytesSlice
523 (lambda unrestricted current : (family DataBytesSlice) . (family DataBytesResult))
524 slice
525 (branch
526 DataBytesSliceView
527 suffix
528 requestedLength
529 .
530 (app
531 (lambda unrestricted suffixLength : Nat .
532 (nat-eliminate
533 (lambda unrestricted current : Nat . (family DataBytesResult))
534 (constructor
535 DataBytesResult
536 DataBytesFailed
537 (constructor DataBytesErrorCode DataBytesBuilderInvariantViolation)
538 (dataBytesTelemetry
539 suffixLength
540 requestedLength
541 zero
542 zero
543 zero
544 zero
545 zero
546 allocationLimit))
547 (lambda unrestricted validPredecessor : Nat .
548 (lambda unrestricted validInduction : (family DataBytesResult) .
549 (nat-eliminate
550 (lambda unrestricted current : Nat . (family DataBytesResult))
551 (constructor
552 DataBytesResult
553 DataBytesFailed
554 (constructor DataBytesErrorCode DataBytesAllocationLimitExceeded)
555 (dataBytesTelemetry
556 suffixLength
557 requestedLength
558 zero
559 zero
560 requestedLength
561 zero
562 zero
563 allocationLimit))
564 (lambda unrestricted limitPredecessor : Nat .
565 (lambda unrestricted limitInduction : (family DataBytesResult) .
566 (nat-eliminate
567 (lambda unrestricted current : Nat . (family DataBytesResult))
568 (constructor
569 DataBytesResult
570 DataBytesSucceeded
571 (dataBytesTakeValidated requestedLength suffix)
572 (dataBytesTelemetry
573 suffixLength
574 requestedLength
575 requestedLength
576 dataBytesNaturalOne
577 zero
578 requestedLength
579 requestedLength
580 allocationLimit))
581 (lambda unrestricted wholePredecessor : Nat .
582 (lambda unrestricted wholeInduction : (family DataBytesResult) .
583 (constructor
584 DataBytesResult
585 DataBytesSucceeded
586 suffix
587 (dataBytesTelemetry
588 suffixLength
589 requestedLength
590 requestedLength
591 dataBytesNaturalOne
592 requestedLength
593 zero
594 zero
595 allocationLimit))))
596 (naturalEqual requestedLength suffixLength))))
597 (naturalLessOrEqual requestedLength allocationLimit))))
598 (naturalLessOrEqual requestedLength suffixLength)))
599 (bytes-length suffix))))))
600
601def dataBytesSliceToBytes =
602 (dataBytesSliceToBytesWithin dataBytesDefaultAllocationLimit)
603
604def dataBytesSliceIndex =
605 (lambda unrestricted slice : (family DataBytesSlice) .
606 (lambda unrestricted index : Nat .
607 (eliminate
608 DataBytesSlice
609 (lambda unrestricted current : (family DataBytesSlice) . (family DataBytesIndexResult))
610 slice
611 (branch
612 DataBytesSliceView
613 suffix
614 sliceLength
615 .
616 (app
617 (lambda unrestricted suffixLength : Nat .
618 (nat-eliminate
619 (lambda unrestricted current : Nat . (family DataBytesIndexResult))
620 (constructor
621 DataBytesIndexResult
622 DataBytesIndexFailed
623 (constructor DataBytesErrorCode DataBytesBuilderInvariantViolation)
624 (dataBytesTelemetry
625 suffixLength
626 dataBytesNaturalOne
627 zero
628 zero
629 zero
630 zero
631 zero
632 suffixLength))
633 (lambda unrestricted validPredecessor : Nat .
634 (lambda unrestricted validInduction : (family DataBytesIndexResult) .
635 (nat-eliminate
636 (lambda unrestricted current : Nat . (family DataBytesIndexResult))
637 (constructor
638 DataBytesIndexResult
639 DataBytesIndexFailed
640 (constructor DataBytesErrorCode DataBytesIndexOutOfRange)
641 (dataBytesTelemetry
642 sliceLength
643 dataBytesNaturalOne
644 zero
645 zero
646 zero
647 zero
648 index
649 sliceLength))
650 (lambda unrestricted fitsPredecessor : Nat .
651 (lambda unrestricted fitsInduction : (family DataBytesIndexResult) .
652 (constructor
653 DataBytesIndexResult
654 DataBytesIndexSucceeded
655 (dataBytesByteAtValidated suffix index)
656 (dataBytesTelemetry
657 sliceLength
658 dataBytesNaturalOne
659 dataBytesNaturalOne
660 zero
661 dataBytesNaturalOne
662 zero
663 index
664 sliceLength))))
665 (naturalLess index sliceLength))))
666 (naturalLessOrEqual sliceLength suffixLength)))
667 (bytes-length suffix))))))
668
669def dataBytesBuilderEmpty =
670 (constructor DataBytesBuilder DataBytesBuilderValue (bytes-builder-empty) zero zero zero zero)
671
672-- Valid builders have no empty chunks and partition their length into shared
673-- source bytes and bytes copied while preparing bounded slices.
674def dataBytesBuilderMetadataValid =
675 (lambda unrestricted length : Nat .
676 (lambda unrestricted chunks : Nat .
677 (lambda unrestricted sharedBytes : Nat .
678 (lambda unrestricted preparationCopiedBytes : Nat .
679 (nat-eliminate
680 (lambda unrestricted current : Nat . Nat)
681 zero
682 (lambda unrestricted basicPredecessor : Nat .
683 (lambda unrestricted basicInduction : Nat .
684 (nat-eliminate
685 (lambda unrestricted current : Nat . Nat)
686 zero
687 (lambda unrestricted sumPredecessor : Nat .
688 (lambda unrestricted sumInduction : Nat .
689 (naturalEqual (naturalAdd sharedBytes preparationCopiedBytes) length)))
690 (naturalLessOrEqual
691 preparationCopiedBytes
692 (naturalSaturatingSubtract length sharedBytes)))))
693 (naturalAnd (naturalLessOrEqual chunks length) (naturalLessOrEqual sharedBytes length)))))))
694
695def dataBytesBuilderChunkWithin =
696 (lambda unrestricted allocationLimit : Nat .
697 (lambda unrestricted chunk : Bytes .
698 (app
699 (lambda unrestricted chunkLength : Nat .
700 (nat-eliminate
701 (lambda unrestricted current : Nat . (family DataBytesBuilderResult))
702 (constructor
703 DataBytesBuilderResult
704 DataBytesBuilderFailed
705 (constructor DataBytesErrorCode DataBytesAllocationLimitExceeded)
706 (dataBytesTelemetry chunkLength chunkLength zero zero zero zero zero allocationLimit))
707 (lambda unrestricted fitsPredecessor : Nat .
708 (lambda unrestricted fitsInduction : (family DataBytesBuilderResult) .
709 (nat-eliminate
710 (lambda unrestricted current : Nat . (family DataBytesBuilderResult))
711 (constructor
712 DataBytesBuilderResult
713 DataBytesBuilderSucceeded
714 dataBytesBuilderEmpty
715 (dataBytesZeroTelemetry allocationLimit))
716 (lambda unrestricted nonemptyPredecessor : Nat .
717 (lambda unrestricted nonemptyInduction : (family DataBytesBuilderResult) .
718 (constructor
719 DataBytesBuilderResult
720 DataBytesBuilderSucceeded
721 (constructor
722 DataBytesBuilder
723 DataBytesBuilderValue
724 (bytes-builder-chunk chunk)
725 chunkLength
726 dataBytesNaturalOne
727 chunkLength
728 zero)
729 (dataBytesTelemetry
730 chunkLength
731 chunkLength
732 zero
733 dataBytesNaturalOne
734 chunkLength
735 zero
736 zero
737 allocationLimit))))
738 chunkLength)))
739 (naturalLessOrEqual chunkLength allocationLimit)))
740 (bytes-length chunk))))
741
742def dataBytesBuilderChunk =
743 (dataBytesBuilderChunkWithin dataBytesDefaultAllocationLimit)
744
745def dataBytesBuilderAppendCheckedValues =
746 (lambda unrestricted allocationLimit : Nat .
747 (lambda unrestricted leftRuntime : BytesBuilder .
748 (lambda unrestricted leftLength : Nat .
749 (lambda unrestricted leftChunks : Nat .
750 (lambda unrestricted leftShared : Nat .
751 (lambda unrestricted leftCopied : Nat .
752 (lambda unrestricted rightRuntime : BytesBuilder .
753 (lambda unrestricted rightLength : Nat .
754 (lambda unrestricted rightChunks : Nat .
755 (lambda unrestricted rightShared : Nat .
756 (lambda unrestricted rightCopied : Nat .
757 (eliminate
758 DataBytesCheckedNaturalResult
759 (lambda unrestricted current : (family DataBytesCheckedNaturalResult) .
760 (family DataBytesBuilderResult))
761 (dataBytesCheckedAddWithin
762 allocationLimit
763 (constructor DataBytesErrorCode DataBytesAllocationLimitExceeded)
764 leftLength
765 rightLength)
766 (branch
767 DataBytesCheckedNaturalSucceeded
768 totalLength
769 .
770 (constructor
771 DataBytesBuilderResult
772 DataBytesBuilderSucceeded
773 (constructor
774 DataBytesBuilder
775 DataBytesBuilderValue
776 (bytes-builder-append leftRuntime rightRuntime)
777 totalLength
778 (naturalAdd leftChunks rightChunks)
779 (naturalAdd leftShared rightShared)
780 (naturalAdd leftCopied rightCopied))
781 (dataBytesTelemetry
782 totalLength
783 totalLength
784 zero
785 (naturalAdd leftChunks rightChunks)
786 (naturalAdd leftShared rightShared)
787 (naturalAdd leftCopied rightCopied)
788 zero
789 allocationLimit)))
790 (branch
791 DataBytesCheckedNaturalFailed
792 code
793 .
794 (constructor
795 DataBytesBuilderResult
796 DataBytesBuilderFailed
797 code
798 (dataBytesTelemetry
799 leftLength
800 rightLength
801 zero
802 zero
803 zero
804 zero
805 zero
806 allocationLimit)))))))))))))))
807
808def dataBytesBuilderAppendWithin =
809 (lambda unrestricted allocationLimit : Nat .
810 (lambda unrestricted left : (family DataBytesBuilder) .
811 (lambda unrestricted right : (family DataBytesBuilder) .
812 (eliminate
813 DataBytesBuilder
814 (lambda unrestricted current : (family DataBytesBuilder) .
815 (family DataBytesBuilderResult))
816 left
817 (branch
818 DataBytesBuilderValue
819 leftRuntime
820 leftLength
821 leftChunks
822 leftShared
823 leftCopied
824 .
825 (eliminate
826 DataBytesBuilder
827 (lambda unrestricted current : (family DataBytesBuilder) .
828 (family DataBytesBuilderResult))
829 right
830 (branch
831 DataBytesBuilderValue
832 rightRuntime
833 rightLength
834 rightChunks
835 rightShared
836 rightCopied
837 .
838 (nat-eliminate
839 (lambda unrestricted current : Nat . (family DataBytesBuilderResult))
840 (constructor
841 DataBytesBuilderResult
842 DataBytesBuilderFailed
843 (constructor DataBytesErrorCode DataBytesBuilderInvariantViolation)
844 (dataBytesZeroTelemetry allocationLimit))
845 (lambda unrestricted validPredecessor : Nat .
846 (lambda unrestricted validInduction : (family DataBytesBuilderResult) .
847 (dataBytesBuilderAppendCheckedValues
848 allocationLimit
849 leftRuntime
850 leftLength
851 leftChunks
852 leftShared
853 leftCopied
854 rightRuntime
855 rightLength
856 rightChunks
857 rightShared
858 rightCopied)))
859 (naturalAnd
860 (dataBytesBuilderMetadataValid leftLength leftChunks leftShared leftCopied)
861 (dataBytesBuilderMetadataValid rightLength rightChunks rightShared rightCopied))))))))))
862
863def dataBytesBuilderAppend =
864 (dataBytesBuilderAppendWithin dataBytesDefaultAllocationLimit)
865
866def dataBytesBuilderBuildWithin =
867 (lambda unrestricted allocationLimit : Nat .
868 (lambda unrestricted builder : (family DataBytesBuilder) .
869 (eliminate
870 DataBytesBuilder
871 (lambda unrestricted current : (family DataBytesBuilder) . (family DataBytesResult))
872 builder
873 (branch
874 DataBytesBuilderValue
875 runtime
876 length
877 chunks
878 shared
879 copied
880 .
881 (nat-eliminate
882 (lambda unrestricted current : Nat . (family DataBytesResult))
883 (constructor
884 DataBytesResult
885 DataBytesFailed
886 (constructor DataBytesErrorCode DataBytesBuilderInvariantViolation)
887 (dataBytesZeroTelemetry allocationLimit))
888 (lambda unrestricted validPredecessor : Nat .
889 (lambda unrestricted validInduction : (family DataBytesResult) .
890 (nat-eliminate
891 (lambda unrestricted current : Nat . (family DataBytesResult))
892 (constructor
893 DataBytesResult
894 DataBytesFailed
895 (constructor DataBytesErrorCode DataBytesAllocationLimitExceeded)
896 (dataBytesTelemetry
897 length
898 length
899 zero
900 chunks
901 shared
902 copied
903 zero
904 allocationLimit))
905 (lambda unrestricted fitsPredecessor : Nat .
906 (lambda unrestricted fitsInduction : (family DataBytesResult) .
907 (app
908 (lambda unrestricted output : Bytes .
909 (nat-eliminate
910 (lambda unrestricted current : Nat . (family DataBytesResult))
911 (constructor
912 DataBytesResult
913 DataBytesFailed
914 (constructor DataBytesErrorCode DataBytesBuilderInvariantViolation)
915 (dataBytesTelemetry
916 length
917 length
918 zero
919 chunks
920 shared
921 copied
922 length
923 allocationLimit))
924 (lambda unrestricted exactPredecessor : Nat .
925 (lambda unrestricted exactInduction : (family DataBytesResult) .
926 (constructor
927 DataBytesResult
928 DataBytesSucceeded
929 output
930 (dataBytesTelemetry
931 length
932 length
933 length
934 chunks
935 shared
936 copied
937 length
938 allocationLimit))))
939 (naturalEqual (bytes-length output) length)))
940 (bytes-builder-build runtime))))
941 (naturalLessOrEqual length allocationLimit))))
942 (dataBytesBuilderMetadataValid length chunks shared copied))))))
943
944def dataBytesBuilderBuild =
945 (dataBytesBuilderBuildWithin dataBytesDefaultAllocationLimit)
946
947def dataBytesConcatWithin =
948 dataBytesBuilderBuildWithin
949
950def dataBytesConcat =
951 dataBytesBuilderBuild
952
953def dataBytesAppendWithin =
954 (lambda unrestricted allocationLimit : Nat .
955 (lambda unrestricted left : Bytes .
956 (lambda unrestricted right : Bytes .
957 (app
958 (lambda unrestricted leftLength : Nat .
959 (app
960 (lambda unrestricted rightLength : Nat .
961 (eliminate
962 DataBytesCheckedNaturalResult
963 (lambda unrestricted current : (family DataBytesCheckedNaturalResult) .
964 (family DataBytesResult))
965 (dataBytesCheckedAddWithin
966 allocationLimit
967 (constructor DataBytesErrorCode DataBytesAllocationLimitExceeded)
968 leftLength
969 rightLength)
970 (branch
971 DataBytesCheckedNaturalSucceeded
972 totalLength
973 .
974 (app
975 (lambda unrestricted output : Bytes .
976 (constructor
977 DataBytesResult
978 DataBytesSucceeded
979 output
980 (dataBytesTelemetry
981 totalLength
982 totalLength
983 totalLength
984 dataBytesNaturalTwo
985 totalLength
986 zero
987 totalLength
988 allocationLimit)))
989 (bytes-builder-build
990 (bytes-builder-append
991 (bytes-builder-chunk left)
992 (bytes-builder-chunk right)))))
993 (branch
994 DataBytesCheckedNaturalFailed
995 code
996 .
997 (constructor
998 DataBytesResult
999 DataBytesFailed
1000 code
1001 (dataBytesTelemetry
1002 leftLength
1003 rightLength
1004 zero
1005 zero
1006 zero
1007 zero
1008 zero
1009 allocationLimit)))))
1010 (bytes-length right)))
1011 (bytes-length left)))))
1012
1013def dataBytesAppendChecked =
1014 (dataBytesAppendWithin dataBytesDefaultAllocationLimit)
1015
1016-- Bootstrap-compatible append now uses a two-chunk build rather than list-like
1017-- nested bytesAppend. Bulk callers use DataBytesBuilder and build exactly once.
1018def dataBytesAppend =
1019 (lambda unrestricted left : Bytes .
1020 (lambda unrestricted right : Bytes .
1021 (bytes-builder-build
1022 (bytes-builder-append (bytes-builder-chunk left) (bytes-builder-chunk right)))))
1023
1024def dataBytesWord32LE =
1025 (lambda unrestricted value : (family ModelWord32) .
1026 (eliminate
1027 ModelWord32
1028 (lambda unrestricted current : (family ModelWord32) . Bytes)
1029 value
1030 (branch
1031 ModelWord32Value
1032 b0
1033 b1
1034 b2
1035 b3
1036 .
1037 (bytes-cons b0 (bytes-cons b1 (bytes-cons b2 (bytes-cons b3 b"")))))))
1038
1039def dataBytesWord32BE =
1040 (lambda unrestricted value : (family ModelWord32) .
1041 (eliminate
1042 ModelWord32
1043 (lambda unrestricted current : (family ModelWord32) . Bytes)
1044 value
1045 (branch
1046 ModelWord32Value
1047 b0
1048 b1
1049 b2
1050 b3
1051 .
1052 (bytes-cons b3 (bytes-cons b2 (bytes-cons b1 (bytes-cons b0 b"")))))))
1053
1054def dataBytesWord64LE =
1055 (lambda unrestricted value : (family ModelWord64) .
1056 (eliminate
1057 ModelWord64
1058 (lambda unrestricted current : (family ModelWord64) . Bytes)
1059 value
1060 (branch
1061 ModelWord64Value
1062 b0
1063 b1
1064 b2
1065 b3
1066 b4
1067 b5
1068 b6
1069 b7
1070 .
1071 (bytes-cons
1072 b0
1073 (bytes-cons
1074 b1
1075 (bytes-cons
1076 b2
1077 (bytes-cons
1078 b3
1079 (bytes-cons b4 (bytes-cons b5 (bytes-cons b6 (bytes-cons b7 b"")))))))))))
1080
1081def dataBytesWord64BE =
1082 (lambda unrestricted value : (family ModelWord64) .
1083 (eliminate
1084 ModelWord64
1085 (lambda unrestricted current : (family ModelWord64) . Bytes)
1086 value
1087 (branch
1088 ModelWord64Value
1089 b0
1090 b1
1091 b2
1092 b3
1093 b4
1094 b5
1095 b6
1096 b7
1097 .
1098 (bytes-cons
1099 b7
1100 (bytes-cons
1101 b6
1102 (bytes-cons
1103 b5
1104 (bytes-cons
1105 b4
1106 (bytes-cons b3 (bytes-cons b2 (bytes-cons b1 (bytes-cons b0 b"")))))))))))
1107
1108def dataBytesWord32Failure =
1109 (constructor
1110 DataBytesWord32DecodeResult
1111 DataBytesWord32DecodeFailed
1112 (constructor DataBytesErrorCode DataBytesWord32InputTooShort))
1113
1114def dataBytesWord64Failure =
1115 (constructor
1116 DataBytesWord64DecodeResult
1117 DataBytesWord64DecodeFailed
1118 (constructor DataBytesErrorCode DataBytesWord64InputTooShort))
1119
1120def dataBytesReadWord32LE =
1121 (lambda unrestricted input : Bytes .
1122 (nat-eliminate
1123 (lambda unrestricted current : Nat . (family DataBytesWord32DecodeResult))
1124 dataBytesWord32Failure
1125 (lambda unrestricted fitsPredecessor : Nat .
1126 (lambda unrestricted fitsInduction : (family DataBytesWord32DecodeResult) .
1127 (constructor
1128 DataBytesWord32DecodeResult
1129 DataBytesWord32Decoded
1130 (constructor
1131 ModelWord32
1132 ModelWord32Value
1133 (dataBytesByteAtValidated input zero)
1134 (dataBytesByteAtValidated input dataBytesNaturalOne)
1135 (dataBytesByteAtValidated input dataBytesNaturalTwo)
1136 (dataBytesByteAtValidated input dataBytesNaturalThree))
1137 (dataBytesDropValidated dataBytesNaturalFour input))))
1138 (naturalLessOrEqual dataBytesNaturalFour (bytes-length input))))
1139
1140def dataBytesReadWord32BE =
1141 (lambda unrestricted input : Bytes .
1142 (nat-eliminate
1143 (lambda unrestricted current : Nat . (family DataBytesWord32DecodeResult))
1144 dataBytesWord32Failure
1145 (lambda unrestricted fitsPredecessor : Nat .
1146 (lambda unrestricted fitsInduction : (family DataBytesWord32DecodeResult) .
1147 (constructor
1148 DataBytesWord32DecodeResult
1149 DataBytesWord32Decoded
1150 (constructor
1151 ModelWord32
1152 ModelWord32Value
1153 (dataBytesByteAtValidated input dataBytesNaturalThree)
1154 (dataBytesByteAtValidated input dataBytesNaturalTwo)
1155 (dataBytesByteAtValidated input dataBytesNaturalOne)
1156 (dataBytesByteAtValidated input zero))
1157 (dataBytesDropValidated dataBytesNaturalFour input))))
1158 (naturalLessOrEqual dataBytesNaturalFour (bytes-length input))))
1159
1160def dataBytesReadWord64LE =
1161 (lambda unrestricted input : Bytes .
1162 (nat-eliminate
1163 (lambda unrestricted current : Nat . (family DataBytesWord64DecodeResult))
1164 dataBytesWord64Failure
1165 (lambda unrestricted fitsPredecessor : Nat .
1166 (lambda unrestricted fitsInduction : (family DataBytesWord64DecodeResult) .
1167 (constructor
1168 DataBytesWord64DecodeResult
1169 DataBytesWord64Decoded
1170 (constructor
1171 ModelWord64
1172 ModelWord64Value
1173 (dataBytesByteAtValidated input zero)
1174 (dataBytesByteAtValidated input dataBytesNaturalOne)
1175 (dataBytesByteAtValidated input dataBytesNaturalTwo)
1176 (dataBytesByteAtValidated input dataBytesNaturalThree)
1177 (dataBytesByteAtValidated input dataBytesNaturalFour)
1178 (dataBytesByteAtValidated input dataBytesNaturalFive)
1179 (dataBytesByteAtValidated input dataBytesNaturalSix)
1180 (dataBytesByteAtValidated input dataBytesNaturalSeven))
1181 (dataBytesDropValidated dataBytesNaturalEight input))))
1182 (naturalLessOrEqual dataBytesNaturalEight (bytes-length input))))
1183
1184def dataBytesReadWord64BE =
1185 (lambda unrestricted input : Bytes .
1186 (nat-eliminate
1187 (lambda unrestricted current : Nat . (family DataBytesWord64DecodeResult))
1188 dataBytesWord64Failure
1189 (lambda unrestricted fitsPredecessor : Nat .
1190 (lambda unrestricted fitsInduction : (family DataBytesWord64DecodeResult) .
1191 (constructor
1192 DataBytesWord64DecodeResult
1193 DataBytesWord64Decoded
1194 (constructor
1195 ModelWord64
1196 ModelWord64Value
1197 (dataBytesByteAtValidated input dataBytesNaturalSeven)
1198 (dataBytesByteAtValidated input dataBytesNaturalSix)
1199 (dataBytesByteAtValidated input dataBytesNaturalFive)
1200 (dataBytesByteAtValidated input dataBytesNaturalFour)
1201 (dataBytesByteAtValidated input dataBytesNaturalThree)
1202 (dataBytesByteAtValidated input dataBytesNaturalTwo)
1203 (dataBytesByteAtValidated input dataBytesNaturalOne)
1204 (dataBytesByteAtValidated input zero))
1205 (dataBytesDropValidated dataBytesNaturalEight input))))
1206 (naturalLessOrEqual dataBytesNaturalEight (bytes-length input))))
1207
1208def dataBytesWord32ExactFailure =
1209 (lambda unrestricted inputLength : Nat .
1210 (constructor
1211 DataBytesWord32ExactDecodeResult
1212 DataBytesWord32ExactDecodeFailed
1213 (constructor DataBytesErrorCode DataBytesWord32MalformedLength)
1214 (dataBytesTelemetry
1215 inputLength
1216 dataBytesNaturalFour
1217 zero
1218 zero
1219 zero
1220 zero
1221 inputLength
1222 dataBytesNaturalFour)))
1223
1224def dataBytesWord64ExactFailure =
1225 (lambda unrestricted inputLength : Nat .
1226 (constructor
1227 DataBytesWord64ExactDecodeResult
1228 DataBytesWord64ExactDecodeFailed
1229 (constructor DataBytesErrorCode DataBytesWord64MalformedLength)
1230 (dataBytesTelemetry
1231 inputLength
1232 dataBytesNaturalEight
1233 zero
1234 zero
1235 zero
1236 zero
1237 inputLength
1238 dataBytesNaturalEight)))
1239
1240def dataBytesWord32ExactFromStream =
1241 (lambda unrestricted inputLength : Nat .
1242 (lambda unrestricted decoded : (family DataBytesWord32DecodeResult) .
1243 (eliminate
1244 DataBytesWord32DecodeResult
1245 (lambda unrestricted current : (family DataBytesWord32DecodeResult) .
1246 (family DataBytesWord32ExactDecodeResult))
1247 decoded
1248 (branch
1249 DataBytesWord32Decoded
1250 value
1251 remaining
1252 .
1253 (constructor
1254 DataBytesWord32ExactDecodeResult
1255 DataBytesWord32ExactlyDecoded
1256 value
1257 (dataBytesTelemetry
1258 inputLength
1259 dataBytesNaturalFour
1260 dataBytesNaturalFour
1261 dataBytesNaturalOne
1262 inputLength
1263 zero
1264 dataBytesNaturalFour
1265 dataBytesNaturalFour)))
1266 (branch DataBytesWord32DecodeFailed code . (dataBytesWord32ExactFailure inputLength)))))
1267
1268def dataBytesWord64ExactFromStream =
1269 (lambda unrestricted inputLength : Nat .
1270 (lambda unrestricted decoded : (family DataBytesWord64DecodeResult) .
1271 (eliminate
1272 DataBytesWord64DecodeResult
1273 (lambda unrestricted current : (family DataBytesWord64DecodeResult) .
1274 (family DataBytesWord64ExactDecodeResult))
1275 decoded
1276 (branch
1277 DataBytesWord64Decoded
1278 value
1279 remaining
1280 .
1281 (constructor
1282 DataBytesWord64ExactDecodeResult
1283 DataBytesWord64ExactlyDecoded
1284 value
1285 (dataBytesTelemetry
1286 inputLength
1287 dataBytesNaturalEight
1288 dataBytesNaturalEight
1289 dataBytesNaturalOne
1290 inputLength
1291 zero
1292 dataBytesNaturalEight
1293 dataBytesNaturalEight)))
1294 (branch DataBytesWord64DecodeFailed code . (dataBytesWord64ExactFailure inputLength)))))
1295
1296def dataBytesDecodeWord32LEExact =
1297 (lambda unrestricted input : Bytes .
1298 (app
1299 (lambda unrestricted inputLength : Nat .
1300 (nat-eliminate
1301 (lambda unrestricted current : Nat . (family DataBytesWord32ExactDecodeResult))
1302 (dataBytesWord32ExactFailure inputLength)
1303 (lambda unrestricted exactPredecessor : Nat .
1304 (lambda unrestricted exactInduction : (family DataBytesWord32ExactDecodeResult) .
1305 (dataBytesWord32ExactFromStream inputLength (dataBytesReadWord32LE input))))
1306 (naturalEqual inputLength dataBytesNaturalFour)))
1307 (bytes-length input)))
1308
1309def dataBytesDecodeWord32BEExact =
1310 (lambda unrestricted input : Bytes .
1311 (app
1312 (lambda unrestricted inputLength : Nat .
1313 (nat-eliminate
1314 (lambda unrestricted current : Nat . (family DataBytesWord32ExactDecodeResult))
1315 (dataBytesWord32ExactFailure inputLength)
1316 (lambda unrestricted exactPredecessor : Nat .
1317 (lambda unrestricted exactInduction : (family DataBytesWord32ExactDecodeResult) .
1318 (dataBytesWord32ExactFromStream inputLength (dataBytesReadWord32BE input))))
1319 (naturalEqual inputLength dataBytesNaturalFour)))
1320 (bytes-length input)))
1321
1322def dataBytesDecodeWord64LEExact =
1323 (lambda unrestricted input : Bytes .
1324 (app
1325 (lambda unrestricted inputLength : Nat .
1326 (nat-eliminate
1327 (lambda unrestricted current : Nat . (family DataBytesWord64ExactDecodeResult))
1328 (dataBytesWord64ExactFailure inputLength)
1329 (lambda unrestricted exactPredecessor : Nat .
1330 (lambda unrestricted exactInduction : (family DataBytesWord64ExactDecodeResult) .
1331 (dataBytesWord64ExactFromStream inputLength (dataBytesReadWord64LE input))))
1332 (naturalEqual inputLength dataBytesNaturalEight)))
1333 (bytes-length input)))
1334
1335def dataBytesDecodeWord64BEExact =
1336 (lambda unrestricted input : Bytes .
1337 (app
1338 (lambda unrestricted inputLength : Nat .
1339 (nat-eliminate
1340 (lambda unrestricted current : Nat . (family DataBytesWord64ExactDecodeResult))
1341 (dataBytesWord64ExactFailure inputLength)
1342 (lambda unrestricted exactPredecessor : Nat .
1343 (lambda unrestricted exactInduction : (family DataBytesWord64ExactDecodeResult) .
1344 (dataBytesWord64ExactFromStream inputLength (dataBytesReadWord64BE input))))
1345 (naturalEqual inputLength dataBytesNaturalEight)))
1346 (bytes-length input)))
1347
1348def dataBytesHexDigit =
1349 (lambda unrestricted nibble : Nat .
1350 (nat-eliminate
1351 (lambda unrestricted current : Nat . Byte)
1352 (nat-to-byte (naturalAdd (byte-to-nat (byte 87)) nibble))
1353 (lambda unrestricted predecessor : Nat .
1354 (lambda unrestricted induction : Byte .
1355 (nat-to-byte (naturalAdd (byte-to-nat (byte 48)) nibble))))
1356 (naturalLess nibble dataBytesNaturalTen)))
1357
1358def dataBytesRenderHexBuilder =
1359 (lambda unrestricted input : Bytes .
1360 (bytes-eliminate
1361 (lambda unrestricted current : Bytes . BytesBuilder)
1362 (bytes-builder-empty)
1363 (lambda unrestricted head : Byte .
1364 (lambda unrestricted tail : Bytes .
1365 (lambda unrestricted induction : BytesBuilder .
1366 (bytes-builder-append
1367 (bytes-builder-chunk
1368 (bytes-cons
1369 (dataBytesHexDigit
1370 (naturalDivideUnchecked (byte-to-nat head) dataBytesNaturalSixteen))
1371 (bytes-cons
1372 (dataBytesHexDigit
1373 (naturalModuloUnchecked (byte-to-nat head) dataBytesNaturalSixteen))
1374 b"")))
1375 induction))))
1376 input))
1377
1378def dataBytesRenderHexWithin =
1379 (lambda unrestricted allocationLimit : Nat .
1380 (lambda unrestricted input : Bytes .
1381 (app
1382 (lambda unrestricted inputLength : Nat .
1383 (eliminate
1384 DataBytesCheckedNaturalResult
1385 (lambda unrestricted current : (family DataBytesCheckedNaturalResult) .
1386 (family DataBytesResult))
1387 (dataBytesCheckedAddWithin
1388 allocationLimit
1389 (constructor DataBytesErrorCode DataBytesAllocationLimitExceeded)
1390 inputLength
1391 inputLength)
1392 (branch
1393 DataBytesCheckedNaturalSucceeded
1394 outputLength
1395 .
1396 (app
1397 (lambda unrestricted output : Bytes .
1398 (constructor
1399 DataBytesResult
1400 DataBytesSucceeded
1401 output
1402 (dataBytesTelemetry
1403 inputLength
1404 outputLength
1405 outputLength
1406 inputLength
1407 zero
1408 outputLength
1409 inputLength
1410 allocationLimit)))
1411 (bytes-builder-build (dataBytesRenderHexBuilder input))))
1412 (branch
1413 DataBytesCheckedNaturalFailed
1414 code
1415 .
1416 (constructor
1417 DataBytesResult
1418 DataBytesFailed
1419 code
1420 (dataBytesTelemetry
1421 inputLength
1422 inputLength
1423 zero
1424 zero
1425 zero
1426 zero
1427 zero
1428 allocationLimit)))))
1429 (bytes-length input))))
1430
1431def dataBytesRenderHexChecked =
1432 (dataBytesRenderHexWithin dataBytesDefaultAllocationLimit)
1433
1434-- Existing digest consumers require a raw Bytes result. New untrusted inputs use
1435-- dataBytesRenderHexChecked and handle DataBytesFailed.
1436def dataBytesRenderHex =
1437 (lambda unrestricted input : Bytes . (bytes-builder-build (dataBytesRenderHexBuilder input)))
1438
1439-- Eta-expanded primitive wrappers: primitives are not first-class
1440-- values; pass these instead when a function value is needed.
1441def bytesAppend =
1442 (lambda unrestricted left : Bytes .
1443 (lambda unrestricted right : Bytes . (bytes-append left right)))
1444
1445def bytesBuilderFromBytes =
1446 (lambda unrestricted value : Bytes . (bytes-builder-chunk value))
1447
1448def bytesDropLeadingZeroes =
1449 (lambda unrestricted value : Bytes .
1450 (bytes-eliminate
1451 (lambda unrestricted current : Bytes . Bytes)
1452 b""
1453 (lambda unrestricted head : Byte .
1454 (lambda unrestricted tail : Bytes .
1455 (lambda unrestricted induction : Bytes .
1456 (nat-eliminate
1457 (lambda unrestricted headValue : Nat . Bytes)
1458 induction
1459 (lambda unrestricted predecessor : Nat .
1460 (lambda unrestricted keepInduction : Bytes . (bytes-cons head tail)))
1461 (byte-to-nat head)))))
1462 value))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.