Ironfleet toy lock refined

An Ivy model of the toy lock example from https://github.com/Microsoft/Ironclad/blob/master/ironfleet/src/Dafny/Distributed/Protocol/Lock/Node.i.dfy

A total order helper module

module total_order(t,r) = {
    axiom r(X:t,X)                        # Reflexivity
    axiom r(X:t, Y) & r(Y, Z) -> r(X, Z)  # Transitivity
    axiom r(X:t, Y) & r(Y, X) -> X = Y    # Anti-symmetry
    axiom r(X:t, Y) | r(Y, X)             # Totality
}

Types, relations and functions describing state of the network

type node
type epoch
type packet

epochs are totally ordered

relation (X:epoch <= Y:epoch)
instantiate total_order(epoch, <=)

module counter(t) = {
    action incr(input:t) returns (output:t) = {
        output := input + 1
    }
}

Abstract specification of counter. This outputs an arbitrary value greater than the input

module abs_counter(t,c) = {
    action incr(input:t) returns (output:t) = {
        assert ~(output <= input)
    }
    mixin incr after c.incr
}

module abs_formatter = {

This is a specification of a packet formatter

These are abstract destructuring functions for packets

       individual dst(P:packet) : node     # the destination address
       individual ep(P:packet) : epoch     # the packet's epoch

Make a packet. Right now there are only transfer packets so there is no tag needed.

       action mk_transfer(d:node,e:epoch) returns (p:packet) = {
           assert dst(p) = d & ep(p) = e
       }

}

module abs_low_intf(fmt) = {

This is a specification of the low-level packet interface. It allows for packet duplication. Parameter "fmt" is the packet formatter.

    relation sent(P:packet)  # the set of sent packets

    init ~sent(P)            # initially, no packets sent

    action send(p:packet) = {
        sent(p) := true
    }

    action recv(dst:node) returns(p:packet) = {
        assert sent(p) & fmt.dst(p) = dst
    }
}

module net_intf(lower,fmt) = {

This is a specification of a network interface that allows sending and receiving of messages tagged with epochs. The specification allows messages to be arbitrarily duplicated.

This is a concrete implementation that sends and receives formatted packets via a lower-level service

The parameter "lower" is the lower-level interface and "fmt" is the packet formatter.

send a transfer message to destination address

    action send_transfer(e:epoch, dst:node) = {
        local p : packet {
        p := fmt.mk_transfer(dst,e);
        call lower.send(p)
        }
    }

receive a transfer message to destination address

    action recv_transfer(dst:node) returns (e:epoch) = {
        local p : packet {
        p := lower.recv(dst);
        e := fmt.ep(p)
        }
    }

    conjecture l.sent(P) -> an.transfer(f.ep(P),f.dst(P))

}

module abs_net_intf(net) = {

This is a specification of a network interface that allows sending and receiving of messages tagged with epochs. The specification allows messages to be arbitrarily duplicated.

This is an abstract specification that is not concerned with the actual message format. We will add that as a refinement.

state of abstract network interface

    relation transfer(E:epoch, N:node)  # the node is the message destination
    init ~transfer(E, N)

send a transfer message to destination address

    action send_transfer(e:epoch, dst:node) = {
        transfer(e,dst) := true
    }
    mixin send_transfer after net.send_transfer

receive a transfer message to destination address

    action recv_transfer(dst:node) returns (e:epoch) = {
        assert transfer(e,dst)  # see (*) below
    }
    mixin recv_transfer after net.recv_transfer

(*) Why is this "assert" and not "assume"? This is a rely/guarantee spec. The implementation of "send_transfer" must guarantee that the assert holds, while the client assumes it. Thus, the assert takes the role of assert or assume depending on context.

}

module proto(cnt,net) = {

This module models all of the nodes. We really want to have an object representing a single node. For that we need a way of assigning unique ids to the nodes.

ep(n) is the current epoch of node n

    individual ep(N:node) : epoch

held(n) is true iff the lock is currently held by node n

    relation held(N:node)

initially exactly one node holds the lock, and all others have epoch zero

    individual first:node

    init held(X) <-> X=first
    init N ~= first -> ep(N) = 0
    init ~(ep(first) <= 0)

set of locked messages, initially none

    relation locked(E:epoch, N:node)  # the node is the message source
    init ~locked(E, N)

Protocol description

release the lock and send a transfer message

    action grant(n1:node, n2:node) = {
        local e: epoch {
        assume held(n1);
        e := cnt.incr(ep(n1));
        call net.send_transfer(e, n2);
        held(n1) := false
        }
    }

receive a transfer message and take the lock, sending a locked message

    action accept(n:node) = {
        local e:epoch {
        e := net.recv_transfer(n);
        if ~(e <= ep(n)) {
        held(n) := true;
        ep(n) := e;
        locked(e, n) := true
        }
    }
    }

added just to have something to verify (mutual exclusion)

    action critical(n:node) = {
        assume held(n);
        assert X ~= n -> ~held(X)
    }

invariant conjectures

no two locked at same epoch (as a sanity check)

    conjecture locked(E, N1) & locked(E, N2) -> N1 = N2

epochs transfer to at most one node

    conjecture an.transfer(E, N1) & an.transfer(E, N2) -> N1 = N2

if a node sent a locked msg, the node's epoch is now higher

    conjecture locked(E, N) -> (E <= ep(N))

holding node's epoch is higher than any other node's epoch (this implies a single node holds the lock)

    conjecture held(N) & N ~= M -> ~(ep(N) <= ep(M))

holding node's epoch is higher than any transfer's epoch

    conjecture held(N) & an.transfer(E, M) -> (E <= ep(N))

pending transfer epoch is higher than any node's epoch

    conjecture an.transfer(E, N) & ~(E <= ep(N)) -> ~(E <= ep(M))

pending transfer epoch is higher than any transfer's epoch

    conjecture an.transfer(E, N) & ~(E <= ep(N)) & an.transfer(F, M) -> (F <= E)
}

Instantiate the modules to build a system

Notice that the formatter and low interface are currently abstract specifications that could be refined in the future.

instantiate c : counter(epoch)
instantiate f : abs_formatter()
instantiate l : abs_low_intf(f)
instantiate n : net_intf(l,f)
instantiate p : proto(c,n)

The type epoch is implemented with native type "int"

interpret epoch -> int

This is the service we provide to the environment

export p.grant
export p.accept
export p.critical

All after this is proof

Overlay the abstract counter specification

instantiate an : abs_net_intf(n)
instantiate ac : abs_counter(epoch,c)

When we verify the protocol claim, we use the abstract counter spec. Notice that we also ignore the implementation of "epoch", so for this claim we treat "epoch: as uninterpreted, leaving us in EPR.

isolate iso_p = p with an,ac

When we verify concrete counter, we use the implementation of "epoch", since we need the arithmetic theory. In this case we are in QF_LRA, which is also decidable.

isolate iso_c = c with ac,epoch

When we verify claims about the network interface, we leave "epoch" abstract. We keep the state of the abstract spec, and the lower and formatter interface specs.

isolate iso_n = n with an, l, f