Verifying a function with a static array variable in VST

Question

I'd like to prove the correctness of this function from libsecp256k1:

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];
}

My specification is

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().

for my own custom implementation of ctz : Z -> nat.

However when I go to prove the associated correctness lemma:

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

I get an error:

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

My goal context is

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

Notably the debruijn array and its content are absent from the context. Am I supposed to be adding v_debruijn to my specification in some manner when a function has a local static variable like this?

Answer 1

Though it's defined locally, debruijn is treated as a global variable in the clightgen generated Coq file.

So it seems like modifying your specification in the following way should at least get you started:

Definition secp256k1_ctz64_var_debruijn_spec : ident * funspec :=
DECLARE _secp256k1_ctz64_var_debruijn
  WITH a : Z, gv : globals
  PRE [ tulong ]
    PROP(0 <= a < Int64.modulus)
    PARAMS(Vlong (Int64.repr a))
    GLOBALS(gv)
  SEP(data_at Ers (tarray tuchar 64) (map (fun x => Vint (Int.repr x)) debruijn) (gv _debruijn))
POST [ tint ]
  PROP()
  RETURN(Vint (Int.repr (Z.of_nat (ctz a))))
  SEP(data_at Ers (tarray tuchar 64) (map (fun x => Vint (Int.repr x)) debruijn) (gv _debruijn)).

where debruijn in the above definition is the appropriate list Z associated with your array.

Answer 2

Supplementary to TJ Machado's answer, the data for the debruijn array is stored in gvar_init v_debruijn in a somewhat unusual data structure specialized for static initialization. I haven't found a good canonical way to turn this into a suitable data_at expression, but I did manage to hack something together for my purposes:

Definition debruijn64_array (sh: share) (gv: globals) : mpred :=
  Eval cbn in
  let
    is_all_init_int8 := fix is_all_init_int8 (l : list init_data) :=
      match l with
      | [] => True
      | Init_int8 _ :: l' => is_all_init_int8 l'
      | _ => False
      end
  in let
    uninit_int8s := fix uninit_int8s (l: list init_data) : 
        is_all_init_int8 l -> list int :=
      match l with
      | [] => fun _ => []
      | x :: l' =>
        match x with
        | Init_int8 i => fun pf => i :: uninit_int8s l' pf
        | _ => False_rec (list int)
        end
      end
  in data_at sh (gvar_info v_debruijn)
    (map Vint (uninit_int8s (gvar_init v_debruijn) I)) (gv _debruijn).

My final specification is:

Definition secp256k1_ctz64_var_debruijn_spec : ident * funspec :=
DECLARE _secp256k1_ctz64_var_debruijn
  WITH a : Z, sh_debruijn : share, gv : globals
  PRE [ tulong ]
    PROP(0 <= a < Int64.modulus; readable_share sh_debruijn)
    PARAMS(Vlong (Int64.repr a))
    GLOBALS(gv)
    SEP(debruijn64_array sh_debruijn gv)
  POST [ tint ]
    PROP()
    RETURN(Vint (Int.repr (Z.of_nat (ctz a))))
    SEP(debruijn64_array sh_debruijn gv).