-
Notifications
You must be signed in to change notification settings - Fork 16
New issue
Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.
By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.
Already on GitHub? Sign in to your account
add current version of safety oracle #13
base: master
Are you sure you want to change the base?
Conversation
|
||
\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.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
!
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))
\end{defn} | ||
|
||
|
||
\begin{defn}[Non-equivocating majority driven property] |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Non-equivocating majority driven property
It should be Majority validators
, A validator set is a majority
or something?
\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. |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
defintion
Typo ;)
\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.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
L^H_M(\sigma))(v)
The second )
is redundant.
\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.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
The function signature is wrong.
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
and the order of params σ
and p
of Clique
is reversed from the definition 7.16?
|
||
\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.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
I guess we also need σ ≠ σ'
for a minimal transition?
If σ = σ'
, σ \ σ' = ∅
and this is not good in the later lemmas.
\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.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
!L^H_M(\sigma')(\overline{v})))
))
is redundant.
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.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
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}"
\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.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
forall
→ \forall
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.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
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. |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Typo: "receiving"
|
||
\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.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
- s/eachother/each other/
- s/mulitple/multiple/
\end{lemma} | ||
|
||
\begin{proof} | ||
The forward direction, $v \in E(\sigma) \implies v \in E(\sigma')$, follows immediatly as equivocation is monotonic, |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
s/immediatly/immediately/
What's the status of this? This PR hasn't been given love in a while and it's pretty important. |
TODO: