How to declare an abstract function in Inox

Question

I'm proving certain properties on elliptic curves and for that I rely on some functions that deal with field operations. However, I don't want Inox to reason about the implementation of these functions but to just assume certain properties on them.

Say for instance I'm proving that the addition of points p1 = (x1,y1) and p2 = (x2,y2) is commutative. For implementing the addition of points I need a function that implements addition over its components (i.e. the elements of a field).

The addition will have the following shape:

val addFunction = mkFunDef(addID)() { case Seq() => 
    val args: Seq[ValDef] = Seq("f1" :: F, "f2" :: F)  
    val retType: Type = F
    val body: Seq[Variable] => Expr = { case Seq(f1,f2) =>
      //do the addition for this field
    } 
    (args, retType, body)
}

For this function I can state properties such as:

val addAssociative: Expr = forall("x" :: F, "y" :: F, "z" :: F){ case (x, y, z) => 
    (x ^+ (y ^+ z)) === ((x ^+ y) ^+ z)
}

where ^+ is just the infix operator corresponding to add as presented in this other question.

What is a proper expression to insert in the body so that Inox does not assume anything on it while unrolling?

score 1 · Accepted Answer · answered Apr 16 '17 at 15:38

There are two ways you can go about this:

Use a choose statement in the body of addFunction:
```
val body: Seq[Variable] => Expr = {
  choose("r" :: F)(_ => E(true))
}
```
During unrolling, Inox will simply replace the choose with a fresh variables and assume the specified predicate (in this case true) on this variable.
Use a first-class function. Instead of using add as a named function, use a function-typed variables:
```
val add: Expr = Variable(FreshIdentifier("add"), (F, F) =>: F)
```
You can then specify your associativity property on add and prove the relevant theorems.

In your case, it's probably better to go with the second option. The issue with proving things about an addFunction with a choose body is that you can't substitute add with some other function in the theorems you've shown about it. However, since the second option only shows things about a free variable, you can then instantiate your theorems with concrete function implementations.

Your theorem would then look something like:

val thm = forallI("add" :: ((F,F) =>: F)) { add =>
  implI(isAssociative(add)) { isAssoc => someProperty }
}

and you can instantiate it through

val isAssocAdd: Theorem = ... /* prove associativity of concreteAdd */
val somePropertyForAdd = implE(
  forallE(thm)(\("x" :: F, "y" :: F)((x,y) => E(concreteAdd)()(x, y))), 
  isAssocAdd
)

How to declare an abstract function in Inox

1 Answers1