kenmcmil / ivy

IVy is a research tool intended to allow interactive development of protocols and their proofs of correctness and to provide a platform for developing and experimenting with automated proof techniques. In particular, IVy provides interactive visualization of automated proofs, and supports a use model in which the human protocol designer and the automated tool interact to expose errors and prove correctness.
Other
77 stars 24 forks source link

Understanding Interference in Ivy #50

Open prpr2770 opened 2 years ago

prpr2770 commented 2 years ago

Based on the example provided in Networking Tutorial

Script derived from above tutorial

#lang ivy1.7

type t

individual bit(X:t) : bool

module foomodule = {

    after init{
        bit(X) := true;
    }

    action flip(self:t) = {
        bit(self) := ~bit(self)
    }
}

instance foo(X:t) :foomodule
export foo.flip

extract iso_foo(me:t) = foo(me), bit(me)

The above script when verified using $ ivy_check study_interference.ivy, checks OK. However, when attempting to generate C++ codes, it provides the following errors.

  1. Using target=test
    
    $ ivyc isolate=iso_foo target=test study_interference.ivy 
    error: cannot strip parameter t from bit

$ ivyc isolate=iso_foo target=test build=true study_interference.ivy error: cannot strip parameter t from bit

$ ivy_to_cpp isolate=iso_foo target=test study_interference.ivy error: cannot strip parameter t from bit

$ ivy_to_cpp isolate=iso_foo target=test build=true study_interference.ivy error: cannot strip parameter t from bit

2. Using `target=repl` + with/without `build=true`

$ ivyc isolate=iso_foo target=repl build=true study_interference.ivy error: cannot strip parameter t from bit

$ ivyc isolate=iso_foo target=repl study_interference.ivy error: cannot strip parameter t from bit

$ ivy_to_cpp isolate=iso_foo target=repl build=true study_interference.ivy error: cannot strip parameter t from bit

$ ivy_to_cpp isolate=iso_foo target=repl study_interference.ivy error: cannot strip parameter t from bit


## Script modified to custom representation

lang ivy1.7

type t

module foomodule = {

individual bit(X:t) : bool

after init{
    bit(X) := true;
}

action flip(self:t) = {
    bit(self) := ~bit(self)
}

}

instance foo(X:t) :foomodule export foo.flip

extract iso_foo(me:t) = foo(me)

`ivy_checks OK`. 

$ ivy_check study_interference.ivy

Isolate this:

The following action implementations are present:
    study_interference.ivy: line 14: implementation of foo.flip

The following initializers are present:
    study_interference.ivy: line 9: foo.init[after1]

Any assertions in initializers must be checked ... PASS

OK

However, when we attempt to compile this to cpp, we obtain some errors. 
1. Produces no messages on terminal. No executable is generated.

$ ivy_to_cpp isolate=iso_foo target=repl study_interference.ivy


2. Produces an Executable. Can engage interactively from terminal.

$ ivy_to_cpp isolate=iso_foo target=repl build=true study_interference.ivy g++ -g -o study_interference study_interference.cpp -pthread

$ ./study_interference 1

foo.flip(1) foo.flip(3) foo.flip(43)

3. Compilation error when using `build=true` and either of `ivyc` or `ivy_to_cpp`

$ ivy_to_cpp isolate=iso_foo target=test build=true study_interference.ivy g++ -I /home/user/.local/lib/python2.7/site-packages/ivy/include -L /home/user/.local/lib/python2.7/site-packages/ivy/lib -Wl,-rpath=/home/user/.local/lib/python2.7/site-packages/ivy/lib -g -o study_interference study_interference.cpp -lz3 -pthread study_interference.cpp: In member function ‘virtual void extfooflip_gen::execute(study_interference&)’: study_interference.cpp:1244:35: error: no matching function for call to ‘study_interference::extfooflip(int&, int&)’ obj.extfooflip(prmX,self); ^ study_interference.cpp:1113:6: note: candidate: virtual void study_interference::extfoo__flip(int) void study_interference::extfooflip(int self){ ^~~~~~ study_interference.cpp:1113:6: note: candidate expects 1 argument, 2 provided

$ ivyc isolate=iso_foo target=test build=true study_interference.ivy g++ -I /home/user/.local/lib/python2.7/site-packages/ivy/include -L /home/user/.local/lib/python2.7/site-packages/ivy/lib -Wl,-rpath=/home/user/.local/lib/python2.7/site-packages/ivy/lib -g -o study_interference study_interference.cpp -lz3 -pthread study_interference.cpp: In member function ‘virtual void extfooflip_gen::execute(study_interference&)’: study_interference.cpp:1244:35: error: no matching function for call to ‘study_interference::extfooflip(int&, int&)’ obj.extfooflip(prmX,self); ^ study_interference.cpp:1113:6: note: candidate: virtual void study_interference::extfoo__flip(int) void study_interference::extfooflip(int self){ ^~~~~~ study_interference.cpp:1113:6: note: candidate expects 1 argument, 2 provided


I'd appreciate some help in understanding how to interpret these errors.