Proof Portal
jsonparser
ProbeLabs23 findings · 123 requirementsThe fastest JSON parser for Go — formally verified with ReqProof (real library, master).
Changes & defects
The chronological log of the proof layer — semantic changes (intended units of work) interleaved with the defects found and fixed, newest first.
- 7 days agoKnown issueMediumFixedKI-4Set on top-level array-index beyond length returns KeyPathNotFoundError instead of appending
Set fails for a common use case (appending to a top-level JSON array); callers must wrap the array in an object.
Buger1 requirement - 3 weeks agoChangeFeatureDraftCHG-260729-YBAEv1.6.0: Append function + KI-2/3/4 fixes
New Append API for clean array append.
- 4 weeks agoRequirementsadded
5 requirements added
GetArrayLen returns the number of elements in the addressed JSON array (0 for an empty array), and GetObjectLen returns the number of key-value pairs in the addressed JSON object (0 for an empty object).SYS-REQ-112EachKeyWildcard, ArrayEachWildcard, and SetWildcard accept [*] as a wildcard array-index component that fans out over every element of the addressed array.SYS-REQ-113ParsePath converts a JSONPath-style string (root $.SYS-REQ-114When a Config with AllowSingleQuotes=true is provided, the parser shall accept single-quoted strings (delimited by ' instead of ") using the same escape rules as double-quoted strings.SYS-REQ-115A ReaderParser shall provide path-based access to JSON data from an io.Reader stream, supporting Get, GetString, and ArrayEach without requiring the entire document to be loaded into memory.SYS-REQ-116 - 4 weeks agoRequirementsupdated
7 requirements updated
When ArrayEach addresses a well-formed non-empty JSON array, the parser shall invoke the callback for each addressed array element in encounter order.SYS-REQ-006When Set is called with a provided path, the parser shall either replace the existing addressed value, create a type-consistent missing path and return the updated JSON document, or return KeyPathNotFoundError when the requested mutation path is not usable for the provided input.SYS-REQ-009When ParseString receives a well-formed raw JSON string literal body, the parser shall return the corresponding decoded Go string value.SYS-REQ-014When ArrayEach receives malformed or otherwise unusable addressed array input, the parser shall return an error.SYS-REQ-029When ParseString encounters a UTF-16 high surrogate escape (e.g., '\uD800') that is not followed by a valid low surrogate escape, the parser shall substitute U+FFFD (replacement character) for the lone surrogate and continue parsing, matching encoding/json behavior, rather than producing corrupted output or synthesizing a bogus code point.SYS-REQ-061When ParseString encounters a UTF-16 high surrogate escape followed by a second unicode escape whose value is below the low surrogate range (e.g., '\uD800\u0041'), the parser shall substitute U+FFFD (replacement character) for the malformed surrogate sequence and continue parsing, matching encoding/json behavior, rather than producing corrupted output or returning an error.SYS-REQ-062 - 4 weeks agoDefects22
4 defects
MediumArrayEach on non-array root emitted spurious callback before erroringFixedDEFECT-260727-ARR1HighUnescape lone-Unicode-surrogate mishandling synthesizes bogus non-BMP charsFixedDEFECT-260727-SNGTMediumSet on top-level array-index beyond length returns KeyPathNotFoundError (SYS-REQ-110 contract gap)FixedDEFECT-260727-T7P7HighSet beyond-length array index on scalar array destroys all elements (SYS-REQ-110 violation)FixedDEFECT-260727-WWWY - 4 weeks agoRequirementsupdated
86 requirements updated
Library users shall retrieve values from JSON byte payloads by specifying a key path without predeclaring Go structs.STK-REQ-001Library users shall retrieve string values with JSON escapes and Unicode decoded into Go strings.STK-REQ-002Library users shall extract known numeric and boolean JSON values through typed helpers without manual byte parsing or ad-hoc conversions.STK-REQ-003Library users shall traverse arrays and objects and extract multiple key paths from one payload without manually walking the JSON structure.STK-REQ-004Library users shall update or delete addressed JSON values in byte payloads through the experimental mutation helpers with deterministic edge-case behavior.STK-REQ-005Library users shall retrieve addressed JSON values as zero-allocation raw strings without JSON unescaping when they intentionally choose the unsafe helper.STK-REQ-006 - 4 weeks agoRequirementsadded
2 requirements added
When Set targets an array-index path component [N] where N >= the current length of the addressed array, the parser shall append the value at the end of the array (index becomes len(array)) and return the mutated document, rather than overwriting existing elements or panicking.SYS-REQ-110When any key path component is the empty string, the parser shall treat the path as unresolvable and return KeyPathNotFoundError (Get family / Delete) or a defined error (Set), and shall never panic.SYS-REQ-111 - 4 weeks agoDefects31
4 defects
LowParseInt("-") returns (0, nil) — silent false-success on sign-only inputFixedDEFECT-260726-3F95HighDelete left dangling trailing comma on array/object element followed by whitespace+commaFixedDEFECT-260726-3PSJHighSet with array-index path component under an object parent produces malformed JSON output (silent corruption)FixedDEFECT-260726-MFPAHighEmpty-string key path component panics (hazard-sweep finding)FixedDEFECT-260726-QS2V - 4 weeks agoKnown issueHighFixedKI-3Set with array-index path component under an object parent produces malformed JSON output
When Set is called with a key path that contains an array-index component ([N]) whose parent in the addressed JSON is an OBJECT rather than an array, the implementation emits malformed JSON output and returns it with a nil error.
Buger3 requirements - 4 months agoRequirementsadded
24 requirements added
When Get is called twice with identical JSON input and identical key paths, the parser shall return identical value slices, value types, offsets, and error values on both calls.SYS-REQ-086When Get is called on a JSON byte slice, the parser shall not mutate the input slice -- the input bytes before and after the call shall be identical.SYS-REQ-087When Get is called with a nil byte slice as input, the parser shall return a not-found or error result without panicking.SYS-REQ-088When Get is called on JSON input with deeply nested structures (e.g., 64+ levels of nesting), the parser shall either return the correct result or a parse error, without panicking or stack-overflowing.SYS-REQ-089When GetString is called twice with identical JSON input and identical key paths, the parser shall return identical decoded string values and identical error values on both calls.SYS-REQ-090When GetString is called with a nil byte slice as input, the parser shall return an empty string and an error or not-found result without panicking.SYS-REQ-091 - 4 months agoRequirementsadded
70 requirements added
When the JSON input is well formed, a key path is provided, and the addressed path does not exist, the parser shall return the defined not-found result with `NotExist`, offset `-1`, and `KeyPathNotFoundError`.SYS-REQ-016When the JSON input is incomplete or truncated before addressed lookup or no-key-path extraction can complete, including incomplete addressed strings, arrays, objects, or missing value tokens, the parser shall return a parse-related error and shall not report a successful lookup result.SYS-REQ-017When the JSON input is well formed and no key path is provided, the parser shall return the closest complete root JSON value according to the API contract, including complete object, array, string, number, boolean, or null values.SYS-REQ-018When the input is empty and a key path is provided, the parser shall return the defined not-found result with `NotExist`, offset `-1`, and `KeyPathNotFoundError`.SYS-REQ-019When the current path segment is an object key and it is evaluated at the current JSON structural scope, Get shall resolve that segment only against object members in that current scope.SYS-REQ-020When the current path segment is a valid in-bounds array index, Get shall resolve the addressed array element and return it through the normal successful lookup contract.SYS-REQ-021 - 4 months agoRequirementsupdated
2 requirements updated
When ObjectEach addresses a well-formed non-empty JSON object, the parser shall invoke the callback with the correct key, value, and value type tuple for each addressed object entry.SYS-REQ-007When ParseFloat receives a well-formed floating-point number token, the parser shall return the corresponding float64 value.SYS-REQ-013 - 4 months agoRequirementsadded
22 requirements added
Library users shall retrieve values from JSON byte payloads by specifying a key path without predeclaring Go structs.STK-REQ-001Library users shall retrieve string values with JSON escapes and Unicode decoded into Go strings.STK-REQ-002Library users shall extract known numeric and boolean JSON values through typed helpers without manual byte parsing or ad-hoc conversions.STK-REQ-003Library users shall traverse arrays and objects and extract multiple key paths from one payload without manually walking the JSON structure.STK-REQ-004Library users shall update or delete addressed JSON values in byte payloads through the experimental mutation helpers with deterministic edge-case behavior.STK-REQ-005Library users shall retrieve addressed JSON values as zero-allocation raw strings without JSON unescaping when they intentionally choose the unsafe helper.STK-REQ-006 - UndatedKnown issueLowFixedKI-2ParseInt("-") returns (0, nil) — silent false-success on sign-only input
parseInt (bytes.go:9) strips a leading sign byte and then iterates over the remainder.
Buger4 requirements
End of timeline