Help with a TLAPS proof for a refinement involving records (and a Proof Decomposition bug)

[Hengfeng Wei]

Dear All,

I have some difficutlty in proving a refinement mapping involving records.

Below are the simplified TLA specs (see also the attached files):

SimpleVoting.tla:

It maintains for each participant a `maxBal` which is a natural number.

In IncreaseMaxBal(p, b), maxBal[p] is increased to a larger value b.

---------------------------- MODULE SimpleVoting ----------------------------
EXTENDS Naturals
-----------------------------------------------------------------------------
CONSTANT Participant

VARIABLE maxBal

TypeOK == maxBal \in [Participant -> Nat]
-----------------------------------------------------------------------------
Init == maxBal = [p \in Participant |-> 0]

IncreaseMaxBal(p, b) ==
  /\ maxBal[p] < b
  /\ maxBal' = [maxBal EXCEPT ![p] = b]
-----------------------------------------------------------------------------
Next == \E p \in Participant, b \in Nat : IncreaseMaxBal(p, b)

Spec == Init /\ [][Next]_maxBal
=============================================================================

Record.tla:

It maintains a 2D array `state`. `state[p][q]` is the State of q from the view of p and a State is a record:

State == [maxBal : Nat, maxVBal : Nat].

In Prepare(p, b): state[p][p].maxBal is increased to a larger value b.

------------------------------- MODULE Record -------------------------------
EXTENDS Naturals, TLAPS
---------------------------------------------------------------------------
CONSTANTS Participant  \* the set of partipants

VARIABLES state \* state[p][q]: the state of q \in Participant from the view of p \in Participant
   
 State == [maxBal: Nat, maxVBal: Nat]

TypeOK == state \in [Participant -> [Participant -> State]]
---------------------------------------------------------------------------
InitState == [maxBal |-> 0, maxVBal |-> 0]

Init == state = [p \in Participant |-> [q \in Participant |-> InitState]]
 

Prepare(p, b) ==
    /\ state[p][p].maxBal < b
    /\ state' = [state EXCEPT ![p][p].maxBal = b]
---------------------------------------------------------------------------
Next == \E p \in Participant, b \in Nat : Prepare(p, b)

Spec == Init /\ [][Next]_state
---------------------------------------------------------------------------

I want to show that Record refines SimpleVoting under the refinement mapping:

maxBal == [p \in Participant |-> state[p][p].maxBal]

SV == INSTANCE SimpleVoting

However, step <4>2 fails (more details below). (In addition, the proof decomposition (Ctrl+G, Ctrl+D) of <3> generates a buggy formula "maxBal[p] SV!< b" in <4>1, which should be "maxBal[p] < b".)

THEOREM Spec => SV!Spec
  <1>1. Init => SV!Init
    BY DEF Init, SV!Init, maxBal, InitState
  <1>2. [Next]_state => [SV!Next]_maxBal
    <2>1. UNCHANGED state => UNCHANGED maxBal
      BY DEF maxBal
    <2>2. Next => SV!Next
      <3> ASSUME NEW p \in Participant, NEW b \in Nat,
                 Prepare(p, b)
          PROVE  SV!IncreaseMaxBal(p, b) \* SV!Next
        <4>1. maxBal[p] < b \* Wrong decomposition here: maxBal[p] SV!< b
          BY DEF Prepare, maxBal
        <4>2. maxBal' = [maxBal EXCEPT ![p] = b]
          BY DEF Prepare, maxBal \* Failed here!!!
        <4>3. QED
          BY <4>1, <4>2 DEF SV!IncreaseMaxBal
      <3>1. QED
        BY DEF Next, SV!Next
    <2>3. QED
      BY <2>1, <2>2
  <1>3. QED
    BY <1>1, <1>2, PTL DEF SV!Spec, Spec

The obligation at <4>2 is as follows. Isn't the `state' = [state EXCEPT ![p] = ...]` in the assumption the same as the conclusion `[p_1 \in Participant |-> state[p_1][p_1].maxBal]' ...`? What is wrong with my proof? How should I proceed?

 

ASSUME NEW CONSTANT Participant,
       NEW VARIABLE state,
       NEW CONSTANT p \in Participant,
       NEW CONSTANT b \in Nat,
       /\ state[p][p].maxBal < b
       /\ state'
          = [state EXCEPT
               ![p] = [state[p] EXCEPT
                         ![p] = [state[p][p] EXCEPT !.maxBal = b]]]
PROVE  [p_1 \in Participant |-> state[p_1][p_1].maxBal]'
       = [[p_1 \in Participant |-> state[p_1][p_1].maxBal] EXCEPT ![p] = b]

Best regards,

hengxin

[Stephan Merz]

Hello Hengxin,

please feel free to post a bug report about the malfunctioning proof decomposition.

Concerning the failure of step <4>2, you need to invoke the type invariant so that the provers can determine the shape of the function `state'. In particular, you have [f EXCEPT ![x] = ...] = f if x is not an element of DOMAIN f (in your case you have a complicated EXCEPT clause involving a two-dimensional array of records). As a rule of thumb, the type invariant is always necessary when reasoning about EXCEPT expressions.

This requires introducing the type invariant in the step simulation part of the proof. Fortunately, you can rely on the type-correctness theorem and PTL checks that this is okay. The refinement proof becomes (see also the attached TLA+ module):

THEOREM Spec => SV!Spec
  <1>1. Init => SV!Init
    BY DEF Init, SV!Init, maxBal, InitState

  <1>2. TypeOK /\ [Next]_state => [SV!Next]_maxBal

    <2>1. UNCHANGED state => UNCHANGED maxBal
      BY DEF maxBal

    <2>2. TypeOK /\ Next => SV!Next

      <3> ASSUME NEW p \in Participant, NEW b \in Nat,

                 TypeOK, Prepare(p, b)

          PROVE  SV!IncreaseMaxBal(p, b) \* SV!Next

        <4>1. maxBal[p] < b \* Wrong decomposition: maxBal[p] SV!< b

          BY DEF Prepare, maxBal
        <4>2. maxBal' = [maxBal EXCEPT ![p] = b]

          BY Zenon DEF Prepare, maxBal, TypeOK, State

        <4>3. QED
          BY <4>1, <4>2 DEF SV!IncreaseMaxBal
      <3>1. QED
        BY DEF Next, SV!Next
    <2>3. QED
      BY <2>1, <2>2
  <1>3. QED

    BY <1>1, <1>2, Invariant, PTL DEF SV!Spec, Spec

and it is checked by TLAPS. (The explicit invocation of Zenon in step <4>2 is not necessary but it documents which backend found the proof and avoids waiting for SMT to timeout.)

Best regards,

Stephan

[Leslie Lamport]

 Stephan wrote:

   please feel free to post a bug report about the malfunctioning proof decomposition.

I do not see any malfunction of the proof decomposition command.  The command is expanding the 
definition of  SV!IncreaseMaxBal(p, b).  The definition of IncreaseMaxBal in module SimpleVoting
uses the operator < (imported from the Naturals module), which is imported by the INSTANCE statement 
as the operator SV!< .  Since the module containing the theorem also imports the Naturals module,
the operator SV!< happens to equal the operator < of the current module.  Please replace < by SV!< 
in the proof and check that it still works.  If it doesn't, please report this as a TLAPS bug.  

Because the definition of < is imported into the instantiated module from a standard module, and 
that same definition is imported into the instantiating module from the same standard module, a
user would almost always prefer that the Decompose Proof command replace SV!< by < .  This should
be straightforward to implement and we would be grateful if someone would volunteer to do it.

Leslie

[Hengfeng Wei]

Dear Leslie,

Thanks for your reply.

Now I understand "SV!<".

So, the real bug here is that the Toolbox (Version 1.6.0 of 10 July 2019) reports a parse error on `maxBal[p] SV!< b`; see the attached .png file (I failed to insert it in the text here.)

See also the attached TLA+ Specs files (SimpleVoting.tla, Record.tla) for the line numbers referred to in the error message.

Best regards,

hengxin

[Hengfeng Wei]

Hi Stephan,

I got it now. Thanks for your help.

Best regards,

hengxin