forked from jepsen-io/elle
-
Notifications
You must be signed in to change notification settings - Fork 0
/
Observation.thy
161 lines (114 loc) · 7.42 KB
/
Observation.thy
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
theory Observation
imports Main History
begin
section \<open>Observations\<close>
text \<open>Fundamentally, an observation is a set of objects and observed transactions over them.\<close>
datatype observation = Observation "object set" "otxn set"
text \<open>We define some basic accessors...\<close>
primrec all_otxns :: "observation \<Rightarrow> otxn set" where
"all_otxns (Observation objs txns) = txns"
instantiation observation :: all_objects
begin
primrec all_objects_observation :: "observation \<Rightarrow> object set" where
"all_objects_observation (Observation objs txns) = objs"
instance ..
end
instantiation observation :: all_versions
begin
primrec all_versions_observation :: "observation \<Rightarrow> version set" where
"all_versions_observation (Observation objs txns) = \<Union>{all_versions t | t. t \<in> txns}"
instance ..
end
instantiation observation :: all_oops
begin
primrec all_oops_observation :: "observation \<Rightarrow> oop set" where
"all_oops_observation (Observation objs txns) = \<Union>{all_oops t | t. t \<in> txns}"
instance ..
end
text \<open>A well-formed observation is made up of well-formed objects and transactions, and its
transactions are over those objects.\<close>
primrec wf_observation :: "observation \<Rightarrow> bool" where
"wf_observation (Observation objs txns) =
((\<forall>obj. obj \<in> objs \<longrightarrow> wf_object obj) \<and>
(\<forall>t. t \<in> txns \<longrightarrow> (wf_otxn t \<and> (\<forall>oop. (oop \<in> (all_oops t)) \<longrightarrow>
(\<exists>!obj. (obj \<in> objs) \<and> ((key oop) = (key obj)))))))"
text \<open>We say an observation is compatible with a history via relation m if they have the same
object set, the same number of transactions, and m is a bijective mapping from observed transactions
in the observation to compatible abstract transactions in the history.\<close>
definition is_compatible_observation :: "observation \<Rightarrow> (otxn \<Rightarrow> atxn) \<Rightarrow> history \<Rightarrow> bool" where
"is_compatible_observation obs m h =
((all_objects obs = all_objects h) \<and>
(\<forall>otxn. otxn \<in> (all_otxns obs) \<longrightarrow> (is_compatible_txn otxn (m otxn))))"
section \<open>Interpretations\<close>
text \<open>An interpretation of an observation O is a history H and a bijection M which translates
operations in O to compatible observations in H. Interpretation is a reserved word, so...\<close>
datatype interp = Interp "observation" "(otxn \<Rightarrow> atxn)" "history"
primrec history :: "interp \<Rightarrow> history" where
"history (Interp obs m h) = h"
text \<open>We say f is a total bijection between a and b iff f is bijective and every a maps to a b.
I feel like there should be something for this in Isabelle already but I'm not sure.\<close>
text \<open>Giuliano: you can use the query panel to search for constants or theorems.
Here, look for a constant of the following type: "(_ \<Rightarrow> _) \<Rightarrow> _ set \<Rightarrow> _ set \<Rightarrow> bool", and it will find:\<close>
thm Fun.bij_betw_def \<comment> \<open>That is probably what you wanted\<close>
definition total_bij :: "('a \<Rightarrow> 'b) \<Rightarrow> 'a set \<Rightarrow> 'b set \<Rightarrow> bool" where
"total_bij f as bs \<equiv> ((bij f) \<and> (\<forall>a. (a \<in> as) \<longrightarrow> ((f a) \<in> bs)))"
(* I can't even show this? Really? *)
text \<open>Giuliano: it's because it does not hold :) You forgot to assume that @{term \<open>a \<in> as\<close>}.
It's often a good idea to run nitpick as a first sanity check. Here, it immediately finds a counter-example\<close>
lemma "(total_bij f as bs \<and> (b = (f a))) \<longrightarrow> (b \<in> bs)"
nitpick
apply (simp add:total_bij_def)
apply auto
oops
lemma my_lemma:
assumes "total_bij f as bs" and "b = f a" and "a \<in> as"
shows "(b \<in> bs)" \<comment> \<open>Note that this syntax is better becuase it produces a lemma in rule format, ready to be applied without transformation.\<close>
using assms total_bij_def by fastforce \<comment> \<open>found by sledgehammer in a few seconds\<close>
lemma my_lemma_bad:
"total_bij f as bs \<and> b = f a \<and> a \<in> as \<longrightarrow> b \<in> bs"
using total_bij_def by fastforce
text \<open>Now check what the lemmas looks like with @{command thm}\<close>
thm my_lemma \<comment> \<open>In rule form\<close>
thm my_lemma_bad \<comment> \<open>Not in rule form; cannot be applied directly by generic proof tools like auto\<close>
(* Huh, would have thought this would be easy *)
lemma total_bij_image1: "(total_bij f a b) \<Longrightarrow> ((f`a) = b)"
nitpick \<comment> \<open>Again, nitpick shows that it does not hold\<close>
apply (simp add: total_bij_def)
oops
text \<open>Well-formed interpretations are made up of a well-formed observation, a bijection between
observed and abstract transactions, and a well-formed history, such that the observation and
the history are compatible via that bijection.\<close>
primrec wf_interpretation :: "interp \<Rightarrow> bool" where
"wf_interpretation (Interp obs m h) = ((wf_observation obs) \<and>
(wf_history h) \<and>
(total_bij m (all_otxns obs) (all_atxns h)) \<and>
(is_compatible_observation obs m h))"
text \<open>This lets us talk about corresponding transactions via that bijection m.\<close>
primrec corresponding_atxn :: "interp \<Rightarrow> otxn \<Rightarrow> atxn" where
"corresponding_atxn (Interp obs m h) otxn = (m otxn)"
primrec corresponding_otxn :: "interp \<Rightarrow> atxn \<Rightarrow> otxn" where
"corresponding_otxn (Interp obs m h) atxn = (THE otxn. atxn = m otxn)"
text \<open>These are invertible, thanks to m being bijective.\<close>
lemma "(corresponding_otxn (Interp obs h m) atxn) \<in> (all_otxns obs)"
lemma corresponding_invertible: "(corresponding_otxn i (corresponding_atxn i t)) = t"
oops
section \<open>Recoverability\<close>
text \<open>Recoverability allows us to (in some cases) map a version of some key to a specific
observed transaction which must have produced it. To start, we figure out when a transaction
could have written a particular version of an object: some write resulting in this version of the
object is compatible with a write in the transaction.\<close>
definition could_have_been_written_by :: "object \<Rightarrow> version \<Rightarrow> otxn \<Rightarrow> bool" where
"could_have_been_written_by obj v t \<equiv> (\<exists>aw ow. aw \<in> awrites_of obj v \<and>
ow \<in> all_owrites t \<and>
is_compatible_op ow aw)"
(* might have this wrong *)
lemma "((could_have_been_written_by obj v ot) \<and> (is_compatible_txn ot atxn)) \<longrightarrow>
(\<exists>v0 a r. (AWrite k v0 a v r) \<in> all_awrites atxn)"
oops
text \<open>Given an observation, we say a version v of key k is recoverable to a transaction t if t is
the only transaction which could have written that v of k.\<close>
definition is_recoverable :: "observation \<Rightarrow> key \<Rightarrow> version \<Rightarrow> otxn \<Rightarrow> bool" where
"is_recoverable obs k v ot \<equiv> (let obj = (THE ob. ob \<in> all_objects obs \<and> key ob = k) in
(could_have_been_written_by obj v ot) \<and>
(\<exists>!t. t \<in> all_otxns obs \<and> could_have_been_written_by obj v t))"
end