[topeuph-ai]

Adds specifications/StaleViewShrink: a coordinator-free "leave only if R remain" protocol (l-mutual inclusion, the mirror of k-exclusion) in which each node acts on a view of the world up to L ticks old. It compares a lowest-ID tie-break with a "patient lowest" rule.

model	result
StaleShrink.cfg	no error (Safety and Progress)
StaleShrinkV6Wait2x.cfg	no error
StaleShrinkV3Cascade.cfg	Safety violated: TLC finds a staggered cascade that breaks the tie-break
StaleShrinkV6TooShort.cfg	Safety violated: control, with the wait shorter than the staleness

Why it may be instructive: an atomic-read model of the same protocol passes the broken rule, and even a bare re-check with no tie-break. Modelling staleness explicitly is what exposes the cascade.

All models run in under 30 s (1–23 s single-worker). Checked locally with check_manifest_schema.py, check_manifest_files.py, check_markdown_table.py and check_small_models.py (TLC 2.19). manifest.json was written by hand: generate_manifest.py would not run on Windows (tree_sitter Language() overflow). Licence: Apache-2.0, as in the source repository (https://github.com/ValiChord/polite-shrink), which also has a Python checker that agrees with every verdict here and a Rust implementation.

Written by Ceri John with AI assistance (Claude, Anthropic).

🤖 Generated with Claude Code

[muenchnerkindl]

Thank you for your contribution. At this point, I haven't run TLC yet, but I have a few questions concerning the motivations and the specification.

[muenchnerkindl]

Can you give (here and/or in the TLA+ module) some references to where the problem and the algorithm come from? It strikes me that time is assumed to be global for all nodes, which is not a standard assumption is distributed computing.

[muenchnerkindl]

Rename l-mutual inclusion to R-mutual inclusion? Also because you have an (upper-case) L below.

[muenchnerkindl]

Perhaps point out that TLC will check for all (type-correct and bounded by L) values of lag, otherwise one may wonder why it is not a CONSTANT parameter of the specification given that it never changes.

[muenchnerkindl]

Stylistically, I suggest moving TypeOK further up in the module, right after the variable declarations: this helps fixing the mindset of readers. More importantly, it should include a conjunct for every declared variable (lag and recent are missing).

[muenchnerkindl]

Perhaps note that t >= lag[n] ensures that Len(recent) - lag[n] + 1 is a valid index into recent.

[muenchnerkindl]

Explain what eff represents.

[muenchnerkindl]

This is a global action – stated differently, it is taken synchronously by all nodes, given that they all share the same global time. Its definition makes use of the global system state, rather than the local views of each node. I would appreciate seeing an explanation in which sense it still can be understood as each node taking a step based on the information that is available to it alone: obviously, the problem has a much simpler solution in a centralized solution where full information is available.

[topeuph-ai]

Thanks for the review. I've restructured the spec along those lines in ddc7240.

The problem comes from dynamic storage-arc sizing in Holochain's kitsune2 DHT (holochain/kitsune2#160). The rules, with a Python checker and a Rust implementation, are in ValiChord/polite-shrink; as far as I know they aren't published elsewhere. The closest literature I found is Kakugawa, "Mutual inclusion in asynchronous message-passing distributed systems", JPDC 77 (2015), and Kamei & Kakugawa, arXiv:1807.05674, whose solutions use quorums and permission messages. Both are now cited in the README and the module header.

On global time: each node now acts in its own steps, Announce(n) and Recheck(n), reading only its own variables and a snapshot published between 1 and L ticks earlier. Time is an explicit clock now, advanced by AdvanceTime once every due re-check has happened, following Abadi and Lamport. Nodes never read now; it stands for two assumptions, that information is at most L ticks old and that a node's timer fires after D ticks. So the model is synchronous rather than asynchronous, and the rule depends on that bound: a node deciding alone can only rule out that a holder it still sees has already left if it knows how old its information can be. A side effect is that the view's age is now chosen afresh at each re-check instead of being fixed per node, so the lag variable is gone.

I've also renamed it R-mutual inclusion (noting the l- name used in the literature), moved TypeOK after the variables and made it cover all of them, and added comments on the snapshots index and on eff.

The verdicts are unchanged. Both V6 models pass, now with 16,848 and 43,348 distinct states (previously 65,001 and 245,146, since view ages are no longer part of the state), and TLC still finds the same descending-ID cascade for V3 and fails the short-wait control. The 3–5 node configurations I tried earlier agree, every model runs in under 3 s, and the manifest, table and small-model checks pass locally.