-
Notifications
You must be signed in to change notification settings - Fork 0
/
SSNICheckerProofs.v
182 lines (154 loc) · 6.65 KB
/
SSNICheckerProofs.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
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
Require Import Coq.Strings.String.
Require Import Arith.EqNat.
Require Import ZArith.
Require Import Machine.
Require Import QuickChick EndToEnd SetOfOutcomes.
Require Import Common.
Require Import Printing.
Require Import Shrinking.
Require Import Generation.
Require Import Indist.
Require Import SSNI.
Require Import ssreflect ssrbool eqtype.
Require Import Show.
(* Possible steps according to SSNI_helper*)
(*
L -> s1'
| | final states indistinguishable
L -> s2'
L -> s1'
|
L -> x no step for the second state
H -> L
| | final states indistinguishable
H -> L
H -> L
| no condition here. Seems a bit strange.
H -> H
H -> H high to high step. Requires no trace and the states before and
after to be indistinguishable
*)
Definition propSSNI_prop (t : table) (v : Variation) : Prop :=
let '(Var lab st1 st2) := v in
(indist lab st1 st2) ->
(is_low_state st1 lab /\ (forall tr1 st1' tr2 st2',
fstep t st1 = Some (tr1, st1') ->
fstep t st2 = Some (tr2, st2') ->
observe_comp (observe lab tr1) (observe lab tr2) /\
(indist lab st1' st2'))) \/
(~~ is_low_state st1 lab /\ (forall tr1 st1',
fstep t st1 = Some (tr1, st1') ->
((is_low_state st1' lab /\
forall tr2 st2',
fstep t st2 = Some (tr2, st2') ->
is_low_state st2' lab ->
observe_comp (observe lab tr1) (observe lab tr2) /\
(indist lab st1' st2')) \/
(~~ is_low_state st1' lab /\
List.length (observe lab tr1) = 0%nat /\
indist lab st1 st1')))).
Definition propSSNI_bool (t : table) (v : Variation) : bool :=
let '(Var lab st1 st2) := v in
if indist lab st1 st2 then
match fstep t st1 with
| Some (tr1, st1') =>
if is_low_state st1 lab then
match fstep t st2 with
| Some (tr2, st2') =>
(observe_comp (observe lab tr1) (observe lab tr2)
&& (indist lab st1' st2'))
| _ => true
end
else (* is_high st1 *)
if is_low_state st1' lab then
match fstep t st2 with
| Some (tr2, st2') =>
if is_low_state st2' lab then
observe_comp (observe lab tr1) (observe lab tr2)
&& (indist lab st1' st2')
else true
| _ => true
end
else
beq_nat (List.length (observe lab tr1)) 0
&& indist lab st1 st1'
| _ => true
end
else true.
Lemma ssniP:
forall (t : table) v,
reflect (propSSNI_prop t v) (propSSNI_bool t v).
Proof.
move=> t [lab st1 st2]. apply/(@iffP (propSSNI_bool t (Var lab st1 st2))); try (by apply idP);
rewrite /propSSNI_bool /propSSNI_prop.
{ destruct (indist lab st1 st2) => //.
destruct (fstep t st1) as [ [tr1' st1'] |].
- destruct (is_low_state st1 lab).
+ destruct (fstep t st2) as [ [tr2' st2'] |];
move => H _; left; split => //.
move=> tr1_ st1'_ st2_ st2'_ [eq1 eq2] [eq3 eq4]; subst.
by apply/andP.
+ move => H _. right. split => //.
move=> tr1_ st1'_ [eq1 eq2]; subst.
destruct (fstep t st2) as [[tr2' st2'] |].
* destruct (is_low_state st1'_ lab).
left. split => //. move => tr2_ st2'_ [eq1 eq2] H'; subst.
destruct (is_low_state st2'_ lab); try congruence.
by apply/andP.
right. split=> //. move : H => /andP [H1 H2]. split => //.
by apply beq_nat_eq.
* destruct (is_low_state st1'_ lab). left. by split => //.
right. split => //. move : H => /andP [H1 H2]. split => //.
by apply beq_nat_eq.
- move=> _ _. destruct (is_low_state st1 lab).
+ left. split => //.
+ right. split => //. }
{ destruct (indist lab st1 st2) => //. move => /(_ is_true_true) H.
move: H => [[H1 H2] | [H1 H2]].
- rewrite H1. destruct (fstep t st1) as [ [tr1' st1'] |] => //.
destruct (fstep t st2) as [ [tr2' st2'] |] => //.
apply/andP. by auto.
- apply Bool.negb_true_iff in H1. rewrite H1.
destruct (fstep t st1) as [ [tr1' st1'] |] => //.
move : H2 => /(_ _ _ Logic.eq_refl) [[H2 H3] | [H2 [H3 H4]]].
+ rewrite H2. destruct (fstep t st2) as [ [tr2' st2'] |] => //.
move: H3 => /(_ _ _ Logic.eq_refl) H3.
destruct (is_low_state st2' lab) => //. apply/andP; by auto.
+ apply Bool.negb_true_iff in H2. rewrite H2.
apply/andP. split => //. by apply beq_nat_true_iff in H3. }
Qed.
Lemma propSSNI_helper_equiv:
forall (t : table) v,
semProperty (@propSSNI_helper Pred _ t v) <-> propSSNI_prop t v.
Proof.
move=> t [lab st1 st2]. split; [move => H; apply/ssniP| move=> /ssniP H];
rewrite /propSSNI_helper /propSSNI_bool /semTestable semCollect_id in H *.
- move=> /semPredQProp H. destruct (indist lab st1 st2) => //.
{ destruct (fstep t st1) as [ [tr1' st1'] |] => //.
destruct (is_low_state st1 lab).
- destruct (fstep t st2) as [ [tr2' st2'] |] => //.
by move/semCollect_id(*/semPredQProp
/semWhenFail_id*)/semBool : H => H.
- destruct (is_low_state st1').
+ destruct (fstep t st2) as [[tr2 st2'] |] => //.
destruct (is_low_state st2' lab).
by move/semCollect_id(*/semPredQProp/semWhenFail_id*)/semBool : H.
by move/semCollect_id/semPredQProp/semBool : H.
+ by move/semCollect_id(*/semPredQProp/semWhenFail_id*)/semBool : H. }
- move=> H.
destruct (indist lab st1 st2);
try by apply/semPredQProp/semCollect_id/semPredQProp/semBool.
{ destruct (fstep t st1) as [ [tr1' st1'] |].
destruct (is_low_state st1 lab).
- destruct (fstep t st2) as [ [tr2' st2'] |].
by apply/semPredQProp/semCollect_id(*/semPredQProp/semWhenFail_id*)/semBool.
by apply/semPredQProp/semCollect_id/semPredQProp/semBool.
- destruct (is_low_state st1').
+ destruct (fstep t st2) as [[tr2 st2'] |].
* destruct (is_low_state st2' lab).
by apply/semPredQProp/semCollect_id(*/semPredQProp/semWhenFail_id*)/semBool.
by apply/semPredQProp/semCollect_id/semPredQProp/semBool.
* by apply/semPredQProp/semCollect_id/semPredQProp/semBool.
+ by apply/semPredQProp/semCollect_id(*/semPredQProp/semWhenFail_id*)/semBool.
- by apply/semPredQProp/semCollect_id/semPredQProp/semBool. }
Qed.