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.
➜ sandbox git:(main) ✗ cat echo.ivy
#lang ivy1.8
# An echo server implemented in Ivy.
# author: ntaylor
include collections
include network
include numbers
global {
type client_id = {0..cid}
type server_id = {0..sid}
alias byte = uint[8]
type msg_kind = {
ping_kind,
pong_kind
}
class msg_t = {
field kind : msg_kind
field sid : server_id
field cid : client_id
field val : byte
}
instance net: tcp_test.net(msg_t)
}
process client(self: client_id) = {
instance sock : net.socket
common {
specification {
# if a ping to client C from server S is not in flight at the moment
relation in_flight(S: server_id, C: client_id)
# - the value if a server S has pinged client C with a value and
# we have not yet received the response.
var pinged(S: server_id, C: client_id): byte
before server.ping(s: server_id, c: client_id, val: byte) {
require ~in_flight(s,c);
in_flight(s,c) := true;
pinged(s, c) := val;
}
before server.sock.send(s: server_id, src:tcp.endpoint, msg: msg_t) {
# Why might this make BMC hang?
#require msg.sid = s;
}
before server.sock.recv(s: server_id, src:tcp.endpoint, msg: msg_t) {
in_flight(s,msg.cid) := false;
}
before client.sock.recv(c: client_id, src:tcp.endpoint, msg: msg_t) {
require c = msg.cid;
require in_flight(msg.sid,msg.cid);
require pinged(msg.sid,msg.cid) = msg.val;
}
}
}
implementation {
implement sock.recv(src:tcp.endpoint, msg: msg_t) {
sock.send(src, msg)
}
}
common {
implementation {
process server(self: server_id) = {
export action ping(c: client_id, v: byte)
import action pong(c: client_id, v: byte)
instance sock : net.socket
implement ping {
var m: msg_t;
m.sid := self;
m.cid := c;
m.val := v;
sock.send(client(c).sock.id, m);
}
implement sock.recv(src:tcp.endpoint, msg: msg_t) {
pong(msg.cid, msg.val)
}
}
}
}
}
axiom client(X).sock.id = client(Y).sock.id -> X = Y
attribute method = bmc[10]
On commit
6f081c8c93
I'm observing an assertion failure intcp_test
:The offending line appears to be in
tcp_test
's ghost code forbefore recv
:The failing program is as follows: