Library mcertikos.objects.cpulocaldef.ByteListProp

Require Import Coqlib.
Require Import Maps.
Require Import Values.
Require Import Constant.
Require Import GlobalOracle.
Require Import CommonTactic.
Require Import AST.

Lemma proj_bytes_bytelist:
  ∀ l l0,
    proj_bytes l = Some l0 →
    ∃ l´, l = ByteList l´.
Proof.
  induction l; simpl; intros.
  - ∃ nil. trivial.
  - subdestruct.
    exploit IHl; eauto.
    intros (l´ & ->).
    ∃ (i::l´). trivial.
Qed.

Lemma decode_val_bytelist:
  ∀ v l,
    Vint v = decode_val Mint32 l →
    ∃ l´, l = ByteList l´.
Proof.
  unfold decode_val. intros.
  destruct (proj_bytes l) eqn: Hp; subst.
  - eapply proj_bytes_bytelist; eauto.
  - unfold proj_pointer in H.
    destruct l; try congruence.
    destruct m; try congruence.
    destruct (check_pointer 4 b i (Pointer b i n :: l)); try congruence.
Qed.

Lemma ByteList_cons:
  ∀ l l´,
    ByteList (l ++ l´) = ByteList (l) ++ ByteList (l´).
Proof.
  induction l.
  - simpl. trivial.
  - intros. simpl. rewrite <- IHl. trivial.
Qed.