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

 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, Specand 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 -- You received this message because you are subscribed to the Google Groups "tlaplus" group. To unsubscribe from this group and stop receiving emails from it, send an email to tlaplus+unsubscribe@xxxxxxxxxxxxxxxx. To view this discussion on the web visit https://groups.google.com/d/msgid/tlaplus/BA505F11-C0A0-48F8-A2BE-65939F2DA92E%40gmail.com.

Attachment: Record.tla
Description: Binary data

 On 15 Aug 2019, at 06:26, Hengfeng Wei wrote: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 ParticipantVARIABLE maxBalTypeOK == 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 partipantsVARIABLES 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 SimpleVotingHowever, 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, SpecThe 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 -- You received this message because you are subscribed to the Google Groups "tlaplus" group. To unsubscribe from this group and stop receiving emails from it, send an email to tlaplus+unsubscribe@xxxxxxxxxxxxxxxx. To view this discussion on the web visit https://groups.google.com/d/msgid/tlaplus/104baa52-4929-42c4-9c5f-dd9ddfe559ae%40googlegroups.com. -- You received this message because you are subscribed to the Google Groups "tlaplus" group. To unsubscribe from this group and stop receiving emails from it, send an email to tlaplus+unsubscribe@xxxxxxxxxxxxxxxx. To view this discussion on the web visit https://groups.google.com/d/msgid/tlaplus/BA505F11-C0A0-48F8-A2BE-65939F2DA92E%40gmail.com.

• Follow-Ups:
• References: