Skip to content

Coallesce duplicate lemmas about pow2, move into Math.Lemmas, add 128… #3910

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Draft
wants to merge 1 commit into
base: master
Choose a base branch
from
Draft

Coallesce duplicate lemmas about pow2, move into Math.Lemmas, add 128… #3910

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
1 commit
Select commit
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
9 changes: 4 additions & 5 deletions doc/book/code/Part5.Pow2.fst
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -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
Expand Down
2 changes: 1 addition & 1 deletion tests/hacl/Lib.IntTypes.fsti
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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)]
Expand Down
2 changes: 1 addition & 1 deletion tests/hacl/Lib.Sequence.fsti
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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

Expand Down
4 changes: 0 additions & 4 deletions tests/tactics/Inlining.fst
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand Down
2 changes: 1 addition & 1 deletion tests/vale/X64.Poly1305.Math_i.fst
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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) :
Expand Down
12 changes: 0 additions & 12 deletions ulib/FStar.Int.fst
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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

Expand Down
14 changes: 0 additions & 14 deletions ulib/FStar.Int.fsti
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand Down
14 changes: 14 additions & 0 deletions ulib/FStar.Math.Lemmas.fst
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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 = ()

Expand Down
18 changes: 17 additions & 1 deletion ulib/FStar.Math.Lemmas.fsti
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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)
Expand Down Expand Up @@ -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))
(ensures (b = a % c))
13 changes: 0 additions & 13 deletions ulib/FStar.UInt.fst
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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

Expand Down
15 changes: 0 additions & 15 deletions ulib/FStar.UInt.fsti
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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:
Expand Down
Loading