Skip to content

Latest commit

 

History

History
94 lines (70 loc) · 3.03 KB

README.md

File metadata and controls

94 lines (70 loc) · 3.03 KB
Raw

SMT-based specification of 3SF

This directory contains a constraint-based encoding of the abstract 3SF protocol.
It was produced as a by-product of our model-checking work on 3SF.

We encode the high-level definitions of 3SF (checkpoints, FFG votes, justification & finalization votes, slashing conditions) using SMT constraints. In particular, we make use of the decision procedure for finite sets and cardinality constraints1 in the CVC5 solver.

This allows us to check Accountable Safety for small models of the protocol.

Experiments

The specification lives in ./ssf.smt.
We conducted experiments using CVC5 v1.2.0.

$ cvc5 --version
This is cvc5 version 1.2.0 [git tag 1.2.0 branch HEAD]

The expected output is:

$ cvc5 ssf.smt
"searching for accountable safety violation [expect unsat]"
unsat

Performance evaluation

We obtained the following runtimes allocating 2 CPU cores of a 3.2 GHz Intel Xeon 8488C with 8GB RAM:

# blocks # checkpoints runtime
3 5 8 min 11 sec
4 5 22 min 00 sec
5 5 1 h 40 min 19 sec
3 6 74 h 1 min 41 sec
4 6 timeout (>80hrs)

The script in ./benchmark_ssf.py can be used to do a grid search over parameters.

Examples: Querying reachable program states

Besides checking Accountable Safety, we can use the SMT solver to discover interesting reachable protocol states within seconds.

Some example queries have been pre-written in the Examples section of the SMT file.
To check them, simply uncomment the respective section and run CVC as above.

An example output:

$ grep -A 3 "find conflicting blocks" ssf.smt
; find conflicting blocks
(assert (not (= conflicting_blocks (as set.empty (Relation Hash Hash)))))
(check-sat)
(get-model)

$ cvc5 ssf.smt
sat
(
(define-fun genesis () Hash Hash1)
(define-fun parent_of (($x1 Hash)) Hash Hash1)
(define-fun slot (($x1 Hash)) Int (ite (= Hash3 $x1) 1 (ite (= Hash2 $x1) 1 0)))
(define-fun conflicting_blocks () (Set (Tuple Hash Hash)) (set.union (set.singleton (tuple Hash3 Hash2)) (set.singleton (tuple Hash2 Hash3))))
[...]
)

Here, the SMT solver has found an example of conflicting blocks Hash2 and Hash3.
The encoded graph looks like this, and indeed contains these conflicting blocks:

flowchart RL
    H1("`**Hash1** *(genesis)*
    slot: 0`")
    H2("`**Hash2**
    slot: 1`")
    H3("`**Hash3**
    slot: 1`")

    H2 --> H1
    H3 --> H1
Loading

You can use CVC5 to find and enumerate more complex scenarios, e.g., justification or slashing conditions.

Footnotes

  1. Kshitij Bansal, Clark W. Barrett, Andrew Reynolds, and Cesare Tinelli. A new decision procedure for finite sets and cardinality constraints in SMT. CoRR, 2017. arXiv:1702.06259. ↩