`FuncApp` in axioms

[pieter-bos]

I just spotted that regular function applications are supported now in domain axioms when they do not have preconditions, which is very nice! I read the commit that introduces it and it seems to me that there is nearly also an encoding for functions that do have (boolean) preconditions, but it is rejected by the parser. I have two questions about this:

1. Should decreases clauses count towards there being a precondition in this case?
2. Are there fundamental problems with allowing precondition-carrying functions in domain axioms (when they are not heap-dependent)?

Thanks!

[marcoeilers]

Regarding point 2, the issue is that that would require us to check domain axioms for well-definedness, which currently isn't necessary and thus doesn't happen at all. Alternatively, we could just assume that all axioms are well-defined, but that would open the door to a bunch of soundness issues. For example:

domain test {
  function f(Int): Int
  axiom {
    forall x: Int :: f(x) == g(x)
  }
}

function g(x: Int): Int
  requires x == 1
  ensures result == 1
{ x }

If we just accept the axiom, then I could use f(2) somewhere and immediately prove false.

So we'd either have to introduce well-formedness checks for axioms, or accept that people can shoot themselves in the foot like in this example. Both are possible of course, but we haven't discussed the options, mostly because so far there was no need to. Do you have a use case that would require this feature?

Regarding point 1), I guess decreases clauses shouldn't count. Currently they probably do? There might be an easy workaround for this; decreases clauses can be parsed both as pre- and as postconditions afaik, and we could just parse them as postconditions in case there are no preconditions at all. I'll look into that.

[pieter-bos]

A lot of our types are axiomatized in a domain, with plain functions added to require well-formedness conditions on accessor functions. (I use option as an easy example, but we also have types that are not easily phrased as an algebraic datatype). Typically we thus duplicate destructors in the domain and as plain functions, so we can encode well-formedness constraints on our own types. I think it would be helpful if they can just be the same term.

domain Opt[T] {
    function opt_none(): Opt[T]
    function some(t: T): Opt[T]

    function opt_get_ax(o: Opt[T]): T

    axiom { forall t: T :: {some(t)} some(t) != opt_none() }
    axiom { forall t: T :: {some(t)} opt_get_ax(some(t)) == t }
}

function opt_get(o: Opt[Int]): Int
requires o != opt_none()
ensures result == opt_get_ax(o)
{
    opt_get_ax(o)
}

So we'd either have to introduce well-formedness checks for axioms, or accept that people can shoot themselves in the foot ...

Ah I see, I had read Implies(tAxPres, tAx) instead of And(tAxPres, tAx), which is a bit more foot-gunny :)

[marcoeilers]

Functions that don't have preconditions but do have decreases-clauses can now be used in domain axioms (https://github.com/viperproject/silver/pull/802).