aman-goel / ic3po Goto Github PK

#lang ivy1.7

module total_order_with_zero(t) = {
    axiom (T:t < U & U < V) -> (T < V)  # Transitivity
    axiom ~(T:t < U & U < T)            # Anti-symmetry
    axiom T:t < U | T = U | U < T       # Totality
    axiom 0 <= X:t
}

type ballot
instantiate total_order_with_zero(ballot)

type acceptor
type proposer
type value
type quorum # majority


# Each ballot(proposal number) should correspond to only one proposer and one value
function get_proposer(B:ballot) : proposer
function get_value(B:ballot) : value

# Note that we only use axioms to describe the abstract characteristics 
# of 'member' instead of assigning any actual values to it
relation member(A:acceptor, Q:quorum)
axiom forall Q1, Q2. exists A. member(A, Q1) & member(A, Q2)


# For Acceptor: ballots that have already been accepted
relation accepted_ballots(A:acceptor, B:ballot)

# A ballot 'B' with value 'V' to acceptor 'A' has been sent out (but can be dropped)
relation ballot_is_sent(A:acceptor, B:ballot, V: value)

# Acceptor 'A' has sent an ack to the proposer that is responsible for ballot 'B'
relation sent_ack(A: acceptor, B:ballot)

after init {
    accepted_ballots(A, B) := false;
    # We want ballot number 0 (which is invalid ballot) stands out
    # when no valid ballot is accepted 
    accepted_ballots(A, 0) := true;
    ballot_is_sent(A, B, V) := false;
    sent_ack(A, B) := false;
}

####### For 1a #######

# There is no action for one_a. When IVy calls one_b it means some proposer has called
# one_a.

####### For 1b #######

# Acceptor 'a' receives a prepare request with number 'b'
# It's possible to accept duplicate ballot
action one_b(a:acceptor, current_promise:ballot, b:ballot) = {
    require 0 < b;
    require sent_ack(a, current_promise) & forall B:ballot. sent_ack(a, B)
        -> B <= current_promise | (current_promise = 0 & forall P. ~sent_ack(a, P));

    if(current_promise <= b) {
        sent_ack(a, b) := true;
    }
}

####### For 2a #######

# q: the quorum from which ACKs has been collected
# a, b, v: A proposer wants to send ballot 'b' to acceptor 'a'
# 'a' is not necessarily within the quorum
action two_a(a:acceptor, b:ballot, q:quorum, maxb:ballot) = {
    require forall A. (member(A, q) & sent_ack(A, b));
    # make sure maxb is really maxb
    require (exists A. (member(A, q) & accepted_ballots(A, maxb))) &
        (forall A1. member(A1, q) & forall B1. (accepted_ballots(A1, B1) -> B1 <= maxb));
    var maxb_val:value;
    # This has already included both case 1 where no accepted proposal has been accepted by a majority and
    # case 2 where some accepted proposals have been accepted
    # If maxb = 0, then the non-deterministic value from get_value is used.
    maxb_val := get_value(maxb);
    ballot_is_sent(a, b, maxb_val) := true;
}

action two_b(a:acceptor, b:ballot, v:value, current_promise:ballot) = {
    # Update accepted_ballots
    # Some proposer must have sent ballot 'b' to 'a' and 'b' must >= promise(a)
    require sent_ack(a, current_promise) & forall B:ballot. sent_ack(a, B)
        -> B <= current_promise | (current_promise = 0 & forall P. ~sent_ack(a, P));
    require (ballot_is_sent(a, b, v) & current_promise <= b);
    get_value(b) := v;
    accepted_ballots(a, b) := true;
}


####### Actions exported to the environment #######
export one_b
export two_a
export two_b

invariant forall B1, B2. (
                (exists Q. (forall A. member(A, Q) & accepted_ballots(A, B1))) &
                (exists Q. (forall A. member(A, Q) & accepted_ballots(A, B2)))
            ) -> get_value(B1) = get_value(B2)

> python2 ic3po.py -o foo -n bar ivy_paxos/paxos.ivy
------------------------------------------------------------------------
IC3PO: IC3 for Proving Protocol Properties
copyright (c) 2021  Aman Goel and Karem Sakallah, University of Michigan
------------------------------------------------------------------------

        (output dir: foo/bar)
        (frontend: ivy)
        (converting: ivy -> vmt)
Traceback (most recent call last):
  File "/root/ic3po/ic3po/ivy_to_vmt.py", line 599, in <module>
    main()
  File "/root/ic3po/ic3po/ivy_to_vmt.py", line 594, in main
    print_module()
  File "/root/ic3po/ic3po/ivy_to_vmt.py", line 574, in print_module
    print_isolate()
  File "/root/ic3po/ic3po/ivy_to_vmt.py", line 554, in print_isolate
    print_module_vmt(mod)
  File "/root/ic3po/ic3po/ivy_to_vmt.py", line 63, in __init__
    self.execute()
  File "/root/ic3po/ic3po/ivy_to_vmt.py", line 97, in execute
    self.process_actions()
  File "/root/ic3po/ic3po/ivy_to_vmt.py", line 348, in process_actions
    sf = self.standardize_action(f, update[0], name)
  File "/root/ic3po/ic3po/ivy_to_vmt.py", line 405, in standardize_action
    action = lgu.substitute(f, subs)
  File "/usr/local/lib/python2.7/dist-packages/ms_ivy-0.3-py2.7.egg/ivy/logic_util.py", line 156, in substitute
    return type(t)(*(substitute(x, subs) for x in t))
  File "/usr/local/lib/python2.7/dist-packages/ms_ivy-0.3-py2.7.egg/ivy/logic_util.py", line 156, in <genexpr>
    return type(t)(*(substitute(x, subs) for x in t))
  File "/usr/local/lib/python2.7/dist-packages/ms_ivy-0.3-py2.7.egg/ivy/logic_util.py", line 166, in substitute
    raise CaptureError(forbidden_variables.intersection(t.variables))
ivy.logic_util.CaptureError
Traceback (most recent call last):
  File "ic3po.py", line 182, in <module>
    main()
  File "ic3po.py", line 138, in main
    raise Exception("conversion error: return code %d" % s)
Exception: conversion error: return code 1

(declare-sort id 0)
(declare-sort node 0)

(define-fun .id ((S id)) id (! S :sort 0))
(define-fun .node ((S node)) node (! S :sort 0))

(declare-fun __trans.forward (id node) Bool)
(declare-fun __spec.leader (node) Bool)
(declare-fun __trans.elected (node) Bool)

(declare-fun trans.forward (id node) Bool)
(declare-fun spec.leader (node) Bool)
(declare-fun trans.elected (node) Bool)

(define-fun .trans.forward ((V0 id) (V1 node)) Bool (! (__trans.forward V0 V1) :next trans.forward))
(define-fun .spec.leader ((V0 node)) Bool (! (__spec.leader V0) :next spec.leader))
(define-fun .trans.elected ((V0 node)) Bool (! (__trans.elected V0) :next trans.elected))

(declare-fun idn (node) id)
(declare-fun id_0 () id)
(declare-fun node.max () node)
(declare-fun node_0 () node)
(declare-fun id_< (id id) Bool)
(declare-fun ring.btw (node node node) Bool)
(declare-fun id.succ (id id) Bool)

(define-fun .idn ((V0 node)) id (! (idn V0) :global true))
(define-fun .id_0 () id (! id_0 :global true))
(define-fun .node.max () node (! node.max :global true))
(define-fun .node_0 () node (! node_0 :global true))
(define-fun .id_< ((V0 id) (V1 id)) Bool (! (id_< V0 V1) :global true))
(define-fun .ring.btw ((V0 node) (V1 node) (V2 node)) Bool (! (ring.btw V0 V1 V2) :global true))
(define-fun .id.succ ((V0 id) (V1 id)) Bool (! (id.succ V0 V1) :global true))

(declare-fun __ts0_a () Bool)
(declare-fun __ts0_b () Bool)

(define-fun .prop () Bool (! 
 (let (($v (forall ((N node)) (=> (__trans.elected N) (__spec.leader N)))
 ))
 (and $v))
 :invar-property 0))

(define-fun .axiom () Bool (! 
 (let (($v (and (forall ((N1 node) (N2 node)) (=> (= (idn N1) (idn N2)) (= N1 N2))) (forall ((X id) (Y id) (Z id)) (=> (id.succ X Z) (and (id_< X Z) (not (and (id_< X Y) (id_< Y Z)))))) (forall ((T id) (U id) (V id)) (=> (and (id_< T U) (id_< U V)) (id_< T V))) (forall ((T id) (U id)) (not (and (id_< T U) (id_< U T)))) (forall ((T id) (U id)) (or (id_< T U) (= T U) (id_< U T))) (forall ((X id)) (not (id_< X id_0))) (forall ((W node) (X node) (Y node) (Z node)) (=> (and (ring.btw W X Y) (ring.btw W Y Z)) (ring.btw W X Z))) (forall ((W node) (X node) (Y node)) (=> (ring.btw W X Y) (not (ring.btw W Y X)))) (forall ((W node) (X node) (Y node)) (or (ring.btw W X Y) (ring.btw W Y X) (= W X) (= W Y) (= X Y))) (forall ((X node) (Y node) (Z node)) (=> (ring.btw X Y Z) (ring.btw Y Z X))))
 ))
 (and $v))
 :axiom true))

(define-fun .init () Bool (! 
 (let (($v (and (forall ((V0 id) (V1 node)) (= (__trans.forward V0 V1) false)) (forall ((V0 node)) (= (__trans.elected V0) false)) (forall ((V0 node)) (= (__spec.leader V0) false)))
 ))
 (and $v))
 :init true))

(define-fun .action_ext:system.server.timer.timeout () Bool (! 
 (let (($v (exists ((Vtmp__fml:y node) (Vtmp__new_fml:dst node) (Vtmp__new_fml:i id) (Vtmp__new_fml:src node) (Vtmp__new_fml:x node) (Vtmp__new_loc:0 node) (Vtmp__prm:V0 node)) (and (= Vtmp__new_fml:x Vtmp__prm:V0) (= Vtmp__new_loc:0 Vtmp__fml:y) (= Vtmp__new_fml:src Vtmp__prm:V0) (= Vtmp__new_fml:dst Vtmp__new_loc:0) (= Vtmp__new_fml:i (idn Vtmp__prm:V0)) (forall ((V0 id) (V1 node)) (= (trans.forward V0 V1) (ite (and (= V0 Vtmp__new_fml:i) (= V1 Vtmp__new_fml:dst)) true (__trans.forward V0 V1)))) (=> (not (= node_0 node.max)) (not (= Vtmp__new_fml:x Vtmp__fml:y))) (forall ((Z node)) (=> (and (not (= Z Vtmp__new_fml:x)) (not (= Z Vtmp__fml:y))) (ring.btw Vtmp__new_fml:x Vtmp__fml:y Z)))))
 ))
 (and $v))
 :action ext:system.server.timer.timeout))

(define-fun .action_ext:trans.recv_elected () Bool (! 
 (let (($v (exists ((Vtmp__fml:dst node)) (__trans.elected Vtmp__fml:dst))
 ))
 (and $v))
 :action ext:trans.recv_elected))

(define-fun .action_ext:trans.recv_forward () Bool (! 
 (let (($v (exists ((Vtmp__fml:dst node) (Vtmp__fml:i id) (Vtmp__fml:y node) (Vtmp__ts0__new_fml:dst_a_a node) (Vtmp__ts0__new_fml:n node) (Vtmp__ts0__new_fml:src_a node) (Vtmp__ts0__ts0__new_fml:dst_a_a node) (Vtmp__ts0__ts0__new_fml:i_a_a id) (Vtmp__ts0__ts0__new_fml:src_a node) (Vtmp__ts0__ts0__new_fml:x_a node) (Vtmp__ts0__ts0__new_loc:0_a node)) (and (= Vtmp__ts0__ts0__new_fml:i_a_a Vtmp__fml:i) (= Vtmp__ts0__ts0__new_loc:0_a Vtmp__fml:y) (= Vtmp__ts0__new_fml:dst_a_a Vtmp__fml:dst) (= __ts0_a (ite __ts0_b (forall ((N node)) (=> (not (= N Vtmp__ts0__new_fml:n)) (not (__spec.leader N)))) (id_< (idn Vtmp__fml:dst) Vtmp__fml:i))) (= Vtmp__ts0__ts0__new_fml:dst_a_a Vtmp__ts0__ts0__new_loc:0_a) (= Vtmp__ts0__ts0__new_fml:x_a Vtmp__fml:dst) (= Vtmp__ts0__ts0__new_fml:src_a Vtmp__fml:dst) (= Vtmp__ts0__new_fml:n Vtmp__fml:dst) (forall ((V0 node)) (= (spec.leader V0) (ite __ts0_b (ite __ts0_a (ite (= V0 Vtmp__ts0__new_fml:n) true (__spec.leader V0)) (__spec.leader V0)) (__spec.leader V0)))) (forall ((V0 id) (V1 node)) (= (trans.forward V0 V1) (ite __ts0_b (__trans.forward V0 V1) (ite __ts0_a (ite (and (= V0 Vtmp__ts0__ts0__new_fml:i_a_a) (= V1 Vtmp__ts0__ts0__new_fml:dst_a_a)) true (__trans.forward V0 V1)) (__trans.forward V0 V1))))) (forall ((V0 node)) (= (trans.elected V0) (ite __ts0_b (ite (= V0 Vtmp__ts0__new_fml:dst_a_a) true (__trans.elected V0)) (__trans.elected V0)))) (= Vtmp__ts0__new_fml:src_a Vtmp__fml:dst) (= __ts0_b (= Vtmp__fml:i (idn Vtmp__fml:dst))) (__trans.forward Vtmp__fml:i Vtmp__fml:dst) (or __ts0_b (or (not __ts0_a) (=> (not (= node_0 node.max)) (not (= Vtmp__ts0__ts0__new_fml:x_a Vtmp__fml:y))))) (forall ((Z node)) (or __ts0_b (or (not __ts0_a) (=> (and (not (= Z Vtmp__ts0__ts0__new_fml:x_a)) (not (= Z Vtmp__fml:y))) (ring.btw Vtmp__ts0__ts0__new_fml:x_a Vtmp__fml:y Z)))))))
 ))
 (and $v))
 :action ext:trans.recv_forward))