Proof Portal

Projects

jsonparser

ProbeLabs23 findings · 123 requirements
Showing the current git stateNo audit has been synced for this project yet — verification results (proof status, coverage, solver signals) appear once an audit is published.proof-demod79405e
All requirements
RequirementSTK-REQ-003StakeholderApproved

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

All automated checks pass and 2/2 obligations are satisfied. Reviewed last month.
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
Strategyinformal

Review

Status
approved
Reviewer
Buger · lead_engineer
Reviewed
Aug 20, 2026, 13:11 UTC
Spec-conformance reviewed (agent:claude:spec-conformance); approved on owner authorization.

History

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

  1. Claude:spec Conformance · AI agentApprovedSpec conformanceAug 20, 2026 · last monthREVIEW-3

    The typed scalar helpers exist and are wired correctly: GetInt/GetFloat/GetBoolean each call Get, enforce the expected ValueType (returning NullValueError for null and a descriptive type error otherwise), then delegate to ParseInt/ParseFloat/ParseBoolean, giving callers a typed value or an explicit error as AC-1..AC-3 require. Two tracked defects sit in the delegated conversions: parseInt's fast-path threshold is widened to l-i < 20 so a 19-digit literal exceeding int64 skips the overflow-checked slow path and wraps silently instead of returning OverflowIntegerError (KI-7, reached through GetInt/SYS-REQ-076), and ParseBoolean uses bytes.HasPrefix rather than bytes.Equal so GetBoolean on a token like 'trueish' returns (true,nil) instead of a malformed error (KI-11). GetFloat's ParseFloat path is sound. The requirement is sound and implemented; the integer-overflow and boolean-exactness bugs are tracked.

    Cited code (4)

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

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

Discharged

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

If it were 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.

If it were 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.

If it were 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.

If it were 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.

If it were 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.

If it were 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
    If it were 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
    If it were 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.

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

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

    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