Proof Portal
jsonparser
ProbeLabs36 findings · 123 requirementsParsePath converts a JSONPath-style string (root $.
Specification
The requirement exactly as authored — its complete prose text and, where present, the formal FRETish sentence it compiles to.
ParsePath converts a JSONPath-style string (root $. optionally followed by dot-delimited keys, [N] numeric array-index bracket components, [*] wildcard, and "quoted" keys containing dots or brackets) into the path-component slice accepted by Get/Set/Delete/ArrayEach/EachKey. CompilePath parses the path once and returns a CompiledPath value whose Get/GetString/GetInt/Set/Delete/ArrayEach/EachKey methods behave identically to invoking the equivalent top-level function with the parsed components. ParsePath returns errEmptyPath for an empty input and errMalformedPath for any non-conforming syntax (unbalanced bracket, missing key between dots, control character in quoted key, non-numeric bracket index other than *).
the parser shall always satisfy compiled_jsonpath_resolves_to_same_result_as_equivalent_key_path
Rationale & tags
Why this requirement exists, and how it is categorised.
Rationale & tags
Why this requirement exists, and how it is categorised.
v1.4.0 exposes a JSONPath compiler so callers can amortize the cost of parsing a path string across many Get/Set/Delete operations and so external callers can express bracket-index paths without hand-assembling [N] tokens. The contract that CompiledPath methods are observationally equivalent to the equivalent top-level function must be explicit so future refactors do not diverge the compiled and uncompiled code paths.
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
- human:buger · lead_engineer
- Reviewed
- Jul 28, 2026, 09:13 UTC
History
- Created
- Jul 28, 2026, 08:29 UTC · human:cli
- Modified
- Jul 28, 2026, 09:13 UTC · human:buger
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.
CompiledPath methods diverge observationally from invoking the equivalent top-level function with the parsed components (different error semantics, different returned offsets, different mutated document shape), breaking the substitution invariant callers rely on.
- nominalrequiredpresentCovered by 2 tests
Behavior at limits, thresholds, and edge-of-range values.
A root path ("$" or "$.") or empty input drives ParsePath to return a wrong-shaped slice (nil vs empty) or to panic; the root-array-index case ("$[0]") misroutes through the dotted-key parser and returns errMalformedPath for a valid path.
- nominalrequiredpresentCovered by 1 test
- negativerecommendedpresentCovered by 1 test
Behavior when inputs are syntactically or structurally invalid.
An unbalanced bracket, missing key between dots, control character in a quoted key, or non-numeric bracket index other than * is accepted as a parsed component instead of returning errMalformedPath / errUnterminatedKey, producing a path slice that silently fails to resolve downstream or crashes searchKeys.
- negativerequiredpresentCovered by 1 test
- 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 compiled_jsonpath_resolves_to_same_result_as_equivalent_key_path
Variables
| Name | Type | Direction | Description |
|---|---|---|---|
| compiled_jsonpath_resolves_to_same_result_as_equivalent_key_path | — | True when ParsePath converts a JSONPath-style string ($.dot, [N], [*], "quoted") into the path-component slice accepted by Get/Set/Delete/ArrayEach/EachKey and CompiledPath methods are observationally equivalent to invoking the matching top-level function with the parsed components, with errEmptyPath for empty input and errMalformedPath for non-conforming syntax. |
Witnesses· 2 scenarios total
- TestMCDC_SYS_REQ_114_Row1_InvariantViolationmcdc_spec_witnesses_test.go:3621exercises 1 condition scenario
- TestMCDC_SYS_REQ_114_Row2_Nominalmcdc_spec_witnesses_test.go:3639exercises 1 condition scenario
- TestCompilePathRoundTrippath_compiler_test.go:165
- TestParsePathErrorspath_compiler_test.go:84
- TestParsePathpath_compiler_test.go:9
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)
- path_compiler.gopath_compiler.go
Tests to re-run (3)
- mcdc_spec_witnesses_test.gomcdc_spec_witnesses_test.go
- parser_test.goparser_test.go
- path_compiler_test.gopath_compiler_test.go
What this rests on
Parent requirements (1)
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.