Assumption failed in tcp_test

[dijkstracula]

On commit 6f081c8c93 I'm observing an assertion failure in tcp_test:

➜  sandbox git:(main) ✗ ~/bin/ivyc target=test echo.ivy && ivy_launch cid=1 sid=1  echo

g++ -Wno-parentheses-equality  -std=c++11  -I /Users/ntaylor/code/ivy/ivy/include -L /Users/ntaylor/code/ivy/ivy/lib -Xlinker -rpath -Xlinker /Users/ntaylor/code/ivy/ivy/lib -I /usr/local/opt/openssl/include -L /usr/local/opt/openssl/lib -Xlinker -rpath -Xlinker /usr/local/opt/openssl/lib -fno-limit-debug-info -g -o echo echo.cpp -lz3 -pthread
ld: warning: directory not found for option '-L/usr/local/opt/openssl/lib'
`ivy_shell`; lldb -- ./echo 1 1 "[[0,{addr:0x7f000001,port:49124}],[1,{addr:0x7f000001,port:49125}]]" "[[0,{addr:0x7f000001,port:49126}],[1,{addr:0x7f000001,port:49127}]]"
NBT: PIDs: 39000
(lldb) target create "./echo"
Current executable set to '/Users/ntaylor/school/phd/projects/ivy_synthesis/sandbox/echo' (arm64).
(lldb) settings set -- target.run-args  "1" "1" "[[0,{addr:0x7f000001,port:49124}],[1,{addr:0x7f000001,port:49125}]]" "[[0,{addr:0x7f000001,port:49126}],[1,{addr:0x7f000001,port:49127}]]"
(lldb) process launch
Process 39008 launched: '/Users/ntaylor/school/phd/projects/ivy_synthesis/sandbox/echo' (arm64)
> client.server.ping(1,0,216)
< client.server.sock.send(1,{addr:2130706433,port:49124},{kind:ping_kind,sid:1,cid:0,val:216})
> client.server.ping(1,1,200)
< client.server.sock.send(1,{addr:2130706433,port:49125},{kind:ping_kind,sid:1,cid:1,val:200})
> client.server.ping(0,0,170)
< client.server.sock.send(0,{addr:2130706433,port:49124},{kind:ping_kind,sid:0,cid:0,val:170})
> client.sock.recv(0,{addr:2130706433,port:49126},{kind:pong_kind,sid:0,cid:0,val:170})
assumption_failed("/Users/ntaylor/code/ivy/ivy/include/1.8/network.ivy: line 287")
/Users/ntaylor/code/ivy/ivy/include/1.8/network.ivy: line 287: error: assumption failed
Process 39008 exited with status = 1 (0x00000001)

The offending line appears to be in tcp_test's ghost code for before recv:

284                     before recv {
285                         require net.len(src,id) > 0;
286                         var thing := net.queue(src,id);
287                         require msg = thing.value(0);
288                     }

The failing program is as follows:

➜  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]