Fixes to F* library and extraction

engine/backends/fstar/fstar_backend.ml

@@ -1114,7 +1114,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 ->
@@ -1147,6 +1147,7 @@ struct
                              List.map ~f:(pgeneric_value e.span) args
                            in
                            ( F.id (name ^ "_" ^ impl_ident_name),
+                             (* Dodgy concatenation *)
                              None,
                              [],
                              F.mk_e_app base args ))
@@ -1163,13 +1164,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 pre =
-                        F.mk_e_app (F.term_of_lid [ name ^ "_pre" ]) inputs
+                        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 =
@@ -1217,7 +1228,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

engine/lib/import_thir.ml

@@ -1521,11 +1521,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; _ } ->
-                             IIFn
-                               {
-                                 body = c_expr body;
-                                 params = List.map ~f:(c_param item.span) 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 } ->

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
 
@@ -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 \

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 = ()
+}

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) = {

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);
 }

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 ());