Stuck in verification

[MikaelMayer]

Dafny version

latest-nightly

Code to produce this issue

// Encoding of Boogie references in Dafny
  datatype World<!A(==), !FieldValue> = World(
      a_to_object: A -> object,
      fields: A ~> set<FieldValue>,
      reachable: FieldValue -> set<A>,
      all_a: set<A>) {
    ghost function AllObjects(): set<object> {
      set a <- all_a :: a_to_object(a)
    }
    ghost predicate closed()
       reads AllObjects()
    {
      forall a: A <- all_a ::
        && fields.requires(a) // insufficient reads clause to invoke function
        && fields.reads(a) <= AllObjects()
        && forall f <- fields(a) :: reachable(f) <= all_a
    }
      }

and If I reverse the reads and requires

// Encoding of Boogie references in Dafny
  datatype World<!A(==), !FieldValue> = World(
      a_to_object: A -> object,
      fields: A ~> set<FieldValue>,
      reachable: FieldValue -> set<A>,
      all_a: set<A>) {
    ghost function AllObjects(): set<object> {
      set a <- all_a :: a_to_object(a)
    }
    ghost predicate closed()
       reads AllObjects()
    {
      forall a: A <- all_a ::
        && fields.reads(a) <= AllObjects() // Function precondition could not be proved + insufficient reads clause
        && fields.requires(a)
        && forall f <- fields(a) :: reachable(f) <= all_a
    }
      }

Command to run and resulting output

Paste in VSCode

What happened?

I can no longer specify anything about general function that read the heap but don't have preconditions I have to bring a tower of reads and no foundation.

What should work here is to be able to stop at

        && fields.reads.reads(a) == {}
        && fields.reads.requires(a)

But I don't know if it's sound.

What type of operating system are you experiencing the problem on?

Windows

[keyboardDrummer]

@MikaelMayer could you be more verbose in your problem description? It's not clear to me what the issue is.

[MikaelMayer]

Updated description.

[keyboardDrummer]

It seems like Dafny is telling you that you don't have sufficient reads clauses to invoke fields. What makes you think that you do? I don't see the reads clause of fields specified anywhere, so I would think it could be anything and that this prevents you from proving that you satisfy it.

The following program is accepted:

// Encoding of Boogie references in Dafny
  datatype World<!A(==), !FieldValue> = World(
      a_to_object: A -> object,
      fields: A ~> set<FieldValue>,
      reachable: FieldValue -> set<A>,
      all_a: set<A>) {
    ghost function AllObjects(): set<object> {
      set a <- all_a :: a_to_object(a)
    }
    ghost predicate closed()
       reads AllObjects()
       requires forall a: A <- all_a :: fields.requires(a) && fields.reads(a) == {}
    {
      forall a: A <- all_a :: forall f <- fields(a) :: reachable(f) <= all_a
    }
}

[MikaelMayer]

That works indeed, but I wanted closed() to be like a Valid() predicate, and I can't refactor your requires into another predicate, do you know why?

[keyboardDrummer]

I see, sorry I only now understand your intent, and now I also understand why it's surprising your program didn't verify to begin with. What's the reads clause of a reads function? I'm guessing you need to define it at some level in the requires clause. You can do:

// Encoding of Boogie references in Dafny
  datatype World<!A(==,!new), !FieldValue> = World(
      a_to_object: A -> object,
      fields: A ~> set<FieldValue>,
      reachable: FieldValue -> set<A>,
      all_a: set<A>) {
    ghost function AllObjects(): set<object> {
      set a <- all_a :: a_to_object(a)
    }
    ghost predicate closed()
       reads AllObjects()
       requires forall a: A <- all_a :: && fields.reads.requires(a) && fields.reads.reads(a) == {} 
    {
      forall a: A <- all_a ::
        && fields.reads(a) <= AllObjects()
        && fields.requires(a)
        && forall f <- fields(a) :: reachable(f) <= all_a
    }
}

I'm confused why moving things to the requires clause even works though. I would have thought that the WF check of the contract fails in the above case because it doesn't know anything about fields.reads.reads.reads. @RustanLeino could you comment?

[RustanLeino]

Summary

General functions (that is, ~> arrow types) are difficult to work with. I don't know of a good way to legally write the body of closed() as intended.

Details

Second example

Here is a shorter version of the second example from above:

ghost predicate Closed'<A>(f: A ~> int, a: A, S: set<object>)
  reads S
{
  && f.reads(a) <= S // precondition violation, and insufficient reads clause to invoke function
  && f.requires(a)
  && f(a) == 5
}

This function body is in error. To be allowed to even ask the question "what does f read when invoked on a?", you need to prove that the precondition of f on a holds. So, Closed' places its conjuncts in the wrong order.

First example

Here is a shorter version of the first example from above:

ghost predicate Closed<A>(f: A ~> int, a: A, S: set<object>)
  reads S
{
  && f.requires(a) // insufficient reads clause to invoke function
  && f.reads(a) <= S
  && f(a) == 5
}

By preceding f.reads(a) with the knowledge f.requires(a), as in the body of Closed, there's no complaint about r.reads(a). But there's a problem with calling f.requires(a) itself. Let's consider three cases:

• Suppose that f.requires(a) returns true -- in other words, f can be invoked on a -- and that f.reads(a) is contained in S. Then, everything will work out:
  • f.requires(a) has true as its precondition, f.reads(a) has f.requires(a) as its precondition and it has already been established (by the first conjunct), and f(a) also has f.requires(a) as its precondition and it has already been established.
  • The reads check for Closed happens "at the end of the function body. In the case we're considering, by the time we get to the end, we know that f.reads(a) <= S holds. This means that what is read by f.requires(a), f.reads(a), and f(a) are all contained within S, so the reads checking of the body of Closed works out.
• Suppose f.requires(a) holds but f.reads(a) <= S does not. Now, by the time we get to the } of the function body, we have already read too much. In particular, the expression f.requires(a) does not live up to the reads S of function Closed.
• Suppose f.requires(a) returns false. Now, by the time we reach the } and do the reads check, we know nothing about f.requires(a) read. As far as we know, it might have read the entire heap. So, function Closed violates its reads clause.

(The rules I applied here are described in section 5.12 Arrow types of the reference manual.)

Adding a precondition

We could add

  requires f.requires.reads(a) == {}

to function Closed. This ought to work, because this would say that the evaluations of f.requires(a) (and thus also the evaluation of f.reads(a)) does not look at the heap. However, this seems not to verify.

We could try to fix this. However, such a precondition would be hard for anyone to establish. A caller would need to prove that f.requires(a) holds in order to reason about f.requires.reads(a). So, then I think a function like Closed could just as well take f.requires(a) as a precondition.

(Section 5.12 Arrow types of the reference manual uses "reads if P(x) then R(x) else *" in its explanations. What I had not thought about before is that this * should not be interpreted as definitely reading the entire heap, but as possibly reading the entire heap. In other words, if P(x) does not hold, then this reads clause should equal some unknown set of objects. If this * definitely meant the entire heap, then the condition f.requires.reads(a) == {} would imply f.requires(a), which seems surprising. Then again, I am arguing that the only way to establish f.requires.reads(a) == {} is to first prove f.requires(a), so I suppose there's no real harm in interpreting the * as definitely meaning the entire heap.)

The difference between the specification and body

The examples above put f.requires(a) and f.reads(a) in the body of the function. By instead putting them in the specification of the function, the verification succeeds:

ghost predicate ClosedWithSpec<A>(f: A ~> int, a: A, S: set<object>)
  requires f.requires(a) && f.reads(a) <= S
  reads S
{
  f(a) == 5
}

ghost predicate ClosedWithSpec'<A>(f: A ~> int, a: A)
  requires f.requires(a)
  reads f.reads(a)
{
  f(a) == 5
}

The reason for this is that these preconditions will only ever be evaluated to true (because callers will be checked to live up to these preconditions). This means that the second and third cases in my list above do not occur.

[MikaelMayer]

requires f.requires.reads(a) == {}

is exactly something that I had envisioned before. It gives the ability of writing heap-reading functions that do not have preconditions (if the requires is true, then the reads is empty)
but unfortunately for now I think we have that f.requires.reads == f.reads or something like that, right @jtristan ?

So, then I think a function like Closed could just as well take f.requires(a) as a precondition.

Of course I'd love to add forall a: A :: f.requires(a) as a precondition to Closed. However, that would iterate over all allocated objects of the heap, which we can't do, so that's why we can't add this here.
In my case, I only provide functions that have "true" as requirement, so this ought to be verifiable no matter what I iterate on.