diff options
author | Son Ho | 2022-05-09 11:07:44 +0200 |
---|---|---|
committer | Son Ho | 2022-05-09 11:07:44 +0200 |
commit | 0191a1196d48e819c834687dc8a6710651ebe76a (patch) | |
tree | 6f49fbda23d2824cfe053158b27738400c9eda1d /tests/betree | |
parent | 7dce6eaffaa4169fab822d833e32b593ad867588 (diff) |
Update the termination proofs of the betree
Diffstat (limited to 'tests/betree')
-rw-r--r-- | tests/betree/BetreeMain.Clauses.fst | 120 | ||||
-rw-r--r-- | tests/betree/BetreeMain.Funs.fst | 16 |
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 -> |