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

*From*: Igor Konnov <igor.konnov@xxxxxxxxx>*Date*: Wed, 5 May 2021 09:45:46 +0200*Cc*: Igor Konnov <igor.konnov@xxxxxxxxx>*References*: <CAFteovKBZYaJtoRsYKPG7rsQOVqNxu3d=p5n4bfigxvSqS0o=Q@mail.gmail.com>

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.

**Follow-Ups**:**Re: [tlaplus] Modelling "eventually, with probability 1"***From:*Stephan Merz

**References**:**[tlaplus] Modelling "eventually, with probability 1"***From:*Karolis Petrauskas

- Prev by Date:
**[tlaplus] Modelling "eventually, with probability 1"** - Next by Date:
**Re: [tlaplus] Modelling "eventually, with probability 1"** - Previous by thread:
**[tlaplus] Modelling "eventually, with probability 1"** - Next by thread:
**Re: [tlaplus] Modelling "eventually, with probability 1"** - Index(es):