diff --git a/doc/book/code/Part5.Pow2.fst b/doc/book/code/Part5.Pow2.fst index 2c45c0b6fe5..403d0315a1a 100644 --- a/doc/book/code/Part5.Pow2.fst +++ b/doc/book/code/Part5.Pow2.fst @@ -1,12 +1,11 @@ module Part5.Pow2 -(* Now (2023/08/30), importing the tactics module bring FStar.Pprint -into scope, which depends on FStar.Char, which depends on FStar.UInt. -We therefore get some facts about pow2 (FStar.UInt.pow2_values) that -break this example (break = make more things work than they should). So, +(* Now (2025/7/16), the pow2_values lemma is in FStar.Math.Lemmas, which +we mention and therefore depend on. We therefore get some facts +about pow2 that break this example (break = make more things work than they should). So, ignore these facts here to retain the example. What we would really want though is a way to scope SMT patterns. *) -#set-options "--using_facts_from -FStar.UInt" +#set-options "--using_facts_from -FStar.Math.Lemmas" [@@expect_failure [19]] //SNIPPET_START: pow2_0 diff --git a/tests/hacl/Lib.IntTypes.fsti b/tests/hacl/Lib.IntTypes.fsti index 943c83b2a35..4a11599d00b 100644 --- a/tests/hacl/Lib.IntTypes.fsti +++ b/tests/hacl/Lib.IntTypes.fsti @@ -4,7 +4,7 @@ open FStar.Mul #set-options "--fuel 0 --max_ifuel 1 --z3rlimit 20" -// Other instances frollow from `FStar.UInt.pow2_values` which is in +// Other instances frollow from `FStar.Math.Lemmas.pow2_values` which is in // scope of every module depending on Lib.IntTypes val pow2_2: n:nat -> Lemma (pow2 2 = 4) [SMTPat (pow2 n)] val pow2_3: n:nat -> Lemma (pow2 3 = 8) [SMTPat (pow2 n)] diff --git a/tests/hacl/Lib.Sequence.fsti b/tests/hacl/Lib.Sequence.fsti index 4ccaa62169c..6a14a0ddd81 100644 --- a/tests/hacl/Lib.Sequence.fsti +++ b/tests/hacl/Lib.Sequence.fsti @@ -552,7 +552,7 @@ val index_generate_blocks: let _,s2 = f (i / len) () in Seq.index s1 i == Seq.index s2 (i % len)) -#push-options "--using_facts_from '+FStar.UInt.pow2_values'" +#push-options "--using_facts_from '+FStar.Math.Lemmas.pow2_values'" val create2: #a:Type -> x0:a -> x1:a -> lseq a 2 diff --git a/tests/tactics/Inlining.fst b/tests/tactics/Inlining.fst index 459c09a6166..8ff5fd5b7d6 100644 --- a/tests/tactics/Inlining.fst +++ b/tests/tactics/Inlining.fst @@ -15,10 +15,6 @@ *) module Inlining -// inlining into stateful functions doesn't work in master; -// see https://github.com/FStarLang/FStar/issues/1190 -// (fixed in guido_fix) - open FStar.Tactics.V2 open FStar.HyperStack diff --git a/tests/vale/X64.Poly1305.Math_i.fst b/tests/vale/X64.Poly1305.Math_i.fst index e49301b9ab5..d17524fe617 100644 --- a/tests/vale/X64.Poly1305.Math_i.fst +++ b/tests/vale/X64.Poly1305.Math_i.fst @@ -261,7 +261,7 @@ let lemma_mod_power2_lo (x0:nat64) (x1:nat64) (y:int) (z:int) = let lemma_power2_add64 (n:nat) = pow2_plus 64 n; - FStar.UInt.pow2_values 64 + FStar.Math.Lemmas.pow2_values 64 //TODO: dafny proof seems tedious let lemma_mod_breakdown (a:nat) (b:pos) (c:pos) : diff --git a/ulib/FStar.Int.fst b/ulib/FStar.Int.fst index 276c926c873..1fe5ffa326e 100644 --- a/ulib/FStar.Int.fst +++ b/ulib/FStar.Int.fst @@ -22,18 +22,6 @@ open FStar.Mul open FStar.BitVector open FStar.Math.Lemmas -let pow2_values x = - match x with - | 0 -> assert_norm (pow2 0 == 1) - | 1 -> assert_norm (pow2 1 == 2) - | 8 -> assert_norm (pow2 8 == 256) - | 16 -> assert_norm (pow2 16 == 65536) - | 31 -> assert_norm (pow2 31 == 2147483648) - | 32 -> assert_norm (pow2 32 == 4294967296) - | 63 -> assert_norm (pow2 63 == 9223372036854775808) - | 64 -> assert_norm (pow2 64 == 18446744073709551616) - | _ -> () - let incr_underspec #n a = if a < max_int n then a + 1 else 0 diff --git a/ulib/FStar.Int.fsti b/ulib/FStar.Int.fsti index d483ed7e917..0a49376d7e7 100644 --- a/ulib/FStar.Int.fsti +++ b/ulib/FStar.Int.fsti @@ -22,20 +22,6 @@ open FStar.Mul open FStar.BitVector open FStar.Math.Lemmas -val pow2_values: x:nat -> Lemma - (let p = pow2 x in - match x with - | 0 -> p=1 - | 1 -> p=2 - | 8 -> p=256 - | 16 -> p=65536 - | 31 -> p=2147483648 - | 32 -> p=4294967296 - | 63 -> p=9223372036854775808 - | 64 -> p=18446744073709551616 - | _ -> True) - [SMTPat (pow2 x)] - /// Specs let max_int (n:pos) : Tot int = pow2 (n-1) - 1 diff --git a/ulib/FStar.Math.Lemmas.fst b/ulib/FStar.Math.Lemmas.fst index 7f3cbbc03f5..a17025119c8 100644 --- a/ulib/FStar.Math.Lemmas.fst +++ b/ulib/FStar.Math.Lemmas.fst @@ -20,6 +20,20 @@ open FStar.Math.Lib #set-options "--fuel 0 --ifuel 0" +let pow2_values x = + match x with + | 0 -> assert_norm (pow2 0 == 1) + | 1 -> assert_norm (pow2 1 == 2) + | 8 -> assert_norm (pow2 8 == 256) + | 16 -> assert_norm (pow2 16 == 65536) + | 31 -> assert_norm (pow2 31 == 2147483648) + | 32 -> assert_norm (pow2 32 == 4294967296) + | 63 -> assert_norm (pow2 63 == 9223372036854775808) + | 64 -> assert_norm (pow2 64 == 18446744073709551616) + | 127 -> assert_norm (pow2 127 == 170141183460469231731687303715884105728) + | 128 -> assert_norm (pow2 128 == 340282366920938463463374607431768211456) + | _ -> () + (* Lemma: definition of Euclidean division *) let euclidean_div_axiom a b = () diff --git a/ulib/FStar.Math.Lemmas.fsti b/ulib/FStar.Math.Lemmas.fsti index 162041482a3..e95f7ea3fbf 100644 --- a/ulib/FStar.Math.Lemmas.fsti +++ b/ulib/FStar.Math.Lemmas.fsti @@ -17,6 +17,22 @@ module FStar.Math.Lemmas open FStar.Mul +val pow2_values: x:nat -> Lemma + (let p = pow2 x in + match x with + | 0 -> p=1 + | 1 -> p=2 + | 8 -> p=256 + | 16 -> p=65536 + | 31 -> p=2147483648 + | 32 -> p=4294967296 + | 63 -> p=9223372036854775808 + | 64 -> p=18446744073709551616 + | 127 -> p=170141183460469231731687303715884105728 + | 128 -> p=340282366920938463463374607431768211456 + | _ -> True) + [SMTPat (pow2 x)] + (* Lemma: definition of Euclidean division *) val euclidean_div_axiom: a:int -> b:pos -> Lemma (a - b * (a / b) >= 0 /\ a - b * (a / b) < b) @@ -404,4 +420,4 @@ val lemma_mod_plus_injective (n:pos) (a:int) (b:nat) (c:nat) : Lemma val modulo_sub_lemma (a : int) (b : nat) (c : pos) : Lemma (requires (b < c /\ (a - b) % c = 0)) - (ensures (b = a % c)) \ No newline at end of file + (ensures (b = a % c)) diff --git a/ulib/FStar.UInt.fst b/ulib/FStar.UInt.fst index 4fe93b65559..0f9b9dac10e 100644 --- a/ulib/FStar.UInt.fst +++ b/ulib/FStar.UInt.fst @@ -22,19 +22,6 @@ open FStar.Mul open FStar.BitVector open FStar.Math.Lemmas -let pow2_values x = - match x with - | 0 -> assert_norm (pow2 0 == 1) - | 1 -> assert_norm (pow2 1 == 2) - | 8 -> assert_norm (pow2 8 == 256) - | 16 -> assert_norm (pow2 16 == 65536) - | 31 -> assert_norm (pow2 31 == 2147483648) - | 32 -> assert_norm (pow2 32 == 4294967296) - | 63 -> assert_norm (pow2 63 == 9223372036854775808) - | 64 -> assert_norm (pow2 64 == 18446744073709551616) - | 128 -> assert_norm (pow2 128 = 0x100000000000000000000000000000000) - | _ -> () - let incr_underspec #n a = if a < max_int n then a + 1 else 0 diff --git a/ulib/FStar.UInt.fsti b/ulib/FStar.UInt.fsti index 67f9eecbba1..cdeb5d792f5 100644 --- a/ulib/FStar.UInt.fsti +++ b/ulib/FStar.UInt.fsti @@ -22,21 +22,6 @@ open FStar.Mul open FStar.BitVector open FStar.Math.Lemmas -val pow2_values: x:nat -> Lemma - (let p = pow2 x in - match x with - | 0 -> p=1 - | 1 -> p=2 - | 8 -> p=256 - | 16 -> p=65536 - | 31 -> p=2147483648 - | 32 -> p=4294967296 - | 63 -> p=9223372036854775808 - | 64 -> p=18446744073709551616 - | 128 -> p=0x100000000000000000000000000000000 - | _ -> True) - [SMTPat (pow2 x)] - /// Specs /// /// Note: lacking any type of functors for F*, this is a copy/paste of [FStar.Int.fst], where the relevant bits that changed are: