Proof Portal
jsonparser
ProbeLabs23 findings · 123 requirementsThe fastest JSON parser for Go — formally verified with ReqProof (real library, master).
Library users shall retrieve addressed JSON values as zero-allocation raw strings without JSON unescaping when they intentionally choose the unsafe helper.
Specification
The requirement exactly as authored — its complete prose text and, where present, the formal FRETish sentence it compiles to.
Library users shall retrieve addressed JSON values as zero-allocation raw strings without JSON unescaping when they intentionally choose the unsafe helper.
Rationale & tags
Why this requirement exists, and how it is categorised.
Rationale & tags
Why this requirement exists, and how it is categorised.
GetUnsafeString is a distinct public contract from GetString because it trades escaping semantics for speed and zero-allocation string mapping.
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
- Leonidbugaev
- Reviewed
- Apr 23, 2026, 00:00 UTC
History
- Created
- Apr 13, 2026, 17:21 UTC · Created via CLI
- Modified
- Jul 26, 2026, 12:54 UTC · Created via CLI
Change history
Every recorded revision of this requirement's source file — newest first, each with its commit message and the diff for that change.
Every recorded revision of this object's source — newest first, each with the commit message and its file-level diff.
Obligations
What this requirement must witness to be considered satisfied — the required evidence, and the tests that discharge each one.
7 obligations · 6 discharged · 1 not yet witnessed
Browse the catalogueEvidence tagged via <REQ> is witnessed by a requirement that satisfies this one — normal for stakeholder / aggregate requirements, which are proven through the requirements that refine them.
Output identical regardless of collection ordering or runtime conditions.
Two GetUnsafeString calls on identical input must return byte-identical Go strings via bytesToString; a regression in slice aliasing produces non-deterministic content if the input buffer is concurrently mutated.
- nominalrecommendedpresentCovered by 1 test
Behavior for unusual but valid input combinations.
GetUnsafeString on a payload with value empty-string must return the empty Go string; a regression in the String-strip path returns the surrounding quotes as part of the value.
- nominalrecommendedpresentCovered by 1 test
Behavior when inputs are absent, nil, zero-length, or blank.
GetUnsafeString on a zero-length []byte flows through Get to internalGet to nextToken=-1; the follow-on data[offset] dereference in getType panics on the empty slice.
- nominalrecommendedpresentCovered by 1 test
Behavior when inputs are syntactically or structurally invalid.
GetUnsafeString on adversarial JSON like {"k":} drives Get to searchKeys returning a stale offset; the follow-on data[offset] dereference panics (the OSS-Fuzz bug class on the unsafe path).
- negativerequiredpresentCovered by 2 tests
- nominalrecommendedpresentCovered by 1 test
Behavior specified when inputs are nil, null, or zero-value.
GetUnsafeString(nil,...) flows through Get to searchKeys nil-slice loop; getType(nil,0) 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.
Payload like {"k":"abc with no closing quote drives stringEnd to -1; if the guard regresses getType data[offset] dereference panics past the buffer end on the unsafe string path.
- 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 retrieve an addressed JSON value through GetUnsafeString and receive the raw bytes as a Go string without JSON unescaping, including the documented lookup-miss behavior from the underlying path lookup.
Derived requirementsAcceptance test
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 (7)
- When GetUnsafeString addresses a JSON string value, the…parser · SYS
- When GetUnsafeString is called on malformed input where the…parser · SYS
- When GetUnsafeString is called on empty input, the parser…parser · SYS
- When GetUnsafeString is called on input truncated at a…parser · SYS
- When GetUnsafeString is called twice with identical JSON…parser · SYS
- When GetUnsafeString is called with a nil byte slice as…parser · SYS
- When GetUnsafeString is called on JSON containing values…parser · SYS
Files to re-check (2)
- fuzz.gofuzz.go
- parser.goparser.go
Tests to re-run (7)
- obligation_evidence_test.goobligation_evidence_test.go
- parser_test.goparser_test.go
- fuzz_native_test.gofuzz_native_test.go
- mcdc_spec_witnesses_test.gomcdc_spec_witnesses_test.go
- mcdc_supplement_test.gomcdc_supplement_test.go
- deep_spec_test.godeep_spec_test.go
- obligation_property_test.goobligation_property_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.