Proof Portal
jsonparser
ProbeLabs36 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
- human:leonidbugaev
- Reviewed
- Apr 23, 2026, 00:00 UTC
History
- Created
- Apr 13, 2026, 17:09 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.
9 obligations · 9 discharged
Browse the catalogueOutput 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 2 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.
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 (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.