MisraReachability: name unnamed companion theorems and add PartialCorrectnessThm

Two small hygienic edits to the existing companion proof modules so the
spec-file THEOREM stubs in `Reachable.tla` and `ParReach.tla` are
covered by named, TLAPS-callable theorems:

  ReachableProofs.tla
    -  THEOREM Spec => []((pc = "Done") => (marked = Reachable))
    +  THEOREM Thm4 == Spec => []((pc = "Done") => (marked = Reachable))
    +  THEOREM PartialCorrectnessThm == Spec => []PartialCorrectness
       BY Thm4, PTL DEF PartialCorrectness

  ParReachProofs.tla
    -  THEOREM Spec => R!Init /\ [][R!Next]_R!vars
    +  THEOREM RefinementSafety == Spec => R!Init /\ [][R!Next]_R!vars

`PartialCorrectnessThm` makes the spec-stub form (under the
`PartialCorrectness` defined name) a TLAPS-callable named theorem;
`RefinementSafety` does the same for the parallel-algorithm
refinement-safety result.  The literal THEOREM stubs in the original
spec files remain unproven in their own modules, since proving them
in-place would require those (textbook-style) spec files to import the
companion proof modules -- a circular dependency.

The actually-unproven theorems in this directory are:

  - Reachable.tla:209 termination (Band H, liveness via well-founded
    measure on the lex pair <<|Reachable \ marked|, |vroot|>>)
  - ParReach.tla:235 fairness refinement (Band H, lifting per-process
    WF_vars(p(self)) to WF_R!vars(R!Next) under the refinement mapping)
  - ParReach.tla:223 Spec => Refines (depends on the above)

These remain deferred; PROOF_DIFFICULTY.md is updated to reflect the
new state.

Verified: ReachableProofs (76 obligations, +3 over previous 73) and
ParReachProofs (52 obligations, unchanged) both pass with TLAPS in
under 5 seconds with -I .../CommunityModules/modules.

Co-authored-by: Claude Opus 4.7 <noreply@anthropic.com>
Signed-off-by: Markus Alexander Kuppe <github.com@lemmster.de>

Author: lemmy

PROOF_DIFFICULTY.md

@@ -132,7 +132,7 @@ the obvious one or `TypeOK ∧ goal`.
 - `[bumped → M]` `specifications/SingleLaneBridge/SingleLaneBridge.tla:114` — `Spec => []TypeOK` (`Len(WaitingBeforeBridge) <= Cardinality(Cars)` is not invariant without additional reasoning that a car may not be enqueued twice)
 - `[bumped → M]` `specifications/SingleLaneBridge/SingleLaneBridge.tla:112` — `Spec => []Invariants` (uses `Cardinality(CarsInBridge) < Cardinality(Bridge) + 1`)
 - `[done]` `specifications/KeyValueStore/KeyValueStore.tla:105` — `Spec => [](TypeInvariant /\ TxLifecycle)`
-- `specifications/MisraReachability/Reachable.tla:195` — `Spec => []PartialCorrectness` (companion `ReachableProofs.tla` already does the heavy lifting via `Inv1..3`; this is the wrap-up)
+- `[done in companion]` `specifications/MisraReachability/Reachable.tla:195` — `Spec => []PartialCorrectness` (now proven as `PartialCorrectnessThm` in `ReachableProofs.tla`, and the existing structurally-equivalent unnamed theorem there is now named `Thm4` for downstream reuse; the spec-file stub itself remains unproven for the usual no-circular-spec→companion-imports reason)
 - `[bumped → M]` `specifications/Huang/Huang.tla:106` — `Spec => Safe` (`[](TerminationDetected => []Terminated)` requires the dyadic-rational weight conservation invariant; depends on the `DyadicRationals` community module)
 
 ## Band M — Moderate (24 items)
@@ -182,9 +182,10 @@ well-founded termination, or routine WF-based liveness.
 - `specifications/byzpaxos/PConProof.tla:517` — `Invariance == Spec => []PInv`
 - `specifications/byzpaxos/PConProof.tla:520` — `Implementation == Spec => V!Spec`
 - `specifications/byzpaxos/PConProof.tla:527` — `Spec => [](chosen = V!chosen)`
-- `specifications/MisraReachability/ParReach.tla:223` — `Spec => Refines`
-- `specifications/MisraReachability/ParReach.tla:235` — `Spec => WF_R!vars(R!Next)` (fairness refinement)
-- `specifications/MisraReachability/Reachable.tla:209` — `IsFiniteSet(Reachable) => Spec => <>(pc = "Done")` (well-founded measure on `Cardinality(unmarked)`)
+- `specifications/MisraReachability/ParReach.tla:223` — `Spec => Refines` (= `Spec => R!Spec`; depends on the fairness-refinement piece below, since `R!Spec` includes `WF_R!vars(R!Next)`)
+- `specifications/MisraReachability/ParReach.tla:235` — `Spec => WF_R!vars(R!Next)` (fairness refinement; the per-process `WF_vars(p(self))` of the parallel spec needs to be lifted via the refinement mapping to `WF_R!vars(R!Next)` of Misra's algorithm; non-trivial PTL reasoning)
+- `[done in companion]` `specifications/MisraReachability/ParReach.tla:234` — `Spec => R!Init /\ [][R!Next]_R!vars` (now named `RefinementSafety` in `ParReachProofs.tla`; the spec-file stub remains unproven as above)
+- `specifications/MisraReachability/Reachable.tla:209` — `IsFiniteSet(Reachable) => Spec => <>(pc = "Done")` (termination, well-founded measure on the lex pair `<<Cardinality(Reachable \ marked), Cardinality(vroot)>>`; uses `WF_vars(Next)` plus `WellFoundedInduction`. Multi-day TLAPS proof; deferred)
 - `specifications/Huang/Huang.tla:111` — `Spec => Live` (termination detection liveness)
 - `specifications/KnuthYao/Prob.tla:38` — `Converges == Spec => <>(state \in Accepting \/ Norm(p) = 0)` (probabilistic, treated as `<>`termination)
 - `specifications/Prisoners/Prisoners.tla:178` — `Spec => Safety /\ Liveness`

specifications/MisraReachability/ParReachProofs.tla

@@ -15,7 +15,7 @@ LEMMA TypeInvariant == Spec  => []Inv
 <1>3. QED
   BY <1>1, <1>2, PTL DEF Spec
 
-THEOREM Spec => R!Init /\ [][R!Next]_R!vars
+THEOREM RefinementSafety == Spec => R!Init /\ [][R!Next]_R!vars
 <1>1. Init => R!Init
     BY ProcsAssump DEF Init, R!Init, pcBar, vrootBar, ProcSet  
 <1>2. Inv /\ [Next]_vars => [R!Next]_R!vars

specifications/MisraReachability/ReachableProofs.tla

@@ -194,7 +194,7 @@ THEOREM Thm3 == Spec => []Inv3
     BY <1>1, <1>2, Thm2, PTL DEF Spec
 
 
-THEOREM Spec => []((pc = "Done") => (marked = Reachable))
+THEOREM Thm4 == Spec => []((pc = "Done") => (marked = Reachable))
   (*************************************************************************)
   (* This theorem follows easily from the invariance of Inv1 and Inv3 and  *)
   (* the trivial result Reachable3 of module ReachabilityProofs that       *)
@@ -209,6 +209,13 @@ THEOREM Spec => []((pc = "Done") => (marked = Reachable))
     BY Reachable3 DEF Inv3  
   <1>3. QED
     BY <1>1, <1>2, Thm1, Thm3, PTL
+
+(***************************************************************************)
+(* The same property restated under the spec's PartialCorrectness name,    *)
+(* matching the THEOREM stub at the bottom of Reachable.tla.               *)
+(***************************************************************************)
+THEOREM PartialCorrectnessThm == Spec => []PartialCorrectness
+BY Thm4, PTL DEF PartialCorrectness
 =============================================================================
 \* Modification History
 \* Last modified Sun Apr 14 16:24:32 PDT 2019 by lamport