aman-goel / ic3po Goto Github PK
View Code? Open in Web Editor NEWIC3PO: IC3 for Proving Protocol Properties
License: GNU General Public License v3.0
IC3PO: IC3 for Proving Protocol Properties
License: GNU General Public License v3.0
Hi, thanks for the amazing tool!
I am using commit e44f6f9. I'm new to Ivy language and recently I have been trying out IC3PO to see if it can infer inductive invariants for my ivy specification. I have written a toy paxos.ivy and it can be parsed by Ivy 1.7. However, for some reason I can't get IC3PO to work on it.
Here's the paxos.ivy:
#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)
And after running ic3po, I get:
> 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
My best guess is that I might have used some Ivy features that are not currently supported by the tool? Or maybe there are just some hidden problems in my Ivy code?
Any feedback or directions would be extremely helpful.
Thank you very much!
I found that the default ic3po doesn't perform the unbounded induction check, and may produce incorrect invariant. I ran this example with python2 ic3po.py -n leader ../leader.vmt --size id=3,node=2
on this vmt file:
(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))
Do you have any idea about this problem?
A declarative, efficient, and flexible JavaScript library for building user interfaces.
๐ Vue.js is a progressive, incrementally-adoptable JavaScript framework for building UI on the web.
TypeScript is a superset of JavaScript that compiles to clean JavaScript output.
An Open Source Machine Learning Framework for Everyone
The Web framework for perfectionists with deadlines.
A PHP framework for web artisans
Bring data to life with SVG, Canvas and HTML. ๐๐๐
JavaScript (JS) is a lightweight interpreted programming language with first-class functions.
Some thing interesting about web. New door for the world.
A server is a program made to process requests and deliver data to clients.
Machine learning is a way of modeling and interpreting data that allows a piece of software to respond intelligently.
Some thing interesting about visualization, use data art
Some thing interesting about game, make everyone happy.
We are working to build community through open source technology. NB: members must have two-factor auth.
Open source projects and samples from Microsoft.
Google โค๏ธ Open Source for everyone.
Alibaba Open Source for everyone
Data-Driven Documents codes.
China tencent open source team.