Skip to content

Commit 6172ecf

Browse files
author
Carmine Abate
committed
The whole diagramis now in Coq
1 parent db0cdff commit 6172ecf

File tree

3 files changed

+287
-1
lines changed

3 files changed

+287
-1
lines changed

‎Robust2relHyperCriterion.v

+168
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,168 @@
1+
From mathcomp Require Import all_ssreflect.
2+
3+
Set Implicit Arguments.
4+
Unset Printing Implicit Defensive.
5+
6+
Require Import ClassicalExtras.
7+
Require Import MyNotation.
8+
Require Import Setoid.
9+
Require Import FunctionalExtensionality.
10+
11+
Require Import Galois.
12+
Require Import LanguageModel.
13+
Require Import TraceModel.
14+
Require Import Properties.
15+
Require Import ChainModel.
16+
Require Import Robust2relHyperProperty.
17+
18+
Require Import PropExtensionality.
19+
Definition prop_extensionality := propositional_extensionality.
20+
21+
Section Robust2relHCrit.
22+
23+
Variable Source Target: Language.
24+
Variable compilation_chain : CompilationChain Source Target.
25+
26+
(*CA: we don't need a particular structure of traces to define preservation
27+
e.g. traces = values or our defn of traces both make sense
28+
*)
29+
Variable trace__S trace__T : Type.
30+
31+
Local Definition prop__S := prop trace__S.
32+
Local Definition prop__T := prop trace__T.
33+
34+
Variable Source_Semantics : Semantics Source trace__S.
35+
Variable Target_Semantics : Semantics Target trace__T.
36+
37+
Local Definition sem__S := sem Source_Semantics.
38+
Local Definition sem__T := sem Target_Semantics.
39+
Local Definition beh__S := beh Source_Semantics.
40+
Local Definition beh__T := beh Target_Semantics.
41+
Local Definition par__S := par Source.
42+
Local Definition par__T := par Target.
43+
Local Definition ctx__S := ctx Source.
44+
Local Definition ctx__T := ctx Target.
45+
Local Definition rhsat__S := rhsat2 Source_Semantics.
46+
Local Definition rhsat__T := rhsat2 Target_Semantics.
47+
48+
Local Definition cmp := compile_par Source Target compilation_chain.
49+
50+
Local Notation "P ↓" := (cmp P) (at level 50).
51+
(* CA: don't understand why this does not work
52+
53+
Local Notation " C [ P ] " := (plug _ P C) (at level 50).
54+
*)
55+
Local Definition plug__S:= plug Source.
56+
Local Definition plug__T := plug Target.
57+
58+
Variable rel : trace__S -> trace__T -> Prop.
59+
60+
(* __π to highlights these maps are mappings between properties *)
61+
Local Definition σ__π : (trace__T -> Prop) -> (trace__S -> Prop) :=
62+
γ (@induced_connection (trace__T) (trace__S) rel).
63+
64+
Local Definition τ__π : (trace__S -> Prop) -> (trace__T -> Prop) :=
65+
α (@induced_connection (trace__T) (trace__S) rel).
66+
67+
Local Definition induced_adj : Adjunction_law τ__π σ__π :=
68+
adjunction_law (induced_connection rel).
69+
70+
Local Definition σ : (prop__T * prop__T -> Prop) -> (prop__S * prop__S -> Prop) := σ σ__π.
71+
Local Definition τ : (prop__S * prop__S -> Prop) -> (prop__T * prop__T -> Prop) := τ τ__π.
72+
73+
Local Definition τR2HP := τR2HP compilation_chain
74+
Source_Semantics Target_Semantics
75+
τ__π.
76+
77+
Local Definition σR2HP := σR2HP compilation_chain
78+
Source_Semantics Target_Semantics
79+
σ__π.
80+
81+
82+
Definition rel_R2HC := forall P1 P2 C__T, exists C__S,
83+
(forall t__T, beh__T (plug__T (P1 ↓) C__T) t__T <->
84+
(exists t__S, rel t__S t__T /\ beh__S (plug__S P1 C__S) t__S))
85+
/\
86+
(forall t__T, (beh__T (plug__T (P2 ↓) C__T) t__T <->
87+
(exists t__S, rel t__S t__T /\ beh__S (plug__S P2 C__S) t__S))).
88+
89+
Lemma rel_R2HC' : rel_R2HC <-> forall P1 P2 C__T, exists C__S,
90+
(beh__T (plug__T (P1 ↓) C__T) = τ__π (beh__S (plug__S P1 C__S))) /\
91+
(beh__T (plug__T (P2 ↓) C__T) = τ__π (beh__S (plug__S P2 C__S))).
92+
Proof.
93+
split => Hrel P1 P2 C__T.
94+
+ destruct (Hrel P1 P2 C__T) as [C__S [Hrel1' Hrel2']].
95+
exists C__S. split;
96+
apply functional_extensionality => t__T; apply: prop_extensionality;
97+
[rewrite Hrel1' | rewrite Hrel2']; by firstorder.
98+
+ destruct (Hrel P1 P2 C__T) as [C__S [Hrel1' Hrel2']].
99+
rewrite Hrel1' Hrel2'. by firstorder.
100+
Qed.
101+
102+
Theorem rel_RHC_τRHP : rel_R2HC <-> τR2HP.
103+
Proof.
104+
rewrite rel_R2HC'. split.
105+
- move => H_rel P1 P2 h__S H_src C__T.
106+
destruct (H_rel P1 P2 C__T) as [C__S [H_rel1' H_rel2']].
107+
exists (beh__S (plug__S P1 C__S)), (beh__S (plug__S P2 C__S)).
108+
rewrite /=. split.
109+
+ exact H_rel1'.
110+
+ split. exact H_rel2'.
111+
apply: (H_src C__S).
112+
- move => H_τHP P1 P2 C__T.
113+
specialize (H_τHP P1 P2 (fun π__S => exists C__S, π__S = (beh__S (plug__S P1 C__S), beh__S (plug__S P2 C__S)))).
114+
have Hfoo : rhsat__S P1 P2 (fun π__S => exists C__S, π__S = (beh__S (plug__S P1 C__S), beh__S (plug__S P2 C__S))).
115+
{ move => C__S. by exists C__S. }
116+
destruct (H_τHP Hfoo C__T) as [bs1 [bs2 [H1 [H2 [C__S Heq]]]]].
117+
exists C__S. inversion Heq. subst. simpl in *.
118+
by rewrite -H1 -H2.
119+
Qed.
120+
121+
(*
122+
To prove the following we need
123+
τ ⇆ σ to be an insertion
124+
*)
125+
126+
Lemma rel_R2HC_σR2HP : (Insertion_snd τ__π σ__π) ->
127+
rel_R2HC -> σR2HP.
128+
Proof.
129+
rewrite rel_R2HC' => HIns Hrel P1 P2 H__T Hsrc C__T.
130+
move: (Hrel P1 P2 C__T).
131+
move => [C__S [Heq1 Heq2]].
132+
move: (Hsrc C__S). move => [b1 [b2 [Hb1 [Hb2 Hσ]]]].
133+
simpl in *.
134+
have [Hfoo1 Hfoo2]: beh__T (plug__T (P1 ↓) C__T) = b1 /\ beh__T (plug__T (P2 ↓) C__T) = b2.
135+
{ split; [rewrite Heq1 | rewrite Heq2];
136+
[have Hsuff: beh__S (plug__S P1 C__S) = (σ__π b1) by apply Hb1 |
137+
have Hsuff: beh__S (plug__S P2 C__S) = (σ__π b2) by apply Hb2];
138+
by rewrite Hsuff HIns. }
139+
rewrite /hsat2.
140+
rewrite <- Hfoo1 in Hσ. rewrite <- Hfoo2 in Hσ.
141+
exact Hσ.
142+
Qed.
143+
144+
Lemma σRHP_rel_RHC:
145+
(Reflection_fst τ__π σ__π) ->
146+
σR2HP -> rel_R2HC.
147+
Proof.
148+
rewrite rel_R2HC' => Hrefl Hσpres P1 P2 Ct.
149+
have Hfoo: (rhsat__S P1 P2 (σ (fun π__T =>
150+
exists C__S : ctx Source,
151+
π__T = (τ__π (beh__S (plug__S P1 C__S)),
152+
τ__π (beh__S (plug__S P2 C__S))) ))).
153+
{
154+
move => C__S. rewrite /hsat2.
155+
exists (fun t : trace__T => (τ__π (beh__S (plug__S P1 C__S)) t)),
156+
(fun t : trace__T => (τ__π (beh__S (plug__S P2 C__S)) t)).
157+
simpl.
158+
rewrite !Hrefl.
159+
repeat split; auto.
160+
by exists C__S.
161+
}
162+
move: (Hσpres P1 P2 _ Hfoo Ct). move => [Cs H].
163+
exists Cs.
164+
by inversion H.
165+
Qed.
166+
167+
168+
End Robust2relHCrit.

‎Robust2relHyperProperty.v

+116
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,116 @@
1+
From mathcomp Require Import all_ssreflect.
2+
3+
Set Implicit Arguments.
4+
Unset Printing Implicit Defensive.
5+
6+
Require Import ClassicalExtras.
7+
Require Import MyNotation.
8+
Require Import Setoid.
9+
Require Import FunctionalExtensionality.
10+
11+
Require Import Galois.
12+
Require Import LanguageModel.
13+
Require Import TraceModel.
14+
Require Import Properties.
15+
Require Import ChainModel.
16+
Require Import RobustTraceProperty.
17+
18+
Require Import PropExtensionality.
19+
Definition prop_extensionality := propositional_extensionality.
20+
21+
Section Robust2relHyperPreservation.
22+
23+
24+
Variable Source Target: Language.
25+
Variable compilation_chain : CompilationChain Source Target.
26+
27+
(*CA: we don't need a particular structure of traces to define preservation
28+
e.g. traces = values or our defn of traces both make sense
29+
*)
30+
Variable trace__S trace__T : Type.
31+
32+
Local Definition prop__S := prop trace__S.
33+
Local Definition prop__T := prop trace__T.
34+
35+
Variable Source_Semantics : Semantics Source trace__S.
36+
Variable Target_Semantics : Semantics Target trace__T.
37+
38+
Local Definition sem__S := sem Source_Semantics.
39+
Local Definition sem__T := sem Target_Semantics.
40+
Local Definition beh__S := beh Source_Semantics.
41+
Local Definition beh__T := beh Target_Semantics.
42+
Local Definition par__S := par Source.
43+
Local Definition par__T := par Target.
44+
Local Definition ctx__S := ctx Source.
45+
Local Definition ctx__T := ctx Target.
46+
Local Definition rsat__S := rhsat2 Source_Semantics.
47+
Local Definition rsat__T := rhsat2 Target_Semantics.
48+
49+
Local Definition cmp := compile_par Source Target compilation_chain.
50+
51+
Local Notation "P ↓" := (cmp P) (at level 50).
52+
(* CA: don't understand why this does not work
53+
54+
Local Notation " C [ P ] " := (plug _ P C) (at level 50).
55+
*)
56+
Local Definition plug__S:= plug Source.
57+
Local Definition plug__T := plug Target.
58+
59+
(* still mappings on trace properties *)
60+
Variable σ__π : (trace__T -> Prop) -> (trace__S -> Prop).
61+
Variable τ__π : (trace__S -> Prop) -> (trace__T -> Prop).
62+
63+
Definition σ : (prop__T * prop__T -> Prop) -> (prop__S * prop__S -> Prop) :=
64+
fun T =>
65+
fun Π => exists π__T π__T', fst Π = σ__π π__T /\
66+
snd Π = σ__π π__T' /\
67+
T (π__T, π__T').
68+
69+
Definition τ : (prop__S * prop__S -> Prop) -> (prop__T * prop__T -> Prop) :=
70+
fun S =>
71+
fun Π => exists π__S π__S', fst Π = τ__π π__S /\
72+
snd Π = τ__π π__S' /\
73+
S (π__S, π__S').
74+
75+
76+
Definition σR2hP (P1 P2 : par__S) (H__T : prop__T * prop__T -> Prop) :=
77+
rsat__S P1 P2 (σ H__T) -> rsat__T (P1 ↓) (P2 ↓) H__T.
78+
79+
Definition σR2HP := forall P1 P2 H__T, σR2hP P1 P2 H__T.
80+
81+
Lemma contra_σR2hP (P1 P2 : par__S) (H__T : prop__T * prop__T -> Prop) :
82+
(σR2hP P1 P2 H__T) <-> ((exists C__T, ~ H__T ((beh__T (plug__T (P1 ↓) C__T)), (beh__T (plug__T (P2 ↓) C__T)))) ->
83+
(exists C__S, ~ (σ H__T) ((beh__S ( plug__S P1 C__S)), (beh__S ( plug__S P2 C__S))))).
84+
Proof.
85+
rewrite /σR2hP. by rewrite [_ -> _] contra !neg_rhsat2.
86+
Qed.
87+
88+
Lemma contra_σR2HP :
89+
σR2HP <-> (forall P1 P2 H__T, ((exists C__T, ~ H__T ((beh__T (plug__T (P1 ↓) C__T)), (beh__T (plug__T (P2 ↓) C__T)))) ->
90+
(exists C__S, ~ (σ H__T) ((beh__S ( plug__S P1 C__S)), (beh__S ( plug__S P2 C__S)))))).
91+
Proof.
92+
rewrite /σR2HP.
93+
split => H P1 P2 H__T; by move/contra_σR2hP: (H P1 P2 H__T).
94+
Qed.
95+
96+
Definition τR2hP (P1 P2 : par__S) (H__S : prop__S * prop__S -> Prop) :=
97+
rsat__S P1 P2 H__S -> rsat__T (P1 ↓) (P2 ↓) (τ H__S).
98+
99+
Definition τR2HP := forall P1 P2 H__S, τR2hP P1 P2 H__S.
100+
101+
Lemma contra_τR2hP (P1 P2 : par__S) (H__S : prop__S * prop__S -> Prop) :
102+
(τR2hP P1 P2 H__S) <-> ((exists C__T, ~ (τ H__S) ((beh__T (plug__T (P1 ↓) C__T)), (beh__T (plug__T (P2 ↓) C__T)))) ->
103+
(exists C__S, ~ H__S ((beh__S (plug__S P1 C__S)), (beh__S (plug__S P2 C__S))))).
104+
Proof.
105+
rewrite /τR2hP. by rewrite [_ -> _] contra !neg_rhsat2.
106+
Qed.
107+
108+
Lemma contra_τRHP :
109+
τR2HP <-> (forall P1 P2 H__S, ((exists C__T, ~ (τ H__S) ((beh__T (plug__T (P1 ↓) C__T)), (beh__T (plug__T (P2 ↓) C__T)))) ->
110+
(exists C__S, ~ H__S ((beh__S (plug__S P1 C__S)), (beh__S (plug__S P2 C__S)))))).
111+
Proof.
112+
rewrite /τR2HP.
113+
split => H P1 P2 H__S; by move/contra_τR2hP: (H P1 P2 H__S).
114+
Qed.
115+
116+
End Robust2relHyperPreservation.

‎_CoqProject

+3-1
Original file line numberDiff line numberDiff line change
@@ -36,13 +36,15 @@ RobustSSCHPreservation.v
3636
RobustSSCHCriterion.v
3737
RobustHyperSafetyPreservation.v
3838
RobustHyperSafetyCriterion.v
39+
Robust2relSafetyCriterion.v
40+
Robust2relHyperCriterion.v
3941

4042
Robust2relTraceProperty.v
4143
Robust2relTraceCriterion.v
4244
Robust2relSSCHPreservation.v
4345
Robust2relSSCHCriterion.v
4446
Robust2relSafetyProperty.v
45-
Robust2relSafetyCriterion.v
47+
Robust2relHyperProperty.v
4648

4749
ResourceExhaustion.v
4850

0 commit comments

Comments
 (0)