Require Import Coqlib.
Require Import Maps.
Require Import Integers.
Require Import Values.
Require Import GenSem.
Require Import Coqlib.
Require Import Maps.
Require Import Integers.
Require Import Values.
Require Import RealParams.
Require Import GenSem.
Require Import Clight.
Require Import CDataTypes.
Require Import Ctypes.
Require Import PrimSemantics.
Require Import CompatClightSem.
Require Import liblayers.compcertx.Stencil.
Require Import liblayers.compat.CompatLayers.
Require Import liblayers.compat.CompatGenSem.
Require Import RData.
Require Import Constants.
Require Import HypsecCommLib.
Require Import Specs.
Require Import Invs.
Require Import Indistinguishable.
Local Open Scope Z.
Local Opaque Z.add Z.mul Z.div Z.shiftl Z.shiftr Z.land Z.lor.
Ltac halt_contra :=
match goal with
| [H1: halt ?x = true, H2: halt ?x = false |- _] =>
rewrite H1 in H2; inversion H2
| [|- _] => simpl in *
end.
Ltac clear_hyp :=
repeat
match goal with
| [H: true = true |- _ ] => clear H
| [H: false = false |- _ ] => clear H
| [H1: ?P, H2: ?P |- _ ] => clear H2
end.
Ltac destruct_zmap :=
let H := fresh "Heq" in
match goal with
| |- context [?a @ (?m # ?b == ?c)] =>
destruct (a =? b) eqn:H; bool_rel;
[rewrite H; repeat rewrite ZMap.gss| repeat rewrite (ZMap.gso _ _ H)]
end.
Ltac srewrite :=
(repeat
let T := fresh "tmp" in
match goal with
| [H:?x = ?y |- _] => repeat rewrite H in *; assert(T: True -> x = y) by (intros; apply H); clear H; rename T into H
end);
(repeat
let E := fresh "Eq" in
match goal with
| [H: True -> ?x = ?y |- _] => assert(E: x = y) by (apply H; constructor); clear H; rename E into H
end).
Ltac simpl_some :=
repeat
let T := fresh "T" in
match goal with
| [H: Some ?x = Some ?y |- _] =>
assert(T: x = y) by (inversion H; reflexivity; assumption); clear H; rename T into H
end.
Ltac simpl_obs_eq :=
match goal with
| [|- ?x _ = ?x _] => unfold x
| [|- ?x _ _ = ?x _ _] => unfold x
| [|- ?x _ _ _ = ?x _ _ _] => unfold x
| [|- ?x _ _ _ _ = ?x _ _ _ _] => unfold x
| [H: ?x = _ |- context [?x]] => rewrite H
| _ => idtac
end.
Ltac simpl_eq_goal :=
let H := fresh "Hdest" in
match goal with
| [ |- match ?x with | Some _ => _ | None => None end =
match ?x with | Some _ => _ | None => None end ] =>
destruct (x) eqn:H
| [ |- if ?x then _ else _ = if ?x then _ else _ ] =>
destruct (x) eqn:H
end.
Ltac unfold_spec H :=
match type of H with
| ?x _ = _ => unfold x in H
| ?x _ _ = _ => unfold x in H
| ?x _ _ _ = _ => unfold x in H
| ?x _ _ _ _ = _ => unfold x in H
| ?x _ _ _ _ _ = _ => unfold x in H
| ?x _ _ _ _ _ _ = _ => unfold x in H
| ?x _ _ _ _ _ _ _ = _ => unfold x in H
end; rm_bind H.
Ltac inv_hyp H := (try unfold_spec H); (try rm_bind H); repeat (simpl_hyp H; contra).
Ltac subst_all := (repeat match goal with
| [H: Some _ = Some _ |- _] => inv H
| [H: (_, _) = (_, _) |- _] => inv H
end); simpl in *.
Ltac inv_all_hyp H :=
let HC := fresh "Hdst" in
lazymatch type of H with
| context [if ?cond then _ else _] =>
destruct cond eqn:HC; contra; inv_all_hyp H
| context [match ?cond with | _ => _ end] =>
destruct cond eqn:HC; contra; inv_all_hyp HC; inv_all_hyp H
| context [post_handle_shadow_s2pt_fault_spec _ _ _ _] => idtac
| context [query_oracle _] => idtac
| context [reset_sys_regs_loop] => idtac
| context [sync_dirty_to_shadow_loop] => idtac
| context [grant_stage2_loop] => idtac
| context [revoke_stage2_loop] => idtac
| context [search_load_info_loop] => idtac
| Some _ = Some _ => inv H
| (_, _) = (_, _) => inv H
| ?f _ _ _ _ _ ?r = _ => match type of r with
| RData => idtac f; unfold f in H; try rm_bind H; inv_all_hyp H
| _ => idtac
end
| ?f _ _ _ _ ?r = _ => match type of r with
| RData => idtac f;unfold f in H; try rm_bind H; inv_all_hyp H
| _ => idtac
end
| ?f _ _ _ ?r = _ => match type of r with
| RData => idtac f;unfold f in H; try rm_bind H; inv_all_hyp H
| _ => idtac
end
| ?f _ _ ?r = _ => match type of r with
| RData => idtac f;unfold f in H; try rm_bind H; inv_all_hyp H
| _ => idtac
end
| ?f _ ?r = _ => match type of r with
| RData => idtac f;unfold f in H; try rm_bind H; inv_all_hyp H
| _ => idtac
end
| ?f ?r = _ => match type of r with
| RData => idtac f;unfold f in H; try rm_bind H; inv_all_hyp H
| _ => idtac
end
| _ => idtac
end.
Ltac simpl_conf H1 H2 :=
match type of H1 with
| match ?cond with
| Some _ => _
| None => None
end = Some _ => simpl_hyp H1; contra; simpl_conf H1 H2
| match ?cond with
| VZ64 _ => _
end = Some _ => simpl_hyp H1; simpl_conf H1 H2
| (if ?cond then ?x else ?y) = _ =>
match x with
| None => simpl_hyp H1; contra; simpl_conf H1 H2
| _ => match y with
| None => simpl_hyp H1; contra; simpl_conf H1 H2
| _ => fail
end
end
| _ =>
match type of H2 with
| match ?cond with
| Some _ => _
| None => None
end = Some _ => simpl_hyp H2; contra; simpl_conf H1 H2
| match ?cond with
| VZ64 _ => _
end = Some _ => simpl_hyp H2; simpl_conf H1 H2
| (if ?cond then ?x else ?y) = _ =>
match x with
| None => simpl_hyp H2; contra; simpl_conf H1 H2
| _ => match y with
| None => simpl_hyp H2; contra; simpl_conf H1 H2
| _ => idtac
end
end
| _ => idtac
end
end.
Ltac solve_conf Heq :=
destruct Heq; intros;
match goal with
| [H:context [observe_reg _ _ _] |- context [observe_reg _ _ _]] =>
unfold observe_reg, active in *; simpl in *; try apply H; try reflexivity
| [H:context [observe_flatmem _ _ _] |- context [observe_flatmem _ _ _]] =>
unfold observe_flatmem in *; simpl in *; try apply H
| [H:context [observe_share _ _ _] |- context [observe_share _ _ _]] =>
unfold observe_share in *; simpl in *; try apply H
| [H:context [observe_shadow_ctxt _ _ _ _] |- context [observe_shadow_ctxt _ _ _ _]] =>
unfold observe_shadow_ctxt in *; simpl in *; try apply H
| [H:context [observe_vminfo _ _] |- context [observe_vminfo _ _]] =>
unfold observe_vminfo in *; simpl in *; try apply H
| [H:context [observe_image_pfn _ _ _] |- context [observe_image_pfn _ _ _]] =>
unfold observe_image_pfn in *; simpl in *; try apply H
| [H:context [observe_cur_vcpuid _ _] |- context [observe_cur_vcpuid _ _]] =>
unfold observe_cur_vcpuid in *; simpl in *; try apply H
| [H:context [observe_data_log _ _] |- context [observe_data_log _ _]] =>
unfold observe_data_log in *; simpl in *; try apply H
| [H:context [observe_data_oracle _ _] |- context [observe_data_oracle _ _]] =>
unfold observe_data_oracle in *; simpl in *; try apply H
| [H: context [curid _] |- context [curid _]] => simpl in *; try assumption
end.
Ltac solve_ctxt_assign :=
let H := fresh "Hcond" in
match goal with
| [|- Some ?x @ (?ctxt # ?y == ?z) = Some ?x @ (?ctxt' # ?y == ?z)] =>
destruct (x=?y) eqn:H; bool_rel; [rewrite H; repeat rewrite ZMap.gss; reflexivity|
repeat rewrite (ZMap.gso _ _ H); solve_ctxt_assign]
| _ => idtac
end.
Ltac solve_role := try solve [unfold valid_role, active in *; simpl in *; assumption].