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