Proof Portal

Sign in
Projects

jsonparser

ProbeLabs36 findings · 123 requirements
All requirements
SYS-REQ-115SystemApproved

When a Config with AllowSingleQuotes=true is provided, the parser shall accept single-quoted strings (delimited by ' instead of ") using the same escape rules as double-quoted strings.

PriorityshallTypeguaranteeCategoryfunctionalComponentparserAssuranceBFindingsnone open

Specification

The requirement exactly as authored — its complete prose text and, where present, the formal FRETish sentence it compiles to.

Description

When a Config with AllowSingleQuotes=true is provided, the parser shall accept single-quoted strings (delimited by ' instead of ") using the same escape rules as double-quoted strings. When AllowUnknownEscapes=true, unknown escape sequences shall be passed through literally instead of returning an error. The default Config shall remain strict (RFC 8259 only).

FRETish formula
the parser shall always satisfy config_lenient_modes_are_opt_in_and_default_remains_strict

Rationale & tags

Why this requirement exists, and how it is categorised.

v1.5.0 introduces explicit opt-in compatibility modes for common non-RFC JSON emitted by external systems while preserving the strict behavior and API contracts of every existing package-level function.

configlenientsingle_quotesescapesnominalmalformed_inputencoding_safety

Verification & provenance

How this requirement was checked: the review trail, edit history, and the machine-analysis status terms (each ⓘ explains what it means).

Assurance levelB
Formalizationvalid
Realizabilityrealizable
Vacuitychecked_ok
Strategyfretish

Review

Status
approved
Reviewer
human:buger · lead_engineer
Reviewed
Jul 28, 2026, 13:58 UTC
“v1.5.0: Config + lenient parsing (SYS-REQ-115), streaming ReaderParser (SYS-REQ-116)”

History

Created
Jul 28, 2026, 00:00 UTC · agent:codex
Modified
Jul 28, 2026, 13:58 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 · 2 discharged · 1 not yet witnessed

Browse the catalogue
Discharged

Happy-path behavior with valid inputs.

Worst case if violatedMedium

A Config with AllowSingleQuotes enabled fails to recognize matching single-quoted keys or values, returns incorrect offsets, or lets a quote/bracket inside a single-quoted string terminate the surrounding container early.

Discharging evidence1/1 required witnessed
  • nominalrequiredpresent
    Covered by 5 tests
1/2 witnessed

Behavior when inputs are syntactically or structurally invalid.

Worst case if violatedMedium

DefaultConfig or an existing package-level function silently accepts single-quoted input or unknown escapes, weakening the established strict contract for callers that rely on malformed-input rejection.

Discharging evidence1/2 required witnessed
  • negativerequirednot yet witnessed
    Required evidence not yet witnessed — no covering test recorded.
  • nominalrequiredpresent
    Covered by 2 tests
Discharged

Behavior specified for encoding and decoding round-trips.

Worst case if violatedMedium

AllowUnknownEscapes drops or duplicates bytes, consumes a malformed Unicode escape as an unknown escape, or emits a different literal value than the escaped input represents.

Discharging evidence1/1 required witnessed
  • nominalrequiredpresent
    Covered by 1 test

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 config_lenient_modes_are_opt_in_and_default_remains_strict

Variables

NameTypeDirectionDescription
config_lenient_modes_are_opt_in_and_default_remains_strict—True when Config accepts single-quoted strings only with AllowSingleQuotes, passes unknown escape bytes through literally only with AllowUnknownEscapes, and the zero/default Config plus package-level functions retain strict RFC 8259 behavior.

Witnesses· 2 scenarios total

  • TestConfigBackwardCompat
    config_test.go:102
  • TestConfigRoundTrip
    config_test.go:115
  • TestConfigTraversalAndDelete
    config_test.go:141
  • TestConfigGetString
    config_test.go:35
  • TestConfigSet
    config_test.go:50
  • TestConfigAllowUnknownEscapes
    config_test.go:65
  • TestConfigStrictStillWorks
    config_test.go:89
  • TestConfigGet
    config_test.go:9
  • TestMCDC_SYS_REQ_115_Row1_StrictConfigRejectsSingleQuotes
    v150_mcdc_witness_test.go:22exercises 1 condition scenario
  • TestMCDC_SYS_REQ_115_Row2_LenientConfigParsesSingleQuotes
    v150_mcdc_witness_test.go:8exercises 1 condition scenario

Its place

This requirement shown inside its trace neighbourhood — the parents it satisfies, the code and tests attached to it, and its findings.

Open in graph

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.

If you change this

Requirements
0
Files
3
Tests
2
At-risk contracts
0

Files to re-check (3)

  • config.goconfig.go
  • escape.goescape.go
  • parser.goparser.go

Tests to re-run (2)

  • config_test.goconfig_test.go
  • v150_mcdc_witness_test.gov150_mcdc_witness_test.go

What this rests on

Parent requirements (4)

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