Partial axiomatization of hybrid logic assertions for actors in Dafny

Actors.dfy

module ActorCore {
    class {:extern} ActorRef<Ms> {}
    predicate {:extern} at<T,Ms>(i: ActorRef<Ms>, p:(T ~> bool))
    /* at[i](_) is a modality */
    lemma 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 self() : ActorRef<Msgs> reads this
        var state: State
        constructor {:extern} () ensures inv()
        predicate inv() reads this

        method 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 introAt(r:Actor)
            requires r.self() == loc
            requires P(r.state)
            ensures at(r.self(), P)
        { assume at(r.self(), P); }
        static method Unpack(w:Witness)
            ensures at(w.loc, w.P)
        {
            assume at(w.loc, w.P);
        }
    }
}




module CounterStuff {


    module CounterMod refines DafnyActor {
	// Work around Dafny issue 332 (https://github.com/dafny-lang/dafny/issues/332)
	// I've introduced a local guarantee Gsub (here and in the manager) giving what
	// *should* be the refined definition of G, and added it as a postcondition to
	// both receive methods.
        twostate predicate stableSub(a:Actor, P:State~>bool) reads a, P.reads {
            (old(P.requires(a.state) && P(a.state)) &&
            a.Gsub())
            ==> (P.requires(a.state)) && P(a.state)
        }
        class Witness {
            var lb: nat
            predicate P(s:State) { lb <= s }
            twostate lemma stability(x:Actor)
                ensures stable(x, P)
                ensures stableSub(x, P)
            {
                // This fails to check the stableSub postcondition (added to work 'fake' a fix to the twostate predicate refinement bug) because I can't add the extra required precondition I added to substable(Actor). 
                assume lb == old(lb);
		// Work around Dafny issue 332 (https://github.com/dafny-lang/dafny/issues/332)
                assume x.Gsub() ==> x.G(); 
                assert stableSub(x,P);
            }
            twostate lemma substable(x:Actor)
		// 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.
                requires lb == old(lb) 
                requires old(P(x.state))
                requires x.Gsub()
                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 Gsub() reads this { old(this.state) <= state }

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

                assert Gsub();
		// Work around Dafny issue 332 (https://github.com/dafny-lang/dafny/issues/332)
                assume Gsub() ==> G();
            }

        }

    }
    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 Gsub() reads this { 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 Gsub()
            {
                var sender := message.loc;
                CounterMod.Witness.Unpack(message);
                atImpl(sender, message.P, (s:nat) reads message => message.lb <= s);
                assert (at(sender, (s:nat) reads message => message.lb <= s));
                if (sender == child && state < message.lb) {
                    state := message.lb;
                    atImpl(child, (s:nat) reads message => message.lb <= s, (s:nat) reads this => this.state <= s);
                } 
                // Gsub here is a standin for G... which I can't refine correctly due to a Dafny bug
                assert Gsub();
                assume Gsub() ==> G();
            }
        }
    }
}