-
Notifications
You must be signed in to change notification settings - Fork 1
/
SoundReduceMaydiff.v
117 lines (99 loc) · 3.18 KB
/
SoundReduceMaydiff.v
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
Require Import syntax.
Require Import alist.
Require Import FMapWeakList.
Require Import Classical.
Require Import Coqlib.
Require Import infrastructure.
Require Import Metatheory.
Import LLVMsyntax.
Import LLVMinfra.
Require Import opsem.
Require Import sflib.
Require Import paco.
Import Opsem.
Require Import TODO.
Require Import Exprs.
Require Import Hints.
Require Import Postcond.
Require Import Validator.
Require Import GenericValues.
Require AssnMem.
Require AssnState.
Set Implicit Arguments.
Lemma project_into_IdT_spec e x:
project_into_IdT e = Some x <-> e = Expr.value (ValueT.id x).
Proof.
destruct e; ss. des_ifs.
split; inversion 1; auto.
Qed.
Lemma project_into_IdTSet_In s x:
IdTSet.In x (project_into_IdTSet s) ->
exists e, ExprPairSet.In (Expr.value (ValueT.id x), e) s.
Proof.
unfold project_into_IdTSet. i.
rewrite ExprPairSet.fold_1 in *.
rewrite <- fold_left_rev_right in *.
remember (rev (ExprPairSet.elements s)) as s_elem.
assert (incl s_elem (rev (ExprPairSet.elements s))).
{ subst. apply incl_refl. }
clear Heqs_elem.
induction s_elem; i.
{ ss. inversion H. }
destruct a as [a1 a2]. ss.
des_ifs.
- rewrite IdTSetFacts.add_iff in *. des.
+ rewrite project_into_IdT_spec in *. subst.
exploit IdT.compare_leibniz; eauto. i. subst.
exists a2.
rewrite ExprPairSetFacts.elements_iff.
eapply InA_equiv with (eqB:=eq).
{ split.
- apply ExprPair.compare_leibniz.
- inversion 1. apply ExprPairFacts.compare_refl.
}
apply InA_iff_In.
apply in_rev.
unfold ExprPairSet.elt in *.
exploit elim_incl_cons; eauto. i. des. eauto.
+ exploit IHs_elem; eauto.
exploit elim_incl_cons; eauto. i. des. eauto.
- exploit IHs_elem; eauto.
exploit elim_incl_cons; eauto. i. des. eauto.
Qed.
Lemma reduce_maydiff_sound
m_src m_tgt
conf_src st_src
conf_tgt st_tgt
invst assnmem inv
(CONF: AssnState.valid_conf m_src m_tgt conf_src conf_tgt)
(STATE: AssnState.Rel.sem conf_src conf_tgt st_src st_tgt invst assnmem inv)
(MEM: AssnMem.Rel.sem conf_src conf_tgt st_src.(Mem) st_tgt.(Mem) assnmem):
exists invst1,
<<STATE: AssnState.Rel.sem conf_src conf_tgt st_src st_tgt invst1 assnmem
(reduce_maydiff inv)>>.
Proof.
exists invst.
unfold reduce_maydiff. red.
inv STATE.
econs; ss. intro x. i.
rewrite IdTSetFacts.diff_b in NOTIN. des_bool. des.
{ apply MAYDIFF. auto. }
des_bool.
rewrite <- IdTSetFacts.mem_iff in NOTIN.
apply project_into_IdTSet_In in NOTIN. des.
rewrite ExprPairSetFacts.filter_iff in NOTIN; [|solve_compat_bool].
rewrite ExprPairSetFacts.filter_iff in NOTIN; [|solve_compat_bool].
rewrite ExprPairSetFacts.filter_iff in NOTIN; [|solve_compat_bool].
des. unfold swap_pair in *. ss.
rewrite <- ExprPairSetFacts.mem_iff in *.
ii.
inv SRC. rename LESSDEF into LESSDEF_SRC.
exploit LESSDEF_SRC; eauto. i. des. ss.
exploit AssnState.Rel.not_in_maydiff_expr_spec; eauto.
i. des.
inv TGT. rename LESSDEF into LESSDEF_TGT.
exploit LESSDEF_TGT; eauto. i. des. ss.
esplits; eauto.
eapply GVs.inject_lessdef_compose; eauto.
eapply GVs.lessdef_inject_compose; eauto.
Qed.