Proof Portal
jsonparser
ProbeLabs23 findings · 123 requirementsLibrary users shall retrieve string values with JSON escapes and Unicode decoded into Go strings.
Specification
The requirement exactly as authored — its complete prose text and, where present, the formal FRETish sentence it compiles to.
Library users shall retrieve string values with JSON escapes and Unicode decoded into Go strings.
Rationale & tags
Why this requirement exists, and how it is categorised.
Rationale & tags
Why this requirement exists, and how it is categorised.
The README explicitly promises that GetString handles escaped and Unicode characters correctly, which is a user-visible contract distinct from raw byte lookup.
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
- Buger · lead_engineer
- Reviewed
- Aug 20, 2026, 13:11 UTC
History
- Created
- Apr 13, 2026, 17:09 UTC · Created via CLI
- Modified
- Aug 20, 2026, 13:11 UTC · Buger
Change history
Every recorded revision of this requirement's source file — newest first, each with its commit message and the diff for that change.
Review history
Human and AI-agent approvals of this requirement — the 'why was this approved' lineage, each with the reviewer's justification and the code it cites.
- Claude:spec Conformance · AI agentApprovedSpec conformanceAug 20, 2026 · last monthREVIEW-2
GetString implements the decode-escapes-and-Unicode contract by fetching the raw String value via Get, rejecting non-string types (Null -> NullValueError, else a type error), returning the raw bytes when no backslash is present, and otherwise delegating to ParseString -> Unescape for full JSON unescaping. The unescaping pipeline is genuinely present but carries tracked defects in its shared decoder: unescapeToUTF8Config's escape switch omits '/' so the valid JSON escape \/ is rejected as malformed (KI-14), decodeSingleUnicodeEscape's length guard was weakened to len(in) < 4 so a truncated \u escape reads in[4]/in[5] out of bounds and panics (KI-5), and h2I accepts byte 'G' as hex 16 so \uGxxx is silently decoded (KI-9); the lone-surrogate guards (KI-6/KI-8) share this path. The requirement and the GetString structure are sound; the escape/Unicode decoding is broken only through these tracked known issues.
Cited code (5)
Obligations
What this requirement must witness to be considered satisfied — the required evidence, and the tests that discharge each one.
9 obligations · 9 discharged
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 GetString calls on identical input must return byte-identical Go strings; a regression in the Unescape path (surrogate-pair handling diverging between stack and heap allocations) produces different decoded output.
- nominalrecommendedpresentCovered by 1 test
Behavior for unusual but valid input combinations.
GetString on an empty JSON string value ("") regresses to returning NullValueError or an empty slice instead of the empty Go string, breaking the empty-string boundary.
- nominalrecommendedpresentCovered by 1 test
Behavior when inputs are absent, nil, zero-length, or blank.
GetString on a zero-length []byte drives Get to internalGet to nextToken=-1; the follow-on getType dereference panics with index-out-of-range on the empty slice.
- nominalrecommendedpresentCovered by 2 tests
Behavior specified for encoding and decoding round-trips.
Malformed UTF-8 inside a JSON string value (lone continuation byte) is passed through Unescape without normalization; the returned Go string contains invalid UTF-8, corrupting downstream string operations.
- nominalrecommendedpresentCovered by 2 tests
Behavior when inputs are syntactically or structurally invalid.
Adversarial JSON like {"k":"\\q"} drives Unescape to MalformedStringEscapeError; if error propagation regresses, GetString returns a corrupt decoded string or panics on the bad escape offset.
- negativerequiredpresentCovered by 4 tests
- nominalrecommendedpresentCovered by 4 tests
Behavior specified when inputs are nil, null, or zero-value.
GetString(nil, ...) flows straight through Get to internalGet 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.
- nominalrecommendedpresent
Truncated \u escape at end of string ("abc\u31") drives Unescape hex-digit scan past the buffer end; if the bounds check regresses the parser reads past len(data) and panics with slice-bounds error.
- nominalrecommendedpresentCovered by 1 test
GetString on a JSON Number or Boolean returns the documented type error or silently coerces the raw bytes; callers expecting a string field read garbage from a numeric value.
- 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 string field and receive the correctly decoded Go string, including escaped and Unicode content, or an error when string access is invalid.
Derived requirementsAcceptance test
Its place
How this requirement connects — what proves it, what it affects, and what it rests on. Authored links only here; automatically derived links come from the audit index.
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 — authored trace links only (automatically derived links come from the audit index and aren't shown here).
Impact
Blast radius — authored trace links only (automatically derived links come from the audit index and aren't shown here).
If you change this
Requirements (11)
- When GetString addresses a JSON string value whose raw…parser · SYS
- When GetString is called on malformed input where the…parser · SYS
- When GetString addresses a JSON string value containing a…parser · SYS
- When GetString addresses a value that is not a JSON string…parser · SYS
- When GetString is called on empty input, the parser shall…parser · SYS
- When GetString is called twice with identical JSON input…parser · SYS
- When GetString is called with a nil byte slice as input,…parser · SYS
- When GetString is called on a JSON string containing…parser · SYS
- When GetString is called on JSON containing Unicode edge…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 (5)
- fuzz.gofuzz.go
- parser.goparser.go
- config.goconfig.go
- escape.goescape.go
- reader_parser.goreader_parser.go
Tests to re-run (12)
- obligation_evidence_test.goobligation_evidence_test.go
- parser_test.goparser_test.go
- escape_test.goescape_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
- property_test.goproperty_test.go
- deep_spec_test.godeep_spec_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.