Как на примере доказать remove_copy из ACSL

Этот вопрос уже устарел, но я надеюсь, что этот ответ все же будет полезен.

В 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);
}

позволяет доказывающим почему3 решить все.