Library mcertikos.invariants.INVLemmaDevice

Require Import Coqlib.
Require Import Maps.
Require Import Constant.
Require Import GlobIdent.
Require Import FlatMemory.
Require Import CommonTactic.
Require Import FutureTactic.
Require Import AuxLemma.
Require Import DeviceStateDataType.
Require Import AbstractDataType.

Require Import Values.
Require Import AsmX.
Require Import Integers.
Require Import liblayers.compat.CompatLayers.
Require Import AST.

Require Import ObjSerialDevice.

Section SERIAL_INV.

  Lemma serial_trans_cpu_preserves_base:
    ∀ op s s´, serial_trans_cpu op s = s´ →
                      Base s = Base s´.
  Proof.
    intros. unfold Base.
    iinv s; simpl; substx; reflexivity.
  Qed.

  Lemma serial_trans_env_preserves_base:
    ∀ e s s´, serial_trans_env e s = s´ →
                      Base s = Base s´.
  Proof.
    intros. unfold Base.
    iinv s; simpl; substx; reflexivity.
  Qed.

  Lemma serial_trans_preserves_base:
    ∀ op e s s´, serial_trans_cpu op (serial_trans_env e s) = s´ →
                      Base s = Base s´.
  Proof.
    intros. remember (serial_trans_env e s) as s0;
    iinv s0; unfold_SerialState; subst; simpl; iinv s; subst s0; simpl; try reflexivity;
    simplify_eq H; auto.
  Qed.

  Lemma serial_trans_cpu_preserves_base_value:
    ∀ op d v,
      Base (s (com1 d)) = v →
      Base (serial_trans_cpu op (s (com1 d))) = v.
  Proof.
    intros. subst.
    remember (s (com1 d)) as s.
    symmetry. apply serial_trans_cpu_preserves_base with (op:=op). reflexivity.
  Qed.

  Lemma serial_trans_env_preserves_base_value:
    ∀ e d v,
      Base (s (com1 d)) = v →
      Base (serial_trans_env e (s (com1 d))) = v.
  Proof.
    intros. subst.
    remember (s (com1 d)) as s.
    symmetry. apply serial_trans_env_preserves_base with (e:=e). reflexivity.
  Qed.

  Lemma serial_trans_preserves_base_value:
    ∀ op e d v,
      Base (s (com1 d)) = v →
      Base (serial_trans_cpu op (serial_trans_env e (s (com1 d)))) = v.
  Proof.
    intros. subst.
    remember (s (com1 d)) as s.
    symmetry. apply serial_trans_preserves_base with (e:=e) (op:=op). reflexivity.
  Qed.

End SERIAL_INV.

Hint Resolve serial_trans_cpu_preserves_base_value.
Hint Resolve serial_trans_env_preserves_base_value.
Hint Resolve serial_trans_preserves_base_value.