Proof Portal

Projects

jsonparser

ProbeLabs36 findings · 123 requirements
STK-REQ-007StakeholderReview

Library users shall parse raw JSON scalar tokens into Go boolean, integer, float, and decoded string values with deterministic error behavior on malformed input.

PriorityshallTypeguaranteeCategoryfunctionalComponentparserAssuranceEFindingsnone open

Specification

The requirement exactly as authored — its complete prose text and, where present, the formal FRETish sentence it compiles to.

Description

Library users shall parse raw JSON scalar tokens into Go boolean, integer, float, and decoded string values with deterministic error behavior on malformed input.

Rationale & tags

Why this requirement exists, and how it is categorised.

The Parse* helpers are public token-level conversion utilities and their malformed-input behavior is part of the callable API surface.

parsedecompositionparseraccepts_user_data

Verification & provenance

How this requirement was checked: the review trail, edit history, and the machine-analysis status terms (each ⓘ explains what it means).

Assurance levelE
Formalizationnone
Vacuitychecked_ok
Strategyinformal

Review

Status
approved
Reviewer
human:leonidbugaev
Reviewed
Apr 23, 2026, 00:00 UTC

History

Created
Apr 13, 2026, 17:21 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.

10 obligations · 9 discharged · 1 not yet witnessed

Browse the catalogue
Discharged

Behavior at limits, thresholds, and edge-of-range values.

Worst case if violatedMedium

ParseInt on input like 9223372036854775808 (int64 max+1) must return OverflowIntegerError; if parseInt overflow flag regresses the result silently wraps to a negative int64.

Discharging evidence0/0 required witnessed
  • nominalrecommendedpresent
    Covered by 1 test
    via SYS-REQ-039
Discharged

Output identical regardless of collection ordering or runtime conditions.

Worst case if violatedMedium

ParseFloat on the same numeric token must return the same float64 across calls; a regression in parseFloat rounding direction produces non-deterministic results across calls.

Discharging evidence0/0 required witnessed
  • nominalrecommendedpresent
    Covered by 1 test
    via SYS-REQ-012
Discharged

Behavior for unusual but valid input combinations.

Worst case if violatedMedium

ParseBoolean on the empty token []byte returns (false, MalformedValueError); a regression returns (false,nil) and silently misreads empty input as boolean false.

Discharging evidence0/0 required witnessed
  • nominalrecommendedpresent
    Covered by 1 test
    via SYS-REQ-015
Discharged

Behavior when inputs are absent, nil, zero-length, or blank.

Worst case if violatedMedium

ParseInt on a zero-length []byte drives parseInt to ok=false; the caller receives MalformedValueError but a regression silently returns 0 instead, masking the empty-input case.

Discharging evidence0/0 required witnessed
  • nominalrecommendedpresent
    Covered by 1 test
    via SYS-REQ-064
Discharged

Behavior specified for encoding and decoding round-trips.

Worst case if violatedHigh

ParseString on a JSON string containing invalid UTF-8 bytes passes them through Unescape; the returned Go string contains invalid UTF-8, corrupting downstream rendering and string operations.

Discharging evidence0/0 required witnessed
  • nominalrecommendedpresent
    Covered by 1 test
    via SYS-REQ-014
Discharged

Behavior when inputs are syntactically or structurally invalid.

Worst case if violatedMedium

ParseFloat on a token like 1.2.3 drives parseFloat to error; a regression in the malformed check returns 1.2 (the partial parse) instead of MalformedValueError, silently corrupting numeric output.

Discharging evidence1/1 required witnessed
Discharged

Behavior specified when inputs are nil, null, or zero-value.

Worst case if violatedHigh

ParseString(nil) flows into Unescape(b, stackbuf[:]); the b[i] dereference inside Unescape panics with nil-slice index-out-of-range on the nil token.

Discharging evidence1/1 required witnessed
  • negativerequiredpresent
    Covered by 2 tests
    via SYS-REQ-015
  • nominalrecommendedpresent
    Covered by 1 test
    via SYS-REQ-015
Not yet witnessed

Happy-path behavior with valid inputs.

Discharging evidence0/0 required witnessed
    Discharged
    Worst case if violatedHigh

    ParseBoolean on a truncated tru or fals token fails bytes.Equal and returns MalformedValueError; a regression in the partial-literal check feeds the truncated bytes to a downstream consumer that panics on the short slice.

    Discharging evidence0/0 required witnessed
    • nominalrecommendedpresent
      Covered by 1 test
      via SYS-REQ-057
    Discharged
    Worst case if violatedHigh

    ParseString on a token ending in a truncated u-escape like abc\u31 drives Unescape hex-digit scan past the token end; if the bounds check regresses the parser reads past len(b) and panics.

    Discharging evidence0/0 required witnessed
    • nominalrecommendedpresent
      Covered by 1 test
      via SYS-REQ-060

    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.

    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.

    If you change this

    Requirements
    24
    Files
    3
    Tests
    14
    At-risk contracts
    0

    Requirements (24)

    Files to re-check (3)

    • fuzz.gofuzz.go
    • parser.goparser.go
    • escape.goescape.go

    Tests to re-run (14)

    • 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
    • mcdc_spec_witnesses_test.gomcdc_spec_witnesses_test.go
    • mcdc_supplement_test.gomcdc_supplement_test.go
    • reference_oracle_test.goreference_oracle_test.go
    • dead_code_audit_test.godead_code_audit_test.go
    • escape_test.goescape_test.go
    • bytes_test.gobytes_test.go
    • property_test.goproperty_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.

    Sign in to discuss this with the proof team.Sign in