Require Import mailbox.verif_atomic_exchange.
Require Import VST.concurrency.conclib.
Require Import VST.concurrency.ghosts.
Require Import VST.floyd.library.
Require Import VST.zlist.sublist.
Require Import mailbox.mailbox.
Require Import mailbox.verif_mailbox_specs.

Opaque eq_dec.

Lemma body_initialize_reader : semax_body Vprog Gprog f_initialize_reader initialize_reader_spec.
Proof.
  start_function.
  rewrite (data_at__isptr _ tint); Intros.
  assert_PROP (Zlength reads = N) by entailer!.
  assert (0 <= r < N) as Hr.
  { exploit (Znth_inbounds r reads); [|lia].
    intro Heq; rewrite Heq in *; contradiction. }
  assert (N < Int.max_signed) by computable.
  forward.
  forward.
  forward.
  forward.
  entailer!.
Qed.

Lemma body_start_read : semax_body Vprog Gprog f_start_read start_read_spec.
Proof.
  start_function.
  rewrite (data_at__isptr _ tint); Intros.
  assert_PROP (Zlength reads = N) by entailer!.
  assert (0 <= r < N) as Hr.
  { exploit (Znth_inbounds r reads); [|lia].
    intro Heq; rewrite Heq in *; contradiction. }
  assert (N < Int.max_signed) by computable.
  forward.
  rewrite comm_loc_isptr; Intros.
  forward.
  { entailer!. rewrite Znth_map; [auto|]. rewrite Zlength_map in *; simpl in *; lia. }
  forward.
  forward.
  set (c := Znth r comms).
  set (l := Znth r locks).
  forward_call (sh2, c, g, l, vint 0, Empty, h,
    fun h b => !!(b = Empty /\ latest_read h (vint b0)) &&
      (EX v : Z, data_at sh tbuffer (vint v) (Znth b0 bufs)) * ghost_var gsh1 (vint b0) g0,
    comm_R bufs sh gsh2 g0 g1 g2, fun h b => EX b' : Z, !!((if eq_dec b Empty then b' = b0 else b = vint b') /\
      -1 <= b' < B /\ latest_read h (vint b')) &&
      (EX v : Z, data_at sh tbuffer (vint v) (Znth b' bufs)) * ghost_var gsh1 (vint b') g0).
  { entailer!. rewrite Znth_map; rewrite Zlength_map in *; auto; lia. }
  { unfold comm_loc; entailer!.
    rewrite <- emp_sepcon at 1; apply sepcon_derives; [|cancel].
    unfold AE_spec.
    apply allp_right; intro hc.
    apply allp_right; intro hx.
    apply allp_right; intro vc.
    apply allp_right; intro vx.
    rewrite <- imp_andp_adjoint; Intros.
    rewrite <- wand_sepcon_adjoint, emp_sepcon; Intros.
    unfold comm_R at 1 2.
    rewrite !rev_app_distr; simpl.
    rewrite !last_two_reads_cons, prev_taken_cons.
    unfold last_write in *; simpl in *.
    pose proof (last_two_reads_fst (rev hx)).
    Intros b b1 b2.
    assert (last_two_reads (rev hx) = (vint b1, vint b2)) as Hlast by assumption.
    rewrite <- sepcon_assoc, sepcon_comm, <- !sepcon_assoc, 3sepcon_assoc.
    erewrite ghost_var_share_join' by eauto; Intros.
    eapply derives_trans; [apply sepcon_derives, derives_refl;
      apply ghost_var_update with (v' := vint (if eq_dec (vint b) Empty then b0 else b))|].
    eapply derives_trans, bupd_mono; [apply bupd_frame_r|].
    assert (repable_signed b0) by (apply repable_buf; lia).
    assert (b1 = b0) by (apply repr_inj_signed; auto); subst.
    lapply (repable_buf b); auto; intro.
    rewrite Hlast.
    erewrite <- ghost_var_share_join by eauto.
    Exists (-1) (if eq_dec (vint b) Empty then b0 else b)
      (if eq_dec (vint b) Empty then b2 else b0); entailer!.
    { split; [rewrite Forall_app; repeat constructor; auto|].
      { exists b, (-1); split; [|split]; auto; lia. }
      rewrite eq_dec_refl.
      if_tac; auto. }
    rewrite !eq_dec_refl.
    Exists (if eq_dec (vint b) Empty then b0 else b).
    rewrite <- exp_sepcon2; cancel.
    lapply (hist_incl_lt hc hx); auto; intro.
    destruct (eq_dec (vint b) Empty).
    - assert (b = -1) by (apply Empty_inj; auto; apply repable_buf; auto).
      subst; rewrite eq_dec_refl; entailer!.
      rewrite latest_read_Empty; auto.
    - destruct (eq_dec b (-1)); [subst; contradiction n; auto|].
      entailer!.
      apply latest_read_new; auto. }
  Intros x b'; destruct x as (t, v). simpl fst in *; simpl snd in *.
  assert (exists b, v = vint b /\ -1 <= b < B /\ if eq_dec b (-1) then b' = b0 else b' = b) as (b & ? & ? & ?).
  { destruct (eq_dec v Empty); subst.
    - exists (-1); rewrite eq_dec_refl; split; auto; lia.
    - do 2 eexists; eauto; split; [lia|].
      destruct (eq_dec b' (-1)); [subst; contradiction n; auto | auto]. }
  exploit repable_buf; eauto; intro; subst.
  forward_if (temp _t'2 (bool2val (negb (eq_dec b (-1))))).
  { if_tac in H13; try lia.
    forward.
    entailer!!.
    destruct (zlt _ _); auto.
    unfold B, N in *; lia. }
  { forward.
    destruct (eq_dec b (-1)); [|lia].
    entailer!!. }
  forward_if (PROP () LOCAL (temp _b (vint (if eq_dec b (-1) then b0 else b)); temp _rr (Znth r reads);
      temp _r (vint r); gvars gv)
    SEP (comm_loc sh2 l c g g0 g1 g2 bufs sh gsh2 (map_upd h t (AE (vint b) Empty));
         EX v : Z, data_at sh tbuffer (vint v) (Znth (if eq_dec b (-1) then b0 else b) bufs);
         ghost_var gsh1 (vint b') g0;
         data_at sh1 (tarray (tptr tint) N) reads (gv _reading); data_at sh1 (tarray (tptr tint) N) lasts (gv _last_read);
         data_at_ Ews tint (Znth r reads);
         data_at Ews tint (vint (if eq_dec b (-1) then b0 else b)) (Znth r lasts);
         data_at sh1 (tarray (tptr tint) N) comms (gv _comm);
         data_at sh1 (tarray (tptr t_lock) N) (map ptr_of locks) (gv _lock))).
  -
    forward. if_tac; inv H11.
    entailer!!.
  - forward. if_tac; inv H11.
    entailer!!.
  - forward.
    forward.
    Exists (if eq_dec b (-1) then b0 else b) t (vint b) v.
    apply andp_right.
    { apply prop_right.
      split; [destruct (eq_dec b (-1)); auto; lia|].
      destruct (eq_dec (vint b) Empty).
      + assert (b = -1) by (apply Empty_inj; auto).
        subst; rewrite eq_dec_refl; auto.
      + destruct (eq_dec b (-1)); [subst; contradiction n; auto|].
        split; auto; split; auto; apply latest_read_new; auto. }
    subst c l; cancel.
    destruct (eq_dec b (-1)); subst; apply derives_refl.
Qed.

Lemma body_finish_read : semax_body Vprog Gprog f_finish_read finish_read_spec.
Proof.
  start_function.
  rewrite (data_at__isptr _ tint); Intros.
  assert_PROP (Zlength reads = N) by entailer!.
  assert (0 <= r < N) as Hr.
  { exploit (Znth_inbounds r reads); [|lia].
    intro Heq; rewrite Heq in *; contradiction. }
  assert (N < Int.max_signed) by computable.
  forward.
  forward.
  entailer!.
Qed.
