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

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