changed 5 years ago  
Linked with GitHub

Prooving correctness

Let \(H\) be a set of target epochs sorted by increasing order (will use an attestation_history in practice but algorithm is the same).
Let \(t_i\) be a target epoch \((t_1, t_2.. t_i ..t_{latest}) \in H\).
Let \(s(t)\) be the source epoch associated with the target epoch \(t\).

We assume that:
(1) \(H\) is sorted by increasing order
(2) Every attestation in \(H\) is well formed i.e.:

\(\forall t \in H\):

  • \(s(t) \in H\) (since a source must always be justified)
  • \(s(t) \lt t\)

Rules

An attestation is slashable if and only if:
\((a).\ \exists (t_a, t_b) \in H\ |\ (t_a == t_b)\)
\((b).\ \exists (t_a, t_b) \in H\ |\ (s(t_a) \lt s(t_b) \land t_b \lt t_a)\)

Lem

When inserting a new attestation \(t_{new}\) in \(H\):
\[ (b) \iff (b_1) \lor (b_2)\] with:
\((b_1) \iff \exists t \in F\ |\ (s(t) < s(t_{new}))\)
\((b_2) \iff \exists t \in G\ |\ (s(t) > s(t_{new}))\)

where
\(F = \{t \in\ ]t_{new},\ t_{latest}]\ \}\)
\(G = \{t \in\ ]f(s(t_{new})),\ t_{new}[\ \}\)

with \(t_{latest} = max(H)\) (max is well defined for H)

and with \(f(s)\) defined as the function that takes a source epoch and returns the element following \(s\). This function is well defined for any valid source in \(H\), as a source always has at least one following target.

Notice that \((b_1)\) is equivalent to checking that we are not inserting an attestation surrounded by previous votes.
Notice that \((b_2)\) is equivalent to checking that we are not inserting an attestation that surrounds previous votes.

Demonstration

\[(b).\ \exists (t_a, t_b) \in H\ |\ (s(t_a) \lt s(t_b) \land t_b \lt t_a)\]

By fixing one of the two targets to \(t_{new}\) we get:

\[(b): \exists t \in H\ |\ ((s(t) \lt s(t_{new}) \land t_{new} \lt t)\lor (s(t_{new}) \lt s(t) \land t \lt t_{new}))\]

Let \((b_a): \exists t \in H\ |\ (s(t) \lt s(t_{new}) \land t \gt t_{new})\)
Let \((b_b):\exists t \in H\ |\ (s(t) \gt s(t_{new}) \land t \lt t_{new})\)

Then we can see that:
\[(b) \iff (b_a) \lor (b_b)\]

  1. First let's show that \((b_a) \iff (b_1)\)

\((b_a): \exists t \in H\ |\ (s(t) \lt s(t_{new}) \land t \gt t_{new})\)
\(\iff \exists t \in\ ]t_{new}, t_{latest}]\ |\ (s(t) \lt s(t_{new}))\)
where \(t_{latest}\) is equivalent to \(max(H)\) (well defined for \(H\)).

Let \(F = \{t \in H\ |\ t \gt\ t_{new}\} \iff \{t \in\ ]t_{new}, t_{latest}]\}\)

Remember \((b_1) \iff \exists t \in F\ |\ (s(t) < s(t_{new}))\)
Hence:
\[(b_1) \iff (b_a)\]

  1. Similarly, let's show that \((b_b) \iff (b_2)\)

Let \(f(s)\) be the function that takes a source epoch and returns the element following \(s\). This function is well defined for any valid source in \(H\), as a source always has at least one following target.

We first notice that
\(s(t) \gt s(t_{new}) \iff t \gt f(s(t_{new}))\) (validity)

\((b_b): \exists t \in H\ |\ (s(t) \gt s(t_{new}) \land t \lt t_{new})\)
\(\iff \exists t \in\ H\ |\ (t \gt f(s(t_{new})) \land t \lt t_{new})\)
\(\iff \exists t \in\ H\ |\ (f(s(t_{new})) \lt t \lt t_{new})\)

Let \(G = \{t \in\ ]f(s(t_{new})),\ t_{new}[\ \} \iff \{ t \in H\ |\ (f(s(t_{new})) \lt t \lt t_{new})\ \}\)

Remember \((b_2) \iff \exists t \in G\ |\ (s(t) > s(t_{new}))\)
Hence:
\[(b_2) \iff (b_b)\]

Finally we have:
\[(b) \iff (b_a) \lor (b_b)\]

\[(b_a) \lor (b_b) \iff (b_1) \lor (b_2)\]

\[(b) \iff (b_1) \lor (b_2)\ \square\]

Algorithm

# t is a list of previous attestations target epochs
def should_sign_attestation(t_new, t):
  if len(t) == 0:
      # No previous attestations
      return True
  i = len(t) - 1
  # Checking for (b1)
  while t[i] > t_new:
      if s(t[i]) < s(t_new):
          return False
      if i == 0:
          # Pruning error : new attestation epoch is smaller 
          # than smallest previous attestation target epoch
          return False
      i -= 1
  # Checking for double vote
  if i == t_new:
      # hash256 is a simple hash function
      # get_data is a function that returns the attestation_data
      # corresponding to the target epoch
      if hash256(get_data(t[i]) == hash256(get_data(t_new):
          return True
      else:
          return False
  else:
      # Checking for (b2)
      # Haven't implemented f(s(t_new)) as described in spec
      while t[i] > s(t_new):
          if s(t[i]) > s(t_new):
              return False
          if i == 0:
              # Pruning error: Target corresponding to new 
              # attestation source doesn't appear in history
              return False
          i -= 1
      return True

The time complexity of this algorithm is \(\mathcal{O}(|F + G|)\).

To play around with PoC: https://github.com/pscott/attestation_slashing_protection/

Select a repo