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
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
|
(** [betree_main]: templates for the decreases clauses *)
module BetreeMain.Clauses
open Primitives
open BetreeMain.Types
#set-options "--z3rlimit 50 --fuel 0 --ifuel 1"
(*** Well-founded relations *)
(* We had a few issues when proving termination of the mutually recursive functions:
* - betree_internal_flush
* - betree_node_apply_messages
*
* The quantity which effectively decreases is:
* (betree_size, messages_length)
* where messages_length is 0 when there are no messages
* (and where we use the lexicographic ordering, of course)
*
* However, the `%[...]` and `{:well-founded ...} notations are not available outside
* of `decrease` clauses.
*
* We thus resorted to writing and proving correct a well-founded relation over
* pairs of natural numbers. The trick is that `<<` can be used outside of decrease
* clauses, and can be used to trigger SMT patterns.
*
* What follows is adapted from:
* https://www.fstar-lang.org/tutorial/book/part2/part2_well_founded.html
*
* Also, the following PR might make things easier:
* https://github.com/FStarLang/FStar/pull/2561
*)
module P = FStar.Preorder
module W = FStar.WellFounded
module L = FStar.LexicographicOrdering
let lt_nat (x y:nat) : Type = x < y == true
let rec wf_lt_nat (x:nat)
: W.acc lt_nat x
= W.AccIntro (fun y _ -> wf_lt_nat y)
// A type abbreviation for a pair of nats
let nat_pair = (x:nat & nat)
// Making a lexicographic ordering from a pair of nat ordering
let lex_order_nat_pair : P.relation nat_pair =
L.lex_t lt_nat (fun _ -> lt_nat)
// The lex order on nat pairs is well-founded, using our general proof
// of lexicographic composition of well-founded orders
let lex_order_nat_pair_wf : W.well_founded lex_order_nat_pair =
L.lex_t_wf wf_lt_nat (fun _ -> wf_lt_nat)
// A utility to introduce lt_nat
let mk_lt_nat (x:nat) (y:nat { x < y }) : lt_nat x y =
let _ : equals (x < y) true = Refl in
()
// A utility to make a lex ordering of nat pairs
let mk_lex_order_nat_pair (xy0:nat_pair)
(xy1:nat_pair {
let (|x0, y0|) = xy0 in
let (|x1, y1|) = xy1 in
x0 < x1 \/ (x0 == x1 /\ y0 < y1)
}) : lex_order_nat_pair xy0 xy1 =
let (|x0, y0|) = xy0 in
let (|x1, y1|) = xy1 in
if x0 < x1 then L.Left_lex x0 x1 y0 y1 (mk_lt_nat x0 x1)
else L.Right_lex x0 y0 y1 (mk_lt_nat y0 y1)
let rec coerce #a #r #x (p:W.acc #a r x) : Tot (W.acc r x) (decreases p) =
W.AccIntro (fun y r -> coerce (p.access_smaller y r))
let coerce_wf #a #r (p: (x:a -> W.acc r x)) : x:a -> W.acc r x =
fun x -> coerce (p x)
(* We need this axiom, which comes from the following discussion:
* https://github.com/FStarLang/FStar/issues/1916
* An issue here is that the `{well-founded ... }` notation
*)
assume
val axiom_well_founded (a : Type) (rel : a -> a -> Type0)
(rwf : W.well_founded #a rel) (x y : a) :
Lemma (requires (rel x y)) (ensures (x << y))
(* This lemma has a pattern (which makes it work) *)
let wf_nat_pair_lem (p0 p1 : nat_pair) :
Lemma
(requires (
let (|x0, y0|) = p0 in
let (|x1, y1|) = p1 in
x0 < x1 || (x0 = x1 && y0 < y1)))
(ensures (p0 << p1))
[SMTPat (p0 << p1)] =
let rel = lex_order_nat_pair in
let rel_wf = lex_order_nat_pair_wf in
let _ = mk_lex_order_nat_pair p0 p1 in
assert(rel p0 p1);
axiom_well_founded nat_pair rel rel_wf p0 p1
(*** Decrease clauses *)
/// "Standard" decrease clauses
(** [betree_main::betree::List::{1}::len]: decreases clause *)
unfold
let betree_list_len_decreases (t : Type0) (self : betree_list_t t) : betree_list_t t =
self
(** [betree_main::betree::List::{1}::split_at]: decreases clause *)
unfold
let betree_list_split_at_decreases (t : Type0) (self : betree_list_t t)
(n : u64) : nat =
n
(** [betree_main::betree::List::{2}::partition_at_pivot]: decreases clause *)
unfold
let betree_list_partition_at_pivot_decreases (t : Type0)
(self : betree_list_t (u64 & t)) (pivot : u64) : betree_list_t (u64 & t) =
self
(** [betree_main::betree::Node::{5}::lookup_in_bindings]: decreases clause *)
unfold
let betree_node_lookup_in_bindings_decreases (key : u64)
(bindings : betree_list_t (u64 & u64)) : betree_list_t (u64 & u64) =
bindings
(** [betree_main::betree::Node::{5}::lookup_first_message_for_key]: decreases clause *)
unfold
let betree_node_lookup_first_message_for_key_decreases (key : u64)
(msgs : betree_list_t (u64 & betree_message_t)) : betree_list_t (u64 & betree_message_t) =
msgs
(** [betree_main::betree::Node::{5}::apply_upserts]: decreases clause *)
unfold
let betree_node_apply_upserts_decreases
(msgs : betree_list_t (u64 & betree_message_t)) (prev : option u64)
(key : u64) (st : state) : betree_list_t (u64 & betree_message_t) =
msgs
(** [betree_main::betree::Internal::{4}::lookup_in_children]: decreases clause *)
unfold
let betree_internal_lookup_in_children_decreases (self : betree_internal_t)
(key : u64) (st : state) : betree_internal_t =
self
(** [betree_main::betree::Node::{5}::lookup]: decreases clause *)
unfold
let betree_node_lookup_decreases (self : betree_node_t) (key : u64)
(st : state) : betree_node_t =
self
(** [betree_main::betree::Node::{5}::lookup_mut_in_bindings]: decreases clause *)
unfold
let betree_node_lookup_mut_in_bindings_decreases (key : u64)
(bindings : betree_list_t (u64 & u64)) : betree_list_t (u64 & u64) =
bindings
unfold
let betree_node_apply_messages_to_leaf_decreases
(bindings : betree_list_t (u64 & u64))
(new_msgs : betree_list_t (u64 & betree_message_t)) : betree_list_t (u64 & betree_message_t) =
new_msgs
(** [betree_main::betree::Node::{5}::filter_messages_for_key]: decreases clause *)
unfold
let betree_node_filter_messages_for_key_decreases (key : u64)
(msgs : betree_list_t (u64 & betree_message_t)) : betree_list_t (u64 & betree_message_t) =
msgs
(** [betree_main::betree::Node::{5}::lookup_first_message_after_key]: decreases clause *)
unfold
let betree_node_lookup_first_message_after_key_decreases (key : u64)
(msgs : betree_list_t (u64 & betree_message_t)) : betree_list_t (u64 & betree_message_t) =
msgs
let betree_node_apply_messages_to_internal_decreases
(msgs : betree_list_t (u64 & betree_message_t))
(new_msgs : betree_list_t (u64 & betree_message_t)) : betree_list_t (u64 & betree_message_t) =
new_msgs
(*** Decrease clauses - nat_pair *)
/// The following decrease clauses use the [nat_pair] definition and the well-founded
/// relation proven above.
let rec betree_size (bt : betree_node_t) : nat =
match bt with
| BetreeNodeInternal node -> 1 + betree_internal_size node
| BetreeNodeLeaf _ -> 1
and betree_internal_size (node : betree_internal_t) : nat =
1 + betree_size node.betree_internal_left + betree_size node.betree_internal_right
let rec betree_list_len (#a : Type0) (ls : betree_list_t a) : nat =
match ls with
| BetreeListCons _ tl -> 1 + betree_list_len tl
| BetreeListNil -> 0
(** [betree_main::betree::Internal::{4}::flush]: decreases clause *)
unfold
let betree_internal_flush_decreases (self : betree_internal_t)
(params : betree_params_t) (node_id_cnt : betree_node_id_counter_t)
(content : betree_list_t (u64 & betree_message_t)) (st : state) : nat_pair =
(|betree_internal_size self, 0|)
(** [betree_main::betree::Node::{5}::apply_messages]: decreases clause *)
unfold
let betree_node_apply_messages_decreases (self : betree_node_t)
(params : betree_params_t) (node_id_cnt : betree_node_id_counter_t)
(msgs : betree_list_t (u64 & betree_message_t)) (st : state) : nat_pair =
(|betree_size self, betree_list_len msgs|)
|
