2268def jsonAuditTreeWithTokenLimits =
2269 (lambda unrestricted maximumStringBytes : (family JSONBound) .
2270 (lambda unrestricted maximumNumberBytes : (family JSONBound) .
2271 (lambda unrestricted maximumContainerEntries : (family JSONBound) .
2272 (lambda unrestricted value : (family JSON) .
2273 (eliminate
2274 JSON
2275 (lambda unrestricted current : (family JSON) . (family JSONTreeAuditResult))
2276 value
2277 (branch
2278 JSONObject
2279 members
2280 membersInduction
2281 .
2282 (eliminate
2283 JSONTreeAuditResult
2284 (lambda unrestricted current : (family JSONTreeAuditResult) .
2285 (family JSONTreeAuditResult))
2286 membersInduction
2287 (branch
2288 JSONTreeAuditSucceeded
2289 kind
2290 counts
2291 depth
2292 sequenceCount
2293 .
2294 (nat-eliminate
2295 (lambda unrestricted valid : Nat . (family JSONTreeAuditResult))
2296 (jsonTreeAuditFailure (constructor JSONErrorCode JSONMalformedTree))
2297 (lambda unrestricted predecessor : Nat .
2298 (lambda unrestricted induction : (family JSONTreeAuditResult) .
2299 (constructor
2300 JSONTreeAuditResult
2301 JSONTreeAuditSucceeded
2302 (constructor JSONTreeKind JSONTreeValueKind)
2303 (jsonCountsAdd jsonCountsObject counts)
2304 (succ depth)
2305 zero)))
2306 (jsonTreeKindIsObjectMembers kind)))
2307 (branch JSONTreeAuditFailed code . (jsonTreeAuditFailure code))))
2308 (branch
2309 JSONObjectEnd
2310 .
2311 (constructor
2312 JSONTreeAuditResult
2313 JSONTreeAuditSucceeded
2314 (constructor JSONTreeKind JSONTreeObjectMembersKind)
2315 jsonCountsZero
2316 zero
2317 zero))
2318 (branch
2319 JSONObjectMember
2320 key
2321 member
2322 tail
2323 memberInduction
2324 tailInduction
2325 .
2326 (jsonAuditTreeWithTokenLimitsPart1
2327 maximumStringBytes
2328 maximumContainerEntries
2329 key
2330 tail
2331 memberInduction
2332 tailInduction))
2333 (branch
2334 JSONArray
2335 values
2336 valuesInduction
2337 .
2338 (eliminate
2339 JSONTreeAuditResult
2340 (lambda unrestricted current : (family JSONTreeAuditResult) .
2341 (family JSONTreeAuditResult))
2342 valuesInduction
2343 (branch
2344 JSONTreeAuditSucceeded
2345 kind
2346 counts
2347 depth
2348 sequenceCount
2349 .
2350 (nat-eliminate
2351 (lambda unrestricted valid : Nat . (family JSONTreeAuditResult))
2352 (jsonTreeAuditFailure (constructor JSONErrorCode JSONMalformedTree))
2353 (lambda unrestricted predecessor : Nat .
2354 (lambda unrestricted induction : (family JSONTreeAuditResult) .
2355 (constructor
2356 JSONTreeAuditResult
2357 JSONTreeAuditSucceeded
2358 (constructor JSONTreeKind JSONTreeValueKind)
2359 (jsonCountsAdd jsonCountsArray counts)
2360 (succ depth)
2361 zero)))
2362 (jsonTreeKindIsArrayValues kind)))
2363 (branch JSONTreeAuditFailed code . (jsonTreeAuditFailure code))))
2364 (branch
2365 JSONArrayEnd
2366 .
2367 (constructor
2368 JSONTreeAuditResult
2369 JSONTreeAuditSucceeded
2370 (constructor JSONTreeKind JSONTreeArrayValuesKind)
2371 jsonCountsZero
2372 zero
2373 zero))
2374 (branch
2375 JSONArrayNext
2376 head
2377 tail
2378 headInduction
2379 tailInduction
2380 .
2381 (jsonAuditTreeWithTokenLimitsPart2
2382 maximumContainerEntries
2383 headInduction
2384 tailInduction))
2385 (branch
2386 JSONString
2387 text
2388 .
2389 (eliminate
2390 UTF8DecodeResult
2391 (lambda unrestricted current : (family UTF8DecodeResult) .
2392 (family JSONTreeAuditResult))
2393 (decodeUTF8 text)
2394 (branch
2395 UTF8DecodeSucceeded
2396 codepoints
2397 .
2398 (nat-eliminate
2399 (lambda unrestricted valid : Nat . (family JSONTreeAuditResult))
2400 (jsonTreeAuditFailure (constructor JSONErrorCode JSONStringLimitExceeded))
2401 (lambda unrestricted predecessor : Nat .
2402 (lambda unrestricted induction : (family JSONTreeAuditResult) .
2403 (constructor
2404 JSONTreeAuditResult
2405 JSONTreeAuditSucceeded
2406 (constructor JSONTreeKind JSONTreeValueKind)
2407 (jsonCountsString (bytes-length text))
2408 (succ zero)
2409 zero)))
2410 (jsonBoundAllows maximumStringBytes (bytes-length text))))
2411 (branch
2412 UTF8DecodeFailed
2413 code
2414 offset
2415 .
2416 (jsonTreeAuditFailure (constructor JSONErrorCode JSONInvalidUTF8)))))
2417 (branch
2418 JSONNumber
2419 number
2420 .
2421 (nat-eliminate
2422 (lambda unrestricted bounded : Nat . (family JSONTreeAuditResult))
2423 (jsonTreeAuditFailure (constructor JSONErrorCode JSONNumberLimitExceeded))
2424 (jsonAuditTreeWithTokenLimitsPart3 number)
2425 (jsonBoundAllows maximumNumberBytes (bytes-length number))))
2426 (branch
2427 JSONBoolean
2428 boolean
2429 .
2430 (nat-eliminate
2431 (lambda unrestricted valid : Nat . (family JSONTreeAuditResult))
2432 (jsonTreeAuditFailure (constructor JSONErrorCode JSONMalformedTree))
2433 (lambda unrestricted predecessor : Nat .
2434 (lambda unrestricted induction : (family JSONTreeAuditResult) .
2435 (constructor
2436 JSONTreeAuditResult
2437 JSONTreeAuditSucceeded
2438 (constructor JSONTreeKind JSONTreeValueKind)
2439 jsonCountsBoolean
2440 (succ zero)
2441 zero)))
2442 (nat-less-than boolean jsonNaturalTwo)))
2443 (branch
2444 JSONNull
2445 .
2446 (constructor
2447 JSONTreeAuditResult
2448 JSONTreeAuditSucceeded
2449 (constructor JSONTreeKind JSONTreeValueKind)
2450 jsonCountsNull
2451 (succ zero)
2452 zero)))))))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.