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))