Module MemdataC

Require Import Coqlib.
Require Archi.
Require Import AST.
Require Import Integers.
Require Import Floats.
Require Import Values.
Require Import Memdata.

Require Import CoqlibC.


Ltac my_tac :=
  match goal with
  | [ H: context[match ?x with _ => _ end] |- _ ] =>
    let name := fresh "A" in destruct x eqn:name; ss; subst;
                             try rewrite andb_true_iff in *; des; des_sumbool; subst
  end.

Lemma proj_bytes_only_bytes
      mvs bts
      (PROJ: proj_bytes mvs = Some bts):
    forall mv (IN: In mv mvs), exists bt, mv = Byte bt.
Proof.
  ginduction mvs; ii; ss. des_ifs. des; clarify; ss; eauto.
Qed.

Lemma decode_fragment_all chunk vl v mv q n
      (DECODE: decode_val chunk vl = v)
      (IN: In (Fragment mv q n) vl)
      (VALUE: v <> Vundef):
    mv = v.
Proof.
  unfold decode_val in *.
  destruct (proj_bytes vl) eqn:T.
  { hexploit proj_bytes_only_bytes; eauto. i; des. clarify. }
  clear T. sguard in IN. destruct chunk; ss; des_ifs; clear_tac; destruct vl; ss; repeat my_tac; unsguard IN; des; clarify.
Qed.

Lemma decode_normal_all_normal chunk vl v mv
      (DECODE: decode_val chunk vl = v)
      (VALUE: v <> Vundef /\ forall blk ofs, v <> Vptr blk ofs)
      (IN: In mv vl):
    forall blk ofs q n, mv <> Fragment (Vptr blk ofs) q n.
Proof.
  ii. des. rewrite H in *.
  destruct v; ss; exploit decode_fragment_all; eauto; i; clarify.
  - exfalso. eapply VALUE0. eauto.
Qed.

Lemma decode_pointer_all_pointer chunk vl mv blk ofs
      (DECODE: decode_val chunk vl = Vptr blk ofs)
      (IN: In mv vl):
    exists q n, mv = Fragment (Vptr blk ofs) q n.
Proof.
  unfold decode_val, Val.load_result in *. des_ifs; unfold proj_value in *; des_ifs;
      repeat (repeat (apply_all_once andb_prop; des); des_sumbool; clarify; des_ifs_safe; ss; des; ss; clarify); eauto; des_ifs.
Qed.

Program Instance memval_inject_Reflexive: RelationClasses.Reflexive (@memval_inject inject_id).
Next Obligation.
  destruct x; ss; econs; eauto. apply val_inject_id. ss.
Qed.