Proof Portal
jsonparser
ProbeLabs36 findings · 123 requirementsLibrary users shall extract known numeric and boolean JSON values through typed helpers without manual byte parsing or ad-hoc conversions.
Specification
The requirement exactly as authored — its complete prose text and, where present, the formal FRETish sentence it compiles to.
Library users shall extract known numeric and boolean JSON values through typed helpers without manual byte parsing or ad-hoc conversions.
Rationale & tags
Why this requirement exists, and how it is categorised.
Rationale & tags
Why this requirement exists, and how it is categorised.
The README presents typed helpers as part of the public API for callers who already know the expected JSON scalar type.
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: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 · 8 discharged · 1 not yet witnessed
Browse the catalogueBehavior at limits, thresholds, and edge-of-range values.
GetInt on int64.MaxInt64+1 silently wraps via parseInt overflow flag; if the overflow check regresses, GetInt returns a negative int64 instead of OverflowIntegerError.
- nominalrecommendedpresentCovered by 1 test
Output identical regardless of collection ordering or runtime conditions.
ParseFloat on the same numeric token must return the same float64 across calls; a regression in parseFloat rounding direction (architecture-dependent FPU) produces non-deterministic results.
- nominalrecommendedpresentCovered by 1 test
Behavior for unusual but valid input combinations.
GetBoolean on a payload with value null returns NullValueError instead of (false,nil); callers treating the zero-value as absent silently misread null fields as boolean false.
- nominalrecommendedpresentCovered by 1 test
Behavior when inputs are absent, nil, zero-length, or blank.
GetInt on a zero-length []byte flows through Get empty-input path; the data[offset] dereference in getType panics with index-out-of-range on the empty slice.
- nominalrecommendedpresentCovered by 1 test
Behavior when inputs are syntactically or structurally invalid.
GetInt on a token like 12x34 drives parseInt to ok=false; if the malformed check regresses, GetInt silently returns 12 (the partial parse) instead of MalformedValueError.
- negativerequiredpresentCovered by 2 tests
- nominalrecommendedpresentCovered by 1 test
Behavior specified when inputs are nil, null, or zero-value.
GetBoolean(nil, ...) flows through Get nil-slice path; 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.
GetBoolean on a truncated tru or fals token fails bytes.Equal against the literal; if the partial-literal recovery regresses the caller path panics on the empty value slice.
- nominalrecommendedpresentCovered by 1 test
GetInt on a JSON String value returns the documented not-a-number error; if the type check regresses, GetInt feeds raw quoted bytes to ParseInt which silently returns 0 instead of erroring.
- 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 an integer-valued field through a typed helper and receive the expected int64 result or an error when integer access is invalid.
Derived requirements - AC-2verify: test
A caller can request a floating-point field through a typed helper and receive the expected float64 result or an error when float access is invalid.
Derived requirements - AC-3verify: test
A caller can request a boolean field through a typed helper and receive the expected bool result or an error when boolean access is invalid.
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 (11)
- When GetInt addresses a JSON number token that is parseable…parser · SYS
- When GetFloat addresses a JSON number token that is…parser · SYS
- When GetBoolean addresses a well-formed JSON boolean token,…parser · SYS
- When GetInt is called on malformed input where the…parser · SYS
- When GetInt addresses a JSON number token whose magnitude…parser · SYS
- When GetInt addresses a value that is not a JSON number (eparser · SYS
- When GetInt is called on empty input, the parser shall…parser · SYS
- When GetBoolean addresses a value that appears to be a…parser · SYS
- When GetInt, GetFloat, or GetBoolean is called twice with…parser · SYS
- When GetInt, GetFloat, or GetBoolean is called with a nil…parser · SYS
- When GetInt is called on JSON containing numeric edge cases…parser · SYS
Files to re-check (3)
- fuzz.gofuzz.go
- parser.goparser.go
- aliases.goaliases.go
Tests to re-run (13)
- 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
- fuzz_native_test.gofuzz_native_test.go
- len_uint_test.golen_uint_test.go
- mcdc_spec_witnesses_test.gomcdc_spec_witnesses_test.go
- mcdc_supplement_test.gomcdc_supplement_test.go
- aliases_test.goaliases_test.go
- array_each_err_test.goarray_each_err_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.