verifiable-c - 证明一个 int 等于一个字符数组

Question

我正在使用 VST v1.7。

有没有人证明一个 int 等于一个字符数组？沿着这些思路：

Definition int2uchars (i : int) : list Z :=
  [
    Int.unsigned (Int.and (Int.shru i (Int.repr 24)) (Int.repr 255));
    Int.unsigned (Int.and (Int.shru i (Int.repr 16)) (Int.repr 255));
    Int.unsigned (Int.and (Int.shru i (Int.repr 8))  (Int.repr 255));
    Int.unsigned (Int.and (Int.shru i (Int.repr 0))  (Int.repr 255))
  ].

Lemma int2chararray :
  forall (i : int) (v : val),
    field_at Tsh tuint [] (Vint i) v
    = data_block Tsh (int2uchars i) v.

除了打破field_at抽象来证明这一点之外，还有其他解决方案吗？