CONVERGED is a hint, not a verdict: nothing runs a ring and its spec on the same inputs #3424

check_ring_spec_drift.py reports CONVERGED when every shared function has an identical signature, and carries a warning it earned:

ring-090 measured CONVERGED at 16 of 16 identical signatures and still disagreed with its spec on 126 of 1190 differential cases — the spec wrapped where the hand-written model saturated (#3420).

Only compiling and running both found it, and that harness was written by hand for one pair. Nothing generalised it, so every future CONVERGED pair would need the same manual work or would go unchecked.

What a generator has to get right

It must refuse, not skip. A harness that quietly covered eight of sixteen functions and printed "agree" would be worse than none: the eight it dropped are exactly where a difference can hide. Any parameter or return type it cannot synthesise or compare is named, and the run exits 2.

A panic is a disagreement, not a crash. Both calls run under catch_unwind with -C overflow-checks=on. Without it the process dies with no output at all, which reads as "no cases run" rather than as the sharpest difference there is — one module panicking where the other returns. A release build would wrap silently in both and hide it.

Structs are built by their producers. SimConfig and SimResult are constructed by calling a same-module function that returns them, driven by the same value grid. That needs no knowledge of their fields, which is how the hand-written harness did it.

Results

Controls, on the live pair and not only a fixture

Re-introducing the exact defect #3421 repaired — deleting the saturation guard from the spec — makes the tool report:

cases 936  agree 864  disagree 72
first disagreement: sim_time_ms

and exit 1. Restoring it returns to 936/936 and exit 0.

Its --self-check additionally proves two synthetic properties: two modules differing by construction are reported as disagreeing, and an unsynthesisable parameter type is REFUSED rather than passed over.

Stated limitation

ring-099s 25 cases are thin. Its functions take &mut [u8], &mut [bool] and &mut usize, and the generator passes zero-initialised buffers — the values are compared after the call, but the inputs are not varied. Real coverage there needs a buffer grid, and 25 cases should not be read as the same strength of evidence as 936.

One more thing the tool reports rather than does silently: it strips inner doc comments and inner attributes from the ring crate before including it as a module (55 lines for ring-090, 3 for ring-099), because include! inside a mod rejects them.