Proof Portal

Sign in
Projects

jsonparser

ProbeLabsviewing a historical run
Viewing historical run d79405eAug 20, 2026, 03:41 PMproof-demoaudited with uncommitted changes — showing the committed treeBack to current
Back to findings
Problem reportDEFECT-260727-T7P7

Set on top-level array-index beyond length returns KeyPathNotFoundError (SYS-REQ-110 contract gap)

FixedFixedMedium

This defect has been fixed and verified.

Closure: Requirement re-verified
Related known issues:KI-4

Affected requirements

The requirement(s) this issue violates — click through to the spec.

SYS-REQ-110

Severity, explained

Why this is rated the way it is — and the scoring signals behind the rating (each ⓘ explains the term).

MediumRated severity — the impact if this issue is exploited or hit.
risk area
Data Integrity

Root cause

What actually went wrong underneath — how it is classified, and the coverage gap that let it slip through.

parser.go:Set, endOffset==-1 branch: the code path for "path not found at all" only handles (pathIsIndex && dataIsObject) and (pathIsObjectKey && dataIsArray) cross-type coercions; the matching (pathIsIndex && dataIsArray) case is explicitly rejected with KeyPathNotFoundError. SYS-REQ-110 does not carve out this exception, so it is a spec/code divergence that requires either narrowing the spec or extending Set.

Spec gap— this behaviour wasn't specified
Why this escaped
Missing requirement

Disposition: Covered by a known issue

Proof it's fixed

The tests, tightened requirements and new obligations that prove this defect is gone — and can't quietly return.

Covered by a known issue.

strengthened requirements
SYS-REQ-110

Blast radius

If you touch this issue, what else may need re-checking — the requirements it affects and the code and tests that hang off them. Historical view: authored trace links only — automatically derived links aren't reconstructible for past runs.

Tracing blast radius…

Touch this finding and you re-check 1 requirements · 2 code files · 7 tests.

Requirements (1)
SYS-REQ-110
Code files (2)
  • append.go
  • parser.go
Tests (7)
  • append_test.go
  • fuzz_native_test.go
  • mcdc_supplement_test.go
  • parser_test.go
  • reference_oracle_test.go
  • set_spec_test.go
  • sys_req_110_111_witness_test.go

Per-requirement evidence

For each requirement this finding touches: the implementing code, verifying tests, and proof obligations that discharge it.

SYS-REQ-110
Implementing code (4)
  • append.go
    Append
  • parser.go
    Set
  • parser.go
    createInsertComponent
  • parser.go
    setConfig
Tests & evidence (9)
  • README.md
  • append_test.go
  • docs/proof-gap-root-cause.md
  • fuzz_native_test.go
  • mcdc_supplement_test.go
  • parser_test.go
  • reference_oracle_test.go
  • set_spec_test.go
  • sys_req_110_111_witness_test.go
Proof obligations (3)
boundary

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

  • ✓nominal (required) — sys_req_110_111_witness_test.go:33
  • ✓negative — parser_test.go:2484
element_type_partition
  • ✓nominal (required) — parser_test.go:2485
nested_mutation
  • ✓nominal (required) — sys_req_110_111_witness_test.go:81

Change history

Every recorded revision of this finding's source file — when it was added, edited, or re-classified, with the diff for each change.

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