From c3a6cf2d4fb053752599db1bb97a1854fe0c6ad3 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Guido=20Mart=C3=ADnez?= Date: Tue, 8 Oct 2024 15:10:40 -0700 Subject: [PATCH] ulib: reducing some warnings --- ulib/FStar.Int.fsti | 2 -- ulib/FStar.LexicographicOrdering.fst | 2 +- ulib/FStar.Math.Lemmas.fst | 2 +- ulib/FStar.UInt128.fst | 3 +++ ulib/FStar.WellFounded.Util.fst | 2 +- ulib/FStar.WellFounded.fst | 2 +- ulib/LowStar.BufferView.Down.fst | 12 +++--------- ulib/LowStar.Monotonic.Buffer.fst | 1 + ulib/experimental/FStar.InteractiveHelpers.Base.fst | 2 +- .../FStar.InteractiveHelpers.Effectful.fst | 2 +- .../FStar.InteractiveHelpers.ExploreTerm.fst | 2 +- .../experimental/FStar.InteractiveHelpers.Output.fst | 2 +- .../FStar.InteractiveHelpers.PostProcess.fst | 2 +- .../FStar.InteractiveHelpers.Propositions.fst | 2 +- ulib/experimental/FStar.Sequence.Permutation.fst | 3 +++ 15 files changed, 20 insertions(+), 21 deletions(-) diff --git a/ulib/FStar.Int.fsti b/ulib/FStar.Int.fsti index e96633055bb..eb4ba64e0d1 100644 --- a/ulib/FStar.Int.fsti +++ b/ulib/FStar.Int.fsti @@ -183,8 +183,6 @@ let gte #n (a:int_t n) (b:int_t n) : Tot bool = a >= b let lt #n (a:int_t n) (b:int_t n) : Tot bool = a < b let lte #n (a:int_t n) (b:int_t n) : Tot bool = a <= b -#push-options "--initial_fuel 1 --max_fuel 1" - /// Casts let to_uint (#n:pos) (x:int_t n) : Tot (UInt.uint_t n) = diff --git a/ulib/FStar.LexicographicOrdering.fst b/ulib/FStar.LexicographicOrdering.fst index ba97a583e9a..ef1349c1151 100644 --- a/ulib/FStar.LexicographicOrdering.fst +++ b/ulib/FStar.LexicographicOrdering.fst @@ -17,7 +17,7 @@ *) module FStar.LexicographicOrdering -#push-options "--warn_error -242" //no inner let recs in SMT +#set-options "--warn_error -242" //no inner let recs in SMT open FStar.ReflexiveTransitiveClosure open FStar.WellFounded diff --git a/ulib/FStar.Math.Lemmas.fst b/ulib/FStar.Math.Lemmas.fst index 3dc80828f8b..7f3cbbc03f5 100644 --- a/ulib/FStar.Math.Lemmas.fst +++ b/ulib/FStar.Math.Lemmas.fst @@ -18,7 +18,7 @@ module FStar.Math.Lemmas open FStar.Mul open FStar.Math.Lib -#push-options "--fuel 0 --ifuel 0" +#set-options "--fuel 0 --ifuel 0" (* Lemma: definition of Euclidean division *) let euclidean_div_axiom a b = () diff --git a/ulib/FStar.UInt128.fst b/ulib/FStar.UInt128.fst index 537beb35331..444ce8b0882 100644 --- a/ulib/FStar.UInt128.fst +++ b/ulib/FStar.UInt128.fst @@ -337,6 +337,8 @@ let sub_mod_wrap1_ok a b = () end #pop-options +#pop-options + let sum_lt (a1 a2 b1 b2:nat) : Lemma (requires (a1 + a2 < b1 + b2 /\ a1 >= b1)) @@ -372,6 +374,7 @@ let sub_mod (a b: t) : Pure t else sub_mod_wrap_ok a b); sub_mod_impl a b #pop-options + #restart-solver val shift_bound : #n:nat -> num:UInt.uint_t n -> n':nat -> diff --git a/ulib/FStar.WellFounded.Util.fst b/ulib/FStar.WellFounded.Util.fst index a738123731b..98661a47d84 100644 --- a/ulib/FStar.WellFounded.Util.fst +++ b/ulib/FStar.WellFounded.Util.fst @@ -1,7 +1,7 @@ module FStar.WellFounded.Util open FStar.WellFounded -#push-options "--warn_error -242" //inner let recs not encoded to SMT; ok +#set-options "--warn_error -242" //inner let recs not encoded to SMT; ok let intro_lift_binrel (#a:Type) (r:binrel a) (y:a) (x:a) : Lemma diff --git a/ulib/FStar.WellFounded.fst b/ulib/FStar.WellFounded.fst index 97ee6223a4b..eab78d99e16 100644 --- a/ulib/FStar.WellFounded.fst +++ b/ulib/FStar.WellFounded.fst @@ -22,7 +22,7 @@ module FStar.WellFounded -#push-options "--warn_error -242" //inner let recs not encoded to SMT; ok +#set-options "--warn_error -242" //inner let recs not encoded to SMT; ok let binrel (a:Type) = a -> a -> Type diff --git a/ulib/LowStar.BufferView.Down.fst b/ulib/LowStar.BufferView.Down.fst index 2ce8aee0578..b5ecee6fc50 100644 --- a/ulib/LowStar.BufferView.Down.fst +++ b/ulib/LowStar.BufferView.Down.fst @@ -209,6 +209,7 @@ let sel'_tail #a #b v es i = FStar.Math.Lemmas.lemma_mod_sub i n 1; FStar.Math.Lemmas.add_div_mod_1 j n; assert (j / n == (i / n) - 1) +#pop-options val as_seq'_sel' (#a #b: _) (v:view a b) @@ -220,13 +221,6 @@ val as_seq'_sel' (#a #b: _) sel' v es i == Seq.index (as_seq' es v) i)) (decreases (Seq.length es)) -//flaky -#reset-options -#set-options "--smtencoding.elim_box true" -#set-options "--smtencoding.l_arith_repr native" -#set-options "--smtencoding.nl_arith_repr wrapped" -#set-options "--z3rlimit_factor 10" //just being conservative -#set-options "--initial_fuel 1 --max_fuel 1 --max_ifuel 0" let rec as_seq'_sel' #a #b v es i = as_seq'_len es v; let n : pos = View?.n v in @@ -251,7 +245,6 @@ let rec as_seq'_sel' #a #b v es i = Seq.index (as_seq' as' v) j); sel'_tail v es i end -#reset-options let as_seq_sel #b h vb i = indexing vb i; @@ -349,7 +342,7 @@ let rec upd_seq'_spec (#a #b: _) (v:view a b) (s:Seq.seq b{Seq.length s % View?. assert (es `Seq.equal` Seq.cons (View?.put v pfx) as'); as_seq'_cons v (View?.put v pfx) as' -#set-options "--z3rlimit 20" +#push-options "--z3rlimit 20" let upd_seq_spec (#b: _) (h:HS.mem) (vb:buffer b{live h vb}) (s:Seq.seq b{Seq.length s = length vb}) = let h' = upd_seq h vb s in Math.cancel_mul_mod (B.length (as_buffer vb)) (View?.n (get_view vb)); @@ -367,3 +360,4 @@ let upd_seq_spec (#b: _) (h:HS.mem) (vb:buffer b{live h vb}) (s:Seq.seq b{Seq.le FStar.Classical.forall_intro_2 (fun as1 as2 -> Classical.move_requires (as_seq'_injective v as1) as2 <: Lemma ((as_seq' as1 v `Seq.equal` as_seq' as2 v) ==> (as1 `Seq.equal` as2))) +#pop-options diff --git a/ulib/LowStar.Monotonic.Buffer.fst b/ulib/LowStar.Monotonic.Buffer.fst index dc5596024b2..684ff260f0d 100644 --- a/ulib/LowStar.Monotonic.Buffer.fst +++ b/ulib/LowStar.Monotonic.Buffer.fst @@ -1876,6 +1876,7 @@ let blit #a #rrel1 #rrel2 #rel1 #rel2 src idx_src dst idx_dst len = assert (h1 == g_upd_seq dst (Seq.slice s2' 0 (U32.v length2)) h); g_upd_seq_as_seq dst (Seq.slice s2' 0 (U32.v length2)) h //for modifies clause | _, _ -> () +#pop-options #restart-solver #push-options "--z3rlimit 256 --max_fuel 0 --max_ifuel 1 --initial_ifuel 1 --z3cliopt smt.qi.EAGER_THRESHOLD=4" diff --git a/ulib/experimental/FStar.InteractiveHelpers.Base.fst b/ulib/experimental/FStar.InteractiveHelpers.Base.fst index 902544301c9..ee4baabf472 100644 --- a/ulib/experimental/FStar.InteractiveHelpers.Base.fst +++ b/ulib/experimental/FStar.InteractiveHelpers.Base.fst @@ -4,7 +4,7 @@ open FStar.List.Tot open FStar.Tactics open FStar.Mul -#push-options "--z3rlimit 15 --fuel 0 --ifuel 1" +#set-options "--z3rlimit 15 --fuel 0 --ifuel 1" (*** Utilities *) val bv_eq : bv -> bv -> Tot bool diff --git a/ulib/experimental/FStar.InteractiveHelpers.Effectful.fst b/ulib/experimental/FStar.InteractiveHelpers.Effectful.fst index 7c5fa630a69..301763e6ad6 100644 --- a/ulib/experimental/FStar.InteractiveHelpers.Effectful.fst +++ b/ulib/experimental/FStar.InteractiveHelpers.Effectful.fst @@ -14,7 +14,7 @@ let term_eq = FStar.Reflection.TermEq.Simple.term_eq /// Effectful term analysis: retrieve information about an effectful term, including /// its return type, its arguments, its correctly instantiated pre/postcondition, etc. -#push-options "--z3rlimit 15 --fuel 0 --ifuel 1" +#set-options "--z3rlimit 15 --fuel 0 --ifuel 1" (*** Effectful term analysis *) diff --git a/ulib/experimental/FStar.InteractiveHelpers.ExploreTerm.fst b/ulib/experimental/FStar.InteractiveHelpers.ExploreTerm.fst index 29179443ac9..86795c53b76 100644 --- a/ulib/experimental/FStar.InteractiveHelpers.ExploreTerm.fst +++ b/ulib/experimental/FStar.InteractiveHelpers.ExploreTerm.fst @@ -5,7 +5,7 @@ open FStar.Tactics open FStar.Mul open FStar.InteractiveHelpers.Base -#push-options "--z3rlimit 15 --fuel 0 --ifuel 1" +#set-options "--z3rlimit 15 --fuel 0 --ifuel 1" (*** Types and effects *) /// Define utilities to handle and carry types and effects diff --git a/ulib/experimental/FStar.InteractiveHelpers.Output.fst b/ulib/experimental/FStar.InteractiveHelpers.Output.fst index acdf34a1ee6..2407760edc3 100644 --- a/ulib/experimental/FStar.InteractiveHelpers.Output.fst +++ b/ulib/experimental/FStar.InteractiveHelpers.Output.fst @@ -10,7 +10,7 @@ open FStar.InteractiveHelpers.Propositions /// Facilities to output results to the IDE/emacs/whatever. /// Contains datatypes and functions to carry information. -#push-options "--z3rlimit 15 --fuel 0 --ifuel 1" +#set-options "--z3rlimit 15 --fuel 0 --ifuel 1" (*** Convert terms to string *) /// The important point is to handle variable shadowing properly, so that the diff --git a/ulib/experimental/FStar.InteractiveHelpers.PostProcess.fst b/ulib/experimental/FStar.InteractiveHelpers.PostProcess.fst index fefe2ca91ec..cf8f9122c77 100644 --- a/ulib/experimental/FStar.InteractiveHelpers.PostProcess.fst +++ b/ulib/experimental/FStar.InteractiveHelpers.PostProcess.fst @@ -13,7 +13,7 @@ open FStar.InteractiveHelpers.Output /// information from the context and generate output which can be exploited /// on the IDE side. -#push-options "--z3rlimit 15 --fuel 0 --ifuel 1" +#set-options "--z3rlimit 15 --fuel 0 --ifuel 1" (*** General utilities *) /// We declare some identifiers that we will use to guide the meta processing diff --git a/ulib/experimental/FStar.InteractiveHelpers.Propositions.fst b/ulib/experimental/FStar.InteractiveHelpers.Propositions.fst index d9b94e4b269..c0537d1e81f 100644 --- a/ulib/experimental/FStar.InteractiveHelpers.Propositions.fst +++ b/ulib/experimental/FStar.InteractiveHelpers.Propositions.fst @@ -17,7 +17,7 @@ let term_eq = FStar.Reflection.TermEq.Simple.term_eq /// [> let z = x / y in // term of interest /// [> assert(...); // post assertion -#push-options "--z3rlimit 15 --fuel 0 --ifuel 1" +#set-options "--z3rlimit 15 --fuel 0 --ifuel 1" /// Analyze a term to retrieve its effectful information diff --git a/ulib/experimental/FStar.Sequence.Permutation.fst b/ulib/experimental/FStar.Sequence.Permutation.fst index f12cf8637f5..5d721c380b9 100644 --- a/ulib/experimental/FStar.Sequence.Permutation.fst +++ b/ulib/experimental/FStar.Sequence.Permutation.fst @@ -196,6 +196,8 @@ let rec permutation_from_equal_counts (#a:eqtype) (s0:seq a) (s1:seq a{(forall x ) ); reveal_is_permutation_nopats s0 s1 f; f) +#pop-options + #restart-solver module CM = FStar.Algebra.CommMonoid @@ -254,6 +256,7 @@ let rec foldm_back_append #a (m:CM.cm a) (s1 s2: seq a) m.mult (foldm_back m s1) (foldm_back m s2); } ) +#pop-options let foldm_back_sym #a (m:CM.cm a) (s1 s2: seq a) : Lemma