raft_logs.ivy

#lang ivy1.5

include theory

# This is a very abstraft model of Raft that considers only
# operations on logs and not leader election.

type log

# this is the prefix order on logs

relation (X:log < Y:log)

instantiate prefix_strict_order(log,<)

# a measure function on logs, totally ordered

type weight

relation (X:log < Y:log)
instantiate total_strict_order(weight,<)

individual meas(X:log) : weight

axiom (X:log < Y:log) -> (meas(X) < meas(Y))
axiom meas(X) = meas(Y) -> X = Y

# protocol nodes and sets of nodes

type node

type node_set
relation mem(N:node,S:node_set)

# is a set a majority?

relation maj(S:node_set)

# two majorities must have a node in common
axiom maj(S1) & maj(S2) -> exists N. mem(N,S1) & mem(N,S2)


# term numbers

type term
relation (X:term < Y:term)
instantiate total_strict_order_with_zero(term,<,0)

# abstract operations on logs

type elem

object logs = {

    individual get_term(l:log) : term

    action extend(l:log,e:elem,t:term) returns(lp:log) = {
	assert l < lp & get_term(lp) = term
    }

}

object proto = {
    
    individual node_logs(X:node) : log
    individual node_terms(X:node) : term
    relation leader(T:term,X:node)
    
    init ~leader(T,X)
    init node_terms(X) = 0

    action extend(n:node, e:elem) = {
	assume leader(node_terms(n),n);
	node_logs(n) := logs.extend(node_logs(n),e,node_terms(n))
    }
    
    action send_log(leader:node, dominated:node_set) = {
	assume maj(dominated);
	assume mem(X,dominated) -> (meas(node_logs(X)) < meas(node_logs(leader)) 
                                    | meas(node_logs(X)) = meas(node_logs(leader)));
	call abs_net.send_log(leader,node_logs(leader))
    }	

    action receive_log(dst:node, leader:node, l:log) = {
	if meas(node_logs(dst)) < meas(l) {
	    node_logs(dst) := l;
	    call abs_net.send_ack(dst,l)
	}
    }

    # This means log L has been committed by majority S
    relation committed(L:log,S:node_set)
    init ~committed(L,S)

    # to commit a log, we mus have a majority of nodes
    # that agree with the leader

    action commit(leader:node, dominated:node_set) = {
	assume maj(dominated);
	assume mem(X,dominated) -> node_logs(X) = node_logs(leader);
	committed(node_logs(leader),dominated) := true
    }


    conjecture committed(L,S) -> maj(S)
    conjecture committed(L,S) & mem(N,S) -> (L < node_logs(N) | L = node_logs(N))
    conjecture committed(L:log,S:node_set) & mem(N:node,S) & ~(L < node_logs(M:node) | L = node_logs(M:node)) -> meas(node_logs(M:node)) < meas(node_logs(N:node))
    conjecture ~(meas(node_logs(NO0)) < meas(LO1) & abs_net.sent(NO0,LO1))
    conjecture committed(L:log,S:node_set) & mem(N:node,S) & abs_net.sent(M,L2) &  ~(L < L2 | L = L2) -> meas(L2) < meas(node_logs(N:node))

}

object abs_net = {

    # this says leader N has sent log L
    relation sent(N:node,L:log)
    init ~(sent(N,L))

    action send_log(leader:node, l:log) = {
	sent(leader,l) := true
    }

    action send_ack(n:node, l:log) = {
	# TODO: fill this in
    }

    action receive_log(dst:node, leader:node, l:log) = {
	assert sent(leader,l)
    }
    execute receive_log before proto.receive_log
}
    
export proto.extend
export proto.send_log
export proto.receive_log
export proto.commit

isolate iso_p = proto with abs_net,logs