OBSERVED
Finding · verify
A widely used library reads a number, writes it back out, and the two are not the same.
§ 1
The record
FINDING · cjson-does-not-round-trip-numbersverify
A widely used library reads a number, writes it back out, and the two are not the same.
- Claim
- A widely used C JSON library does not preserve numbers across a serialise-and-reparse round trip: its number pipeline is lossy by design, printing with limited precision and comparing re-reads by tolerance rather than equality.
- Status
- OBSERVED Witnessed in one instance. No claim about how often.
- Subject
- cJSON, a widely used C JSON library (third-party system), against a Lean re-implementation. third-party subject
- Frame
- Number round-trip only; a lax parser tuned for triage.
- Method
- Differential testing of the Lean model against the C reference over a fuzzed corpus.
- Oracle
- The C library's own output on the same inputs.
- Negative control
- Present A 20-attack mutation suite guards the harness; 0 port-wrong classifications over 120,000 inputs.
- Denominator
- 116,476 agree of 120,000 fuzzed inputs; idempotence over 20,318.
- Limitation
- That the library is defective for its purpose. A lax parser tuned for triage is a different artifact from one built to be exactly round-tripping; this is that a round-trip theorem is false of the target, not a quality judgement.
- Source
- repowazdogz-droid/vsf-cjson @ dcdae40b
- Reproduce
./verify.sh --quick
- Independent reproduction
- None known.
§ 2
Where this sits
This finding answers The specification proved is not the property intended and supports the VERIFY stage of the operating method.