-
Notifications
You must be signed in to change notification settings - Fork 0
/
logic.mlw
160 lines (129 loc) · 6.44 KB
/
logic.mlw
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
(* Program logic (hoare logic + weakest preconditions) over
Virtual Machine language. *)
module Compiler_logic
use int.Int
use list.List
use list.Length
use list.Append
use vm.Vm
use state.State
function fst (p: ('a,'b)) : 'a = let (x,_) = p in x
meta rewrite_def function fst
function snd (p: ('a,'b)) : 'b = let (_,y) = p in y
meta rewrite_def function snd
predicate (-->) (x y:'a) = [@rewrite] x = y
meta rewrite_def predicate (-->)
(* Unary predicates over machine states *)
type pred = machine_state -> bool
(* Binary predicates over machine states *)
type rel = machine_state -> pred
(* pre/post-conditions types, as parameterized unary/binary predicates.
'a represents auxiliary variables
pos is an auxiliary variable representing the absolute position at which
the code is loaded. *)
type pre 'a = 'a -> pos -> pred
type post 'a = 'a -> pos -> rel
(* Machine transition valid whatever the global code is. *)
predicate contextual_irrelevance (c:code) (p:pos) (ms1 ms2:machine_state) =
forall c_glob. codeseq_at c_glob p c -> transition_star c_glob ms1 ms2
(* Hoare triples with explicit pre & post *)
type hl 'a = { code: code; ghost pre : pre 'a; ghost post: post 'a }
(* (Total) correctness for hoare triple. *)
invariant { forall x:'a,p ms. pre x p ms ->
exists ms'. post x p ms ms' /\ contextual_irrelevance code p ms ms' }
by { code = Nil; pre = (fun _ _ _ -> false); post = fun _ _ _ _ -> true }
(* Predicate transformer type. Same auxiliary variables as for
Hoare triples. *)
type wp_trans 'a = 'a -> pos -> pred -> pred
(* Code with backward predicate transformer. *)
type wp 'a = { wcode : code; ghost wp : wp_trans 'a }
(* Similar invariant for backward predicate transformers *)
invariant { forall x:'a,p post ms. wp x p post ms ->
exists ms'. post ms' /\ contextual_irrelevance wcode p ms ms' }
by { wcode = Nil; wp = fun _ _ _ _ -> false }
(* WP combinator for sequence. Similar to the standard WP calculus
for sequence. The initial machine state is memorized in auxiliary
variables for potential use in the second code specification. *)
function seq_wp
(l1:int) (w1:wp_trans 'a) (w2:wp_trans ('a,machine_state)) : wp_trans 'a =
fun x p q ms -> w1 x p (w2 (x,ms) (p+l1) q) ms
lemma seq_wp_lemma: [@rewrite] forall l1,w1: wp_trans 'a,w2 x p q ms.
seq_wp l1 w1 w2 x p q ms = w1 x p (w2 (x,ms) (p+l1) q) ms
(* Code combinator for sequence, with wp. *)
let (--) (s1 : wp 'a) (s2 : wp ('a, machine_state)) : wp 'a
ensures { result.wcode.length --> s1.wcode.length + s2.wcode.length }
ensures { result.wp --> seq_wp s1.wcode.length s1.wp s2.wp }
= let code = s1.wcode ++ s2.wcode in
let res = { wcode = code; wp = seq_wp s1.wcode.length s1.wp s2.wp } in
assert { forall x: 'a, p post ms. res.wp x p post ms ->
not (exists ms'. post ms' /\ contextual_irrelevance res.wcode p ms ms') ->
(forall ms'. s2.wp (x,ms) (p + s1.wcode.length) post ms' /\
contextual_irrelevance res.wcode p ms ms' -> false) && false };
res
function fork_wp (w:wp_trans 'a) (cond:pre 'a) : wp_trans 'a =
fun x p q ms -> if cond x p ms then w x p q ms else q ms
lemma fork_wp_lemma: [@rewrite] forall w:wp_trans 'a,cond x p q ms.
fork_wp w cond x p q ms =
((not cond x p ms -> q ms) /\ (cond x p ms -> w x p q ms))
(* Code combinator for conditional execution.
Similar to WP calculus for (if cond then s). *)
let (%) (s:wp 'a) (ghost cond:pre 'a) : wp 'a
ensures { result.wp --> fork_wp s.wp cond }
ensures { result.wcode.length --> s.wcode.length }
= { wcode = s.wcode; wp = fork_wp s.wp cond }
(* WP transformer for hoare triples. *)
function towp_wp (pr:pre 'a) (ps:post 'a) : wp_trans 'a =
fun x p q ms -> pr x p ms && (forall ms'. ps x p ms ms' -> q ms')
lemma towp_wp_lemma: [@rewrite]
forall pr ps, x:'a, p q ms. towp_wp pr ps x p q ms =
(pr x p ms && (forall ms'. ps x p ms ms' -> q ms'))
(* Unwrap code with hoare triple into code with wp.
Analogous to procedure call/abstract block. *)
let ($_) (c:hl 'a) : wp 'a
ensures { result.wcode.length --> c.code.length }
ensures { result.wp --> towp_wp c.pre c.post }
= { wcode = c.code; wp = towp_wp c.pre c.post }
(* Equip code with pre/post-condition. That is here that proof happen.
(P -> wp (c,Q)). Anologous to checking function/abstract block
specification. *)
let hoare (ghost pre:pre 'a) (c:wp 'a) (ghost post:post 'a) : hl 'a
requires { forall x p ms. pre x p ms -> (c.wp x p (post x p ms)) ms }
ensures { result.pre --> pre }
ensures { result.post --> post }
ensures { result.code.length --> c.wcode.length }
= { code = c.wcode ; pre = pre; post = post }
function trivial_pre: pre 'a = fun _ p ms -> let VMS p' _ _ _ = ms in p = p'
meta rewrite_def function trivial_pre
(* Accessibility predicate. *)
inductive acc ('a -> 'a -> bool) 'a =
| Acc : forall r, x:'a. (forall y. r y x -> acc r y) -> acc r x
(* Utility: some flavor of conjonction. *)
function pconj (p1:pred) (x:machine_state)
(p2:machine_state -> pred) : pred =
fun y -> p1 y && p2 y x
lemma pconj_lemma:[@rewrite] forall p1 x p2 y. pconj p1 x p2 y <-> p1 y && p2 y x
(* WP combinator for looping construction. Similar to weakest precondition
for while loops. *)
function loop_wp (w:wp_trans 'a) (inv cont:pre 'a)
(var:post 'a) : wp_trans 'a =
fun x p q ms -> inv x p ms && acc (var x p) ms && forall ms'. inv x p ms' ->
if cont x p ms'
then w x p (pconj (inv x p) ms' (var x p)) ms'
else w x p q ms'
lemma loop_wp_lemma: [@rewrite] forall w:wp_trans 'a,inv cont var x p q ms.
loop_wp w inv cont var x p q ms <->
inv x p ms && acc (var x p) ms && forall ms'. inv x p ms' ->
(cont x p ms' -> w x p (pconj (inv x p) ms' (var x p)) ms')
/\ (not cont x p ms' -> w x p q ms')
(* Code combinator for looping construct. *)
let make_loop (c:wp 'a) (ghost inv cont:pre 'a)
(ghost var:post 'a) : wp 'a
ensures { result.wp --> loop_wp c.wp inv cont var }
ensures { result.wcode.length --> c.wcode.length }
= let ghost wpt = loop_wp c.wp inv cont var in
assert { forall x p q ms0. wpt x p q ms0 ->
forall ms. inv x p ms -> acc (var x p) ms ->
exists ms'. contextual_irrelevance c.wcode p ms ms' /\ q ms'
};
{ wcode = c.wcode; wp = wpt }
end