NB: This Coq documentation contains a revised version of the Coq implementation of these papers [1], [2], [3], [4], and is also the support for ongoing research. A partial archive (14/01/2001) is available at here. Drop us a line if you are interested in a complete, up-to-date archive.

Library C_examples

Require Import ssreflect ssrbool eqtype.
Require Import Bool_ext ZArith_ext Lists_ext String_ext.
Require Import machine_int.
Import MachineInt.
Require Import C_types C_expr C_bipl C_cmd C_seplog.

Local Open Scope minC_expr_scope.
Local Open Scope minC_cmd_scope.

Module example_m.

Definition fields_typs := (("a", btyp uint32) :: ("b", btyp uint32) :: nil)%string.
Definition pair_ab : typ := styp (mkStag "pair") fields_typs.

Definition fields_values := bval32 one32 :: bval32 four32 :: nil.
Definition pair_ab_14 : value := sval fields_values.

Lemma nil_is_map : map_ctxt nil.
Lemma nil_is_wft : wft_ctxt nil.

Eval compute in ( [ cst32_0 \+e cst32_0 ]_(Build_store nil nil_is_map nil_is_wft empty_tstore) ).

Definition var_expr := (var_e "apair")%string.

Eval compute in ( [ var_expr ]_(Build_store
  nil nil_is_map nil_is_wft (("apair", (pair_ab_14, pair_ab))::nil)%string)).
Eval compute in ( [ var_e "apair" .\ "a" ]_ (Build_store
  nil nil_is_map nil_is_wft (("apair", (pair_ab_14, pair_ab)) :: nil)))%string.
Eval compute in ( [ var_e "apair" .\ "b" ]_ (Build_store
  nil nil_is_map nil_is_wft (("apair", (pair_ab_14, pair_ab)):: nil)))%string.
Eval compute in (
  [ var_e "apair" .\ "b" ]_ (Build_store nil nil_is_map nil_is_wft nil))%string.


Definition test_prog : while.cmd := (
  "x" <- cst32_0 ;
  "x" <-* add_pe (var_e "y") cst32_1 ;
  "z" <-malloc cst32_1 ;

  var_e "z" *<- var_e "y" ;
  free (var_e "y") ;
  free (var_e "z")
)%string.

End example_m.

Module inplace_reverse_list_m.


Definition fields_typs := (("data", btyp uint32) :: ("next", rtyp (mkStag "C_lst")) :: nil)%string.
Definition C_lst : typ := styp (mkStag "C_lst") fields_typs.
Lemma wf_C_lst : wft C_lst.
Lemma sizeof_C_lst : sizeof C_lst = (4 + ptr_size)%nat.

Definition NULL : exp := cst_pe wf_C_lst (Z2u ptr_len 0).

Definition i : var := "i"%string. Definition ret : var := "ret"%string. Definition rem : var := "rem"%string.
Notation "'\~b' x" := (bneg (exp2bexp x)) (at level 60) : minC_expr_scope.

Definition reverse_list :=
  ret <- NULL ;
  while.while (\~b (var_e i \=pe NULL)) (
     rem <-* (var_e i .-> "next") ;
     (var_e i .-> "next") *<- var_e ret ;
     ret <- var_e i ;
     i <- var_e rem
  )%string.

Local Open Scope heap_scope.
Local Open Scope zarith_ext_scope.
Local Open Scope minC_assert_scope.

Inductive list_seplog : list (int 32) -> int ptr_len -> int ptr_len -> MINC_Semop.store -> MINC_Semop.heap -> Prop :=
| list_end : forall l i j s h,
  h = hp.emp ->
  u2Z i < 2 ^^ ptr_len ->
  i = j ->
  l = nil ->
  list_seplog l i j s h
| list_next : forall l i k s h l' d j h1 h2,
  h1 # h2 ->
  h = h1 +++ h2 ->
  u2Z i + 4 + Z_of_nat ptr_size < 2 ^^ ptr_len ->
  u2Z j + 4 + Z_of_nat ptr_size < 2 ^^ ptr_len ->
  u2Z k + 4 + Z_of_nat ptr_size < 2 ^^ ptr_len ->
  i <> k ->
  i <> j ->
  l = d :: l' ->
  (cst_pe wf_C_lst i |~ C_lst ~> (bval32 d :: pval j :: nil) CST_SE wf_C_lst)
  s h1 ->
  list_seplog l' j k s h2 ->
  list_seplog l i k s h.

Lemma list_seplog_ext : forall l i j s1 s2 h,
  cover (_ctxt s1) C_lst -> cover (_ctxt s2) C_lst ->
  list_seplog l i j s1 h -> list_seplog l i j s2 h.


Lemma list_seplog_hd_neq : forall l1 l2 hd1 hd2 s h,
  (list_seplog l1 hd1 (Z2u ptr_len 0) ** list_seplog l2 hd2 (Z2u ptr_len 0)) s h -> hd1 <> Z2u ptr_len 0 -> hd1 <> hd2.

Lemma cover_C_lst : forall s, s |g- "C_lst" -| fields_typs ->
 cover (_ctxt s) C_lst.

Definition pointed_list l (hd : var) : assert := fun s h =>
  exists v, [ var_e hd ]_ s = Some (pval v) /\
    list_seplog l v (Z2u ptr_len 0) s h.

Local Open Scope minC_hoare_scope.
Local Open Scope machine_int_scope.

Local Open Scope minC_types.

Lemma chars2val_styp_inv2 : forall i vi j elt tl s h lst fld tg
  (wft_t : wft (styp (mkStag tg) lst)),
  cover (_ctxt s) (styp (mkStag tg) lst) ->
  ifind fld (uzip1 lst) = Some 1%nat ->
  assoc_get fld lst = Some (rtyp (mkStag tg)) ->
  u2Z vi + Z_of_nat (iplus (map sizeof (firstn 1 (uzip2 lst)))) < 2 ^^ ptr_len ->
  s |g- tg -| lst ->
  s |t- i -| ptyp (styp (mkStag tg) lst) ->
  [var_e i ]_ s = Some (pval vi) ->
  seq_ext.s2l (hp.dom h) = seq (Zabs_nat (u2Z vi)) (sizeof (styp (mkStag tg) lst)) ->
  chars2val (styp (mkStag tg) lst) (seq_ext.s2l (hp.cdom h)) =
    (sval (elt :: pval j :: tl), nil) ->
  sizeof (styp (mkStag tg) lst) = List.length (seq_ext.s2l (hp.cdom h)) ->
  (var_e i .-> fld |~ ptyp (styp (mkStag tg) lst) ~> cst_pe wft_t j)
  s (hp.proj h (seq_ext.ran (Zabs_nat (u2Z (vi [.+] Z2u ptr_len
    (Z_of_nat (iplus (map sizeof (firstn 1 (uzip2 lst)))))))) ptr_size)).


Lemma ran_helper : forall h (i j : hp.l) a' a b b',
  (a' <= a <= a' + b)%nat -> (a + b = a' + b')%nat ->
  hp.dom h = seq_ext.ran a' b' ->
  seq.mem_seq (hp.dom (h [\m] (seq_ext.ran a b))) i ->
  seq.mem_seq (seq_ext.ran a b) j ->
  hp.ltl i j.

Lemma reverse_list_verif : forall l,
  {{ fun s h => (wf_tstore (_tstore s) /\
     s |g- "C_lst" -| fields_typs /\
     s |t- rem -| ptyp C_lst /\
     s |t- i -| ptyp C_lst /\
     s |t- ret -| ptyp C_lst) /\
    pointed_list l i s h }}
  reverse_list
  {{ pointed_list (rev l) ret }}.
Proof.
rewrite /pointed_list /reverse_list => l.

ret <- NULL ;

apply hoare_assign with (t := ptyp (C_lst)) (R := fun s h =>
    (wf_tstore (_tstore s) /\
     s |g- "C_lst" -| fields_typs /\
     s |t- rem -| ptyp C_lst /\
     s |t- i -| ptyp C_lst /\
     s |t- ret -| ptyp C_lst) /\
  exists v, [ var_e i ]_ s = Some (pval v) /\
    list_seplog l v (Z2u ptr_len 0) s h /\
    [ var_e ret ]_ s = Some pval_0).

rewrite /wp_assign => s h [[wf_s [HC_lst [Hrem [Hi Hret]]]] [v [Hv H_h]]].
rewrite /= in Hv.
rewrite /wp_assign.
exists (pval (Z2u ptr_len 0)); split; first by reflexivity.
split; first by OEqtm; apply cover_C_lst.
split; first by OEqtm; apply cover_C_lst.
split.
  repeat (split; first by Store_upd).
  by Store_upd.
exists v; split; first by Store_upd.
split; last by Store_upd.
move: H_h; apply list_seplog_ext; by apply cover_C_lst.

while.while (bop_b neq_b (var_e i) cst_expr_0)

apply minc_hoare_prop_m.hoare_while_invariant with (fun s h =>
    (wf_tstore (_tstore s) /\
     s |g- "C_lst" -| fields_typs /\
     s |t- rem -| ptyp C_lst /\
     s |t- i -| ptyp C_lst /\
     s |t- ret -| ptyp C_lst) /\
  exists l1, exists l2, l = l1 ++ l2 /\
    exists v_i, exists v_ret,
      [ var_e i ]_ s = Some (pval v_i) /\
      [ var_e ret ]_ s = Some (pval v_ret) /\
      (list_seplog l2 v_i (Z2u ptr_len 0) **
        list_seplog (rev l1) v_ret (Z2u ptr_len 0)) s h).

- rewrite /while.entails => s h [[wf_s [HC_lst [Hrem [Hi Hret]]]] [v [Hi' [Hmem Hret']]]].
  split; first by done.
  exists nil, l; split; first by reflexivity.
  eexists; eexists; split; first by apply Hi'.
  split; first by apply Hret'.
  rewrite [rev _]/=.
  exists h, hp.emp.
  split; first by map_tac_m.Disj.
  split; first by map_tac_m.Equal.
  split; first by exact Hmem.
  constructor => //.
  rewrite u2Z_Z2u.
  + by apply Zpower_0.
  + split; by [apply Zle_refl | apply Zpower_0].

- rewrite /while.entails => s h [[Henv [l1 [l2 [Hl [v_i [v_ret [Hi [Hret Hmem]]]]]]]] Hcond].
  case: Hmem => h1 [h2 [h1_d_h2 [h1_U_h2 [Hh1 Hh2]]]].
  rewrite /MINC_Hoare.eval_b /= in Hi Hcond.
  move/negPn : Hcond.

  rewrite /typof /=. typ_var.
  rewrite Hi.
  case: ifP => [|?]; last by rewrite u2Z_Z2u.
  move/Zeq_boolP => v_i_0 _.
  exists v_ret.
  split; first by exact Hret.
  inversion Hh1; subst.
  + by rewrite -app_nil_end hp.union_emp_L.
  + move/u2Z_inj : v_i_0 => ?; tauto.

rem <-* var_e i .-> "next";

apply minc_hoare_prop_m.hoare_stren with (fun s h =>
    (wf_tstore (_tstore s) /\
     s |g- "C_lst" -| fields_typs /\
     s |t- rem -| ptyp C_lst /\
     s |t- i -| ptyp C_lst /\
     s |t- ret -| ptyp C_lst) /\
  exists l1, exists l2,
  exists elt, l = l1 ++ elt :: l2 /\ exists v_i, exists v_ret, [ var_e i ]_ s = Some (pval v_i) /\
    [ var_e ret ]_ s = Some (pval v_ret) /\ v_i <> Z2u ptr_len 0 /\ v_i <> v_ret /\
    (list_seplog (elt :: l2) v_i (Z2u ptr_len 0) ** list_seplog (rev l1) v_ret (Z2u ptr_len 0)) s h).

rewrite /while.entails => s h [[[wf_s [wf_p Henv] [l1 [l2 [Hl [x1 [x2 [Hi [Hj Hmem]]]]]]]]] Hi'].
rewrite /MINC_Hoare.eval_b /= in Hi Hi'.
rewrite Hi in Hi'.

rewrite /typof /= in Hi'; typ_var2.

case: ifP Hi' => [X|X _]; first by rewrite u2Z_Z2u.
move/Zeq_boolP : X => Hi'.
case: Hmem => h1 [h2 [h1_d_h2 [h1_U_h2 [Hh1 Hh2]]]].
inversion Hh1; subst.
- by move: Hi'; move/(_ (refl_equal _)).
- split; first by tauto.
  exists l1, l', d; split; first by reflexivity.
  exists x1, x2; repeat (split => //).
  + apply (list_seplog_hd_neq (d :: l') (rev l1) _ _ s ((h3 +++ h4) +++ h2)); last by assumption.
    by exists (h3 +++ h4), h2.
  + by exists (h3 +++ h4), h2.

apply hoare_lookup_back'' with (ptyp C_lst) (fun s h =>
    (wf_tstore (_tstore s) /\
     s |g- "C_lst" -| fields_typs /\
     s |t- rem -| ptyp C_lst /\
     s |t- i -| ptyp C_lst /\
     s |t- ret -| ptyp C_lst) /\
    exists l1, exists l2, exists elt, l = l1 ++ elt :: l2 /\
      exists v_i, exists v_ret, exists v_rem,
        [ var_e i ]_ s = Some (pval v_i) /\ [ var_e ret ]_ s = Some (pval v_ret) /\
        [ var_e rem ]_ s = Some (pval v_rem) /\
        v_i <> Z2u ptr_len 0 /\ v_i <> v_ret /\
        (list_seplog (elt :: nil) v_i v_rem ** list_seplog l2 v_rem (Z2u ptr_len 0) **
          list_seplog (rev l1) v_ret (Z2u ptr_len 0)) s h).

rewrite /while.entails => s h [[wf_s [HC_lst [type_t [type_i type_ret]]]] [l1 [l2 [elt [Hl [vi [vj [Hi [Hj [Hvi_not_0 [Hvi_not_vj Hmem]]]]]]]]]]].

split; first by exact wf_s.
split; first by OEqtm; apply cover_C_lst.
split.
  rewrite /typof /=. typ_var. rewrite /=.
  Eqtm_inj.
  rewrite /C_lst.
  Eqtm.
  split.
  by Cover.
  Cover; by apply cover_C_lst.

case: Hmem => h1 [h2 [h1_U_h2 [h1_d_h2 [Hh1 Hh2]]]].
inversion Hh1; first by done.
subst l0 i0 k s0 h1.
case: H6 => elt_d l2_l'; subst d l'.

case: H7 => vi' [Hvi' [vi_type [elt_l2' [Helt_l2' [len_h3 [cdom_h3 dom_h3]]]]]].
rewrite /= in Hvi'; case: Hvi' => ?; subst vi'.
rewrite /= in Helt_l2'; case: Helt_l2' => ?; subst elt_l2'.
exists (vi [.+] Z2u ptr_len 4).
split.
  rewrite /= in Hi.
  rewrite /= /typof /=; typ_var.
  by rewrite Hi.
exists (cst_pe wf_C_lst j).
set slice_ptr := seq_ext.ran (Zabs_nat (u2Z (vi [.+] Z2u ptr_len 4))) ptr_size.
exists (hp.proj h3 slice_ptr).
exists ((h3 [\m] slice_ptr) +++ h4 +++ h2).
split.
  move: (hp.proj_difs_disj h3 slice_ptr _ (seq_ext.inc_refl _ _)) => ?.
  move: (hp.proj_difs h3 slice_ptr) => ?; by map_tac_m.Disj.
split.
  rewrite !hp.union_assoc -(hp.proj_difs h3 slice_ptr); by map_tac_m.Equal.

have H_tail_list : (var_e i .-> "next" |~ ptyp C_lst ~> cst_pe wf_C_lst j) s
     (hp.proj h3 slice_ptr).
  eapply chars2val_styp_inv2 => //.
  by apply cover_C_lst.
  rewrite /=; omega.
  rewrite cdom_h3; reflexivity.
split; first by exact H_tail_list.

eapply mapsto_strictly_exact' with (h1 := hp.proj h3 slice_ptr); last by exact H_tail_list.
- done.
- reflexivity.
- rewrite -hp.union_assoc.
  apply hp.disj_union_R.
  + by apply hp.proj_difs_disj, seq_ext.inc_refl.
  + apply hp.disj_proj_L; by map_tac_m.Disj.
- rewrite /wp_assign.
  eexists; split; first by reflexivity.
  split; first by OEqtm; apply cover_C_lst.
  split; first by OEqtm; apply cover_C_lst.
  split.
    split; first by Store_upd.
    split; first by done.
    by repeat Store_upd.
  + exists l1, l2, elt.
    split; first by exact Hl.
    exists vi, vj, j; split; repeat (split; first by Store_upd).
    by Store_upd.
    split.
      exact H4.     split.
      exact Hvi_not_vj.
    rewrite !hp.union_assoc -hp.proj_difs.
    apply (con_cons _ _ _ _ _ h1_U_h2).
    * apply (con_cons _ _ _ _ _ H).
      - apply list_next with (d := elt) (l' := nil) (h1 := h3) (h2 := hp.emp) (j := j) => //.
        + by map_tac_m.Disj.
        + by map_tac_m.Equal.
        + exists vi.
          split; first by reflexivity.
          split.
            rewrite /=; apply eqtm_refl, cover_ptyp, cover_C_lst; tauto.
          exists (sval (bval32 elt :: pval j :: nil)).
          split; first by reflexivity.
          split; first by exact len_h3.
          split; first by exact cdom_h3.
          exact dom_h3.
        + apply list_end => //; omega.
      - move: H8; apply list_seplog_ext; by apply cover_C_lst.
    * move: Hh2; apply list_seplog_ext; by apply cover_C_lst.

var_e i .-> "next" *<- var_e ret

apply hoare_mutation_backwards'' with (t := ptyp C_lst) (R := fun s h =>
  (wf_tstore (_tstore s) /\
   s |g- "C_lst" -| fields_typs /\
   s |t- rem -| ptyp C_lst /\
   s |t- i -| ptyp C_lst /\
   s |t- ret -| ptyp C_lst) /\
  exists l1, exists l2, exists elt,
    l = l1 ++ elt :: l2 /\ exists v_i, exists v_rem, [ var_e i ]_ s = Some (pval v_i) /\
      [ var_e rem ]_ s = Some (pval v_rem) /\ v_i <> Z2u ptr_len 0 /\
      (list_seplog (rev (l1 ++ elt :: nil)) v_i (Z2u ptr_len 0) **
        list_seplog l2 v_rem (Z2u ptr_len 0)) s h).

move=> s h [Henv [l1 [l2 [elt [Hl [vi [vj [vk [Hvi [Hvj [Hvk [Hvi_not_0 [Hvi_not_vj Hmem]]]]]]]]]]]]].
case: Hmem => [h1 [h2 [h1_d_h2 [h1_U_h2 [H_h1 H_h2]]]]].
case: H_h1=> [h11 [h12 [h11_d_h12 [h11_h12 [H_h11 H_h12]]]]].

split; first by tauto.
split; first by tauto.
inversion H_h11 => //; subst h0 s0 k i0 l0.
case: H6 => ? ?; subst d l'.
inversion_clear H8 => //; subst j h4; move=> {H11 H}.
rewrite hp.union_emp_R in H0; subst h11.
rewrite /= in H7.
case: H7 => vi' [Hvi' [Hvi'_type [vi'_val [Hvi'_val [len_h3 [cdom_h3 dom_h3]]]]]].
rewrite /= in Hvi'; case : Hvi' => Hvi'; subst vi'.
rewrite /= in Hvi'_val; case: Hvi'_val => Hvi'_val; subst vi'_val.

exists (cst_pe wf_C_lst vk).

set slice_ptr := seq_ext.ran (Zabs_nat (u2Z (vi [.+] Z2u ptr_len 4))) ptr_size.

exists (hp.proj h3 slice_ptr).
exists (h2 +++ (h3 [\m] slice_ptr) +++ h12).
split.
  apply hp.disj_union_R.
  + apply hp.disj_union_R.
    + apply hp.disj_proj_L; by map_tac_m.Disj.
    + apply hp.proj_difs_disj; by rewrite seq_ext.inc_refl.
  + apply hp.disj_proj_L. by map_tac_m.Disj.
split.
  move: (hp.proj_difs h3 slice_ptr) => X.
  move: (hp.proj_difs_disj h3 slice_ptr _ (seq_ext.inc_refl _ _)) => Y.
  rewrite (hp.union_com h2); last by map_tac_m.Disj.
  rewrite !hp.union_assoc -X.
  by map_tac_m.Equal.
split.

have H_tail_list : (var_e i .-> "next" |~ ptyp C_lst ~> cst_pe wf_C_lst vk) s
     (hp.proj h3 slice_ptr).
  eapply chars2val_styp_inv2 => //.
  apply cover_C_lst; tauto.
  rewrite /=; omega.
  tauto.
  tauto.
  rewrite cdom_h3; reflexivity.
exact H_tail_list.

rewrite /imp => h32' disj_h32' mapsto_h32' h' Hh'.
split; first by tauto.
exists l1, l2, elt; split; first by done.
exists vi, vk; repeat (split=> //).

exists ((h3 [\m] slice_ptr) +++ h32' +++ h2), h12.
split.
  apply hp.disj_union_L; last by map_tac_m.Disj.
  apply hp.disj_union_L; last by map_tac_m.Disj.
  apply hp.disj_sym, hp.disj_difs; by map_tac_m.Disj.
split.
  rewrite Hh' -!hp.union_assoc hp.union_com; last first.
    apply hp.disj_union_R; last by map_tac_m.Disj.
    apply hp.disj_difs; last by map_tac_m.Disj.
  rewrite -!hp.union_assoc.
  f_equal.
  by map_tac_m.Equal.
rewrite distr_rev /=.
split; last by exact H_h12.
apply list_next with (d := elt) (l' := rev l1) (h2 := h2) (j := vj)
  (h1 := (h3 [\m] slice_ptr) +++ h32') => //.
- apply hp.disj_union_L; last by map_tac_m.Disj.
  apply hp.disj_sym, hp.disj_difs; by map_tac_m.Disj.
- inversion H_h2 => //.
  rewrite H6 u2Z_Z2u //.
  + move: (min_u2Z vi) => ?; omega.
  + split; by [apply Zle_refl | apply Zpower_0].
- rewrite u2Z_Z2u //.
  + move: (min_u2Z vi) => ?; omega.
  + split; by [apply Zle_refl | apply Zpower_0].

exists vi; split; first by reflexivity.
split.
  rewrite /=; apply eqtm_refl, cover_ptyp, cover_C_lst; tauto.
eexists; split; first by reflexivity.
split.
  case: mapsto_h32' => x2 [Hx2 [Hx2' [vret [Hvret [Htype [Htype' dom_h32']]]]]].
  rewrite seq_ext.len_s2l hp.size_cdom_dom heap_prop_m.size_dom_union; last by map_tac_m.Disj.
  rewrite heap_prop_m.size_dom_difs.
  + rewrite seq_ext.size_ran -seq_ext.len_s2l dom_h3 seq_length -seq_ext.len_s2l dom_h32' seq_length sizeof_ptyp.
    rewrite Arith_ext.le_plus_minus_r2 // /C_lst sizeof_styp_iplus /= sizeof_rtyp plus_0_r; omega.
  + rewrite nodup.uniq_nodup seq_ext.s2l_ran; by apply nodup.nodup_seq.
  + apply/seq_ext.incP.
    rewrite dom_h3 seq_ext.s2l_ran /C_lst.
    apply incl_seq.
    * rewrite u2Z_add_Z2u //; last by omega.
      rewrite Zabs_nat_plus_pos //; [omega | by apply min_u2Z].
    * rewrite sizeof_styp_iplus /= u2Z_add_Z2u //; last by omega.
      rewrite Zabs_nat_plus_pos //; last by apply min_u2Z.
      rewrite sizeof_rtyp plus_0_r minus_plus (_ : Zabs_nat _ = 4%nat) //; omega.

have cdom_union_helper : forall i0 j : hp.l,
   seq.mem_seq (hp.dom (h3 [\m] slice_ptr)) i0 ->
   seq.mem_seq (hp.dom h32') j -> hp.ltl i0 j.
  move=> i j Hi Hj.
  apply ran_helper with (a' := (Zabs_nat (u2Z vi))) (a := (Zabs_nat (u2Z (vi[.+]Z2u ptr_len 4))))
    (b := ptr_size) (b' := (sizeof C_lst)) (h := h3) => //.
  rewrite u2Z_add_Z2u //; last by omega.
  rewrite Zabs_nat_Zplus //; last by apply min_u2Z.
  rewrite (_ : Zabs_nat 4 = 4%nat) //.
  move: ptr_size_4 => X; omega.
  rewrite sizeof_styp_iplus /= sizeof_rtyp plus_0_r u2Z_add_Z2u //; last by omega.
  rewrite Zabs_nat_Zplus //; last by apply min_u2Z.
  rewrite (_ : Zabs_nat 4 = 4%nat) //; omega.
  apply seq_ext.s2l_inj.
  by rewrite dom_h3 seq_ext.s2l_ran.
  case/mapsto_inv_dom : mapsto_h32' => x [Hx dom_h32'].
  rewrite sizeof_ptyp in dom_h32'.
  rewrite /= in Hvi .
  rewrite /= /typof /= in Hx; typ_var2.
  rewrite /= Hvi in Hx.
  case: Hx => ->.
  by rewrite -dom_h32'.

have Htmp4 : List.length (seq_ext.s2l (hp.cdom (h3[\m] slice_ptr))) = sizeof (btyp uint32).
  rewrite seq_ext.len_s2l hp.size_cdom_dom heap_prop_m.size_dom_difs.
  - by rewrite -seq_ext.len_s2l dom_h3 seq_length seq_ext.size_ran sizeof_C_lst plus_comm minus_plus.
  - rewrite /slice_ptr -seq_ext.l2s_seq nodup.uniq_nodup seq_ext.s2l2s; by apply nodup.nodup_seq.
  - apply/seq_ext.incP.
    rewrite dom_h3 seq_ext.s2l_ran sizeof_C_lst.
    apply incl_seq.
    + rewrite u2Z_add_Z2u //; last by omega.
      rewrite Zabs_nat_plus_pos //; by [apply le_plus_l | apply min_u2Z].
    - rewrite u2Z_add_Z2u //; last by omega.
      rewrite Zabs_nat_plus_pos //; last by apply min_u2Z.
      by rewrite minus_plus // (_ : Zabs_nat 4 = 4%nat) // plus_comm.

split.
  have Htmp : skipn (sizeof (C_lst)) (seq_ext.s2l
    (hp.cdom ((h3 [\m] slice_ptr) +++ h32'))) = nil.
    rewrite /sizeof [sizeof' _ _]/= plus_0_r.
    apply skipn_all.
    rewrite seq_ext.len_s2l hp.size_cdom_dom heap_prop_m.size_dom_union; last by map_tac_m.Disj.
    rewrite heap_prop_m.size_dom_difs; last 2 first.
    + rewrite nodup.uniq_nodup seq_ext.s2l_ran; by apply nodup.nodup_seq.
    + apply/seq_ext.incP.
      rewrite dom_h3 seq_ext.s2l_ran.
      apply incl_seq.
      - rewrite u2Z_add_Z2u //; last by omega.
        rewrite Zabs_nat_plus_pos //; [omega | by apply min_u2Z].
      - rewrite u2Z_add_Z2u //; last by omega.
        rewrite Zabs_nat_plus_pos //; last by apply min_u2Z.
        by rewrite minus_plus sizeof_C_lst (_ : Zabs_nat _ = 4%nat) // plus_comm.
    rewrite seq_ext.size_ran -{1}seq_ext.len_s2l dom_h3 seq_length sizeof_C_lst.
    move/mapsto_inv_len : mapsto_h32' => ->; rewrite sizeof_ptyp; omega.
  rewrite -Htmp.
  apply chars2val_styp_cons.
  - rewrite [snd _]/=.
    have Htmp' : skipn (sizeof (C_lst)) (seq_ext.s2l (hp.cdom h3)) = nil.
      apply skipn_all.
      by rewrite seq_ext.len_s2l hp.size_cdom_dom -seq_ext.len_s2l dom_h3 seq_length.
    rewrite -Htmp' in cdom_h3.
    case/chars2val_styp_inv : cdom_h3 => //.
      rewrite -len_h3; by apply le_refl.
    move=> cdom_h3 cdom_h3'.
    rewrite [snd _]/= in cdom_h3.
    rewrite (_ : seq_ext.s2l (hp.cdom ((h3 [\m] slice_ptr) +++ h32')) =
    seq_ext.s2l (hp.cdom (h3 [\m] slice_ptr))
    ++ seq_ext.s2l (hp.cdom h32')); last first.
      rewrite hp.cdom_union.
      + by rewrite seq_ext.s2l_cat.
      + exact cdom_union_helper.
    rewrite (skipn_app' (sizeof (btyp uint32))); last 2 first.
    + exact Htmp4.
    + by apply le_refl.
    apply chars2val_app => //; first by rewrite Htmp4.
    apply chars2val_firstn in cdom_h3.
    + have -> : seq_ext.s2l (hp.cdom (h3[\m] slice_ptr)) =
        firstn (sizeof (btyp uint32)) (seq_ext.s2l (hp.cdom h3)).
        apply trans_eq with (seq_ext.s2l (seq.take (sizeof (btyp uint32)) (hp.cdom h3))).
        * f_equal.
          move: (hp.proj_difs h3 slice_ptr) => X.
          rewrite (hp.cdom_difs _ (seq_ext.ran (Zabs_nat (u2Z vi)) (sizeof (btyp uint32)))).
          - by rewrite seq_ext.size_ran.
          - apply seq_ext.s2l_inj.
            rewrite seq_ext.s2l_cat 2!seq_ext.s2l_ran dom_h3.
            rewrite (_ : sizeof C_lst = (sizeof (btyp uint32)) + ptr_size)%nat; last by rewrite sizeof_styp_iplus /= sizeof_rtyp plus_0_r.
            rewrite seq_app2 u2Z_add_Z2u //; last by omega.
            rewrite /sizeof /= Zabs_nat_plus_pos //.
            by apply min_u2Z.
        * by apply seq_ext.s2l_take.
      by rewrite skipn_firstn.
    + rewrite seq_ext.len_s2l hp.size_cdom_dom -seq_ext.len_s2l dom_h3 seq_length sizeof_C_lst /sizeof /=; omega.
  - have -> : skipn (sizeof (snd ("data"%string, btyp uint32)))
      (seq_ext.s2l
        (hp.cdom ((h3 [\m] slice_ptr) +++ h32'))) = seq_ext.s2l (hp.cdom h32').
      rewrite hp.cdom_union.
      by rewrite seq_ext.s2l_cat skipn_app.
      exact cdom_union_helper.
    rewrite sizeof_styp_iplus /= sizeof_rtyp plus_0_r.
    move: (mapsto_h32') => mapsto_h32'_save.
    apply mapsto_inv_cdom in mapsto_h32'.
    case: mapsto_h32' => [v [X2 X3]].


    rewrite (_ : ptr_size = sizeof (styp (mkStag "C_lst")
      (("next"%string, rtyp (mkStag "C_lst")) :: nil))).
    apply chars2val_styp_cons => /=.

    have -> : chars2val (rtyp (mkStag "C_lst")) (seq_ext.s2l (hp.cdom h32')) =
      chars2val (ptyp C_lst) (seq_ext.s2l (hp.cdom h32')).
      apply chars2val_same_layout with (_ctxt s) => //.
      exact (Hctxt s).
      rewrite /C_lst.
      Eqtm.
      split.
      apply (cover_rtyp _ _ fields_typs); tauto.
      Cover. apply cover_C_lst; tauto.
    rewrite X3.
    rewrite X2 in Hvj; case: Hvj => Hvj; subst v.
    f_equal.
    rewrite skipn_all //.
    apply mapsto_inv_dom in mapsto_h32'_save.
    case: mapsto_h32'_save => x [Hx dom_h32'].
    rewrite seq_ext.len_s2l hp.size_cdom_dom -seq_ext.len_s2l.
    rewrite dom_h32'.
    rewrite seq_ext.s2l_ran seq_length.
    by rewrite sizeof_ptyp sizeof_rtyp.
    by rewrite /chars2val /=.
    by rewrite sizeof_styp_iplus /= sizeof_rtyp plus_0_r.

rewrite hp.dom_union //.
case/mapsto_inv_dom : mapsto_h32' => x [X2 X3].
rewrite X3 hp.dom_difs_del seq_ext.s2l_cat sizeof_ptyp seq_ext.s2l_del_remove_pred.
rewrite dom_h3 !seq_ext.s2l_ran remove_pred_filter -{1}seq_ext.s2l_ran seq_ext.l2s_filter.
have -> : seq_ext.ran (Zabs_nat (u2Z vi)) (sizeof C_lst) =
  seq.cat (seq_ext.ran (Zabs_nat (u2Z vi)) (sizeof (btyp uint32)))
  slice_ptr.
  apply seq_ext.s2l_inj.
  rewrite seq_ext.s2l_cat 3!seq_ext.s2l_ran u2Z_add_Z2u //; last by omega.
  rewrite Zabs_nat_plus_pos //; last by apply min_u2Z.
  by rewrite (_ : sizeof (btyp uint32) = 4%nat) // -seq_app2 sizeof_C_lst.
rewrite seq_ext.filter_ran_ran; last first.
  apply/seq_ext.disP.
  rewrite /slice_ptr 2!seq_ext.s2l_ran.
  apply disj_seq_seq.
  rewrite u2Z_add_Z2u //; last by omega.
  rewrite Zabs_nat_plus_pos //; last by apply min_u2Z.
  rewrite (_ : sizeof (btyp uint32) = 4%nat) // inj_plus (_ : (Zabs_nat 4) = 4%nat) //; by apply Zle_refl.
rewrite seq_ext.s2l_ran sizeof_C_lst seq_app2 // (_ : sizeof (btyp uint32) = 4%nat) //.
rewrite /= in X2.
rewrite /= in Hvi.
rewrite /typof /= in X2; typ_var2.
rewrite /= Hvi in X2.
case: X2 => <-.
rewrite u2Z_add_Z2u //; last by omega.
rewrite Zabs_nat_plus_pos //; by apply min_u2Z.

ret <- var_e i

apply hoare_assign with (t := ptyp C_lst) (R := fun s h =>
  (wf_tstore (_tstore s) /\
   s |g- "C_lst" -| fields_typs /\
   s |t- rem -| ptyp C_lst /\
   s |t- i -| ptyp C_lst /\
   s |t- ret -| ptyp C_lst) /\
  exists l1, exists l2, exists elt,
  l = l1 ++ elt :: l2 /\ exists v_j, exists v_rem,
    [ var_e ret ]_ s = Some (pval v_j) /\ [ var_e rem ]_ s = Some (pval v_rem) /\
    (list_seplog (rev (l1 ++ elt :: nil)) v_j (Z2u ptr_len 0) **
      list_seplog l2 v_rem (Z2u ptr_len 0)) s h).

move=> s h [[wf_s [HC_lst [Hrem [Hi Hret]]]] [l1 [l2 [elt [Hl [vi [vrem [Hvi [Hvrem [Hvi_not_0 Hmem]]]]]]]]]].
rewrite /wp_assign.
exists (pval vi); split; first by exact Hvi.
split; first by OEqtm; apply cover_C_lst.
split; first by OEqtm; apply cover_C_lst.
split.
  split; first by Store_upd.
  split; first by done.
  by repeat Store_upd.
exists l1, l2, elt; split; first by exact Hl.
exists vi, vrem; repeat (split; first by Store_upd).
case: Hmem => h1 [h2 [h1_d_h2 [h1_U_h2 [H_h1 H_h2]]]].
exists h1, h2; split; first by exact h1_d_h2.
split; first by exact h1_U_h2.

split.
- move: H_h1; apply list_seplog_ext; by apply cover_C_lst.
- move: H_h2; apply list_seplog_ext; by apply cover_C_lst.

i <- var_e rem

apply hoare_assign' with (t := ptyp C_lst).
move=> s h [[wf_s [HC_lst [Hrem [Hi Hret]]]] [l1 [l2 [elt [Hl [vi [vrem [Hvi [Hvrem Hmem]]]]]]]]].
rewrite /wp_assign.
exists (pval vrem); split; first by exact Hvrem.
split; first by OEqtm; apply cover_C_lst.
split; first by OEqtm; apply cover_C_lst.
split.
  split; first by Store_upd.
  split; first by done.
  by repeat Store_upd.
exists (l1 ++ elt :: nil), l2.

split; first by rewrite /= app_ass.
exists vrem, vi; repeat (split; first by Store_upd).

case: Hmem => h1 [h2 [h1_d_h2 [h1_U_h2 [H_h1 H_h2]]]].
exists h2, h1; split; first by map_tac_m.Disj.
split; first by map_tac_m.Equal.
split.
- move: H_h2; apply list_seplog_ext; by apply cover_C_lst.
- move: H_h1; apply list_seplog_ext; by apply cover_C_lst.
Qed.

End inplace_reverse_list_m.