coq - 如何通过示例证明来自 ACSL 的 remove_copy

Question

我试图证明该算法从“ACSL by Example”版本 11.1.0 中删除副本(第一个版本)。

我使用了 Alt-Ergo (0.99.1)、CVC3 (2.4.1)、Z3 (4.3.2)、CVC4 (1.4) 和 Why3 (0.85) why3 的​​时间限制是 50 秒并开始 frama- c、我使用了命令:

frama-c-gui -wp -wp-model Typed+ref -wp-rte -wp-split remove_copy_11.c

Only one proof obligation was not solved (timeout).

Its body is:

Goal Preservation of Invariant 'kept' (file remove_copy_11.c, line 73) (1/2):
Tags: Then Then.
Let x_0 = (L_Count Mint_2 a_0 i_1 v_0).
Let x_1 = -x_0.
Let x_2 = i_1-x_0.
Let a_1 = (shift_sint32 b_0 x_2).
Let a_2 = (shift_sint32 a_0 i_1).
Let x_3 = Mint_2[a_2].
Let x_4 = 1+i_1.
Let x_5 = 1+i_1-x_0.
Let a_3 = (shift_sint32 b_0 0).
Let a_4 = (shift_sint32 a_0 0).
Assume {
  Type: (is_sint32 v_0) /\ (is_uint32 i_1) /\ (is_uint32 n_0)
        /\ (is_uint32 x_4) /\ (is_sint32 x_3) /\ (is_uint32 x_2)
        /\ (is_uint32 x_5).
  Have: (linked Malloc_0) /\ ((region (base a_0))<=0)
        /\ ((region (base b_0))<=0).
  Have: (valid_rd Malloc_0 a_4 n_0).
  Have: (valid_rw Malloc_0 a_3 n_0).
  Have: (separated a_4 n_0 a_3 n_0).
  Have: (havoc Mint_1 Mint_2 a_3 n_0).
  Have: (P_Unchanged Mint_1 Mint_2 b_0 x_2 n_0).
  Have: (P_PreserveCount Mint_2 a_0 i_1 b_0 x_2 v_0).
  Have: not (P_HasValue Mint_2 b_0 x_2 v_0).
  Have: (i_1<=n_0) /\ (0<=x_0) /\ (x_0<=i_1).
  Have: i_1<n_0.
  Have: (P_EqualRanges_2_ Mint_1 Mint_2 a_0 n_0).
  Have: (valid_rd Malloc_0 a_2 1).
  Have: v_0!=x_3.
  Have: i_1<=(4294967294+x_0).
  Have: (valid_rw Malloc_0 a_1 1).
  Have: i_1<=4294967294.
}
Prove: (P_PreserveCount Mint_2[a_1->x_3] a_0 x_4 b_0 x_5 v_0).
e

由于文档表明该算法的两个证明是使用 Coq 验证的，我猜这是其中之一。我是 Coq 的新手，所以我的问题是，如果是这样的话，如何用 Coq 证明这种证明义务。

Answer 1

这个问题已经有点老了，但我希望这个答案仍然有用。

在 Frama-C 中，您可以选择一个目标并将其转换为 Coq 可以理解的格式。

你应该得到这样的东西:

(* ---------------------------------------------------------- *)
(* --- Preservation of Invariant 'kept' (file remove_copy.c, line 95) (1/2) --- *)
(* ---------------------------------------------------------- *)
Require Import ZArith.
Require Import Reals.
Require Import BuiltIn.
Require Import bool.Bool.
Require Import int.Int.
Require Import int.Abs.
Require Import int.ComputerDivision.
Require Import real.Real.
Require Import real.RealInfix.
Require Import real.FromInt.
Require Import map.Map.
Require Import Qedlib.
Require Import Qed.
Require Import Memory.
Require Import Cint.

Require Import Compound.
Require Import Axiomatic.
Require Import A_CountAxiomatic.
Require Import Axiomatic1.

Goal
  forall (i_2 i_1 i : Z),
  forall (t : array Z),
  forall (t_2 t_1 : farray addr Z),
  forall (a_1 a : addr),
  let a_2 := (shift_sint32 a_1 i%Z) in
  let x := (t_1.[ a_2 ])%Z in
  let x_1 := (1%Z + i%Z)%Z in
  let x_2 := ((L_Count t_1 a_1 i%Z i_1%Z))%Z in
  let a_3 := (shift_sint32 a_1 0%Z) in
  let a_4 := (shift_sint32 a 0%Z) in
  let x_3 := (-x_2)%Z in
  let x_4 := (i%Z - x_2)%Z in
  let x_5 := (1%Z + i%Z - x_2)%Z in
  let a_5 := (shift_sint32 a x_4) in
  ((i < i_2)%Z) ->
  ((i <= 4294967294)%Z) ->
  ((i <= i_2)%Z) ->
  ((linked t)) ->
  ((is_sint32 i_1%Z)) ->
  ((is_uint32 i%Z)) ->
  ((is_uint32 i_2%Z)) ->
  ((i_1 <> x)%Z)%Z ->
  ((((region ((base a))%Z)) <= 0)%Z) ->
  ((((region ((base a_1))%Z)) <= 0)%Z) ->
  ((is_uint32 x_1)) ->
  ((P_EqualRanges t_2 t_1 a_1 i_2%Z)) ->
  ((0 <= x_2)%Z) ->
  ((x_2 <= i)%Z) ->
  ((is_sint32 x)) ->
  ((valid_rd t a_3 i_2%Z)) ->
  ((valid_rd t a_2 1%Z)) ->
  ((valid_rw t a_4 i_2%Z)) ->
  ((separated a_3 i_2%Z a_4 i_2%Z)) ->
  ((havoc t_2 t_1 a_4 i_2%Z)) ->
  ((i <= (4294967294 + x_2))%Z) ->
  ((is_uint32 x_4)) ->
  ((is_uint32 x_5)) ->
  ((P_Unchanged t_2 t_1 a x_4 i_2%Z)) ->
  (~((P_HasValue t_1 a x_4 i_1%Z))) ->
  ((valid_rw t a_5 1%Z)) ->
  ((P_PreserveCount t_1 a_1 i%Z a x_4 i_1%Z)) ->
  ((P_PreserveCount (t_1.[ a_5 <- x ]) a_1 x_1 a x_5 i_1%Z)).

这里有三个难点:

• 翻译重命名了所有变量，因此 Coq 版本比 Frama-C 版本更难理解，您经常需要比较假设才能理解 Coq 中的变量代表什么
• 很多假设是自动添加的，对证明这个特定目标毫无用处
• 你一定对 Coq 对内存的表示有点熟悉 (shift_sint32, separated, havoc, ...)

这是一个有效的证明，但我不知道它是否是一个好的证明。我试图在评论中解释主要思想。

Proof.
  (* Some preliminary steps in order to clean the hypotheses and the goal *)
  intros.
  clear H0 H1 H2 H3 H4 H5 H7 H8 H9 H10 H13 H14 H15 H16 H18 H19 H20 H21 H22
    H23 H24 t_2 x_3.
  assert(a_4=a) as Ha1.
  { unfold a_4. unfold shift_sint32. unfold shift.
    replace (offset a + 0) with (offset a) by omega.
    destruct a; reflexivity.
  }
  assert(a_3=a_1) as Ha2.
  { unfold a_3. unfold shift_sint32. unfold shift.
    replace (offset a_1 + 0) with (offset a_1) by omega.
    destruct a_1; reflexivity.
  }
  rewrite Ha1, Ha2 in *. clear dependent a_3. clear dependent a_4.
  unfold x_1, x_5. replace (1+i-x_2) with (1+(i-x_2)) by omega.
  remember (i-x_2) as j.
  unfold x_4 in *.

  (* Here we see what the goal of this proof really means: we have
     the property P_PreserveCount for the indices i and j (hypothesis H25),
     and we want to prove that it is preserved after one iteration
     of the loop for the indices (i+1) and (j+1). *)

  (* The idea is to prove the following intermediary result:
     after the iteration, P_PreserveCount holds for i and j.
     This is actually trivial, since the arrays a and b (named here a_1 and a)
     are not modified until i and j. *)
  assert (P_PreserveCount (t_1 .[ a_5 <- x]) a_1 i a j i_1) as Ha.
  { unfold P_PreserveCount; intros.
    rewrite 2!Q_CountRead with (t:=t_1 .[a_5 <- x]) (t_1:=t_1); try assumption.
    apply H25; try assumption.
    - unfold P_EqualRanges. intros.
      rewrite access_update_neq. reflexivity.
      unfold a_5, shift_sint32, shift.
      injection; intros. omega.
    - unfold P_EqualRanges. intros.
      rewrite access_update_neq. reflexivity.
      unfold a_5, shift_sint32, shift.
      apply separated_1 with (a:=i_2) (b:=i_2).
      apply separated_sym. assumption. omega. omega.
  }

  (* a[i] and b[j] are equal (to x) *)
  assert((t_1 .[ a_5 <- x]) .[ shift_sint32 a j] = x) as Ha1.
  { apply access_update. }
  assert((t_1 .[ a_5 <- x]) .[ shift_sint32 a_1 i] = x) as Ha2.
  { rewrite access_update_neq. reflexivity.
    unfold a_5, shift_sint32, shift.
    apply separated_1 with (a:=i_2) (b:=i_2).
    apply separated_sym. assumption. omega. omega.
  }

  (* here, we know that P_PreserveCount holds for the indices i and j,
     and that a[i]=b[j], so the conclusion is easy. We just have to distinguish
     the different cases *)
  unfold P_PreserveCount; intros.
  destruct(why_decidable_eq i0 x).
  - subst i0.
    rewrite 2!Q_CountOneHit; try assumption.
    rewrite Ha by assumption. reflexivity.
    rewrite Ha1; reflexivity. rewrite Ha2; reflexivity. 
  - rewrite <- 2!Q_CountOneMiss; try assumption.
    apply Ha; assumption.
    rewrite Ha1. assumption. rewrite Ha2. omega.
Qed.

总而言之，在 Coq 中进行证明的一个优势是了解 SMT 求解器缺乏什么来自动得出结论。经过几次尝试，我发现将循环替换为:

for (size_type i = 0; i < n; ++i)
{
  //@ assert EqualRanges{Here,Pre}(a, n);
  L:if (a[i] != v)
  {
    b[j++] = a[i];
  }
  //@ assert EqualRanges{Here,L}(a, i);
  //@ assert EqualRanges{Here,L}(b, \at(j, L));
  //@ assert PreserveCount(a, i, b, \at(j, L), v);
}

允许 why3 的​​证明者解决所有问题。