Verify the landing queue

verification/landing-queue/LandingQueue.tla and the sibling modules beside it are a hand-written TLA+ model of the landing queue and its path leases. TLC checks the model inside a stated bound.

TLA+ checks the model. It does not read the Python. A rerun of an unchanged model passes after a real code regression, with the same state counts. A passing rerun alone does not show the model matches the current code.

Before a passing run counts, and before Verified at moves, compare each affected action and its helper assumptions with the changed code and update the model to match. Start from the diff, not from the table. Run git diff --stat <Verified at> ..HEAD -- t3/added/landing/scripts/landing_lib/ and read every changed function against its action before you run anything. A function can change behaviour without moving a transaction boundary and without appearing in the table's right column.

Read every result with the pstack /statechart skill. It turns an invariant violation into the shortest path to it in plain words, and draws the state graph when nothing breaks. Use it rather than reading tlc.out yourself.

Does my change touch the verified code?

Compare the model and run the check when a change touches any of these, in t3/added/landing/scripts/landing_lib/.

These actions stand for an actor and not for our code, so read them when an assumption about that actor changes.

ReleaseThenSettle stands for no code. It is the broken order behind one variant.

The model also leans on helpers. These are foundation.overlaps, foundation.covered, foundation.fingerprint, and Store.tx. It assumes overlap is intersection over atomic paths, coverage is a subset test, a fingerprint is equal exactly when a replay carries the same change, and a transaction is all or nothing. A change to any of them can invalidate a promise without moving a transaction boundary. So can a change to the values land.py passes to these functions. Message-only changes do not need this comparison.

If the change moves a transaction boundary, adds or removes a Store.tx(), adds an external call between two transactions, or changes when the queue lock is taken, the model needs updating even when the table does not name the function. Say which transaction moved.

Run it

One command, from the repository root:

python3 skills/landing/scripts/land.py slot -- python3 verification/landing-queue/check.py --scratch-parent <parent>

--scratch-parent is required and has no default. It takes the machine's scratch directory, the one a brief or the restaurant's scratchDir names. Any existing writable directory works, so when neither names one, make one with mktemp -d and delete it afterwards. check.py creates a new directory under the parent for each config's TLC state and deletes that directory, by its exact path, when TLC exits. With the argument missing it prints a usage error naming --scratch-parent and runs nothing.

It runs five base configs and every config in variants/, and exits 0 only when each answers what the model says it should. It prints one row per config with the states generated, the distinct states found, the deepest level, and the wall time.

Bounds. TLC explores with one worker in breadth-first order. Depth is 12 in leases.cfg, 30 in publish-one.cfg, 32 in merge-one.cfg, 24 in publish.cfg, and 18 in merge.cfg. Each variant sets its own depth. The bound is enforced in Next, and there is no CONSTRAINT, so no violation is reported past Depth. leases.cfg, publish-one.cfg, and merge-one.cfg run out of new states before Depth. publish.cfg and merge.cfg stop at it. What is left out is listed in verification/landing-queue/README.md under "What the check does not cover".

A base config must report holds. A variant must report breaks <invariant> with the invariant its EXPECT: line names. A variant's result counts only while every base config holds. When a base config breaks, the variants that name the same invariant may be breaking through that bug rather than through the rule they remove, and check.py cannot tell the difference.

Tell a real bug from a modelling error

The model is written by hand from the code, so it can describe the design and miss the code. Before you report a bug, check these in order.

1. Does the model's action match the function the map in the model's header names, line for line? A missing guard, a guard in the wrong order, or two transactions folded with no reason in the map is a modelling error. Fix the model, then re-run.
2. Is the counterexample a sequence the code can really produce? Read each step against the function it names. A step the code cannot take is a modelling error.
3. Only then is it a bug in the code. Do not weaken the invariant to make it pass and do not change landing_lib/ to match the model. Write the counterexample as a numbered list of steps in the code's words, reproduce it in a throwaway repository and store, and file it as Correctness: or Safety:.

A variant that reports holds is a modelling error in the variant. A base config that reports breaks is a finding against the code, or a modelling error, decided by steps 1 and 2.

When the change is intended

1. Read the code at the new commit, the action that covers it, and the helper assumptions above.
2. Update the action so it still stands for one transaction or one external call, or say in the map why a fold cannot change a promise. If a guard moved, move it. Keep a check's pass or fail outcome in the model even when the code stops acting on it. The failure comes from outside the program, and dropping it deletes the case that proves the promise.
3. If a promise changed, update verification/landing-queue/README.md and the model's promises section together, and add or change a variant in verification/landing-queue/variants/ that shows the new promise failing when its check is removed. A promise with no failing variant is unproven and belongs in the report as a gap.
4. Run the check. Every base config holds and every variant breaks its own invariant.
5. Move Verified at below to the new commit, and only after steps 1 to 4 pass.

Coverage record

• Model: verification/landing-queue/LandingQueue.tla and its sibling modules, configs beside it and in variants/.
• Runner: verification/landing-queue/check.py.
• Verified at: 91251ca92. Each action was compared with the code at that commit.
• Last full run: 21 runs, every base config held and every variant broke its named invariant, in 2m48s through the slot, with the config rows adding up to about 168 seconds. States generated and distinct: leases 133,513 and 7,714; merge-one 6,140,551 and 816,762; merge 4,570,849 and 898,400; publish-one 6,408,995 and 631,184; publish 2,668,895 and 633,592.

Before advancing Verified at, compare every affected action and helper assumption with the changed code. Update the model to reflect changed guards, outcomes, and transaction boundaries, then run the check. An unchanged model can pass after a code regression. If the check fails, work through "Tell a real bug from a modelling error".

For the reverse case, a change to verified code that never updated the model, see the /maintain-formal-verification-skill skill.

Known limits

The search is bounded, and a pass covers the modelled actions and nothing else. Git and GitHub are modelled as external actors, along with the clock and other writers on trunk, so the model holds only as far as those actors behave as its actions say. The model drifts unless someone compares it with changed code and updates it. Verified at records that comparison. Rerunning an unchanged model cannot detect drift by itself.