Is it possible to remove precondition checks for unexported actions

[MadeByMars]

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.

[MadeByMars]

Here is a simple example:

#lang ivy1.7

include order
include udp

type node
interpret node -> bv[2]

instance round : unbounded_sequence
instance net : udp_simple(node,round)

isolate virtual_net = {
    relation msg(R: round, N: node)
    after init {
        msg(R, N) := false;
    }
    action send(r: round, n: node) = {
        msg(r, n) := true;
    }
}

isolate protocol = {
    object server(self: node) = {
        individual current : round
        after init {
            current := 0;
        }

        action start(r: round) = {
            current := r;
            call virtual_net.send(current, self+1);
        }

        action recv(r: round) = {
            require virtual_net.msg(r, self);
            require r > current;
            current := r;
        }
    }
} with node, round, virtual_net

isolate system = {
    object server(self: node) = {
        action print(r: round)
        action start(r: round) = {
            call protocol.server(self).start(r);
            call net.send(self, self + 1, r);
            call print(r);
        }

        implement net.recv(r: round) {
            if r > protocol.server(self).current {
                call print(r);
                call protocol.server(self).recv(r);
            }
        }
        import print
        export start
    }
    invariant net.spec.sent(R, N) -> virtual_net.msg(R, N)
} with node, round, protocol, net, virtual_net

extract iso_impl(self: node) = node, round, system, system.server(self), net(self), protocol.server(self)

ivy_check works fine, but ivyc would fail due to call to virtual_net and the precondition, which is not necessary in real implementation. I can either remove call virtual_net.send(current, self+1); or require virtual_net.msg(r, self); to compile it, but it would break the proof.