module Data.Bytes import Model.Config import Model.Parameter import Std.Byte import Std.Natural -- Stable public failures. Assigned ALPHA-DATA-BYTES codes never change. family DataBytesErrorCode : Type 0 constructor DataBytesWord32InputTooShort constructor DataBytesWord64InputTooShort constructor DataBytesLengthOverflow constructor DataBytesOffsetOverflow constructor DataBytesOffsetOutOfRange constructor DataBytesIndexOutOfRange constructor DataBytesSliceOutOfRange constructor DataBytesWord32MalformedLength constructor DataBytesWord64MalformedLength constructor DataBytesAllocationLimitExceeded constructor DataBytesBuilderInvariantViolation end-family family DataBytesOrdering : Type 0 constructor DataBytesLess constructor DataBytesEqual constructor DataBytesGreater end-family family DataBytesTelemetry : Type 0 constructor DataBytesTelemetryValue field unrestricted dataBytesTelemetryInputBytes : Nat field unrestricted dataBytesTelemetryRequestedBytes : Nat field unrestricted dataBytesTelemetryOutputBytes : Nat field unrestricted dataBytesTelemetryChunks : Nat field unrestricted dataBytesTelemetrySharedBytes : Nat field unrestricted dataBytesTelemetryPreparationCopiedBytes : Nat field unrestricted dataBytesTelemetryVisitedBytes : Nat field unrestricted dataBytesTelemetryAllocationLimit : Nat end-family family DataBytesResult : Type 0 constructor DataBytesSucceeded field unrestricted dataBytesSucceededValue : Bytes field unrestricted dataBytesSucceededTelemetry : (family DataBytesTelemetry) constructor DataBytesFailed field unrestricted dataBytesFailureCode : (family DataBytesErrorCode) field unrestricted dataBytesFailureTelemetry : (family DataBytesTelemetry) end-family family DataBytesCheckedNaturalResult : Type 0 constructor DataBytesCheckedNaturalSucceeded field unrestricted dataBytesCheckedNaturalValue : Nat constructor DataBytesCheckedNaturalFailed field unrestricted dataBytesCheckedNaturalError : (family DataBytesErrorCode) end-family -- A slice retains a suffix of its immutable source and a bounded visible length. family DataBytesSlice : Type 0 constructor DataBytesSliceView field unrestricted dataBytesSliceSuffix : Bytes field unrestricted dataBytesSliceLength : Nat end-family family DataBytesSliceResult : Type 0 constructor DataBytesSliceSucceeded field unrestricted dataBytesSliceSucceededValue : (family DataBytesSlice) field unrestricted dataBytesSliceSucceededTelemetry : (family DataBytesTelemetry) constructor DataBytesSliceFailed field unrestricted dataBytesSliceFailureCode : (family DataBytesErrorCode) field unrestricted dataBytesSliceFailureTelemetry : (family DataBytesTelemetry) end-family family DataBytesIndexResult : Type 0 constructor DataBytesIndexSucceeded field unrestricted dataBytesIndexedByte : Byte field unrestricted dataBytesIndexTelemetry : (family DataBytesTelemetry) constructor DataBytesIndexFailed field unrestricted dataBytesIndexFailureCode : (family DataBytesErrorCode) field unrestricted dataBytesIndexFailureTelemetry : (family DataBytesTelemetry) end-family -- Appending builders creates runtime DAG nodes. No byte payload is copied until -- the one checked bytes-builder-build at the edge of the operation. family DataBytesBuilder : Type 0 constructor DataBytesBuilderValue field unrestricted dataBytesBuilderRuntime : BytesBuilder field unrestricted dataBytesBuilderLength : Nat field unrestricted dataBytesBuilderChunks : Nat field unrestricted dataBytesBuilderSharedBytes : Nat field unrestricted dataBytesBuilderPreparationCopiedBytes : Nat end-family family DataBytesBuilderResult : Type 0 constructor DataBytesBuilderSucceeded field unrestricted dataBytesBuilderSucceededValue : (family DataBytesBuilder) field unrestricted dataBytesBuilderSucceededTelemetry : (family DataBytesTelemetry) constructor DataBytesBuilderFailed field unrestricted dataBytesBuilderFailureCode : (family DataBytesErrorCode) field unrestricted dataBytesBuilderFailureTelemetry : (family DataBytesTelemetry) end-family family DataBytesWord32DecodeResult : Type 0 constructor DataBytesWord32Decoded field unrestricted dataBytesDecodedWord32 : (family ModelWord32) field unrestricted dataBytesWord32Remaining : Bytes constructor DataBytesWord32DecodeFailed field unrestricted dataBytesWord32DecodeError : (family DataBytesErrorCode) end-family family DataBytesWord64DecodeResult : Type 0 constructor DataBytesWord64Decoded field unrestricted dataBytesDecodedWord64 : (family ModelWord64) field unrestricted dataBytesWord64Remaining : Bytes constructor DataBytesWord64DecodeFailed field unrestricted dataBytesWord64DecodeError : (family DataBytesErrorCode) end-family family DataBytesWord32ExactDecodeResult : Type 0 constructor DataBytesWord32ExactlyDecoded field unrestricted dataBytesExactlyDecodedWord32 : (family ModelWord32) field unrestricted dataBytesWord32ExactTelemetry : (family DataBytesTelemetry) constructor DataBytesWord32ExactDecodeFailed field unrestricted dataBytesWord32ExactDecodeError : (family DataBytesErrorCode) field unrestricted dataBytesWord32ExactFailureTelemetry : (family DataBytesTelemetry) end-family family DataBytesWord64ExactDecodeResult : Type 0 constructor DataBytesWord64ExactlyDecoded field unrestricted dataBytesExactlyDecodedWord64 : (family ModelWord64) field unrestricted dataBytesWord64ExactTelemetry : (family DataBytesTelemetry) constructor DataBytesWord64ExactDecodeFailed field unrestricted dataBytesWord64ExactDecodeError : (family DataBytesErrorCode) field unrestricted dataBytesWord64ExactFailureTelemetry : (family DataBytesTelemetry) end-family def dataBytesNaturalOne = (byte-to-nat (byte 1)) def dataBytesNaturalTwo = (byte-to-nat (byte 2)) def dataBytesNaturalThree = (byte-to-nat (byte 3)) def dataBytesNaturalFour = (byte-to-nat (byte 4)) def dataBytesNaturalFive = (byte-to-nat (byte 5)) def dataBytesNaturalSix = (byte-to-nat (byte 6)) def dataBytesNaturalSeven = (byte-to-nat (byte 7)) def dataBytesNaturalEight = (byte-to-nat (byte 8)) def dataBytesNaturalTen = (byte-to-nat (byte 10)) def dataBytesNaturalSixteen = (byte-to-nat (byte 16)) def dataBytesNaturalSixtyFour = (byte-to-nat (byte 64)) def dataBytesNaturalOneThousandTwentyFour = (naturalMultiply dataBytesNaturalSixteen dataBytesNaturalSixtyFour) -- 64 MiB. Callers handling larger artifacts must supply an explicit limit. def dataBytesDefaultAllocationLimit = (naturalMultiply dataBytesNaturalSixtyFour (naturalMultiply dataBytesNaturalOneThousandTwentyFour dataBytesNaturalOneThousandTwentyFour)) def dataBytesErrorCodeBytes = (lambda unrestricted code : (family DataBytesErrorCode) . (eliminate DataBytesErrorCode (lambda unrestricted current : (family DataBytesErrorCode) . Bytes) code (branch DataBytesWord32InputTooShort . b"ALPHA-DATA-BYTES-001") (branch DataBytesWord64InputTooShort . b"ALPHA-DATA-BYTES-002") (branch DataBytesLengthOverflow . b"ALPHA-DATA-BYTES-003") (branch DataBytesOffsetOverflow . b"ALPHA-DATA-BYTES-004") (branch DataBytesOffsetOutOfRange . b"ALPHA-DATA-BYTES-005") (branch DataBytesIndexOutOfRange . b"ALPHA-DATA-BYTES-006") (branch DataBytesSliceOutOfRange . b"ALPHA-DATA-BYTES-007") (branch DataBytesWord32MalformedLength . b"ALPHA-DATA-BYTES-008") (branch DataBytesWord64MalformedLength . b"ALPHA-DATA-BYTES-009") (branch DataBytesAllocationLimitExceeded . b"ALPHA-DATA-BYTES-010") (branch DataBytesBuilderInvariantViolation . b"ALPHA-DATA-BYTES-011"))) def dataBytesTelemetry = (lambda unrestricted inputBytes : Nat . (lambda unrestricted requestedBytes : Nat . (lambda unrestricted outputBytes : Nat . (lambda unrestricted chunks : Nat . (lambda unrestricted sharedBytes : Nat . (lambda unrestricted preparationCopiedBytes : Nat . (lambda unrestricted visitedBytes : Nat . (lambda unrestricted allocationLimit : Nat . (constructor DataBytesTelemetry DataBytesTelemetryValue inputBytes requestedBytes outputBytes chunks sharedBytes preparationCopiedBytes visitedBytes allocationLimit))))))))) def dataBytesZeroTelemetry = (lambda unrestricted allocationLimit : Nat . (dataBytesTelemetry zero zero zero zero zero zero zero allocationLimit)) -- Check before addition. Runtime Nat is machine-sized, so a post-add check could -- observe a wrapped value and is not acceptable. def dataBytesCheckedAddWithin = (lambda unrestricted limit : Nat . (lambda unrestricted failure : (family DataBytesErrorCode) . (lambda unrestricted left : Nat . (lambda unrestricted right : Nat . (nat-eliminate (lambda unrestricted current : Nat . (family DataBytesCheckedNaturalResult)) (constructor DataBytesCheckedNaturalResult DataBytesCheckedNaturalFailed failure) (lambda unrestricted leftFitsPredecessor : Nat . (lambda unrestricted leftFitsInduction : (family DataBytesCheckedNaturalResult) . (nat-eliminate (lambda unrestricted current : Nat . (family DataBytesCheckedNaturalResult)) (constructor DataBytesCheckedNaturalResult DataBytesCheckedNaturalFailed failure) (lambda unrestricted rightFitsPredecessor : Nat . (lambda unrestricted rightFitsInduction : (family DataBytesCheckedNaturalResult) . (constructor DataBytesCheckedNaturalResult DataBytesCheckedNaturalSucceeded (naturalAdd left right)))) (naturalLessOrEqual right (naturalSaturatingSubtract limit left))))) (naturalLessOrEqual left limit)))))) def dataBytesCheckedLengthAdd = (dataBytesCheckedAddWithin dataBytesDefaultAllocationLimit (constructor DataBytesErrorCode DataBytesLengthOverflow)) def dataBytesCheckedOffsetAdd = (dataBytesCheckedAddWithin dataBytesDefaultAllocationLimit (constructor DataBytesErrorCode DataBytesOffsetOverflow)) -- These helpers are called only after a public bounds proof. def dataBytesDropValidated = (lambda unrestricted count : Nat . (nat-eliminate (lambda unrestricted current : Nat . (pi unrestricted input : Bytes . Bytes)) (lambda unrestricted input : Bytes . input) (lambda unrestricted predecessor : Nat . (lambda unrestricted induction : (pi unrestricted input : Bytes . Bytes) . (lambda unrestricted input : Bytes . (induction (bytes-tail input))))) count)) -- Build the prefix once. Repeated bytes-cons copies every growing suffix in -- the native evaluator, making a large imported normalization table quadratic. -- A builder retains each byte as a chunk and materializes the prefix linearly. -- Keep the total helper's old zero-padding behavior past the end; public -- bounded slices reject those requests before calling this helper. def dataBytesTakeBuilder = (lambda unrestricted count : Nat . (nat-eliminate (lambda unrestricted current : Nat . (pi unrestricted input : Bytes . BytesBuilder)) (lambda unrestricted input : Bytes . (bytes-builder-empty)) (lambda unrestricted predecessor : Nat . (lambda unrestricted induction : (pi unrestricted input : Bytes . BytesBuilder) . (lambda unrestricted input : Bytes . (bytes-builder-append (bytes-builder-chunk (bytes-cons (bytes-head input) b"")) (induction (bytes-tail input)))))) count)) def dataBytesTakeValidated = (lambda unrestricted count : Nat . (lambda unrestricted input : Bytes . (bytes-builder-build (dataBytesTakeBuilder count input)))) def dataBytesByteAtValidated = (lambda unrestricted input : Bytes . (lambda unrestricted index : Nat . (bytes-head (dataBytesDropValidated index input)))) -- Bytes is the runtime's project-owned immutable byte value. def dataBytesEmpty = b"" def dataBytesFromBytes = (lambda unrestricted value : Bytes . value) def dataBytesToBytes = (lambda unrestricted value : Bytes . value) -- Repeat a complete chunk, materializing once. This does not repeatedly -- copy a growing suffix as bytes-cons/bytes-append in a linear fold would. def dataBytesRepeat = (lambda unrestricted chunk : Bytes . (lambda unrestricted count : Nat . (bytes-builder-build (nat-eliminate (lambda unrestricted n : Nat . BytesBuilder) (bytes-builder-empty) (lambda unrestricted index : Nat . (lambda unrestricted previous : BytesBuilder . (bytes-builder-append previous (bytes-builder-chunk chunk)))) count)))) -- Batch single-byte repetitions into 4096-byte chunks. This is a construction -- granularity, not a maximum extent: quotient and remainder cover all bytes. def dataBytesRepeatByte = (lambda unrestricted value : Byte . (lambda unrestricted count : Nat . (let unrestricted single = (bytes-cons value b"") in (nat-eliminate (lambda unrestricted small : Nat . Bytes) (let unrestricted block = (dataBytesRepeat single 4096) in (bytes-append (dataBytesRepeat block (naturalDivideUnchecked count 4096)) (dataBytesRepeat single (naturalModuloUnchecked count 4096)))) (lambda unrestricted predecessor : Nat . (lambda unrestricted unused : Bytes . (dataBytesRepeat single count))) (nat-less-than count 4096))))) def dataBytesLength = (lambda unrestricted value : Bytes . (bytes-length value)) def dataBytesEqual = (lambda unrestricted left : Bytes . (lambda unrestricted right : Bytes . (bytes-equal left right))) def dataBytesCompare = (lambda unrestricted left : Bytes . (bytes-eliminate (lambda unrestricted current : Bytes . (pi unrestricted right : Bytes . (family DataBytesOrdering))) (lambda unrestricted right : Bytes . (bytes-eliminate (lambda unrestricted current : Bytes . (family DataBytesOrdering)) (constructor DataBytesOrdering DataBytesEqual) (lambda unrestricted rightHead : Byte . (lambda unrestricted rightTail : Bytes . (lambda unrestricted rightInduction : (family DataBytesOrdering) . (constructor DataBytesOrdering DataBytesLess)))) right)) (lambda unrestricted leftHead : Byte . (lambda unrestricted leftTail : Bytes . (lambda unrestricted leftInduction : (pi unrestricted right : Bytes . (family DataBytesOrdering)) . (lambda unrestricted right : Bytes . (bytes-eliminate (lambda unrestricted current : Bytes . (family DataBytesOrdering)) (constructor DataBytesOrdering DataBytesGreater) (lambda unrestricted rightHead : Byte . (lambda unrestricted rightTail : Bytes . (lambda unrestricted rightInduction : (family DataBytesOrdering) . (nat-eliminate (lambda unrestricted current : Nat . (family DataBytesOrdering)) (nat-eliminate (lambda unrestricted current : Nat . (family DataBytesOrdering)) (constructor DataBytesOrdering DataBytesGreater) (lambda unrestricted lessPredecessor : Nat . (lambda unrestricted lessInduction : (family DataBytesOrdering) . (constructor DataBytesOrdering DataBytesLess))) (byte-less-than leftHead rightHead)) (lambda unrestricted equalPredecessor : Nat . (lambda unrestricted equalInduction : (family DataBytesOrdering) . (leftInduction rightTail))) (byte-equal leftHead rightHead))))) right))))) left)) def dataBytesIndex = (lambda unrestricted input : Bytes . (lambda unrestricted index : Nat . (app (lambda unrestricted inputLength : Nat . (nat-eliminate (lambda unrestricted current : Nat . (family DataBytesIndexResult)) (constructor DataBytesIndexResult DataBytesIndexFailed (constructor DataBytesErrorCode DataBytesIndexOutOfRange) (dataBytesTelemetry inputLength dataBytesNaturalOne zero zero zero zero index inputLength)) (lambda unrestricted fitsPredecessor : Nat . (lambda unrestricted fitsInduction : (family DataBytesIndexResult) . (constructor DataBytesIndexResult DataBytesIndexSucceeded (dataBytesByteAtValidated input index) (dataBytesTelemetry inputLength dataBytesNaturalOne dataBytesNaturalOne zero dataBytesNaturalOne zero index inputLength)))) (naturalLess index inputLength))) (bytes-length input)))) def dataBytesSlice = (lambda unrestricted input : Bytes . (lambda unrestricted offset : Nat . (lambda unrestricted requestedLength : Nat . (app (lambda unrestricted inputLength : Nat . (nat-eliminate (lambda unrestricted current : Nat . (family DataBytesSliceResult)) (constructor DataBytesSliceResult DataBytesSliceFailed (constructor DataBytesErrorCode DataBytesOffsetOutOfRange) (dataBytesTelemetry inputLength requestedLength zero zero zero zero zero inputLength)) (lambda unrestricted offsetFitsPredecessor : Nat . (lambda unrestricted offsetFitsInduction : (family DataBytesSliceResult) . (nat-eliminate (lambda unrestricted current : Nat . (family DataBytesSliceResult)) (constructor DataBytesSliceResult DataBytesSliceFailed (constructor DataBytesErrorCode DataBytesSliceOutOfRange) (dataBytesTelemetry inputLength requestedLength zero zero zero zero offset inputLength)) (lambda unrestricted lengthFitsPredecessor : Nat . (lambda unrestricted lengthFitsInduction : (family DataBytesSliceResult) . (constructor DataBytesSliceResult DataBytesSliceSucceeded (constructor DataBytesSlice DataBytesSliceView (dataBytesDropValidated offset input) requestedLength) (dataBytesTelemetry inputLength requestedLength zero zero requestedLength zero offset inputLength)))) (naturalLessOrEqual requestedLength (naturalSaturatingSubtract inputLength offset))))) (naturalLessOrEqual offset inputLength))) (bytes-length input))))) def dataBytesSliceToBytesWithin = (lambda unrestricted allocationLimit : Nat . (lambda unrestricted slice : (family DataBytesSlice) . (eliminate DataBytesSlice (lambda unrestricted current : (family DataBytesSlice) . (family DataBytesResult)) slice (branch DataBytesSliceView suffix requestedLength . (app (lambda unrestricted suffixLength : Nat . (nat-eliminate (lambda unrestricted current : Nat . (family DataBytesResult)) (constructor DataBytesResult DataBytesFailed (constructor DataBytesErrorCode DataBytesBuilderInvariantViolation) (dataBytesTelemetry suffixLength requestedLength zero zero zero zero zero allocationLimit)) (lambda unrestricted validPredecessor : Nat . (lambda unrestricted validInduction : (family DataBytesResult) . (nat-eliminate (lambda unrestricted current : Nat . (family DataBytesResult)) (constructor DataBytesResult DataBytesFailed (constructor DataBytesErrorCode DataBytesAllocationLimitExceeded) (dataBytesTelemetry suffixLength requestedLength zero zero requestedLength zero zero allocationLimit)) (lambda unrestricted limitPredecessor : Nat . (lambda unrestricted limitInduction : (family DataBytesResult) . (nat-eliminate (lambda unrestricted current : Nat . (family DataBytesResult)) (constructor DataBytesResult DataBytesSucceeded (dataBytesTakeValidated requestedLength suffix) (dataBytesTelemetry suffixLength requestedLength requestedLength dataBytesNaturalOne zero requestedLength requestedLength allocationLimit)) (lambda unrestricted wholePredecessor : Nat . (lambda unrestricted wholeInduction : (family DataBytesResult) . (constructor DataBytesResult DataBytesSucceeded suffix (dataBytesTelemetry suffixLength requestedLength requestedLength dataBytesNaturalOne requestedLength zero zero allocationLimit)))) (naturalEqual requestedLength suffixLength)))) (naturalLessOrEqual requestedLength allocationLimit)))) (naturalLessOrEqual requestedLength suffixLength))) (bytes-length suffix)))))) def dataBytesSliceToBytes = (dataBytesSliceToBytesWithin dataBytesDefaultAllocationLimit) def dataBytesSliceIndex = (lambda unrestricted slice : (family DataBytesSlice) . (lambda unrestricted index : Nat . (eliminate DataBytesSlice (lambda unrestricted current : (family DataBytesSlice) . (family DataBytesIndexResult)) slice (branch DataBytesSliceView suffix sliceLength . (app (lambda unrestricted suffixLength : Nat . (nat-eliminate (lambda unrestricted current : Nat . (family DataBytesIndexResult)) (constructor DataBytesIndexResult DataBytesIndexFailed (constructor DataBytesErrorCode DataBytesBuilderInvariantViolation) (dataBytesTelemetry suffixLength dataBytesNaturalOne zero zero zero zero zero suffixLength)) (lambda unrestricted validPredecessor : Nat . (lambda unrestricted validInduction : (family DataBytesIndexResult) . (nat-eliminate (lambda unrestricted current : Nat . (family DataBytesIndexResult)) (constructor DataBytesIndexResult DataBytesIndexFailed (constructor DataBytesErrorCode DataBytesIndexOutOfRange) (dataBytesTelemetry sliceLength dataBytesNaturalOne zero zero zero zero index sliceLength)) (lambda unrestricted fitsPredecessor : Nat . (lambda unrestricted fitsInduction : (family DataBytesIndexResult) . (constructor DataBytesIndexResult DataBytesIndexSucceeded (dataBytesByteAtValidated suffix index) (dataBytesTelemetry sliceLength dataBytesNaturalOne dataBytesNaturalOne zero dataBytesNaturalOne zero index sliceLength)))) (naturalLess index sliceLength)))) (naturalLessOrEqual sliceLength suffixLength))) (bytes-length suffix)))))) def dataBytesBuilderEmpty = (constructor DataBytesBuilder DataBytesBuilderValue (bytes-builder-empty) zero zero zero zero) -- Valid builders have no empty chunks and partition their length into shared -- source bytes and bytes copied while preparing bounded slices. def dataBytesBuilderMetadataValid = (lambda unrestricted length : Nat . (lambda unrestricted chunks : Nat . (lambda unrestricted sharedBytes : Nat . (lambda unrestricted preparationCopiedBytes : Nat . (nat-eliminate (lambda unrestricted current : Nat . Nat) zero (lambda unrestricted basicPredecessor : Nat . (lambda unrestricted basicInduction : Nat . (nat-eliminate (lambda unrestricted current : Nat . Nat) zero (lambda unrestricted sumPredecessor : Nat . (lambda unrestricted sumInduction : Nat . (naturalEqual (naturalAdd sharedBytes preparationCopiedBytes) length))) (naturalLessOrEqual preparationCopiedBytes (naturalSaturatingSubtract length sharedBytes))))) (naturalAnd (naturalLessOrEqual chunks length) (naturalLessOrEqual sharedBytes length))))))) def dataBytesBuilderChunkWithin = (lambda unrestricted allocationLimit : Nat . (lambda unrestricted chunk : Bytes . (app (lambda unrestricted chunkLength : Nat . (nat-eliminate (lambda unrestricted current : Nat . (family DataBytesBuilderResult)) (constructor DataBytesBuilderResult DataBytesBuilderFailed (constructor DataBytesErrorCode DataBytesAllocationLimitExceeded) (dataBytesTelemetry chunkLength chunkLength zero zero zero zero zero allocationLimit)) (lambda unrestricted fitsPredecessor : Nat . (lambda unrestricted fitsInduction : (family DataBytesBuilderResult) . (nat-eliminate (lambda unrestricted current : Nat . (family DataBytesBuilderResult)) (constructor DataBytesBuilderResult DataBytesBuilderSucceeded dataBytesBuilderEmpty (dataBytesZeroTelemetry allocationLimit)) (lambda unrestricted nonemptyPredecessor : Nat . (lambda unrestricted nonemptyInduction : (family DataBytesBuilderResult) . (constructor DataBytesBuilderResult DataBytesBuilderSucceeded (constructor DataBytesBuilder DataBytesBuilderValue (bytes-builder-chunk chunk) chunkLength dataBytesNaturalOne chunkLength zero) (dataBytesTelemetry chunkLength chunkLength zero dataBytesNaturalOne chunkLength zero zero allocationLimit)))) chunkLength))) (naturalLessOrEqual chunkLength allocationLimit))) (bytes-length chunk)))) def dataBytesBuilderChunk = (dataBytesBuilderChunkWithin dataBytesDefaultAllocationLimit) def dataBytesBuilderAppendCheckedValues = (lambda unrestricted allocationLimit : Nat . (lambda unrestricted leftRuntime : BytesBuilder . (lambda unrestricted leftLength : Nat . (lambda unrestricted leftChunks : Nat . (lambda unrestricted leftShared : Nat . (lambda unrestricted leftCopied : Nat . (lambda unrestricted rightRuntime : BytesBuilder . (lambda unrestricted rightLength : Nat . (lambda unrestricted rightChunks : Nat . (lambda unrestricted rightShared : Nat . (lambda unrestricted rightCopied : Nat . (eliminate DataBytesCheckedNaturalResult (lambda unrestricted current : (family DataBytesCheckedNaturalResult) . (family DataBytesBuilderResult)) (dataBytesCheckedAddWithin allocationLimit (constructor DataBytesErrorCode DataBytesAllocationLimitExceeded) leftLength rightLength) (branch DataBytesCheckedNaturalSucceeded totalLength . (constructor DataBytesBuilderResult DataBytesBuilderSucceeded (constructor DataBytesBuilder DataBytesBuilderValue (bytes-builder-append leftRuntime rightRuntime) totalLength (naturalAdd leftChunks rightChunks) (naturalAdd leftShared rightShared) (naturalAdd leftCopied rightCopied)) (dataBytesTelemetry totalLength totalLength zero (naturalAdd leftChunks rightChunks) (naturalAdd leftShared rightShared) (naturalAdd leftCopied rightCopied) zero allocationLimit))) (branch DataBytesCheckedNaturalFailed code . (constructor DataBytesBuilderResult DataBytesBuilderFailed code (dataBytesTelemetry leftLength rightLength zero zero zero zero zero allocationLimit))))))))))))))) def dataBytesBuilderAppendWithin = (lambda unrestricted allocationLimit : Nat . (lambda unrestricted left : (family DataBytesBuilder) . (lambda unrestricted right : (family DataBytesBuilder) . (eliminate DataBytesBuilder (lambda unrestricted current : (family DataBytesBuilder) . (family DataBytesBuilderResult)) left (branch DataBytesBuilderValue leftRuntime leftLength leftChunks leftShared leftCopied . (eliminate DataBytesBuilder (lambda unrestricted current : (family DataBytesBuilder) . (family DataBytesBuilderResult)) right (branch DataBytesBuilderValue rightRuntime rightLength rightChunks rightShared rightCopied . (nat-eliminate (lambda unrestricted current : Nat . (family DataBytesBuilderResult)) (constructor DataBytesBuilderResult DataBytesBuilderFailed (constructor DataBytesErrorCode DataBytesBuilderInvariantViolation) (dataBytesZeroTelemetry allocationLimit)) (lambda unrestricted validPredecessor : Nat . (lambda unrestricted validInduction : (family DataBytesBuilderResult) . (dataBytesBuilderAppendCheckedValues allocationLimit leftRuntime leftLength leftChunks leftShared leftCopied rightRuntime rightLength rightChunks rightShared rightCopied))) (naturalAnd (dataBytesBuilderMetadataValid leftLength leftChunks leftShared leftCopied) (dataBytesBuilderMetadataValid rightLength rightChunks rightShared rightCopied)))))))))) def dataBytesBuilderAppend = (dataBytesBuilderAppendWithin dataBytesDefaultAllocationLimit) def dataBytesBuilderBuildWithin = (lambda unrestricted allocationLimit : Nat . (lambda unrestricted builder : (family DataBytesBuilder) . (eliminate DataBytesBuilder (lambda unrestricted current : (family DataBytesBuilder) . (family DataBytesResult)) builder (branch DataBytesBuilderValue runtime length chunks shared copied . (nat-eliminate (lambda unrestricted current : Nat . (family DataBytesResult)) (constructor DataBytesResult DataBytesFailed (constructor DataBytesErrorCode DataBytesBuilderInvariantViolation) (dataBytesZeroTelemetry allocationLimit)) (lambda unrestricted validPredecessor : Nat . (lambda unrestricted validInduction : (family DataBytesResult) . (nat-eliminate (lambda unrestricted current : Nat . (family DataBytesResult)) (constructor DataBytesResult DataBytesFailed (constructor DataBytesErrorCode DataBytesAllocationLimitExceeded) (dataBytesTelemetry length length zero chunks shared copied zero allocationLimit)) (lambda unrestricted fitsPredecessor : Nat . (lambda unrestricted fitsInduction : (family DataBytesResult) . (app (lambda unrestricted output : Bytes . (nat-eliminate (lambda unrestricted current : Nat . (family DataBytesResult)) (constructor DataBytesResult DataBytesFailed (constructor DataBytesErrorCode DataBytesBuilderInvariantViolation) (dataBytesTelemetry length length zero chunks shared copied length allocationLimit)) (lambda unrestricted exactPredecessor : Nat . (lambda unrestricted exactInduction : (family DataBytesResult) . (constructor DataBytesResult DataBytesSucceeded output (dataBytesTelemetry length length length chunks shared copied length allocationLimit)))) (naturalEqual (bytes-length output) length))) (bytes-builder-build runtime)))) (naturalLessOrEqual length allocationLimit)))) (dataBytesBuilderMetadataValid length chunks shared copied)))))) def dataBytesBuilderBuild = (dataBytesBuilderBuildWithin dataBytesDefaultAllocationLimit) def dataBytesConcatWithin = dataBytesBuilderBuildWithin def dataBytesConcat = dataBytesBuilderBuild def dataBytesAppendWithin = (lambda unrestricted allocationLimit : Nat . (lambda unrestricted left : Bytes . (lambda unrestricted right : Bytes . (app (lambda unrestricted leftLength : Nat . (app (lambda unrestricted rightLength : Nat . (eliminate DataBytesCheckedNaturalResult (lambda unrestricted current : (family DataBytesCheckedNaturalResult) . (family DataBytesResult)) (dataBytesCheckedAddWithin allocationLimit (constructor DataBytesErrorCode DataBytesAllocationLimitExceeded) leftLength rightLength) (branch DataBytesCheckedNaturalSucceeded totalLength . (app (lambda unrestricted output : Bytes . (constructor DataBytesResult DataBytesSucceeded output (dataBytesTelemetry totalLength totalLength totalLength dataBytesNaturalTwo totalLength zero totalLength allocationLimit))) (bytes-builder-build (bytes-builder-append (bytes-builder-chunk left) (bytes-builder-chunk right))))) (branch DataBytesCheckedNaturalFailed code . (constructor DataBytesResult DataBytesFailed code (dataBytesTelemetry leftLength rightLength zero zero zero zero zero allocationLimit))))) (bytes-length right))) (bytes-length left))))) def dataBytesAppendChecked = (dataBytesAppendWithin dataBytesDefaultAllocationLimit) -- Bootstrap-compatible append now uses a two-chunk build rather than list-like -- nested bytesAppend. Bulk callers use DataBytesBuilder and build exactly once. def dataBytesAppend = (lambda unrestricted left : Bytes . (lambda unrestricted right : Bytes . (bytes-builder-build (bytes-builder-append (bytes-builder-chunk left) (bytes-builder-chunk right))))) def dataBytesWord32LE = (lambda unrestricted value : (family ModelWord32) . (eliminate ModelWord32 (lambda unrestricted current : (family ModelWord32) . Bytes) value (branch ModelWord32Value b0 b1 b2 b3 . (bytes-cons b0 (bytes-cons b1 (bytes-cons b2 (bytes-cons b3 b""))))))) def dataBytesWord32BE = (lambda unrestricted value : (family ModelWord32) . (eliminate ModelWord32 (lambda unrestricted current : (family ModelWord32) . Bytes) value (branch ModelWord32Value b0 b1 b2 b3 . (bytes-cons b3 (bytes-cons b2 (bytes-cons b1 (bytes-cons b0 b""))))))) def dataBytesWord64LE = (lambda unrestricted value : (family ModelWord64) . (eliminate ModelWord64 (lambda unrestricted current : (family ModelWord64) . Bytes) value (branch ModelWord64Value b0 b1 b2 b3 b4 b5 b6 b7 . (bytes-cons b0 (bytes-cons b1 (bytes-cons b2 (bytes-cons b3 (bytes-cons b4 (bytes-cons b5 (bytes-cons b6 (bytes-cons b7 b""))))))))))) def dataBytesWord64BE = (lambda unrestricted value : (family ModelWord64) . (eliminate ModelWord64 (lambda unrestricted current : (family ModelWord64) . Bytes) value (branch ModelWord64Value b0 b1 b2 b3 b4 b5 b6 b7 . (bytes-cons b7 (bytes-cons b6 (bytes-cons b5 (bytes-cons b4 (bytes-cons b3 (bytes-cons b2 (bytes-cons b1 (bytes-cons b0 b""))))))))))) def dataBytesWord32Failure = (constructor DataBytesWord32DecodeResult DataBytesWord32DecodeFailed (constructor DataBytesErrorCode DataBytesWord32InputTooShort)) def dataBytesWord64Failure = (constructor DataBytesWord64DecodeResult DataBytesWord64DecodeFailed (constructor DataBytesErrorCode DataBytesWord64InputTooShort)) def dataBytesReadWord32LE = (lambda unrestricted input : Bytes . (nat-eliminate (lambda unrestricted current : Nat . (family DataBytesWord32DecodeResult)) dataBytesWord32Failure (lambda unrestricted fitsPredecessor : Nat . (lambda unrestricted fitsInduction : (family DataBytesWord32DecodeResult) . (constructor DataBytesWord32DecodeResult DataBytesWord32Decoded (constructor ModelWord32 ModelWord32Value (dataBytesByteAtValidated input zero) (dataBytesByteAtValidated input dataBytesNaturalOne) (dataBytesByteAtValidated input dataBytesNaturalTwo) (dataBytesByteAtValidated input dataBytesNaturalThree)) (dataBytesDropValidated dataBytesNaturalFour input)))) (naturalLessOrEqual dataBytesNaturalFour (bytes-length input)))) def dataBytesReadWord32BE = (lambda unrestricted input : Bytes . (nat-eliminate (lambda unrestricted current : Nat . (family DataBytesWord32DecodeResult)) dataBytesWord32Failure (lambda unrestricted fitsPredecessor : Nat . (lambda unrestricted fitsInduction : (family DataBytesWord32DecodeResult) . (constructor DataBytesWord32DecodeResult DataBytesWord32Decoded (constructor ModelWord32 ModelWord32Value (dataBytesByteAtValidated input dataBytesNaturalThree) (dataBytesByteAtValidated input dataBytesNaturalTwo) (dataBytesByteAtValidated input dataBytesNaturalOne) (dataBytesByteAtValidated input zero)) (dataBytesDropValidated dataBytesNaturalFour input)))) (naturalLessOrEqual dataBytesNaturalFour (bytes-length input)))) def dataBytesReadWord64LE = (lambda unrestricted input : Bytes . (nat-eliminate (lambda unrestricted current : Nat . (family DataBytesWord64DecodeResult)) dataBytesWord64Failure (lambda unrestricted fitsPredecessor : Nat . (lambda unrestricted fitsInduction : (family DataBytesWord64DecodeResult) . (constructor DataBytesWord64DecodeResult DataBytesWord64Decoded (constructor ModelWord64 ModelWord64Value (dataBytesByteAtValidated input zero) (dataBytesByteAtValidated input dataBytesNaturalOne) (dataBytesByteAtValidated input dataBytesNaturalTwo) (dataBytesByteAtValidated input dataBytesNaturalThree) (dataBytesByteAtValidated input dataBytesNaturalFour) (dataBytesByteAtValidated input dataBytesNaturalFive) (dataBytesByteAtValidated input dataBytesNaturalSix) (dataBytesByteAtValidated input dataBytesNaturalSeven)) (dataBytesDropValidated dataBytesNaturalEight input)))) (naturalLessOrEqual dataBytesNaturalEight (bytes-length input)))) def dataBytesReadWord64BE = (lambda unrestricted input : Bytes . (nat-eliminate (lambda unrestricted current : Nat . (family DataBytesWord64DecodeResult)) dataBytesWord64Failure (lambda unrestricted fitsPredecessor : Nat . (lambda unrestricted fitsInduction : (family DataBytesWord64DecodeResult) . (constructor DataBytesWord64DecodeResult DataBytesWord64Decoded (constructor ModelWord64 ModelWord64Value (dataBytesByteAtValidated input dataBytesNaturalSeven) (dataBytesByteAtValidated input dataBytesNaturalSix) (dataBytesByteAtValidated input dataBytesNaturalFive) (dataBytesByteAtValidated input dataBytesNaturalFour) (dataBytesByteAtValidated input dataBytesNaturalThree) (dataBytesByteAtValidated input dataBytesNaturalTwo) (dataBytesByteAtValidated input dataBytesNaturalOne) (dataBytesByteAtValidated input zero)) (dataBytesDropValidated dataBytesNaturalEight input)))) (naturalLessOrEqual dataBytesNaturalEight (bytes-length input)))) def dataBytesWord32ExactFailure = (lambda unrestricted inputLength : Nat . (constructor DataBytesWord32ExactDecodeResult DataBytesWord32ExactDecodeFailed (constructor DataBytesErrorCode DataBytesWord32MalformedLength) (dataBytesTelemetry inputLength dataBytesNaturalFour zero zero zero zero inputLength dataBytesNaturalFour))) def dataBytesWord64ExactFailure = (lambda unrestricted inputLength : Nat . (constructor DataBytesWord64ExactDecodeResult DataBytesWord64ExactDecodeFailed (constructor DataBytesErrorCode DataBytesWord64MalformedLength) (dataBytesTelemetry inputLength dataBytesNaturalEight zero zero zero zero inputLength dataBytesNaturalEight))) def dataBytesWord32ExactFromStream = (lambda unrestricted inputLength : Nat . (lambda unrestricted decoded : (family DataBytesWord32DecodeResult) . (eliminate DataBytesWord32DecodeResult (lambda unrestricted current : (family DataBytesWord32DecodeResult) . (family DataBytesWord32ExactDecodeResult)) decoded (branch DataBytesWord32Decoded value remaining . (constructor DataBytesWord32ExactDecodeResult DataBytesWord32ExactlyDecoded value (dataBytesTelemetry inputLength dataBytesNaturalFour dataBytesNaturalFour dataBytesNaturalOne inputLength zero dataBytesNaturalFour dataBytesNaturalFour))) (branch DataBytesWord32DecodeFailed code . (dataBytesWord32ExactFailure inputLength))))) def dataBytesWord64ExactFromStream = (lambda unrestricted inputLength : Nat . (lambda unrestricted decoded : (family DataBytesWord64DecodeResult) . (eliminate DataBytesWord64DecodeResult (lambda unrestricted current : (family DataBytesWord64DecodeResult) . (family DataBytesWord64ExactDecodeResult)) decoded (branch DataBytesWord64Decoded value remaining . (constructor DataBytesWord64ExactDecodeResult DataBytesWord64ExactlyDecoded value (dataBytesTelemetry inputLength dataBytesNaturalEight dataBytesNaturalEight dataBytesNaturalOne inputLength zero dataBytesNaturalEight dataBytesNaturalEight))) (branch DataBytesWord64DecodeFailed code . (dataBytesWord64ExactFailure inputLength))))) def dataBytesDecodeWord32LEExact = (lambda unrestricted input : Bytes . (app (lambda unrestricted inputLength : Nat . (nat-eliminate (lambda unrestricted current : Nat . (family DataBytesWord32ExactDecodeResult)) (dataBytesWord32ExactFailure inputLength) (lambda unrestricted exactPredecessor : Nat . (lambda unrestricted exactInduction : (family DataBytesWord32ExactDecodeResult) . (dataBytesWord32ExactFromStream inputLength (dataBytesReadWord32LE input)))) (naturalEqual inputLength dataBytesNaturalFour))) (bytes-length input))) def dataBytesDecodeWord32BEExact = (lambda unrestricted input : Bytes . (app (lambda unrestricted inputLength : Nat . (nat-eliminate (lambda unrestricted current : Nat . (family DataBytesWord32ExactDecodeResult)) (dataBytesWord32ExactFailure inputLength) (lambda unrestricted exactPredecessor : Nat . (lambda unrestricted exactInduction : (family DataBytesWord32ExactDecodeResult) . (dataBytesWord32ExactFromStream inputLength (dataBytesReadWord32BE input)))) (naturalEqual inputLength dataBytesNaturalFour))) (bytes-length input))) def dataBytesDecodeWord64LEExact = (lambda unrestricted input : Bytes . (app (lambda unrestricted inputLength : Nat . (nat-eliminate (lambda unrestricted current : Nat . (family DataBytesWord64ExactDecodeResult)) (dataBytesWord64ExactFailure inputLength) (lambda unrestricted exactPredecessor : Nat . (lambda unrestricted exactInduction : (family DataBytesWord64ExactDecodeResult) . (dataBytesWord64ExactFromStream inputLength (dataBytesReadWord64LE input)))) (naturalEqual inputLength dataBytesNaturalEight))) (bytes-length input))) def dataBytesDecodeWord64BEExact = (lambda unrestricted input : Bytes . (app (lambda unrestricted inputLength : Nat . (nat-eliminate (lambda unrestricted current : Nat . (family DataBytesWord64ExactDecodeResult)) (dataBytesWord64ExactFailure inputLength) (lambda unrestricted exactPredecessor : Nat . (lambda unrestricted exactInduction : (family DataBytesWord64ExactDecodeResult) . (dataBytesWord64ExactFromStream inputLength (dataBytesReadWord64BE input)))) (naturalEqual inputLength dataBytesNaturalEight))) (bytes-length input))) def dataBytesHexDigit = (lambda unrestricted nibble : Nat . (nat-eliminate (lambda unrestricted current : Nat . Byte) (nat-to-byte (naturalAdd (byte-to-nat (byte 87)) nibble)) (lambda unrestricted predecessor : Nat . (lambda unrestricted induction : Byte . (nat-to-byte (naturalAdd (byte-to-nat (byte 48)) nibble)))) (naturalLess nibble dataBytesNaturalTen))) def dataBytesRenderHexBuilder = (lambda unrestricted input : Bytes . (bytes-eliminate (lambda unrestricted current : Bytes . BytesBuilder) (bytes-builder-empty) (lambda unrestricted head : Byte . (lambda unrestricted tail : Bytes . (lambda unrestricted induction : BytesBuilder . (bytes-builder-append (bytes-builder-chunk (bytes-cons (dataBytesHexDigit (naturalDivideUnchecked (byte-to-nat head) dataBytesNaturalSixteen)) (bytes-cons (dataBytesHexDigit (naturalModuloUnchecked (byte-to-nat head) dataBytesNaturalSixteen)) b""))) induction)))) input)) def dataBytesRenderHexWithin = (lambda unrestricted allocationLimit : Nat . (lambda unrestricted input : Bytes . (app (lambda unrestricted inputLength : Nat . (eliminate DataBytesCheckedNaturalResult (lambda unrestricted current : (family DataBytesCheckedNaturalResult) . (family DataBytesResult)) (dataBytesCheckedAddWithin allocationLimit (constructor DataBytesErrorCode DataBytesAllocationLimitExceeded) inputLength inputLength) (branch DataBytesCheckedNaturalSucceeded outputLength . (app (lambda unrestricted output : Bytes . (constructor DataBytesResult DataBytesSucceeded output (dataBytesTelemetry inputLength outputLength outputLength inputLength zero outputLength inputLength allocationLimit))) (bytes-builder-build (dataBytesRenderHexBuilder input)))) (branch DataBytesCheckedNaturalFailed code . (constructor DataBytesResult DataBytesFailed code (dataBytesTelemetry inputLength inputLength zero zero zero zero zero allocationLimit))))) (bytes-length input)))) def dataBytesRenderHexChecked = (dataBytesRenderHexWithin dataBytesDefaultAllocationLimit) -- Existing digest consumers require a raw Bytes result. New untrusted inputs use -- dataBytesRenderHexChecked and handle DataBytesFailed. def dataBytesRenderHex = (lambda unrestricted input : Bytes . (bytes-builder-build (dataBytesRenderHexBuilder input))) -- Eta-expanded primitive wrappers: primitives are not first-class -- values; pass these instead when a function value is needed. def bytesAppend = (lambda unrestricted left : Bytes . (lambda unrestricted right : Bytes . (bytes-append left right))) def bytesBuilderFromBytes = (lambda unrestricted value : Bytes . (bytes-builder-chunk value)) def bytesDropLeadingZeroes = (lambda unrestricted value : Bytes . (bytes-eliminate (lambda unrestricted current : Bytes . Bytes) b"" (lambda unrestricted head : Byte . (lambda unrestricted tail : Bytes . (lambda unrestricted induction : Bytes . (nat-eliminate (lambda unrestricted headValue : Nat . Bytes) induction (lambda unrestricted predecessor : Nat . (lambda unrestricted keepInduction : Bytes . (bytes-cons head tail))) (byte-to-nat head))))) value))