Extended robustness test suite (proptest / fuzz / miri / kani) — offered as-is

[enomado]

Hi! 👋 This is an independent, external robustness audit of the parser +
serializer, offered purely as an FYI — take whatever is useful and drop the
rest. No pressure, no CI changes proposed, and nothing here alters crate
behaviour (the kani code is #[cfg(kani)]-gated and inert in normal builds).

Headline

No memory-safety issue was found. ron held up across every angle:

Layer	Result
miri (Stacked Borrows)	lib unit tests + the RawValue unsafe — 0 UB
fuzz (libFuzzer + ASAN)	from_str, a new fixpoint roundtrip, and a new raw_value target — 11.7M execs, 0 crashes
proptest (~14k cases)	no-panic, serializer self-consistency, ser→parse fixpoint, pretty≡compact — all green
kani	decode_hex + is_int_char proven total / panic-free over the entire char domain

What's added

• tests/zz_audit_proptest.rs — property harness over a recursive Value.
• fuzz/fuzz_targets/roundtrip.rs — fixpoint round-trip (parse → ser → parse must agree).
• fuzz/fuzz_targets/raw_value.rs — drives the crate's only unsafe (RawValue transmutes + trim_boxed drain) under AddressSanitizer.
• src/kani_verification.rs + #[cfg(kani)] mod kani_parse_proofs in parse.rs — bounded proofs. (Note: the full from_str path overwhelms CBMC's budget — expected for string-scanning parsers; the pure helpers verify instantly.)

Two correctness/fidelity notes (NOT soundness), each pinned by a test

1. Value round-trip is not type-preserving (zz_finding_number_narrowing.rs). The default serializer emits no type suffix, so 1.5f64 → "1.5" → f32 and 5u16 → "5" → u8. The value survives; the numeric type narrows. The roundtrip fuzzer found and minimised this to NaNf64.
2. IMPLICIT_SOME map serialization is not injective (zz_finding_implicit_some.rs). Keys Some(()) and () both print as (), producing a duplicate-key map that silently drops an entry on re-parse. Same root cause as the documented IMPLICIT_SOME ambiguity class in 502_known_bugs.rs; proptest rediscovered it automatically.

Both are surprising-but-arguably-known consequences of existing design trade-offs, not new bugs — sharing them in case the concrete reproductions are useful.

Thanks for ron! 🦀

---

🤖 Generated with Claude Code

[enomado]

Follow-up: a longer fuzz run of the roundtrip target surfaced a third,
sharper note — an f32-typed Value does not survive a serialize→parse
round-trip, and the numeric value drifts (pinned in tests/zz_finding_float_precision.rs).

Minimised from 924444480f64..922.:

• 924444480 is exactly f32-representable, so Value infers F32. (The
  "fits in f32" check is otherwise fine — e.g. 16777217 is correctly kept as
  F64, so this is not a blanket "Value truncates floats" issue.)
• Rust's f32 formatter prints that value's shortest round-tripping decimal as
  "924444500.0" — a different decimal that maps to the same f32 — and ron
  serializes exactly that.
• Re-parsing "924444500.0" no longer fits f32, so ron falls back to
  F64(924444500.0) — the value has drifted 924444480 → 924444500.

Same missing-suffix root cause as the number-narrowing note, but here the
numeric value itself changes across one round-trip. Still fidelity, not
soundness. Sharing the reproduction in case it's useful.