在VST中验证含静态数组的secp256k1函数时遇到的问题

我想用VST验证libsecp256k1库中secp256k1_ctz64_var_debruijn函数的正确性，该函数包含一个局部静态常量数组debruijn。我已经写好对应的规格说明和证明代码，但执行forward策略时出现「无法计算右侧表达式」的错误，且上下文里缺少debruijn数组及其内容。请问是否需要在规格中添加v_debruijn来处理这类局部静态变量？

相关代码 #

C函数代码 #

static int secp256k1_ctz64_var_debruijn(uint64_t x) {
    static const uint8_t debruijn[64] = {
        0, 1, 2, 53, 3, 7, 54, 27, 4, 38, 41, 8, 34, 55, 48, 28,
        62, 5, 39, 46, 44, 42, 22, 9, 24, 35, 59, 56, 49, 18, 29, 11,
        63, 52, 6, 26, 37, 40, 33, 47, 61, 45, 43, 21, 23, 58, 17, 10,
        51, 25, 36, 32, 60, 20, 57, 16, 50, 31, 19, 15, 30, 14, 13, 12
    };
    return debruijn[((x & -x) * 0x022FDD63CC95386D) >> 58];
}

规格说明代码 #

Definition secp256k1_ctz64_var_debruijn_spec : ident * funspec :=
DECLARE _secp256k1_ctz64_var_debruijn
  WITH a : Z
  PRE [ tulong ]
    PROP(0 <= a < Int64.modulus)
    PARAMS(Vlong (Int64.repr a))
  SEP()
POST [ tint ]
  PROP()
  RETURN(Vint (Int.repr (Z.of_nat (ctz a))))
  SEP().

证明代码 #

Lemma body_secp256k1_umul128: semax_body Vprog Gprog f_secp256k1_ctz64_var_debruijn secp256k1_ctz64_var_debruijn_spec.
Proof.
start_function.
forward.

错误信息 #

Tactic failure: Cannot evaluate right-hand-side expression (sometimes this is caused by missing LOCALs in your precondition) (level 995).

目标上下文 #

1 goal
Espec : OracleKind
a : Z
Delta_specs : Maps.PTree.t funspec
Delta := abbreviate : tycontext
H : and (Z.le 0 a) (Z.lt a Int64.modulus)
POSTCONDITION := abbreviate : ret_assert
MORE_COMMANDS := abbreviate : statement
______________________________________(1/1)
semax Delta
  (PROPx nil
     (LOCALx (cons (temp _x (Vlong (Int64.repr a))) nil) (SEPx nil)))
  (Ssequence
     (Sset _t'1
        (Ederef
           (Ebinop Oadd (Evar _debruijn (tarray tuchar 64))
              (Ebinop Oshr
                 (Ebinop Omul
                    (Ebinop Oand (Etempvar _x tulong)
                       (Eunop Oneg (Etempvar _x tulong) tulong) tulong)
                    (Econst_long (Int64.repr 157587932685088877) tlong)
                    tulong) (Econst_int (Int.repr 58) tint) tulong)
              (tptr tuchar)) tuchar)) MORE_COMMANDS) POSTCONDITION

解答 #

是的，你需要在规格的前置条件中声明这个静态数组的存在及其内容，因为VST需要明确静态变量的状态才能正确分析代码。

具体操作步骤如下：

1. 定义数组的Coq表示
   先把C中的debruijn数组转换成Coq可识别的常量列表：

   Definition debruijn_array : list byte :=
     [|0;1;2;53;3;7;54;27;4;38;41;8;34;55;48;28;
       62;5;39;46;44;42;22;9;24;35;59;56;49;18;29;11;
       63;52;6;26;37;40;33;47;61;45;43;21;23;58;17;10;
       51;25;36;32;60;20;57;16;50;31;19;15;30;14;13;12|].
   

2. 修改函数规格
   在PRE的LOCAL部分添加静态变量_debruijn的声明，用varray描述其类型和内容：

   Definition secp256k1_ctz64_var_debruijn_spec : ident * funspec :=
   DECLARE _secp256k1_ctz64_var_debruijn
     WITH a : Z
     PRE [ tulong ]
       PROP(0 <= a < Int64.modulus)
       PARAMS(Vlong (Int64.repr a))
       LOCAL(temp _x (Vlong (Int64.repr a));
             temp _debruijn (varray tuchar debruijn_array))
     SEP()
   POST [ tint ]
     PROP()
     RETURN(Vint (Int.repr (Z.of_nat (ctz a))))
     SEP().
   

3. 调整证明流程
   修改规格后，再执行start_function和forward策略，VST就能识别到_debruijn数组的状态，正确处理数组访问操作。

原因在于：局部静态变量属于函数执行环境的一部分，程序启动时就完成初始化。VST的forward策略需要明确知道这些变量的类型和内容，才能解析涉及它们的表达式。如果前置条件中没有声明，VST无法识别_debruijn的引用，就会抛出「无法计算右侧表达式」的错误。

内容的提问来源于stack exchange，提问作者Russell O'Connor