Proposed annotation: verified — heap-free function postconditions as domain axioms

[budney]

Motivation

If you want a function to appear in specs (preconditions, postconditions), it must be pure. But pure requires a single-expression body -- it can't have loops or multi-statement logic. If the implementation is more complex than a pure expression, your only option is to write a trusted pure stub in a .gobra file: a bodyless declaration whose postconditions you assert without proof. Gobra accepts it unconditionally. If the real function's behavior changes, nothing checks that the stub stays in sync; that invariant is entirely on the author to maintain.

Proposal

I propose to add a new keyword, verified, that gives an impure function unconditional, heap-free post-conditions, that can then be used in specifications without holding any permissions.

How it Works

A verified function or method is:

1. Verified by Gobra like any other function. Gobra proves that the pre- and post-conditions hold for the function.
2. Encoded as a Viper domain axiom. After verification, the postcondition is lifted into a Viper domain so it holds unconditionally for all arguments, independent of heap state.
3. Callable from any specification context. Because the axiom requires no heap, a verified function can appear in requires, preserves, ensures, ghost assignments, and as arguments to other verified calls.

Each verified function f with postcondition Q produces a standard Viper domain f_domain containing a standard Viper domain function f_spec(args): RetType and one axiom ∀ args :: pre(args) ⟹ f_spec(args) == Q(args) for each ensures and preserves clause.

Semantics

The following things can be verified (after this I'll say "function" for convenience, but always mean all of the following):

• Functions whose spec makes no references to the heap
• Methods whose spec makes no references to the heap, including pointer dereferences
• Interface method signatures -- Gobra automatically verifies all methods actually used as that type somewhere in the code being verified, which must be tagged as verified and have preconditions not stronger than, and postconditions not weaker than, the interface method declaration

A verified function can't be pure or trusted, because they have conflicting encoding strategies. It must have a body (except interface signatures), so there's something to verify. It must return at least one result, and have at least one ensures clause, so it yields at least one nontrivial axiom. It must have a decreases clause, because non-terminating functions can't yield axioms. Its spec clauses can't contain acc(), old(), *ptr, or recv.field where recv is a pointer, because axioms can't reference the heap. A verified function body can't contain assume or inhale, because that can lead to invalid proofs in Viper.

Call Tree Restrictions

The spec clauses of a verified function can call other functions that are verified or pure. All verified or pure functions called from the specs of f(), directly or via other verified or pure functions, must all have heap-free specs. This prevents the verified function from implicitly involving the heap in its specs. Note that trusted pure functions are relied on as axioms without checking that the implementation actually enforces those axioms, which is exactly what the verified keyword is being proposed to avoid. I would especially discourage it in specs.

Similarly, the call graph rooted at f(), including calls in both the specs and body, restricted to the connected component of f() containing only verified and pure functions, must be acyclic. This is necessary to prevent circular axioms and non-terminating proofs.

[ArquintL]

@budney thanks for opening this issue and I completely agree with you that the current Gobra version heavily restricts bodies of pure functions.

Do I understand your proposal correctly, that you're suggesting the following transformation:

requires stronglyPurePre(a)
ensures  stronglyPurePost(a, res)
verified
func impureFoo(a int) (res int) {
  // some complicated stmts
}

should be turned into:

requires stronglyPurePre(a)
ensures  stronglyPurePost(a, res)
func impureFoo(a int) (res int) {
  // some complicated stmts
}

ghost type impureFooDomain domain {
  func impureFooSpec(int) int

  axiom {
    forall a int :: { impureFooSpec(a) } stronglyPurePre(a) ==> stronglyPurePost(a, impureFooSpec(a))
  }
}

where strongly pure refers to the fact that the pre- and postconditions do not specify any permissions (neither for fields nor predicates)

However, impureFooSpec and impureFoo seem completely unrelated right now, so at least, one would have to assume as an additional postcondition of impureFoo that res == impureFooSpec(a) holds, right?

However, I see the following shortcomings:

• assuming that impureFoo behaves like a pure (domain) function introduces the assumption that impureFoo is deterministic and terminates, which might not be the case if it, e.g., contains non-determinism or a non-terminating loop.
• it seems very specialized to functions that do not access the heap, so I'm wondering how much value such a transformation provides in practice as I guess many functions would not meet the requirements.
• even if impureFoo's specification does not specify any permissions, we can a priori not rule out that its body does not access the heap. The easiest case being a memory allocation whose permissions are leaked and, thus, do not show up in the postcondition. I would have to think more about this case, but the fact that impureFoo's behavior could depend on the heap (despite the requirements for its specification) would at least constitute another source of potential non-determinism.

[budney]

You're right: so far there's nothing preventing the spec function from satisfying impureFoo_spec(a) == -impureFoo(a). We need at least:

requires stronglyPurePre(a)
ensures  stronglyPurePost(a, res)
verified
decreases _
func impureFoo(a int) (res int) {
  // some complicated stmts
}

to transform into

method impureFoo(a: Int) returns (res: Int)
  requires stronglyPurePre(a)
  ensures stronglyPurePost(a, res)
  ensures res == impureFoo_spec(a)
{
  // some complicated stmts
}

domain impureFoo_domain {
  function impureFoo_spec(a: Int): Int
  axiom forall a ::
    stronglyPurePre(a) ==> stronglyPurePost(a, impureFoo_spec(a))
}

* Note that a verified keyword without a decreases clause is an error. Functions can only be verified if they do terminate.

So we definitely need to add ensures res == impureFoo_spec(a) as a postcondition.

My intent is to model the function as externally pure, not necessarily allocation-free. It may allocate and mutate local heap internally, as long as it does not depend on or expose external heap state.

An example that comes to mind is a verified func that accepts an array of tokens, creates a parse tree from it, and then returns a bool indicating whether the parse was successful or not. I.e., a syntax check.

Your last point is a bit of a stumper. There are very tight restrictions on pure functions that make it hard (hopefully impossible) for a pure function to indirectly access the heap. Here I'm looking for a weaker condition: that neither it, nor anything in its call chain, reference the heap except heap allocated by the func.

I'm thinking about another, unfortunately similarly complex, proposal: a keyword like isolated, which would be required for verified functions. An isolated func can access heap it was explicitly given as an argument, heap it allocates, and heap returned by callees that satisfies the same invariant, but can neither read nor write globals, closure variables, or heap reachable through non-owned external variables. This requirement would be transitively required: only isolated callees are allowed.

[budney]

The background of this idea is that I can't express something like an idempotency requirement without writing a pure ghost function in a .gobra file. So:

package test

// @ ensures x >= 0 ==> ret == x
// @ ensures x <  0 ==> ret == -x
// @ ensures myAbs(myAbs(x)) == myAbs(x)
// @ decreases
func myAbs(x int) (ret int) {
	if x > 0 {
		return x
	} else {
		return -x
	}
}

This fails to validate because myAbs() isn't pure, but myAbs() can't be pure because it's not a single expression. One solution is to write a ghost func that I can use in the spec, and give it the postcondition that makes it idempotent. I'd be claiming is the same function as myAbs(), but can't make Gobra prove that they're equal, because of the same problem as above: myAbs() isn't spec-callable.

I don't want to have to maintain two versions of my function--if I can even write an equivalent pure function--and I don't even want to write .gobra files unless absolutely necessary. So I looked for a way to make a function spec-callable, without the stringent requirements imposed on pure functions, and verified is what I came up with.

[budney]

@ArquintL, what are your thoughts on all this?

[jcp19]

Hi @budney! Thanks for bringing this topic back up, pure functions are definitely a source of toil that we should address. I don't think the proposed transformation described above would work though, as we are assuming the contract of a function at the same time we verify it. Defining stronglyPurePre(x) as true and stronglyPurePost(x, y) as false above leads to a program that verifies even though this is not intended. This shows that supporting such a feature would not be trivial, and that we would need to verify the method before introducing the domain with the specification. This is not easy to do given the current architecture of Gobra, which expects one complete Viper program to be generated per Go package.

I think a much cleaner solution to this problem is to actually allow statements in the bodies of pure functions, as long as they are compiled into Viper functions. We had a project on this (https://ethz.ch/content/dam/ethz/special-interest/infk/chair-program-method/pm/documents/Education/Theses/Timon_Stampfli_BA_description.pdf), but we never got around merging the results.

[budney]

Hi @jcp19! Thanks for your reply! And thanks for linking that paper--it was very helpful, and more rigorous than the bottom-up approach I've been taking so far. I think you're right on all three counts:

1. This "verified" feature is "pure" in spirit. It treats functions as if they were pure, as long as they satisfy a particular definition of "side-effect free." Namely that the function must not reference globals, closure variables, etc., and (if we get fancy) must not to access heap or use channels except "internally," for some careful definition of "internal." Currently pure functions are restricted even more than that, so this would be an extension of the feature.
2. Currently there's at least some risk that the spec for a verified function might be injected as an axiom, even if the function itself fails verification. The code I have so far generates both the proof obligation and the domain axiom, but it doesn't directly enforce that the axiom be contingent on the proof of the function body.
3. Getting this right is definitely complicated and a lot of work. The branch I'm working in touches a lot of code.

The paper captures something I failed to. Determinism is necessary for the function to even be well-defined in the mathematical sense, and it's not explicitly included in my design. It needs to be added. And of course making the axiom contingent on the verification of the body.

My work so far does side-step an issue identified as thorny in the paper. The recursion problem identified in the paper is avoided by forbidding recursion outright. The ban extends to any cycles in the call graph involving pure or verified functions, which prevents sneaky "recursion" by multiple functions. (That could be weakened by, for example, verifying tail-recursion by generating the iteration and verifying that, but I left that whole bees' nest alone.)

Making axioms contingent on verification entails that interface methods must have at least one successfully verified witness implementation for the spec domain to be created; interface methods with no implementation are ignored. Every implementation called via the interface is already verified separately.

* Note that there's an existing bug in Gobra related to that last requirement: you can put //@ ensures false before any interface method, and if there are no implementations then no error will be raised--but other functions can invoke the interface method and inject true == false at the call site. We already need something that rejects calls to interface methods that don't have at least one successfully verified implementation.

[jcp19]

• Note that there's an existing bug in Gobra related to that last requirement: you can put //@ ensures false before any interface method, and if there are no implementations then no error will be raised--but other functions can invoke the interface method and inject true == false at the call site. We already need something that rejects calls to interface methods that don't have at least one successfully verified implementation.

I don't think that is a problem. In order for the code that calls such an interface method to be reachable, you will have to costruct a value of a concrete type that implements that interface somewhere in the execution in order to have a receiver for the method call (the nil value of an interface type is not a valid receiver). As such, if no concrete implementation exists for the interface, you will not be able to reach that code path.

[budney]

If the implementations all live in a different package, then no proof obligations are ever generated, and bad code verifies successfully because true == false is smuggled in via the interface function's spec.

Here's a fairly minimal reproduction: test_case.tgz

[budney]

If the implementations all live in a different package, then no proof obligations are ever generated, and bad code verifies successfully because true == false is smuggled in via the interface function's spec.

Here's a fairly minimal reproduction: test_case.tgz

I should clarify that proof obligations are generated when the type checker resolves a (ConcreteType, InterfaceType) pair, but in the attached code that doesn't happen because verification stays at the package level and trusts what's on the other side of the package boundary.

You can force Gobra to catch the error by adding var _ impl.Doer = impl.Agent{} to main.go.