add current version of safety oracle #13
Open
Conversation
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
nrryuya
reviewed
Jan 8, 2019
|
|
||
| \begin{defn}[Clique with $n$ layers] | ||
| \begin{align} | ||
| Clique&: \mathbb{N}^+ \times \mathcal{P}(\mathcal{V}) \times P_{\mathcal{C}} \times \Sigma \to \{True, False\} \\ |
There was a problem hiding this comment.
!s are missing just before L^H_J and L^H_M?
Clique&: \mathbb{N}^+ \times \mathcal{P}(\mathcal{V}) \times P_{\mathcal{C}} \times \Sigma \to \{True, False\} \\
Clique(1, V, p, \sigma) &:\Leftrightarrow \forall v \in V, V \subseteq Agreeing(p, !L^H_J(\sigma)(v)) \\
&~~~~\land \forall v' \in V, Later\_Disagreeing(p, !L^H_M(!L^H_J(\sigma)(v))(v'), v', \sigma) = \emptyset \\
Clique(n, V, p, \sigma) &:\Leftrightarrow \forall v \in V, V \subseteq Agreeing(p, !L^H_J(\sigma)(v)) \\
&~~~~\land \forall v \in V, Clique\_Cond(n - 1, V, p, !L^H_J(\sigma)(v))
nrryuya
reviewed
Jan 16, 2019
| \end{defn} | ||
|
|
||
|
|
||
| \begin{defn}[Non-equivocating majority driven property] |
There was a problem hiding this comment.
Non-equivocating majority driven property
It should be Majority validators, A validator set is a majority or something?
nrryuya
reviewed
Jan 18, 2019
| \implies&\{m \in \sigma': Sender(m) = \overline{v} \land Later(m, \overline{m})\} = \emptyset \\ | ||
| \implies&Later\_From(\overline{m}, \overline{v}, \sigma') = \emptyset \\ | ||
| \end{align} | ||
| We will now be able to show that $\overline{m}$ is a latest honest message. Note that if a validator is not equivocating in $\sigma'$, the validators latest honest message is equal to the validators latest messages, by the defintion of latest honest message. |
nrryuya
reviewed
Jan 18, 2019
| \begin{proof} | ||
| Due to the definition of $L^H_M$, there are two cases: when $v \in E(\sigma)$ and otherwise: | ||
|
|
||
| \[ L^H_M(\sigma))(v) = \left\{ |
There was a problem hiding this comment.
L^H_M(\sigma))(v)
The second ) is redundant.
nrryuya
reviewed
Jan 18, 2019
| \begin{align} | ||
| &\neg (\exists m \in Justification(\overline{m}): Sender(m) = \overline{v} \land Later(m, !L^H_M(\sigma)(\overline{v}))) \\ | ||
| \implies&\nexists m \in Justification(\overline{m}): Sender(m) = \overline{v} \land Later(m, !L^H_M(\sigma)(\overline{v})) \\ | ||
| \implies&\{m \in Just |
There was a problem hiding this comment.
The function signature is wrong.
There was a problem hiding this comment.
and the order of params σ and p of Clique is reversed from the definition 7.16?
nrryuya
reviewed
Jan 18, 2019
|
|
||
| \begin{defn}[Minimal transitions] | ||
| $$ | ||
| Minimal_t = \{ (\sigma, \sigma') \in \Sigma_t^2: \sigma \to \sigma' \land \nexists \sigma'' . \sigma \to \sigma'' \to \sigma' \land \sigma'' \neq \sigma \land \sigma'' \neq \sigma' \} |
There was a problem hiding this comment.
I guess we also need σ ≠ σ' for a minimal transition?
If σ = σ', σ \ σ' = ∅ and this is not good in the later lemmas.
nrryuya
reviewed
Jan 23, 2019
| \begin{lemma}[$\overline{m}$ is $\overline{v}$'s latest message in $\sigma$'] | ||
| $\forall (\sigma, \sigma') \in Minimal_t$, letting $\overline{m} =~!\sigma'\setminus\sigma$ and $\overline{v} = Sender(\overline{m})$, | ||
| $$ | ||
| \overline{v} \notin E(\sigma') \implies \overline{m} = !L^H_M(\sigma')(\overline{v}))) |
There was a problem hiding this comment.
!L^H_M(\sigma')(\overline{v})))
)) is redundant.
nrryuya
reviewed
Feb 6, 2019
| Agreeing: P_{\mathcal{C}} \times \Sigma \to \mathcal{P}(\mathcal{V}) | ||
| $$ | ||
| $$ | ||
| Agreeing(p, \sigma) :\Leftrightarrow \{v \in \mathcal{V} : \forall c \in L^H_E(\sigma)(v), p(c)\} |
There was a problem hiding this comment.
In HOL, ∀ a ∈ ∅. P is True. Therefore, v s.t. L^H_E(\sigma)(v) is empty is included in agreeing.
I think it should be re-defined to remove validators which are not observed or equivocating like this (Isabelle code):
fun observed_non_equivocating_validators :: "state ⇒ validator set"
where
"observed_non_equivocating_validators σ = observed σ - equivocating_validators σ"
fun agreeing_validators :: "(consensus_value_property * state) ⇒ validator set"
where
"agreeing_validators (p, σ) = {v ∈ observed_non_equivocating_validators σ. ∀ c ∈ latest_estimates_from_non_equivocating_validators σ v. p c}"
nrryuya
reviewed
Feb 24, 2019
| \begin{align} | ||
| &\neg (\exists m \in Justification(\overline{m}): Sender(m) = \overline{v} \land Later(m, !L^H_M(\sigma)(\overline{v}))) \\ | ||
| \implies&\nexists m \in Justification(\overline{m}): Sender(m) = \overline{v} \land Later(m, !L^H_M(\sigma)(\overline{v})) \\ | ||
| \implies&\{m \in Just |
afck
reviewed
Mar 4, 2019
| L^H_J:\Sigma \to (\mathcal{V} \to \mathcal{P}(\Sigma)) | ||
| $$ | ||
| $$ | ||
| L^H_J(\sigma)(v) = \{Justification(m) : m \in L^H_M(\sigma)(v)\} |
There was a problem hiding this comment.
Should this be the union (or !) of that set, i.e. just Justification(m) for the unique m \in L^H_M(\sigma)(v)?
| $$ | ||
| \end{defn} | ||
|
|
||
| A minimal transition corresponds to recieving a single new message with justification drawn from the initial protocol state. We will show that any minimal transition from a validator not in the clique will not affect the clique. |
0xjac
reviewed
Jul 16, 2019
|
|
||
| \subsection{Validator Cliques} | ||
|
|
||
| A clique of validators for some proposition $p$ can be thought of as a set of validators who pairwise see eachother agreeing with $p$, where there are also no later messages from these validators that are disagreeing with $p$. A clique can have mulitple layers, although the minimum viable safety oracle will only be $1-layer$ deep. \\ |
There was a problem hiding this comment.
- s/eachother/each other/
- s/mulitple/multiple/
0xjac
reviewed
Jul 16, 2019
| \end{lemma} | ||
|
|
||
| \begin{proof} | ||
| The forward direction, $v \in E(\sigma) \implies v \in E(\sigma')$, follows immediatly as equivocation is monotonic, |
|
What's the status of this? This PR hasn't been given love in a while and it's pretty important. |
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
Add this suggestion to a batch that can be applied as a single commit.
This suggestion is invalid because no changes were made to the code.
Suggestions cannot be applied while the pull request is closed.
Suggestions cannot be applied while viewing a subset of changes.
Only one suggestion per line can be applied in a batch.
Add this suggestion to a batch that can be applied as a single commit.
Applying suggestions on deleted lines is not supported.
You must change the existing code in this line in order to create a valid suggestion.
Outdated suggestions cannot be applied.
This suggestion has been applied or marked resolved.
Suggestions cannot be applied from pending reviews.
Suggestions cannot be applied on multi-line comments.
Suggestions cannot be applied while the pull request is queued to merge.
Suggestion cannot be applied right now. Please check back later.
TODO: