Add Vortex DSE specifications

[vasilisnasopoulos]

Adds specifications/VortexDSE/ — a deterministic slot-based admission
protocol with a separate per-slot agreement layer. A message carries its own
slot stamp and each node decides admission locally against its own clock;
there is no leader, quorum or vote.

Two admission modes, both specified because both are implemented.
Vortex_DSE_CSlot admits a late message into its own slot, so nothing is
dropped. Vortex_DSE_CSlot_TTL rejects it permanently, which bounds memory
behind the frontier. The difference is <= versus = in one conjunct.

Vortex_DSE_CSlot_AE (Freeze / Reconcile / Commit) is specified over the TTL
mode, not the default. Its NoReorderAcrossCslot invariant encodes the strict
gate, so it is not a refinement of the late-tolerant rule; extending it would
mean restating what "no reordering across slots" means, and I have not done
that here. The spec README says this rather than leaving it to be discovered.

Checked:

TLC models	6, all success, 0.6–3.3s
Vortex_DSE_CSlot_Proofs	194 obligations
Vortex_DSE_CSlot_ExactlyOnce_Proof	131 obligations
Vortex_DSE_CSlot_AE_Proofs	34 obligations

All three proof modules exit 0 under tlapm --strict and contain no OMITTED
steps. Model runtimes and state counts in manifest.json were measured with
check_small_models.py locally; check_manifest_schema, check_manifest_files,
check_manifest_features and check_markdown_table all pass.

Scope is deliberately limited: Vortex_DSE_CSlot_Skew states the bounded-skew
assumption structurally but does not model the mechanism that maintains it, and
Reconcile is a single atomic step rather than the multi-round protocol
underneath.

Two notes from preparing this, neither blocking:

• generate_manifest.py rewrites every spec's manifest.json, not only the new
  one; it produced diffs in 14 unrelated manifests, which I reverted. Only
  specifications/VortexDSE/ and the README table are touched here.
• check_proofs.py reads module['proof']['runtime'], but the schema requires
  maxRuntimeMinutes and sets additionalProperties: false. It raises
  KeyError: 'runtime' on any spec with a proof, including on a clean master.
  CI is unaffected because it invokes tlapm directly. Happy to open a separate
  issue or PR for it if useful.

[lemmy]

Isn’t it better if Apalache reports the name of the invariant that’s been violated?

[lemmy]

MaxSlot is a model-checking concern, so it doesn’t belong in the high-level specification. Instead, TLC should be used to box the state space by using state and action constraints.

[lemmy]

If any part of this commit was generated with AI assistance, please add a Co-authored-by footer naming the model to the commit message. AI use is permitted; we simply ask that it be disclosed for transparency.

[lemmy]

Two notes from preparing this, neither blocking:

• generate_manifest.py rewrites every spec's manifest.json, not only the new
  one; it produced diffs in 14 unrelated manifests, which I reverted. Only
  specifications/VortexDSE/ and the README table are touched here.
• check_proofs.py reads module['proof']['runtime'], but the schema requires
  maxRuntimeMinutes and sets additionalProperties: false. It raises
  KeyError: 'runtime' on any spec with a proof, including on a clean master.
  CI is unaffected because it invokes tlapm directly. Happy to open a separate
  issue or PR for it if useful.

@ahelwer ^^

[lemmy]

Careful when checking liveness properties under state- and action-constraints.

[lemmy]

nit: consider extracting strings like "up", ... into constants.

[lemmy]

Related: https://github.com/tlaplus/Examples/tree/master/specifications/FiniteMonotonic

[lemmy]

This and the constant MaxSlot should be pushed into one of the MC_...tla files.

[lemmy]

WF_ should be sufficient.

[lemmy]

This could be strengthened to <>[], but MaxSlot should be here anyway.

[lemmy]

Should this module refine the other (under some suitable refinement mapping)?

[vasilisnasopoulos]

Thank you — this was a more careful read than I expected, and the MaxSlot point was right.

MaxSlot is gone from all four specifications. Each now has an MC_ module that fixes the horizon inside the actions rather than through a CONSTRAINT, which also answers the liveness warning: no successor states are discarded, so the temporal properties are checked against a genuinely finite graph rather than a truncated one. There is no CONSTRAINT left anywhere in the directory. MaxSkew stays in the Skew module, since it is an assumption the protocol relies on rather than a checking artifact.

FiniteMonotonic was the useful pointer — the MC_ modules follow its shape.

Also done: WF_vars(Tick) now that the ticker is unbounded; TickProgress strengthened to <>[] in the MC modules, where the horizon makes it permanent; node states and AE phases named rather than written as bare strings; and AllInv dropped so a checker reports which invariant failed.

On refinement — a fair question, and the answer today is no.

The obstacle is not the admission rule. It is that Vortex_DSE_CSlot_AE does something neither core module can: NextCslot clears processed for every node at once at a slot boundary. In the core specifications processed only grows, except when a single node crashes and goes down. So AE behaviours are not core behaviours under any mapping that hides phase and committed_set. The two also model disjoint failure dimensions — the core has crash and rejoin, AE has neither, deliberately.

They are complementary views rather than stacked layers: the core is accumulation across slots under crash, AE is one slot's agreement cycle with a reset at the boundary. The README now says as much instead of implying composition.

A module that does cross-cut both is the right thing to have, and I intend to write it — but as its own contribution, with a proved mapping, rather than asserted here.

Seven TLC models, all under five seconds. The three proof modules discharge 191, 128 and 32 obligations and exit 0 under tlapm --strict.

[vasilisnasopoulos]

The macOS failure here is not from this change. EWD998_proof.tla hit its 4-minute wall in the shared proof step:

54195 Killed: 9  timeout --signal=KILL 4m ... EWD998_proof.tla

It proved fine in the other five jobs, the proof step runs sequentially so the modules added here do not compete for CPU, and they take about three seconds between them.

That budget is one I set in #218, and it is too tight — locally the proof takes 86 seconds, while the macOS runner needed more than 2.8x that. #221 raises it to 6 minutes.

[vasilisnasopoulos]

Added the Co-authored-by footer to both commits here, and to #221. Claude Opus 5 throughout — writing the module and README text, running the models and proofs, and preparing the manifest.

[lemmy]

Build problem appears to be caused by apalache-mc/apalache#3432 (comment)

[lemmy]

FWIW: https://github.com/tlaplus/vscode-tlaplus/blob/master/resources/knowledgebase/tla-review-guidelines.md might be useful for your agentic workflow

[vasilisnasopoulos]

The red here is not from this branch. master itself is failing all six jobs right now — run 31018433496 — for the same reasons:

specifications/GermanProtocol/APGermanData.cfg      expected success, got 1
specifications/FlashProtocol/APFlashWithMutex.cfg   expected success, got 1
Error: Could not create the Java Virtual Machine.

Apalache is not starting on the runners. This branch additionally hits smoke_test_large_models.py, where TLC reports SmokeEWD998.cfg: File not found although the file is present in the tree — a working-directory problem rather than a missing file.

Nothing under specifications/VortexDSE/ appears in either failure, and its own models and proofs pass in every job.

[vasilisnasopoulos]

Thanks for the guidelines link — I ran the specs against it and four things were not being followed.

Constants had no assumptions. All four specifications declared Nodes and MsgIDs with nothing constraining them, and Skew's MaxSkew with nothing saying it is a natural number. Named assumptions are in now. Worth having here in particular, since these modules carry TLAPS proofs.

Type invariants are back to the var \in S form — network \subseteq MsgRecord rather than a quantifier over its elements. MsgRecord ranges over Nat and cannot be enumerated, so the MC module carries a bounded MCTypeInvariant for TLC instead of the specification bending to suit it.

Strong fairness on Process is now justified by measurement rather than assertion. I tried weak fairness, as the guidelines ask: the liveness model reports a temporal-property violation under it, because a crash intermittently disables Process. That is recorded next to the definition.

One deviation, deliberate. The guidelines prefer a state CONSTRAINT over enablement conditions, and I moved the horizon into MCTick instead. I tried the constraint first and it does not work here: TLC evaluates invariants on the state that crosses the boundary before the constraint discards it, so with MaxSlot = 2 a Tick reaches current_slot = 3 and any invariant mentioning the horizon fails there. The reason is in the module header rather than left unexplained. Happy to be told there is a better way around it.

Seven TLC models, all under five seconds; the three proof modules discharge 191, 128 and 32 obligations and exit 0 under tlapm --strict.

[vasilisnasopoulos]

The refinement module is written and proved, on a branch stacked on this one. It keeps the core's variables, lets processed accumulate rather than clearing it at a slot boundary, and holds the per-slot input set in committed, so THEOREM Refinement == Spec => C!Spec goes through under the identity mapping — 25 obligations, exit 0 under tlapm --strict, and TLC checks it as a temporal property as well.

I will open it as its own pull request once this one lands, rather than growing this one further.

[lemmy]

master is green again

[muenchnerkindl]

I'm a little late to the party, but perhaps you'll find my comments helpful nevertheless.

[muenchnerkindl]

This action clearly subsumes Submit(id), why do you have both – in particular given that there is no fairness constraint on Submit?

[muenchnerkindl]

This is a direct consequence of the type invariant. I think you even have the stronger invariant
\A n \in Nodes : processed[n] \subseteq {m.id : m \in network}
which states that only sent messages are processed.

[muenchnerkindl]

NB: The invariant I suggested above is a consequence of this one.

[muenchnerkindl]

Why is this asserted only when the node is down? It should hold at all times?

[muenchnerkindl]

That's what I suggested above, and it immediately follows from NoFutureAdmission.

[muenchnerkindl]

This should rather be stated as network \in SUBSET MsgRecord. In fact, the semantics of TLA+ is such that this is not implied by the predicate asserted here.

[muenchnerkindl]

Cf. my comment to Vortex_DSE_CSlot.tla: this one is a direct consequence of the type invariant.

[muenchnerkindl]

Again, probably no need for this condition.

[muenchnerkindl]

Immediate consequence of CSlotLocalAdmission.

[muenchnerkindl]

If I'm not mistaken, the only difference to Vortex_DSE_CSlot.tla is that here equality is required whereas the other spec has <=. Therefore, all safety properties verified for the other spec also hold for this one. Moreover, the only liveness properties stated here are independent of the processing mechanism (and indeed, liveness for sent messages would not hold here because a message received late will not be accepted anymore). So, I wonder if this spec is of real interest?

[vasilisnasopoulos]

All of it applied — thank you, this was a much closer read than I had any right to expect.

The proofs. You were right that they collapse. NextType, NextSafe and NextStrictExactlyOnce were case splits where one BY DEF does the job, and StrictExactlyOnceCorrect was carrying the type invariant through as a conjunct instead of appealing to TypeCorrect, which is exactly the pattern you described:

	lines	obligations
Vortex_DSE_CSlot_Proofs	263 → 88	191 → 23
Vortex_DSE_CSlot_ExactlyOnce_Proof	295 → 131	128 → 19
Vortex_DSE_CSlot_AE_Proofs	60 → 36	32 → 10

Seven times more obligations than the argument needed.

Submit and DuplicateInject are now one Send. They differed only in preconditions nothing relied on, and with no fairness on either the split distinguished nothing — as you say.

The invariant sections. Each module now names the property of interest and marks the rest as following from it, rather than presenting a flat list that reads as more strength than is there. In the agreement layer I took the two facts you gave — ProcessedAreCurrentSlot and CommittedIsUnion — as the pair everything else derives from, with intermediate definitions as suggested. The corollaries stay defined and checked, but as regressions rather than claims.

PersistedReflectsReality — no reason at all; it holds unconditionally, verified, and the guard is gone in all three modules.

Skew. network \in SUBSET MsgRecord now, and thank you for being precise about why the quantified form does not imply it. The origin field was written and never read, so an adversary spoofing it changed nothing observable — it is removed rather than left looking like modelled adversarial power.

AE fairness — weak is enough for both, confirmed against the liveness model.

On the global current_slot: Vortex_DSE_CSlot_Skew is that weakening, with node_slot[n] per node and a bounded-drift tick. It is a sibling module rather than a refinement of the core, which is probably why it did not read as an answer to the point.

Seven TLC models and three proof modules, all green locally.

[vasilisnasopoulos]

You are right on both counts, and as written the module did not earn its place. Rather than argue for it, I have made it say the two things you pointed at.

The relationship is now proved, not asserted. Vortex_DSE_CSlot_TTL_Proofs establishes Spec => C!Spec: the strict mode refines the default one under the identity mapping, so every safety property of the default is inherited and none of it is reproved. Your observation that equality is the only difference is exactly what the proof turns on — and the type invariant is needed in precisely one place, going from m.cslot = current_slot to m.cslot <= current_slot, since that step needs both to be naturals. 34 obligations.

And the loss is now checked. MC_Vortex_DSE_CSlot_TTL_admission.cfg states EventualAdmission and registers it as a liveness failure, which is the point of the module: a message whose slot has passed is refused for good. That property holds under the default rule and does not hold here, so the difference between the two modes is a machine-checked fact rather than a sentence in a comment.

That, I think, is the only reason for the module to exist: not that the strict rule is interesting on its own, but that the pair makes the trade-off explicit. The default admits late messages and keeps eventual admission; the strict rule bounds memory and gives it up. Neither dominates, and now neither claim rests on prose.

If you would still rather the directory carried one admission rule, I am happy to drop it — the refinement proof would then move into the core module's README as a remark.

[muenchnerkindl]

Thank you, LGTM.

[lemmy]

"deterministic" doesn't seem to be needed here.

[lemmy]

What is “that structure”? Is it the “separate layer” or the part that has a very high-level characterization above?

In general, the README doesn’t help readers understand Vortex DSE’s conceptual functioning. Most of the other examples in this repository are accompanied by primarily academic publications. It would be beneficial for this example to also state the problem and how the solution works. The TLA+ specifications provide the formal proof that the solution solves the problem.

[lemmy]

Why not deep links?

[lemmy]

Since I lack the time to familiarize myself with Vortex DSE, I sought a review from a frontier model. Here’s the unfiltered response:

AI-based assessment: The specs model a meaningful but narrow component: local time-slot admission, duplicate filtering, abstract crash/rejoin state, and the difference between late-tolerant and strict admission. They do not yet model a meaningful consensus system. The project’s own public documentation similarly describes C-slot as a local admission predicate rather than consensus and says the admission-to-agreement system is not formally composed.

The core uses one globally visible network set and records only processed message IDs. It therefore does not represent separate per-node delivery state, selective loss or equivocation, conflicting payloads, within-slot ordering, or replicated application state. The agreement module’s Reconcile action atomically assigns the union of every node’s processed set to all nodes, so agreement is assumed by the action rather than established by a distributed reconciliation protocol.

The TTL model also never deletes network, processed, or persisted state, so its bounded-memory motivation is not actually modeled.

Recommendation: include it only if it is framed as slot admission plus idealized set reconciliation. Keeping the consensus protocol framing should require a composed model with per-node channels, loss/equivocation and crashes during reconciliation, persistent ordered history or state-machine effects, garbage collection, and end-to-end agreement, validity, and termination properties.

[vasilisnasopoulos]

You are right on every point, and the framing you quote is better than mine.

Where the overstatement came from. The specifications in this directory are one part of a much larger private set — a bit over a hundred modules and around a hundred and twenty model configurations, which between them cover the things you list as missing: per-node clocks and bounded skew, lossy delivery, equivocation and accountability, crash and rejoin composed with agreement, the timing layer that keeps the slot boundary. I chose to publish this part and keep the rest private, and then wrote the README as though it described the whole thing. That is how "consensus" ended up in the first sentence of a directory that does not model consensus.

I am not offering the private material as evidence — you cannot review what you cannot read, and a reviewer should not be asked to take a claim on trust. I mention it only because it explains the mistake, and because it is the honest answer to "what is that structure": it is the structure of a system most of which is not here.

So, for what is here: slot admission plus idealized set reconciliation. The README will say that and nothing larger.

The specific points all hold:

• One global network set. No per-node delivery state, no selective loss, no conflicting payloads for one id, no within-slot ordering, no replicated application state.
• Reconcile assigns the union in a single atomic step. Agreement is a property of that action, not something a reconciliation protocol establishes. I wrote as much in the scope note and then titled the module an agreement layer, which reads as more than it is.
• The TTL module never deletes anything, so bounded memory — the whole reason that mode exists — is not modelled. I added a liveness failure showing what the strict rule refuses, and left unmodelled the half that motivates it. That is the weakest thing I submitted.

On "that structure": the sentence pointed at nothing definite, and it is going.

On the README more generally — you are right that the other examples come with a paper and this one does not. I will rewrite it to state the problem, how the solution works conceptually, and explicitly what these modules do not cover, so a reader can tell what is proved and what is left open. I would rather that be plain than have someone infer a stronger result from one word.