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

*From*: Karolis Petrauskas <k.petrauskas@xxxxxxxxx>*Date*: Wed, 5 May 2021 00:28:48 +0300*Ironport-hdrordr*: A9a23:PU8Dyq+IcBmyXr3SJQhuk+Hkdr1zdoIgy1knxilNYDRvWIixi92ukPMH1RX9lTYWXzUalcqdPbSbKEmxhOVIyKErF/OHUBP9sGWlaLtj44zr3iH6F0TFm58k6Y5JSII7MtH5CDFB57eC3CCTFdE8zN6btJ25nOu29QYYcShGSYFFqz14BAGSD1FsSGB9avQEPbeV+8YvnUvRRV05dcK+b0N1LtTrgt3QidbPehQGBwEqgTP+zA+Azb7hDly40hIGOgk/j4sK1GjejkjYy8yYwruG4zrdzXKW1pJNhbLau5R+LemNkNVQFjL3lg2zbp9gULHqhkF0nMiKyHIH1ObBuA0hOcMb0QKuQkiQqRvp2w7vlDMv8WKK8y7SvVLGrdbiTDw3T+pt7LgpASfx0lEttt1w3KVA0wuixtJqJCjNlij8+NTEPisC/iHExgtZ4JIupkdSW4cfd7Nd6bYn0ypuYeo9NRn38YU2VNRpZfusrcp+S1+cYnzD11MO/PWXQn8xEh2aK3JyyPC97j4+pgEN82IogOcSknA89Z4nR/B/loD5G5UturULasMNd6pyCKM6XMOrBgX2MHHxGVPXD1LgGqQKf1/ui7qy2rU64+m2ZIcFpaFSpL3xFH1fs2A2dwbBEsuTxdlq/3n2MSmAdAWo5MdZ6Z10/of5WaOuCyueU1oj+vHQwck3M4n8QPa8OJVfBrvKMXbuFYFV3wf3RplVLj0kXNcIv8sgMmj+1P7jG8nNrezUcPHaIf7WHTEoVniXOAp1YBHDYP5N5EyqRXP06SKhPgKKCzPC1KM1KrHT+6w4yYQGNIFA9igTzXqj4N2TQAcy/5ALQA==

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

=========================================================

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

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? :)

<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.

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

- Prev by Date:
**Re: [tlaplus] TLC Error that had me puzzled for a while** - Next by Date:
**Re: [tlaplus] Modelling "eventually, with probability 1"** - Previous by thread:
**Re: [tlaplus] TLC Error that had me puzzled for a while** - Next by thread:
**Re: [tlaplus] Modelling "eventually, with probability 1"** - Index(es):