-
Notifications
You must be signed in to change notification settings - Fork 0
/
Copy pathRobustHyperCriterion.v
156 lines (125 loc) · 5.62 KB
/
RobustHyperCriterion.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
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
From mathcomp Require Import all_ssreflect.
Set Implicit Arguments.
Unset Printing Implicit Defensive.
Require Import ClassicalExtras.
Require Import MyNotation.
Require Import Setoid.
Require Import FunctionalExtensionality.
Require Import Galois.
Require Import LanguageModel.
Require Import TraceModel.
Require Import Properties.
Require Import ChainModel.
Require Import RobustHyperProperty.
Require Import RobustTraceCriterion.
Require Import PropExtensionality.
Definition prop_extensionality := propositional_extensionality.
Section RobustHyperCriterion.
Variable Source Target: Language.
Variable compilation_chain : CompilationChain Source Target.
(*CA: we don't need a particular structure of traces to define preservation
e.g. traces = values or our defn of traces both make sense
*)
Variable trace__S trace__T : Set.
Local Definition prop__S := prop trace__S.
Local Definition prop__T := prop trace__T.
Local Definition hprop__S := hprop trace__S.
Local Definition hprop__T := hprop trace__T.
Variable Source_Semantics : Semantics Source trace__S.
Variable Target_Semantics : Semantics Target trace__T.
Local Definition sem__S := sem Source_Semantics.
Local Definition sem__T := sem Target_Semantics.
Local Definition beh__S := beh Source_Semantics.
Local Definition beh__T := beh Target_Semantics.
Local Definition par__S := par Source.
Local Definition ctx__S := ctx Source.
Local Definition par__T := par Target.
Local Definition ctx__T := ctx Target.
Local Definition rsat__S := rsat Source_Semantics.
Local Definition rsat__T := rsat Target_Semantics.
Local Definition hsat__S := hsat Source_Semantics.
Local Definition rhsat__S := rhsat Source_Semantics.
Local Definition rhsat__T := rhsat Target_Semantics.
Local Definition cmp := compile_par Source Target compilation_chain.
Local Definition plug__S := plug Source.
Local Definition plug__T := plug Target.
Local Notation "P ↓" := (cmp P) (at level 50).
Variable rel : trace__S -> trace__T -> Prop.
Local Definition adjunction := induced_connection rel.
Local Definition τ' : prop__S -> prop__T := α adjunction.
Local Definition σ' : prop__T -> prop__S := γ adjunction.
Local Definition rel_adjunction_law : Adjunction_law τ' σ' := adjunction_law adjunction.
Local Definition τRhP := τRhP compilation_chain
Source_Semantics Target_Semantics
τ'.
Local Definition σRhP := σRhP compilation_chain
Source_Semantics Target_Semantics
σ'.
Local Definition τRHP := τRHP compilation_chain
Source_Semantics Target_Semantics
τ'.
Local Definition σRHP := σRHP compilation_chain
Source_Semantics Target_Semantics
σ'.
Definition rel_RHC := forall P C__T, exists C__S,
forall t__T, (beh__T (plug__T (P ↓) C__T) t__T <->
(exists t__S, rel t__S t__T /\ beh__S (plug__S P C__S) t__S)).
Lemma rel_RHC' : rel_RHC <-> forall P C__T, exists C__S, (beh__T (plug__T (P ↓) C__T) = τ' (beh__S (plug__S P C__S))).
split => Hrel P C__T.
destruct (Hrel P C__T) as [C__S Hrel'].
exists C__S. apply functional_extensionality => t__T. apply: prop_extensionality.
rewrite Hrel'. by firstorder.
destruct (Hrel P C__T) as [C__S Hrel'].
rewrite Hrel'. by firstorder.
Qed.
Theorem rel_RHC_τRHP : rel_RHC <-> τRHP.
Proof.
rewrite rel_RHC'. split.
- move => H_rel P h__S H_src C__T.
destruct (H_rel P C__T) as [C__S H_rel'].
exists (beh__S (plug__S P C__S)). split.
+ by apply: (H_src C__S).
+ by rewrite -H_rel'.
- move => H_τHP P C__T. specialize (H_τHP P (fun π__S => exists C__S, π__S = beh__S (plug__S P C__S))).
have Hfoo : rhsat__S P (fun π__S => exists C__S, π__S = beh__S (plug__S P C__S)).
{ move => C__S. by exists C__S. }
destruct (H_τHP Hfoo C__T) as [bs [[C__S Heq] H]].
exists C__S. subst. exact H.
Qed.
(*CA: if τ ⇆ σ is an insertion then
tilde_HC => σHP
but not able to prove the vicerversa holds
(quite convinced it is not true)
*)
Lemma rel_RHC_σRHP : (Insertion_snd τ' σ') ->
rel_RHC -> σRHP.
Proof.
rewrite rel_RHC' => HIns Hrel P H__T Hsrc C__T.
move: (Hrel P C__T).
move => [C__S Heq].
move: (Hsrc C__S). move => [b__t [Hb__T Hσ]].
have Hfoo: beh__T (plug__T (P ↓) C__T) = b__t.
{ rewrite Heq.
have Hfoo' : τ' (beh__S (plug__S P C__S)) = τ' ( σ' b__t) by rewrite -Hσ.
move: Hfoo'. by rewrite HIns. }
rewrite /hsat.
have Hstrange: (beh Target_Semantics (plug Target (RobustHyperProperty.cmp compilation_chain P) C__T))= b__t by rewrite -Hfoo.
now rewrite Hstrange.
Qed.
Lemma σRHP_rel_RHC:
(Reflection_fst τ' σ') ->
σRHP -> rel_RHC.
Proof.
rewrite rel_RHC' => Hrefl Hσpres P Ct.
rewrite /RobustHyperProperty.σRhP .
have Hfoo: (RobustHyperProperty.rhsat__S Source_Semantics P
(RobustHyperProperty.σ σ'
(fun π__T : prop trace__T => exists C__S : ctx Source, π__T = τ' (beh__S (plug__S P C__S))))).
{
move => C__S. exists (fun t => (τ' (beh__S (plug__S P C__S)) t)).
split. by exists C__S. by rewrite Hrefl.
}
move: (Hσpres P (fun π__T => exists C__S, π__T = τ' (beh__S (plug__S P C__S))) Hfoo).
by firstorder.
Qed.
End RobustHyperCriterion.