diff --git a/docs/backlog/P2/B-0179-fix-spineasyncprotocol-tla-counterexample-blocks-b1-ci-registration-2026-05-03.md b/docs/backlog/P2/B-0179-fix-spineasyncprotocol-tla-counterexample-blocks-b1-ci-registration-2026-05-03.md new file mode 100644 index 000000000..41804c836 --- /dev/null +++ b/docs/backlog/P2/B-0179-fix-spineasyncprotocol-tla-counterexample-blocks-b1-ci-registration-2026-05-03.md @@ -0,0 +1,48 @@ +--- +id: B-0179 +priority: P2 +status: open +title: Fix SpineAsyncProtocol.tla counterexample (blocks B1 → A CI registration; depth-9 trace dump on TLC run) +tier: formal-verification +effort: M +ask: Otto 2026-05-03 verify-then-claim sweep (#1397) — running TLC on the 4 deferred B1 specs from the math-proofs honest assessment (#1383) found SpineAsyncProtocol produces a TTrace dump at depth 9, indicating counterexample / invariant violation. The "deliberately skipped pending re-verification" framing in `docs/research/proof-tool-coverage.md` §2 was correct; this row tracks the actual fix. +created: 2026-05-03 +last_updated: 2026-05-03 +depends_on: [] +composes_with: [docs/research/2026-05-03-math-proofs-honest-assessment.md, docs/research/proof-tool-coverage.md, B-0180, B-0181] +tags: [tla-plus, formal-verification, spine-async, counterexample, b1, math-proofs-assessment, verify-then-claim] +--- + +# Fix SpineAsyncProtocol.tla counterexample + +## Symptom + +Running `java -cp tools/tla/tla2tools.jar tlc2.TLC -workers 4 -config tools/tla/specs/SpineAsyncProtocol.cfg tools/tla/specs/SpineAsyncProtocol.tla` produces a TTrace dump: + +``` +Trace exploration spec path: tools/tla/specs/SpineAsyncProtocol_TTrace_.tla +The depth of the complete state graph search is 9. +Finished in 00s +``` + +TLC dumps a trace file when it finds an invariant violation or a `run` that can't be satisfied. The depth-9 termination + 0-second run suggests TLC found a violation immediately (rather than exhausting state space). + +## Investigation needed + +1. Read the TTrace file to identify which invariant fails +2. Determine whether the invariant or the spec needs the fix: + - If the spec models the protocol incorrectly, fix the spec + - If the invariant is over-strong (asks for a property the protocol doesn't actually guarantee), weaken the invariant +3. Verify the fix locally — re-run TLC; expect clean "No error has been found" +4. Add `[] TLC validates SpineAsyncProtocol` to `tests/Tests.FSharp/Formal/Tlc.Runner.Tests.fs` +5. Add registry row to `docs/research/verification-registry.md` + +## Why P2 + +Pre-existing failure surfaced by verify-then-claim sweep, not a new regression. Blocks B1 → A in the assessment matrix but doesn't block any current functionality (the SpineAsync runtime works in practice; this is a formal-verification gap). + +## Composes with + +- B-0180 (CircuitRegistration config bug — sibling B1 issue) +- B-0181 (SpineMergeInvariants counterexample — sibling B1 issue) +- The closure of B1 → A in the math-proofs honest assessment requires all 3 sibling fixes to land diff --git a/docs/backlog/P2/B-0180-fix-circuitregistration-tla-config-bug-safety-invariant-undefined-2026-05-03.md b/docs/backlog/P2/B-0180-fix-circuitregistration-tla-config-bug-safety-invariant-undefined-2026-05-03.md new file mode 100644 index 000000000..30dd4863f --- /dev/null +++ b/docs/backlog/P2/B-0180-fix-circuitregistration-tla-config-bug-safety-invariant-undefined-2026-05-03.md @@ -0,0 +1,54 @@ +--- +id: B-0180 +priority: P2 +status: open +title: Fix CircuitRegistration.tla config bug — `.cfg` references invariant `Safety` not defined in `.tla` (blocks B1 → A CI registration) +tier: formal-verification +effort: S +ask: Otto 2026-05-03 verify-then-claim sweep (#1397) — running TLC on `CircuitRegistration` produces a clear configuration error rather than a counterexample; the `.cfg` references `INVARIANT Safety` but the `.tla` spec doesn't define a `Safety` predicate. Fixable in either direction (define `Safety` in spec OR remove `Safety` line from cfg). +created: 2026-05-03 +last_updated: 2026-05-03 +depends_on: [] +composes_with: [docs/research/2026-05-03-math-proofs-honest-assessment.md, docs/research/proof-tool-coverage.md, B-0179, B-0181] +tags: [tla-plus, formal-verification, circuit-registration, config-bug, b1, math-proofs-assessment, verify-then-claim, smallest-of-3-b1-fixes] +--- + +# Fix CircuitRegistration.tla config bug + +## Symptom + +Running `java -cp tools/tla/tla2tools.jar tlc2.TLC -workers 4 -config tools/tla/specs/CircuitRegistration.cfg tools/tla/specs/CircuitRegistration.tla` produces: + +``` +Error: The invariant Safety specified in the configuration file +is not defined in the specification. +Finished in 00s +``` + +The TLC error is unambiguous: `CircuitRegistration.cfg` has an `INVARIANT Safety` directive but `CircuitRegistration.tla` doesn't define a `Safety` operator. + +## Fix options + +Two directions, decision needed: + +1. **Define `Safety` in the spec.** Read the spec; identify which invariant the original author intended `Safety` to capture; add `Safety == ...` operator that captures it. Most likely the existing `FlagSound` post-condition or a similar property. + +2. **Remove `Safety` from the cfg.** Inspect what other invariants the cfg references; if those alone are sufficient validation, drop the missing `Safety` reference. Risk: may drop an intentional invariant the author meant to add but never finished writing. + +The verify-then-claim follow-up tick should pick (1) if the spec has a clear "what was Safety supposed to mean" thread, else (2) with a comment in the cfg documenting why. + +## Why this is the smallest of 3 B1 fixes + +This is a config-syntax error, not a semantic counterexample. The other two B1 broken specs (B-0179 SpineAsyncProtocol, B-0181 SpineMergeInvariants) require investigating actual counterexamples — substantially harder. This one is bounded to "find the missing operator definition or drop the line." + +## After the fix + +1. Re-run TLC locally; expect clean "No error has been found" +2. Add `[] TLC validates CircuitRegistration` to `tests/Tests.FSharp/Formal/Tlc.Runner.Tests.fs` +3. Add registry row to `docs/research/verification-registry.md` + +## Composes with + +- B-0179 (SpineAsyncProtocol counterexample — sibling B1 issue) +- B-0181 (SpineMergeInvariants counterexample — sibling B1 issue) +- Closure of B1 → A in the math-proofs honest assessment requires all 3 sibling fixes diff --git a/docs/backlog/P2/B-0181-fix-spinemergeinvariants-tla-counterexample-blocks-b1-ci-registration-2026-05-03.md b/docs/backlog/P2/B-0181-fix-spinemergeinvariants-tla-counterexample-blocks-b1-ci-registration-2026-05-03.md new file mode 100644 index 000000000..66d68a2ba --- /dev/null +++ b/docs/backlog/P2/B-0181-fix-spinemergeinvariants-tla-counterexample-blocks-b1-ci-registration-2026-05-03.md @@ -0,0 +1,64 @@ +--- +id: B-0181 +priority: P2 +status: open +title: Fix SpineMergeInvariants.tla counterexample (blocks B1 → A CI registration; depth-17 trace dump on TLC run) +tier: formal-verification +effort: M +ask: Otto 2026-05-03 verify-then-claim sweep (#1397) — running TLC on `SpineMergeInvariants` produces a TTrace dump at depth 17, indicating counterexample / invariant violation. Sibling failure to B-0179 SpineAsyncProtocol but at deeper depth, which may indicate the violation is more subtle (further from initial state). +created: 2026-05-03 +last_updated: 2026-05-03 +depends_on: [] +composes_with: [docs/research/2026-05-03-math-proofs-honest-assessment.md, docs/research/proof-tool-coverage.md, B-0179, B-0180] +tags: [tla-plus, formal-verification, spine-merge, balanced-spine, counterexample, b1, math-proofs-assessment, verify-then-claim] +--- + +# Fix SpineMergeInvariants.tla counterexample + +## Symptom + +Running `java -cp tools/tla/tla2tools.jar tlc2.TLC -workers 4 -config tools/tla/specs/SpineMergeInvariants.cfg tools/tla/specs/SpineMergeInvariants.tla` produces a TTrace dump: + +``` +Trace exploration spec path: tools/tla/specs/SpineMergeInvariants_TTrace_.tla +The depth of the complete state graph search is 17. +Finished in 00s +``` + +TLC dumps a trace file when it finds an invariant violation. The depth-17 termination suggests TLC explored 17 transitions before finding the violation — deeper than the SpineAsyncProtocol failure (depth 9), which may indicate the violation is more subtle (further from initial state, requires more interleaving to manifest). + +## Investigation needed + +1. Read the TTrace file to identify which invariant fails at the depth-17 state +2. Determine the failure class: + - **Spec bug**: spec models the LSM-spine merge protocol incorrectly + - **Invariant over-specification**: invariant asks for a property the merge protocol doesn't actually guarantee + - **Real bug found**: the invariant is correct but the modeled protocol violates it; this would indicate a bug in `BalancedSpine.fs` itself +3. The third class is the most interesting — TLA+ found a real concurrency bug. If that's the case, file as a P0/P1 in BUGS.md instead of treating it as a spec-fix. + +## Composes with + +- B-0179 (SpineAsyncProtocol counterexample — sibling B1 issue) +- B-0180 (CircuitRegistration config bug — sibling B1 issue, smallest fix) +- `src/Core/BalancedSpine.fs` — the production code this spec models +- Closure of B1 → A in the math-proofs honest assessment requires all 3 sibling fixes + +## Why P2 + +Pre-existing failure surfaced by verify-then-claim sweep, not a new regression. The actual blast radius depends on the failure class — if it's a "real bug found" case, escalate to BUGS.md P0 immediately. If it's spec-bug or over-specification, P2 is right. + +## After the fix (or escalation) + +If spec-bug or over-specification: + +1. Fix the spec / invariant +2. Verify locally — TLC clean "No error has been found" +3. Add `[] TLC validates SpineMergeInvariants` to `tests/Tests.FSharp/Formal/Tlc.Runner.Tests.fs` +4. Add registry row to `docs/research/verification-registry.md` + +If real bug found: + +1. File P0/P1 BUGS.md entry referencing this spec + the TTrace +2. Land the production-code fix +3. Verify spec passes after fix +4. Then land the CI registration as above