working on tutorial

doc/examples/testing/hello1.ivy

@@ -0,0 +1,82 @@
+#lang ivy1.6
+
+# This is a simple "hello world" program in IVy.
+#
+# IVy is a *synchronous* programming language. One thing this means is
+# that everything an IVy program does is a response to some action by
+# its environment (there are other implications that we'll see later). 
+#
+# To make a "hello world" program, we'll define an action called
+# `hello` that the environment can call. Our program response by
+# calling back with the action `world`.
+#
+# To make things a little more interesting, we'll give each action a
+# parameter of type `t`.
+
+# This is a declaration of type `t`. Notice we haven't said anything
+# yet about `t`, just that it is a type.
+
+type t
+
+# Now we declare two actions with parameters of type `t`.
+
+action hello(val:t)
+action world(val:t)
+
+# The action `hello` is called by the environment, so we say it is
+# "exported" by the program.
+
+export hello
+
+# The action `world` is provided by the environment, so we say it is
+# "imported":
+
+import world
+
+# Since our program exports `hello`, we need to give it an *implementation*.
+# When the environment calls `hello` with value `val`, our program responds
+# by calling `world` with value `val+1`.
+
+implement hello {
+    call world(val+1)
+}
+
+# But wait! We haven't said what type `t` is. How do we know what it
+# means to add one to `val` if `val` has an unknown type? Of course,
+# we don't, and neither does IVy. To run this program, we need to
+# *interpret* `t` as some concrete type. The following statement tells
+# IVy that `t` should be interpreted as the type of (unsigned) binary numbers
+# of four bits:
+
+interpret t -> bv[4]
+
+# Ivy does things this way because in verification, we often want to
+# interpret the types differently for different purposes.
+
+# One way to run this program is to generate a read-eval-print loop (a
+# REPL). In this case, the user at a terminal plays the rols of the
+# environment. We build a REPL with a command line this:
+#
+#     $ ivy_to_cpp target=repl build=true hello1.ivy
+#
+# This tells IVy to create a REPL from our program in C++ and then
+# build it into an executable file called "hello1.exe". If
+# you're looking at this file in Visual Studio, you can just say
+# "Build" and "Run".
+#
+# The REPL will print a prompt and wait for the environment (you) to
+# call `hello`. Here's a sample run:
+#
+#     > hello(7)
+#     < world(8)
+#     > hello(3)
+#     < world(4)
+#     ...
+#
+# Now have a look at `hello2.ivy`.
+
+
+
+
+
+

doc/examples/testing/hello2.ivy

@@ -0,0 +1,98 @@
+#lang ivy1.6
+
+# Now let's write a specification for our "hello world" program.
+#
+# In IVy, a specification is just a piece of code that monitors
+# another piece of code (but doesn't interfere with it).
+#
+# We'll define the same interface that we had before:
+
+
+type t
+
+action hello(val:t)
+action world(val:t)
+
+export hello
+import world
+
+# Now we'll write a monitor that watches the interface actions `hello`
+# and `world` and makes sure they're working correctly. It's an IVy
+# idiom to write a specification inside an object called `spec`. This
+# object can member variables that record information about the
+# history of actions. For example, we want to record when a `hello` is
+# pending and only allow `world` to be called when this is true.
+# Here's how we can specify that there are no unsolicited calls to
+# `world`:
+
+object spec = {
+
+    # First we declare a state variable `pending` for our spec.
+
+    var pending : bool
+
+    # This says to initialize `pending` to `false`.
+
+    after init {
+	pending := false
+    }
+
+    # This says, before executing the implementation of `hello`, set
+    # `pending` to true.
+
+    before hello(val:t) {
+	pending := true
+    }
+
+    # This says, before executing the implementation of `world`,
+    # *assert* that `pending` is true, then set it to false. If we get
+    # an unsolicited call to `world`, this assertion will fail.
+
+    before world(val:t) {
+	assert pending;
+	pending := false
+    }
+}
+
+# That's our program's specification. Now let's give the implementation. It's
+# an IVY idiom to put the implementation in an object called `impl`.
+
+object impl = {
+    implement hello {
+	call world(val+1)
+    }
+}
+
+# Once again, we have to interpret type `t`.
+
+interpret t -> bv[4]
+
+# This time, instead of interacting with the program in a REPL, we're
+# going to *test* it automatically. We can produce a tester for the program
+# with a command like this:
+#
+#     $ ivy_to_cpp target=test build=true hello2.ivy
+#
+# This tells IVy to create a randomized tester to play the role of the environment.
+# and build it into an executable file called "hello2.exe". If
+# you're looking at this file in Visual Studio, you can just say
+# "Build" and "Run".
+#
+# The tester will just run by itself and print out something like the following:
+#
+#     > hello(7)
+#     < world(8)
+#     > hello(3)
+#     < world(4)
+#     ...
+#
+# The values of the parameter to `hello` are chosen randomly by the
+# tester.
+#
+# Now have a look at `hello3.ivy`. 
+
+
+
+
+
+

doc/examples/testing/hello3.ivy

@@ -0,0 +1,88 @@
+#lang ivy1.6
+
+# Now let's try to specify something a little more interesting about
+# the "hello world" program. We want the value of the `world` response
+# to be beigger thatn the value of the `hello` it responds to.
+
+# We'll define the same interface that we had before:
+
+
+type t
+
+action hello(val:t)
+action world(val:t)
+
+export hello
+import world
+
+# Now we'll add to our monitor a variable `hello_value` that remembers
+# the parameter to `hello`. We assert that the `world` value has to be greater than this.
+
+object spec = {
+
+    var pending : bool
+
+    # Here is our new variable, of type `t`. We don't care what its
+    # initial value is.
+
+    var hello_value : t
+
+    after init {
+	pending := false
+    }
+
+    before hello(val:t) {
+	pending := true;
+	hello_value := val        # remember the value
+    }
+
+    before world(val:t) {
+	assert pending;
+	assert val > hello_value;  #  new assertion
+	pending := false
+    }
+}
+
+# The rest is the same as before.
+
+object impl = {
+    implement hello {
+	call world(val+1)
+    }
+}
+
+interpret t -> bv[4]
+
+# Now build a tester and run it. What happens?
+#
+# You might see something like this:
+#
+#     > hello(1)
+#     < world(2)
+#     > hello(12)
+#     < world(13)
+#     > hello(10)
+#     < world(11)
+#     ...
+#     > hello(1)
+#     < world(2)
+#     > hello(15)
+#     < world(0)
+#     assertion_failed("hello3.ivy: line 41: ")
+#     hello3.ivy: line 41: : assertion failed
+#
+# Yikes! It looks like we got an overflow. Since we are using 4-bit
+# numbers, 15 + 1 = 0. So our implementation fails the specification.
+# Notice that if we had used, say 32-bit integers as our data type,
+# we probably wouldn'[t have found this error, since the chance of randomly
+# drawing 2^32 - 1 would be too samll. This is one good reason to set limits
+# low in testing. It becomes more likely that we will reach them.
+#
+# But maybe we really didn't want to allow the environment to say
+# `hello` with the maximum value. Have a look at `hello4.ivy`.
+
+
+
+
+
+

doc/examples/testing/hello4.ivy

@@ -0,0 +1,105 @@
+#lang ivy1.6
+
+# Now let's changte our spec so that we require the environment not to
+# say `hello` with the maximum value. That is, we want this to be a *guarantee* of the environment,
+# but an *assumption* of our program.
+
+# We'll define the same interface that we had before:
+
+
+type t
+
+action hello(val:t)
+action world(val:t)
+
+export hello
+import world
+
+# Now we add an assertion that executes before the implementation of
+# `hello`, stating that `val` is not max. Notice we state this in a
+# way that will for any integer type, even an unbounded type with no
+# max. That way our spec will work for various interpretations of `t`.
+
+object spec = {
+
+    var pending : bool
+
+    var hello_value : t
+
+    after init {
+	pending := false
+    }
+
+    before hello(val:t) {
+	assert val + 1 ~= 0;      # val is not max
+	pending := true;
+	hello_value := val
+    }
+
+    before world(val:t) {
+	assert pending;
+	assert val > hello_value;
+	pending := false
+    }
+}
+
+# This demonstrates a special feature of `before`. That is, any
+# assertion in a `before` monitor is a *guarantee* for the caller of
+# the action and an *assumption* for the implementer of the action.
+# In this case, the caller is the environment.
+
+# The rest is the same as before.
+
+object impl = {
+    implement hello {
+	call world(val+1)
+    }
+}
+
+interpret t -> bv[4]
+
+# Now build a tester and run it. What happens?
+#
+# You might see something like this:
+#
+#     > hello(1)
+#     < world(2)
+#     > hello(12)
+#     < world(13)
+#     > hello(10)
+#     ...
+#     > hello(6)
+#     < world(7)
+#     test_completed
+#
+# Why din't we see a `hello(15)` in trace? The tester only generates
+# environment actions that satisfy the assumptions of the program. In
+# this case the value 15 violates that assumption, so the tester
+# doesn't generate it. This technique is called "specification-based
+# testing".
+#
+# How is this actually accomplished? The tester executes the
+# specification code symbolically. This means it puts symbolic
+# variables in place of the inputs and generates an expression that is
+# true exactly when execution passes thorugh without violating any
+# assertions. The SMT solver Z3 is then used to solve for input values
+# that make the expression true. IVy tries to produce values that are
+# uniformly distributed over the satisfying set, though in practice
+# the distribution can be skewed. 
+#
+# The nice thing about specification-based testing is that it
+# eliminates human bias in the test generation. Plus, of course, it's
+# completely automatic, so you don't have to write tests manually.
+#
+# By the way, the tester executable has some useful command-line options.
+# For example, to generate 1000 input events and write the event log to file foo.iev,
+# you could use the following command line:
+#
+#      $ ./hello4 iters=1000 out=file.iev
+#
+# The extension "iev" stands for "IVy event log".
+
+
+
+
+

doc/examples/testing/repstore_variant.ivy

@@ -0,0 +1,249 @@
+#lang ivy1.6
+
+include tcp
+include udp
+
+type key
+type value
+ghost type txid
+
+type request_body
+
+object write_req = {
+    variant t of request_body = struct {
+	ky : key,
+	vl : value
+    }
+}
+
+object read_req = {
+    variant t of request_body = struct {
+	ky : key
+    }
+}
+
+object request = {
+    type t = struct {
+	tx : txid,
+	bd : request_body
+    }
+}
+
+type response_body
+
+object write_resp = {
+    variant t of response_body = struct {
+    }
+}
+
+object read_resp = {
+    variant t of response_body = struct {
+	vl : value
+    }
+}
+
+object response = {
+    type t = struct {
+	tx : txid,
+	bd : response_body
+    }
+}
+
+module replica = {
+    function store(K:key) : value
+    after init {
+	store(K) := 0
+    }
+    action exec(inp : request_body) returns (out:response_body) = {
+	if some (r:write_req.t) inp *> r {
+	    store(r.ky) := r.vl;
+	    var wr : write_resp.t;
+	    out := wr
+	}
+	else if some (r:read_req.t) inp *> r {
+	    var rr : read_resp.t;
+	    rr.vl := store(r.ky);
+	    out := rr
+	}
+    }
+}
+
+
+module reference = {
+    instance rep : replica
+
+    
+    action create(inp : request_body) returns (tx : txid)
+    action serialize(tx : txid)
+    action commit(tx : txid)
+    action eval(tx : txid) returns (res : response_body)
+
+    individual next : txid
+    function txs(X:txid) : request_body
+    function txres(X:txid) : response_body
+    relation serialized(X:txid)
+    relation committed(X:txid)
+
+    after init {
+	next := 0;
+	committed(X) := false;
+	serialized(X) := false;
+    }
+
+    implement create {
+	tx := next;
+	txs(tx) := inp;
+	next := next + 1;
+    }
+
+    implement serialize {
+	assert 0 <= tx & tx < next;
+	assert ~serialized(tx);
+	serialized(tx) := true;
+    }
+    delegate serialize
+
+    implement commit {
+	assert 0 <= tx & tx < next;
+	assert serialized(tx) & ~committed(tx);
+	txres(tx) := rep.exec(txs(tx));
+	committed(tx) := true;
+    }
+    delegate commit
+
+    implement eval {
+	assert committed(tx);
+	res := txres(tx);
+    }
+    delegate eval
+
+    interpret txid -> int
+}
+
+instance ref : reference
+
+type client_id
+
+type req_msg = struct {
+    cid : client_id,
+    req : request.t
+}
+
+module client(cid,srvr_chan,cl_chans) = {
+    
+    action client_request(req : request_body)
+
+    implement client_request {
+	local m : req_msg {
+	    m.cid := cid;
+	    m.req.tx := ref.create(req);
+	    m.req.bd := req;
+	    call srvr_chan.send(m);
+	}
+    }
+}
+
+module primary_node(port, fwd_chan, rev_chan, cl_chans) = {
+    instance rep : replica
+
+    instance req_chan : nondup_endpoint(port,req_msg)
+
+    instance counter : unbounded_sequence
+    function pending(K:key) : counter.t
+
+    after init {
+	pending(K) := 0;
+    }
+	
+    implement req_chan.recv(inp : req_msg) {
+        if some (rr:read_req.t) inp.req.bd *> rr {
+	    if pending(rr.ky) = 0 {
+		call ref.commit(inp.req.tx);
+		var res : response.t;
+		res.tx := inp.req.tx;
+		res.bd := rep.exec(rr);
+		call cl_chans(inp.cid).send(res)
+	    } else {
+                call req_chan.send(inp);  # if cannot execute, recirculate
+	    }
+	} else if some (wr:write_req.t) inp.req.bd *> wr {
+	    call ref.serialize(inp.req.tx);           # this is ghost!
+	    call fwd_chan.send(inp);
+	    pending(wr.ky) := pending(wr.ky).next;
+	    var res := rep.exec(inp.req.bd);
+	} 	    
+    }
+
+    implement rev_chan.recv(inp : req_msg) {
+	if some (wr:write_req.t) inp.req.bd *> wr {
+	    pending(wr.ky) := pending(wr.ky).prev;
+	}
+    }
+}
+
+module secondary_node(port, fwd_chan, rev_chan, cl_chans) = {
+    instance rep : replica
+
+    instance req_chan : nondup_endpoint(port,req_msg)
+	
+    implement req_chan.recv(inp : req_msg) {
+        if some (rr:read_req.t) inp.req.bd *> rr {
+	    var res : response.t;
+	    res.tx := inp.req.tx;
+	    res.bd := rep.exec(rr);
+	    call cl_chans(inp.cid).send(res);
+	} 	    
+	# ignore writes!
+    }
+
+    implement fwd_chan.recv(inp : req_msg) {
+	call ref.commit(inp.req.tx);
+	var res : response.t;
+	res.tx := inp.req.tx;
+	res.bd := rep.exec(inp.req.bd);
+	call cl_chans(inp.cid).send(res);
+	call rev_chan.send(inp);
+    }
+
+}
+
+
+instance fwd_chan : tcp_channel("localhost:44090",req_msg)
+instance rev_chan : tcp_channel("localhost:44091",req_msg)
+
+instance cl_chans : nondup_endpoint_set(client_id,44100,response.t)
+instance cl(X:client_id) : client(X,prim.req_chan,cl_chans)
+instance prim : primary_node(44200,fwd_chan.sndr,rev_chan.rcvr,cl_chans)
+instance sec : secondary_node(44201,fwd_chan.rcvr,rev_chan.sndr,cl_chans)
+
+object service_spec = {
+    before cl_chans.send(p : client_id, m : response.t) {
+	assert m.bd = ref.eval(m.tx);
+    }
+}
+
+object mid_spec = {
+    instance queue : unbounded_queue(txid)
+
+    after ref.serialize(tx:txid) {
+	call queue.push(tx);
+    }
+
+    before fwd_chan.rcvr.recv(inp : req_msg) {
+	assert inp.req.bd = ref.txs(inp.req.tx);
+	assert inp.req.tx = queue.pop;
+	call ref.commit(inp.req.tx);
+    }
+
+    delegate fwd_chan_rcvr_recv[before] -> prim
+
+}
+
+export cl.client_request
+import cl_chans.recv
+
+trusted isolate iso_prim = prim with cl,cl_chans,ref,service_spec,mid_spec,fwd_chan,rev_chan
+trusted isolate iso_sec = sec with ref,service_spec,mid_spec
+
+interpret value -> bv[16]
+

ivy/ivy_parser.py

@@ -405,6 +405,10 @@ def p_constantdecl_constant_tterms(p):
     'constantdecl : INDIV tterms'
     p[0] = ConstantDecl(*p[2])
 
+def p_constantdecl_var_tterms(p):
+    'constantdecl : VAR tterms'
+    p[0] = ConstantDecl(*p[2])
+
 def p_relationdecl_relation_tatoms(p):
     'relationdecl : RELATION tatoms'
     p[0] = RelationDecl(*apps_to_atoms(p[2]))

ivy/ivy_to_cpp.py

@@ -695,8 +695,6 @@ def emit_randomize(header,symbol,classname=None):
     cname = varname(name)
     sort = symbol.sort
     domain = sort_domain(sort)
-    iu.dbg('symbol')
-    iu.dbg('symbol.sort')
     for idx,dsort in enumerate(domain):
         dcard = sort_card(dsort)
         indent(header)
@@ -732,7 +730,6 @@ def emit_action_gen(header,impl,name,action,classname):
     global indent_level
     global global_classname
     global_classname = classname
-    iu.dbg('name')
     caname = varname(name)
     if name in im.module.before_export:
         action = im.module.before_export[name]
@@ -3941,7 +3938,7 @@ target = iu.EnumeratedParameter("target",["impl","gen","repl","test"],"gen")
 opt_classname = iu.Parameter("classname","")
 opt_build = iu.BooleanParameter("build",False)
 opt_trace = iu.BooleanParameter("trace",False)
-opt_test_iters = iu.Parameter("test_iters","1000")
+opt_test_iters = iu.Parameter("test_iters","100")
 opt_compiler = iu.EnumeratedParameter("compiler",["g++","cl"],"g++")
 opt_main = iu.Parameter("main","main")
 opt_stdafx = iu.BooleanParameter("stdafx",False)

test/enum1.ivy

@@ -0,0 +1,9 @@
+#lang ivy1.3
+
+type t
+type color = {red,green,blue}
+
+individual c(X:t):color
+relation p(X:t)
+
+init p(X) -> c(X) = green

test/ext_precond.ivy

@@ -0,0 +1,19 @@
+#lang ivy1.6
+
+type t
+
+object foo = {
+    action a(v:t) = {
+	assert v = 0
+    }
+}
+
+object bar = {
+    action a = {
+	call foo.a(0)
+    }
+}
+
+isolate iso_foo = foo
+
+interpret t -> int

test/nesteddestr1.py

@@ -0,0 +1,33 @@
+
+from ivy import ivy_module as im
+from ivy.ivy_compiler import ivy_from_string
+from ivy import ivy_utils as iu
+prog = """#lang ivy1.6
+
+type t
+
+type s1 = struct {
+    foo : t,
+    bar : t
+}
+
+type s2 = struct {
+    baz : s1,
+    bif : t
+} 
+
+individual w : t
+individual v : s2
+
+action a = {
+   v.baz.foo := w
+}
+
+export a
+"""
+
+with im.Module():
+    iu.set_parameters({'show_compiled':'true'})
+    ivy_from_string(prog,create_isolate=False)
+    print im.module.actions["a"].update(im.module,{})
+