-
Notifications
You must be signed in to change notification settings - Fork 0
/
Copy pathRobustHyperSafetyCriterion.v
150 lines (120 loc) · 5.44 KB
/
RobustHyperSafetyCriterion.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
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 RobustHyperSafetyPreservation.
Require Import RobustSSCHCriterion.
Require Import PropExtensionality.
Definition prop_extensionality := propositional_extensionality.
Section RobustHSafeCriterion.
Variable Source Target: Language.
Variable compilation_chain : CompilationChain Source Target.
Variable T_evs S_evs : Events.
Variable T_end S_end : Endstates.
Local Definition trace__S := @trace S_evs S_end.
Local Definition finpref__S := @finpref S_evs S_end.
Local Definition trace__T := @trace T_evs T_end.
Local Definition finpref__T := @finpref T_evs T_end.
Local Definition prefix__T := @prefix T_evs T_end.
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.
Local Definition HSafety__S := @HSafe S_evs S_end.
Local Definition HSafety__T := @HSafe T_evs T_end.
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 par__T := par Target.
Local Definition ctx__S := ctx Source.
Local Definition ctx__T := ctx Target.
Local Definition rhsat__S := rhsat Source_Semantics.
Local Definition rhsat__T := rhsat Target_Semantics.
Local Definition cmp := compile_par Source Target compilation_chain.
Local Notation "P ↓" := (cmp P) (at level 50).
(* CA: don't understand why this does not work
Local Notation " C [ P ] " := (plug _ P C) (at level 50).
*)
Local Definition plug__S:= plug Source.
Local Definition plug__T := plug Target.
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 sCl_σRhP := sCl_σRhP compilation_chain
Source_Semantics Target_Semantics
σ'.
Local Definition hsCl_τRhP := hsCl_τRhP compilation_chain
Source_Semantics Target_Semantics
τ'.
Definition rel_RHSC :=
forall P C__T (M : finpref -> Prop), Observations M ->
M <<< (beh__T (plug__T (P↓) C__T)) ->
(exists C__S, forall m, M m -> exists t s, prefix__T m t /\
rel s t /\
beh__S (plug__S P C__S) s).
Lemma conclusion_RSHC (P : par__S) (M : finpref__T -> Prop) (C__S : ctx__S) :
(forall m, M m -> exists t s, prefix__T m t /\
rel s t /\
beh__S (plug__S P C__S) s) <->
M <<< τ' (beh__S (plug__S P C__S)).
Proof. firstorder. Qed.
Local Definition rel_RSCHC := @rel_RSCHC Source Target compilation_chain trace__S trace__T
Source_Semantics Target_Semantics rel.
Lemma rel_RSCHC_rel_RHSC : rel_RSCHC -> rel_RHSC.
Proof.
move => H_tilde P Ct M Obs_M H_M.
destruct (H_tilde P Ct) as [Cs H_Cs].
exists Cs => m M_m.
destruct (H_M m M_m) as [t [H_t m_pref_t]].
destruct (H_Cs t H_t) as [s [rel_s_t H_s]]. now exists t, s.
Qed.
Theorem rel_RHSC_sCl_σRHSP :
rel_RHSC <-> (forall P (H: hprop__T), HSafe H -> sCl_σRhP P H).
Proof.
split.
- move => H_tilde P H__T H_HSafe.
setoid_rewrite contra_σRhP. move => [Ct H_tgt].
destruct (H_HSafe _ H_tgt) as [M [M_obs [M_leq_beh M_wit]]].
destruct (H_tilde P Ct M) as [Cs H_conclusion]; auto.
move/conclusion_RSHC : H_conclusion => H_conclusion.
exists Cs => Hf. destruct Hf as [bs [H_bs beh_γ_bs]].
destruct H_bs as [bt [H_bt Heq]]. subst.
move/rel_adjunction_law : beh_γ_bs => τ_beh_bt.
apply: (M_wit bt); auto.
{ move => m M_m. destruct (H_conclusion m) as [t [H_t pref_m_t]]; auto.
exists t. split; auto. }
- move => Hσ P Ct M M_obs M_leq_beh_tgt.
have HSafe_H : HSafe (fun b :prop__T => ~ M <<< b).
{ move => b. rewrite -dne => M_b. now exists M. }
move/contra: (Hσ P (fun b : prop__T => ~ M <<< b) HSafe_H).
rewrite !neg_rhsat. move => HγP.
destruct HγP as [Cs H_src]. by exists Ct.
exists Cs. rewrite conclusion_RSHC.
apply: NNPP => Hf. apply: H_src.
exists (σ' (τ' (beh__S (plug__S P Cs)))). split.
+ by exists (τ' (beh__S (plug__S P Cs))).
+ move/Galois_equiv : rel_adjunction_law.
move => [mono_gamma [mono_tau [G1 G2]]]. by apply: G1.
Qed.
Theorem rel_RHSC_hsCl_τRHSP :
rel_RHSC <-> (forall P (H: hprop__S), SSC H -> hsCl_τRhP P H).
Proof.
setoid_rewrite <- τRSCHP_σRSCHP.
exact rel_RHSC_sCl_σRHSP.
exact rel_adjunction_law.
Qed.
End RobustHSafeCriterion.