Proof Portal
jsonparser
ProbeLabs36 findings · 123 requirementsLibrary users shall retrieve values from JSON byte payloads by specifying a key path without predeclaring Go structs.
Specification
The requirement exactly as authored — its complete prose text and, where present, the formal FRETish sentence it compiles to.
Library users shall retrieve values from JSON byte payloads by specifying a key path without predeclaring Go structs.
Rationale & tags
Why this requirement exists, and how it is categorised.
Rationale & tags
Why this requirement exists, and how it is categorised.
This is the core value proposition described in the project README and the primary reason to adopt jsonparser over encoding/json for dynamic payloads.
Verification & provenance
How this requirement was checked: the review trail, edit history, and the machine-analysis status terms (each ⓘ explains what it means).
Review
- Status
- approved
- Reviewer
- human:leonidbugaev
- Reviewed
- Apr 23, 2026, 00:00 UTC
History
- Created
- Apr 13, 2026, 16:22 UTC · human:cli
- Modified
- Jul 26, 2026, 12:53 UTC · human:cli
Obligations
What this requirement must witness to be considered satisfied — the required evidence, and the tests that discharge each one.
15 obligations · 15 discharged
Browse the catalogueBehavior at limits, thresholds, and edge-of-range values.
Value at exactly len(data) makes tokenEnd return len(data); an omitted bounds check slices data[offset:endOffset] past the buffer end and panics with index-out-of-range.
- negativerecommendedpresentCovered by 1 test
- nominalrecommendedpresentCovered by 4 tests
Output identical regardless of collection ordering or runtime conditions.
lastMatched state in searchKeys leaks across sibling object keys, so two Get calls on identical []byte can resolve to different value slices for the same path.
- nominalrecommendedpresentCovered by 1 test
Behavior for unusual but valid input combinations.
Get on a bare scalar payload ("null"/"true") with no key path regresses the no-keys fast path to return an empty slice or wrong ValueType instead of the scalar bytes.
- nominalrecommendedpresentCovered by 1 test
Behavior when inputs are absent, nil, zero-length, or blank.
Get on a zero-length []byte drives internalGet nextToken to -1; the subsequent data[offset] dereference in getType panics with index-out-of-range on the empty slice.
- nominalrecommendedpresentCovered by 2 tests
Applying the operation twice produces the same result as applying once.
Returned value slice aliases the input buffer via value[:len(value):len(value)]; a caller mutating the buffer between calls sees the prior Get result silently change.
- nominalrecommendedpresentCovered by 1 test
Behavior when inputs are syntactically or structurally invalid.
Adversarial JSON like {"a":,} drives searchKeys data[i] dereference on a delimiter with no following value, replicating the OSS-Fuzz Delete panic class on Get.
- negativerequiredpresentCovered by 3 tests
- nominalrecommendedpresent
A stale valueFound from a prior sibling match in the same call leaves Get returning a wrong-key byte slice instead of KeyPathNotFoundError, silently corrupting downstream decoding.
- nominalrecommendedpresentCovered by 1 test
Path [-1] parses to aIdx=-1 via strconv.Atoi with no sign check; the curIdx match never fires and stale valueOffset arithmetic can panic on stale-offset dereference.
- nominalrecommendedpresentCovered by 1 test
Behavior specified when inputs are nil, null, or zero-value.
Get(nil) flows into searchKeys; nextToken on the nil slice returns -1 and getType(nil,0) data[offset] dereference panics with nil-slice index-out-of-range.
- negativerequiredpresentCovered by 3 tests
- nominalrecommendedpresentCovered by 2 tests
Happy-path behavior with valid inputs.
- nominalrecommendedpresent
When searchKeys/blockEnd/nextToken return the -1 sentinel for not-found, internalGet/ArrayEach dereference data[offset] without re-checking offset>=0 (the OSS-Fuzz Delete panic class).
- nominalrecommendedpresentCovered by 1 test
Payload like {"a": with no value drives nextToken to -1 on the remainder; the subsequent data[offset] dereference in getType panics with index-out-of-range.
- nominalrecommendedpresentCovered by 1 test
Payload like {"key with no closing quote drives stringEnd to -1; if the break guard regresses, searchKeys continues and dereferences data[i] past len(data), crashing the process.
- nominalrecommendedpresentCovered by 1 test
Payload like {"a":[1,2 with no matching close bracket drives blockEnd to -1; if the return-check regresses the unbounded loop dereferences past the buffer end, crashing the parser.
- nominalrecommendedpresentCovered by 1 test
Get on a JSON String where the caller expected Number returns quoted bytes; strconv.ParseInt on the quoted token silently returns 0 instead of an explicit type error.
- nominalrecommendedpresentCovered by 1 test
Acceptance criteria
Stakeholder conditions for satisfaction, traced to the derived requirements and evidence that discharge them.
Acceptance criteria
Stakeholder conditions for satisfaction, traced to the derived requirements and evidence that discharge them.
Stakeholder-authored conditions defining when the requirement is satisfied, traced to derived requirements / evidence.
- AC-1verify: test
A caller can request a nested value by path from a JSON byte slice and receive the correct value, not-found result, or parsing error for the addressed input case.
Derived requirements
Its place
This requirement shown inside its trace neighbourhood — the parents it satisfies, the code and tests attached to it, and its findings.
Loading graph…
Trace evidence
The concrete artifacts linked to this requirement — implementing code, verifying tests, documents, and the findings raised against it.
No implementation linked
No source files are traced to this requirement yet.
Impact
Blast radius — if you change this requirement, what else may need re-checking, and what it in turn depends on.
Impact
Blast radius — if you change this requirement, what else may need re-checking, and what it in turn depends on.
If you change this
Requirements (27)
- When the JSON input is well formed, a key path is provided,…parser · SYS
- When the JSON input is well formed, a key path is provided,…parser · SYS
- When the JSON input is incomplete or truncated before…parser · SYS
- When the JSON input is well formed and no key path is…parser · SYS
- When the input is empty and a key path is provided, the…parser · SYS
- When the current path segment is an object key and it is…parser · SYS
- When the current path segment is a valid in-bounds array…parser · SYS
- When the current path segment is intended as an array index…parser · SYS
- When the current path segment is a valid array index but…parser · SYS
- When a JSON object member key is escaped in the payload and…parser · SYS
- When the addressed value is a JSON string, Get shall return…parser · SYS
- When the input is malformed outside the addressed token…parser · SYS
- When the addressed token cannot be classified as string,…parser · SYS
- When the JSON input is truncated at a value boundary (eparser · SYS
- When the JSON input is truncated in the middle of a…parser · SYS
- When the JSON input is truncated in the middle of a key…parser · SYS
- When internal helper tokenEnd returns len(data) as a…parser · SYS
- When internal helper stringEnd returns -1 indicating no…parser · SYS
- When internal helper blockEnd returns -1 indicating no…parser · SYS
- When the current path segment is a negative array index (eparser · SYS
- When Get is called twice with identical JSON input and…parser · SYS
- When Get is called on a JSON byte slice, the parser shall…parser · SYS
- When Get is called with a nil byte slice as input, the…parser · SYS
- When Get is called on JSON input with deeply nested…parser · SYS
- ParsePath converts a JSONPath-style string (root $parser · SYS
- When a Config with AllowSingleQuotes=true is provided, the…parser · SYS
- A ReaderParser shall provide path-based access to JSON data…parser · SYS
Files to re-check (6)
- fuzz.gofuzz.go
- parser.goparser.go
- path_compiler.gopath_compiler.go
- config.goconfig.go
- escape.goescape.go
- reader_parser.goreader_parser.go
Tests to re-run (24)
- benchmark_large_payload_test.gobenchmark/benchmark_large_payload_test.go
- benchmark_medium_payload_test.gobenchmark/benchmark_medium_payload_test.go
- benchmark_small_payload_test.gobenchmark/benchmark_small_payload_test.go
- encoding_json_regression_test.gobenchmark/encoding_json_regression_test.go
- mcdc_supplement_test.gomcdc_supplement_test.go
- obligation_evidence_test.goobligation_evidence_test.go
- parser_test.goparser_test.go
- bytes_unsafe_test.gobytes_unsafe_test.go
- dead_code_audit_test.godead_code_audit_test.go
- fuzz_native_test.gofuzz_native_test.go
- mcdc_code_supplement_test.gomcdc_code_supplement_test.go
- mcdc_spec_witnesses_test.gomcdc_spec_witnesses_test.go
- parser_error_test.goparser_error_test.go
- path_compiler_test.gopath_compiler_test.go
- property_test.goproperty_test.go
- reference_oracle_test.goreference_oracle_test.go
- deep_spec_test.godeep_spec_test.go
- empty_key_path_test.goempty_key_path_test.go
- sys_req_110_111_witness_test.gosys_req_110_111_witness_test.go
- optimization_equiv_test.gooptimization_equiv_test.go
- obligation_property_test.goobligation_property_test.go
- config_test.goconfig_test.go
- v150_mcdc_witness_test.gov150_mcdc_witness_test.go
- reader_parser_test.goreader_parser_test.go
What this rests on
Discussions
Discuss this with the proof team. Nothing changes in your audit automatically — you open a request and a staff member records any outcome inside the thread.