----------------------------- MODULE Increment -----------------------------
(***************************************************************************)
(* This file contains the TLA+ version of the abstract program Increment   *)
(* in Figure 3.5 of the book "A Science of Concurrent Programs".  It also  *)
(* contains a proof of the invariance of Inv that was checked by the TLAPS *)
(* theorem prover.  It first gives the the part of the proof contained in  *)
(* Appendix B.1 of the book.  It then gives the complete proof.            *)
(***************************************************************************)

EXTENDS Integers, FiniteSets,  TLAPS
   (************************************************************************)
   (* The module FiniteSets defines the operator Cardinality, which is     *)
   (* written # in the book.                                               *)
   (************************************************************************)
CONSTANT Procs
N == Cardinality(Procs)

VARIABLES x, pc, t

Init == /\ x = 0
        /\ t = [p \in Procs |-> 0]
        /\ pc = [p \in Procs |-> "a"]

aStep(p) == /\ pc[p] = "a"
            /\ x' = x
            /\ t' = [t EXCEPT ![p] = x]
            /\ pc' = [pc EXCEPT ![p] = "b"]

bStep(p) == /\ pc[p] = "b"
            /\ x' = t[p] + 1
            /\ t' = t
            /\ pc' = [pc EXCEPT ![p] = "done"]
            
PgmStep == \E p \in Procs : aStep(p) \/ bStep(p)            

Stutter == /\ \A p \in Procs: pc[p] = "done"
           /\ UNCHANGED <<x, t, pc>>
              (*************************************************************)
              (* UNCHANGED exp is defined to equals exp', so               *)
              (*                                                           *)
              (*     UNCHANGED <<x, t, pc>>                                *)
              (*                                                           *)
              (* is equivalent to                                          *)
              (*                                                           *)
              (*   <<x', t', pc'>> = <<x, t, pc>>.                         *)
              (*                                                           *)
              (* However, when evaluating a next-state action, the first   *)
              (* time TLC encounters a primed variable like x' must        *)
              (* normally be in an expression of the form x' = ...  .  So, *)
              (* we would have to write it as                              *)
              (*                                                           *)
              (*    (x' = x) /\ (t' = t) /\ (pc' = pc)                     *)
              (*                                                           *)
              (* But since this is a common idiom, TLC will accept the     *)
              (* version written with UNCHANGED.                           *)
              (*                                                           *)
              (*************************************************************)

Next == PgmStep \/ Stutter
------------------------------------------------------------------------------
(***************************************************************************)
(* The definitions of TypeOK, NumberDone, and Inv are the same as in the   *)
(* book.                                                                   *)
(***************************************************************************)
TypeOK == /\ x \in 0..N
          /\ t \in [Procs -> 0..N]
          /\ pc \in [Procs -> {"a","b","done"}]
          
NumberDone == Cardinality({i \in Procs : pc[i] = "done"})

Inv == /\ TypeOK
       /\ \A i \in Procs : (pc[i] = "b") => (t[i] =< NumberDone)
       /\ x =< NumberDone   
----------------------------------------------------------------------------
(***************************************************************************)
(* Below is the TLAPS proof of all the steps proved in Appendix B.1 of the *)
(* book.                                                                   *)
(***************************************************************************) 
THEOREM Next /\ Inv => Inv' 
<1>1.  ASSUME NEW p \in Procs, aStep(p), Inv
       PROVE  Inv'
  (*************************************************************************)
  (* The following proof decomposition is unnecessary because, as shown    *)
  (* below, TLAPS can prove the step with                                  *)
  (*                                                                       *)
  (*      BY <1>1 DEF aStep, Inv, TypeOK, NumberDone                       *)
  (*************************************************************************) 
  <2>1. TypeOK'
    BY <1>1 DEF aStep, Inv, TypeOK
  <2>2. \A i \in Procs : (pc'[i] = "b") => (t'[i] =< NumberDone')
    <3>1. SUFFICES ASSUME NEW i \in Procs, pc'[i] = "b"
                   PROVE  t'[i] =< NumberDone'
      OBVIOUS
    <3>2. NumberDone' = NumberDone
    <3>3. CASE i = p
    <3>4. CASE i # p
      <4>1. (t'[i] = t[i] /\ pc'[i] = pc[i])
        BY <1>1, <3>4  DEF aStep, Inv,  TypeOK
      <4>2. pc[i] = "b"
        BY <4>1, <3>1
      <4>3. t[i] =< NumberDone
        BY <4>2, <1>1 DEF Inv
      <4>4. QED
        BY <4>1, <4>3, <3>2 
    <3>5. QED
      BY <3>3, <3>4                                
  <2>3. x' =< NumberDone'
  <2>4. QED
    BY <2>1, <2>2, <2>3  DEF Inv       
<1>2. ASSUME NEW p \in Procs, bStep(p), Inv
      PROVE  Inv'
<1>3. ASSUME Stutter, Inv
      PROVE Inv'
  BY <1>3 DEF Stutter, Inv, TypeOK, NumberDone  
<1>4. QED
  BY <1>1, <1>2, <1>3 DEF Next, PgmStep
----------------------------------------------------------------------------  
(***************************************************************************)
(* Here is a complete TLAPS checked proof of the invariance of Inv.  The   *)
(* first thing we need to do is assert the assumption that Procs is a      *)
(* finite non-empty set.  An AXIOM is a THEOREM that has no proof.         *)
(***************************************************************************)
AXIOM ProcsFinite == IsFiniteSet(Procs) /\ (Procs # {})

(***************************************************************************)
(* We will need some simple facts about finite sets that are in the        *)
(* library module FiniteSetTheorems, which we now import.                  *)
(***************************************************************************)
INSTANCE FiniteSetTheorems

(***************************************************************************)
(* We will need these theorems from the FiniteSetTheorems module.  Note    *)
(* that theorems can be given a name so they can be applied in later       *)
(* proofs.                                                                 *)
(*                                                                         *)
(*    THEOREM FS_Subset ==                                                 *)
(*      ASSUME NEW S, IsFiniteSet(S), NEW T \in SUBSET S                   *)
(*      PROVE  /\ IsFiniteSet(T)                                           *)
(*             /\ Cardinality(T) =< Cardinality(S)                         *)
(*             /\ Cardinality(S) = Cardinality(T) => S = T                 *)
(*                                                                         *)
(*    THEOREM FS_CardinalityType ==                                        *)
(*      ASSUME NEW S, IsFiniteSet(S)                                       *)
(*      PROVE  /\ Cardinality(S) \in Nat                                   *)
(*             /\ ExistsBijection(1..Cardinality(S), S)                    *)
(*                                                                         *)
(*    THEOREM FS_AddElement ==                                             *)
(*      ASSUME NEW S, NEW x, IsFiniteSet(S)                                *)
(*      PROVE  /\ IsFiniteSet(S \cup {x})                                  *)
(*             /\ Cardinality(S \cup {x}) =                                *)
(*                  IF x \in S THEN Cardinality(S) ELSE Cardinality(S)+1   *)
(*                                                                         *)
(* We use these theorems to prove the two simple lemmas about finite sets  *)
(* that we will need.                                                      *)
(***************************************************************************)
 THEOREM Lemma1 == ASSUME NEW S, IsFiniteSet(S),
                         NEW T, T \subseteq S 
                  PROVE  /\ Cardinality(S) \in Nat
                         /\ IsFiniteSet(T)
                         /\ Cardinality(T) \in 0..Cardinality(S)
                         /\ (T # S) => (Cardinality(T) < Cardinality(S))
  BY   FS_Subset, FS_CardinalityType

THEOREM Lemma2 == ASSUME NEW S, IsFiniteSet(S),
                         NEW e, e \notin S
                  PROVE  Cardinality(S \cup {e}) = Cardinality(S) + 1
  BY FS_AddElement

(***************************************************************************)
(* Here is the complete proof of that Inv is an invariant of program       *)
(* Increment.  The machine-checked proof is as simple as we might expect   *)
(* for proving an invariant of such a simple program.  However, it was     *)
(* simple only because the FiniteSetTheorems was available to prove the    *)
(* two lemmas stating the facts about finite sets that were needed.        *)
(* Fortunately, reasoning about most programs only requires facts about a  *)
(* few simple data types such as sets, functions, and sequences for which  *)
(* we have library modules.                                                *)
(***************************************************************************)
THEOREM Next /\ Inv => Inv'
<1>1. ASSUME NEW p \in Procs, aStep(p), Inv
      PROVE  Inv'
  BY <1>1 DEF aStep, Inv, TypeOK,  NumberDone
<1>2. ASSUME NEW p \in Procs, bStep(p), Inv
      PROVE  Inv'
  <2>1. (N \in Nat) /\ (NumberDone \in 0..N) /\ (NumberDone < N)
    BY ProcsFinite, Lemma1, <1>2 DEF NumberDone, N, bStep
  <2>2. NumberDone' = NumberDone + 1
    BY <1>2, Inv, ProcsFinite,   Lemma1, Lemma2 
      DEF bStep, Inv, TypeOK,  NumberDone  
  <2>3. QED                                                          
    BY <1>2, <2>1, <2>2 DEF Inv, bStep,  TypeOK 
<1>3. ASSUME Stutter, Inv
      PROVE Inv'
  BY <1>3 DEF Stutter, Inv, TypeOK, NumberDone \* , vars
<1>4. QED
  BY <1>1, <1>2, <1>3 DEF Next, PgmStep
=============================================================================
\* Modification History
\* Last modified Wed Oct 23 11:58:59 CEST 2024 by lamport
\* Created Thu May 12 09:39:37 PDT 2022 by lamport
