Skip to content

walker_sim: #824's safety justification is false as written, and the skipped-bucket exemption's rationale applies equally to a gated bucket #830

Description

@djhenry

Split out of the round-2 review of #824 (fix for #805). Both items are non-blocking — the reviewer
approved and I merged over them — but both are false-or-undisclosed sentences in a tracked file,
which is the defect class this project keeps rediscovering.

1. The replacement universal at tests/walker_sim.rs:871-872 is false as written

#824 replaced a claim about the old terminal-only check with a new one about the per-zone gate:

a per-zone refusal … could never fire where the terminal one would not

That is false. assert!(tot_walked > 0) at :810 precedes the terminal completeness assert at
:828. An all-unmeasured run (or an all-skipped one) dies at :810, so :828 never runs
— while the new per-zone gate does fire. There is a real case where the per-zone refusal fires
and the terminal one does not, which is exactly what the sentence denies.

The intended property — that the per-zone gate introduces no new false positives — is true.
The reviewer confirmed it independently: the hole Vecs in water_grid.rs are push-only, so a
zone that the per-zone gate refuses is one the terminal check would also have refused had it been
reached. Only the sentence is wrong, and a one-clause fix ("except where an earlier assert aborts
the run first") restores it.

Why this matters beyond pedantry: the sentence is a justification for the new gate's safety.
An agent or a future author reading it would conclude the gate cannot change which runs fail, and
that conclusion is load-bearing for anyone deciding whether to weaken the earlier asserts.

2. The skipped exemption's rationale applies equally to a bucket that IS gated

tests/walker_sim.rs:874 exempts the skipped bucket from the gate, on the grounds that a
skip is the COMMON state of a partial $ZONE_DIR. By the doc's own #762 exhibit, that rationale
applies just as well to unmeasured — and unmeasured is gated.

The asymmetry may well be correct (a skip and an unmeasured zone are not the same fact about the
world), but the doc gives one reason and applies it to only one of the two buckets it covers,
without saying why the other is different. Either the rationale needs the distinguishing clause,
or the exemption needs re-deciding.

Scope

Doc/comment work in one file, plus whatever the second item's re-decision implies. No production
code is implicated: the reviewer attacked the gate with nine mutations and broke none of the
behaviour.

Filed as a follow-up rather than blocking #824, per the review-cost policy: a finding that does
not change what the code does becomes an issue and the PR merges.

Metadata

Metadata

Assignees

No one assigned

    Labels

    agent-honestyClient reports success or state that is false — a lie an agent cannot detect

    Projects

    No projects

    Milestone

    No milestone

    Relationships

    None yet

    Development

    No branches or pull requests

    Issue actions