如何在 Inox 中声明抽象函数

Question

我正在证明椭圆曲线的某些性质，为此我依赖于一些处理场操作的函数。但是，我不希望 Inox 对这些函数的实现进行推理，而只是假设它们具有某些属性。

比如说我要证明点的加法 p1 = (x1,y1) and p2 = (x2,y2) 是可交换的。为了实现点的加法，我需要一个函数来实现对其组件（即字段的元素）的加法。

添加将具有以下形状：

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)
}

对于这个函数，我可以声明如下属性：

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

其中 ^+ 只是对应于其他问题中出现的 add 的中缀运算符。

插入 body 的正确表达式是什么，以便 Inox 在展开时不承担任何责任？

Answer 1

您可以通过两种方式解决此问题：

在 addFunction:
的正文中使用 choose 语句
```
val body: Seq[Variable] => Expr = {
  choose("r" :: F)(_ => E(true))
}
```
在展开过程中，Inox 将简单地用新的替换 choose 变量并假定指定的谓词（在本例中为 true）这个变量。
使用第一个-class函数。而不是使用 add 作为命名函数，使用函数类型变量：
```
val add: Expr = Variable(FreshIdentifier("add"), (F, F) =>: F)
```
然后您可以在 add 上指定结合律属性并证明相关定理.

在您的情况下，选择第二个选项可能更好。用 choose body 证明 addFunction 的问题是你不能用你展示的定理中的其他函数替换 add 。但是，由于第二个选项仅显示有关自由变量的信息，因此您可以使用具体的函数实现来实例化您的定理。

你的定理将类似于：

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

并且可以通过

实例化

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

如何在 Inox 中声明抽象函数

How to declare an abstract function in Inox

leon