summaryrefslogtreecommitdiff
path: root/tests/betree
diff options
context:
space:
mode:
authorSon Ho2022-05-09 11:07:44 +0200
committerSon Ho2022-05-09 11:07:44 +0200
commit0191a1196d48e819c834687dc8a6710651ebe76a (patch)
tree6f49fbda23d2824cfe053158b27738400c9eda1d /tests/betree
parent7dce6eaffaa4169fab822d833e32b593ad867588 (diff)
Update the termination proofs of the betree
Diffstat (limited to 'tests/betree')
-rw-r--r--tests/betree/BetreeMain.Clauses.fst120
-rw-r--r--tests/betree/BetreeMain.Funs.fst16
2 files changed, 110 insertions, 26 deletions
diff --git a/tests/betree/BetreeMain.Clauses.fst b/tests/betree/BetreeMain.Clauses.fst
index 8fb43e07..0006e3ac 100644
--- a/tests/betree/BetreeMain.Clauses.fst
+++ b/tests/betree/BetreeMain.Clauses.fst
@@ -5,6 +5,100 @@ 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
+ *)
+
+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 =
@@ -82,18 +176,10 @@ let betree_node_apply_messages_to_internal_decreases
(new_msgs : betree_list_t (u64 & betree_message_t)) : betree_list_t (u64 & betree_message_t) =
new_msgs
-(* This is annoying, we can't use the following trick when defining decrease
- * clauses as separate functions:
- * [https://github.com/FStarLang/FStar/issues/138]
- *
- * Note that 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)
- *
- * For now, we "patch" the code directly (we need to find a better way...)
- *)
+(*** 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
@@ -107,18 +193,16 @@ let rec betree_list_len (#a : Type0) (ls : betree_list_t a) : nat =
| 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 =
- admit ()
+ (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 =
- admit ()
-*)
+ (msgs : betree_list_t (u64 & betree_message_t)) (st : state) : nat_pair =
+ (|betree_size self, betree_list_len msgs|)
diff --git a/tests/betree/BetreeMain.Funs.fst b/tests/betree/BetreeMain.Funs.fst
index d2f63634..b11ca399 100644
--- a/tests/betree/BetreeMain.Funs.fst
+++ b/tests/betree/BetreeMain.Funs.fst
@@ -1173,8 +1173,8 @@ let rec betree_internal_flush_fwd
(node_id_cnt : betree_node_id_counter_t)
(content : betree_list_t (u64 & betree_message_t)) (st : state) :
Tot (result (state & (betree_list_t (u64 & betree_message_t))))
- (decreases %[betree_internal_size self; 0])
- //(decreases (betree_internal_flush_decreases self params node_id_cnt content st))
+ (decreases (betree_internal_flush_decreases self params node_id_cnt content
+ st))
=
begin match
betree_list_partition_at_pivot_fwd betree_message_t content
@@ -1241,8 +1241,8 @@ and betree_internal_flush_back
(node_id_cnt : betree_node_id_counter_t)
(content : betree_list_t (u64 & betree_message_t)) (st : state) :
Tot (result (betree_internal_t & betree_node_id_counter_t))
- (decreases %[betree_internal_size self; 0])
- //(decreases (betree_internal_flush_decreases self params node_id_cnt content st))
+ (decreases (betree_internal_flush_decreases self params node_id_cnt content
+ st))
=
begin match
betree_list_partition_at_pivot_fwd betree_message_t content
@@ -1305,8 +1305,8 @@ and betree_node_apply_messages_fwd
(node_id_cnt : betree_node_id_counter_t)
(msgs : betree_list_t (u64 & betree_message_t)) (st : state) :
Tot (result (state & unit))
- (decreases %[betree_size self; betree_list_len msgs])
-// (decreases (betree_node_apply_messages_decreases self params node_id_cnt msgs st))
+ (decreases (betree_node_apply_messages_decreases self params node_id_cnt msgs
+ st))
=
begin match self with
| BetreeNodeInternal node ->
@@ -1400,8 +1400,8 @@ and betree_node_apply_messages_back
(node_id_cnt : betree_node_id_counter_t)
(msgs : betree_list_t (u64 & betree_message_t)) (st : state) :
Tot (result (betree_node_t & betree_node_id_counter_t))
- (decreases %[betree_size self; betree_list_len msgs])
-// (decreases (betree_node_apply_messages_decreases self params node_id_cnt msgs st))
+ (decreases (betree_node_apply_messages_decreases self params node_id_cnt msgs
+ st))
=
begin match self with
| BetreeNodeInternal node ->