зеркало из https://github.com/microsoft/ivy.git
404 строки
12 KiB
XML
404 строки
12 KiB
XML
#lang ivy1.7
|
|
|
|
include order
|
|
|
|
type node
|
|
|
|
instance epochobj : unbounded_sequence
|
|
alias epoch = epochobj.t
|
|
|
|
instance stakeord : unbounded_sequence
|
|
alias stake = stakeord.t
|
|
|
|
axiom 0 <= X:epoch
|
|
axiom X:stake >= 0
|
|
axiom ~(X:stake < 0)
|
|
axiom X:stake < Y -> Y ~= 0
|
|
axiom X:stake = Y -> (X = 0 <-> Y = 0)
|
|
axiom X:stake < Y | X ~= 0 | Y = 0
|
|
|
|
instance inst_object : unbounded_sequence
|
|
alias inst = inst_object.t
|
|
|
|
axiom ~(T:epoch < T)
|
|
axiom X:epoch < Y -> Y ~= 0
|
|
axiom X:epoch = Y -> (X = 0 <-> Y = 0)
|
|
axiom X:epoch < Y | X ~= 0 | Y = 0
|
|
|
|
type value
|
|
|
|
type config
|
|
relation val_at(C:config, I:inst, V:value)
|
|
|
|
object nodeset = {
|
|
type set
|
|
relation member(N:node,S:set)
|
|
relation majority(S:set)
|
|
function common(S:set,T:set) : node
|
|
axiom majority(S) & majority(T) & N = common(S,T) -> member(N,S) & member(N,T)
|
|
}
|
|
|
|
function leader_of(E:epoch) : node
|
|
|
|
relation wedge_msg(E:epoch, S:stake)
|
|
relation wedge_ack_msg(E:epoch, N:node, S1:stake, S2:stake, C:config)
|
|
relation accept_msg(E:epoch, S:stake, C:config)
|
|
relation accepted_msg(E:epoch, N:node, S:stake, C:config)
|
|
relation wedged(E:epoch, N:node)
|
|
relation started(E:epoch, N:node) # TODO: add nodes and nodesets
|
|
function config_decided(E:epoch) : config # ghost relation
|
|
|
|
# derived relations:
|
|
function node_stake(E:epoch, N:node) : stake
|
|
|
|
relation proposal(E:epoch, I:inst, V:value)
|
|
relation vote(E:epoch, N:node, I:inst, V:value)
|
|
relation decision(E:epoch, N:node, I:inst, V:value)
|
|
relation transferral(E:epoch, N:node, I:inst, V:value)
|
|
|
|
# records past decisions of any epoch or node
|
|
|
|
relation any_decision(I:inst, V:value)
|
|
function dec_maj(I:inst, V:value) : nodeset.set # records majority for decision
|
|
function dec_epoch(I:inst, V:value) : epoch
|
|
function accept_maj(E:epoch,K:stake) : nodeset.set
|
|
function epoch_maj(E:epoch) : nodeset.set # The majority that finished epoch E
|
|
relation epoch_ended(E:epoch)
|
|
function epoch_stake(E:epoch) : stake
|
|
function left_maj(E:epoch,K:stake) : nodeset.set
|
|
function accepted_maj(E:epoch) : nodeset.set
|
|
|
|
after init {
|
|
wedge_msg(E,S) := false;
|
|
wedge_ack_msg(E,N,S1,S2,C2) := false;
|
|
accept_msg(E,S,C2) := false;
|
|
accepted_msg(E,N,S,C) := false;
|
|
proposal(E,I,V) := false;
|
|
vote(E,N,I,V) := false;
|
|
decision(E,N,I,V) := false;
|
|
any_decision(I,V) := false;
|
|
transferral(E,N,I,V) := false;
|
|
node_stake(E,N) := 0;
|
|
wedged(E,N) := false;
|
|
started(E,N) := E = 0;
|
|
epoch_ended(E) := false;
|
|
}
|
|
|
|
# a client sends a wedge message:
|
|
action send_wedge (e:epoch,s:stake) = { # TODO add nodeset.sets and membershipt
|
|
require s ~= 0;
|
|
wedge_msg(e,s) := true
|
|
}
|
|
|
|
action join_stake (e:epoch, n:node, s:stake) = {
|
|
require s ~= 0;
|
|
require started(e,n);
|
|
require wedge_msg(e,s);
|
|
require node_stake(e,n) < s;
|
|
wedged(e,n) := true;
|
|
node_stake(e,n) := s;
|
|
}
|
|
|
|
action receive_wedge_ack_msgs(e:epoch, s:stake, nset:nodeset.set, maxs : stake, n: node, c : config) = {
|
|
|
|
require s ~= 0;
|
|
assume forall C. ~accept_msg(e,s,C);
|
|
require forall N. nodeset.member(N,nset) -> ~(node_stake(e,N) < s);
|
|
require nodeset.majority(nset);
|
|
|
|
if maxs = 0 {
|
|
# if no stake, n must have the exact configuration and it must be maximal
|
|
require nodeset.member(n,nset) & forall I,V . val_at(c,I,V) <-> (vote(e,n,I,V) | transferral(e,n,I,V));
|
|
require forall N,I,V. nodeset.member(N,nset) & (vote(e, N, I, V) | transferral(e,N,I,V)) -> val_at(c, I, V);
|
|
require forall N,S,C. 0 < S & S < s & nodeset.member(N, nset) -> ~accepted_msg(e,N,S,C);
|
|
accept_maj(e,s) := nset;
|
|
} else {
|
|
# if stake, n must have accepted at the stake and stake must be maximal
|
|
require maxs < s & nodeset.member(n, nset) & accepted_msg(e,n,maxs,c);
|
|
require forall N,MAXS,C. (MAXS < s & nodeset.member(N, nset) & accepted_msg(e,N,MAXS,C)) -> MAXS <= maxs;
|
|
accept_maj(e,s) := accept_maj(e,maxs);
|
|
};
|
|
|
|
# Key invariant for stakes: when we create a new stake, all lesser stakes with different configs are
|
|
# dead. A stake is dead if there is a majority that has left it and not accepted it. The function
|
|
# left_maj records the majority that witnesses the death of a stake.
|
|
|
|
left_maj(e,K) := nset if maxs < K & K < s else left_maj(e,K);
|
|
|
|
# assert N1 = n & K2 = maxs & E1 = e & C1 = c & S1 = left_maj(E1,K) &
|
|
# 0 < K & K < s -> (accept_msg(e,K,c) | (nodeset.majority(S1) & (nodeset.member(N,S1) -> K < node_stake(e,N) & ~accepted_msg(e,N,K,C))));
|
|
assume forall K,C,N.
|
|
0 < K & K < s -> (accept_msg(e,K,c) | (nodeset.majority(left_maj(e,K)) & (nodeset.member(N,left_maj(e,K)) -> K < node_stake(e,N) & ~accepted_msg(e,N,K,C))));
|
|
|
|
|
|
# assert N1 = n & K2=maxs & E1 = e & C1 = c & S1 = accept_maj(e,s) & K = s ->
|
|
# nodeset.majority(accept_maj(e,s)) & (nodeset.member(N,accept_maj(e,s)) -> ~(node_stake(e,N) = 0) & ((vote(e, N, I, V) | transferral(e,N,I,V)) -> val_at(c, I, V)));
|
|
assume forall N,I,V. nodeset.majority(accept_maj(e,s)) & (nodeset.member(N,accept_maj(e,s)) -> ~(node_stake(e,N) = 0) & ( (vote(e, N, I, V) | transferral(e,N,I,V)) -> val_at(c, I, V)));
|
|
|
|
accept_msg(e, s, c) := true;
|
|
}
|
|
|
|
action send_accepted_msg(e:epoch, n:node, s:stake, c:config) = {
|
|
require s ~= 0;
|
|
require started(e,n);
|
|
require ~(s < node_stake(e,n));
|
|
require accept_msg(e,s,c);
|
|
accepted_msg(e, n, s, c) := true
|
|
}
|
|
|
|
|
|
action start(e:epoch, e_prev: epoch, n:node, s:stake, nset:nodeset.set, c:config) = {
|
|
require s ~= 0;
|
|
require ~started(e,n);
|
|
require nodeset.majority(nset);
|
|
require e_prev < e & forall E. ~(e_prev < E & E < e);
|
|
# require epochobj.succ(e_prev, e); # make sure e_prev is the previous epoch deterministically
|
|
require forall N. nodeset.member(N,nset) -> accepted_msg(e_prev, N, s, c);
|
|
|
|
# assert E1 = e_prev & C1 = c & C2 = config_decided(e_prev) & K = s & K2 = epoch_stake(E1) &
|
|
# S1 = left_maj(E1,K2) & S2 = accepted_maj(E1) & N = nodeset.common(S1,S2) & N1 = nodeset.common(nset,nset) &
|
|
# K2 < s -> (epoch_ended(e_prev) -> c = config_decided(e_prev));
|
|
# assert E1 = e_prev & C1 = c & C2 = config_decided(e_prev) & K = s & K2 = epoch_stake(E1) & N1 = nodeset.common(nset,nset) &
|
|
# S1 = left_maj(E1,K) & S2 = nset & N = nodeset.common(S1,S2) &
|
|
# (s < K2) -> (epoch_ended(e_prev) -> c = config_decided(e_prev));
|
|
assume epoch_ended(e_prev) -> c = config_decided(e_prev);
|
|
|
|
# assume epoch_ended(e_prev) -> s = epoch_stake(e_prev) & c = config_decided(e_prev);
|
|
# assert E1 = e_prev & K = s & C = c & N = nodeset.common(nset,nset) -> accept_msg(e_prev,s,c);
|
|
# assume accept_msg(e_prev,s,c);
|
|
|
|
# assert forall C,K,E1,N,E2. C = c & K = s & E1 = e_prev & N = nodeset.common(nset,nset) & E2 < e_prev -> epoch_ended(E2);
|
|
assume forall E2. (E2 < e_prev -> epoch_ended(E2));
|
|
|
|
assert forall C,K,E1,N,E2,N1,I,V1,S2,K2,C2. C = c & K = s & E1 = e_prev & S1 = accept_maj(E1,s) & N = nodeset.common(S1,S1) & S2 = epoch_maj(E2) & K2 = epoch_stake(E2) & C2 = config_decided(E2)
|
|
& E2 < e_prev & nodeset.member(N1,epoch_maj(E2)) & vote(E2,N1,I,V1) -> val_at(c,I,V1);
|
|
assume forall E2,N1,I,V1. E2 < e_prev & nodeset.member(N1,epoch_maj(E2)) & vote(E2,N1,I,V1) -> val_at(c,I,V1);
|
|
|
|
config_decided(e_prev) := c;
|
|
transferral(e,n,I,V) := val_at(c,I,V);
|
|
decision(e,n,I,V) := val_at(c,I,V);
|
|
started(e,n) := true;
|
|
if ~epoch_ended(e_prev) {
|
|
epoch_maj(e_prev) := accept_maj(e_prev,s);
|
|
epoch_stake(e_prev) := s;
|
|
accepted_maj(e_prev) := nset;
|
|
};
|
|
epoch_ended(e_prev) := true;
|
|
}
|
|
|
|
# the leader proposes a value to vote for at instance i.
|
|
action propose(e:epoch, i:inst, v:value) = {
|
|
require started(e,leader_of(e));
|
|
require forall BIG_I,V. i <= BIG_I -> ~transferral(e,leader_of(e),BIG_I,V);
|
|
require forall BIG_I,V. i <= BIG_I -> ~proposal(e,BIG_I,V);
|
|
|
|
proposal(e,i,v) := true
|
|
}
|
|
|
|
|
|
action do_vote(e:epoch, n:node, i:inst, v:value) = {
|
|
require started(e, n);
|
|
require ~wedged(e,n);
|
|
require proposal(e,i,v);
|
|
# assume ~(i <= I) -> exists V . vote(c,n,I,V);
|
|
|
|
vote(e, n, i, v) := true
|
|
}
|
|
|
|
|
|
action decide(e:epoch, n:node, v:value, nset:nodeset.set, i:inst) = {
|
|
require started(e, n);
|
|
require nodeset.majority(nset);
|
|
require forall N. nodeset.member(N, nset) -> vote(e, N, i, v);
|
|
|
|
|
|
# assert I = i & V1 = v & S1 = epoch_maj(E2) & S2 = dec_maj(I,V2) & N = nodeset.common(S1,S2) & E1 = e & E2 = dec_epoch(I,V2) & K = epoch_stake(E2) & C = config_decided(E2)
|
|
# & E2 < E1 & N1 = leader_of(E1) & N2 = nodeset.common(nset,nset) -> (any_decision(i,V2) -> v = V2);
|
|
# assert I = i & V1 = v & S1 = epoch_maj(E1) & S2 = nset & N = nodeset.common(S1,S2) & E1 = e & E2 = dec_epoch(I,V2) & K = epoch_stake(E1) & C = config_decided(E1)
|
|
# & E1 < E2 & N1 = leader_of(E2) & S3 = dec_maj(I,V2) & N2 = nodeset.common(S3,S3) -> (any_decision(i,V2) -> v = V2);
|
|
assume forall V2. any_decision(i,V2) -> v = V2;
|
|
decision(e, n, i, v) := true;
|
|
any_decision(i,v) := true;
|
|
dec_maj(i,v) := nset;
|
|
dec_epoch(i,v) := e;
|
|
}
|
|
|
|
# invariant ~(any_decision(I,V1) & any_decision(I,V2) & V1 ~= V2)
|
|
# proof let S1 = dec_maj(I,V1), S2 = dec_maj(I,V2), N = nodeset.common(S1,S2), E1 = dec_epoch(I,V1), E2 = dec_epoch(I,V2)
|
|
|
|
# invariant any_decision(I,V1) & dec_epoch(I,V1) < E1 & started(E1,N1) -> transferral(E1,N1,I,V1)
|
|
# proof let E2 = dec_epoch(I,V1), S1 = dec_maj(I,V1), S2 = epoch_maj(E2), N = nodeset.common(S1,S2)
|
|
|
|
# invariant E2 < E1 & nodeset.member(N,epoch_maj(E2)) & vote(E2,N,I,V1) & started(E1,N1) -> transferral(E1,N1,I,V1)
|
|
|
|
|
|
export send_wedge
|
|
export join_stake
|
|
export receive_wedge_ack_msgs
|
|
export send_accepted_msg
|
|
export start
|
|
export propose
|
|
export do_vote
|
|
export decide
|
|
|
|
|
|
|
|
|
|
schema trans1 = {
|
|
type t
|
|
function x : t
|
|
function z : t
|
|
property x = X & z = X -> x = z
|
|
}
|
|
|
|
schema trans2 = {
|
|
type t
|
|
function x : t
|
|
property Y = X -> (x = X <-> x = Y)
|
|
}
|
|
|
|
schema contra = {
|
|
type t
|
|
function x : t
|
|
property Y ~= X -> ~(x = X & x = Y)
|
|
}
|
|
|
|
# schema cong1 = {
|
|
# type t
|
|
# type u
|
|
# function x : t
|
|
# function f1(X:t) : u
|
|
# property x = X -> f1(x) = f1(X)
|
|
# }
|
|
|
|
schema cong1 = {
|
|
type t
|
|
type u
|
|
function x : t
|
|
function y : u
|
|
function f1(X:t) : u
|
|
property (f1(X) = y <-> f1(x) = y) | x ~= X
|
|
}
|
|
|
|
schema cong1b = {
|
|
type t
|
|
function x : t
|
|
function f2(X:t) : bool
|
|
property (f2(X) = f2(x)) | x ~= X
|
|
}
|
|
|
|
schema cong2 = {
|
|
type t1
|
|
type t2
|
|
type u
|
|
function x1 : t1
|
|
function x2 : t2
|
|
function y : u
|
|
function f1(X1:t1,X2:t2) : u
|
|
property (f1(X1,X2) = y <-> f1(x1,x2) = y) | x1 ~= X1 | x2 ~= X2
|
|
}
|
|
|
|
schema cong2b = {
|
|
type t1
|
|
type t2
|
|
type u
|
|
function x1 : t1
|
|
function x2 : t2
|
|
function f1(X1:t1,X2:t2) : u
|
|
property (f1(X1,X2) = f1(x1,x2)) | x1 ~= X1 | x2 ~= X2
|
|
}
|
|
|
|
schema cong3 = {
|
|
type t1
|
|
type t2
|
|
type t3
|
|
type u
|
|
function x1 : t1
|
|
function x2 : t2
|
|
function x3 : t3
|
|
function y : u
|
|
function f1(X1:t1,X2:t2,X3:t3) : u
|
|
property (f1(X1,X2,X3) = y <-> f1(x1,x2,x3) = y) | x1 ~= X1 | x2 ~= X2 | x3 ~= X3
|
|
}
|
|
|
|
schema cong3b = {
|
|
type t1
|
|
type t2
|
|
type t3
|
|
type u
|
|
function x1 : t1
|
|
function x2 : t2
|
|
function x3 : t3
|
|
function f1(X1:t1,X2:t2,X3:t3) : u
|
|
property (f1(X1,X2,X3) = f1(x1,x2,x3)) | x1 ~= X1 | x2 ~= X2 | x3 ~= X3
|
|
}
|
|
|
|
schema cong4 = {
|
|
type t1
|
|
type t2
|
|
type t3
|
|
type t4
|
|
type u
|
|
function x1 : t1
|
|
function x2 : t2
|
|
function x3 : t3
|
|
function x4 : t4
|
|
function y : u
|
|
function f1(X1:t1,X2:t2,X3:t3,X4:t4) : u
|
|
property (f1(X1,X2,X3,X4) = y <-> f1(x1,x2,x3,x4) = y) | x1 ~= X1 | x2 ~= X2 | x3 ~= X3 | x4 ~= X4
|
|
}
|
|
|
|
schema cong4b = {
|
|
type t1
|
|
type t2
|
|
type t3
|
|
type t4
|
|
type u
|
|
function x1 : t1
|
|
function x2 : t2
|
|
function x3 : t3
|
|
function x4 : t4
|
|
function f1(X1:t1,X2:t2,X3:t3,X4:t4) : u
|
|
property (f1(X1,X2,X3,X4) = f1(x1,x2,x3,x4)) | x1 ~= X1 | x2 ~= X2 | x3 ~= X3 | x4 ~= X4
|
|
}
|
|
|
|
schema lt1 = {
|
|
function x1 : stake
|
|
property ~(X < Y & Y < x1 & x1 < X)
|
|
}
|
|
|
|
schema lt2 = {
|
|
function x1 : stake
|
|
property ~(~(X < Y) & ~(x1 < X) & x1 < Y)
|
|
}
|
|
|
|
schema lt3 = {
|
|
function x1 : stake
|
|
property Y = X -> (x1 < X <-> x1 < Y)
|
|
}
|
|
|
|
schema lt4 = {
|
|
type t1
|
|
type t2
|
|
function x1 : t1
|
|
function x2 : t2
|
|
function x : stake
|
|
function f1(X1:t1,X2:t2) : stake
|
|
property (x < f1(X1,X2) <-> x < f1(x1,x2)) | x1 ~= X1 | x2 ~= X2
|
|
}
|
|
|
|
schema lt5 = {
|
|
function x1 : stake
|
|
property X = x1 -> ~(X < x1) & ~(x1 < X)
|
|
}
|
|
|
|
schema lt6 = {
|
|
type t1
|
|
type t2
|
|
function x1 : t1
|
|
function x2 : t2
|
|
function x : stake
|
|
function f1(X1:t1,X2:t2) : stake
|
|
property (f1(X1,X2) = 0 <-> f1(x1,x2) = 0) | x1 ~= X1 | x2 ~= X2
|
|
}
|