Hi,
I believe the idea of reducing "almost-sure" properties of probabilistic programs (i.e., properties that hold with probability 1) to fairness conditions goes back to work by Vardi and others in the 1980s. In your specification, instead of assuming Live, you could assume
\A b \in BOOLEAN : SF_vars(Round /\ val' = b)
that is, if it is infinitely often possible to throw a coin and obtain value b then eventually such a throw will occur. (In your spec, writing WF or SF makes no difference, but in general SF will be stronger.)
Your proof actually doesn't need the experimental support for ENABLED in that branch of TLAPS (but you would need it if you were to adopt the fairness hypothesis above), since the essence of the proof is showing the safety property
[](done => []done),
the rest follows by propositional temporal logic. But you are completely right that documentation on how to prove temporal properties is sorely lacking at the moment. Stay tuned. ;-)
Stephan
> On 5 May 2021, at 09:45, Igor Konnov <igor.konnov@xxxxxxxxx> wrote:
>
> Hi Karolis,
>
> I agree, your reasoning looks circular to me. Basically, the theorem states that <>[]done should hold by assuming <>done in Live.
>
> However, it’s a nice idea to reduce a probabilistic argument to a non-probabilistic one. We did something similar for the Ben-Or’s algorithm in the paper that is not related to TLA+. However, the reduction argument required a hand-written proof to reason about adversaries and limits, see Section 7 in [1]. I am not sure about how much of it could be mechanized.
>
> [1]: https://drops.dagstuhl.de/opus/volltexte/2019/10935/
>
>
> Best regards,
> Igor
>
>> On 04.05.2021, at 23:28, Karolis Petrauskas <k.petrauskas@xxxxxxxxx> wrote:
>>
>> I'm trying to model a consensus algorithm, in which a common coin (a distributed random number) is used to overcome the FLP impossibility.
>> An example of such an algorithm is presented in https://eprint.iacr.org/2016/199.pdf, Figure 11.
>>
>> The termination of the algorithm is based on the fact that by repeating the coin flips we will get the needed value eventually (because of the uniform randomness, as I understand).
>> The below spec does not model the entire algorithm, just the part with the common coin.
>>
>> Does it look reasonable to model that "eventual" with <>done as a fairness assumption?
>> I'm not sure. It sounds a bit like assuming the conclusion, but on the other hand I'm not trying to prove that probabilistic property, just use it.
>> In this example Decides looks similar to Live, but in the final spec the Decides property would be different.
>>
>> ------------- MODULE CommonCoinConverges --------------
>> EXTENDS TLAPS
>> VARIABLE val
>> VARIABLE done
>> vars == <<val, done>>
>> Round == /\ ~done
>> /\ \E newCoin \in BOOLEAN : \* Take a new random number.
>> /\ done' = (newCoin = val) \* Check, if the value is lucky.
>> /\ val' = newCoin
>> Terminated == done /\ UNCHANGED vars \* Just to avoid a deadlock in a proof bellow.
>> Init == /\ val \in BOOLEAN
>> /\ done = FALSE
>> Next == Round \/ Terminated
>> Live == <>done
>> Spec == Init /\ [][Next]_vars /\ Live
>> ---------------------------------------------------------
>> TypeOK == /\ val \in BOOLEAN
>> /\ done \in BOOLEAN
>> Decides == <>[]done
>> THEOREM Spec => []TypeOK /\ Decides
>> =========================================================
>>
>>
>> As a side note, I managed to prove the above theorem in TLAPS from the updated_enabled_cdot branch by looking
>> at https://github.com/tlaplus/tlapm/blob/updated_enabled_cdot/examples-draft/SimpleExampleWF.tla.
>> Although I'm still not sure if I would be able to do that again :) The proof tactics for temporal operators are not clear to me.
>> Maybe there is a paper or a book on such tactics that I should read before trying to prove something like this? :)
>>
>> THEOREM Spec => []TypeOK /\ Decides
>> <1>1. Spec => []TypeOK
>> <2>1. Init => TypeOK BY DEF Init, TypeOK
>> <2>2. TypeOK /\ [Next]_vars => TypeOK'
>> <3> SUFFICES ASSUME TypeOK, Next PROVE TypeOK' BY DEF vars, TypeOK
>> <3> CASE Round BY DEF Round, TypeOK
>> <3> CASE Terminated BY DEF Terminated, TypeOK, vars
>> <3>q. QED BY DEF TypeOK, Next, Round, Terminated
>> <2>q. QED BY <2>1, <2>2, PTL DEF Spec
>> <1>2. Spec => Decides
>> <2>x. TypeOK /\ Spec => [] (~done \/ []done)
>> <3>1. ASSUME TypeOK /\ [Next]_vars PROVE ~done \/ done'
>> <4> SUFFICES ASSUME TypeOK, Next PROVE ~done \/ (done') BY <3>1 DEF vars
>> <4> CASE Round BY DEF Round
>> <4> CASE Terminated BY DEF Terminated, vars
>> <4> QED BY DEF Next
>> <3>q. QED BY <3>1, <1>1, PTL DEF Spec
>> <2>q. QED BY <1>1, <2>x, PTL DEF Spec, Live, Decides
>> <1>q. QED BY <1>1, <1>2
>>
>> Sincerely,
>> Karolis Petrauskas
>>
>> --
>> 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/CAFteovKBZYaJtoRsYKPG7rsQOVqNxu3d%3Dp5n4bfigxvSqS0o%3DQ%40mail.gmail.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/E25C481E-0232-4281-AF35-4D0DE8748165%40gmail.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/EF826A2F-FA88-4E2F-834A-E1A094208EBF%40gmail.com.