[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

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

Hi Stephan,

I got it now. Thanks for your help.

Best regards,

On Monday, August 19, 2019 at 5:01:31 PM UTC+8, Stephan Merz wrote:
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,

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/96605c35-b2a7-454b-8520-e44ede772837%40googlegroups.com.