nootxlm/reset-certificate

The Reset Certificate

Was that episode a fresh trial — or was it still wearing the last one?

Every benchmark number rests on a reset. If state carries over, the next measurement is partly a memory of the last — and a policy can look steadier, calmer, and safer than it is.

This instrument settles that by measurement. It walks the rig itself, discovers every home of state, runs an episode, resets the way your harness resets, and names whatever the reset failed to restore. What it cannot read, it prints. What it cannot measure, it says so beside the verdict.

That matters where decisions follow the numbers: a lab deciding a policy is ready, a facility trusting a robot beside residents, an insurer asking which exact policy ran and whether its evaluation was clean, a buyer checking that a used robot truly arrived in its factory settings.

One reset, a sequence, or a whole fleet — each judged against its own fresh reference, each with its own verdict, limits on its face.

A certificate does not ask to be believed. It asks to be re-run.

Files

• cert.py — the verifier core (snapshot, anchor, diff, echo classification, verdict classes, and the sequence judge). Harness-agnostic.
• ADAPTER.md — how to point the instrument at your own harness: the environments the two paths need, the twelve-member Rig interface, and the anchor wiring.
• mdk.py — the Microduck adapter + CLI (worker / run).
• stub.py — a second, stateful policy shape used as a test rig.
• jstub.py — the jittered stub: the same shape with non-determinism injected into its stepping (the STATE-CLEAN live attempt).
• tests.py — the instrument's own tests: python3 tests.py.
• LICENSE — MIT, the package's own licence.
• requirements.txt — the verified environments, transcribed from ADAPTER.md.
• plant/ — scratch copy of the BAM package carrying one planted third write (the falsifier). Never a shipped tree.
• plant_fuse/ — scratch copy of the BAM package carrying the horizon fuse: a counter no reset restores, arming a write only from the second reset onward. Never a shipped tree.
• proof/ — every leg's saved output.

Run it

Against any microduck_rl checkout (the anchor build runs as a separate process on its own):

python3 mdk.py run --tree <checkout> --reset <mode> \
    --seed 7 --declare-commands

Reset modes: naive (mj_resetData alone), full (the patched contract: reset_episode + reset_action_history), eponly, nonestate, noclock. Add --plant

to judge a harness whose stepping carries a planted write. Add --no-trace for a diff-only run (earns at most STATE-ONLY). Add --episodes N (N > 1) to judge the reset at every boundary of an N-episode sequence instead of a single transition: cumulative state whose effect lands beyond one episode (a slow charge, a counter with a long fuse) is re-judged at each reset, and an INERT classification earned at one boundary expires at the next. The sequence judge restores nothing mid-sequence — the single judge's echo restore test would launder the state the next boundary must judge — so a diverged boundary names its differing fields as pre-echo leaks, and echo separation runs once at the end as a post-sequence classification pass over one further reset (naming refined, the sequence verdict untouched).

Against a fleet — many devices judged in one run:

python3 cert.py fleet --devices 12

certify_fleet judges each device independently against its own fresh reference, in the one run: every device earns its own full verdict with its leaks named, a device whose build raises is recorded ERROR while the fleet judges the rest, and the run closes with a fleet summary — the device count, the verdict counts, and the wall time of the whole run. The sequence judge is available per device as an option. A fleet verdict is exactly the per-device verdicts and nothing more: no device inherits another's result, and the summary claims no horizon wider than each device's own printed profile.

Against the stub's second policy shape:

python3 stub.py run --variant clean|leaky

Against the jittered stub (the STATE-CLEAN attempt — genuine non-determinism in the stepping, so the verdict rests on the measured final-state deviation):

python3 jstub.py run --jitter J     (J=0 is the control)

Verdict classes

• BIT-IDENTICAL — discovery diff empty, and a 750-step dynamically excited trace matches a fresh rig bit for bit.
• STATE-CLEAN — diff empty, trace hash differs but the final state lands within the stated tolerance (1e-6) of fresh, deviation measured and printed. The tolerance is measured on the final state, not along the trace path.
• STATE-ONLY — diff empty, no trace leg ran. Weaker; says so.
• FAIL — differing fields named, each classified leak or echo (an echo clears when the true write-set is restored).

Differing fields the judged episode provably did not read — the trace matched fresh bit for bit with them standing (diagnostics, high-water marks, visual state) — are printed as INERT on the certificate: named, with the operational evidence, never silently dropped and never counted as leaks. When the trace diverges, attribution is impossible and every differing field stays a leak. The discovery walk covers array and scalar attributes — an owner's own and its class's alike — and descends into struct sub-objects two levels; struct lists (contacts, solver, timers) and anything deeper are printed as opaque handles. Methods are not state and are the walk's one stated exclusion. Episode seeds are parameters (--ep-seeds on the CLI), not constants.

• REFUSED-AT-ANCHOR — two independent builds disagree at episode start; the differing fields are named and no reset is judged. Construction-time RNG draws land here.

No class is ever upgraded silently. A snapshot is provenance-stamped (model hash, harness, step count, sim time) and refused once the rig has stepped; certifying without one is an error, never a default. Per-episode state the design intends to vary is DECLARED with its sampler and reported as declared — undeclared differences are leaks by definition.

Every certificate also prints beside its verdict: the judged profile (episodes × steps × episode seeds — the horizon the verdict actually covers); the part of the final state its deviation cannot measure (fields captured as tokens only — RNG stream states, byte strings, object arrays — whose final tokens differ are printed as not measurable by count and name, never silently scored as zero deviation; the deviation itself is measured over the union of the two final states, so a field that exists on one side only is priced — as an unbounded deviation, when its value was captured, and named beside the deviation — or named with the token-only fields, never invisible; a difference the arithmetic cannot order — a NaN on either side, infinity met by infinity, or an exact magnitude no float can carry — is likewise never scored as zero: its field is printed as not measurable in full, the elements of it the arithmetic can order are priced and printed beside the name, and the deviation prices as unbounded; integer differences are measured in exact arithmetic wider than the field's own dtype, so none wraps or is erased, and a field whose two sides disagree in kind — integer against float — is priced element for element in exact rational arithmetic, the integer side never converted into the float dtype, so none is erased at the seam between kinds either; complex differences are measured by the exact modulus of the difference — the squared modulus is an exact rational, zero only when the two values are equal, and only the worst element's modulus is converted — so a difference carried purely in phase prices at its true modulus, never at zero; the exact measurements walk a field's elements in turn (measured on the house rigs: integer roughly 0.2–1.6 microseconds per element, mixed roughly 6–17, complex roughly 22–35; linear in the field's size), and all of these names print whether or not the traced episode diverged); on rigs whose walk records opaque handles, the limit of the naming promise (those contents are identity-checked only; a write inside one cannot be named, only detected as a verdict change where the judged horizon reaches its effect — the limit is evaluated over the snapshot, the post-reset state, and the final state, so a handle an episode itself creates is disclosed in the run that judged it); and, on a FAIL that names no field, a line saying the measured divergence is carried outside the walked state — an unnamed FAIL is a reachable output, and the certificate explains it in the same breath as the verdict instead of leaving it bare. That line stands down when the deviation has already named a field that carries the divergence (a one-sided field priced unbounded, or a difference the arithmetic cannot order); a token-only naming does not stand it down.

Standing practice — the words are re-derived with the code

Every instrument change ships, in the same pass, with a re-derivation of the words that describe it: CONTRACT.md and the staged follow-up post are re-read against the new outputs, clause by clause and claim by claim, and corrected where the change moved what they may say. The code has a regression battery (tests.py, re-run after every change); the words have this step. Twice in a row — rounds 2 and 3 — the standard's page and its staged send were found one change behind the instrument, because each was verified against the code as it stood when its own lane read it and a parallel change invalidated the check in silence. A round is not closed while the words trail the code.