Code Extraction - for Asymmetric Protocols

[prpr2770]

Compiled using IVy 1.7

I'm attempting to re-implement the PING-PONG tutorial, with the networking module, so that the actions ping and pong may be translated into messages sent over the network. The correctness of the ping-pong protocol, should be checked for correctness, in consideration of the network dynamics.

source:Specification Tutorial

I have attempted to implement this, using the following codebase. However, it generates the following error:

$ ivy_check ping_pong_trans_v2.ivy 

Isolate abstract_protocol:
error: The verification condition is not in the fragment FAU.

The following terms may generate an infinite sequence of instantiations:

ping_pong_trans_v2.ivy: side(neighbor(N_b))
    (position 0 is a function from node to node)

Is there an alternative/easier representation that's possible within IVy? Or is the code-extraction within IVy designed only for symmetric protocols?

#lang ivy1.7

include order
include timeout 
include udp

isolate id = {
    type this

    specification{
        instantiate totally_ordered(this)
    }

    implementation{
        interpret this -> bv[32]
    }
}

object node = {
    type this

    object leftnode = {
        variant this of node 
    }

    object rightnode = {
        variant this of node
    }

}

interpret node ->bv[1]

parameter pid(N:node) : id
axiom [pid_injective] pid(N) = pid(M) -> N = M

# Captures the GLobal-Network: Mapping between LeftPlayers and RightPlayers
parameter neighbor(N:node) : node
axiom [neighbor_one_to_one] neighbor(N) = neighbor(M) <-> N = M
#axiom [neighbor_no_self_loop] neighbor(N) ~= N

# Captures the global-notion of SIDE
parameter side(N:node) : bool
axiom [opponents_sides] side(N) & side(neighbor(N)) = 0

type packet={ping, pong}
type players_t = {left, right}

isolate abstract_protocol ={

    # -------------------------------------
    # INTERFACE: 
    # -------------------------------------

    # HOW TO REPRESENT STATE - OF WHICH AGENT's side it is. 
    # function side(n:node, m:node) : players_t

    action send(n:node, p:packet)           # node-n sends pid-p to the next-node in the ring.

    action ping
    action pong

    # -------------------------------------
    # SPECIFICATION: 
    # -------------------------------------
    specification{
        relation sent(P:packet, N:node)    

        after init{
            sent(P,N) := false;         # Empty Channel.

            # How should this be initialized, such that the left-agents can initialize their pings.
            # Is this already captured by the property: `opponents_sides` ??
            #side(N:node.leftnode) := true;      # LEFT-NODES
            #side(N:node.rightnode) := false;    # RIGHT-NODES
        }

        after send{

            sent(p, neighbor(n)) := true;
        }

    }

} with node, id, pid_injective, neighbor_one_to_one, opponents_sides #, neighbor_no_self_loop

isolate refined_protocol_left = {

    # -------------------------------------
    # INTERFACE: 
    # -------------------------------------
    # THere's no interface. At each timer-expiry, the LEFT-NODE sends the PING-message if it has its turn set.

    individual ball : bool
    after init {
        ball := true
    } 

    # -------------------------------------
    # IMPLEMENTATION:  SEQUENTIAL REACTIVE PROGRAM
    # -------------------------------------
    implementation{

        #instantiate net: udp_simple2(node.leftnode, packet)      # Networking Service: `address_type`: node, `packet_type`: packet
        instantiate net: udp_simple2(node, packet)      

        # PARAMETERIZED collection of instances of the `timeout_sec` service:
        #instantiate timer(N:node.leftnode) : timeout_sec     # There is ONE instance of `timeout_sec` for each node 
        instantiate timer(N:node) : timeout_sec     # There is ONE instance of `timeout_sec` for each node 

        implement timer.timeout(self:node){

            if ball{
                call abstract_protocol.send(self, ping);   

                # PING

                # ACTUAL: 
                call net.send(self, neighbor(self), ping);
                ball := false;            
            };

        }

        #implement net.recv(self:node.leftnode, v:packet){
        implement net.recv(self:node, v:packet){

            if v=pong{
                # GHOST: Having NO EFFECT in extracted implementation. 
                call abstract_protocol.pong;

            };

        }
    }

    private{        # REFINEMENT RELATION

        # [Prop 3] The state of the implementation should be mapped to corresponding states of the abstract-protocol state. 
        invariant net.sent(V,N) -> abstract_protocol.sent(V,N)

        # TODO: How do we represent this relationship between the ConcreteModel and the AbstractModel? 
        #invariant ball -> side(self) = true
    }

#} with node.leftnode, id, pid_injective, neighbor_one_to_one, neighbor_no_self_loop
} with abstract_protocol, node, id, pid_injective, neighbor_one_to_one, opponents_sides #, neighbor_no_self_loop

#extract leftcode(n:node.leftnode) = refined_protocol(n), pid(n), node.leftnode, id
extract leftcode(n:node) = refined_protocol_left(n), pid(n), node, id

isolate refined_protocol_right = {

    # -------------------------------------
    # INTERFACE: 
    # -------------------------------------
    # THere's no interface. At each timer-expiry, the UE sends the PING-message if it has its turn set. 

    individual ball : bool
    after init {
        ball := false;
    } 

    # -------------------------------------
    # IMPLEMENTATION:  SEQUENTIAL REACTIVE PROGRAM
    # -------------------------------------
    implementation{

        #instantiate net: udp_simple2(node.rightnode, packet)      # Networking Service: `address_type`: node, `packet_type`: id
        instantiate net: udp_simple2(node, packet)     

        # PARAMETERIZED collection of instances of the `timeout_sec` service:
        #instantiate timer(N:node.rightnode) : timeout_sec     # There is ONE instance of `timeout_sec` for each node 
        instantiate timer(N:node) : timeout_sec

        #implement timer.timeout(self:node.rightnode){
        implement timer.timeout(self:node){

            if ball{
                # GHOST: Having NO EFFECT in extracted implementation. 
                call abstract_protocol.send(self, pong);   

                # ACTUAL: 
                call net.send(self, neighbor(self), pong);
                ball := false;            
            };

        }

        #implement net.recv(self:node.rightnode, v:packet){
        implement net.recv(self:node, v:packet){

            if v=ping{
                # GHOST: Having NO EFFECT in extracted implementation. 
                call abstract_protocol.ping;

            };

        }
    }

    private{        # REFINEMENT RELATION

        # [Prop 3] The state of the implementation should be mapped to corresponding states of the abstract-protocol state. 
        invariant net.sent(V,N) -> abstract_protocol.sent(V,N)

        # TODO: How do we represent this relationship between the ConcreteModel and the AbstractModel? 
        #invariant ball -> (abstract_protocol.side = left)
        #invariant ball -> side(self) = true
    }

#} with node.rightnode, id, pid_injective, neighbor_one_to_one, neighbor_no_self_loop
} with abstract_protocol, node, id, pid_injective, neighbor_one_to_one, opponents_sides #, neighbor_no_self_loop

#extract rightcode(n:node.rightnode) = refined_protocol(n), pid(n), node.rightnode, id
extract rightcode(n:node) = refined_protocol_right(n), pid(n), node, id

[prpr2770]

While making the following assumptions:

1. The different entities participating in the protocol, should NOT be separate isolates, with a separation of their actions and specifications. They should be merged into a single entity description, as the code-extraction and definition of the udp requires definition of a single node type, that gets mapped to a process in the OS.
2. The primary focus is to not model the interface as being defined by the actions, but to first capture the send/recv functionality. And then build the action definitions around the derived structure.
3. The EVEN-Numbered Nodes shall be left-players and the ODD-Numbered Nodes shall be right-players.
4. The abstract protocol SHOULD be parameterized on both the (src:node, dest:node).

We obtain the following errors:

$ ivy_check trace=true ping_pong_trans_v4.ivy 

...
 The following program assertions are treated as guarantees:
        in action node.next when called from refined_protocol.net.recv,refined_protocol.timer.timeout,refined_protocol.timer.timeout:
            /home/user/.local/lib/python2.7/site-packages/ivy/include/1.7/order.ivy: line 92: guarantee ... FAIL
searching for a small model... done
two numerals assigned same value!: 2:node = 0:node
two numerals assigned same value!: 2:node = 0:node
two numerals assigned same value!: 2:node = 0:node
[
    refined_protocol.net.sent(msg_ping,0) = true
    refined_protocol.net.sent(msg_pong,0) = true
    node.succ(0,0) = false
    0:node < 0 = false
    2:node = 0
    0:node = 0
    pid(0) = 0
    0:id < 0 = false
    0:node * 0 = 0
    abstract_protocol.sent(msg_ping,0) = true
    abstract_protocol.sent(msg_pong,0) = true
    node.max = 0
    refined_protocol.ball(0) = false
    abstract_protocol.protocolSide(0,0,left) = false
    abstract_protocol.protocolSide(0,0,right) = false
    abstract_protocol.protocolSide(0,0,none) = false
]
fail call refined_protocol.net.recv
{
    [
        fml:v = msg_pong
        fml:dst = 0
    ]
    /home/user/.local/lib/python2.7/site-packages/ivy/include/1.7/udp.ivy: line 194: assume refined_protocol.net.sent(fml:v,fml:dst)

    ping_pong_trans_v4.ivy: line 213: refined_protocol.ball(fml:dst) := true

    [
        refined_protocol.ball(0) = true
        loc:0 = 0
    ]
    ping_pong_trans_v4.ivy: line 219: call loc:0 := node.next(fml:dst)
    {
        [
            fml:x = 0
        ]
        /home/user/.local/lib/python2.7/site-packages/ivy/include/1.7/order.ivy: line 92: assert exists S. S:node > fml:x

    }

}

$ ivy_check ping_pong_trans_v4.ivy 
...
error: failed checks: 4

We derive the following definition for the ping-pong example.

#lang ivy1.7

# Attempt at combining the `left-node` and `right-node` into a single `node` description. Also, combining their functionalities. 
# LEFT-PLAYERS are EVEN-NUMBERED. 

include order
include timeout 
include udp

isolate id = {
    type this

    specification{
        instantiate totally_ordered(this)
    }

    implementation{
        interpret this -> bv[8]
    }
}

instance node : iterable    # from library.order

object node = { ...         # include the desription extracted from the definition of `iterable` 

    action get_next(x:this) returns (y:this)
    action get_prev(x:this) returns (y:this)

    specification{

        # `get_next` has the property that: 
        # 1. either we wrap around ( i.e. the output is least element and the input is the greatest) [(y <= X & X <= x)]
        # 2. or, the output is the successor of the input ( i.e the output is greater than input and that there's no other element in between them. ) [(x<y & ~(x <Z & Z<y)]

        after get_next{
            # default: (x<y & ~(x <Z & Z<y))
            # wrap-around: (y <= X & X <= x)
            ensure (y <= X & X <= x) | (x<y & ~(x <Z & Z<y))
        }

        after get_prev{
            # wrap-around: (x <= X & X <= y)
            # default: (y<x & ~(y <Z & Z<x))
            ensure (x <= X & X <= y) | (y<x & ~(y <Z & Z<x))
        }

    }

    # NOTE: we describe the property as an `ensure` : This suggests that the onus is on the implementation of this module to guarantee that this property holds
    # Therefore, we need to write an appropriate implementation. 

    implementation{

        implement get_next{
            y:= 0 if x = node.max else x.next; 
        }

        implement get_prev{
            y:= node.max if x = 0 else x.prev; 
        }
    }

}

parameter pid(N:node) : id
axiom [pid_injective] pid(N) = pid(M) <-> N = M

type side_t = {left, right, none}

type packet={msg_ping, msg_pong}

isolate abstract_protocol ={

    # -------------------------------------
    # INTERFACE: 
    # -------------------------------------

    # HOW TO REPRESENT STATE - OF WHICH AGENT's side it is. 
    relation protocolSide(X:node, Y:node, Z:side_t)

    action send(src:node, dest:node, p:packet)           # node-n sends pid-p to the next-node in the ring.

    action ping(src:node, dest:node)
    action pong(src:node, dest:node)

    # -------------------------------------
    # SPECIFICATION: 
    # -------------------------------------
    specification{
        relation sent(P:packet, N:node)    

        after init{
            sent(P,N) := false;  
            protocolSide(X,Y,none):= true;

            # EVEN LEFT-PLAYERS
            #protocolSide(X, X.next,left):= ( (X/2)*2 = X )
            #require forall X:node. protocolSide(X, M,left) = ( (X/2)*2 = X ) & ( (M <= P & P <= X) | (X<M & ~(X <Q & Q<M)) )
            require forall X:node. protocolSide(X, M,left) = ( (X/2)*2 = X ) & ( M = X + 1 )

        }

        after send{
            sent(p, dest) := true;   
        }

        before ping {
            assert protocolSide(src, dest,left) = true;
            protocolSide(src, dest,left) := false;
            protocolSide(src, dest, right) := true;
        }

        # When `pong` occurs, the ball must be on the right. It moves to the left.

        before pong {
            assert protocolSide(dest, src, right) = true;
            protocolSide( dest, src, right) := false;
            protocolSide(dest, src, left) := true;
        }

        private{

            # Conditions NOT IN FAU
            #invariant sent(msg_ping, X) -> ( (X/2)*2 ~= X )
            #invariant sent(msg_pong, X) -> ( (X/2)*2 = X )
        }

    }

} with node, id, pid_injective 

isolate refined_protocol = {

    # -------------------------------------
    # INTERFACE: 
    # -------------------------------------
    # THere's no interface. At each timer-expiry, the LEFT-NODE sends the PING-message if it has its turn set.

    specification{

        relation ball(S:node)

        after init(self:node) {

            ball(Y) := false;
            ball(self) := true;
        }     
    }

    # -------------------------------------
    # IMPLEMENTATION:  SEQUENTIAL REACTIVE PROGRAM
    # -------------------------------------
    implementation{

        #instantiate net: udp_simple2(node.leftnode, packet)      # Networking Service: `address_type`: node, `packet_type`: packet
        instantiate net: udp_simple2(node, packet)      

        # PARAMETERIZED collection of instances of the `timeout_sec` service:
        instantiate timer(N:node) : timeout_sec     # There is ONE instance of `timeout_sec` for each node 

        implement timer.timeout(self:node){

            if ball(self){

                if ((self/2) * 2 ~= self){ # Odd Numbers are Right-Players

                    call abstract_protocol.send(self, self.prev, msg_pong);   

                    # PONG

                    call net.send(self, self.prev, msg_pong);

                }else{ # Even Numbers are Left-Players

                    call abstract_protocol.send(self, self.next, msg_ping);   

                    # PING

                    call net.send(self, self.next, msg_ping);

                };

                ball(self) := false;            
            };

        }

        implement net.recv(self:node, v:packet){

            ball(self) := true;

            if (v=msg_pong & (self/2) * 2 = self){

                # LEFT-PLAYER(EVEN) RECEIVES PONG

                call abstract_protocol.pong( self.next, self);

            };

            if (v=msg_ping & (self/2) * 2 ~= self){

                # RIGHT-PLAYER(ODD) RECEIVES PING

                call abstract_protocol.ping( self.prev, self);

            };

        }
    }

    private{        

        # [Prop 3] The state of the implementation should be mapped to corresponding states of the abstract-protocol state. 
        invariant net.sent(V,N) -> abstract_protocol.sent(V,N)

    }

} with abstract_protocol, node, id, pid_injective 

extract code(n:node) = refined_protocol(n), pid(n), node, id

[prpr2770]

We adopted a simpler strategy to get the UDP implementation working. However, it generates the following error:

$ ivy_check ping_pong_udp_sendrecv.ivy
...
Initialization must establish the invariant
player.id := Yfml:self:side_t
ping_pong_udp_sendrecv.ivy: line 59: error: multiply assigned: player.id

May I have some guidance on what causes the multiple-assignment? I'd really appreciate some help with this issue.

#lang ivy1.7

include udp
#include tcp 

type side_t = {left,right}
type msg_t = {ping, pong}

isolate intf = {

    # actions are parameterized by the receiver. 
    action ping(dst:side_t) 
    action pong(dst:side_t)

    specification {
        individual side : side_t

        after init {
            side := left
        }

        before ping {
            require side = left;
            side := right
        }

        before pong {
            require side = right;
            side := left
        }

    }

}

isolate player = {

    action hit(self:side_t)
    action objectify(self:side_t)

    specification{

        individual ball : bool
        individual id: side_t

        after init(self:side_t){ 

            #call objectify(self);

            id := self;

            if (id=left){
                ball := true;
            }else{
                ball := false;
            };

        }

        after objectify(self:side_t){

            if (self=left){
                id := left;
                ball := true;
            }else{
                id := right;
                ball := false;
            };
        }

        private{
            invariant ball -> intf.side = left
        }

    }

    implementation{

        instance trans : udp_simple2(side_t, msg_t)

        implement intf.pong(self:side_t) {
            ball := true
        }

        implement intf.ping(self:side_t) {
            ball := true
        }

        implement trans.recv(self:side_t, v:msg_t){

            if (v = ping & ball){
                #call intf.ping(left, dst);
                call intf.ping(self);
            };

            if (v = pong & ball){
                call intf.pong(self);
            };

        }

        implement hit(self:side_t) {
            if ball {

                if(id = left){
                    #call intf.ping;
                    call trans.send(id, right, ping);
                    ball := false            
                }else{

                    #call intf.pong;
                    call trans.send(id, left, pong);
                    ball := false;         

                };

            }
        }

    }

} with intf, side_t

export player.hit

[prpr2770]

We got the following description of the ping-pong using udp.send-recv to compile correctly. However, when we attempt to generate the executable, we obtain the following error:

$ ivyc ping_pong_udp_sendrecv_v2_b.ivy
ping_pong_udp_sendrecv_v2_b.ivy: line 55: error: cannot strip isolate parameters from ext:player.hit

Modification of the code to the following gist generates the following error:

$ ivyc ping_pong_udp_sendrecv_v2_b_1.ivy 
ping_pong_udp_sendrecv_v2_b_1.ivy: line 79: error: mixin player.intf_pong[implement31] has wrong number of input parameters for intf.pong

The code that ivy_check OK is provided below:

#lang ivy1.8

include udp

type side_t = {left,right}
type msg_t = {ping, pong}

isolate intf = {
    action ping(dest:side_t)
    action pong(dest:side_t)

    specification {
        individual side : side_t

        after init {
            side := left
        }

        before ping {
            require side = left;
            side := right
        }

        before pong {
            require side = right;
            side := left
        }

    }

} 

isolate player = {
    individual ball : bool
    individual id: side_t

    after init{ 

        if *{
            id := left;
            ball := true;
        }else{
            id := right;
            ball := false;
        };

    }

    action hit = {
        if ball {

            if(id = left){
                #call intf.ping;
                ball := false;
                call trans.send(id, right, ping);

            }else{

                #call intf.pong;
                ball := false;
                call trans.send(id, left, pong);

            };

        }
    }

implementation{
    instance trans : udp_simple2(side_t, msg_t)

    implement intf.pong {
        #require id=left;
        ball := true;
    }

    implement intf.ping {
        #require id=right;
        ball := true;
    }

    implement trans.recv(self:side_t, v:msg_t){
        #require ~ball; 

        if (v = ping & ~ball & id=left & id=self){
            call intf.ping(self);
        };

        if (v = pong & ~ball& id=right & id=self){
            call intf.pong(self);
        };

    }

}

    private{
        # 1: 
        invariant ball & id = left -> intf.side = left
        # 2: 
        invariant ball & id = right -> intf.side = right

        # 3: constraints on the system messages
        invariant ~trans.sent(ping,left) & ~trans.sent(pong,right)

    }

} with intf, side_t

export player.hit

extract code(n:side_t) = player(n), intf, side_t