Summary: The 4.6.0 version of z3 produces the following error message, while 4.7.1 and 4.8.5 run without an issue. The ivy_to_cpp seems to be compatible with 4.7.1, but as previously noted 4.8.5 isn't
Details:when running a regression for the IVy models, I get the following error message with z3 4.6.0 both on MacOS Mojave and Linux. The Python executable grows in size to 50+GB (on MacOS) before this error message is displayed. The regression runs clean with z3 versions 4.7.1 and 4.8.5

What I don't know is if someone else is seeing IVy issues with using z3 4.7.1 (which was chosen based on being the next release after 4.6.0 see https://github.com/Z3Prover/z3/releases)

Traceback (most recent call last):
File "/opt/local/Library/Frameworks/Python.framework/Versions/2.7/bin/ivy_check", line 11, in
load_entry_point('ms-ivy==0.1', 'console_scripts', 'ivy_check')()
File "/opt/local/Library/Frameworks/Python.framework/Versions/2.7/lib/python2.7/site-packages/ms_ivy-0.1-py2.7.egg/ivy/ivy_check.py", line 696, in main
check_module()
File "/opt/local/Library/Frameworks/Python.framework/Versions/2.7/lib/python2.7/site-packages/ms_ivy-0.1-py2.7.egg/ivy/ivy_check.py", line 675, in check_module
check_isolate()
File "/opt/local/Library/Frameworks/Python.framework/Versions/2.7/lib/python2.7/site-packages/ms_ivy-0.1-py2.7.egg/ivy/ivy_check.py", line 544, in check_isolate
summarize_isolate(mod)
File "/opt/local/Library/Frameworks/Python.framework/Versions/2.7/lib/python2.7/site-packages/ms_ivy-0.1-py2.7.egg/ivy/ivy_check.py", line 522, in summarize_isolate
if not check_safety_in_state(mod,ag,fail,report_pass=False):
File "/opt/local/Library/Frameworks/Python.framework/Versions/2.7/lib/python2.7/site-packages/ms_ivy-0.1-py2.7.egg/ivy/ivy_check.py", line 331, in check_safety_in_state
return check_fcs_in_state(mod,ag,post,[Checker(lg.Or(),report_pass=report_pass)])
File "/opt/local/Library/Frameworks/Python.framework/Versions/2.7/lib/python2.7/site-packages/ms_ivy-0.1-py2.7.egg/ivy/ivy_check.py", line 299, in check_fcs_in_state
model = itr.small_model_clauses(clauses,ffcs,shrink=True)
File "/opt/local/Library/Frameworks/Python.framework/Versions/2.7/lib/python2.7/site-packages/ms_ivy-0.1-py2.7.egg/ivy/ivy_transrel.py", line 555, in small_model_clauses
return get_small_model(cls,ivy_logic.uninterpreted_sorts(),[],final_cond=final_cond,shrink=shrink)
File "/opt/local/Library/Frameworks/Python.framework/Versions/2.7/lib/python2.7/site-packages/ms_ivy-0.1-py2.7.egg/ivy/ivy_solver.py", line 1101, in get_small_model
res = decide(s)
File "/opt/local/Library/Frameworks/Python.framework/Versions/2.7/lib/python2.7/site-packages/ms_ivy-0.1-py2.7.egg/ivy/ivy_solver.py", line 1028, in decide
res = s.check() if atoms == None else s.check(atoms)
File "/opt/local/Library/Frameworks/Python.framework/Versions/2.7/lib/python2.7/site-packages/z3/z3.py", line 6246, in check
r = Z3_solver_check_assumptions(self.ctx.ref(), self.solver, num, _assumptions)
File "/opt/local/Library/Frameworks/Python.framework/Versions/2.7/lib/python2.7/site-packages/z3/z3core.py", line 3402, in Z3_solver_check_assumptions
_elems.Check(a0)
File "/opt/local/Library/Frameworks/Python.framework/Versions/2.7/lib/python2.7/site-packages/z3/z3core.py", line 1328, in Check
raise self.Exception(self.get_error_message(ctx, err))
z3.z3types.Z3Exception: Overflow encountered when expanding vector

This example does not check in ivy:

#lang ivy1.7

type node
isolate nset = {
    type this
    relation member(N:node, S:this)
    individual emptyset : nset
    invariant ~member(N, emptyset)
    implementation {

        relation _member(N:node, S:this)
        definition member(N, S) = _member(N, S)
        after init {
            _member(N, emptyset) := false;
        }
    }
}
with node

object localstate = {
    individual my_voters : nset
    invariant ~nset.member(VOTER, my_voters) 
    after init {
        my_voters := nset.emptyset;
    }
} #localstate

isolate ilocalstate = localstate with nset, node

The problem seems to be invariant ~nset.member(VOTER, my_voters):

$ ivy_check test.ivy 

Isolate ilocalstate:

    The inductive invariant consists of the following conjectures:
        test.ivy: line 22: localstate.invar4

    The following initializers are present:
        test.ivy: line 23: localstate.init[after5]

    Initialization must establish the invariant
        test.ivy: line 22: localstate.invar4 ... FAIL

This is strange because invariant ~member(N, emptyset) passes correctly and is exactly the same content, I expected to prove one from the other.

Notice that if I expose all the code from nset (without using the implement keyword) the code passes:

#lang ivy1.7

type node
isolate nset = {
    type this
    relation member(N:node, S:this)
    individual emptyset : nset
    invariant ~member(N, emptyset)
    #implementation {
        relation _member(N:node, S:this)
        definition member(N, S) = _member(N, S)
        after init {
            _member(N, emptyset) := false;
        }
    #}
}
with node

object localstate = {
    individual my_voters : nset
    invariant ~nset.member(VOTER, my_voters) 
    after init {
        my_voters := nset.emptyset;
    }
} #localstate

isolate ilocalstate = localstate with nset, node

I have an abstract representation of a model where I have two isolates : replica (that contains a set/array) and is totally ordered and another isolate that performs operations on a set belonging to a certain replica. I have an inductive invariant which states that for any two different replicas, if their set sizes are same, the sets have the same elements and in the same order. This fails, but the counter example produced by Ivy is giving a wrong behavior when an element is added to an array. If you look at the picture, we see that there are 3 sets and 2 replicas. The 2 replicas point to two different sets (arr = 0, arr = 1) at first, and after the add operation has been executed at replica R1 points to arr = 2 and the index remains 0. I fail to understand the reason for this behavior. How do I eliminate three sets and make the replica point to the same set as it was pointing before? Here is my code :

#lang ivy1.7
include collections
include order
include deduction

type elem
instance index : unbounded_sequence
instance arr : array(index,elem)

module total_order_properties(t) = 
{
     property [transitivity] X:t < Y & Y < Z -> X < Z
     property [antisymmetry] ~(X:t < Y & Y < X)
     property [totality] X:t < Y | X = Y | Y < X
}


isolate replica = 
{

     type this 
     function setrep(X:replica) : arr
     axiom [inejectivity] setrep(X) = setrep(Y) -> X = Y
     after init
     {
        setrep(X) := arr.create(0,0);
     }
     specification 
     {
        instantiate total_order_properties(this)
     }
     implementation 
     {
         interpret this -> bv[1]
     }
 }


isolate gset_protocol = 
{
    type this
    relation repEqual(R1:replica,R2:replica)
    relation send(R:replica,E:elem) 
    relation member(R:replica,E:elem)
    #v is a replica
    action add(v:replica,e:elem) 
    after init
    {
	#initially no replica has anything set
	send(R,E) := false;
    }
    specification 
    {

	definition member(R:replica,E:elem) = exists Z. 0 <= Z & Z < replica.setrep(R).end & replica.setrep(R).value(Z) = E
        definition repEqual(R1:replica,R2:replica) = (forall Z. 0 <= Z & Z < replica.setrep(R1).end & replica.setrep(R1).value(Z) = replica.setrep(R2).value(Z)) 

	before add 
	{
		send(v,e) := true;
	}
	after add 
	{
		send(R,e) := true;
	}
    }
    implementation 
    {
	implement add(v:replica,e:elem) 
	{
		require send(v,e);
		if (replica.setrep(v).end = 0) | ~member(v,e)
            	{
		 	replica.setrep(v) := arr.resize(replica.setrep(v),replica.setrep(v).end.next,e);
            	}

	}
    }
    private 
    {
          invariant ((R1:replica ~= R2) & (replica.setrep(R1).end = replica.setrep(R2).end) & replica.setrep(R1).end > 0) -> repEqual(R1,R2) 
    }
}with replica

interpret elem -> int
export gset_protocol.add

Hello, I think the following example from values.md should be valid, but the generated code fails to compile. Am I misunderstanding something conceptually, or is it an issue of the code generator?

isolate iso_4 = {
    type t
    interpret t -> int
    type dimension = {x,y,z}
    type my_point_t = struct {
        coords(X:dimension) : t
    }
    individual my_point : my_point_t
    export action my_action = {
        coords(my_point,x) := 1
    }
}

extract code_4 = iso_4

Hello, it seems that instantiating a module within an object or another module confuses Ivy regarding what actions should be exported.

For example, in doc/example/leader_tutorial.ivy, ivy_show isolate=leader ... reveals that node.next and node.prev are exported actions of the leader isolate. I don't think this should be the case, as those are implemented in node.iso.

Guards of while statements should take the full expression language, just like guards of conditionals, including "some". (The workaround is predictably gross.)

The following gets an internal error, but only if the instantiation is parameterized:

#lang ivy1.7
module counter(t) = {
individual val : t
after init {
val := *;
}
}
type foo
type bar
instance c(X:bar) : counter(foo)

ivy.logic.SortError: in application of new_c.val, at position 1, expected sort bar, got sort <built-in method sort of list object at 0x7f2eab94d050>

Suppose I have n nodes and I would want to send the id of a particular node to all other n - 1 nodes, on the reception of which the nodes would have to perform a certain task. I want to embed the sending of id in the form of action (say : call sendnodes(n.id, nodes) ). Here sendnodes is my action, n.id is the id of node n and nodes are the set of all other nodes.

Ex : In leader election protocol, we just have to send id to the next node only, which is fetched by get_next function. Say I would like to send id to all nodes and not just the next node and would like to do it in the form of action and not relation. However, I am not able to figure out how to do this. I can create a relation send, and set it to true for all nodes N. But that does not work in my case as I need to perform some action in each of the nodes on reception and hence I would like to have action like sendnodes. Any insights would be highly helpful to me.

#lang ivy1.7

type t 
type u
function 161auth( X : t ) : u

axiom [foo] 161auth(X) = 161auth(X)

AttributeError: 'TopSort' object has no attribute 'range'

While using Ivy for networking, based on udp_impl.ivy, I found that using the following definition of a packet:

type packet
interpret packet -> bv[16]
instance pkt_serdes : serdes(packet,bytes, ivy_binary_ser, ivy_binary_deser)
instance net : udp_impl(endpoint_id, packet, ivy_binary_ser, ivy_binary_deser)

Enables, transmitting random messages of 8bytes, with only 2bytes(16bits) that is randomly initialized, while the 6 bytes are initialized to 0x00.
The destination thus receives, 8bytes in total, rather than the expected 2bytes.

While trying to debug this issue, I found that the following script for compilation:
/ivy/ivy_to_cpp.py provides the following description for __ser:

template <class T> void __ser(ivy_ser &res, const T &inp);
template <>
void __ser<int>(ivy_ser &res, const int &inp) {
    res.set((long long)inp);
}

Which suggests that the packet is interpreted to be a long long. Is there a way, to ensure that the __ser and __deser, can be modified so that randomized data-packets of length 16bits can be generated, and no extra-padding bytes are sent on the wire?

This fails with a stack trace, but renaming one of the variables to avoid shadowing fixes it.

#lang ivy1.7

type t

axiom [my_axiom] {
    property exists N:t . forall N:t . true
}

property exists N:t . forall N:t . true
proof {
    apply my_axiom
}

While compiling tcp_test.ivy from the networking branch, I obtained the following error

# ivyc target=test tcp_test.ivy
tcp_test.ivy: line 232: error: unknown symbol: uint16.random

I believe I have installed Ivy from the main-branch.

While compiling ip_test.ivy, I found the following compilation error:

# ivyc target=test ip_test.ivy
stream.ivy: line 48: error: symbol has no interpretation: bfe[0][7] : pos -> byte

This program fails to give a CTI with the following command:

ivy ui=cti ivy_bug.ivy

#lang ivy1.5

type s
relation p(X:s)
individual v:s

relation error
init ~error
conjecture ~error

action f returns (u:s) = {
    assume p(u)
}

action action1 = {
    error := true;
    v := *;
    assume ~p(v);
    v := f
}

action action2 = {
    v := f;
    v := *
}

export action1
export action2

Hello, I noticed that ivyc sometimes gets stuck at line 3869 in ivy_to_cpp.ivy
At this location, it seems that Ivy is checking whether module axioms are satisfiable, including definitions expressed as universally quantified formulas even if they are macros. So, if you use a macro to avoid a quantifier alternation in a definition, at this point Ivy will nevertheless send a non-stratified formula to Z3, which may diverge.

When I run the following test case with command line:

ivy_check diagnose=true debug=true trace=true multicast.ivy

where multicast.ivy contains the following:

#lang ivy1.7

type proc

type msg_type = { m_init, m1, m2, m3 }

module send_mod = {
individual vec(P:proc) : bool
individual vec2(P:proc) : bool

individual msg(P:proc) : msg_type

action step = {
    while some p:proc. vec(p) {
        #       msg(p) := m1;                                                                                                                                                                                                  
        vec2(p) := true;
    }
}

}

instantiate send : send_mod

export send.step

after init {
send.vec(P) := false;
send.vec2(P) := false;
send.msg(P) := m_init;
}

conjecture ~send.vec(P)
conjecture ~send.vec2(P)

conjecture send.msg(P) ~= m2
conjecture send.msg(P) ~= m3

I get the following results

The following set of external actions must preserve the invariant:
(internal) ext:send.step
multicast.ivy: line 31: conj2 ... PASS
multicast.ivy: line 32: conj3 ... FAIL
searching for a small model... done

Trace follows...

send.vec(0) = false
send.msg(0) = m1
@P = 0
send.vec2(0) = false

multicast.ivy: line 14: send.vec2 := *
send.vec2(0) = true

--

When I comment out the conjecture ~send.vec2(P) that passes

--

In the original test case there is parameter to the step action and the condition in the loop is along the lines of "vec(p) & p~=param_p" and a msg is sent for the p meeting that condition

Please comment on if IVy is working as expected

I've downloaded the networking branch of Ivy and tried to build Ivy from source. I obtained the following errors

# python ./build_submodules.py 
python scripts/mk_make.py --python --prefix /home/docker/ivy_networking/ivy --pypkgdir /home/docker/ivy_networking/ivy/ivy/
python: can't open file 'scripts/mk_make.py': [Errno 2] No such file or directory

# python setup.py 
usage: setup.py [global_opts] cmd1 [cmd1_opts] [cmd2 [cmd2_opts] ...]
   or: setup.py --help [cmd1 cmd2 ...]
   or: setup.py --help-commands
   or: setup.py cmd --help

error: no commands supplied

Hello, the following simple example fails with No property thm1 exists in the current context.
Can I use theorems like that or am I misunderstanding something?

#lang ivy1.7

include deduction

theorem [thm1] {
    property true
}

invariant true
proof {
    assume thm1
}

Hello 👋

I saw the latest release is missing all language versions above 1.4. How would one go about building an up to date ms-ivy_X.X_amd64.deb file?

Thanks

Hello,

First of all, I am unable even to execute:
ivy client_server.ivy
It returns this traceback:

Traceback (most recent call last):
  File "/media/marcos/6f3d3766-82c3-49e1-8e67-22d2e9d02b22/FIB/MIRI/QP_15-16/MA/riscv/ivy/src/ivy/ivy.py", line 107, in <module>
    ui_main_loop(ivy_init())
  File "/media/marcos/6f3d3766-82c3-49e1-8e67-22d2e9d02b22/FIB/MIRI/QP_15-16/MA/riscv/ivy/src/ivy/ivy.py", line 96, in ivy_init
    source_file(fn,f)
  File "/media/marcos/6f3d3766-82c3-49e1-8e67-22d2e9d02b22/FIB/MIRI/QP_15-16/MA/riscv/ivy/src/ivy/ivy.py", line 64, in source_file
    ivy_load_file(f,**kwargs)
  File "/media/marcos/6f3d3766-82c3-49e1-8e67-22d2e9d02b22/FIB/MIRI/QP_15-16/MA/riscv/ivy/src/ivy/ivy_compiler.py", line 481, in ivy_load_file
    decls = read_module(f)
  File "/media/marcos/6f3d3766-82c3-49e1-8e67-22d2e9d02b22/FIB/MIRI/QP_15-16/MA/riscv/ivy/src/ivy/ivy_compiler.py", line 459, in read_module
    decls = parse(s,nested)
  File "/media/marcos/6f3d3766-82c3-49e1-8e67-22d2e9d02b22/FIB/MIRI/QP_15-16/MA/riscv/ivy/src/ivy/ivy_parser.py", line 980, in parse
    res = copy.copy(parser).parse(s,lexer=copy.copy(lexer))
  File "/usr/local/lib/python2.7/dist-packages/ply/yacc.py", line 331, in parse
    return self.parseopt_notrack(input, lexer, debug, tracking, tokenfunc)
  File "/usr/local/lib/python2.7/dist-packages/ply/yacc.py", line 1106, in parseopt_notrack
    p.callable(pslice)
  File "/media/marcos/6f3d3766-82c3-49e1-8e67-22d2e9d02b22/FIB/MIRI/QP_15-16/MA/riscv/ivy/src/ivy/ivy_parser.py", line 890, in p_expr_tilda_atom
    p[0] = NamedSpace(~p[2].lit)
AttributeError: 'ProductSpace' object has no attribute 'lit'

Also, concerning the tilelink example, the README inside ivy/examples/tilelink/unit_test says doing make should create two binaries, however, file tilelink_two_port_tester.ivy is not in the directory. I tried copying it from ivy/examples/tilelink/unit_test/single_client as well as doing make inside the directory where the file actually exists. The result of the make in both cases is the following:

ivy_to_cpp isolate=iso_b tilelink_two_port_tester.ivy
error: wrong number of arguments to module tl_interface
Traceback (most recent call last):
  File "/media/marcos/6f3d3766-82c3-49e1-8e67-22d2e9d02b22/FIB/MIRI/QP_15-16/MA/riscv/ivy/src/ivy/ivy_to_cpp.py", line 1256, in <module>
    ivy.ivy_init()
  File "/media/marcos/6f3d3766-82c3-49e1-8e67-22d2e9d02b22/FIB/MIRI/QP_15-16/MA/riscv/ivy/src/ivy/ivy.py", line 96, in ivy_init
    source_file(fn,f)
  File "/media/marcos/6f3d3766-82c3-49e1-8e67-22d2e9d02b22/FIB/MIRI/QP_15-16/MA/riscv/ivy/src/ivy/ivy.py", line 64, in source_file
    ivy_load_file(f,**kwargs)
  File "/media/marcos/6f3d3766-82c3-49e1-8e67-22d2e9d02b22/FIB/MIRI/QP_15-16/MA/riscv/ivy/src/ivy/ivy_compiler.py", line 481, in ivy_load_file
    decls = read_module(f)
  File "/media/marcos/6f3d3766-82c3-49e1-8e67-22d2e9d02b22/FIB/MIRI/QP_15-16/MA/riscv/ivy/src/ivy/ivy_compiler.py", line 459, in read_module
    decls = parse(s,nested)
  File "/media/marcos/6f3d3766-82c3-49e1-8e67-22d2e9d02b22/FIB/MIRI/QP_15-16/MA/riscv/ivy/src/ivy/ivy_parser.py", line 980, in parse
    res = copy.copy(parser).parse(s,lexer=copy.copy(lexer))
  File "/usr/local/lib/python2.7/dist-packages/ply/yacc.py", line 331, in parse
    return self.parseopt_notrack(input, lexer, debug, tracking, tokenfunc)
  File "/usr/local/lib/python2.7/dist-packages/ply/yacc.py", line 1106, in parseopt_notrack
    p.callable(pslice)
  File "/media/marcos/6f3d3766-82c3-49e1-8e67-22d2e9d02b22/FIB/MIRI/QP_15-16/MA/riscv/ivy/src/ivy/ivy_parser.py", line 185, in p_top_instantiate_insts
    do_insts(p[0],p[3])
  File "/media/marcos/6f3d3766-82c3-49e1-8e67-22d2e9d02b22/FIB/MIRI/QP_15-16/MA/riscv/ivy/src/ivy/ivy_parser.py", line 76, in do_insts
    raise iu.IvyError(instantiation,"wrong number of arguments to module {}".format(inst.relname))
  File "/media/marcos/6f3d3766-82c3-49e1-8e67-22d2e9d02b22/FIB/MIRI/QP_15-16/MA/riscv/ivy/src/ivy/ivy_utils.py", line 197, in __init__
    assert False
AssertionError
Makefile:9: recipe for target 'tilelink_two_port_tester.h' failed
make: *** [tilelink_two_port_tester.h] Error 1

Can you help me to generate the binaries?

Thank you in advance.

• The expression syntax construction e1 if p else e2 seems to be missing. This bit of syntax seems to be critical, as there is no other obvious way to update a non-Boolean function at many points at once.

• Another feature, type this appears in only one place, and without any explanation.

• There is reference to a nonexistent section on import "below" (and no explanation of import). It also mentions reducing the need to use old in monitors, without actually describing old.

• The even-odd example has bugs (e.g. nat := 0). It's probably a good idea to make documentation examples part of the build.

Please refer to Issue #45

After the fix there is still a failure, i.e. when I change the following (that passes)

type packet
type node

to the following:

type packet
type node = {bridge,router}

With same command line as in #45 I now get

..
Initialization must establish the invariant
learning_switch.ivy: line 24: route(N:node) ... PASS
learning_switch.ivy: line 25: route(N:node) ... PASS
learning_switch.ivy: line 26: route(N:node) ... FAIL
searching for a small model... done
warning: model doesn't give a value for enumerated term @n. returning bridge.
warning: model doesn't give a value for enumerated term @n. returning bridge.

Trace follows...

pending(0,bridge,bridge) = false
pending(0,bridge,router) = false
pending(0,router,bridge) = false
pending(0,router,router) = false
@N = bridge
@Y = bridge
@X = router
route.tc(bridge,bridge,bridge) = true
route.tc(bridge,router,router) = true
route.tc(router,bridge,bridge) = true
route.tc(router,router,router) = true
route.tc(bridge,bridge,router) = false
route.tc(bridge,router,bridge) = false
route.tc(router,bridge,router) = false
route.tc(router,router,bridge) = false
link(bridge,bridge) = false
link(bridge,router) = false
link(router,bridge) = false
link(router,router) = false
route.dom(bridge,bridge) = false
route.dom(bridge,router) = false
route.dom(router,bridge) = false
route.dom(router,router) = false

When I downgraded z3 back to 4.6.0 from 4.8.5 I needed to change the Ivy installation process in the following way. Once I installed z3 4.6.0 successfully ivy_to_cpp works again (it was running into the API changes you mentioned before).

Please update MacOS installation instructions for the z3 part

5. Install Z3
   5.1 Use pip install z3-solver when that works

sudo pip install z3-solver (will install the newest version)
sudo pip install z3-solver==4.5.1.0.post2 (will install that version)

5.2 Build the executable locally (when pip doesn't have the required version e.g. 4.6.0 when checked on 09/03/2019)
Download the following file
https://github.com/Z3Prover/z3/archive/z3-4.6.0.tar.gz

cd ~/Downloads/z3-z3-4.6.0
python scripts/mk_make.py --prefix=/opt/local/Library/Frameworks/Python.framework/Versions/2.7 --python --pypkgdir=/opt/local/Library/Frameworks/Python.framework/Versions/2.7/lib/python2.7/site-packages
cd build
make -j 4
sudo make install

To check version accessed by Ivy after 5.1 or 5.2 above

python
import z3
z3.get_version()
(4L, 6L, 0L, 0L)
indicates 4.6.0

Currently ivy deserialize for string literals produces a loop which does not advance the loop index, effectively creating an infinite loop

Look at the code extracted:

        while (pos < inp.size() && inp[pos]) {
            if (inp[pos] == '"')
                throw deser_err();
         }
        res.push_back(inp[pos++]);
     }

Additionally i think it might be better to serialize the string size at the beggining of the package rather than checking for the first '\0' tab, that is because some users might want to treat the string as a generic buffer to store any binary piece of data.

Hello, ivy_check crashes with a stack trace on the following, printing AttributeError: 'Sequence' object has no attribute 'labels'

#lang ivy1.7
include order
instance t : iterable
temporal property globally true
proof {
    tactic l2s
}

Hello, ivyc generates invalid C++ code on the example below. Should it be working?

instance elem : iterable
object obj = {
    type my_set = struct {
        member(N:elem) : bool
    }
    relation empty(S:my_set)
    definition empty(s:my_set) = forall N . ~member(s,N)
    export action emptyset returns (s:my_set) = {
        member(s,N) := false;
    }
    export action add(s:my_set, n:elem) returns (s:my_set) = {
        if ~member(s,n) {
            member(s,N) := member(s,N) | N = n
        }
    }
}
extract code = obj, elem

The following fails with error: token 'proof': syntax error.

#lang ivy1.7

type t
relation r(X:t)

export action my_action = { r(X) := true }

axiom [test] {
    property true
}

temporal property forall X . eventually r(X)
proof {
    tactic l2s with
        invariant true
        proof {
            assume test
        }
}

The documentation suggests in several places that you guys are maintaining up-to-date windows binaries, but it appears that's not the case.

I'm trying to create a random packet of a particular datatype arbit_data defined as follows

#lang ivy1.7

include ip_codec


# define a new data-type
type packetload
interpret packetload -> bv[16]



object arbitdata = { 

    object datagram = {
    type this = struct{
        load : packetload
        }

    }

    instance packet_codec : bv_codec(packetload,2)

    action decode(raw:stream) returns (dgram:datagram) = {
        require raw.end = 2;
        dgram.load := packet_codec.decode(raw,0);

    }

    action encode(dgram:datagram) returns (raw:stream) = {
        raw := raw.resize(2,0);
        raw := packet_codec.encode(raw,0,dgram.load);
    }

}

After defining the above data-type, I attempt to send randomly generated data through the UDP socket using the following script.

#lang ivy1.7

include udp_host
include udp_spec

parameter client_addr : ip.addr = 0x7f000001
parameter server_addr : ip.addr = 0x7f000001
parameter client_port : udp.port = 8008
parameter server_port : udp.port = 8585

instance udp_intf : udp_host(udp.endpoint,stream)

var udp_endpoint : udp.endpoint
var udp_sock : udp_intf.socket

after init {
    udp_endpoint := udp.endpoint.make(client_addr,client_port);
    udp_sock := udp_intf.open(udp_endpoint)            
}


include arbitdata_codec

action client_send_data(src:udp.endpoint,dst:udp.endpoint,pkt:arbitdata.datagram)
#action client_send_data(pkt:arbitdata.datagram)

implement client_send_data(src:udp.endpoint,dst:udp.endpoint,pkt:arbitdata.datagram){
#implement client_send_data(pkt:arbitdata.datagram){
    if _generating{
        
        # obtain the byte-stream payload
        var pyld := arbitdata.encode(pkt);

        if src.addr = client_addr & src.port = client_port {
            call udp_sending_pkt(dst,pyld);
            call udp_sock.send(dst,pyld);
        }

    }
}

export client_send_data
import action udp_sending_pkt(dst:udp.endpoint,pyld:stream)

I however, end up with the following error, which I do not know how to resolve.

# ivyc target=test udp_networkingref_echoclient.ivy
stream.ivy: line 49: error: cannot determine an iteration bound for loop over pos

Could you please help resolve this issue? Is there something wrong in the way I'm implementing this?

Hello, I have a case where wrapping code in "if true {...}" causes a verification condition to fail.
The code is here: https://github.com/nano-o/ivy-proofs/blob/bfbeed009f44a4d84852b7d62c7e4588f6c27f9e/multi-paxos-impl/multi_paxos_system_2.ivy

The issue can be demonstrated by running: ivy_check isolate=system.iso_model action=shim.two_b_handler.handle multi_paxos_system_2.ivy. With lines 326 and 362 of multi_paxos_system_2.ivy uncommented, it fails. Commenting them out, it passes.

Hello, I am trying to generate code using module simple_tcp, as follows:

#lang ivy1.7
include tcp
instance node : iterable
type t
interpret t -> int
instance net : simple_tcp(node, t)
export net.send
import net.recv
extract code(self:node) = net(self), node

Why I run ivyc isolate=code target=class tcp_test.ivy I get the following error:
ivy/include/1.7/tcp.ivy: line 243: error: cannot find an upper bound for loc:other
This corresponds to an existential quantification over sort node.

It seems that attribute cardinality = size in iterable should enable code generation for quantification over node, or I am doing something wrong?

I wrote something like

instance node: iterable
...
call shim.unicast(self, 0 if node.is_max(self) else node.next(self), m);

Ivy complains that ivy/include/1.7/order.ivy: line 92: guarantee ... FAIL. That assertion is assert exists S. S > x;

Once I change it to:

if node.is_max(self) {
    call shim.unicast(self, 0, m);
} else {
    call shim.unicast(self, node.next(self), m);
}

it passes.

I guess the condition may not be correctly instantiated in if-expression.

The language manual seems to say that, aside from being polymorphic, relations like < behave like other relations. However, they don't seem to shadow properly. For example:
#lang ivy1.7
type s
type t
relation lt(T:t,T1:t)
axiom X:s=0 -> X < 1
axiom X:t=0 -> lt(X,1)
object o = {
relation (S:s < S:s) # this should shadow the outer < on s
relation lt(T:t,T:t) # this does shadow the outer lt on t
action testS = { var x:s; assert x=0 -> x < 1 } # succeeds (but should fail)
action testT = { var x:t; assert x=0 -> lt(x,1) } # fails (as it should)
}

Proper shadowing for built in relations is useful, as it allows theories over a single relation to be written using built in relational symbols and instantiated with non-relational symbols without having to commit the type being axiomatized to using that symbol with the same meaning.

The lack of proper shadowing for interpreted types also leads to inconsistency (though perhaps this is really a different issue):
#lang ivy1.7
type nat
interpret nat->nat
relation (N:nat < N:nat)
definition (N:nat < N1) = true
invariant X:nat<X
invariant false

When I try ivy_check on oddeven2.ivy (or on the text taken from the language manual), I get the following error message:

Isolate evens:
error: The verification condition is not in the fragment FAU.

The following terms may generate an infinite sequence of instantiations:

test.ivy: nat.even(N_a + 1)
(position 0 is a function from nat to nat)

I tried reinstalling and still get the same error.

I'm trying to implement a complex protocol.

I first made a virtual network to help me to prove my protocol. And then, I introduce the real network and show that the messages in the real network are equivalent to the virtual network. However, When I want to extract the implementation, Ivy complains that function calls to the virtual network may have visible effect.

I found that it is because I have a precondition that the message exists in the virtual network in my proof. Although I don't want to include the virtual network in my implementation, Ivy still generates these functions and checks these preconditions at the run time. I'm wondering if it is possible to remove the precondition checks for these internal actions, as we have already proved it.

Also, I'm wondering if there is any way to bypass it.

Hello, I would like to verify the liveness property below with the l2s tactic (as in test_liveness2.ivy). This fails with a Python stack trace. Is such a proof possible at this time?

#lang ivy1.7

type node
type value
type quorum
relation member(N:node, Q:quorum)
axiom exists N . member(N,Q1) & member(N,Q2)
relation proposal(N:node,V:value)
relation decision(N:node,V:value)
relation received(N:node,M:node,V:value)
after init {
  proposal(N,V) := false;
  decision(N,V) := false;
  received(N,M,V) := false;
}
export action propose(n:node, v:value) = {
  assume ~proposal(n,V); # never proposed before
  proposal(n,v) := true;
}
export action receive(n:node, m:node, v:value) = {
    assume proposal(m,v);
    received(n,m,v) := true;
}
export action decide(n:node, v:value, q:quorum) = {
  assume forall N . member(N,q) -> received(n,N,v);
  decision(n,v) := true;
}
# safety proof:
invariant [safety] decision(N1,V1) & decision(N2,V2) -> V1 = V2
invariant proposal(N,V1) & proposal(N,V2) -> V1 = V2
invariant received(N,M,V) -> proposal(M,V)
invariant decision(N,V) -> exists Q . forall N . member(N,Q) -> proposal(N,V)
# liveness property:
individual q:quorum
individual v:value
temporal property (
    (forall N,V . globally member(N,q) & proposal(N,V) -> V = v) &
    (forall N . exists V . eventually proposal(N,V)) &
    (forall N,M,V . globally proposal(N,V) -> eventually received(M,N,V))
) -> eventually forall N . decision(N,v)
proof {
    tactic l2s
}

Hello, the generated code for impl crashes at runtime with the following error, although ivy_check does not complain.

terminate called after throwing an instance of 'std::logic_error'
  what():  basic_string::_M_construct null not valid

#lang ivy1.7

type t
interpret t -> strlit
individual x:t
action my_action(x:t) = {
}
after init {
    call my_action(0);
}

extract impl = this

Hi,

The installation instructions we've come up with at Apple for MacOS are the following, and because there are some extra steps required we thought this might be helpful for people getting started with IVy on MacOS

Please add to IVy installation documentation if you agree this might be helpful

Follow up questions can be directed to aeiriksson at apple.com

Regards,

'Asgeir

Installation instructions on MacOS High Sierra and Mojave

Preliminaries:

1. Install Xcode from App Store
2. Install Xcode command line tools

   xcode-select --install

3. Install Xserver

• https://www.xquartz.org

4. Macports

sudo xcodebuild -license
https://www.macports.org/install.php (select matching macOS 10.12 or 10.13 depending on macOS running on machine)
macOS 10.3 Mojave (make sure you've installed all patches because various steps below were broken until about 7/15/2019 patch)
sudo easy_install pip (required on 10.13 Mojave and/or required by 8/1/2019)
a) sudo port install graphviz-gui
sudo port select --set python python27
sudo port select --set python2 python27
sudo pip install pygraphviz --install-option="--include-path=/opt/local/include" --install-option="--library-path=/opt/local/lib"
b) sudo port install Tix
c) sudo port install py27-ply
d) sudo port install py27-ipython
e) suo port install py27-tkinter (added this step with 10.13 Mojave)

5. Install Z3

• https://github.com/Z3Prover/z3
  Select download zip in the “Clone or download” button
  $ pwd
  /Users/asgeireiriksson/Downloads/z3-master

python scripts/mk_make.py
cd build
make
sudo make install
sudo pip install z3-solver

6. Install Ivy:
   https://github.com/Microsoft/ivy
   -Select download zip in the “Clone or download” button

$ pwd
/Users/asgeireiriksson/Downloads/ivy-master
$ sudo python setup.py install
export PATH=/opt/local/Library/Frameworks/Python.framework/Versions/2.7/bin:$PATH

7 running test

pwd
/Users/asgeireiriksson/Downloads/ivy-master
cd doc/examples
ivy_check diagnose=true client_server_example.ivy

Using ivy_check and ivy_to_cpp for testing the quic-scripts generates the following error.

(base) # ivy_to_cpp ./quic_connection.ivy 
quic_frame.ivy: line 486: error: unknown symbol: _generating

Example: using ivy-master/examples/pld16/learning_switch.ivy

Command line: ivy_check diagnose=true debug=true trace=true learning_switch.ivy

Tried this on macOS Catalina 10.15 and Linux

1. The example has uninterpreted types

type packet
type node

This runs correctly and if I comment out the last conjecture within learning_switch.ivy produces a failing trace

2. when I change type packet to an enumerated type

type packet = {arp,ip}
type node

And don't comment out the last conjecture the the verification is successful, but when I comment out the last conjecture I get the following:
learning_switch.ivy: line 120: (no name) ... FAIL
searching for a small model... done
warning: model doesn't give a value for enumerated term __loc:p. returning arp.
warning: model doesn't give a value for enumerated term __loc:p. returning arp.
Traceback (most recent call last):
File "/opt/local/Library/Frameworks/Python.framework/Versions/2.7/bin/ivy_check", line 11, in
load_entry_point('ms-ivy==0.1', 'console_scripts', 'ivy_check')()
File "/opt/local/Library/Frameworks/Python.framework/Versions/2.7/lib/python2.7/site-packages/ms_ivy-0.1-py2.7.egg/ivy/ivy_check.py", line 696, in main
check_module()
File "/opt/local/Library/Frameworks/Python.framework/Versions/2.7/lib/python2.7/site-packages/ms_ivy-0.1-py2.7.egg/ivy/ivy_check.py", line 675, in check_module
check_isolate()
File "/opt/local/Library/Frameworks/Python.framework/Versions/2.7/lib/python2.7/site-packages/ms_ivy-0.1-py2.7.egg/ivy/ivy_check.py", line 544, in check_isolate
summarize_isolate(mod)
File "/opt/local/Library/Frameworks/Python.framework/Versions/2.7/lib/python2.7/site-packages/ms_ivy-0.1-py2.7.egg/ivy/ivy_check.py", line 460, in summarize_isolate
check_conjs_in_state(mod,ag,post,indent=12)
File "/opt/local/Library/Frameworks/Python.framework/Versions/2.7/lib/python2.7/site-packages/ms_ivy-0.1-py2.7.egg/ivy/ivy_check.py", line 328, in check_conjs_in_state
return check_fcs_in_state(mod,ag,post,[ConjChecker(c,indent) for c in lcs])
File "/opt/local/Library/Frameworks/Python.framework/Versions/2.7/lib/python2.7/site-packages/ms_ivy-0.1-py2.7.egg/ivy/ivy_check.py", line 304, in check_fcs_in_state
handler = MatchHandler(mclauses,model,vocab)
File "/opt/local/Library/Frameworks/Python.framework/Versions/2.7/lib/python2.7/site-packages/ms_ivy-0.1-py2.7.egg/ivy/ivy_check.py", line 209, in init
mod_clauses = islv.clauses_model_to_clauses(clauses,model=model,numerals=True)
File "/opt/local/Library/Frameworks/Python.framework/Versions/2.7/lib/python2.7/site-packages/ms_ivy-0.1-py2.7.egg/ivy/ivy_solver.py", line 1232, in clauses_model_to_clauses
res = model_facts(h,ignore,clauses1)
File "/opt/local/Library/Frameworks/Python.framework/Versions/2.7/lib/python2.7/site-packages/ms_ivy-0.1-py2.7.egg/ivy/ivy_solver.py", line 1177, in model_facts
for l in relation_model_to_clauses(h,r,n)]
File "/opt/local/Library/Frameworks/Python.framework/Versions/2.7/lib/python2.7/site-packages/ms_ivy-0.1-py2.7.egg/ivy/ivy_solver.py", line 1364, in relation_model_to_clauses
get_lit_facts(h,lit,res)
File "/opt/local/Library/Frameworks/Python.framework/Versions/2.7/lib/python2.7/site-packages/ms_ivy-0.1-py2.7.egg/ivy/ivy_solver.py", line 1372, in get_lit_facts
vs,rows = h.check(lit)
File "/opt/local/Library/Frameworks/Python.framework/Versions/2.7/lib/python2.7/site-packages/ms_ivy-0.1-py2.7.egg/ivy/ivy_solver.py", line 734, in check
ranges = [self.constants[x.sort] for x in vs]
KeyError: EnumeratedSort('packet', ('arp', 'ip'))

3. When change type node

type packet
type node = {bridge, router}

And don't comment out the last conjecture I get the following:
Initialization must establish the invariant
learning_switch.ivy: line 24: route(N:node) ... PASS
learning_switch.ivy: line 25: route(N:node) ... PASS
learning_switch.ivy: line 26: route(N:node) ... FAIL
searching for a small model... done
warning: model doesn't give a value for enumerated term __N. returning bridge.
warning: model doesn't give a value for enumerated term __N. returning bridge.
Traceback (most recent call last):
File "/opt/local/Library/Frameworks/Python.framework/Versions/2.7/bin/ivy_check", line 11, in
load_entry_point('ms-ivy==0.1', 'console_scripts', 'ivy_check')()
File "/opt/local/Library/Frameworks/Python.framework/Versions/2.7/lib/python2.7/site-packages/ms_ivy-0.1-py2.7.egg/ivy/ivy_check.py", line 696, in main
check_module()
File "/opt/local/Library/Frameworks/Python.framework/Versions/2.7/lib/python2.7/site-packages/ms_ivy-0.1-py2.7.egg/ivy/ivy_check.py", line 675, in check_module
check_isolate()
File "/opt/local/Library/Frameworks/Python.framework/Versions/2.7/lib/python2.7/site-packages/ms_ivy-0.1-py2.7.egg/ivy/ivy_check.py", line 544, in check_isolate
summarize_isolate(mod)
File "/opt/local/Library/Frameworks/Python.framework/Versions/2.7/lib/python2.7/site-packages/ms_ivy-0.1-py2.7.egg/ivy/ivy_check.py", line 435, in summarize_isolate
check_conjs_in_state(mod,ag,ag.states[0])
File "/opt/local/Library/Frameworks/Python.framework/Versions/2.7/lib/python2.7/site-packages/ms_ivy-0.1-py2.7.egg/ivy/ivy_check.py", line 328, in check_conjs_in_state
return check_fcs_in_state(mod,ag,post,[ConjChecker(c,indent) for c in lcs])
File "/opt/local/Library/Frameworks/Python.framework/Versions/2.7/lib/python2.7/site-packages/ms_ivy-0.1-py2.7.egg/ivy/ivy_check.py", line 304, in check_fcs_in_state
handler = MatchHandler(mclauses,model,vocab)
File "/opt/local/Library/Frameworks/Python.framework/Versions/2.7/lib/python2.7/site-packages/ms_ivy-0.1-py2.7.egg/ivy/ivy_check.py", line 209, in init
mod_clauses = islv.clauses_model_to_clauses(clauses,model=model,numerals=True)
File "/opt/local/Library/Frameworks/Python.framework/Versions/2.7/lib/python2.7/site-packages/ms_ivy-0.1-py2.7.egg/ivy/ivy_solver.py", line 1232, in clauses_model_to_clauses
res = model_facts(h,ignore,clauses1)
File "/opt/local/Library/Frameworks/Python.framework/Versions/2.7/lib/python2.7/site-packages/ms_ivy-0.1-py2.7.egg/ivy/ivy_solver.py", line 1177, in model_facts
for l in relation_model_to_clauses(h,r,n)]
File "/opt/local/Library/Frameworks/Python.framework/Versions/2.7/lib/python2.7/site-packages/ms_ivy-0.1-py2.7.egg/ivy/ivy_solver.py", line 1364, in relation_model_to_clauses
get_lit_facts(h,lit,res)
File "/opt/local/Library/Frameworks/Python.framework/Versions/2.7/lib/python2.7/site-packages/ms_ivy-0.1-py2.7.egg/ivy/ivy_solver.py", line 1372, in get_lit_facts
vs,rows = h.check(lit)
File "/opt/local/Library/Frameworks/Python.framework/Versions/2.7/lib/python2.7/site-packages/ms_ivy-0.1-py2.7.egg/ivy/ivy_solver.py", line 734, in check
ranges = [self.constants[x.sort] for x in vs]
KeyError: EnumeratedSort('node', ('bridge', 'router'))

When I model the German Cache Coherence Protocol in IVy I would like to multi-cast the invalidates to chan2 that is a struct

I'm transcribing the German protocol as described in "SMT-Based Verification With DVF", by Goel et al.

type msg_cmd = {empty,reqs,reqe,inv,invack,gnts,gnte}
..
module noc_msg = {
individual m_cmd : msg_cmd
individual m_data : data
}
..
module noc_mod = {
instantiate chan1(P:proc) : noc_msg # requests
instantiate chan2(P:proc) : noc_msg
relation chan2_inv(P:proc) # invalidates
instantiate chan3(P:proc) : noc_msg # invacks
}

export action recv_req(p:proc) = {
var others : bool;

    others := d_state=shared & (exists P. shrset(P) & P~=p); 

..
} else if noc.chan1(p).m_cmd=reqe & d_state=shared & others {
d_state := locked;

        noc.chan2_inv(P) := shrset(P) & P~=p; # multi-cast inval to all nodes that have bit set in shrset except p 

shrset(P) := P=p;

noc.chan1(p).m_cmd := empty;

ownerptr := p;

--

Is it possible to eliminate chan2_inv and multi-cast to chan2?

In the following example, the fragment checker does not complain but, depending on the random seed, Z3 diverges when checking the loop in after init (i.e. it either takes about 10 seconds or much longer than I'm willing to wait). Is the fragment checker missing something or is this a problem of Z3?

#lang ivy1.7

# This file contains a specification and implementation of node sets with a
# majority test.

include order
include collections

instance node : iterable

# node sets

isolate nset = {

    type this
    alias t = this
    type index

    relation member(N:node, S:t)
    relation majority(S:t)

    action emptyset returns (s:t)
    action add(s:t, n : node) returns (s:t)

    specification {
        after emptyset {
            ensure ~member(N, s)
        }

        after add {
            ensure member(N,s) <-> (member(N , old s) | N = n)
        }
    }

    # This invariant has quantifier alternation, thus we make it private. It
    # can always be used explitely in a `with` clause
    private {
        invariant [majorities_intersect]
            majority(S) & majority(T) -> exists N. member(N,S) & member(N,T)
    }

    implementation {
        interpret index -> int
        function card(S:t) : index
        instance arr : rel_array(index,node)
        destructor repr(N:nset) : arr
        individual all : nset

        definition member(N,S) = exists I. 0 <= I & I < repr(S).end & repr(S).value_is(I, N)
        definition majority(S) = card(S) + card(S) > card(all)

        after init {
            card(S) := 0;
            repr(all) := arr.empty;
            var i := node.iter.create(0);
            while ~i.is_end
                invariant (forall N.~(member(N,S) & member(N,T))) ->
                              card(S) + card(T) <= card(all)
                invariant node.iter.done(N,i) <-> member(N,all)
                invariant card(S) >= 0
            {
                repr(all) := repr(all).append(i.val);
                card(S) := card(S) + 1 if member(i.val, S) else card(S);
                i := i.next
            };
        }

        implement emptyset {
            repr(s) := arr.empty()
        }

        implement add {
            if ~member(n, s) {
                repr(s) := repr(s).append(n)
            }
        }
    }

} with node

export nset.emptyset
export nset.add

Hello, ivy_check does not complain when verifying the following file. Is this a bug or am I misunderstanding what before and after mean? (the same thing happen using after)

#lang ivy1.7

isolate iso_1 = {
    action my_action = {
        require false
    }
}

isolate iso_2 = {
    export action my_action = {
    }
    before my_action {
        call iso_1.my_action
    }
} with iso_1

Consider

type t
theorem [thm1] {
    relation p(X1:t,X2:t)
    property forall X1,X2 . p(X1,X2)
}
proof {
    apply introA;
    apply introA
}

This fails with error: symbol x is captured in substitution. Can I make this work somehow? I'm trying to obtain a goal of the form p(x1,x2) for two individuals x1 and x2.

I'm having trouble installing and running Ivy following the instructions. I have installed the prerequisites and am using Python 2.7.12. I cloned the Master branch and tried running sudo python setup.py install. I get

  File "setup.py", line 12
    install_requires=[
                   ^
SyntaxError: invalid syntax

The setup.py file contains:

from setuptools import setup, find_packages

setup(name='ms_ivy',
      version='0.1',
      description='IVy verification tool',
      url='http://github.com/microsoft/ivy',
      author='IVy team',
      author_email='[email protected]',
      license='MIT',
      packages=find_packages(),
      include_package_data={'ivy':['include/*.ivy','include/*.h']}
      install_requires=[
          'ply',
          'pygraphviz',
          'tarjan'
      ],
      entry_points = {
        'console_scripts': ['ivy=ivy.ivy:main','ivy_check=ivy.ivy_check:main','ivy_to_cpp=ivy.ivy_to_cpp:main','ivy_show=ivy.ivy_show:main',],
        },
      zip_safe=False)

At first I thought that the line starting "include_package_data = ..." seems to be missing a comma. After fixing this and running sudo python setup.py install I get:

error in ms_ivy setup command: 'include_package_data' must be a boolean value (got {'ivy': ['include/*.ivy', 'include/*.h']})

Next I thought that perhaps the line was supposed to just be commented out or something and tried installing Ivy again with the line commented out. This time installing worked.

Trying to run the client_server_example I ran into more trouble though, which may or may not be related (My knowledge of Python is quite limited). I navigated to the /doc/examples folder and ran ivy ui=cti client_server_example.ivy. The window opened up fine, but when I click Invariant-> Check induction I get the following error and nothing happens in the Ivy window.

Exception in Tkinter callback
Traceback (most recent call last):
  File "/usr/lib/python2.7/lib-tk/Tkinter.py", line 1540, in __call__
    return self.func(*args)
  File "/usr/local/lib/python2.7/dist-packages/ms_ivy-0.1-py2.7.egg/ivy/ivy_ui_cti.py", line 167, in check_inductiveness
    res = ag.check_bounded_safety(post, _get_model_clauses)
  File "/usr/local/lib/python2.7/dist-packages/ms_ivy-0.1-py2.7.egg/ivy/ivy_art.py", line 357, in check_bounded_safety
    res = self.bmc(fail,true_clauses(),_get_model_clauses=_get_model_clauses,bound=bound)
  File "/usr/local/lib/python2.7/dist-packages/ms_ivy-0.1-py2.7.egg/ivy/ivy_art.py", line 335, in bmc
    bmc_res = history_satisfy(history,state,_get_model_clauses,final_cond=error_cond)
  File "/usr/local/lib/python2.7/dist-packages/ms_ivy-0.1-py2.7.egg/ivy/ivy_interp.py", line 578, in history_satisfy
    final_cond
  File "/usr/local/lib/python2.7/dist-packages/ms_ivy-0.1-py2.7.egg/ivy/ivy_transrel.py", line 566, in satisfy
    model = _get_model_clauses(post,final_cond=final_cond)
  File "/usr/local/lib/python2.7/dist-packages/ms_ivy-0.1-py2.7.egg/ivy/ivy_ui_cti.py", line 163, in <lambda>
    final_cond = final_cond
  File "/usr/local/lib/python2.7/dist-packages/ms_ivy-0.1-py2.7.egg/ivy/ivy_solver.py", line 849, in get_small_model
    s.add(clauses_to_z3(clauses))
  File "/usr/local/lib/python2.7/dist-packages/ms_ivy-0.1-py2.7.egg/ivy/ivy_solver.py", line 349, in clauses_to_z3
    z3_clauses = [conj_to_z3(cl) for cl in clauses.fmlas]
  File "/usr/local/lib/python2.7/dist-packages/ms_ivy-0.1-py2.7.egg/ivy/ivy_solver.py", line 346, in conj_to_z3
    return formula_to_z3(cl)
  File "/usr/local/lib/python2.7/dist-packages/ms_ivy-0.1-py2.7.egg/ivy/ivy_solver.py", line 386, in formula_to_z3
    z3_formula = formula_to_z3_int(fmla)
  File "/usr/local/lib/python2.7/dist-packages/ms_ivy-0.1-py2.7.egg/ivy/ivy_solver.py", line 356, in formula_to_z3_int
    return atom_to_z3(fmla)
  File "/usr/local/lib/python2.7/dist-packages/ms_ivy-0.1-py2.7.egg/ivy/ivy_solver.py", line 324, in atom_to_z3
    return apply_z3_func(pred,tup)
  File "/usr/local/lib/python2.7/dist-packages/ms_ivy-0.1-py2.7.egg/ivy/ivy_solver.py", line 222, in apply_z3_func
    _args, sz = z3._to_ast_array(tup)
AttributeError: 'module' object has no attribute '_to_ast_array'

I am using Ubuntu 16.04.2 LTS.

I've verified that the MacOS installation instructions work as-is for MacOS 10.15 Catalina

Built on both MacBook Air and MacBook Pro and ran a regression on the MacBook Pro

Please make a note in the Installing IVy section

Thanks,

'Asgeir (aeiriksson at apple.com)

This is in the last master branch of ivy.
I get errors on interference for the "after init" action of the nset isolate:

~/ivy_master/doc/examples ((detached from 02a56dc)) $ ivy_to_cpp isolate=iso_impl target=repl toy_consensus.ivy 
toy_consensus.ivy: line 47: error: assignment may be interfering

This fails with error: unknown symbol: q

#lang ivy1.7

axiom [my_axiom] {
    individual p:bool
    property true
}

individual q:bool

invariant true
proof {
    apply my_axiom with p = q
}

The manual says that definitions are equivalent to axioms. However, the following verifies, and when the definition is changed to an axiom, it gets a syntax error for assigning to a function used in an axiom:

function f(T:bool) : bool definition f(T:bool) = T after init { f(T) := false; }
I assume that definitions should give the same error.

Moreover, if you add an assertion at the end of the initializer above, ivy_check gets an AssertionError.