Proof Portal
jsonparser
ProbeLabs36 findings · 123 requirementsLibrary users shall update or delete addressed JSON values in byte payloads through the experimental mutation helpers with deterministic edge-case behavior.
Specification
The requirement exactly as authored — its complete prose text and, where present, the formal FRETish sentence it compiles to.
Library users shall update or delete addressed JSON values in byte payloads through the experimental mutation helpers with deterministic edge-case behavior.
Rationale & tags
Why this requirement exists, and how it is categorised.
Rationale & tags
Why this requirement exists, and how it is categorised.
Set and Delete are documented experimental APIs, so their mutation and malformed-input behavior still needs explicit contract coverage.
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:15 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.
13 obligations · 13 discharged
Browse the catalogueBehavior for unusual but valid input combinations.
Set on a payload where the target path parent is an empty object must insert with comma=false; a regression inserts a leading comma, producing invalid JSON output downstream.
- nominalrecommendedpresentCovered by 1 test
Behavior when inputs are absent, nil, zero-length, or blank.
Set on a zero-length []byte drives internalGet to nextToken=-1; if the empty-input guard regresses the follow-on data[firstToken] dereference panics on the empty slice.
- nominalrecommendedpresentCovered by 1 test
Set internalGet returns an error on malformed input; if the error check regresses Set continues with stale startOffset/endOffset=-1 and slices data[:-1] or panics on the negative offset.
- nominalrecommendedpresentCovered by 1 test
Applying the operation twice produces the same result as applying once.
Delete applied twice to the same path must produce the same output as Delete once; a regression in the trailing-comma cleanup leaves a stray comma on the second call, corrupting the mutated payload.
- nominalrecommendedpresentCovered by 1 test
Behavior when inputs are syntactically or structurally invalid.
Delete on adversarial JSON like {"a":,} drives findKeyStart/tokenEnd to stale offsets; if guards regress the data[endOffset+tokEnd] dereference panics (OSS-Fuzz 4649128545288192 class).
- negativerequiredpresentCovered by 4 tests
- nominalrecommendedpresent
Delete for a non-existent key must return the original payload unchanged; a regression in findKeyStart KeyPathNotFoundError handling leaves Delete mutating an arbitrary sibling position.
- nominalrecommendedpresentCovered by 3 tests
Set on a deeply nested path (a.b.c.d) drives createInsertComponent to emit nested object scaffolding; a regression in calcAllocateSpace under-allocates the buffer and WriteToBuffer writes past the end.
- nominalrecommendedpresentCovered by 3 tests
Behavior specified when inputs are nil, null, or zero-value.
Delete(nil,...) drives internalGet to searchKeys nil-slice loop; the follow-on tokenEnd/findTokenStart/data[prevTok] dereference panics on the nil slice.
- negativerequiredpresentCovered by 4 tests
- nominalrecommendedpresentCovered by 3 tests
Set/Delete with zero keys must return early; if the early-return guard regresses the next data[keys[lk-1][0]] dereference panics on the empty keys slice with index-out-of-range.
- nominalrecommendedpresentCovered by 3 tests
Happy-path behavior with valid inputs.
- nominalrecommendedpresent
When internalGet/searchKeys return -1 sentinel for not-found, Delete tokenEnd/findTokenStart arithmetic dereferences data[endOffset+tokEnd] without bounds re-check (the OSS-Fuzz 4649128545288192 panic class).
- nominalrecommendedpresentCovered by 1 test
Delete on payload like {"a": with no value drives internalGet to error; if the error guard regresses Delete continues with stale offsets and the data[endOffset+tokEnd] dereference panics on the truncated slice.
- nominalrecommendedpresentCovered by 1 test
Delete on payload like {"a":[1,2 with no closing bracket drives blockEnd to -1; if the guard regresses the unguarded data[endOffset+tokEnd] dereference panics past the buffer end.
- 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 update an existing addressed JSON value or create a supported missing addressed value through Set and receive the expected mutated payload, or a defined error when the requested mutation path is unusable.
- AC-2verify: test
A caller can delete an addressed JSON value through Delete and receive either the expected mutated payload, the unchanged original payload for a missing addressed target in otherwise usable input, or the unchanged original payload for malformed, truncated, or otherwise unusable input, without process crash or panic.
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 (20)
- When Set is called with a provided path, the parser shall…parser · SYS
- When Delete is called without a path, the parser shall…parser · SYS
- When Delete is called with a provided path and the…parser · SYS
- When Delete is called with a provided path, the addressed…parser · SYS
- When Delete is called with a provided path but the input is…parser · SYS
- When internal helper tokenEnd returns len(data) as a…parser · SYS
- When Delete is called on input that is truncated at a value…parser · SYS
- When Delete calls internalGet and internalGet returns an…parser · SYS
- When Delete is called with an array-element path on input…parser · SYS
- When Set is called on truncated JSON input where the path…parser · SYS
- When Delete is called on input that is truncated…parser · SYS
- When Set is called with a path that resolves to a location…parser · SYS
- When Set is called with a multi-level path where…parser · SYS
- When Set is called without any key path, the parser shall…parser · SYS
- When Set is called twice on the same input with the same…parser · SYS
- When Set or Delete is called with a nil byte slice as…parser · SYS
- When Set or Delete is called with key paths containing…parser · SYS
- When Set targets an array-index path component [N] where N…parser · SYS
- When any key path component is the empty string, the parser…parser · SYS
- When a Config with AllowSingleQuotes=true is provided, the…parser · SYS
Files to re-check (6)
- append.goappend.go
- escape.goescape.go
- fuzz.gofuzz.go
- parser.goparser.go
- path_compiler.gopath_compiler.go
- config.goconfig.go
Tests to re-run (29)
- benchmark_delete_test.gobenchmark/benchmark_delete_test.go
- benchmark_medium_payload_test.gobenchmark/benchmark_medium_payload_test.go
- benchmark_set_test.gobenchmark/benchmark_set_test.go
- benchmark_small_payload_test.gobenchmark/benchmark_small_payload_test.go
- mcdc_supplement_test.gomcdc_supplement_test.go
- obligation_evidence_test.goobligation_evidence_test.go
- parser_test.goparser_test.go
- set_spec_test.goset_spec_test.go
- sys_req_110_111_witness_test.gosys_req_110_111_witness_test.go
- empty_key_path_test.goempty_key_path_test.go
- escape_test.goescape_test.go
- fuzz_native_test.gofuzz_native_test.go
- issues_56_107_229_test.goissues_56_107_229_test.go
- mcdc_code_supplement_test.gomcdc_code_supplement_test.go
- mcdc_spec_witnesses_test.gomcdc_spec_witnesses_test.go
- path_compiler_test.gopath_compiler_test.go
- property_test.goproperty_test.go
- reference_oracle_test.goreference_oracle_test.go
- v131_regression_test.gov131_regression_test.go
- coverage_closure_test.gocoverage_closure_test.go
- dead_code_audit_test.godead_code_audit_test.go
- deep_spec_test.godeep_spec_test.go
- encoding_json_fuzz_test.goencoding_json_fuzz_test.go
- json_fuzz_test.gojson_fuzz_test.go
- path_fuzz_test.gopath_fuzz_test.go
- obligation_property_test.goobligation_property_test.go
- append_test.goappend_test.go
- config_test.goconfig_test.go
- v150_mcdc_witness_test.gov150_mcdc_witness_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.