带本地变量的forward_call

Question

VST版本1.7。

我有一个问题，当我尝试在函数调用中使用它们时，coq将无法识别本地声明的变量。我的代码：

void deSignArray(int bits[], int invKey, int size) 
{ 
int i = 0; 
while (i < size) { 
int bit = bits[i]; 
int ans = deSignInt(bit, invKey); 
bits[i] = ans; 
i++; 
} 
} 

与COQ类型位：列表Z，invKey：Z，尺寸：Z.

我通过位成功阶梯=位[I]的步骤，但是，当我然后重使用步骤

forward_call((Int.repr bit), (Int.repr invKey)). 

该步骤失败，未在环境中找到位。我尝试使用

forward_call(_bit, (Int.repr invKey)). 

作为_bit出现LOCAL子句中，但它提供了打字错配，因为_bit是IDENT类型，而不是int或Z型。我想知道我应该如何使用我的本地定义的值来调用其他函数作为结果，任何帮助将不胜感激。

Answer 1

在您的情况下（Int.repr位，Int.repr invKey），您提供给forward_call的参数必须是Coq值。在你的情况下，如果（在forward_call的时候）你的Coq证明目标中有线，变量“bit”和“invKey”，那么这应该起作用。

你会如何得到这种线上的变量？如果函数precondition的LOCALS部分包含（temp _invKey（Vint（Int.repr invkey））），那么您应该在该行上方有invKey。然后，在通过加载语句（bit = bits [i]）前往转发之后，您当前的验证目标的前提条件应该有一个形式的LOCALS（temp _bit something-or-other），并且这就是说，其他你应该使用，而不是“位”。