Research / cJSON
For cJSON numbers, print-then-parse is not value-preserving.
MeasuredScoped- Result
- No. Numbers are printed at limited precision and re-read values are compared within a tolerance, so print-then-parse is not value-preserving.
- Boundary
- Number round-trip behaviour only, at one pinned revision. Not a judgement that the library is defective for its intended use.
- Who did what
- Independent study by Warren; no upstream report.
- Public evidence
- Public reproduction repositoryResults table
Interactive figure. Every number it draws is stated in the record below.
The question
Does a C JSON library preserve a number exactly through parse, print and parse again?
Exact round-tripping matters wherever JSON carries measurements or identifiers between systems. It is also the natural property for a machine-checked proof of the library to state, so it is worth finding out whether it is true before trying to prove it.
Measured: A quantity was measured independently, with the instrument itself checked on known answers. Scoped: Holds only for the revision, inputs and property named; read the boundary.
What was tested
- Read the number pipeline at source level.
- Wrote an independent re-implementation in Lean 4 and compared it with the C library on 120,000 fuzzed inputs from a fixed seed.
- Gave every input exactly one label, so no case could fall through unexplained.
- Guarded the harness with 16 verification gates and 20 deliberate attacks that check each gate actually fires.
What happened
- The source-level reading established the result: limited-precision printing plus a tolerance comparison means print-then-parse is not value-preserving.
- Of 120,000 inputs, 116,476 agreed exactly; 3,390 differed in ways the specification deliberately changes; 112 were attributed to the library’s floating-point pipeline; the harness could not decide 22; the Lean port was at fault in 0; none were unclassified.
- The 112 are recognised by a signature chosen by the author, so they are a classified subset, not an objective count of defects, and the finding does not rest on them.
Challenge
The objections that would most easily undo the conclusion, and what answered each.
- Could the Lean re-implementation be the one at fault?
- Checked by rules that use no author-chosen signature: it was at fault on 0 of 120,000 inputs.
- Could a gate in the harness silently fail to fire?
- 20 deliberate attacks confirm each of the 16 gates can fail.
- Does the result depend on the 112 classified cases?
- No. It rests on the source-level reading; the 112 are a classified subset that corroborates it.
What survived
Did not survive
- Print-then-parse preserves every number exactly.False by construction of the number pipeline; corroborated by the differential.
Survived
- The Lean re-implementation is never the side at fault.PORT_WRONG = 0 of 120,000, decided by rules that use no author-chosen signature.
Not established, or not tested
- Not a judgement that the library is defective for its intended use. A tolerant parser is a different design goal from an exactly round-tripping one.
- Divergence frequencies reflect the fuzzer’s mutation operator, not real-world prevalence.
Limits
Number round-trip behaviour only, at the pinned library revision.
Reproduce or inspect
- Source
- repowazdogz-droid/vsf-cjson
- Revision
dcdae40b (verified revision)- Command
./verify.sh --quick- Expect
16 gates pass, exit 0; PORT_WRONG = 0
Toolchain: Lean 4 v4.32.0 (Std only), Python 3 standard library, a C99 oracle. The full suite takes about 20 minutes. The command is given as the repository documents it; it was not re-run for this page.