Using a method inside a predicate: Dafny

Question

I want to use a method inside a predicate. Brief explanation:

I have defined a data type RSState which looks like the following tuple.

datatype RSState = RSState(ceilingPrio: nat,
                            takenBy: nat,
                            cs: map<Process, TState>)

In the validity invariant, I want to set (check, not set... it's a predicate!) the ceilingPrio field using a Max method.

predicate validRS(r: RSState, T: set<Process>)
{
    r.cs.Keys == T &&
    r.ceilingPrio == Max(T)
}

The Max(T) is a method which finds the largest from a set:

datatype Process = Process(id: nat,
                    qPrio: nat)

function maximum(x: nat, y: nat): (m: nat)
    ensures m >= x
    ensures m >= y
{
    if x >= y then x else y
}

method Max(s: set<P>) returns (t: nat)
    requires s != {} && validTS(s)
    ensures forall p :: p in s ==> p.qPrio <= t
{
    var x :| x in s;
    if s == {x} {
        t := x.qPrio;
    } else {
        var s' := s - {x};
        var y := Max(s');
        t := maximum(x.qPrio, y);
    }
}

The predicate validRS fails saying: "expression is not allowed to invoke a method (Max)".

The solution I found uses the concept of Lambda functions in Dafny. I'm pretty lost after reading the documentation. I have used Lambda functions in Python and understand it conceptually but I'm failing to use it for my purpose.

Also, if I try to declare Max as a function method, the IDE complains the phrase 'function method' is not allowed when using --function-syntax:4; to declare a compiled function, use just 'function'

Answer 1

In Dafny, there is distinction between ghost and non ghost code. Ghost code is only present for verification. Non ghost code can be run by transpiling to other language (rust, c# etc in case of Dafny). There is also distinction between expression and statement.

Predicate body is expression but method invocation is statement. Since recent version of Dafny, predicate and function can be used in both ghost and non ghost context. Both can be prefixed with ghost like ghost predicate and ghost function to be used in ghost context exclusively. Now expression can't use statement like method call. Reason I think why it is not allowed here is to separate ghost & non ghost context (function) with non ghost context (method).

If you care about verification only just convert everything to ghost predicate and ghost function.

ghost function Max(s: set<Process>) : (t: nat)
  requires s != {} && validTS(s)
  ensures forall p :: p in s ==> p.qPrio <= t 
{
    var x :| x in s;
    if s == {x} then x.qPrio 
     else  
        var s' := s - {x};
        var y := Max(s');
        maximum(x.qPrio, y)
}

ghost predicate validRS(r: RSState, T: set<Process>)
    requires T != {} && validTS(T)
{
    r.cs.Keys == T && r.ceilingPrio == Max(T)
}