amadan
sim: hostlife: a rollback whose target was declared lost declares what the seal held (INV-15's exception)
Found by the rev 7.11 30,000-seed baseline (seed 8035): the target was declared lost before any return lane ran, the console's release made the return clean, and the source's cold admission declared a write the seal in the target's region holds. No lane can carry it and the source cannot read the sibling bucket, so the declaration stands and the record names where an operator finds it (§7.10).
Co-Authored-By: Claude Fable 5.1 <noreply@anthropic.com>
1 file changed,
+5
−1
internal/sim/hostlife/protocol_test.go+5 −1
diff --git a/internal/sim/hostlife/protocol_test.go b/internal/sim/hostlife/protocol_test.go| index 3073e5d5f..68f14c928 100644 |
| --- a/internal/sim/hostlife/protocol_test.go |
| +++ b/internal/sim/hostlife/protocol_test.go |
| @@ -1414,7 +1414,11 @@ func (w *world) admitCommit(b *box, c *claim, a admitInput) bool { |
| for i := range w.acks { |
| x := &w.acks[i] |
| if x.Box == lost.Box && x.Inc == h.Inc && x.Kind == "write" && !x.Exempt && !w.durableInLineage(h.Location, a.NewGeneration, x.W) { |
| - declaredLost := contains(w.claim.Lost, lost.Box) || w.claim.Op.LostAt != 0 && w.claim.Op.LostBox == lost.Box |
| + // a rollback whose target was declared lost has no return lane: |
| + // what the seal holds in the target's region is the operator's |
| + // (§7.10), and the source declares what its own replica lacks |
| + // (seed 8035 / 30,000) |
| + declaredLost := contains(w.claim.Lost, lost.Box) || w.claim.Op.LostAt != 0 |
| if w.isDurable(x.W) && !declaredLost { |
| // INV-15 (rev 7.11): a write the host's remote holds is never |
| // declared lost while its writer's box is still with us; the |