Prototyping Actor verification in Dafny

HybridAssertionsForActors.dfy

/*
 * Sample code for the AGERE 2019 paper "Modal Assertions for Actor Correctness" by Colin S. Gordon, DOI 10.1145/3358499.3361221.
  * Note that at the time of this writing, there is an issue (https://github.com/dafny-lang/dafny/issues/359) where this file only verifies from the command line (modulo complains about missing implementations of abstract methods).  Currently, verifying this via the Dafny Visual Studio Code plugin runs into trouble with the higher-order predicates.

 * Last checked with a local build of Dafny commit 8f141e9d05b2dba9de4ba997040df6166c2d168c and Boogie commit bc49937e7ee88e931bbe2dbf779a42612731a8fd
 */

module ActorCore {
    class {:extern} ActorRef<Ms> {}
    predicate {:extern} at<T,Ms>(i: ActorRef<Ms>, p:(T ~> bool))
    /* at[i](_) is a modality */
    lemma {:extern} atImpl<T,M>(c:ActorRef<M>, P:T~>bool, Q:T~>bool)
        requires forall x:T :: P.requires(x) ==> Q.requires(x)
        requires forall x:T :: P.requires(x) ==> P(x) ==> Q(x)
        ensures at(c, P) ==> at(c, Q)
    /* When using the above, Dafny sometimes doesn't notice the precondition holds;
    this variant forces it to look for it. */
    lemma atImpl2<T,M>(c:ActorRef<M>, P:T~>bool, Q:T~>bool)
        requires forall x:T :: P.requires(x) ==> Q.requires(x)
        requires forall x:T :: P.requires(x) ==> P(x) ==> Q(x)
        requires at(c,P)
        ensures at(c, Q)
    {
        atImpl(c,P,Q);
    }

    /* Generic utility for packing a sender with an arbitrary message */
    class MsgBox<T,U> {
        var sender: ActorRef<T>
        var msg: U
        constructor(s:ActorRef<T>, m:U) {
            sender := s;
            msg := m;
        }
    }
}


abstract module DafnyActor {
    import opened ActorCore
    type State
    type Msgs

    twostate predicate stable(a:Actor, P:State~>bool) reads a, P.reads {
        (old(P.requires(a.state) && P(a.state)) &&
        a.G())
        ==> (P.requires(a.state)) && P(a.state)
    }

    class Actor {

        twostate predicate G() reads this

        function method {:extern} self() : ActorRef<Msgs> reads this
        var state: State
        constructor {:extern} () ensures inv()
        predicate inv() reads this

        method {:extern} send<T>(dest: ActorRef<T>, msg:T)
        method receive(message: Msgs)
            modifies this
            requires inv()
            ensures inv()
            ensures G()
    }

    class Witness {
        var loc: ActorRef<Msgs>
        predicate P(s:State) reads this
        twostate lemma stability(x:Actor)
            ensures stable(x, P)
        constructor(r:Actor)
            ensures P(r.state)
            ensures at(r.self(), P)
        lemma {:extern} introAt(r:Actor)
            requires r.self() == loc
            requires P(r.state)
            ensures at(r.self(), P)
        static method {:extern} Unpack(w:Witness)
            ensures at(w.loc, w.P)
    }
}




module CounterStuff {


    module CounterMod refines DafnyActor {
        class Witness {
            var lb: nat
            predicate P(s:State) { lb <= s }
            twostate lemma stability(x:Actor)
                ensures stable(x, P)
            {
                // Currently no way in Dafny to say all fields of an object remain fixed, which would need to be in the *abstract* module's precondition.
                // Hack it here by stating this specifically for lb.
                // Would be fixed by adding object immutability to Dafny.
                assume lb == old(lb);
            }
            twostate lemma substable(x:Actor)
                requires lb == old(lb) 
                requires old(P(x.state))
                requires x.G()
                ensures P(x.state)
            {
                assert (lb <= old(x.state));
                assert (old(x.state) <= x.state);
            }
            constructor(r:Actor)
                ensures P(r.state)
                ensures at(r.self(), P)
            {
                lb := r.state;
                loc := r.self();
                new;
                assert P(r.state);
                introAt(r);
            }
        }

        type State = nat
        type Msgs = MsgBox<Witness,nat>

        class Actor {

            constructor()
                ensures inv()
            {
                state := 0;
                new;
            }
            twostate predicate G() { old(this.state) <= state }

            predicate inv() { 0 <= this.state }
            method receive(message: Msgs)
                ensures inv()
                ensures G()
            {
                state := state + message.msg;
                var w := new Witness(this);
                send(message.sender, w);
            }

        }

    }
    module ManagerMod refines DafnyActor {
        import CounterMod
        type State = nat
        type Msgs = CounterMod.Witness
        class Actor {
            function method self() : ActorRef<Msgs>

            var child: ActorRef<MsgBox<CounterMod.Witness,nat>>

            twostate predicate G() { old(child)==child && old(state) <= state && at(child, (s:nat) reads this => state <= s) }
            predicate inv() { at(child, (s:nat) reads this => state <= s) }
            method send<T>(dest: ActorRef<T>, msg:T)
            method receive(message: Msgs)
                ensures inv()
                ensures G()
            {
                assert inv();
                assert (at(child, (s:nat) reads this => state <= s));
                CounterMod.Witness.Unpack(message);
                var sender := message.loc;
                assert (at(message.loc, message.P));
                assert (at(sender, message.P));
                atImpl2(message.loc, message.P, (s:nat) reads message => message.lb <= s);
                assert (at(message.loc, (s:nat) reads message => message.lb <= s));
                if (message.loc == child && state < message.lb) {
                    state := message.lb;
                    atImpl2(child, (s:nat) reads message => message.lb <= s, (s:nat) reads this => this.state <= s);
                    assert (old(child) == child);
                    assert (old(state) <= state);
                    assert (at(child, (s:nat) reads this => this.state <= s));
                    assert G();
                } 
                assert G();
            }
        }
        class {:extern} Witness { 
            // Hack so the dafny compiler doesn't complain about missing Witness implementation for a module that doesn't need it
            twostate lemma {:extern} stability(x:Actor)
            predicate {:extern} P(s:State)
            constructor {:extern} (r:Actor)
        }
    }
}