Large source region · 2,617 lines
module Data.JSON
import Data.UTF8
import Model.Word32
import Std.Byte
import Std.Natural
import Std.Flag
family JSON : Type 0
constructor JSONObject
recursive unrestricted jsonObjectMembers
constructor JSONObjectEnd
constructor JSONObjectMember
field unrestricted jsonObjectMemberKey : Bytes
recursive unrestricted jsonObjectMemberValue
recursive unrestricted jsonObjectMemberTail
constructor JSONArray
recursive unrestricted jsonArrayValues
constructor JSONArrayEnd
constructor JSONArrayNext
recursive unrestricted jsonArrayHead
recursive unrestricted jsonArrayTail
constructor JSONString
field unrestricted jsonStringBytes : Bytes
constructor JSONNumber
field unrestricted jsonNumberBytes : Bytes
constructor JSONBoolean
field unrestricted jsonBooleanValue : Nat
constructor JSONNull
end-family
family JSONErrorCode : Type 0
constructor JSONInvalidUTF8
constructor JSONUnexpectedEnd
constructor JSONTrailingBytes
constructor JSONInvalidValue
constructor JSONObjectKeyNotString
constructor JSONObjectColonMissing
constructor JSONObjectDelimiterMissing
constructor JSONObjectDuplicateKey
constructor JSONArrayDelimiterMissing
constructor JSONStringUnterminated
constructor JSONStringControlCharacter
constructor JSONEscapeInvalid
constructor JSONUnicodeEscapeInvalid
constructor JSONUnicodeLowWithoutHigh
constructor JSONUnicodeHighWithoutLow
constructor JSONNumberIntegerInvalid
constructor JSONNumberFractionDigitsMissing
constructor JSONNumberExponentDigitsMissing
constructor JSONExpectedObject
constructor JSONMissingMember
constructor JSONDuplicateMember
constructor JSONExpectedString
constructor JSONExpectedArray
constructor JSONExpectedNumber
constructor JSONExpectedInteger
constructor JSONExpectedBoolean
constructor JSONExpectedNull
constructor JSONInputLimitExceeded
constructor JSONDepthLimitExceeded
constructor JSONStringLimitExceeded
constructor JSONNumberLimitExceeded
constructor JSONContainerLimitExceeded
constructor JSONOutputLimitExceeded
constructor JSONNumericRangeUnsupported
constructor JSONMalformedTree
end-family
-- A limit the parser or renderer checks a size against. `JSONBoundAtMost n`
-- allows values up to and including n; `JSONBoundBelowTwoPower bits` allows
-- values below 2^bits WITHOUT ever building 2^bits -- a runtime natural costs
-- about 164 bytes per unit of magnitude (measured 2026-09-16: 2^24 is 2.75 GB,
-- 2^63 cannot exist), so the old Nat limits of 2^24 and 2^20 were an
-- out-of-memory the first time a real document met them (the 593 KB tokenizer
-- JSON). A bound is compared with jsonBoundAllows.
family JSONBound : Type 0
constructor JSONBoundAtMost
field unrestricted jsonBoundValue : Nat
constructor JSONBoundBelowTwoPower
field unrestricted jsonBoundBits : Nat
end-family
family JSONLimits : Type 0
constructor JSONLimitsValue
field unrestricted jsonMaximumInputBytes : (family JSONBound)
field unrestricted jsonMaximumDepth : (family JSONBound)
field unrestricted jsonMaximumStringBytes : (family JSONBound)
field unrestricted jsonMaximumNumberBytes : (family JSONBound)
field unrestricted jsonMaximumContainerEntries : (family JSONBound)
field unrestricted jsonMaximumOutputBytes : (family JSONBound)
end-family
family JSONCounts : Type 0
constructor JSONCountsValue
field unrestricted jsonCountValues : Nat
field unrestricted jsonCountObjects : Nat
field unrestricted jsonCountObjectMembers : Nat
field unrestricted jsonCountArrays : Nat
field unrestricted jsonCountArrayElements : Nat
field unrestricted jsonCountStrings : Nat
field unrestricted jsonCountNumbers : Nat
field unrestricted jsonCountBooleans : Nat
field unrestricted jsonCountNulls : Nat
field unrestricted jsonCountStringBytes : Nat
field unrestricted jsonCountNumberBytes : Nat
end-family
family JSONTreeKind : Type 0
constructor JSONTreeValueKind
constructor JSONTreeObjectMembersKind
constructor JSONTreeArrayValuesKind
end-family
family JSONTreeAuditResult : Type 0
constructor JSONTreeAuditSucceeded
field unrestricted jsonTreeAuditKind : (family JSONTreeKind)
field unrestricted jsonTreeAuditCounts : (family JSONCounts)
field unrestricted jsonTreeAuditMaximumDepth : Nat
field unrestricted jsonTreeAuditSequenceCount : Nat
constructor JSONTreeAuditFailed
field unrestricted jsonTreeAuditError : (family JSONErrorCode)
end-family
family JSONParseTelemetry : Type 0
constructor JSONParseTelemetryValue
field unrestricted jsonTelemetryInputBytes : Nat
field unrestricted jsonTelemetryConsumedBytes : Nat
field unrestricted jsonTelemetryRemainingBytes : Nat
field unrestricted jsonTelemetryParserFuel : Nat
field unrestricted jsonTelemetryMaximumDepth : Nat
field unrestricted jsonTelemetryCounts : (family JSONCounts)
end-family
family JSONObservedDocumentResult : Type 0
constructor JSONObservedDocumentParsed
field unrestricted jsonObservedDocumentValue : (family JSON)
field unrestricted jsonObservedDocumentTelemetry : (family JSONParseTelemetry)
constructor JSONObservedDocumentFailed
field unrestricted jsonObservedDocumentError : (family JSONErrorCode)
field unrestricted jsonObservedDocumentErrorOffset : Nat
field unrestricted jsonObservedDocumentFailureTelemetry : (family JSONParseTelemetry)
end-family
family JSONParseResult : Type 0
constructor JSONParsed
field unrestricted jsonParsedValue : (family JSON)
field unrestricted jsonParsedRemaining : Bytes
constructor JSONParseFailed
field unrestricted jsonParseError : (family JSONErrorCode)
field unrestricted jsonParseRemainingAtFailure : Bytes
end-family
family JSONDocumentResult : Type 0
constructor JSONDocumentParsed
field unrestricted jsonDocumentValue : (family JSON)
constructor JSONDocumentFailed
field unrestricted jsonDocumentError : (family JSONErrorCode)
field unrestricted jsonDocumentErrorOffset : Nat
end-family
family JSONLiteralResult : Type 0
constructor JSONLiteralConsumed
field unrestricted jsonLiteralRemaining : Bytes
constructor JSONLiteralFailed
field unrestricted jsonLiteralFailureRemaining : Bytes
end-family
family JSONHexQuadResult : Type 0
constructor JSONHexQuadParsed
field unrestricted jsonHexQuadValue : Nat
field unrestricted jsonHexQuadRemaining : Bytes
constructor JSONHexQuadFailed
field unrestricted jsonHexQuadFailureRemaining : Bytes
end-family
family JSONStringParseResult : Type 0
constructor JSONStringParsed
field unrestricted jsonStringParsedBuilder : BytesBuilder
field unrestricted jsonStringParsedRemaining : Bytes
constructor JSONStringParseFailed
field unrestricted jsonStringParseError : (family JSONErrorCode)
field unrestricted jsonStringFailureRemaining : Bytes
end-family
family JSONDigitSplit : Type 0
constructor JSONDigitSplitValue
field unrestricted jsonDigitSplitBuilder : BytesBuilder
field unrestricted jsonDigitSplitRemaining : Bytes
field unrestricted jsonDigitSplitCount : Nat
end-family
family JSONNumberParseResult : Type 0
constructor JSONNumberParsed
field unrestricted jsonNumberParsedBytes : Bytes
field unrestricted jsonNumberParsedRemaining : Bytes
constructor JSONNumberParseFailed
field unrestricted jsonNumberParseError : (family JSONErrorCode)
field unrestricted jsonNumberFailureRemaining : Bytes
end-family
family JSONParser : Type 0
constructor JSONParserValue
field unrestricted jsonParserValueFunction : (pi unrestricted input : Bytes . (family JSONParseResult))
field unrestricted jsonParserObjectFunction : (pi unrestricted input : Bytes . (family JSONParseResult))
field unrestricted jsonParserArrayFunction : (pi unrestricted input : Bytes . (family JSONParseResult))
end-family
-- First-order accumulator for the string-body scan. `Going` carries the decoded
-- prefix builder and the current remaining bytes; `Done`/`Failed` are absorbing
-- so the remaining fuel steps are O(1) no-ops (the runtime-graph evaluator runs
-- every fuel step, so the loop must terminate itself in the accumulator rather
-- than by short-circuiting the fold).
family JSONStringLoop : Type 0
constructor JSONStringLoopGoing
field unrestricted jsonStringLoopBuilder : BytesBuilder
field unrestricted jsonStringLoopRemaining : Bytes
constructor JSONStringLoopDone
field unrestricted jsonStringLoopDoneBuilder : BytesBuilder
field unrestricted jsonStringLoopDoneRemaining : Bytes
constructor JSONStringLoopFailed
field unrestricted jsonStringLoopFailedError : (family JSONErrorCode)
field unrestricted jsonStringLoopFailedRemaining : Bytes
end-family
def jsonNaturalOne =
(succ zero)
def jsonNaturalTwo =
(succ jsonNaturalOne)
def jsonNaturalFour =
(byte-to-nat (byte 4))
def jsonNaturalSixteen =
(byte-to-nat (byte 16))
def jsonNaturalOneThousandTwentyFour =
(naturalPowerOfTwo (byte-to-nat (byte 10)))
def jsonNaturalFiftyFiveThousandTwoHundredNinetySix =
(naturalMultiply (byte-to-nat (byte 216)) byteNaturalTwoHundredFiftySix)
def jsonNaturalFiftySixThousandThreeHundredTwenty =
(naturalMultiply (byte-to-nat (byte 220)) byteNaturalTwoHundredFiftySix)
def jsonNaturalFiftySevenThousandThreeHundredFortyFour =
(naturalMultiply (byte-to-nat (byte 224)) byteNaturalTwoHundredFiftySix)
def jsonNaturalSixtyFiveThousandFiveHundredThirtySix =
(naturalPowerOfTwo (byte-to-nat (byte 16)))
-- Delegates to the one owner (Std.Flag): this body is alpha-equivalent to
-- Std.Flag.inferenceFlagNot (binder renamed value<->flag, otherwise
-- identical) -- missed by `alpha-ast duplicates`' exact (binder-name-
-- sensitive) shape digest, found by manual inspection after that tool
-- grouped it with Std.Natural.naturalIsZero instead (also alpha-equivalent
-- to inferenceFlagNot, coincidentally under the same binder name "value").
def jsonFlagNot =
inferenceFlagNot
-- Delegates to the one owner (Std.Flag), which this file already had a
-- byte-for-byte copy of before `alpha-ast duplicates` found it (L24d).
def jsonFlagAnd =
inferenceFlagAnd
-- Delegates to the one owner (Std.Flag), which this file already had a
-- byte-for-byte copy of before `alpha-ast duplicates` found it (L24d).
def jsonFlagOr =
inferenceFlagOr
def jsonByteInHalfOpenRange =
(lambda unrestricted value : Byte .
(lambda unrestricted minimum : Byte .
(lambda unrestricted maximum : Byte .
(jsonFlagAnd (jsonFlagNot (byte-less-than value minimum)) (byte-less-than value maximum)))))
def jsonByteIsWhitespace =
(lambda unrestricted value : Byte .
(jsonFlagOr
(byte-equal value (byte 32))
(jsonFlagOr
(byte-equal value (byte 9))
(jsonFlagOr (byte-equal value (byte 10)) (byte-equal value (byte 13))))))
def jsonByteIsDigit =
(lambda unrestricted value : Byte . (jsonByteInHalfOpenRange value (byte 48) (byte 58)))
def jsonByteIsNonzeroDigit =
(lambda unrestricted value : Byte . (jsonByteInHalfOpenRange value (byte 49) (byte 58)))
-- First-order whitespace drop.
--
-- The previous definition folded a FUNCTION accumulator (`pi input . Bytes`) and,
-- inside each step, ran `bytes-eliminate` over the input. The runtime-graph
-- evaluator forces a fold's induction (and a `bytes-eliminate`'s ignored
-- tail-result) EAGERLY, so composing the two symbolically re-walked every suffix
-- at every fuel level -- an exponential blow-up. This version folds a FIRST-ORDER
-- value accumulator (the current byte string) with the O(1) native views
-- `bytes-head` / `bytes-tail`: at each step it either peels one leading
-- whitespace byte or keeps the string (idempotent once a non-whitespace byte is
-- reached). `bytes-head` of the empty string is byte 0, which is not whitespace,
-- so the empty input is a fixed point. The surviving bytes are identical to the
-- original; only the cost changed.
def jsonDropWhitespaceWithFuel =
(lambda unrestricted fuel : Nat .
(lambda unrestricted input : Bytes .
(nat-eliminate
(lambda unrestricted current : Nat . Bytes)
input
(lambda unrestricted predecessor : Nat .
(lambda unrestricted induction : Bytes .
(nat-eliminate
(lambda unrestricted whitespace : Nat . Bytes)
induction
(lambda unrestricted whitespacePredecessor : Nat .
(lambda unrestricted whitespaceInduction : Bytes . (bytes-tail induction)))
(jsonByteIsWhitespace (bytes-head induction)))))
fuel)))
-- Drop leading whitespace. When the first byte is not whitespace (the common
-- case for compact JSON, which has no inter-token whitespace) the answer is the
-- input unchanged, so we short-circuit in O(1) instead of running a
-- length-sized fold of no-ops. Only a genuine leading whitespace run pays the
-- O(run) fold. Behaviour is identical to `jsonDropWhitespaceWithFuel` over the
-- full length.
def jsonDropWhitespace =
(lambda unrestricted input : Bytes .
(nat-eliminate
(lambda unrestricted nonEmpty : Nat . Bytes)
(nat-eliminate
(lambda unrestricted leadingWhitespace : Nat . Bytes)
input
(lambda unrestricted whitespacePredecessor : Nat .
(lambda unrestricted whitespaceInduction : Bytes .
(jsonDropWhitespaceWithFuel (bytes-length input) input)))
(jsonByteIsWhitespace (bytes-head input)))
(lambda unrestricted emptyPredecessor : Nat .
(lambda unrestricted emptyInduction : Bytes . input))
(naturalIsZero (bytes-length input))))
def jsonConsumeLiteral =
(lambda unrestricted expected : Bytes .
(bytes-eliminate
(lambda unrestricted current : Bytes .
(pi unrestricted input : Bytes . (family JSONLiteralResult)))
(lambda unrestricted input : Bytes .
(constructor JSONLiteralResult JSONLiteralConsumed input))
(lambda unrestricted expectedHead : Byte .
(lambda unrestricted expectedTail : Bytes .
(lambda unrestricted induction : (pi unrestricted input : Bytes . (family JSONLiteralResult)) .
(lambda unrestricted input : Bytes .
(nat-eliminate
(lambda unrestricted nonEmpty : Nat . (family JSONLiteralResult))
(nat-eliminate
(lambda unrestricted equal : Nat . (family JSONLiteralResult))
(constructor JSONLiteralResult JSONLiteralFailed input)
(lambda unrestricted predecessor : Nat .
(lambda unrestricted equalInduction : (family JSONLiteralResult) .
(induction (bytes-tail input))))
(byte-equal expectedHead (bytes-head input)))
(lambda unrestricted emptyPredecessor : Nat .
(lambda unrestricted emptyInduction : (family JSONLiteralResult) .
(constructor JSONLiteralResult JSONLiteralFailed input)))
(naturalIsZero (bytes-length input)))))))
expected))
def jsonHexNibble =
(lambda unrestricted value : Byte .
(nat-eliminate
(lambda unrestricted decimal : Nat . Nat)
(nat-eliminate
(lambda unrestricted lower : Nat . Nat)
(nat-eliminate
(lambda unrestricted upper : Nat . Nat)
jsonNaturalSixteen
(lambda unrestricted predecessor : Nat .
(lambda unrestricted induction : Nat .
(naturalSaturatingSubtract (byte-to-nat value) (byte-to-nat (byte 55)))))
(jsonByteInHalfOpenRange value (byte 65) (byte 71)))
(lambda unrestricted predecessor : Nat .
(lambda unrestricted induction : Nat .
(naturalSaturatingSubtract (byte-to-nat value) (byte-to-nat (byte 87)))))
(jsonByteInHalfOpenRange value (byte 97) (byte 103)))
(lambda unrestricted predecessor : Nat .
(lambda unrestricted induction : Nat .
(naturalSaturatingSubtract (byte-to-nat value) (byte-to-nat (byte 48)))))
(jsonByteIsDigit value)))
def jsonHexQuadValue =
(lambda unrestricted a : Nat .
(lambda unrestricted b : Nat .
(lambda unrestricted c : Nat .
(lambda unrestricted d : Nat .
(naturalAdd
(naturalMultiply
(naturalAdd
(naturalMultiply
(naturalAdd (naturalMultiply a jsonNaturalSixteen) b)
jsonNaturalSixteen)
c)
jsonNaturalSixteen)
d)))))
-- Part of `jsonParseHexQuad`, lifted out to keep it inside the §28.3 size and
-- nesting limits; the parameters are the locals it still needs.
def jsonParseHexQuadPart1 =
(lambda unrestricted input : Bytes .
(lambda unrestricted a : Byte .
(lambda unrestricted b : Byte .
(lambda unrestricted c : Byte .
(lambda unrestricted d : Byte .
(lambda unrestricted remaining : Bytes .
(lambda unrestricted remainingInduction : (family JSONHexQuadResult) .
(app
(lambda unrestricted na : Nat .
(app
(lambda unrestricted nb : Nat .
(app
(lambda unrestricted nc : Nat .
(app
(lambda unrestricted nd : Nat .
(nat-eliminate
(lambda unrestricted valid : Nat . (family JSONHexQuadResult))
(constructor JSONHexQuadResult JSONHexQuadFailed input)
(lambda unrestricted predecessor : Nat .
(lambda unrestricted induction : (family JSONHexQuadResult) .
(constructor
JSONHexQuadResult
JSONHexQuadParsed
(jsonHexQuadValue na nb nc nd)
remaining)))
(jsonFlagAnd
(nat-less-than na jsonNaturalSixteen)
(jsonFlagAnd
(nat-less-than nb jsonNaturalSixteen)
(jsonFlagAnd
(nat-less-than nc jsonNaturalSixteen)
(nat-less-than nd jsonNaturalSixteen))))))
(jsonHexNibble d)))
(jsonHexNibble c)))
(jsonHexNibble b)))
(jsonHexNibble a)))))))))
-- First-order hex-quad reader. Each of the four byte reads was a
-- `bytes-eliminate` over the input, whose ignored tail-induction the runtime
-- forces -- a full re-walk of the whole remaining input per byte. Each is now an
-- O(1) `bytes-head` / `bytes-tail` peek guarded by an emptiness check, so the
-- four reads together are constant work. The bytes and result are unchanged.
def jsonParseHexQuad =
(lambda unrestricted input : Bytes .
(nat-eliminate
(lambda unrestricted nonEmpty : Nat . (family JSONHexQuadResult))
(app
(lambda unrestricted a : Byte .
(app
(lambda unrestricted afterA : Bytes .
(nat-eliminate
(lambda unrestricted nonEmpty : Nat . (family JSONHexQuadResult))
(app
(lambda unrestricted b : Byte .
(app
(lambda unrestricted afterB : Bytes .
(nat-eliminate
(lambda unrestricted nonEmpty : Nat . (family JSONHexQuadResult))
(app
(lambda unrestricted c : Byte .
(app
(lambda unrestricted afterC : Bytes .
(nat-eliminate
(lambda unrestricted nonEmpty : Nat .
(family JSONHexQuadResult))
(jsonParseHexQuadPart1
input
a
b
c
(bytes-head afterC)
(bytes-tail afterC)
(constructor JSONHexQuadResult JSONHexQuadFailed afterC))
(lambda unrestricted emptyPredecessor : Nat .
(lambda unrestricted emptyInduction : (family JSONHexQuadResult) .
(constructor JSONHexQuadResult JSONHexQuadFailed afterC)))
(naturalIsZero (bytes-length afterC))))
(bytes-tail afterB)))
(bytes-head afterB))
(lambda unrestricted emptyPredecessor : Nat .
(lambda unrestricted emptyInduction : (family JSONHexQuadResult) .
(constructor JSONHexQuadResult JSONHexQuadFailed afterB)))
(naturalIsZero (bytes-length afterB))))
(bytes-tail afterA)))
(bytes-head afterA))
(lambda unrestricted emptyPredecessor : Nat .
(lambda unrestricted emptyInduction : (family JSONHexQuadResult) .
(constructor JSONHexQuadResult JSONHexQuadFailed afterA)))
(naturalIsZero (bytes-length afterA))))
(bytes-tail input)))
(bytes-head input))
(lambda unrestricted emptyPredecessor : Nat .
(lambda unrestricted emptyInduction : (family JSONHexQuadResult) .
(constructor JSONHexQuadResult JSONHexQuadFailed input)))
(naturalIsZero (bytes-length input))))
def jsonStringFailure =
(lambda unrestricted code : (family JSONErrorCode) .
(lambda unrestricted remaining : Bytes .
(constructor JSONStringParseResult JSONStringParseFailed code remaining)))
def jsonStringPrepend =
(lambda unrestricted prefix : Bytes .
(lambda unrestricted suffix : (family JSONStringParseResult) .
(eliminate
JSONStringParseResult
(lambda unrestricted current : (family JSONStringParseResult) .
(family JSONStringParseResult))
suffix
(branch
JSONStringParsed
builder
remaining
.
(constructor
JSONStringParseResult
JSONStringParsed
(bytes-builder-append (bytes-builder-chunk prefix) builder)
remaining))
(branch
JSONStringParseFailed
code
remaining
.
(constructor JSONStringParseResult JSONStringParseFailed code remaining)))))
def jsonEncodeCodepointThen =
(lambda unrestricted continuation : (pi unrestricted input : Bytes . (family JSONStringParseResult)) .
(lambda unrestricted codepoint : Nat .
(lambda unrestricted remaining : Bytes .
(eliminate
UTF8CodepointEncodeResult
(lambda unrestricted current : (family UTF8CodepointEncodeResult) .
(family JSONStringParseResult))
(utf8EncodeCodepoint
(constructor
UTF8Codepoint
UTF8CodepointValue
(modelWord32FromNaturalTruncated codepoint)))
(branch
UTF8CodepointEncoded
encoded
.
(jsonStringPrepend encoded (continuation remaining)))
(branch
UTF8CodepointRejected
code
.
(jsonStringFailure (constructor JSONErrorCode JSONUnicodeEscapeInvalid) remaining))))))
def jsonParseUnicodeEscape =
(lambda unrestricted continuation : (pi unrestricted input : Bytes . (family JSONStringParseResult)) .
(lambda unrestricted input : Bytes .
(eliminate
JSONHexQuadResult
(lambda unrestricted current : (family JSONHexQuadResult) . (family JSONStringParseResult))
(jsonParseHexQuad input)
(branch
JSONHexQuadParsed
high
remaining
.
(nat-eliminate
(lambda unrestricted highSurrogate : Nat . (family JSONStringParseResult))
(nat-eliminate
(lambda unrestricted lowSurrogate : Nat . (family JSONStringParseResult))
(jsonEncodeCodepointThen continuation high remaining)
(lambda unrestricted predecessor : Nat .
(lambda unrestricted induction : (family JSONStringParseResult) .
(jsonStringFailure
(constructor JSONErrorCode JSONUnicodeLowWithoutHigh)
remaining)))
(jsonFlagAnd
(jsonFlagNot (nat-less-than high jsonNaturalFiftySixThousandThreeHundredTwenty))
(nat-less-than high jsonNaturalFiftySevenThousandThreeHundredFortyFour)))
(lambda unrestricted predecessor : Nat .
(lambda unrestricted induction : (family JSONStringParseResult) .
(eliminate
JSONLiteralResult
(lambda unrestricted current : (family JSONLiteralResult) .
(family JSONStringParseResult))
(jsonConsumeLiteral b"\\u" remaining)
(branch
JSONLiteralConsumed
afterPrefix
.
(eliminate
JSONHexQuadResult
(lambda unrestricted current : (family JSONHexQuadResult) .
(family JSONStringParseResult))
(jsonParseHexQuad afterPrefix)
(branch
JSONHexQuadParsed
low
afterLow
.
(nat-eliminate
(lambda unrestricted validLow : Nat . (family JSONStringParseResult))
(jsonStringFailure
(constructor JSONErrorCode JSONUnicodeHighWithoutLow)
afterLow)
(lambda unrestricted validPredecessor : Nat .
(lambda unrestricted validInduction : (family JSONStringParseResult) .
(jsonEncodeCodepointThen
continuation
(naturalAdd
jsonNaturalSixtyFiveThousandFiveHundredThirtySix
(naturalAdd
(naturalMultiply
(naturalSaturatingSubtract
high
jsonNaturalFiftyFiveThousandTwoHundredNinetySix)
jsonNaturalOneThousandTwentyFour)
(naturalSaturatingSubtract
low
jsonNaturalFiftySixThousandThreeHundredTwenty)))
afterLow)))
(jsonFlagAnd
(jsonFlagNot
(nat-less-than low jsonNaturalFiftySixThousandThreeHundredTwenty))
(nat-less-than low jsonNaturalFiftySevenThousandThreeHundredFortyFour))))
(branch
JSONHexQuadFailed
failureRemaining
.
(jsonStringFailure
(constructor JSONErrorCode JSONUnicodeHighWithoutLow)
failureRemaining))))
(branch
JSONLiteralFailed
failureRemaining
.
(jsonStringFailure
(constructor JSONErrorCode JSONUnicodeHighWithoutLow)
failureRemaining)))))
(jsonFlagAnd
(jsonFlagNot (nat-less-than high jsonNaturalFiftyFiveThousandTwoHundredNinetySix))
(nat-less-than high jsonNaturalFiftySixThousandThreeHundredTwenty))))
(branch
JSONHexQuadFailed
remaining
.
(jsonStringFailure (constructor JSONErrorCode JSONUnicodeEscapeInvalid) remaining)))))
def jsonParseEscape =
(lambda unrestricted continuation : (pi unrestricted input : Bytes . (family JSONStringParseResult)) .
(lambda unrestricted input : Bytes .
(nat-eliminate
(lambda unrestricted nonEmpty : Nat . (family JSONStringParseResult))
(app
(lambda unrestricted escaped : Byte .
(app
(lambda unrestricted remaining : Bytes .
(nat-eliminate
(lambda unrestricted quote : Nat . (family JSONStringParseResult))
(nat-eliminate
(lambda unrestricted slash : Nat . (family JSONStringParseResult))
(nat-eliminate
(lambda unrestricted solidus : Nat . (family JSONStringParseResult))
(nat-eliminate
(lambda unrestricted backspace : Nat . (family JSONStringParseResult))
(nat-eliminate
(lambda unrestricted formFeed : Nat . (family JSONStringParseResult))
(nat-eliminate
(lambda unrestricted newline : Nat . (family JSONStringParseResult))
(nat-eliminate
(lambda unrestricted carriage : Nat . (family JSONStringParseResult))
(nat-eliminate
(lambda unrestricted tab : Nat . (family JSONStringParseResult))
(nat-eliminate
(lambda unrestricted unicode : Nat .
(family JSONStringParseResult))
(jsonStringFailure
(constructor JSONErrorCode JSONEscapeInvalid)
input)
(lambda unrestricted predecessor : Nat .
(lambda unrestricted induction : (family JSONStringParseResult) .
(jsonParseUnicodeEscape continuation remaining)))
(byte-equal escaped (byte 117)))
(lambda unrestricted predecessor : Nat .
(lambda unrestricted induction : (family JSONStringParseResult) .
(jsonStringPrepend (bytes 9) (continuation remaining))))
(byte-equal escaped (byte 116)))
(lambda unrestricted predecessor : Nat .
(lambda unrestricted induction : (family JSONStringParseResult) .
(jsonStringPrepend (bytes 13) (continuation remaining))))
(byte-equal escaped (byte 114)))
(lambda unrestricted predecessor : Nat .
(lambda unrestricted induction : (family JSONStringParseResult) .
(jsonStringPrepend (bytes 10) (continuation remaining))))
(byte-equal escaped (byte 110)))
(lambda unrestricted predecessor : Nat .
(lambda unrestricted induction : (family JSONStringParseResult) .
(jsonStringPrepend (bytes 12) (continuation remaining))))
(byte-equal escaped (byte 102)))
(lambda unrestricted predecessor : Nat .
(lambda unrestricted induction : (family JSONStringParseResult) .
(jsonStringPrepend (bytes 8) (continuation remaining))))
(byte-equal escaped (byte 98)))
(lambda unrestricted predecessor : Nat .
(lambda unrestricted induction : (family JSONStringParseResult) .
(jsonStringPrepend b"/" (continuation remaining))))
(byte-equal escaped (byte 47)))
(lambda unrestricted predecessor : Nat .
(lambda unrestricted induction : (family JSONStringParseResult) .
(jsonStringPrepend b"\\" (continuation remaining))))
(byte-equal escaped (byte 92)))
(lambda unrestricted predecessor : Nat .
(lambda unrestricted induction : (family JSONStringParseResult) .
(jsonStringPrepend b"\"" (continuation remaining))))
(byte-equal escaped (byte 34))))
(bytes-tail input)))
(bytes-head input))
(lambda unrestricted emptyPredecessor : Nat .
(lambda unrestricted emptyInduction : (family JSONStringParseResult) .
(jsonStringFailure (constructor JSONErrorCode JSONStringUnterminated) input)))
(naturalIsZero (bytes-length input)))))
-- One first-order string-body step over the `JSONStringLoop` accumulator.
--
-- `Going builder remaining` peeks the head with the O(1) `bytes-head` view
-- (never the tail-forcing `bytes-eliminate`): a closing quote absorbs to `Done`,
-- a control byte to `Failed`, `\` decodes exactly one escape via `jsonParseEscape`
-- (given a trivial continuation that just packages the position after the escape,
-- so the existing CPS escape decoder is reused unchanged), and any other byte is
-- appended to the decoded-prefix builder. `Done`/`Failed` are fixed points. Bytes
-- are appended front-to-back, matching the original's head-first prepend, so the
-- decoded string is byte-for-byte identical.
def jsonParseStringBodyStep =
(lambda unrestricted acc : (family JSONStringLoop) .
(eliminate
JSONStringLoop
(lambda unrestricted current : (family JSONStringLoop) . (family JSONStringLoop))
acc
(branch
JSONStringLoopGoing
builder
remaining
.
(nat-eliminate
(lambda unrestricted nonEmpty : Nat . (family JSONStringLoop))
(app
(lambda unrestricted head : Byte .
(nat-eliminate
(lambda unrestricted quote : Nat . (family JSONStringLoop))
(nat-eliminate
(lambda unrestricted escape : Nat . (family JSONStringLoop))
(nat-eliminate
(lambda unrestricted control : Nat . (family JSONStringLoop))
(constructor
JSONStringLoop
JSONStringLoopGoing
(bytes-builder-append builder (bytes-builder-chunk (bytes-cons head b"")))
(bytes-tail remaining))
(lambda unrestricted controlPredecessor : Nat .
(lambda unrestricted controlInduction : (family JSONStringLoop) .
(constructor
JSONStringLoop
JSONStringLoopFailed
(constructor JSONErrorCode JSONStringControlCharacter)
remaining)))
(byte-less-than head (byte 32)))
(lambda unrestricted escapePredecessor : Nat .
(lambda unrestricted escapeInduction : (family JSONStringLoop) .
(eliminate
JSONStringParseResult
(lambda unrestricted current : (family JSONStringParseResult) .
(family JSONStringLoop))
(jsonParseEscape
(lambda unrestricted escRemaining : Bytes .
(constructor
JSONStringParseResult
JSONStringParsed
(bytes-builder-empty)
escRemaining))
(bytes-tail remaining))
(branch
JSONStringParsed
escBuilder
afterEsc
.
(constructor
JSONStringLoop
JSONStringLoopGoing
(bytes-builder-append builder escBuilder)
afterEsc))
(branch
JSONStringParseFailed
code
failRemaining
.
(constructor JSONStringLoop JSONStringLoopFailed code failRemaining)))))
(byte-equal head (byte 92)))
(lambda unrestricted quotePredecessor : Nat .
(lambda unrestricted quoteInduction : (family JSONStringLoop) .
(constructor JSONStringLoop JSONStringLoopDone builder (bytes-tail remaining))))
(byte-equal head (byte 34))))
(bytes-head remaining))
(lambda unrestricted emptyPredecessor : Nat .
(lambda unrestricted emptyInduction : (family JSONStringLoop) .
(constructor
JSONStringLoop
JSONStringLoopFailed
(constructor JSONErrorCode JSONStringUnterminated)
remaining)))
(naturalIsZero (bytes-length remaining))))
(branch JSONStringLoopDone doneBuilder doneRemaining . acc)
(branch JSONStringLoopFailed failError failRemaining . acc)))
-- First-order string-body scan: fold the step `fuel` times over a VALUE
-- accumulator (no function-valued fold, no tail-forcing `bytes-eliminate`), then
-- project. `fuel = bytes-length input` bounds the scan; each step consumes at
-- least one input byte before `Done`/`Failed`, so a well-fuelled call never ends
-- `Going`.
def jsonParseStringBodyWithFuel =
(lambda unrestricted fuel : Nat .
(lambda unrestricted input : Bytes .
(eliminate
JSONStringLoop
(lambda unrestricted current : (family JSONStringLoop) . (family JSONStringParseResult))
(nat-eliminate
(lambda unrestricted current : Nat . (family JSONStringLoop))
(constructor JSONStringLoop JSONStringLoopGoing (bytes-builder-empty) input)
(lambda unrestricted predecessor : Nat .
(lambda unrestricted induction : (family JSONStringLoop) .
(jsonParseStringBodyStep induction)))
fuel)
(branch
JSONStringLoopGoing
builder
remaining
.
(jsonStringFailure (constructor JSONErrorCode JSONStringUnterminated) remaining))
(branch
JSONStringLoopDone
builder
remaining
.
(constructor JSONStringParseResult JSONStringParsed builder remaining))
(branch
JSONStringLoopFailed
code
remaining
.
(constructor JSONStringParseResult JSONStringParseFailed code remaining)))))
def jsonParseStringBody =
(lambda unrestricted input : Bytes . (jsonParseStringBodyWithFuel (bytes-length input) input))
-- One first-order digit-take step over the `JSONDigitSplit` accumulator.
--
-- The head is peeked with the O(1) `bytes-head` view (not the tail-forcing
-- `bytes-eliminate`): a digit is appended to the builder and the remaining
-- advances; a non-digit or the empty string is a fixed point (the accumulator is
-- returned unchanged, so `remaining` keeps pointing at the first non-digit and
-- every later step is a no-op). Digits are appended front-to-back, matching the
-- original's head-first prepend.
def jsonTakeDigitsStep =
(lambda unrestricted acc : (family JSONDigitSplit) .
(eliminate
JSONDigitSplit
(lambda unrestricted current : (family JSONDigitSplit) . (family JSONDigitSplit))
acc
(branch
JSONDigitSplitValue
builder
remaining
count
.
(nat-eliminate
(lambda unrestricted nonEmpty : Nat . (family JSONDigitSplit))
(app
(lambda unrestricted head : Byte .
(nat-eliminate
(lambda unrestricted digit : Nat . (family JSONDigitSplit))
acc
(lambda unrestricted digitPredecessor : Nat .
(lambda unrestricted digitInduction : (family JSONDigitSplit) .
(constructor
JSONDigitSplit
JSONDigitSplitValue
(bytes-builder-append builder (bytes-builder-chunk (bytes-cons head b"")))
(bytes-tail remaining)
(succ count))))
(jsonByteIsDigit head)))
(bytes-head remaining))
(lambda unrestricted emptyPredecessor : Nat .
(lambda unrestricted emptyInduction : (family JSONDigitSplit) . acc))
(naturalIsZero (bytes-length remaining))))))
-- First-order leading-digit scan: fold the step `fuel` times over a VALUE
-- accumulator (no function-valued fold, no tail-forcing `bytes-eliminate`).
def jsonTakeDigitsWithFuel =
(lambda unrestricted fuel : Nat .
(lambda unrestricted input : Bytes .
(nat-eliminate
(lambda unrestricted current : Nat . (family JSONDigitSplit))
(constructor JSONDigitSplit JSONDigitSplitValue (bytes-builder-empty) input zero)
(lambda unrestricted predecessor : Nat .
(lambda unrestricted induction : (family JSONDigitSplit) . (jsonTakeDigitsStep induction)))
fuel)))
def jsonTakeDigits =
(lambda unrestricted input : Bytes . (jsonTakeDigitsWithFuel (bytes-length input) input))
def jsonNumberFailure =
(lambda unrestricted code : (family JSONErrorCode) .
(lambda unrestricted remaining : Bytes .
(constructor JSONNumberParseResult JSONNumberParseFailed code remaining)))
-- First-order exponent tail. The three `bytes-eliminate` reads (the exponent
-- marker over the whole remaining input, and the optional sign over its tail)
-- forced their ignored tail-inductions -- a re-walk of the remaining per call,
-- on a path taken for EVERY number. Each is now an O(1) `bytes-head` /
-- `bytes-tail` peek guarded by emptiness. The emitted number bytes are unchanged.
def jsonParseNumberExponent =
(lambda unrestricted prefix : BytesBuilder .
(lambda unrestricted input : Bytes .
(nat-eliminate
(lambda unrestricted nonEmpty : Nat . (family JSONNumberParseResult))
(app
(lambda unrestricted marker : Byte .
(app
(lambda unrestricted tail : Bytes .
(nat-eliminate
(lambda unrestricted exponent : Nat . (family JSONNumberParseResult))
(constructor
JSONNumberParseResult
JSONNumberParsed
(bytes-builder-build prefix)
(bytes-cons marker tail))
(lambda unrestricted exponentPredecessor : Nat .
(lambda unrestricted exponentInduction : (family JSONNumberParseResult) .
(app
(lambda unrestricted signedPrefix : BytesBuilder .
(app
(lambda unrestricted afterSign : Bytes .
(eliminate
JSONDigitSplit
(lambda unrestricted current : (family JSONDigitSplit) .
(family JSONNumberParseResult))
(jsonTakeDigits afterSign)
(branch
JSONDigitSplitValue
digits
remaining
count
.
(nat-eliminate
(lambda unrestricted nonempty : Nat .
(family JSONNumberParseResult))
(jsonNumberFailure
(constructor JSONErrorCode JSONNumberExponentDigitsMissing)
afterSign)
(lambda unrestricted predecessor : Nat .
(lambda unrestricted induction : (family JSONNumberParseResult) .
(constructor
JSONNumberParseResult
JSONNumberParsed
(bytes-builder-build
(bytes-builder-append signedPrefix digits))
remaining)))
count))))
(nat-eliminate
(lambda unrestricted signNonEmpty : Nat . Bytes)
(app
(lambda unrestricted sign : Byte .
(app
(lambda unrestricted signTail : Bytes .
(nat-eliminate
(lambda unrestricted signed : Nat . Bytes)
tail
(lambda unrestricted predecessor : Nat .
(lambda unrestricted induction : Bytes . signTail))
(jsonFlagOr
(byte-equal sign (byte 43))
(byte-equal sign (byte 45)))))
(bytes-tail tail)))
(bytes-head tail))
(lambda unrestricted signEmptyPredecessor : Nat .
(lambda unrestricted signEmptyInduction : Bytes . tail))
(naturalIsZero (bytes-length tail)))))
(bytes-builder-append
prefix
(bytes-builder-chunk
(nat-eliminate
(lambda unrestricted signNonEmpty : Nat . Bytes)
(app
(lambda unrestricted sign : Byte .
(app
(lambda unrestricted signTail : Bytes .
(nat-eliminate
(lambda unrestricted signed : Nat . Bytes)
(bytes-cons marker b"")
(lambda unrestricted predecessor : Nat .
(lambda unrestricted induction : Bytes .
(bytes-cons marker (bytes-cons sign b""))))
(jsonFlagOr
(byte-equal sign (byte 43))
(byte-equal sign (byte 45)))))
(bytes-tail tail)))
(bytes-head tail))
(lambda unrestricted signEmptyPredecessor : Nat .
(lambda unrestricted signEmptyInduction : Bytes .
(bytes-cons marker b"")))
(naturalIsZero (bytes-length tail))))))))
(jsonFlagOr (byte-equal marker (byte 101)) (byte-equal marker (byte 69)))))
(bytes-tail input)))
(bytes-head input))
(lambda unrestricted emptyPredecessor : Nat .
(lambda unrestricted emptyInduction : (family JSONNumberParseResult) .
(constructor
JSONNumberParseResult
JSONNumberParsed
(bytes-builder-build prefix)
b"")))
(naturalIsZero (bytes-length input)))))
def jsonParseNumberFraction =
(lambda unrestricted prefix : BytesBuilder .
(lambda unrestricted input : Bytes .
(nat-eliminate
(lambda unrestricted nonEmpty : Nat . (family JSONNumberParseResult))
(app
(lambda unrestricted marker : Byte .
(app
(lambda unrestricted tail : Bytes .
(nat-eliminate
(lambda unrestricted fraction : Nat . (family JSONNumberParseResult))
(jsonParseNumberExponent prefix (bytes-cons marker tail))
(lambda unrestricted fractionPredecessor : Nat .
(lambda unrestricted fractionInduction : (family JSONNumberParseResult) .
(eliminate
JSONDigitSplit
(lambda unrestricted current : (family JSONDigitSplit) .
(family JSONNumberParseResult))
(jsonTakeDigits tail)
(branch
JSONDigitSplitValue
digits
remaining
count
.
(nat-eliminate
(lambda unrestricted nonempty : Nat . (family JSONNumberParseResult))
(jsonNumberFailure
(constructor JSONErrorCode JSONNumberFractionDigitsMissing)
tail)
(lambda unrestricted predecessor : Nat .
(lambda unrestricted induction : (family JSONNumberParseResult) .
(jsonParseNumberExponent
(bytes-builder-append
prefix
(bytes-builder-append (bytes-builder-chunk b".") digits))
remaining)))
count)))))
(byte-equal marker (byte 46))))
(bytes-tail input)))
(bytes-head input))
(lambda unrestricted emptyPredecessor : Nat .
(lambda unrestricted emptyInduction : (family JSONNumberParseResult) .
(jsonParseNumberExponent prefix b"")))
(naturalIsZero (bytes-length input)))))
def jsonParseNumberUnsigned =
(lambda unrestricted prefix : BytesBuilder .
(lambda unrestricted input : Bytes .
(nat-eliminate
(lambda unrestricted nonEmpty : Nat . (family JSONNumberParseResult))
(app
(lambda unrestricted first : Byte .
(app
(lambda unrestricted tail : Bytes .
(nat-eliminate
(lambda unrestricted zeroDigit : Nat . (family JSONNumberParseResult))
(nat-eliminate
(lambda unrestricted nonzero : Nat . (family JSONNumberParseResult))
(jsonNumberFailure (constructor JSONErrorCode JSONNumberIntegerInvalid) input)
(lambda unrestricted predecessor : Nat .
(lambda unrestricted induction : (family JSONNumberParseResult) .
(eliminate
JSONDigitSplit
(lambda unrestricted current : (family JSONDigitSplit) .
(family JSONNumberParseResult))
(jsonTakeDigits tail)
(branch
JSONDigitSplitValue
digits
remaining
count
.
(jsonParseNumberFraction
(bytes-builder-append
prefix
(bytes-builder-append
(bytes-builder-chunk (bytes-cons first b""))
digits))
remaining)))))
(jsonByteIsNonzeroDigit first))
(lambda unrestricted predecessor : Nat .
(lambda unrestricted induction : (family JSONNumberParseResult) .
(jsonParseNumberFraction
(bytes-builder-append prefix (bytes-builder-chunk b"0"))
tail)))
(byte-equal first (byte 48))))
(bytes-tail input)))
(bytes-head input))
(lambda unrestricted emptyPredecessor : Nat .
(lambda unrestricted emptyInduction : (family JSONNumberParseResult) .
(jsonNumberFailure (constructor JSONErrorCode JSONNumberIntegerInvalid) input)))
(naturalIsZero (bytes-length input)))))
def jsonParseNumber =
(lambda unrestricted input : Bytes .
(nat-eliminate
(lambda unrestricted nonEmpty : Nat . (family JSONNumberParseResult))
(app
(lambda unrestricted head : Byte .
(app
(lambda unrestricted tail : Bytes .
(nat-eliminate
(lambda unrestricted negative : Nat . (family JSONNumberParseResult))
(jsonParseNumberUnsigned (bytes-builder-empty) input)
(lambda unrestricted predecessor : Nat .
(lambda unrestricted induction : (family JSONNumberParseResult) .
(jsonParseNumberUnsigned (bytes-builder-chunk b"-") tail)))
(byte-equal head (byte 45))))
(bytes-tail input)))
(bytes-head input))
(lambda unrestricted emptyPredecessor : Nat .
(lambda unrestricted emptyInduction : (family JSONNumberParseResult) .
(jsonNumberFailure (constructor JSONErrorCode JSONNumberIntegerInvalid) input)))
(naturalIsZero (bytes-length input))))
def jsonParseFailure =
(lambda unrestricted code : (family JSONErrorCode) .
(lambda unrestricted remaining : Bytes .
(constructor JSONParseResult JSONParseFailed code remaining)))
def jsonParserValue =
(lambda unrestricted parser : (family JSONParser) .
(eliminate
JSONParser
(lambda unrestricted current : (family JSONParser) .
(pi unrestricted input : Bytes . (family JSONParseResult)))
parser
(branch JSONParserValue valueFunction objectFunction arrayFunction . valueFunction)))
def jsonParserObject =
(lambda unrestricted parser : (family JSONParser) .
(eliminate
JSONParser
(lambda unrestricted current : (family JSONParser) .
(pi unrestricted input : Bytes . (family JSONParseResult)))
parser
(branch JSONParserValue valueFunction objectFunction arrayFunction . objectFunction)))
def jsonParserArray =
(lambda unrestricted parser : (family JSONParser) .
(eliminate
JSONParser
(lambda unrestricted current : (family JSONParser) .
(pi unrestricted input : Bytes . (family JSONParseResult)))
parser
(branch JSONParserValue valueFunction objectFunction arrayFunction . arrayFunction)))
def jsonObjectContainsKey =
(lambda unrestricted wanted : Bytes .
(lambda unrestricted members : (family JSON) .
(eliminate
JSON
(lambda unrestricted current : (family JSON) . Nat)
members
(branch JSONObject nested nestedInduction . zero)
(branch JSONObjectEnd . zero)
(branch
JSONObjectMember
key
value
tail
valueInduction
tailInduction
.
(jsonFlagOr (bytes-equal wanted key) tailInduction))
(branch JSONArray values valuesInduction . zero)
(branch JSONArrayEnd . zero)
(branch JSONArrayNext head tail headInduction tailInduction . zero)
(branch JSONString text . zero)
(branch JSONNumber number . zero)
(branch JSONBoolean value . zero)
(branch JSONNull . zero))))
-- Part of `jsonParseObjectMembersStep`, lifted out to keep it inside the §28.3 size and
-- nesting limits; the parameters are the locals it still needs.
def jsonParseObjectMembersStepPart1 =
(lambda unrestricted parser : (family JSONParser) .
(lambda unrestricted key : Bytes .
(lambda unrestricted value : (family JSON) .
(lambda unrestricted delimiterInput : Bytes .
(lambda unrestricted delimiter : Byte .
(lambda unrestricted afterDelimiter : Bytes .
(nat-eliminate
(lambda unrestricted comma : Nat . (family JSONParseResult))
(nat-eliminate
(lambda unrestricted close : Nat . (family JSONParseResult))
(jsonParseFailure
(constructor JSONErrorCode JSONObjectDelimiterMissing)
delimiterInput)
(lambda unrestricted closePredecessor : Nat .
(lambda unrestricted closeInduction : (family JSONParseResult) .
(constructor
JSONParseResult
JSONParsed
(constructor
JSON
JSONObjectMember
key
value
(constructor JSON JSONObjectEnd))
afterDelimiter)))
(byte-equal delimiter (byte 125)))
(lambda unrestricted commaPredecessor : Nat .
(lambda unrestricted commaInduction : (family JSONParseResult) .
(app
(lambda unrestricted nextInput : Bytes .
(nat-eliminate
(lambda unrestricted nonEmpty : Nat . (family JSONParseResult))
(app
(lambda unrestricted nextHead : Byte .
(app
(lambda unrestricted nextTail : Bytes .
(nat-eliminate
(lambda unrestricted trailingComma : Nat .
(family JSONParseResult))
(eliminate
JSONParseResult
(lambda unrestricted current : (family JSONParseResult) .
(family JSONParseResult))
(jsonParserObject parser nextInput)
(branch
JSONParsed
members
remaining
.
(constructor
JSONParseResult
JSONParsed
(constructor JSON JSONObjectMember key value members)
remaining))
(branch
JSONParseFailed
code
remaining
.
(jsonParseFailure code remaining)))
(lambda unrestricted trailingPredecessor : Nat .
(lambda unrestricted trailingInduction : (family JSONParseResult) .
(jsonParseFailure
(constructor JSONErrorCode JSONObjectKeyNotString)
nextInput)))
(byte-equal nextHead (byte 125))))
(bytes-tail nextInput)))
(bytes-head nextInput))
(lambda unrestricted emptyPredecessor : Nat .
(lambda unrestricted emptyInduction : (family JSONParseResult) .
(jsonParseFailure
(constructor JSONErrorCode JSONObjectKeyNotString)
nextInput)))
(naturalIsZero (bytes-length nextInput))))
(jsonDropWhitespace afterDelimiter))))
(byte-equal delimiter (byte 44)))))))))
-- Part of `jsonParseObjectMembersStep`, lifted out to keep it inside the §28.3 size and
-- nesting limits; the parameters are the locals it still needs.
def jsonParseObjectMembersStepPart2 =
(lambda unrestricted parser : (family JSONParser) .
(lambda unrestricted key : Bytes .
(lambda unrestricted colonInput : Bytes .
(lambda unrestricted colon : Byte .
(lambda unrestricted afterColon : Bytes .
(lambda unrestricted afterColonInduction : (family JSONParseResult) .
(nat-eliminate
(lambda unrestricted validColon : Nat . (family JSONParseResult))
(jsonParseFailure (constructor JSONErrorCode JSONObjectColonMissing) colonInput)
(lambda unrestricted colonPredecessor : Nat .
(lambda unrestricted colonInduction : (family JSONParseResult) .
(eliminate
JSONParseResult
(lambda unrestricted current : (family JSONParseResult) .
(family JSONParseResult))
(jsonParserValue parser afterColon)
(branch
JSONParsed
value
afterValue
.
(app
(lambda unrestricted delimiterInput : Bytes .
(nat-eliminate
(lambda unrestricted nonEmpty : Nat . (family JSONParseResult))
(app
(lambda unrestricted delimiter : Byte .
(app
(lambda unrestricted afterDelimiter : Bytes .
(jsonParseObjectMembersStepPart1
parser
key
value
delimiterInput
delimiter
afterDelimiter))
(bytes-tail delimiterInput)))
(bytes-head delimiterInput))
(lambda unrestricted emptyPredecessor : Nat .
(lambda unrestricted emptyInduction : (family JSONParseResult) .
(jsonParseFailure
(constructor JSONErrorCode JSONObjectDelimiterMissing)
delimiterInput)))
(naturalIsZero (bytes-length delimiterInput))))
(jsonDropWhitespace afterValue)))
(branch JSONParseFailed code remaining . (jsonParseFailure code remaining)))))
(byte-equal colon (byte 58)))))))))
def jsonParseObjectMembersStep =
(lambda unrestricted parser : (family JSONParser) .
(lambda unrestricted input : Bytes .
(app
(lambda unrestricted clean : Bytes .
(nat-eliminate
(lambda unrestricted nonEmpty : Nat . (family JSONParseResult))
(app
(lambda unrestricted head : Byte .
(app
(lambda unrestricted tail : Bytes .
(nat-eliminate
(lambda unrestricted closed : Nat . (family JSONParseResult))
(nat-eliminate
(lambda unrestricted quote : Nat . (family JSONParseResult))
(jsonParseFailure (constructor JSONErrorCode JSONObjectKeyNotString) clean)
(lambda unrestricted quotePredecessor : Nat .
(lambda unrestricted quoteInduction : (family JSONParseResult) .
(eliminate
JSONStringParseResult
(lambda unrestricted current : (family JSONStringParseResult) .
(family JSONParseResult))
(jsonParseStringBody tail)
(branch
JSONStringParsed
keyBuilder
afterKey
.
(app
(lambda unrestricted key : Bytes .
(app
(lambda unrestricted colonInput : Bytes .
(nat-eliminate
(lambda unrestricted nonEmpty : Nat .
(family JSONParseResult))
(jsonParseObjectMembersStepPart2
parser
key
colonInput
(bytes-head colonInput)
(bytes-tail colonInput)
(jsonParseFailure
(constructor JSONErrorCode JSONObjectColonMissing)
colonInput))
(lambda unrestricted emptyPredecessor : Nat .
(lambda unrestricted emptyInduction : (family JSONParseResult) .
(jsonParseFailure
(constructor JSONErrorCode JSONObjectColonMissing)
colonInput)))
(naturalIsZero (bytes-length colonInput))))
(jsonDropWhitespace afterKey)))
(bytes-builder-build keyBuilder)))
(branch
JSONStringParseFailed
code
remaining
.
(jsonParseFailure code remaining)))))
(byte-equal head (byte 34)))
(lambda unrestricted closePredecessor : Nat .
(lambda unrestricted closeInduction : (family JSONParseResult) .
(constructor
JSONParseResult
JSONParsed
(constructor JSON JSONObjectEnd)
tail)))
(byte-equal head (byte 125))))
(bytes-tail clean)))
(bytes-head clean))
(lambda unrestricted emptyPredecessor : Nat .
(lambda unrestricted emptyInduction : (family JSONParseResult) .
(jsonParseFailure (constructor JSONErrorCode JSONUnexpectedEnd) clean)))
(naturalIsZero (bytes-length clean))))
(jsonDropWhitespace input))))
-- Part of `jsonParseArrayValuesStep`, lifted out to keep it inside the §28.3 size and
-- nesting limits; the parameters are the locals it still needs.
def jsonParseArrayValuesStepPart1 =
(lambda unrestricted parser : (family JSONParser) .
(lambda unrestricted value : (family JSON) .
(lambda unrestricted delimiterInput : Bytes .
(lambda unrestricted delimiter : Byte .
(lambda unrestricted afterDelimiter : Bytes .
(lambda unrestricted afterDelimiterInduction : (family JSONParseResult) .
(nat-eliminate
(lambda unrestricted comma : Nat . (family JSONParseResult))
(nat-eliminate
(lambda unrestricted close : Nat . (family JSONParseResult))
(jsonParseFailure
(constructor JSONErrorCode JSONArrayDelimiterMissing)
delimiterInput)
(lambda unrestricted closePredecessor : Nat .
(lambda unrestricted closeInduction : (family JSONParseResult) .
(constructor
JSONParseResult
JSONParsed
(constructor JSON JSONArrayNext value (constructor JSON JSONArrayEnd))
afterDelimiter)))
(byte-equal delimiter (byte 93)))
(lambda unrestricted commaPredecessor : Nat .
(lambda unrestricted commaInduction : (family JSONParseResult) .
(app
(lambda unrestricted nextInput : Bytes .
(nat-eliminate
(lambda unrestricted nonEmpty : Nat . (family JSONParseResult))
(app
(lambda unrestricted nextHead : Byte .
(app
(lambda unrestricted nextTail : Bytes .
(nat-eliminate
(lambda unrestricted trailingComma : Nat .
(family JSONParseResult))
(eliminate
JSONParseResult
(lambda unrestricted current : (family JSONParseResult) .
(family JSONParseResult))
(jsonParserArray parser nextInput)
(branch
JSONParsed
values
remaining
.
(constructor
JSONParseResult
JSONParsed
(constructor JSON JSONArrayNext value values)
remaining))
(branch
JSONParseFailed
code
remaining
.
(jsonParseFailure code remaining)))
(lambda unrestricted trailingPredecessor : Nat .
(lambda unrestricted trailingInduction : (family JSONParseResult) .
(jsonParseFailure
(constructor JSONErrorCode JSONInvalidValue)
nextInput)))
(byte-equal nextHead (byte 93))))
(bytes-tail nextInput)))
(bytes-head nextInput))
(lambda unrestricted emptyPredecessor : Nat .
(lambda unrestricted emptyInduction : (family JSONParseResult) .
(jsonParseFailure
(constructor JSONErrorCode JSONInvalidValue)
nextInput)))
(naturalIsZero (bytes-length nextInput))))
(jsonDropWhitespace afterDelimiter))))
(byte-equal delimiter (byte 44)))))))))
def jsonParseArrayValuesStep =
(lambda unrestricted parser : (family JSONParser) .
(lambda unrestricted input : Bytes .
(app
(lambda unrestricted clean : Bytes .
(nat-eliminate
(lambda unrestricted nonEmpty : Nat . (family JSONParseResult))
(app
(lambda unrestricted head : Byte .
(app
(lambda unrestricted tail : Bytes .
(nat-eliminate
(lambda unrestricted closed : Nat . (family JSONParseResult))
(eliminate
JSONParseResult
(lambda unrestricted current : (family JSONParseResult) .
(family JSONParseResult))
(jsonParserValue parser clean)
(branch
JSONParsed
value
afterValue
.
(app
(lambda unrestricted delimiterInput : Bytes .
(nat-eliminate
(lambda unrestricted nonEmpty : Nat . (family JSONParseResult))
(jsonParseArrayValuesStepPart1
parser
value
delimiterInput
(bytes-head delimiterInput)
(bytes-tail delimiterInput)
(jsonParseFailure
(constructor JSONErrorCode JSONArrayDelimiterMissing)
delimiterInput))
(lambda unrestricted emptyPredecessor : Nat .
(lambda unrestricted emptyInduction : (family JSONParseResult) .
(jsonParseFailure
(constructor JSONErrorCode JSONArrayDelimiterMissing)
delimiterInput)))
(naturalIsZero (bytes-length delimiterInput))))
(jsonDropWhitespace afterValue)))
(branch JSONParseFailed code remaining . (jsonParseFailure code remaining)))
(lambda unrestricted closePredecessor : Nat .
(lambda unrestricted closeInduction : (family JSONParseResult) .
(constructor
JSONParseResult
JSONParsed
(constructor JSON JSONArrayEnd)
tail)))
(byte-equal head (byte 93))))
(bytes-tail clean)))
(bytes-head clean))
(lambda unrestricted emptyPredecessor : Nat .
(lambda unrestricted emptyInduction : (family JSONParseResult) .
(jsonParseFailure (constructor JSONErrorCode JSONUnexpectedEnd) clean)))
(naturalIsZero (bytes-length clean))))
(jsonDropWhitespace input))))
-- Part of `jsonParseValueStep`, lifted out to keep it inside the §28.3 size and
-- nesting limits; the parameters are the locals it still needs.
def jsonParseValueStepPart1 =
(lambda unrestricted parser : (family JSONParser) .
(lambda unrestricted clean : Bytes .
(lambda unrestricted head : Byte .
(lambda unrestricted tail : Bytes .
(nat-eliminate
(lambda unrestricted array : Nat . (family JSONParseResult))
(nat-eliminate
(lambda unrestricted trueValue : Nat . (family JSONParseResult))
(nat-eliminate
(lambda unrestricted falseValue : Nat . (family JSONParseResult))
(nat-eliminate
(lambda unrestricted nullValue : Nat . (family JSONParseResult))
(nat-eliminate
(lambda unrestricted number : Nat . (family JSONParseResult))
(jsonParseFailure (constructor JSONErrorCode JSONInvalidValue) clean)
(lambda unrestricted numberPredecessor : Nat .
(lambda unrestricted numberInduction : (family JSONParseResult) .
(eliminate
JSONNumberParseResult
(lambda unrestricted current : (family JSONNumberParseResult) .
(family JSONParseResult))
(jsonParseNumber clean)
(branch
JSONNumberParsed
numberBytes
remaining
.
(constructor
JSONParseResult
JSONParsed
(constructor JSON JSONNumber numberBytes)
remaining))
(branch
JSONNumberParseFailed
code
remaining
.
(jsonParseFailure code remaining)))))
(jsonFlagOr (byte-equal head (byte 45)) (jsonByteIsDigit head)))
(lambda unrestricted nullPredecessor : Nat .
(lambda unrestricted nullInduction : (family JSONParseResult) .
(eliminate
JSONLiteralResult
(lambda unrestricted current : (family JSONLiteralResult) .
(family JSONParseResult))
(jsonConsumeLiteral b"null" clean)
(branch
JSONLiteralConsumed
remaining
.
(constructor
JSONParseResult
JSONParsed
(constructor JSON JSONNull)
remaining))
(branch
JSONLiteralFailed
remaining
.
(jsonParseFailure (constructor JSONErrorCode JSONInvalidValue) remaining)))))
(byte-equal head (byte 110)))
(lambda unrestricted falsePredecessor : Nat .
(lambda unrestricted falseInduction : (family JSONParseResult) .
(eliminate
JSONLiteralResult
(lambda unrestricted current : (family JSONLiteralResult) .
(family JSONParseResult))
(jsonConsumeLiteral b"false" clean)
(branch
JSONLiteralConsumed
remaining
.
(constructor
JSONParseResult
JSONParsed
(constructor JSON JSONBoolean zero)
remaining))
(branch
JSONLiteralFailed
remaining
.
(jsonParseFailure (constructor JSONErrorCode JSONInvalidValue) remaining)))))
(byte-equal head (byte 102)))
(lambda unrestricted truePredecessor : Nat .
(lambda unrestricted trueInduction : (family JSONParseResult) .
(eliminate
JSONLiteralResult
(lambda unrestricted current : (family JSONLiteralResult) .
(family JSONParseResult))
(jsonConsumeLiteral b"true" clean)
(branch
JSONLiteralConsumed
remaining
.
(constructor
JSONParseResult
JSONParsed
(constructor JSON JSONBoolean (succ zero))
remaining))
(branch
JSONLiteralFailed
remaining
.
(jsonParseFailure (constructor JSONErrorCode JSONInvalidValue) remaining)))))
(byte-equal head (byte 116)))
(lambda unrestricted arrayPredecessor : Nat .
(lambda unrestricted arrayInduction : (family JSONParseResult) .
(eliminate
JSONParseResult
(lambda unrestricted current : (family JSONParseResult) .
(family JSONParseResult))
(jsonParserArray parser tail)
(branch
JSONParsed
values
remaining
.
(constructor
JSONParseResult
JSONParsed
(constructor JSON JSONArray values)
remaining))
(branch JSONParseFailed code remaining . (jsonParseFailure code remaining)))))
(byte-equal head (byte 91)))))))
def jsonParseValueStep =
(lambda unrestricted parser : (family JSONParser) .
(lambda unrestricted input : Bytes .
(app
(lambda unrestricted clean : Bytes .
(nat-eliminate
(lambda unrestricted nonEmpty : Nat . (family JSONParseResult))
(app
(lambda unrestricted head : Byte .
(app
(lambda unrestricted tail : Bytes .
(nat-eliminate
(lambda unrestricted string : Nat . (family JSONParseResult))
(nat-eliminate
(lambda unrestricted object : Nat . (family JSONParseResult))
(jsonParseValueStepPart1 parser clean head tail)
(lambda unrestricted objectPredecessor : Nat .
(lambda unrestricted objectInduction : (family JSONParseResult) .
(eliminate
JSONParseResult
(lambda unrestricted current : (family JSONParseResult) .
(family JSONParseResult))
(jsonParserObject parser tail)
(branch
JSONParsed
members
remaining
.
(constructor
JSONParseResult
JSONParsed
(constructor JSON JSONObject members)
remaining))
(branch
JSONParseFailed
code
remaining
.
(jsonParseFailure code remaining)))))
(byte-equal head (byte 123)))
(lambda unrestricted stringPredecessor : Nat .
(lambda unrestricted stringInduction : (family JSONParseResult) .
(eliminate
JSONStringParseResult
(lambda unrestricted current : (family JSONStringParseResult) .
(family JSONParseResult))
(jsonParseStringBody tail)
(branch
JSONStringParsed
builder
remaining
.
(constructor
JSONParseResult
JSONParsed
(constructor JSON JSONString (bytes-builder-build builder))
remaining))
(branch
JSONStringParseFailed
code
remaining
.
(jsonParseFailure code remaining)))))
(byte-equal head (byte 34))))
(bytes-tail clean)))
(bytes-head clean))
(lambda unrestricted emptyPredecessor : Nat .
(lambda unrestricted emptyInduction : (family JSONParseResult) .
(jsonParseFailure (constructor JSONErrorCode JSONUnexpectedEnd) clean)))
(naturalIsZero (bytes-length clean))))
(jsonDropWhitespace input))))
def jsonParserWithFuel =
(lambda unrestricted fuel : Nat .
(nat-eliminate
(lambda unrestricted current : Nat . (family JSONParser))
(constructor
JSONParser
JSONParserValue
(lambda unrestricted input : Bytes .
(jsonParseFailure (constructor JSONErrorCode JSONUnexpectedEnd) input))
(lambda unrestricted input : Bytes .
(jsonParseFailure (constructor JSONErrorCode JSONUnexpectedEnd) input))
(lambda unrestricted input : Bytes .
(jsonParseFailure (constructor JSONErrorCode JSONUnexpectedEnd) input)))
(lambda unrestricted predecessor : Nat .
(lambda unrestricted induction : (family JSONParser) .
(constructor
JSONParser
JSONParserValue
(jsonParseValueStep induction)
(jsonParseObjectMembersStep induction)
(jsonParseArrayValuesStep induction))))
fuel))
def jsonParseDocumentUnchecked =
(lambda unrestricted input : Bytes .
(eliminate
UTF8DecodeResult
(lambda unrestricted current : (family UTF8DecodeResult) . (family JSONDocumentResult))
(decodeUTF8 input)
(branch
UTF8DecodeSucceeded
codepoints
.
(eliminate
JSONParseResult
(lambda unrestricted current : (family JSONParseResult) . (family JSONDocumentResult))
(jsonParserValue (jsonParserWithFuel (bytes-length input)) input)
(branch
JSONParsed
value
remaining
.
(app
(lambda unrestricted trailing : Bytes .
(nat-eliminate
(lambda unrestricted empty : Nat . (family JSONDocumentResult))
(constructor
JSONDocumentResult
JSONDocumentFailed
(constructor JSONErrorCode JSONTrailingBytes)
(naturalSaturatingSubtract (bytes-length input) (bytes-length trailing)))
(lambda unrestricted predecessor : Nat .
(lambda unrestricted induction : (family JSONDocumentResult) .
(constructor JSONDocumentResult JSONDocumentParsed value)))
(naturalIsZero (bytes-length trailing))))
(jsonDropWhitespace remaining)))
(branch
JSONParseFailed
code
remaining
.
(constructor
JSONDocumentResult
JSONDocumentFailed
code
(naturalSaturatingSubtract (bytes-length input) (bytes-length remaining))))))
(branch
UTF8DecodeFailed
code
offset
.
(constructor
JSONDocumentResult
JSONDocumentFailed
(constructor JSONErrorCode JSONInvalidUTF8)
(modelWord32ToNatural offset)))))
def jsonNaturalTwenty =
(byte-to-nat (byte 20))
def jsonNaturalTwentyFour =
(byte-to-nat (byte 24))
-- the same six limits as before -- 16 MiB of input and output, depth 256,
-- 1 MiB per string, 1024 bytes per number, 65536 entries per container -- with
-- the two megabyte-scale ones as two-power bounds, so no limit is a large Nat
def jsonDefaultLimits =
(constructor
JSONLimits
JSONLimitsValue
(constructor JSONBound JSONBoundBelowTwoPower jsonNaturalTwentyFour)
(constructor JSONBound JSONBoundAtMost byteNaturalTwoHundredFiftySix)
(constructor JSONBound JSONBoundBelowTwoPower jsonNaturalTwenty)
(constructor JSONBound JSONBoundAtMost jsonNaturalOneThousandTwentyFour)
(constructor JSONBound JSONBoundAtMost jsonNaturalSixtyFiveThousandFiveHundredThirtySix)
(constructor JSONBound JSONBoundBelowTwoPower jsonNaturalTwentyFour))
def jsonNaturalLessThanOrEqual =
(lambda unrestricted left : Nat .
(lambda unrestricted right : Nat . (jsonFlagNot (nat-less-than right left))))
-- 1 when the bound allows the value
def jsonBoundAllows =
(lambda unrestricted bound : (family JSONBound) .
(lambda unrestricted value : Nat .
(eliminate
JSONBound
(lambda unrestricted current : (family JSONBound) . Nat)
bound
(branch JSONBoundAtMost limit . (jsonNaturalLessThanOrEqual value limit))
(branch JSONBoundBelowTwoPower bits . (naturalBelowTwoPower bits value)))))
def jsonNaturalMaximum =
(lambda unrestricted left : Nat .
(lambda unrestricted right : Nat .
(nat-eliminate
(lambda unrestricted leftSmaller : Nat . Nat)
left
(lambda unrestricted predecessor : Nat . (lambda unrestricted induction : Nat . right))
(nat-less-than left right))))
def jsonCountsZero =
(constructor JSONCounts JSONCountsValue zero zero zero zero zero zero zero zero zero zero zero)
def jsonCountsObject =
(constructor
JSONCounts
JSONCountsValue
(succ zero)
(succ zero)
zero
zero
zero
zero
zero
zero
zero
zero
zero)
def jsonCountsObjectMember =
(lambda unrestricted keyBytes : Nat .
(constructor
JSONCounts
JSONCountsValue
zero
zero
(succ zero)
zero
zero
zero
zero
zero
zero
keyBytes
zero))
def jsonCountsArray =
(constructor
JSONCounts
JSONCountsValue
(succ zero)
zero
zero
(succ zero)
zero
zero
zero
zero
zero
zero
zero)
def jsonCountsArrayElement =
(constructor
JSONCounts
JSONCountsValue
zero
zero
zero
zero
(succ zero)
zero
zero
zero
zero
zero
zero)
def jsonCountsString =
(lambda unrestricted length : Nat .
(constructor
JSONCounts
JSONCountsValue
(succ zero)
zero
zero
zero
zero
(succ zero)
zero
zero
zero
length
zero))
def jsonCountsNumber =
(lambda unrestricted length : Nat .
(constructor
JSONCounts
JSONCountsValue
(succ zero)
zero
zero
zero
zero
zero
(succ zero)
zero
zero
zero
length))
def jsonCountsBoolean =
(constructor
JSONCounts
JSONCountsValue
(succ zero)
zero
zero
zero
zero
zero
zero
(succ zero)
zero
zero
zero)
def jsonCountsNull =
(constructor
JSONCounts
JSONCountsValue
(succ zero)
zero
zero
zero
zero
zero
zero
zero
(succ zero)
zero
zero)
def jsonCountsAdd =
(lambda unrestricted left : (family JSONCounts) .
(lambda unrestricted right : (family JSONCounts) .
(eliminate
JSONCounts
(lambda unrestricted current : (family JSONCounts) . (family JSONCounts))
left
(branch
JSONCountsValue
lv
lo
lm
la
le
ls
ln
lb
lz
lsb
lnb
.
(eliminate
JSONCounts
(lambda unrestricted current : (family JSONCounts) . (family JSONCounts))
right
(branch
JSONCountsValue
rv
ro
rm
ra
re
rs
rn
rb
rz
rsb
rnb
.
(constructor
JSONCounts
JSONCountsValue
(naturalAdd lv rv)
(naturalAdd lo ro)
(naturalAdd lm rm)
(naturalAdd la ra)
(naturalAdd le re)
(naturalAdd ls rs)
(naturalAdd ln rn)
(naturalAdd lb rb)
(naturalAdd lz rz)
(naturalAdd lsb rsb)
(naturalAdd lnb rnb))))))))
def jsonTreeKindIsValue =
(lambda unrestricted kind : (family JSONTreeKind) .
(eliminate
JSONTreeKind
(lambda unrestricted current : (family JSONTreeKind) . Nat)
kind
(branch JSONTreeValueKind . (succ zero))
(branch JSONTreeObjectMembersKind . zero)
(branch JSONTreeArrayValuesKind . zero)))
def jsonTreeKindIsObjectMembers =
(lambda unrestricted kind : (family JSONTreeKind) .
(eliminate
JSONTreeKind
(lambda unrestricted current : (family JSONTreeKind) . Nat)
kind
(branch JSONTreeValueKind . zero)
(branch JSONTreeObjectMembersKind . (succ zero))
(branch JSONTreeArrayValuesKind . zero)))
def jsonTreeKindIsArrayValues =
(lambda unrestricted kind : (family JSONTreeKind) .
(eliminate
JSONTreeKind
(lambda unrestricted current : (family JSONTreeKind) . Nat)
kind
(branch JSONTreeValueKind . zero)
(branch JSONTreeObjectMembersKind . zero)
(branch JSONTreeArrayValuesKind . (succ zero))))
def jsonTreeAuditFailure =
(lambda unrestricted code : (family JSONErrorCode) .
(constructor JSONTreeAuditResult JSONTreeAuditFailed code))
-- One audit condition: the result when `flag` holds, else the failure `code`.
-- The container audits chain these so that each rejected condition reports
-- its own code (a malformed tree, a duplicate key, a key past the string
-- limit, a container past the entry limit) instead of one shared code.
def jsonAuditGate =
(lambda unrestricted flag : Nat .
(lambda unrestricted code : (family JSONErrorCode) .
(lambda unrestricted otherwise : (family JSONTreeAuditResult) .
(nat-eliminate
(lambda unrestricted valid : Nat . (family JSONTreeAuditResult))
(jsonTreeAuditFailure code)
(lambda unrestricted predecessor : Nat .
(lambda unrestricted induction : (family JSONTreeAuditResult) . otherwise))
flag))))
-- Part of `jsonAuditTreeWithTokenLimits`, lifted out to keep it inside the §28.3 size and
-- nesting limits; the parameters are the locals it still needs.
def jsonAuditTreeWithTokenLimitsPart1 =
(lambda unrestricted maximumStringBytes : (family JSONBound) .
(lambda unrestricted maximumContainerEntries : (family JSONBound) .
(lambda unrestricted key : Bytes .
(lambda unrestricted tail : (family JSON) .
(lambda unrestricted memberInduction : (family JSONTreeAuditResult) .
(lambda unrestricted tailInduction : (family JSONTreeAuditResult) .
(eliminate
UTF8DecodeResult
(lambda unrestricted current : (family UTF8DecodeResult) .
(family JSONTreeAuditResult))
(decodeUTF8 key)
(branch
UTF8DecodeSucceeded
codepoints
.
(eliminate
JSONTreeAuditResult
(lambda unrestricted current : (family JSONTreeAuditResult) .
(family JSONTreeAuditResult))
memberInduction
(branch
JSONTreeAuditSucceeded
memberKind
memberCounts
memberDepth
memberSequence
.
(eliminate
JSONTreeAuditResult
(lambda unrestricted current : (family JSONTreeAuditResult) .
(family JSONTreeAuditResult))
tailInduction
(branch
JSONTreeAuditSucceeded
tailKind
tailCounts
tailDepth
tailSequence
.
(jsonAuditGate
(jsonFlagAnd
(jsonTreeKindIsValue memberKind)
(jsonTreeKindIsObjectMembers tailKind))
(constructor JSONErrorCode JSONMalformedTree)
(jsonAuditGate
(jsonFlagNot (jsonObjectContainsKey key tail))
(constructor JSONErrorCode JSONObjectDuplicateKey)
(jsonAuditGate
(jsonBoundAllows maximumStringBytes (bytes-length key))
(constructor JSONErrorCode JSONStringLimitExceeded)
(jsonAuditGate
(jsonBoundAllows maximumContainerEntries (succ tailSequence))
(constructor JSONErrorCode JSONContainerLimitExceeded)
(constructor
JSONTreeAuditResult
JSONTreeAuditSucceeded
(constructor JSONTreeKind JSONTreeObjectMembersKind)
(jsonCountsAdd
(jsonCountsObjectMember (bytes-length key))
(jsonCountsAdd memberCounts tailCounts))
(jsonNaturalMaximum memberDepth tailDepth)
(succ tailSequence)))))))
(branch JSONTreeAuditFailed code . (jsonTreeAuditFailure code))))
(branch JSONTreeAuditFailed code . (jsonTreeAuditFailure code))))
(branch
UTF8DecodeFailed
code
offset
.
(jsonTreeAuditFailure (constructor JSONErrorCode JSONInvalidUTF8))))))))))
-- Part of `jsonAuditTreeWithTokenLimits`, lifted out to keep it inside the §28.3 size and
-- nesting limits; the parameters are the locals it still needs.
def jsonAuditTreeWithTokenLimitsPart2 =
(lambda unrestricted maximumContainerEntries : (family JSONBound) .
(lambda unrestricted headInduction : (family JSONTreeAuditResult) .
(lambda unrestricted tailInduction : (family JSONTreeAuditResult) .
(eliminate
JSONTreeAuditResult
(lambda unrestricted current : (family JSONTreeAuditResult) .
(family JSONTreeAuditResult))
headInduction
(branch
JSONTreeAuditSucceeded
headKind
headCounts
headDepth
headSequence
.
(eliminate
JSONTreeAuditResult
(lambda unrestricted current : (family JSONTreeAuditResult) .
(family JSONTreeAuditResult))
tailInduction
(branch
JSONTreeAuditSucceeded
tailKind
tailCounts
tailDepth
tailSequence
.
(jsonAuditGate
(jsonFlagAnd (jsonTreeKindIsValue headKind) (jsonTreeKindIsArrayValues tailKind))
(constructor JSONErrorCode JSONMalformedTree)
(jsonAuditGate
(jsonBoundAllows maximumContainerEntries (succ tailSequence))
(constructor JSONErrorCode JSONContainerLimitExceeded)
(constructor
JSONTreeAuditResult
JSONTreeAuditSucceeded
(constructor JSONTreeKind JSONTreeArrayValuesKind)
(jsonCountsAdd jsonCountsArrayElement (jsonCountsAdd headCounts tailCounts))
(jsonNaturalMaximum headDepth tailDepth)
(succ tailSequence)))))
(branch JSONTreeAuditFailed code . (jsonTreeAuditFailure code))))
(branch JSONTreeAuditFailed code . (jsonTreeAuditFailure code))))))
-- Part of `jsonAuditTreeWithTokenLimits`, lifted out to keep it inside the §28.3 size and
-- nesting limits; the parameters are the locals it still needs.
def jsonAuditTreeWithTokenLimitsPart3 =
(lambda unrestricted number : Bytes .
(lambda unrestricted boundedPredecessor : Nat .
(lambda unrestricted boundedInduction : (family JSONTreeAuditResult) .
(eliminate
JSONNumberParseResult
(lambda unrestricted current : (family JSONNumberParseResult) .
(family JSONTreeAuditResult))
(jsonParseNumber number)
(branch
JSONNumberParsed
parsed
remaining
.
(nat-eliminate
(lambda unrestricted complete : Nat . (family JSONTreeAuditResult))
(jsonTreeAuditFailure (constructor JSONErrorCode JSONMalformedTree))
(lambda unrestricted predecessor : Nat .
(lambda unrestricted induction : (family JSONTreeAuditResult) .
(constructor
JSONTreeAuditResult
JSONTreeAuditSucceeded
(constructor JSONTreeKind JSONTreeValueKind)
(jsonCountsNumber (bytes-length number))
(succ zero)
zero)))
(naturalIsZero (bytes-length remaining))))
(branch JSONNumberParseFailed code remaining . (jsonTreeAuditFailure code))))))
def jsonAuditTreeWithTokenLimits =
(lambda unrestricted maximumStringBytes : (family JSONBound) .
(lambda unrestricted maximumNumberBytes : (family JSONBound) .
(lambda unrestricted maximumContainerEntries : (family JSONBound) .
(lambda unrestricted value : (family JSON) .
(eliminate
JSON
(lambda unrestricted current : (family JSON) . (family JSONTreeAuditResult))
value
(branch
JSONObject
members
membersInduction
.
(eliminate
JSONTreeAuditResult
(lambda unrestricted current : (family JSONTreeAuditResult) .
(family JSONTreeAuditResult))
membersInduction
(branch
JSONTreeAuditSucceeded
kind
counts
depth
sequenceCount
.
(nat-eliminate
(lambda unrestricted valid : Nat . (family JSONTreeAuditResult))
(jsonTreeAuditFailure (constructor JSONErrorCode JSONMalformedTree))
(lambda unrestricted predecessor : Nat .
(lambda unrestricted induction : (family JSONTreeAuditResult) .
(constructor
JSONTreeAuditResult
JSONTreeAuditSucceeded
(constructor JSONTreeKind JSONTreeValueKind)
(jsonCountsAdd jsonCountsObject counts)
(succ depth)
zero)))
(jsonTreeKindIsObjectMembers kind)))
(branch JSONTreeAuditFailed code . (jsonTreeAuditFailure code))))
(branch
JSONObjectEnd
.
(constructor
JSONTreeAuditResult
JSONTreeAuditSucceeded
(constructor JSONTreeKind JSONTreeObjectMembersKind)
jsonCountsZero
zero
zero))
(branch
JSONObjectMember
key
member
tail
memberInduction
tailInduction
.
(jsonAuditTreeWithTokenLimitsPart1
maximumStringBytes
maximumContainerEntries
key
tail
memberInduction
tailInduction))
(branch
JSONArray
values
valuesInduction
.
(eliminate
JSONTreeAuditResult
(lambda unrestricted current : (family JSONTreeAuditResult) .
(family JSONTreeAuditResult))
valuesInduction
(branch
JSONTreeAuditSucceeded
kind
counts
depth
sequenceCount
.
(nat-eliminate
(lambda unrestricted valid : Nat . (family JSONTreeAuditResult))
(jsonTreeAuditFailure (constructor JSONErrorCode JSONMalformedTree))
(lambda unrestricted predecessor : Nat .
(lambda unrestricted induction : (family JSONTreeAuditResult) .
(constructor
JSONTreeAuditResult
JSONTreeAuditSucceeded
(constructor JSONTreeKind JSONTreeValueKind)
(jsonCountsAdd jsonCountsArray counts)
(succ depth)
zero)))
(jsonTreeKindIsArrayValues kind)))
(branch JSONTreeAuditFailed code . (jsonTreeAuditFailure code))))
(branch
JSONArrayEnd
.
(constructor
JSONTreeAuditResult
JSONTreeAuditSucceeded
(constructor JSONTreeKind JSONTreeArrayValuesKind)
jsonCountsZero
zero
zero))
(branch
JSONArrayNext
head
tail
headInduction
tailInduction
.
(jsonAuditTreeWithTokenLimitsPart2
maximumContainerEntries
headInduction
tailInduction))
(branch
JSONString
text
.
(eliminate
UTF8DecodeResult
(lambda unrestricted current : (family UTF8DecodeResult) .
(family JSONTreeAuditResult))
(decodeUTF8 text)
(branch
UTF8DecodeSucceeded
codepoints
.
(nat-eliminate
(lambda unrestricted valid : Nat . (family JSONTreeAuditResult))
(jsonTreeAuditFailure (constructor JSONErrorCode JSONStringLimitExceeded))
(lambda unrestricted predecessor : Nat .
(lambda unrestricted induction : (family JSONTreeAuditResult) .
(constructor
JSONTreeAuditResult
JSONTreeAuditSucceeded
(constructor JSONTreeKind JSONTreeValueKind)
(jsonCountsString (bytes-length text))
(succ zero)
zero)))
(jsonBoundAllows maximumStringBytes (bytes-length text))))
(branch
UTF8DecodeFailed
code
offset
.
(jsonTreeAuditFailure (constructor JSONErrorCode JSONInvalidUTF8)))))
(branch
JSONNumber
number
.
(nat-eliminate
(lambda unrestricted bounded : Nat . (family JSONTreeAuditResult))
(jsonTreeAuditFailure (constructor JSONErrorCode JSONNumberLimitExceeded))
(jsonAuditTreeWithTokenLimitsPart3 number)
(jsonBoundAllows maximumNumberBytes (bytes-length number))))
(branch
JSONBoolean
boolean
.
(nat-eliminate
(lambda unrestricted valid : Nat . (family JSONTreeAuditResult))
(jsonTreeAuditFailure (constructor JSONErrorCode JSONMalformedTree))
(lambda unrestricted predecessor : Nat .
(lambda unrestricted induction : (family JSONTreeAuditResult) .
(constructor
JSONTreeAuditResult
JSONTreeAuditSucceeded
(constructor JSONTreeKind JSONTreeValueKind)
jsonCountsBoolean
(succ zero)
zero)))
(nat-less-than boolean jsonNaturalTwo)))
(branch
JSONNull
.
(constructor
JSONTreeAuditResult
JSONTreeAuditSucceeded
(constructor JSONTreeKind JSONTreeValueKind)
jsonCountsNull
(succ zero)
zero)))))))
def jsonEmptyParseTelemetry =
(lambda unrestricted inputBytes : Nat .
(lambda unrestricted consumedBytes : Nat .
(constructor
JSONParseTelemetry
JSONParseTelemetryValue
inputBytes
consumedBytes
(naturalSaturatingSubtract inputBytes consumedBytes)
inputBytes
zero
jsonCountsZero)))
def parseJSONObservedWithLimits =
(lambda unrestricted limits : (family JSONLimits) .
(lambda unrestricted input : Bytes .
(eliminate
JSONLimits
(lambda unrestricted current : (family JSONLimits) . (family JSONObservedDocumentResult))
limits
(branch
JSONLimitsValue
maximumInputBytes
maximumDepth
maximumStringBytes
maximumNumberBytes
maximumContainerEntries
maximumOutputBytes
.
(nat-eliminate
(lambda unrestricted inputBounded : Nat . (family JSONObservedDocumentResult))
(constructor
JSONObservedDocumentResult
JSONObservedDocumentFailed
(constructor JSONErrorCode JSONInputLimitExceeded)
zero
(jsonEmptyParseTelemetry (bytes-length input) zero))
(lambda unrestricted inputPredecessor : Nat .
(lambda unrestricted inputInduction : (family JSONObservedDocumentResult) .
(eliminate
JSONDocumentResult
(lambda unrestricted current : (family JSONDocumentResult) .
(family JSONObservedDocumentResult))
(jsonParseDocumentUnchecked input)
(branch
JSONDocumentParsed
parsed
.
(eliminate
JSONTreeAuditResult
(lambda unrestricted current : (family JSONTreeAuditResult) .
(family JSONObservedDocumentResult))
(jsonAuditTreeWithTokenLimits
maximumStringBytes
maximumNumberBytes
maximumContainerEntries
parsed)
(branch
JSONTreeAuditSucceeded
kind
counts
depth
sequenceCount
.
(nat-eliminate
(lambda unrestricted valueKind : Nat .
(family JSONObservedDocumentResult))
(constructor
JSONObservedDocumentResult
JSONObservedDocumentFailed
(constructor JSONErrorCode JSONMalformedTree)
(bytes-length input)
(constructor
JSONParseTelemetry
JSONParseTelemetryValue
(bytes-length input)
(bytes-length input)
zero
(bytes-length input)
depth
counts))
(lambda unrestricted kindPredecessor : Nat .
(lambda unrestricted kindInduction : (family JSONObservedDocumentResult) .
(nat-eliminate
(lambda unrestricted depthBounded : Nat .
(family JSONObservedDocumentResult))
(constructor
JSONObservedDocumentResult
JSONObservedDocumentFailed
(constructor JSONErrorCode JSONDepthLimitExceeded)
(bytes-length input)
(constructor
JSONParseTelemetry
JSONParseTelemetryValue
(bytes-length input)
(bytes-length input)
zero
(bytes-length input)
depth
counts))
(lambda unrestricted depthPredecessor : Nat .
(lambda unrestricted depthInduction : (family JSONObservedDocumentResult) .
(constructor
JSONObservedDocumentResult
JSONObservedDocumentParsed
parsed
(constructor
JSONParseTelemetry
JSONParseTelemetryValue
(bytes-length input)
(bytes-length input)
zero
(bytes-length input)
depth
counts))))
(jsonBoundAllows maximumDepth depth))))
(jsonTreeKindIsValue kind)))
(branch
JSONTreeAuditFailed
code
.
(constructor
JSONObservedDocumentResult
JSONObservedDocumentFailed
code
(bytes-length input)
(jsonEmptyParseTelemetry (bytes-length input) (bytes-length input))))))
(branch
JSONDocumentFailed
code
offset
.
(constructor
JSONObservedDocumentResult
JSONObservedDocumentFailed
code
offset
(jsonEmptyParseTelemetry (bytes-length input) offset))))))
(jsonBoundAllows maximumInputBytes (bytes-length input)))))))
def parseJSONWithLimits =
(lambda unrestricted limits : (family JSONLimits) .
(lambda unrestricted input : Bytes .
(eliminate
JSONObservedDocumentResult
(lambda unrestricted current : (family JSONObservedDocumentResult) .
(family JSONDocumentResult))
(parseJSONObservedWithLimits limits input)
(branch
JSONObservedDocumentParsed
value
telemetry
.
(constructor JSONDocumentResult JSONDocumentParsed value))
(branch
JSONObservedDocumentFailed
code
offset
telemetry
.
(constructor JSONDocumentResult JSONDocumentFailed code offset)))))
def parseJSON =
(lambda unrestricted input : Bytes . (parseJSONWithLimits jsonDefaultLimits input))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.