0

我正在证明椭圆曲线上的某些属性，为此我依赖于一些处理现场操作的函数。但是，我不希望 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)
}

where^+只是与 add 相对应的中缀运算符，如另一个问题中所示。

插入正文中的正确表达式是什么，以便 Inox 在展开时不会在其上假设任何内容？

4

1 回答 1

1

有两种方法可以解决这个问题：

  1. 在 的正文中使用选择语句addFunction：

    val body: Seq[Variable] => Expr = {
  choose("r" :: F)(_ => E(true))
}

    在展开期间，Inox 将简单地将 替换choose为新变量，并假定此变量上的指定谓词（在本例中为true）。

  2. 使用一流的功能。不要使用add命名函数，而是使用函数类型变量：

    val add: Expr = Variable(FreshIdentifier("add"), (F, F) =>: F)

    然后，您可以指定您的关联性属性add并证明相关定理。

在您的情况下，使用第二个选项可能会更好。用选择体证明 an 的问题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
)
于 2017-04-16T15:38:08.597 回答