Skip to content

Commit

Permalink
Add initial batch of more documented and organized examples
Browse files Browse the repository at this point in the history
  • Loading branch information
@odedp
odedp committed Apr 9, 2024
1 parent 23edbe8 commit 7b4f612
Show file tree
Hide file tree
Showing 39 changed files with 5,245 additions and 0 deletions.
316 changes: 316 additions & 0 deletions examples_2024/block_cache_system.pyv
View file

Large diffs are not rendered by default.

220 changes: 220 additions & 0 deletions examples_2024/bosco_3t_safety.pyv
View file
Original file line number Diff line number Diff line change
@@ -0,0 +1,220 @@
# Model of Byzantine One-Step COnsensus (BOSCO)
#
# Song Y.J., van Renesse R. Bosco: One-Step Byzantine Asynchronous
# Consensus. DISC 2008.
# https://link.springer.com/chapter/10.1007/978-3-540-87779-0_30
#
# This file is based on the Ivy model from:
#
# Berkovits I., Lazic M., Losa G., Padon O., Shoham S. Verification of
# Threshold-Based Distributed Algorithms by Decomposition to Decidable
# Logics. CAV 2019.
# https://link.springer.com/chapter/10.1007%2F978-3-030-25543-5_15


sort quorum_a # >= n - t
sort value
sort quorum_b # >= (n+3t+1)/2
sort quorum_c # >= (n-t+1)/2
sort node # n > 3t

immutable relation member_f(node) # faulty nodes
immutable relation member_a(node, quorum_a)
immutable relation member_b(node, quorum_b)
immutable relation member_c(node, quorum_c)

################################################################################
#
# Intersection properties
#
################################################################################

# n > 3t:

# A(~f) --- not needed for safety
# axiom exists A:quorum_a. forall N:node. member_a(N,A) -> ~member_f(N)

# C( A & B & ~f )
axiom forall A:quorum_a,B:quorum_b. exists C:quorum_c. forall N:node. member_c(N,C) -> member_a(N,A) & member_b(N,B) & !member_f(N)

# nonempty( B & C & ~f )
axiom forall B:quorum_b,C:quorum_c. exists N:node. member_b(N,B) & member_c(N,C) & !member_f(N)

# n > 5t:
# axiom forall A:quorum_a. exists B:quorum_b. forall N:node. member_b(N,B) -> member_a(N,A)

# n > 7t:
# axiom forall A:quorum_a. exists B:quorum_b. forall N:node. member_b(N,B) -> member_a(N,A) & !member_f(N)

################################################################################
#
# Protocol state
#
################################################################################

# state of nodes
immutable relation input(node, value) # input value of a process
mutable relation dec(node, value) # a process N decided on V
mutable relation und_cons(node, value) # a process N calls the underlying consensus with value V
mutable relation done(node) # has the process done lines 3-7
mutable relation und_cons_dec(value) # the underlying consensus decission

# state of the network
mutable relation sent_msg(node, node, value) # (src, dst, v)
mutable relation rcv_msg(node, node, value) # (src, dst, v)

# instrumentation relations
mutable relation sent_msg_proj(node, node) # sent_msg_proj(N1, N2) := exists V. sent_msg(N1, N2, V)
mutable relation rcv_msg_proj(node, node) # rcv_msg_proj(N1, N2) := exists V. rcv_msg(N1, N2, V)


axiom !member_f(N) & input(N,V1) & input(N,V2) -> V1 = V2
init !member_f(N) -> !dec(N,V)
init !member_f(N) -> !und_cons(N,V)
init !und_cons_dec(V)
init !member_f(N1) -> (sent_msg(N1,N2,V) <-> input(N1,V))
init !member_f(N1) -> sent_msg_proj(N1,N2) # assume every node has some input
init sent_msg(N1,N2,V) -> sent_msg_proj(N1,N2)
init rcv_msg(N1,N2,V) -> rcv_msg_proj(N1,N2)
init !member_f(N2) -> !rcv_msg(N1,N2,V)
init !member_f(N2) -> !rcv_msg_proj(N1,N2)
init !done(N)

################################################################################
#
# Protocol transitions
#
################################################################################

transition receive_msg_0(n: node, s: node, v: value)
modifies rcv_msg, rcv_msg_proj
& ( !done(n) )
& ( sent_msg(s,n,v) )
& ( forall S, D, V. new(rcv_msg(S, D, V)) <-> (rcv_msg(S, D, V) | (S = s & D = n & V = v)) )
& ( forall S, D. new(rcv_msg_proj(S, D)) <-> (rcv_msg_proj(S, D) | (S = s & D = n)) )
& ( !(exists A. forall N. member_a(N,A) -> new(rcv_msg_proj(N,n))) )

transition receive_msg_1(n: node, s: node, v: value, u: value, w: value)
modifies rcv_msg, rcv_msg_proj, dec, und_cons, done
& ( !done(n) )
& ( sent_msg(s,n,v) )
& ( forall S, D, V. new(rcv_msg(S, D, V)) <-> (rcv_msg(S, D, V) | (S = s & D = n & V = v)) )
& ( forall S, D. new(rcv_msg_proj(S, D)) <-> (rcv_msg_proj(S, D) | (S = s & D = n)) )
& ( exists A. forall N. member_a(N,A) -> new(rcv_msg_proj(N,n)) )
& ( if exists U. exists B. forall N. member_b(N, B) -> new(rcv_msg(N, n, U)) then
& ( exists B. forall N. member_b(N, B) -> new(rcv_msg(N, n, u)) )
& (forall N, V. new(dec(N, V)) <-> (dec(N, V) | (N = n & V = u)) )
else
(forall N, V. new(dec(N, V)) <-> dec(N, V))
)
& ( exists C. forall N. member_c(N, C) -> new(rcv_msg(N, n, w)) )
& ( forall N, V. new(und_cons(N, V)) <-> (und_cons(N, V) | (N = n & V = w) ) )
& ( forall N. new(done(N)) <-> (done(N) | N = n) )

transition receive_msg_2(n: node, s: node, v: value, u: value, w: value)
modifies rcv_msg, rcv_msg_proj, dec, und_cons, done
& ( !done(n) )
& ( sent_msg(s,n,v) )
& ( forall S, D, V. new(rcv_msg(S, D, V)) <-> (rcv_msg(S, D, V) | (S = s & D = n & V = v)) )
& ( forall S, D. new(rcv_msg_proj(S, D)) <-> (rcv_msg_proj(S, D) | (S = s & D = n)) )
& ( exists A. forall N. member_a(N,A) -> new(rcv_msg_proj(N,n)) )
& ( if exists U. exists B. forall N. member_b(N, B) -> new(rcv_msg(N, n, U)) then
& ( exists B. forall N. member_b(N, B) -> new(rcv_msg(N, n, u)) )
& ( forall N, V. new(dec(N, V)) <-> (dec(N, V) | (N = n & V = u)) )
else
(forall N, V. new(dec(N, V)) <-> dec(N, V))
)
& ( !exists W,C. forall N. member_c(N, C) -> new(rcv_msg(N, n, W)) )
& input(n, w)
& ( forall N, V. new(und_cons(N, V)) <-> (und_cons(N, V) | (N = n & V = w) ) )
& ( forall N. new(done(N)) <-> (done(N) | N = n) )

transition receive_msg_3(n: node, s: node, v: value, u: value, w: value)
modifies rcv_msg, rcv_msg_proj, dec, und_cons, done
& ( !done(n) )
& ( sent_msg(s,n,v) )
& ( forall S, D, V. new(rcv_msg(S, D, V)) <-> (rcv_msg(S, D, V) | (S = s & D = n & V = v)) )
& ( forall S, D. new(rcv_msg_proj(S, D)) <-> (rcv_msg_proj(S, D) | (S = s & D = n)) )
& ( exists A. forall N. member_a(N,A) -> new(rcv_msg_proj(N,n)) )
& ( if exists U. exists B. forall N. member_b(N, B) -> new(rcv_msg(N, n, U)) then
& ( exists B. forall N. member_b(N, B) -> new(rcv_msg(N, n, u)) )
& ( forall N, V. new(dec(N, V)) <-> (dec(N, V) | (N = n & V = u)) )
else
(forall N, V. new(dec(N, V)) <-> dec(N, V))
)
& ( exists U1,U2,C1,C2.
& U1 != U2
& (forall N. member_c(N, C1) -> new(rcv_msg(N, n, U1)))
& (forall N. member_c(N, C2) -> new(rcv_msg(N, n, U2)))
)
& input(n, w)
& ( forall N, V. new(und_cons(N, V)) <-> (und_cons(N, V) | (N = n & V = w) ) )
& ( forall N. new(done(N)) <-> (done(N) | N = n) )

transition underlying_consensus(v:value)
modifies und_cons_dec
& ( forall V. !und_cons_dec(V) ) # from agreement
& ( | ( exists N. !member_f(N) & und_cons(N, v) )
| ( exists N1,N2,V1,V2.
& !member_f(N1)
& !member_f(N2)
& und_cons(N1, V1)
& und_cons(N2, V2)
& V1 != V2
)
)
& ( forall V. new(und_cons_dec(V)) <-> (und_cons_dec(V) | V = v) )

################################################################################
#
# Safety property
#
################################################################################

safety [agreement1] forall N1, N2, V1, V2. !member_f(N1) & !member_f(N2) & dec(N1,V1) & dec(N2,V2) -> V1 = V2 # agreement (lemma 3)
safety [agreement2] forall N, V1, V2. !member_f(N) & dec(N,V1) & und_cons_dec(V2) -> V1 = V2 # ultimate agreement
safety [validity1] forall V1, V2. ((forall N:node. !member_f(N) -> input(N,V1)) & V1 != V2) -> (forall M. !member_f(M) -> !dec(M,V2)) # validity
safety [validity2] forall V1, V2. (forall N:node. !member_f(N) -> input(N,V1)) & V1 != V2 -> !und_cons_dec(V2) # validity

################################################################################
#
# Inductive invariant
#
################################################################################

# properties of projections
invariant [lemma] sent_msg(N1,N2,V) -> sent_msg_proj(N1,N2)
invariant [lemma] rcv_msg(N1,N2,V) -> rcv_msg_proj(N1,N2)
invariant [lemma] !member_f(N1) & !member_f(N2) & sent_msg(N1,N2,V) & rcv_msg_proj(N1,N2) -> rcv_msg(N1,N2,V)

# simple universal properties
invariant [lemma] !member_f(N1) -> (sent_msg(N1,N2,V) <-> input(N1,V))
invariant [lemma] !member_f(N) & und_cons(N,V1) & und_cons(N,V2) -> V1 = V2
invariant [lemma] !member_f(N) & und_cons(N,V) -> done(N)
invariant [lemma] !member_f(N2) & rcv_msg(N1,N2,V) -> sent_msg(N1,N2,V)

# "choosable"
# invariant [free_lemma] (exists N. !member_f(N) & dec(N,V)) -> (exists B. forall M. member_b(M,B) & !member_f(M) -> sent_msg(M,M,V))
invariant forall V. (forall N. member_f(N) | !dec(N,V)) | (exists B. forall M. !member_b(M,B) | member_f(M) | sent_msg(M,M,V))
invariant forall V. (exists N. !member_f(N) & done(N) & !und_cons(N,V)) -> !(exists B. forall M. member_b(M,B) & !member_f(M) -> sent_msg(M,M,V))

# property of und_cons_dec
invariant [lemma] (forall V. und_cons_dec(V) -> exists N. !member_f(N) & und_cons(N,V)) |
(exists N1,N2,V1,V2. !member_f(N1) & !member_f(N2) & und_cons(N1,V1) & und_cons(N2,V2) & V1 != V2)

################################################################################
#
# sanity checks using trace
#
################################################################################

unsat trace {
underlying_consensus

}

# TODO: add more, the following diverges because of the "any transition"
# sat trace {
# any transition
# underlying_consensus
# }
Loading

0 comments on commit 7b4f612

Please sign in to comment.