fix(protocol): refuse merging notices cut for different shapes; correct the evidence (improvise-z2vr)

Co-Authored-By: Claude Sonnet 5.5 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_01VdfEGXA7aJ6ftMsCc9PJze
This commit is contained in:
Claude (dbsp-delivery)
2026-10-10 20:25:23 -07:00
committed by Edward Langley
parent 69fb5e625e
commit 3378d3d48a
4 changed files with 29 additions and 8 deletions
+13 -4
View File
@@ -202,8 +202,11 @@ swap's notice delivered three steps late, an old reply replayed). The client had
the generation-1 notice arrived: `seen` was rewound into generation 1, a notice from the same history set
`restructured`, and the window correction that answered was covered by the watermark, so it never cleared
the mark and `poll` retried until `Exhausted`. The test replays the history step for step, with the
property's own weather and a Flaky edge. Rival: the notice-ignore test in `accept` disabled; this test
and the random property fail. The seed file is not committed (`proptest-regressions/` is ignored).
property's own weather and a Flaky edge. Rival at the time: the notice-ignore test in `accept` disabled;
this test and the random property failed. **Since the round-three change (a foreign notice only marks the
shape stale) nothing fails with that shortcut disabled**: it is an optimisation that saves one round, not a
correctness rule. The test still replays the seed. The seed file is not committed
(`proptest-regressions/` is ignored).
Run after the fix, the property passed 4 x 4000 cases and 2 x 20000 cases, with no third failure.
@@ -221,9 +224,15 @@ The same rewind, then an unsolicited covered correction: the duplicate branch se
below a queued entry, and each fetch for that `through` came back a duplicate. Failed on the head before
the change.
### a_notice_from_another_epoch_marks_the_shape_stale_and_moves_nothing_else
### a_foreign_notice_marks_the_shape_stale_and_the_home_hosts_answer_settles_it
The new rule itself: a foreign notice sets `stale`; the home host's next notice is still contiguous.
A foreign notice sets `stale`, and the home host's answer then settles the shape. It does not see `seen`
stay put (an answer heals it either way); route A and route B are what pin that.
### notices_cut_for_different_shapes_or_not_cut_do_not_merge
A merge of notices cut for different shapes, or a cut one with an uncut one, would keep one shape's
mark and make the other shape see a gap. `merge` refuses it. Rival: the `cut_for` comparison removed.
### a_pulled_notice_pushed_through_on_notice_still_reaches_only_its_shape