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
|
From QuickChick Require Import QuickChick.
Require Import ZArith.
Require Import List.
From QuickChick.ifcbasic Require Import Machine.
(* Manual, handwritten indist instances *)
Fixpoint forallb2 {A : Type} (f : A -> A -> bool) (l1 l2 :list A) : bool :=
match l1, l2 with
| nil, nil => true
| cons h1 t1, cons h2 t2 => f h1 h2 && forallb2 f t1 t2
| _, _ => false
end.
(* Indistinguishability type class *)
Class Indist (A : Type) : Type :=
{
indist : A -> A -> bool
}.
#[global]
Instance indist_atom : Indist Atom :=
{|
indist a1 a2 :=
let '(x1@l1) := a1 in
let '(x2@l2) := a2 in
match l1, l2 with
| L, L => Z.eqb x1 x2
| H, H => true
| _, _ => false
end
|}.
#[global]
Instance indist_mem : Indist Mem :=
{|
indist m1 m2 := forallb2 indist m1 m2
|}.
Fixpoint cropTop (s:Stack) : Stack :=
match s with
| Mty => Mty
| x::s' => cropTop s'
| (x@H:::s') => cropTop s'
| (_@L:::_) => s
end.
(* Assumes stacks have been cropTopped! *)
#[global]
Instance indist_stack : Indist Stack :=
{|
indist s1 s2 :=
let fix aux s1 s2 :=
match s1, s2 with
| a1::s1', a2::s2' => indist a1 a2 && aux s1' s2'
| a1:::s1', a2:::s2' => indist a1 a2 && aux s1' s2'
| Mty, Mty => true
| _, _ => false
end
in aux s1 s2
|}.
#[global]
Instance indist_state : Indist State :=
{|
indist st1 st2 :=
let '(St imem1 mem1 stk1 pc1) := st1 in
let '(St imem2 mem2 stk2 pc2) := st2 in
if negb (indist mem1 mem2) then (* trace "Memory" *) false
else if negb (indist pc1 pc2) then (* trace "PC" *) false
else let (stk1',stk2') :=
match pc1 with
| _ @ H => (cropTop stk1, cropTop stk2)
| _ => (stk1, stk2)
end in
if negb (indist stk1' stk2') then (* trace "Stack" *) false
else true
|}.
(* Inductive versions *)
Inductive IndistAtom : Atom -> Atom -> Prop :=
| IAtom_Lo : forall x, IndistAtom (x@L) (x@L)
| IAtom_Hi : forall x y, IndistAtom (x@H) (y@H).
Derive DecOpt for (IndistAtom a1 a2).
Inductive IndistMem : Mem -> Mem -> Prop :=
| IMem_Nil : IndistMem nil nil
| IMem_Cons : forall a1 a2 m1 m2,
IndistAtom a1 a2 -> IndistMem m1 m2 ->
IndistMem (cons a1 m1) (cons a2 m2).
Derive DecOpt for (IndistMem m1 m2).
Inductive IndistStack : Stack -> Stack -> Prop :=
| IStack_Mty : IndistStack Mty Mty
| IStack_Cons : forall a1 a2 s1 s2,
IndistAtom a1 a2 -> IndistStack s1 s2 ->
IndistStack (Cons a1 s1) (Cons a2 s2)
| IStack_RetCons : forall a1 a2 s1 s2,
IndistAtom a1 a2 -> IndistStack s1 s2 ->
IndistStack (RetCons a1 s1) (RetCons a2 s2).
Derive DecOpt for (IndistStack s1 s2).
#[global] Instance Label_DecEq (l1 l2 : Label) : Dec (l1 = l2).
Proof. dec_eq. Defined.
Inductive IndistState : State -> State -> Prop :=
| IState_Low : forall im1 im2 m1 m2 s1 s2 pc1 pc2,
IndistAtom pc1 pc2 ->
IndistMem m1 m2 ->
pc_lab pc1 = L ->
IndistStack s1 s2 ->
IndistState (St im1 m1 s1 pc1) (St im2 m2 s2 pc2)
| IState_High : forall im1 im2 m1 m2 s1 s2 pc1 pc2,
IndistAtom pc1 pc2 ->
IndistMem m1 m2 ->
pc_lab pc1 = H ->
IndistStack (cropTop s1) (cropTop s2) ->
IndistState (St im1 m1 s1 pc1) (St im2 m2 s2 pc2).
Derive DecOpt for (IndistState s1 s2).
|
