hacspec · W95Psp · Jun 26, 2024 · Jun 26, 2024 · Jun 26, 2024 · Jun 26, 2024
diff --git a/engine/backends/fstar/fstar_backend.ml b/engine/backends/fstar/fstar_backend.ml
@@ -407,14 +407,16 @@ struct
  (* in *)
  F.term @@ F.AST.Const (F.Const.Const_string ("failure", F.dummyRange))
 
- and fun_application ~span f args generic_args =
+ and make_application ~span ~generic_qualifier f args generic_args =
+ let is_arrow =
+ (* TODO: why? add documentation *)
+ [%matches? GType (TArrow _)]
+ in
  let generic_args =
  generic_args
- |> List.filter ~f:(function GType (TArrow _) -> false | _ -> true)
- |> List.map ~f:(function
- | GConst const -> (pexpr const, F.AST.Nothing)
- | GLifetime _ -> .
- | GType ty -> (pty span ty, F.AST.Hash))
+ |> List.filter ~f:(is_arrow >> not)
+ |> List.map ~f:(pgeneric_value span)
+ |> List.map ~f:(fun g -> (g, generic_qualifier))
  in
  let args = List.map ~f:(pexpr &&& Fn.const F.AST.Nothing) args in
  F.mk_app f (generic_args @ args)
@@ -464,7 +466,8 @@ struct
  chars: '" ^ s ^ "'");
  F.AST.Const (F.Const.Const_int (s, None)) |> F.term
  | App { f; args; generic_args; bounds_impls = _; impl = _ } ->
- fun_application ~span:e.span (pexpr f) args generic_args
+ make_application ~span:e.span ~generic_qualifier:F.AST.Hash (pexpr f)
+ args generic_args
  | If { cond; then_; else_ } ->
  F.term
  @@ F.AST.If
@@ -635,7 +638,7 @@ struct
  match p.kind with
  | GPLifetime _ -> Error.assertion_failure span "pgeneric_param:LIFETIME"
  | GPType { default = _ } -> { kind; typ = F.type0_term; ident }
- | GPConst { typ } -> { kind = Explicit; typ = pty span typ; ident }
+ | GPConst { typ } -> { kind; typ = pty span typ; ident }
 
  let of_generic_constraint span (nth : int) (c : generic_constraint) =
  match c with
@@ -676,6 +679,10 @@ struct
  let to_term (x : t) : F.AST.term =
  F.term @@ F.AST.Var (FStar_Ident.lid_of_ns_and_id [] (to_ident x))
 
+ let to_qualified_term (x : t) : F.AST.term * F.AST.imp =
+ ( to_term x,
+ match x.kind with Explicit -> F.AST.Nothing | _ -> F.AST.Hash )
+
  let to_binder (x : t) : F.AST.binder =
  F.AST.
  {
@@ -1159,7 +1166,7 @@ struct
  | Trait { name; generics; items } ->
  let bds =
  List.map
- ~f:FStarBinder.(of_generic_param e.span >> to_binder)
+ ~f:FStarBinder.(of_generic_param ~kind:Explicit e.span >> to_binder)
  generics.params
  in
  let name_str = U.Concrete_ident_view.to_definition_name name in
@@ -1184,22 +1191,12 @@ struct
  (* in *)
  (F.id name, None, [], t)
  :: List.map
- ~f:
- (fun {
- goal = { trait; args };
- name = impl_ident_name;
- } ->
- let base =
- F.term @@ F.AST.Name (pconcrete_ident trait)
- in
- let args =
- List.map ~f:(pgeneric_value e.span) args
- in
+ ~f:(fun { goal; name = impl_ident_name } ->
  ( F.id (name ^ "_" ^ impl_ident_name),
  (* Dodgy concatenation *)
  None,
  [],
- F.mk_e_app base args ))
+ c_trait_goal e.span goal ))
  bounds
  | TIFn (TArrow (inputs, output))
  when Attrs.find_unique_attr i.ti_attrs ~f:(function
@@ -1212,14 +1209,16 @@ struct
  let inputs = generics @ inputs in
  let output = pty e.span output in
  let ty_pre_post =
- let inputs = List.map ~f:FStarBinder.to_term inputs in
+ let inputs =
+ List.map ~f:FStarBinder.to_qualified_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 [ pre_name_str ]) inputs
+ F.mk_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
@@ -1228,9 +1227,9 @@ struct
  (Concrete_ident.Create.map_last ~f:add_post i.ti_ident)
  in
  let post =
- F.mk_e_app
+ F.mk_app
  (F.term_of_lid [ post_name_str ])
- (inputs @ [ result ])
+ (inputs @ [ (result, F.AST.Nothing) ])
  in
  let post =
  F.mk_e_abs
@@ -1296,7 +1295,7 @@ struct
  @@ F.AST.PatApp (pat, List.map ~f:FStarBinder.to_pattern generics)
  in
  let typ =
- fun_application ~span:e.span
+ make_application ~generic_qualifier:F.AST.Nothing ~span:e.span
  (F.term @@ F.AST.Name (pglobal_ident e.span trait))
  [] generic_args
  in

diff --git a/proof-libs/fstar/core/Makefile b/proof-libs/fstar/core/Makefile
@@ -49,7 +49,7 @@ all:
 
 # By default, we process all the files in the current directory. Here, we
 # *extend* the set of relevant files with the tests.
-ROOTS = $(wildcard *.fst)
+ROOTS = $(wildcard *.fst) $(wildcard *.fsti)
 
 FSTAR_INCLUDE_DIRS = $(HACL_HOME)/lib $(HAX_PROOF_LIBS_HOME)/rust_primitives $(HAX_PROOF_LIBS_HOME)/core $(HAX_LIBS_HOME)/proofs/fstar/extraction/
 

diff --git a/proof-libs/fstar/rust_primitives/Makefile b/proof-libs/fstar/rust_primitives/Makefile
@@ -49,7 +49,7 @@ all:
 
 # By default, we process all the files in the current directory. Here, we
 # *extend* the set of relevant files with the tests.
-ROOTS = $(wildcard *.fst)
+ROOTS = $(wildcard *.fst) $(wildcard *.fsti)
 
 FSTAR_INCLUDE_DIRS = $(HACL_HOME)/lib $(HAX_PROOF_LIBS_HOME)/rust_primitives $(HAX_PROOF_LIBS_HOME)/core $(HAX_LIBS_HOME)/proofs/fstar/extraction/
 

diff --git a/test-harness/src/snapshots/toolchain__attribute-opaque into-fstar.snap b/test-harness/src/snapshots/toolchain__attribute-opaque into-fstar.snap
@@ -37,7 +37,7 @@ module Attribute_opaque
 open Core
 open FStar.Mul
 
-val t_OpaqueEnum (v_X: usize) (#v_T #v_U: Type0) : Type0
+val t_OpaqueEnum (#v_X: usize) (#v_T #v_U: Type0) : Type0
 
-val t_OpaqueStruct (v_X: usize) (#v_T #v_U: Type0) : Type0
+val t_OpaqueStruct (#v_X: usize) (#v_T #v_U: Type0) : Type0
 '''
diff --git a/test-harness/src/snapshots/toolchain__attributes into-fstar.snap b/test-harness/src/snapshots/toolchain__attributes into-fstar.snap
@@ -62,7 +62,7 @@ let impl__SafeIndex__new (i: usize) : Core.Option.t_Option t_SafeIndex =
  else Core.Option.Option_None <: Core.Option.t_Option t_SafeIndex
 
 [@@ FStar.Tactics.Typeclasses.tcinstance]
-let impl_1 (#v_T: Type0) : Core.Ops.Index.t_Index #(t_Array v_T (sz 10)) #t_SafeIndex =
+let impl_1 (#v_T: Type0) : Core.Ops.Index.t_Index (t_Array v_T (sz 10)) t_SafeIndex =
  {
  f_Output = v_T;
  f_index_pre = (fun (self: t_Array v_T (sz 10)) (index: t_SafeIndex) -> true);
@@ -79,7 +79,7 @@ open FStar.Mul
 type t_Foo = | Foo : u8 -> t_Foo
 
 [@@ FStar.Tactics.Typeclasses.tcinstance]
-let impl: Core.Ops.Arith.t_Add #t_Foo #t_Foo =
+let impl: Core.Ops.Arith.t_Add t_Foo t_Foo =
  {
  f_Output = t_Foo;
  f_add_pre = (fun (self: t_Foo) (rhs: t_Foo) -> self._0 <. (255uy -! rhs._0 <: u8));
@@ -88,7 +88,7 @@ let impl: Core.Ops.Arith.t_Add #t_Foo #t_Foo =
  }
 
 [@@ FStar.Tactics.Typeclasses.tcinstance]
-let impl_1: Core.Ops.Arith.t_Mul #t_Foo #t_Foo =
+let impl_1: Core.Ops.Arith.t_Mul t_Foo t_Foo =
  {
  f_Output = t_Foo;
  f_mul_pre
@@ -131,7 +131,7 @@ let mutation_example
  (t_MyArray & t_Slice u8 & Alloc.Vec.t_Vec u8 Alloc.Alloc.t_Global)
 
 [@@ FStar.Tactics.Typeclasses.tcinstance]
-let impl: Core.Ops.Index.t_Index #t_MyArray #usize =
+let impl: Core.Ops.Index.t_Index t_MyArray usize =
  {
  f_Output = u8;
  f_index_pre = (fun (self: t_MyArray) (index: usize) -> index <. v_MAX);
@@ -145,7 +145,7 @@ module Attributes.Refinement_types
 open Core
 open FStar.Mul
 
-let t_BoundedU8 (v_MIN v_MAX: u8) = x: u8{x >=. v_MIN && x <=. v_MAX}
+let t_BoundedU8 (#v_MIN #v_MAX: u8) = x: u8{x >=. v_MIN && x <=. v_MAX}
 
 /// Example of a specific constraint on a value
 let t_CompressionFactor = x: u8{x =. 4uy || x =. 5uy || x =. 10uy || x =. 11uy}
@@ -158,7 +158,7 @@ let t_Even = x: u8{(x %! 2uy <: u8) =. 0uy}
 let t_FieldElement = x: u16{x <=. 2347us}
 
 /// A modular mutliplicative inverse
-let t_ModInverse (v_MOD: u32) =
+let t_ModInverse (#v_MOD: u32) =
  n:
  u32
  { (((cast (n <: u32) <: u128) *! (cast (v_MOD <: u32) <: u128) <: u128) %!

diff --git a/test-harness/src/snapshots/toolchain__generics into-fstar.snap b/test-harness/src/snapshots/toolchain__generics into-fstar.snap
@@ -45,22 +45,22 @@ module Generics
 open Core
 open FStar.Mul
 
-let impl__Bar__inherent_impl_generics (#v_T: Type0) (v_N: usize) (x: t_Array v_T v_N) : Prims.unit =
+let impl__Bar__inherent_impl_generics (#v_T: Type0) (#v_N: usize) (x: t_Array v_T v_N) : Prims.unit =
  ()
 
-class t_Foo (#v_Self: Type0) = {
- f_const_add_pre:v_N: usize -> v_Self -> bool;
- f_const_add_post:v_N: usize -> v_Self -> usize -> bool;
- f_const_add:v_N: usize -> x0: v_Self
- -> Prims.Pure usize (f_const_add_pre v_N x0) (fun result -> f_const_add_post v_N x0 result)
+class t_Foo (v_Self: Type0) = {
+ f_const_add_pre:#v_N: usize -> v_Self -> bool;
+ f_const_add_post:#v_N: usize -> v_Self -> usize -> bool;
+ f_const_add:#v_N: usize -> x0: v_Self
+ -> Prims.Pure usize (f_const_add_pre #v_N x0) (fun result -> f_const_add_post #v_N x0 result)
 }
 
 [@@ FStar.Tactics.Typeclasses.tcinstance]
-let impl_Foo_for_usize: t_Foo #usize =
+let impl_Foo_for_usize: t_Foo usize =
  {
- f_const_add_pre = (fun (v_N: usize) (self: usize) -> true);
- f_const_add_post = (fun (v_N: usize) (self: usize) (out: usize) -> true);
- f_const_add = fun (v_N: usize) (self: usize) -> self +! v_N
+ f_const_add_pre = (fun (#v_N: usize) (self: usize) -> true);
+ f_const_add_post = (fun (#v_N: usize) (self: usize) (out: usize) -> true);
+ f_const_add = fun (#v_N: usize) (self: usize) -> self +! v_N
  }
 
 let dup
@@ -69,12 +69,12 @@ let dup
  (x: v_T)
  : (v_T & v_T) = Core.Clone.f_clone #v_T x, Core.Clone.f_clone #v_T x <: (v_T & v_T)
 
-let f (v_N x: usize) : usize = (v_N +! v_N <: usize) +! x
+let f (#v_N x: usize) : usize = (v_N +! v_N <: usize) +! x
 
-let call_f (_: Prims.unit) : usize = (f (sz 10) (sz 3) <: usize) +! sz 3
+let call_f (_: Prims.unit) : usize = (f #(sz 10) (sz 3) <: usize) +! sz 3
 
 let g
- (v_N: usize)
+ (#v_N: usize)
  (#v_T: Type0)
  (#[FStar.Tactics.Typeclasses.tcresolve ()] i1: Core.Convert.t_Into v_T (t_Array usize v_N))
  (arr: v_T)
@@ -93,7 +93,7 @@ let g
  v_N
 
 let call_g (_: Prims.unit) : usize =
- (g (sz 3)
+ (g #(sz 3)
  #(t_Array usize (sz 3))
  (let list = [sz 42; sz 3; sz 49] in
  FStar.Pervasives.assert_norm (Prims.eq2 (List.Tot.length list) 3);
@@ -102,7 +102,7 @@ let call_g (_: Prims.unit) : usize =
  usize) +!
  sz 3
 
-let foo (v_LEN: usize) (arr: t_Array usize v_LEN) : usize =
+let foo (#v_LEN: usize) (arr: t_Array usize v_LEN) : usize =
  let acc:usize = v_LEN +! sz 9 in
  let acc:usize =
  Core.Iter.Traits.Iterator.f_fold (Core.Iter.Traits.Collect.f_into_iter #(Core.Ops.Range.t_Range
@@ -121,7 +121,7 @@ let foo (v_LEN: usize) (arr: t_Array usize v_LEN) : usize =
  acc
 
 let repeat
- (v_LEN: usize)
+ (#v_LEN: usize)
  (#v_T: Type0)
  (#[FStar.Tactics.Typeclasses.tcresolve ()] i1: Core.Marker.t_Copy v_T)
  (x: v_T)

diff --git a/test-harness/src/snapshots/toolchain__include-flag into-fstar.snap b/test-harness/src/snapshots/toolchain__include-flag into-fstar.snap
@@ -32,7 +32,7 @@ module Include_flag
 open Core
 open FStar.Mul
 
-class t_Trait (#v_Self: Type0) = { __marker_trait_t_Trait:Prims.unit }
+class t_Trait (v_Self: Type0) = { __marker_trait_t_Trait:Prims.unit }
 
 /// Indirect dependencies
 let main_a_a (_: Prims.unit) : Prims.unit = ()
@@ -76,7 +76,7 @@ let main_c (_: Prims.unit) : Prims.unit =
 type t_Foo = | Foo : t_Foo
 
 [@@ FStar.Tactics.Typeclasses.tcinstance]
-let impl_Trait_for_Foo: t_Trait #t_Foo = { __marker_trait = () }
+let impl_Trait_for_Foo: t_Trait t_Foo = { __marker_trait = () }
 
 /// Entrypoint
 let main (_: Prims.unit) : Prims.unit =

diff --git a/test-harness/src/snapshots/toolchain__interface-only into-fstar.snap b/test-harness/src/snapshots/toolchain__interface-only into-fstar.snap
@@ -54,7 +54,7 @@ type t_Bar = | Bar : t_Bar
 /// dropped. This might be a bit surprising: see
 /// https://github.com/hacspec/hax/issues/616.
 [@@ FStar.Tactics.Typeclasses.tcinstance]
-let impl: Core.Convert.t_From #t_Bar #Prims.unit =
+let impl: Core.Convert.t_From t_Bar Prims.unit =
  {
  f_from_pre = (fun ((): Prims.unit) -> true);
  f_from_post = (fun ((): Prims.unit) (out: t_Bar) -> true);
@@ -65,7 +65,7 @@ val from__from: u8 -> Prims.Pure t_Bar Prims.l_True (fun _ -> Prims.l_True)
 
 /// If you need to drop the body of a method, please hoist it:
 [@@ FStar.Tactics.Typeclasses.tcinstance]
-let impl_1: Core.Convert.t_From #t_Bar #u8 =
+let impl_1: Core.Convert.t_From t_Bar u8 =
  {
  f_from_pre = (fun (x: u8) -> true);
  f_from_post = (fun (x: u8) (out: t_Bar) -> true);

diff --git a/test-harness/src/snapshots/toolchain__loops into-fstar.snap b/test-harness/src/snapshots/toolchain__loops into-fstar.snap
@@ -37,7 +37,7 @@ open FStar.Mul
 
 let bool_returning (x: u8) : bool = x <. 10uy
 
-let chunks (v_CHUNK_LEN: usize) (arr: Alloc.Vec.t_Vec usize Alloc.Alloc.t_Global) : usize =
+let chunks (#v_CHUNK_LEN: usize) (arr: Alloc.Vec.t_Vec usize Alloc.Alloc.t_Global) : usize =
  let acc:usize = sz 0 in
  let chunks:Core.Slice.Iter.t_ChunksExact usize =
  Core.Slice.impl__chunks_exact #usize

diff --git a/test-harness/src/snapshots/toolchain__mut-ref-functionalization into-fstar.snap b/test-harness/src/snapshots/toolchain__mut-ref-functionalization into-fstar.snap
@@ -32,7 +32,7 @@ module Mut_ref_functionalization
 open Core
 open FStar.Mul
 
-class t_FooTrait (#v_Self: Type0) = {
+class t_FooTrait (v_Self: Type0) = {
  f_z_pre:v_Self -> bool;
  f_z_post:v_Self -> v_Self -> bool;
  f_z:x0: v_Self -> Prims.Pure v_Self (f_z_pre x0) (fun result -> f_z_post x0 result)
@@ -173,7 +173,7 @@ type t_Bar = {
 type t_Foo = { f_field:Alloc.Vec.t_Vec u8 Alloc.Alloc.t_Global }
 
 [@@ FStar.Tactics.Typeclasses.tcinstance]
-let impl_FooTrait_for_Foo: t_FooTrait #t_Foo =
+let impl_FooTrait_for_Foo: t_FooTrait t_Foo =
  {
  f_z_pre = (fun (self: t_Foo) -> true);
  f_z_post = (fun (self: t_Foo) (out: t_Foo) -> true);

diff --git a/test-harness/src/snapshots/toolchain__naming into-fstar.snap b/test-harness/src/snapshots/toolchain__naming into-fstar.snap
@@ -108,22 +108,22 @@ type t_Foo2 =
  | Foo2_A : t_Foo2
  | Foo2_B { f_x:usize }: t_Foo2
 
-class t_FooTrait (#v_Self: Type0) = { f_ASSOCIATED_CONSTANT:usize }
+class t_FooTrait (v_Self: Type0) = { f_ASSOCIATED_CONSTANT:usize }
 
-class t_T1 (#v_Self: Type0) = { __marker_trait_t_T1:Prims.unit }
+class t_T1 (v_Self: Type0) = { __marker_trait_t_T1:Prims.unit }
 
 [@@ FStar.Tactics.Typeclasses.tcinstance]
-let impl_T1_for_Foo: t_T1 #t_Foo = { __marker_trait = () }
+let impl_T1_for_Foo: t_T1 t_Foo = { __marker_trait = () }
 
 [@@ FStar.Tactics.Typeclasses.tcinstance]
-let impl_T1_for_tuple_Foo_u8: t_T1 #(t_Foo & u8) = { __marker_trait = () }
+let impl_T1_for_tuple_Foo_u8: t_T1 (t_Foo & u8) = { __marker_trait = () }
 
-class t_T2_for_a (#v_Self: Type0) = { __marker_trait_t_T2_for_a:Prims.unit }
+class t_T2_for_a (v_Self: Type0) = { __marker_trait_t_T2_for_a:Prims.unit }
 
-class t_T3_e_for_a (#v_Self: Type0) = { __marker_trait_t_T3_e_for_a:Prims.unit }
+class t_T3_e_for_a (v_Self: Type0) = { __marker_trait_t_T3_e_for_a:Prims.unit }
 
 [@@ FStar.Tactics.Typeclasses.tcinstance]
-let impl_T3_e_e_for_a_for_Foo: t_T3_e_for_a #t_Foo = { __marker_trait = () }
+let impl_T3_e_e_for_a_for_Foo: t_T3_e_for_a t_Foo = { __marker_trait = () }
 
 let v_INHERENT_CONSTANT: usize = sz 3
 
@@ -146,7 +146,7 @@ let reserved_names (v_val v_noeq v_of: u8) : u8 = (v_val +! v_noeq <: u8) +! v_o
 type t_Arity1 (v_T: Type0) = | Arity1 : v_T -> t_Arity1 v_T
 
 [@@ FStar.Tactics.Typeclasses.tcinstance]
-let impl_T2_e_for_a_for_Arity1_of_tuple_Foo_u8: t_T2_for_a #(t_Arity1 (t_Foo & u8)) =
+let impl_T2_e_for_a_for_Arity1_of_tuple_Foo_u8: t_T2_for_a (t_Arity1 (t_Foo & u8)) =
  { __marker_trait = () }
 
 type t_B = | B : t_B