From d21e1afd044a181483fddee6946f78cb88655ced Mon Sep 17 00:00:00 2001 From: Karthikeyan Bhargavan Date: Thu, 4 Apr 2024 17:27:21 +0200 Subject: [PATCH 1/9] a rand core annotation --- proof-libs/fstar/core/Rand_core.fsti | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/proof-libs/fstar/core/Rand_core.fsti b/proof-libs/fstar/core/Rand_core.fsti index d660bf008..60f53bb75 100644 --- a/proof-libs/fstar/core/Rand_core.fsti +++ b/proof-libs/fstar/core/Rand_core.fsti @@ -4,7 +4,7 @@ open Rust_primitives class t_RngCore (t_Self: Type0) = { f_next_u32: t_Self -> t_Self & u32; f_next_u64: t_Self -> t_Self & u64; - f_fill_bytes: t_Self -> t_Slice u8 -> t_Self & t_Slice u8 + f_fill_bytes: t_Self -> x:t_Slice u8 -> t_Self & (y:t_Slice u8{Seq.length x == Seq.length y}) } class t_CryptoRng (t_Self: Type0) = { From a940818ad93ce4453003fe8eacecdb7d14821fda Mon Sep 17 00:00:00 2001 From: Karthikeyan Bhargavan Date: Tue, 23 Apr 2024 18:06:26 +0200 Subject: [PATCH 2/9] slice --- proof-libs/fstar/rust_primitives/Rust_primitives.fst | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/proof-libs/fstar/rust_primitives/Rust_primitives.fst b/proof-libs/fstar/rust_primitives/Rust_primitives.fst index da8e88eab..d80eabfde 100644 --- a/proof-libs/fstar/rust_primitives/Rust_primitives.fst +++ b/proof-libs/fstar/rust_primitives/Rust_primitives.fst @@ -41,7 +41,7 @@ class unsize_tc source = { } instance array_to_slice_unsize t n: unsize_tc (t_Array t n) = { - output = t_Slice t; + output = (x:t_Slice t{Seq.length x == v n}); unsize = (fun (arr: t_Array t n) -> arr <: t_Slice t); } From 37a519c180920f55958ef041f7251e8c85a7a3c3 Mon Sep 17 00:00:00 2001 From: Karthikeyan Bhargavan Date: Wed, 24 Apr 2024 08:33:11 +0200 Subject: [PATCH 3/9] copy trait --- proof-libs/fstar/core/Core.Marker.fst | 9 +++++++++ 1 file changed, 9 insertions(+) diff --git a/proof-libs/fstar/core/Core.Marker.fst b/proof-libs/fstar/core/Core.Marker.fst index 0ceacbe99..dcf5440fc 100644 --- a/proof-libs/fstar/core/Core.Marker.fst +++ b/proof-libs/fstar/core/Core.Marker.fst @@ -8,3 +8,12 @@ class t_Sized (h: Type) = { instance t_Sized_all t: t_Sized t = { dummy_field = () } + +class t_Copy (h: Type) = { + dummy_copy_field: unit +} + +(** we consider everything to be copyable *) +instance t_Copy_all t: t_Copy t = { + dummy_copy_field = () +} From 31ab83b53e51d08d5771d51b0de2b5bb4a5da0bc Mon Sep 17 00:00:00 2001 From: Karthikeyan Bhargavan Date: Wed, 24 Apr 2024 09:26:29 +0200 Subject: [PATCH 4/9] fix for precondition/postcondition function naming in traits --- engine/backends/fstar/fstar_backend.ml | 15 +++++++++------ 1 file changed, 9 insertions(+), 6 deletions(-) diff --git a/engine/backends/fstar/fstar_backend.ml b/engine/backends/fstar/fstar_backend.ml index 97cae64b3..b630885d9 100644 --- a/engine/backends/fstar/fstar_backend.ml +++ b/engine/backends/fstar/fstar_backend.ml @@ -1079,7 +1079,7 @@ struct generics.params in let name_str = U.Concrete_ident_view.to_definition_name name in - let name = F.id @@ name_str in + let name_id = F.id @@ name_str in let fields = List.concat_map ~f:(fun i -> @@ -1111,7 +1111,7 @@ struct let args = List.map ~f:(pgeneric_value e.span) args in - ( F.id (name ^ "_" ^ impl_ident_name), + ( F.id (name ^ "_" ^ impl_ident_name), (* Dodgy concatenation *) None, [], F.mk_e_app base args )) @@ -1128,13 +1128,16 @@ struct let output = pty e.span output in let ty_pre_post = let inputs = List.map ~f:FStarBinder.to_term inputs in + let add_pre n = n ^ "_pre" in + let pre_name_str = U.Concrete_ident_view.to_definition_name (Concrete_ident.Create.map_last ~f:add_pre i.ti_ident) in let pre = - F.mk_e_app (F.term_of_lid [ name ^ "_pre" ]) inputs - in + F.mk_e_app (F.term_of_lid [pre_name_str]) inputs in let result = F.term_of_lid [ "result" ] in + let add_post n = n ^ "_post" in + let post_name_str = U.Concrete_ident_view.to_definition_name (Concrete_ident.Create.map_last ~f:add_post i.ti_ident) in let post = F.mk_e_app - (F.term_of_lid [ name ^ "_post" ]) + (F.term_of_lid [ post_name_str]) (inputs @ [ result ]) in let post = @@ -1182,7 +1185,7 @@ struct [ (F.id marker_field, None, [], pty e.span U.unit_typ) ] else fields in - let tcdef = F.AST.TyconRecord (name, bds, None, [], fields) in + let tcdef = F.AST.TyconRecord (name_id, bds, None, [], fields) in let d = F.AST.Tycon (false, true, [ tcdef ]) in [ `Intf { d; drange = F.dummyRange; quals = []; attrs = [] } ] | Impl From 677efae7232750b23258036e056d0ea2c4a312e0 Mon Sep 17 00:00:00 2001 From: Karthikeyan Bhargavan Date: Wed, 24 Apr 2024 10:28:41 +0200 Subject: [PATCH 5/9] fixes for traits, WIP --- engine/lib/import_thir.ml | 6 +++++- 1 file changed, 5 insertions(+), 1 deletion(-) diff --git a/engine/lib/import_thir.ml b/engine/lib/import_thir.ml index 4edc4209f..8a7ec37dd 100644 --- a/engine/lib/import_thir.ml +++ b/engine/lib/import_thir.ml @@ -1502,10 +1502,14 @@ and c_item_unwrapped ~ident ~drop_body (item : Thir.item) : item list = ii_v = (match (item.kind : Thir.impl_item_kind) with | Fn { body; params; _ } -> + let params = + if List.is_empty params then [ U.make_unit_param span ] + else List.map ~f:(c_param item.span) params + in IIFn { body = c_expr body; - params = List.map ~f:(c_param item.span) params; + params = params; } | Const (_ty, e) -> IIFn { body = c_expr e; params = [] } From ae7c460af588eb7de756a2d75c6e1be180295d75 Mon Sep 17 00:00:00 2001 From: Karthikeyan Bhargavan Date: Wed, 24 Apr 2024 19:44:46 +0200 Subject: [PATCH 6/9] ocamlformat --- engine/backends/fstar/fstar_backend.ml | 22 +++++++++++++++------- engine/lib/import_thir.ml | 15 ++++++--------- 2 files changed, 21 insertions(+), 16 deletions(-) diff --git a/engine/backends/fstar/fstar_backend.ml b/engine/backends/fstar/fstar_backend.ml index b630885d9..39d054901 100644 --- a/engine/backends/fstar/fstar_backend.ml +++ b/engine/backends/fstar/fstar_backend.ml @@ -1111,7 +1111,8 @@ struct let args = List.map ~f:(pgeneric_value e.span) args in - ( F.id (name ^ "_" ^ impl_ident_name), (* Dodgy concatenation *) + ( F.id (name ^ "_" ^ impl_ident_name), + (* Dodgy concatenation *) None, [], F.mk_e_app base args )) @@ -1128,16 +1129,23 @@ struct let output = pty e.span output in let ty_pre_post = let inputs = List.map ~f:FStarBinder.to_term inputs in - let add_pre n = n ^ "_pre" in - let pre_name_str = U.Concrete_ident_view.to_definition_name (Concrete_ident.Create.map_last ~f:add_pre i.ti_ident) in + let add_pre n = n ^ "_pre" in + let pre_name_str = + U.Concrete_ident_view.to_definition_name + (Concrete_ident.Create.map_last ~f:add_pre i.ti_ident) + in let pre = - F.mk_e_app (F.term_of_lid [pre_name_str]) inputs in + F.mk_e_app (F.term_of_lid [ pre_name_str ]) inputs + in let result = F.term_of_lid [ "result" ] in - let add_post n = n ^ "_post" in - let post_name_str = U.Concrete_ident_view.to_definition_name (Concrete_ident.Create.map_last ~f:add_post i.ti_ident) in + let add_post n = n ^ "_post" in + let post_name_str = + U.Concrete_ident_view.to_definition_name + (Concrete_ident.Create.map_last ~f:add_post i.ti_ident) + in let post = F.mk_e_app - (F.term_of_lid [ post_name_str]) + (F.term_of_lid [ post_name_str ]) (inputs @ [ result ]) in let post = diff --git a/engine/lib/import_thir.ml b/engine/lib/import_thir.ml index 8a7ec37dd..9899d41a9 100644 --- a/engine/lib/import_thir.ml +++ b/engine/lib/import_thir.ml @@ -1502,15 +1502,12 @@ and c_item_unwrapped ~ident ~drop_body (item : Thir.item) : item list = ii_v = (match (item.kind : Thir.impl_item_kind) with | Fn { body; params; _ } -> - let params = - if List.is_empty params then [ U.make_unit_param span ] - else List.map ~f:(c_param item.span) params - in - IIFn - { - body = c_expr body; - params = params; - } + let params = + if List.is_empty params then + [ U.make_unit_param span ] + else List.map ~f:(c_param item.span) params + in + IIFn { body = c_expr body; params } | Const (_ty, e) -> IIFn { body = c_expr e; params = [] } | Type { ty; parent_bounds } -> From fbaa9760d1b9a880fce2c0924ab8c595882a28cc Mon Sep 17 00:00:00 2001 From: Lucas Franceschino Date: Thu, 25 Apr 2024 07:26:08 +0200 Subject: [PATCH 7/9] fix(tests): refresh --- test-harness/src/snapshots/toolchain__traits into-fstar.snap | 4 +++- 1 file changed, 3 insertions(+), 1 deletion(-) diff --git a/test-harness/src/snapshots/toolchain__traits into-fstar.snap b/test-harness/src/snapshots/toolchain__traits into-fstar.snap index 887b59401..e27f0766a 100644 --- a/test-harness/src/snapshots/toolchain__traits into-fstar.snap +++ b/test-harness/src/snapshots/toolchain__traits into-fstar.snap @@ -123,7 +123,9 @@ let impl_Foo_for_tuple_: t_Foo Prims.unit = f_AssocType = i32; f_AssocType_886671949818196346 = FStar.Tactics.Typeclasses.solve; f_N = sz 32; - f_assoc_f = () <: Prims.unit; + f_assoc_f_pre = (fun (_: Prims.unit) -> true); + f_assoc_f_post = (fun (_: Prims.unit) (out: Prims.unit) -> true); + f_assoc_f = (fun (_: Prims.unit) -> () <: Prims.unit); f_method_f_pre = (fun (self: Prims.unit) -> true); f_method_f_post = (fun (self: Prims.unit) (out: Prims.unit) -> true); f_method_f = (fun (self: Prims.unit) -> f_assoc_f ()); From d87cb47b5f551215bd505fd350aecf4766ab8e44 Mon Sep 17 00:00:00 2001 From: Karthikeyan Bhargavan Date: Thu, 25 Apr 2024 21:27:19 +0200 Subject: [PATCH 8/9] fixed paths in makefile --- examples/kyber_compress/proofs/fstar/extraction/Makefile | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/examples/kyber_compress/proofs/fstar/extraction/Makefile b/examples/kyber_compress/proofs/fstar/extraction/Makefile index f39ae304f..005f98a09 100644 --- a/examples/kyber_compress/proofs/fstar/extraction/Makefile +++ b/examples/kyber_compress/proofs/fstar/extraction/Makefile @@ -40,8 +40,8 @@ FSTAR_BIN ?= $(shell command -v fstar.exe 1>&2 2> /dev/null && echo "fstar. HAX_PROOF_LIBS_HOME ?= $(HAX_HOME)/proof-libs/fstar HAX_LIBS_HOME ?= $(HAX_HOME)/hax-lib/proofs/fstar/extraction -CACHE_DIR ?= $(HAX_PROOF_LIBS)/.cache -HINT_DIR ?= $(HAX_PROOF_LIBS)/.hints +CACHE_DIR ?= $(HAX_PROOF_LIBS_HOME)/.cache +HINT_DIR ?= $(HAX_PROOF_LIBS_HOME)/.hints .PHONY: all verify clean From 6a892efd3b178a6c2ed95276f16002ccea902500 Mon Sep 17 00:00:00 2001 From: Karthikeyan Bhargavan Date: Fri, 26 Apr 2024 12:44:25 +0200 Subject: [PATCH 9/9] bump rlimit for Kyber_compress --- examples/kyber_compress/proofs/fstar/extraction/Makefile | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/examples/kyber_compress/proofs/fstar/extraction/Makefile b/examples/kyber_compress/proofs/fstar/extraction/Makefile index 005f98a09..2cfa01554 100644 --- a/examples/kyber_compress/proofs/fstar/extraction/Makefile +++ b/examples/kyber_compress/proofs/fstar/extraction/Makefile @@ -54,7 +54,7 @@ all: ROOTS = Kyber_compress.fst $(ROOTS): ../../../src/lib.rs - cargo hax into fstar --z3rlimit 150 + cargo hax into fstar --z3rlimit 200 FSTAR_INCLUDE_DIRS = $(HACL_HOME)/lib \ $(HAX_PROOF_LIBS_HOME)/rust_primitives $(HAX_PROOF_LIBS_HOME)/core \