Opus 4.7 uses Apalache to search for inductive invariant candidates, then proves main theorem with TLAPS

[lemmy]

Full TLAPS safety proof for tcp.tla

This PR adds a complete, machine-checked safety proof of the abstract RFC 9293 TCP state machine in specifications/tcp/tcp.tla. The original spec is not modified — every obligation is discharged in two new files.

Result

Top-level theorem	THEOREM SpecImpliesInv == Spec => []Inv
Strengthening	THEOREM SpecImpliesIndInv == Spec => []IndInv
Proof obligations	4540 (all proved by TLAPS, 0 OMITTED)
tcp_proof.tla size	5665 lines
Backends used	Z3, Zenon, Isabelle/TLA+, PTL

Inv is the existing two-peer "both queues empty implies same EST status" invariant from tcp.tla; IndInv is a 6-clause auxiliary strengthening discovered with Apalache and ported back to TLAPS.

Files added

• specifications/tcp/tcp_proof.tla — full TLAPS proof
• specifications/tcp/IndInv_apa.tla — Apalache module used to discover IndInv
• specifications/tcp/IndInv_apa.cfg, IndInv_apa_init.cfg — Apalache
  configurations for Init => IndInv and IndInv /\ [Next] => IndInv'

Approach (3 phases)

Phase 1 — Static obligations (commit 1758f209)

Started with the obligations that don't require an inductive strengthening:

• TypeCorrect == Spec => []TypeOK (~268 obligations) — refactored into a
  reusable TypeOKInductive lemma to keep the top-level theorem tractable.
• InvInit == Init => Inv — direct from the initial-state predicate.
• Added two generic helper lemmas PrefixOneNonEmpty and PrefixTwoNonEmpty,
  derived from the unfolded IsPrefix definition, used throughout the rest of
  the proof to chain Tail/Append through Seq(Msgs).
• Added an explicit ASSUME PeersFinite == IsFiniteSet(Peers) (the spec's bare
  Cardinality(Peers) = 2 only implies cardinality, not finiteness, in TLA+).
• Proved PeersAB and InvIsAB to enable explicit two-peer reasoning.

After phase 1, the remaining obstacle was the inductive stepInv /\ [Next]_vars => Inv', which is not inductive on its own — the spec needs auxiliary invariants correlating connection states with queue contents.

Phase 2 — Discovering IndInv with Apalache (commit b47fe66c)

Built a dedicated Apalache module IndInv_apa.tla (extends tcp via
INSTANCE):

• Replaced the unbounded TypeOK with TypeOKBounded + BoundedNetwork
  (Len(network[p]) <= MaxLen with MaxLen = 4).
• Defined IndInit (havoc state subject to IndInv) and NextBounded.
• Iterated:

    apalache-mc check --length=0 --init=Init    --inv=IndInv  IndInv_apa.tla   # base
    apalache-mc check --length=1 --init=IndInit --inv=IndInv  IndInv_apa.tla   # step

• Each counterexample (~26 in total) produced a refinement of one auxiliary
  clause. Several intermediate candidates (Aux_RST_head, Aux_q_PostEst,
  Aux_FIN_handshake_predecessor, Aux_SR_q_EST_has_ACK) had to be discarded
  as over-restrictive: they excluded reachable Inv-respecting states where
  Inv was only vacuously true.

The converged invariant has 6 auxiliary clauses on top of TypeOK /\ Inv:

• Aux_singleton_RST — if n[p] = <<"RST">> and n[q] = <<>>, then connstate[q] # EST.
• Aux_singleton_ACK — if n[p] = <<"ACK">>, n[q] = <<>> and connstate[p] = SR, then connstate[q] = EST.
• Aux_singleton_ACKofFIN — if n[p] = <<"ACKofFIN">>, n[q] = <<>> and connstate[p] in {FW1, CLOSING, LA}, then connstate[q] # EST.
• Aux_EST_evidence — if connstate[p] = EST, then either connstate[q] has reached a post-EST state or some handshake message (SYN, ACK, SYN,ACK, FIN,
  ACKofFIN, RST) is still in n[p] or n[q].
• Aux_LastMsg — for each connstate[q] in {SR, FW1, CW, LA, CLOSING, SS}, LastMsg(n[p]) is pinned to the message q appended on entry to that state (e.g. q = SR pins it to "SYN,ACK").
• Aux_RST_at_end — if LastMsg(n[p]) = "RST", then connstate[q] in {TIME-WAIT, CLOSED, LISTEN}.
  Apalache established (with MaxLen = 4, Cardinality(Peers) = 2):
• Init => IndInv in ~5 s
• IndInv /\ [Next]_vars => IndInv' in ~70 s

Apalache established (for MaxLen = 4):

• Init => IndInv in ~5 s
• IndInv /\ [Next]_vars => IndInv' in ~70 s

Phase 3 — Unbounded TLAPS proof of IndInv (commits 5c821be … 201a14f)

Translated the bounded Apalache result into a fully unbounded TLAPS proof,
proceeding one action at a time so each commit ran TLAPS to completion:

Action(s)	Commit	Pattern
IndInvInit, IndInvStutter	5c821be	direct
5 user actions (no-network-change + append-only)	cb290c8	append m to n[remote]
8 user actions (all of User)	9e201fd	same
TimeWait, Closing	006cbff	TimeWait: no network change; Closing: tail-only
LastAck	881d857	tail-only
Note3 send (Reset)	2e27b5a	append-only
Listen	ac749ed	tail + append
Established	246e0f6	tail + append, post CW ∈ PostEst
FinWait2	61d2b21	tail + append, post TW (vacuous on covered states)
Note3 RST receive	1ed3985	tail-only, q=local case-split on n[local] = <<RST>> vs Len ≥ 2
Note2	e1cdcb1	SubSeq(_, 3, _) consume 2 + append
FinWait1 (FIN, ACKofFIN)	374cafb	two sub-cases mirroring Established and Note3 RST
SynSent (SYN, SYN,ACK)	0c7cba3	two sub-cases — sub-case (b) transitions into EST
SynReceived (RST, ACK)	0a1ae9b	two sub-cases — sub-case (b) transitions into EST; ~700 lines
SpecImpliesIndInv, SpecImpliesInv	201a14f	PTL closing

The "transitions into EST" subcases in SynSent and SynReceived were the most subtle — Aux_EST_evidence' requires a case-split on Len(n[local]) and on whether n[remote] is empty to dispatch the disjunction.

Notes / lessons

• A reproducible internal tlapm crash (src/expr/e_levels.ml: Assertion failed) is triggered by WITNESS Len(network'[p]) \in 1..Len(network'[p]). Workaround: replace the witness with the literal value Len(network[p]) + 1 (which TLAPS can prove lies in 1..Len(network'[p]) from the Append length identity).
• Many "obviously true" structural invariants were rejected by Apalache as over-restrictive. The minimal six-clause IndInv is meaningfully smaller than the first plausible candidates.
• Each per-action sub-proof follows the same skeleton (USE/SUFFICES/CASE on q, then on p), which makes future maintenance and review tractable despite the file's overall size.
• TLAPS runtime per action ranges from ~6 min (no-network actions) to ~25 min (SynReceived); the cumulative full-rebuild time is ~3 hours.

[lemmy]

@muenchnerkindl This might interest you as well