Proof Portal
jsonparser
ProbeLabs36 findings · 123 requirementsLibrary users shall traverse arrays and objects and extract multiple key paths from one payload without manually walking the JSON structure.
Specification
The requirement exactly as authored — its complete prose text and, where present, the formal FRETish sentence it compiles to.
Library users shall traverse arrays and objects and extract multiple key paths from one payload without manually walking the JSON structure.
Rationale & tags
Why this requirement exists, and how it is categorised.
Rationale & tags
Why this requirement exists, and how it is categorised.
The traversal helpers and EachKey are part of the library's value proposition for dynamic JSON inspection without struct predeclaration or hand-written walkers.
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, 17:10 UTC · human:cli
- Modified
- Jul 26, 2026, 12:54 UTC · human:cli
Obligations
What this requirement must witness to be considered satisfied — the required evidence, and the tests that discharge each one.
11 obligations · 11 discharged
Browse the catalogueIf ObjectEach/ArrayEach swallow a callback returned error and continue iterating, the next iteration invokes the callback on stale offset state, corrupting traversal and dereferencing past the buffer end.
- nominalrecommendedpresentCovered by 1 test
Output identical regardless of collection ordering or runtime conditions.
EachKey callback order on identical input must be deterministic; a regression in pathFlags match order produces callbacks in different order across calls, breaking deterministic processing.
- nominalrecommendedpresentCovered by 1 test
Behavior for unusual but valid input combinations.
ArrayEach on a single-element array must invoke the callback exactly once; a regression in the post-callback offset arithmetic invokes it twice or zero times, breaking the count contract.
- nominalrecommendedpresentCovered by 1 test
Behavior when inputs are absent, nil, zero-length, or blank.
ArrayEach on a zero-length []byte returns MalformedObjectError via the early guard; if the guard regresses nextToken returns -1 and the follow-on data[offset] dereference panics on the empty slice.
- nominalrecommendedpresentCovered by 2 tests
Behavior when inputs are syntactically or structurally invalid.
ArrayEach on adversarial JSON like [1,2,,] drives Get to a parse error mid-array; if the error-propagation guard regresses the loop continues past the malformed token and dereferences data[offset] past len(data).
- negativerequiredpresent
- nominalrecommendedpresent
Behavior specified when inputs are nil, null, or zero-value.
ObjectEach(nil,...) flows through searchKeys nil-slice loop; the subsequent nextToken/data[offset] dereference panics with nil-slice index-out-of-range.
- negativerequiredpresentCovered by 2 tests
- nominalrecommendedpresentCovered by 1 test
Happy-path behavior with valid inputs.
- nominalrecommendedpresent
When searchKeys or blockEnd returns -1 sentinel for malformed structure, ArrayEach/EachKey dereference data[offset] without re-checking offset>=0 (the OSS-Fuzz Delete panic class).
- nominalrecommendedpresentCovered by 1 test
Truncated JSON like [1,2 with no closing bracket drives nextToken in ArrayEach to -1; the follow-on data[offset] dereference panics with index-out-of-range on the truncated remainder.
- nominalrecommendedpresentCovered by 1 test
Truncated JSON like [1,"abc with no closing string mid-element drives Get to stringEnd returning -1; the follow-on data[offset] dereference in ArrayEach panics past the buffer end.
- nominalrecommendedpresentCovered by 1 test
Truncated JSON like {"a":[1,2 with no matching close bracket drives blockEnd to -1; if the guard regresses the unbounded loop dereferences past the buffer end, crashing the process.
- 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 iterate an addressed JSON array in encounter order, receive no callbacks for a well-formed empty addressed array, and receive an error for malformed or otherwise unusable array input.
- AC-2verify: test
A caller can iterate an addressed JSON object and receive the correct key, value, and value type tuples for well-formed entries, no entries for well-formed empty objects, propagated callback errors, and an error for malformed or otherwise unusable object input.
Derived requirements - AC-3verify: test
A caller can request multiple key paths from one payload scan and receive the correct found or missing-path behavior for each requested path.
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 (22)
- When ArrayEach addresses a well-formed non-empty JSON…parser · SYS
- When ObjectEach addresses a well-formed non-empty JSON…parser · SYS
- When EachKey is called with one or more requested key…parser · SYS
- When ArrayEach addresses a well-formed empty JSON array,…parser · SYS
- When ArrayEach receives malformed or otherwise unusable…parser · SYS
- When ObjectEach addresses a well-formed empty JSON object,…parser · SYS
- When ObjectEach receives malformed or otherwise unusable…parser · SYS
- When ObjectEach addresses a well-formed object and the…parser · SYS
- When ArrayEach iterates a well-formed array and the Get…parser · SYS
- When ArrayEach encounters an array element that is…parser · SYS
- When ObjectEach encounters an object entry that is…parser · SYS
- When ArrayEach encounters a malformed delimiter between…parser · SYS
- When ArrayEach is called on input truncated at a value…parser · SYS
- When ObjectEach is called on input truncated mid-structure…parser · SYS
- When EachKey encounters a tokenEnd sentinel value…parser · SYS
- When ArrayEach, ObjectEach, or EachKey is called twice with…parser · SYS
- When ArrayEach, ObjectEach, or EachKey is called with a nil…parser · SYS
- When ArrayEach or ObjectEach is called on JSON with deeply…parser · SYS
- GetArrayLen returns the number of elements in the addressed…parser · SYS
- EachKeyWildcard, ArrayEachWildcard, and SetWildcard accept…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 (7)
- aliases.goaliases.go
- parser.goparser.go
- fuzz.gofuzz.go
- wildcard.gowildcard.go
- config.goconfig.go
- escape.goescape.go
- reader_parser.goreader_parser.go
Tests to re-run (26)
- 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
- obligation_evidence_test.goobligation_evidence_test.go
- parser_test.goparser_test.go
- aliases_test.goaliases_test.go
- dead_code_audit_oob_test.godead_code_audit_oob_test.go
- dead_code_audit_test.godead_code_audit_test.go
- mcdc_spec_witnesses_test.gomcdc_spec_witnesses_test.go
- mcdc_supplement_test.gomcdc_supplement_test.go
- property_test.goproperty_test.go
- coverage_closure_test.gocoverage_closure_test.go
- fuzz_native_test.gofuzz_native_test.go
- path_fuzz_test.gopath_fuzz_test.go
- array_each_err_test.goarray_each_err_test.go
- empty_key_path_test.goempty_key_path_test.go
- issues_56_107_229_test.goissues_56_107_229_test.go
- parser_error_test.goparser_error_test.go
- v131_regression_test.gov131_regression_test.go
- deep_spec_test.godeep_spec_test.go
- obligation_property_test.goobligation_property_test.go
- len_uint_test.golen_uint_test.go
- wildcard_test.gowildcard_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.