Proof Portal

Projects

jsonparser

ProbeLabs36 findings · 123 requirements
STK-REQ-003StakeholderReview

Library users shall extract known numeric and boolean JSON values through typed helpers without manual byte parsing or ad-hoc conversions.

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 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.

The README presents typed helpers as part of the public API for callers who already know the expected JSON scalar type.

parseraccepts_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: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 catalogue
Discharged

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

Worst case if violatedMedium

GetInt on int64.MaxInt64+1 silently wraps via parseInt overflow flag; if the overflow check regresses, GetInt returns a negative int64 instead of OverflowIntegerError.

Discharging evidence0/0 required witnessed
  • nominalrecommendedpresent
    Covered by 1 test
    via SYS-REQ-076
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 (architecture-dependent FPU) produces non-deterministic results.

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

Behavior for unusual but valid input combinations.

Worst case if violatedMedium

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.

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

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

Worst case if violatedHigh

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.

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

Behavior when inputs are syntactically or structurally invalid.

Worst case if violatedHigh

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.

Discharging evidence1/1 required witnessed
  • negativerequiredpresent
    Covered by 2 tests
    via SYS-REQ-075
  • nominalrecommendedpresent
    Covered by 1 test
    via SYS-REQ-075
Discharged

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

Worst case if violatedHigh

GetBoolean(nil, ...) flows through Get nil-slice path; getType(nil,0) data[offset] dereference panics with nil-slice index-out-of-range.

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

Happy-path behavior with valid inputs.

Discharging evidence0/0 required witnessed
    Discharged
    Worst case if violatedHigh

    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.

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

    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.

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

    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.

    • 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.

    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
    11
    Files
    3
    Tests
    13
    At-risk contracts
    0

    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.

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