Proof Portal
jsonparser
ProbeLabs23 findings · 123 requirementsThe fastest JSON parser for Go — formally verified with ReqProof (real library, master).
GetArrayLen returns the number of elements in the addressed JSON array (0 for an empty array), and GetObjectLen returns the number of key-value pairs in the addressed JSON object (0 for an empty object).
Specification
The requirement exactly as authored — its complete prose text and, where present, the formal FRETish sentence it compiles to.
GetArrayLen returns the number of elements in the addressed JSON array (0 for an empty array), and GetObjectLen returns the number of key-value pairs in the addressed JSON object (0 for an empty object). Both helpers address the container by key path without invoking a caller callback, returning KeyPathNotFoundError when the path is missing and MalformedArrayError / MalformedObjectError when the addressed value is not the expected container type.
the parser shall always satisfy !addressed_container_is_array_or_object | returns_container_element_count
Rationale & tags
Why this requirement exists, and how it is categorised.
Rationale & tags
Why this requirement exists, and how it is categorised.
Existing ArrayEach/ObjectEach iteration APIs force the caller to provide a callback that runs per element; callers who only need the count pay callback overhead and must carry mutation hazards in the callback closure. A direct length accessor closes the gap as a v1.4.0 exported helper.
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
- Buger · lead_engineer
- Reviewed
- Jul 28, 2026, 08:49 UTC
History
- Created
- Jul 28, 2026, 08:28 UTC · Created via CLI
- Modified
- Jul 28, 2026, 08:49 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.
Every recorded revision of this object's source — newest first, each with the commit message and its file-level diff.
Obligations
What this requirement must witness to be considered satisfied — the required evidence, and the tests that discharge each one.
3 obligations · 3 discharged
Browse the catalogueHappy-path behavior with valid inputs.
GetArrayLen/GetObjectLen return a count that does not match the actual number of elements/pairs in the addressed container, silently corrupting downstream length-based branching.
- nominalrequiredpresentCovered by 2 tests
Behavior at limits, thresholds, and edge-of-range values.
An empty addressed array ([]) or object ({}) drives a regression in scanContainerLen that double-counts the closing delimiter or panics on the empty body, inverting the zero-vs-nonzero branch downstream.
- nominalrequiredpresentCovered by 2 tests
Behavior when inputs are syntactically or structurally invalid.
A non-container addressed value (scalar, mismatched bracket) or a missing path returns a silent zero count or a wrong error type (e.g. nil instead of MalformedArrayError / KeyPathNotFoundError), hiding the lookup failure from the caller.
- negativerequiredpresentCovered by 2 tests
- nominalrequiredpresentCovered by 2 tests
Formula evidence
The formal formula behind this requirement, the variables it is written over, and the tests that exercise it (each term is explained inline).
Formula evidence
The formal formula behind this requirement, the variables it is written over, and the tests that exercise it (each term is explained inline).
FRETish formula
the parser shall always satisfy !addressed_container_is_array_or_object | returns_container_element_count
Variables
| Name | Type | Direction | Description |
|---|---|---|---|
| addressed_container_is_array_or_object | — | True when the value addressed by the GetArrayLen/GetObjectLen key path is a JSON array (GetArrayLen) or object (GetObjectLen) container rather than a scalar or missing path. | |
| returns_container_element_count | — | True when GetArrayLen returns the number of elements in the addressed array (0 for an empty array) or GetObjectLen returns the number of key-value pairs in the addressed object (0 for an empty object), with no caller callback invoked. |
Witnesses· 3 scenarios total
- TestMCDC_SYS_REQ_112_Row1_TriggerFalseexercises 1 condition scenario
- TestMCDC_SYS_REQ_112_Row2_InvariantViolationexercises 1 condition scenario
- TestMCDC_SYS_REQ_112_Row3_Nominalexercises 1 condition scenario
MC/DC truth table· 3 rows
Each row assigns the formula's conditions (T/F) and shows the Result— the formula's value for that input row, not a test pass/fail. A row proves a condition when flipping only that condition flips the outcome. The test that covers each row is linked.
mcdc:ignoreNo-actionfalse-result row satisfied by designUncoveredneeds a covering test| # | addressed_container_is_array_or_object | returns_container_element_count | Result | Proves | Covering test |
|---|---|---|---|---|---|
| 1 | F | F | T | addressed_container_is_array_or_object | |
| 2 | T | F | F | addressed_container_is_array_or_object | |
| 3 | T | T | T | returns_container_element_count |
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.
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
Files to re-check (1)
- parser.goparser.go
Tests to re-run (3)
- len_uint_test.golen_uint_test.go
- mcdc_spec_witnesses_test.gomcdc_spec_witnesses_test.go
- parser_test.goparser_test.go
What this rests on
Parent requirements (1)
Changes
Semantic changes that move or scope this requirement — the intended work touching it. Each links to the full 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.