Skip to content
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

Adapt proofs to use transparent integers #756

Merged
merged 9 commits into from
Jan 25, 2025
Merged

Adapt proofs to use transparent integers #756

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
9 commits
Select commit Hold shift + click to select a range
47a70ca
ml-kem laxes
karthikbhargavan Jan 18, 2025
29b3134
ml-dsa laxes
karthikbhargavan Jan 18, 2025
9d8d421
everything except ind-cpa verified
karthikbhargavan Jan 18, 2025
7d21a8a
fmt
karthikbhargavan Jan 18, 2025
ccbb5f7
refactor(fstar-helpers/tactics): drop the tactics related to machine …
W95Psp Jan 23, 2025
ad18ea1
Merge branch 'main' into transparent-integers
karthikbhargavan Jan 24, 2025
3398e71
re-extract
karthikbhargavan Jan 24, 2025
70eddcd
Merge branch 'main' into transparent-integers
karthikbhargavan Jan 24, 2025
985ac38
switch to main
karthikbhargavan Jan 24, 2025
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
2 changes: 1 addition & 1 deletion Cargo.toml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -88,7 +88,7 @@ log = { version = "0.4", optional = true }
# WASM API
wasm-bindgen = { version = "0.2.87", optional = true }
getrandom = { version = "0.2", features = ["js"], optional = true }
hax-lib = { version = "0.1.0-alpha.1", git = "https://github.com/hacspec/hax/" }
hax-lib = { version = "0.1.0", git = "https://github.com/hacspec/hax/" }

[dev-dependencies]
libcrux = { path = ".", features = ["rand", "tests"] }
Expand Down
88 changes: 44 additions & 44 deletions fstar-helpers/fstar-bitvec/BitVec.Intrinsics.fsti
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -22,7 +22,7 @@ let mm256_srli_epi64 (shift: i32 {v shift >= 0 /\ v shift <= 64}) (vec: bit_vec

let mm256_castsi256_si128 (vec: bit_vec 256): bit_vec 128
= mk_bv (fun i -> vec i)
let mm256_extracti128_si256 (control: i32{control == 1l}) (vec: bit_vec 256): bit_vec 128
let mm256_extracti128_si256 (control: i32{control == mk_i32 1}) (vec: bit_vec 256): bit_vec 128
= mk_bv (fun i -> vec (i + 128))

let mm256_si256_from_two_si128 (lower upper: bit_vec 128): bit_vec 256
Expand Down Expand Up @@ -86,7 +86,7 @@ let mm256_and_si256 (x y: bit_vec 256): bit_vec 256
= mk_bv (fun i -> if y i = 0 then 0 else x i)

let mm256_set1_epi16 (constant: i16)
(#[Tactics.exact (match unify_app (quote constant) (quote (fun n -> ((1s <<! Int32.int_to_t n <: i16) -! 1s <: i16))) [] with
(#[Tactics.exact (match unify_app (quote constant) (quote (fun n -> (((mk_i16 1) <<! mk_i32 n <: i16) -! (mk_i16 1) <: i16))) [] with
| Some [x] -> `(mm256_set1_epi16_pow2_minus_one (`#x))
| _ -> (quote (mm256_set1_epi16_no_semantics constant))
)]result: bit_vec 256)
Expand Down Expand Up @@ -173,26 +173,26 @@ open FStar.Tactics.V2
let mm256_mullo_epi16
(a count: bit_vec 256)
(#[(
if match unify_app (quote count) (quote (fun x -> mm256_set_epi16 (1s <<! 8l <: i16) (x <<! 9l <: i16)
(1s <<! 10l <: i16) (1s <<! 11l <: i16) (1s <<! 12l <: i16) (1s <<! 13l <: i16)
(1s <<! 14l <: i16) (-32768s) (1s <<! 8l <: i16) (1s <<! 9l <: i16) (1s <<! 10l <: i16)
(1s <<! 11l <: i16) (1s <<! 12l <: i16) (1s <<! 13l <: i16) (1s <<! 14l <: i16) (-32768s))) [] with
| Some [x] -> unquote x = 1s
if match unify_app (quote count) (quote (fun x -> mm256_set_epi16 ((mk_i16 1) <<! (mk_i32 8) <: i16) (x <<! (mk_i32 9) <: i16)
((mk_i16 1) <<! (mk_i32 10) <: i16) ((mk_i16 1) <<! (mk_i32 11) <: i16) ((mk_i16 1) <<! (mk_i32 12) <: i16) ((mk_i16 1) <<! (mk_i32 13) <: i16)
((mk_i16 1) <<! (mk_i32 14) <: i16) (mk_i16 (-32768)) ((mk_i16 1) <<! (mk_i32 8) <: i16) ((mk_i16 1) <<! (mk_i32 9) <: i16) ((mk_i16 1) <<! (mk_i32 10) <: i16)
((mk_i16 1) <<! (mk_i32 11) <: i16) ((mk_i16 1) <<! (mk_i32 12) <: i16) ((mk_i16 1) <<! (mk_i32 13) <: i16) ((mk_i16 1) <<! (mk_i32 14) <: i16) (mk_i16 (-32768)))) [] with
| Some [x] -> unquote x = (mk_i16 1)
| _ -> false
then Tactics.exact (quote (mm256_mullo_epi16_specialized1 a))
else if match unify_app (quote count) (quote (fun x -> mm256_set_epi16 (1s <<! 0l <: i16) (x <<! 4l <: i16)
(1s <<! 0l <: i16) (1s <<! 4l <: i16) (1s <<! 0l <: i16) (1s <<! 4l <: i16) (1s <<! 0l <: i16)
(1s <<! 4l <: i16) (1s <<! 0l <: i16) (1s <<! 4l <: i16) (1s <<! 0l <: i16) (1s <<! 4l <: i16)
(1s <<! 0l <: i16) (1s <<! 4l <: i16) (1s <<! 0l <: i16) (1s <<! 4l <: i16))) [] with
| Some [x] -> unquote x = 1s
else if match unify_app (quote count) (quote (fun x -> mm256_set_epi16 ((mk_i16 1) <<! (mk_i32 0) <: i16) (x <<! (mk_i32 4) <: i16)
((mk_i16 1) <<! (mk_i32 0) <: i16) ((mk_i16 1) <<! (mk_i32 4) <: i16) ((mk_i16 1) <<! (mk_i32 0) <: i16) ((mk_i16 1) <<! (mk_i32 4) <: i16) ((mk_i16 1) <<! (mk_i32 0) <: i16)
((mk_i16 1) <<! (mk_i32 4) <: i16) ((mk_i16 1) <<! (mk_i32 0) <: i16) ((mk_i16 1) <<! (mk_i32 4) <: i16) ((mk_i16 1) <<! (mk_i32 0) <: i16) ((mk_i16 1) <<! (mk_i32 4) <: i16)
((mk_i16 1) <<! (mk_i32 0) <: i16) ((mk_i16 1) <<! (mk_i32 4) <: i16) ((mk_i16 1) <<! (mk_i32 0) <: i16) ((mk_i16 1) <<! (mk_i32 4) <: i16))) [] with
| Some [x] -> unquote x = (mk_i16 1)
| _ -> false
then Tactics.exact (quote (mm256_mullo_epi16_specialized2 a))
else
if match unify_app (quote count) (quote (fun x -> mm256_set_epi16 (1s <<! 0l <: i16) (x <<! 2l <: i16)
(1s <<! 4l <: i16) (1s <<! 6l <: i16) (1s <<! 0l <: i16) (1s <<! 2l <: i16) (1s <<! 4l <: i16)
(1s <<! 6l <: i16) (1s <<! 0l <: i16) (1s <<! 2l <: i16) (1s <<! 4l <: i16) (1s <<! 6l <: i16)
(1s <<! 0l <: i16) (1s <<! 2l <: i16) (1s <<! 4l <: i16) (1s <<! 6l <: i16))) [] with
| Some [x] -> unquote x = 1s
if match unify_app (quote count) (quote (fun x -> mm256_set_epi16 ((mk_i16 1) <<! (mk_i32 0) <: i16) (x <<! (mk_i32 2) <: i16)
((mk_i16 1) <<! (mk_i32 4) <: i16) ((mk_i16 1) <<! (mk_i32 6) <: i16) ((mk_i16 1) <<! (mk_i32 0) <: i16) ((mk_i16 1) <<! (mk_i32 2) <: i16) ((mk_i16 1) <<! (mk_i32 4) <: i16)
((mk_i16 1) <<! (mk_i32 6) <: i16) ((mk_i16 1) <<! (mk_i32 0) <: i16) ((mk_i16 1) <<! (mk_i32 2) <: i16) ((mk_i16 1) <<! (mk_i32 4) <: i16) ((mk_i16 1) <<! (mk_i32 6) <: i16)
((mk_i16 1) <<! (mk_i32 0) <: i16) ((mk_i16 1) <<! (mk_i32 2) <: i16) ((mk_i16 1) <<! (mk_i32 4) <: i16) ((mk_i16 1) <<! (mk_i32 6) <: i16))) [] with
| Some [x] -> unquote x = (mk_i16 1)
| _ -> false
then Tactics.exact (quote (mm256_mullo_epi16_specialized3 a))
else
Expand All @@ -201,22 +201,22 @@ let mm256_mullo_epi16

let madd_rhs (n: nat {n < 16}) =
mm256_set_epi16
(1s <<! Int32.int_to_t n <: i16)
1s
(1s <<! Int32.int_to_t n <: i16)
1s
(1s <<! Int32.int_to_t n <: i16)
1s
(1s <<! Int32.int_to_t n <: i16)
1s
(1s <<! Int32.int_to_t n <: i16)
1s
(1s <<! Int32.int_to_t n <: i16)
1s
(1s <<! Int32.int_to_t n <: i16)
1s
(1s <<! Int32.int_to_t n <: i16)
1s
((mk_i16 1) <<! mk_i32 n <: i16)
(mk_i16 1)
((mk_i16 1) <<! mk_i32 n <: i16)
(mk_i16 1)
((mk_i16 1) <<! mk_i32 n <: i16)
(mk_i16 1)
((mk_i16 1) <<! mk_i32 n <: i16)
(mk_i16 1)
((mk_i16 1) <<! mk_i32 n <: i16)
(mk_i16 1)
((mk_i16 1) <<! mk_i32 n <: i16)
(mk_i16 1)
((mk_i16 1) <<! mk_i32 n <: i16)
(mk_i16 1)
((mk_i16 1) <<! mk_i32 n <: i16)
(mk_i16 1)

val mm256_madd_epi16_no_semantic: bit_vec 256 -> bit_vec 256 -> bit_vec 256

Expand Down Expand Up @@ -273,8 +273,8 @@ let mm_shuffle_epi8
let t = match unify_app (quote y)
(quote (fun x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 ->
mm_set_epi8
(UInt8.uint_to_t x0 ) (UInt8.uint_to_t x1 ) (UInt8.uint_to_t x2 ) (UInt8.uint_to_t x3 ) (UInt8.uint_to_t x4 ) (UInt8.uint_to_t x5 ) (UInt8.uint_to_t x6 ) (UInt8.uint_to_t x7 )
(UInt8.uint_to_t x8 ) (UInt8.uint_to_t x9 ) (UInt8.uint_to_t x10) (UInt8.uint_to_t x11) (UInt8.uint_to_t x12) (UInt8.uint_to_t x13) (UInt8.uint_to_t x14) (UInt8.uint_to_t x15))) [] with
(mk_u8 x0 ) (mk_u8 x1 ) (mk_u8 x2 ) (mk_u8 x3 ) (mk_u8 x4 ) (mk_u8 x5 ) (mk_u8 x6 ) (mk_u8 x7 )
(mk_u8 x8 ) (mk_u8 x9 ) (mk_u8 x10) (mk_u8 x11) (mk_u8 x12) (mk_u8 x13) (mk_u8 x14) (mk_u8 x15))) [] with
| Some [x0;x1;x2;x3;x4;x5;x6;x7;x8;x9;x10;x11;x12;x13;x14;x15] ->
`(mm_shuffle_epi8_u8 (`@x)
(mk_list_16
Expand All @@ -301,10 +301,10 @@ let mm256_shuffle_epi8
let t = match unify_app (quote y)
(quote (fun x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 x17 x18 x19 x20 x21 x22 x23 x24 x25 x26 x27 x28 x29 x30 x31 ->
mm256_set_epi8
(Int8.int_to_t x0 ) (Int8.int_to_t x1 ) (Int8.int_to_t x2 ) (Int8.int_to_t x3 ) (Int8.int_to_t x4 ) (Int8.int_to_t x5 ) (Int8.int_to_t x6 ) (Int8.int_to_t x7 )
(Int8.int_to_t x8 ) (Int8.int_to_t x9 ) (Int8.int_to_t x10) (Int8.int_to_t x11) (Int8.int_to_t x12) (Int8.int_to_t x13) (Int8.int_to_t x14) (Int8.int_to_t x15)
(Int8.int_to_t x16) (Int8.int_to_t x17) (Int8.int_to_t x18) (Int8.int_to_t x19) (Int8.int_to_t x20) (Int8.int_to_t x21) (Int8.int_to_t x22) (Int8.int_to_t x23)
(Int8.int_to_t x24) (Int8.int_to_t x25) (Int8.int_to_t x26) (Int8.int_to_t x27) (Int8.int_to_t x28) (Int8.int_to_t x29) (Int8.int_to_t x30) (Int8.int_to_t x31))) [] with
(mk_i8 x0 ) (mk_i8 x1 ) (mk_i8 x2 ) (mk_i8 x3 ) (mk_i8 x4 ) (mk_i8 x5 ) (mk_i8 x6 ) (mk_i8 x7 )
(mk_i8 x8 ) (mk_i8 x9 ) (mk_i8 x10) (mk_i8 x11) (mk_i8 x12) (mk_i8 x13) (mk_i8 x14) (mk_i8 x15)
(mk_i8 x16) (mk_i8 x17) (mk_i8 x18) (mk_i8 x19) (mk_i8 x20) (mk_i8 x21) (mk_i8 x22) (mk_i8 x23)
(mk_i8 x24) (mk_i8 x25) (mk_i8 x26) (mk_i8 x27) (mk_i8 x28) (mk_i8 x29) (mk_i8 x30) (mk_i8 x31))) [] with
| Some [x0;x1;x2;x3;x4;x5;x6;x7;x8;x9;x10;x11;x12;x13;x14;x15;x16;x17;x18;x19;x20;x21;x22;x23;x24;x25;x26;x27;x28;x29;x30;x31] ->
`(mm256_shuffle_epi8_i8 (`@x)
(mk_list_32
Expand All @@ -331,8 +331,8 @@ let mm256_permutevar8x32_epi32
let t = match unify_app (quote y)
(quote (fun x0 x1 x2 x3 x4 x5 x6 x7 ->
mm256_set_epi32
(Int32.int_to_t x0) (Int32.int_to_t x1) (Int32.int_to_t x2) (Int32.int_to_t x3)
(Int32.int_to_t x4) (Int32.int_to_t x5) (Int32.int_to_t x6) (Int32.int_to_t x7))) [] with
(mk_i32 x0) (mk_i32 x1) (mk_i32 x2) (mk_i32 x3)
(mk_i32 x4) (mk_i32 x5) (mk_i32 x6) (mk_i32 x7))) [] with
| Some [x0;x1;x2;x3;x4;x5;x6;x7] ->
`(mm256_permutevar8x32_epi32_i32 (`@x)
(mk_list_8 (`#x0 ) (`#x1 ) (`#x2 ) (`#x3 ) (`#x4 ) (`#x5 ) (`#x6 ) (`#x7 )))
Expand All @@ -354,8 +354,8 @@ let mm256_sllv_epi32
let t = match unify_app (quote y)
(quote (fun x0 x1 x2 x3 x4 x5 x6 x7 ->
mm256_set_epi32
(Int32.int_to_t x0) (Int32.int_to_t x1) (Int32.int_to_t x2) (Int32.int_to_t x3)
(Int32.int_to_t x4) (Int32.int_to_t x5) (Int32.int_to_t x6) (Int32.int_to_t x7))) [] with
(mk_i32 x0) (mk_i32 x1) (mk_i32 x2) (mk_i32 x3)
(mk_i32 x4) (mk_i32 x5) (mk_i32 x6) (mk_i32 x7))) [] with
| Some [x0;x1;x2;x3;x4;x5;x6;x7] ->
`(mm256_sllv_epi32_i32 (`@x)
(mk_list_8 (`#x0 ) (`#x1 ) (`#x2 ) (`#x3 ) (`#x4 ) (`#x5 ) (`#x6 ) (`#x7 )))
Expand Down Expand Up @@ -421,5 +421,5 @@ let tassert (x: bool): Tac unit
private let example: bit_vec 256 = mk_bv (fun i -> if i % 16 = 15 then 1 else 0)

private let x = bv_to_string example
private let y = bv_to_string (mm256_srli_epi16 15l example)
private let y = bv_to_string (mm256_srli_epi16 (mk_i32 15) example)

71 changes: 0 additions & 71 deletions fstar-helpers/fstar-bitvec/RwLemmas.fst
View file
Open in desktop

This file was deleted.

6 changes: 2 additions & 4 deletions fstar-helpers/fstar-bitvec/Tactics.GetBit.fst
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -15,9 +15,6 @@ open Tactics.Pow2
open BitVecEq
open Tactics.Seq


let norm_machine_int () = Tactics.MachineInts.(transform norm_machine_int_term)

/// Does one round of computation
let compute_one_round (): Tac _ =
norm [ iota; zeta; reify_
Expand All @@ -31,7 +28,6 @@ let compute_one_round (): Tac _ =
]
; primops; unmeta];
trace "compute_one_round: norm_pow2" norm_pow2;
trace "compute_one_round: norm_machine_int" norm_machine_int;
trace "compute_one_round: norm_index" norm_index

/// Normalizes up to `get_bit`
Expand All @@ -57,10 +53,12 @@ let prove_bit_vector_equality'' (): Tac unit =
print ("Ask SMT: " ^ term_to_string (cur_goal ()));
focus smt_sync
))

let prove_bit_vector_equality' (): Tac unit =
if lax_on ()
then iterAll tadmit
else prove_bit_vector_equality'' ()

let prove_bit_vector_equality (): Tac unit =
set_rlimit 100;
with_compat_pre_core 0 prove_bit_vector_equality'
Loading
Loading