Skip to content

spec: compare the tics before a refused one in native diff #540

Description

@MarcusKainth

What broke, or what became impossible under the current contract

NATIVE.md §7 says native diff stops at the first refused tic "before any
field is compared". Read literally, that is what the driver does, and the
consequence is that a run whose span contains a refusal compares nothing at all
while reporting exit 3 and a message naming a tic and a bit, which reads as a
clean result up to that point.

So every run on a branch that refuses is a check that never ran. That is not a
theoretical reading. On #517's branch, which moved demo3's first refused tic
from 181 to 210, native diff 215 reported the refusal and native diff 209
reported a field differing at tic 206. Both runs walked through 206 and produced
the same wrong row. The divergence is #502, and it sat behind seventeen green CI
checks, a passing sim_parity_live and a passing native_diff_live, because
none of them compared a field. It surfaced only because a differential needed
both sides to stop at the same tic, so the span asked for was 209 rather than
the usual 215.

The tics before a refusal are not in doubt. Their rows are in the table and the
statement produced them exactly. Only the refused tic itself is the one the
contract has a reason to exclude. The current sentence excludes all of them.

Filed as #534. Implemented in #539, which carries this contract text so the two
move together; that PR waits on this decision.

Proposed contract text

--- a/NATIVE.md
+++ b/NATIVE.md
@@ -176,9 +176,10 @@
 its bits named in `sim::unresolved`; `native_state.unimplemented` says the
 level itself carries a path native mode does not model, decided once when
 the level loads, with its bits named in `sim::unimplemented`. `native diff`
 reads both columns for every tic it ran and stops at the first tic either
-sets, before any field is compared, with exit 3 and a message naming the tic
-and the bits. `native demo` and `native play` stop at the same tic rather
-than drawing past it.
+sets, with exit 3 and a message naming the tic and the bits. The tics before
+it are compared, and a field differing there is what the run reports instead,
+with the refusal named as where it stopped. `native demo` and `native play`
+stop at the same tic rather than drawing past it.

What has to change if this is ratified

  • driver or render

Migration

Not breaking, so driver: rather than spec!:. The state row, the tic, the
frame and the resident statements are untouched, and no value the simulation or
the renderer computes moves. What changes is which tics the driver compares and
what it prints.

Nothing has to change in order. #539 is one commit carrying the contract text
and the behaviour together, so the tree is never in a state where NATIVE.md
and the driver disagree. The exit codes a caller scripts against are unchanged:
0 when the compared tics agree and nothing refused, 3 when a tic refused or a
field differs.

The one visible difference for an existing caller is that a run which refuses
may now report a field instead of the refusal, where before it always reported
the refusal. That is the point of the change, and it can only turn a silent pass
into a named divergence, never the reverse.

Activity

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Metadata

Metadata

Assignees

No one assigned

    Labels

    area: specSPEC.md, PURITY.md, and the crate that encodes their constantsneeds: maintainerWaiting on a maintainer. SPEC and PURITY changes always arespec-changeA proposed change to the SPEC.md contract. Maintainer gated

    Projects

    No projects

      Milestone

      No milestone

      Relationships

      None yet

      Development

      No branches or pull requests

      Issue actions