coq - How to prove remove_copy from ACSL by example -

i tried prove algorithm remove copy (the first version) "acsl example" version 11.1.0.

i used alt-ergo (0.99.1), cvc3 (2.4.1), z3 (4.3.2), cvc4 (1.4) , why3 (0.85) time limit in why3 50 sec , start frama-c, used command:

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

only 1 proof obligation not solved (timeout).

its body is:

goal preservation of invariant 'kept' (file remove_copy_11.c, line 73) (1/2): tags: 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 

since document indicates 2 proofs of algorithm validated using coq, guess 1 of them. i'm beginner coq, question is, how proof obligation proved coq, if case.

this question bit old, hope answer still useful.

from frama-c, can select goal , convert in format coq understands.

you should this:

(* ---------------------------------------------------------- *) (* --- 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 : z),   forall (t : array z),   forall (t_2 t_1 : farray addr z),   forall (a_1 : 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 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 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 x_4 i_2%z)) ->   (~((p_hasvalue t_1 x_4 i_1%z))) ->   ((valid_rw t a_5 1%z)) ->   ((p_preservecount t_1 a_1 i%z x_4 i_1%z)) ->   ((p_preservecount (t_1.[ a_5 <- x ]) a_1 x_1 x_5 i_1%z)). 

there 3 difficulties here:

• the translation renames variables, therefore coq version more difficult understand frama-c one, , have compare hypotheses understand variable in coq represents
• a lot of hypotheses added automatically , useless prove particular goal
• you must bit familiar representation of memory coq (shift_sint32, separated, havoc, ...)

here proof works, have no idea if proof. tried explain main ideas in comments.

proof.   (* preliminary steps in order clean hypotheses , 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) ha1.   { unfold a_4. unfold shift_sint32. unfold shift.     replace (offset + 0) (offset a) omega.     destruct a; reflexivity.   }   assert(a_3=a_1) ha2.   { unfold a_3. unfold shift_sint32. unfold shift.     replace (offset a_1 + 0) (offset a_1) 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) (1+(i-x_2)) omega.   remember (i-x_2) j.   unfold x_4 in *.    (* here see goal of proof means: have      property p_preservecount indices , j (hypothesis h25),      , want prove preserved after 1 iteration      of loop indices (i+1) , (j+1). *)    (* idea prove following intermediary result:      after iteration, p_preservecount holds , j.      trivial, since arrays , b (named here a_1 , a)      not modified until , j. *)   assert (p_preservecount (t_1 .[ a_5 <- x]) a_1 j i_1) ha.   { unfold p_preservecount; intros.     rewrite 2!q_countread (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 (a:=i_2) (b:=i_2).       apply separated_sym. assumption. omega. omega.   }    (* a[i] , b[j] equal (to x) *)   assert((t_1 .[ a_5 <- x]) .[ shift_sint32 j] = x) ha1.   { apply access_update. }   assert((t_1 .[ a_5 <- x]) .[ shift_sint32 a_1 i] = x) ha2.   { rewrite access_update_neq. reflexivity.     unfold a_5, shift_sint32, shift.     apply separated_1 (a:=i_2) (b:=i_2).     apply separated_sym. assumption. omega. omega.   }    (* here, know p_preservecount holds indices , j,      , a[i]=b[j], conclusion easy. have distinguish      different cases *)   unfold p_preservecount; intros.   destruct(why_decidable_eq i0 x).   - subst i0.     rewrite 2!q_countonehit; try assumption.     rewrite ha assumption. reflexivity.     rewrite ha1; reflexivity. rewrite ha2; reflexivity.    - rewrite <- 2!q_countonemiss; try assumption.     apply ha; assumption.     rewrite ha1. assumption. rewrite ha2. omega. qed. 

to conclude, advantage of doing proof in coq understanding smt solvers lack conclude automatically. after several tries, found replacing loop by:

for (size_type = 0; < 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); } 

allows provers of why3 solve everything.