From ac4230d9c0a10867024e5fdbb42d5eee6b00be17 Mon Sep 17 00:00:00 2001 From: Lucas Franceschino Date: Thu, 16 May 2024 09:37:07 +0200 Subject: [PATCH 1/2] feat(engine/fstar): add a prelude that explicits typeclass dependencies --- engine/backends/fstar/fstar_backend.ml | 69 +++++++++++++++---- engine/hax-engine.opam | 2 +- .../toolchain__literals into-fstar.snap | 6 ++ .../toolchain__traits into-fstar.snap | 57 +++++++++++++++ tests/traits/src/lib.rs | 24 ++++++- 5 files changed, 144 insertions(+), 14 deletions(-) diff --git a/engine/backends/fstar/fstar_backend.ml b/engine/backends/fstar/fstar_backend.ml index 9614a087a..1d907c44d 100644 --- a/engine/backends/fstar/fstar_backend.ml +++ b/engine/backends/fstar/fstar_backend.ml @@ -78,6 +78,7 @@ module FStarNamePolicy = struct end module U = Ast_utils.MakeWithNamePolicy (InputLanguage) (FStarNamePolicy) +module Visitors = Ast_visitors.Make (InputLanguage) open AST module F = Fstar_ast @@ -1434,8 +1435,52 @@ let strings_of_item ~signature_only (bo : BackendOptions.t) m items if interface_mode then [ (`Impl s, `Newline); (`Intf s, `Newline) ] else [ (`Impl s, `Newline) ]) -let string_of_items ~signature_only (bo : BackendOptions.t) m items : +(** Convers a namespace to a module name *) +let module_name (ns : string * string list) : string = + String.concat ~sep:"." + (List.map ~f:(map_first_letter String.uppercase) (fst ns :: snd ns)) + +let string_of_items ~signature_only ~mod_name (bo : BackendOptions.t) m items : string * string = + let collect_trait_goal_idents = + object + inherit [_] Visitors.reduce as super + inherit [_] U.Sets.Concrete_ident.monoid as _m + + method! visit_trait_goal (_env : unit) x = + Set.singleton (module Concrete_ident) x.trait + end + in + let header = + let lines = + List.map ~f:(collect_trait_goal_idents#visit_item ()) items + |> Set.union_list (module Concrete_ident) + |> Set.map + (module String) + ~f:(fun i -> U.Concrete_ident_view.to_namespace i |> module_name) + |> Fn.flip Set.remove mod_name + |> Set.to_list + |> List.filter ~f:(fun m -> + (* Special treatment for modules handled specifically in our F* libraries *) + String.is_prefix ~prefix:"Core." m |> not + && String.is_prefix ~prefix:"Alloc." m |> not + && String.equal "Hax_lib.Int" m |> not) + |> List.map ~f:(fun mod_path -> "let open " ^ mod_path ^ " in") + in + match lines with + | [] -> "" + | _ -> + "let _ =" + ^ ([ + "(* This module has implicit dependencies, here we make them \ + explicit. *)"; + "(* The implicit dependencies arise from typeclasses instances. *)"; + ] + @ lines @ [ "()" ] + |> List.map ~f:(( ^ ) "\n ") + |> String.concat ~sep:"") + ^ "\n\n" + in let strings = List.concat_map ~f:(strings_of_item ~signature_only bo m items) items |> List.map @@ -1456,11 +1501,14 @@ let string_of_items ~signature_only (bo : BackendOptions.t) m items : strings in let n = List.length l - 1 in - List.mapi - ~f:(fun i (s, space) -> - s ^ if [%matches? `NoNewline] space || [%eq: int] i n then "" else "\n") - l - |> String.concat ~sep:"\n" + let lines = + List.mapi + ~f:(fun i (s, space) -> + s + ^ if [%matches? `NoNewline] space || [%eq: int] i n then "" else "\n") + l + in + match lines with [] -> "" | _ -> header ^ String.concat ~sep:"\n" lines in ( string_for (function `Impl s -> Some s | _ -> None), string_for (function `Intf s -> Some s | _ -> None) ) @@ -1490,13 +1538,10 @@ let translate m (bo : BackendOptions.t) (items : AST.item list) : in List.exists ~f:contains_dropped_body items in - let mod_name = - String.concat ~sep:"." - (List.map - ~f:(map_first_letter String.uppercase) - (fst ns :: snd ns)) + let mod_name = module_name ns in + let impl, intf = + string_of_items ~signature_only ~mod_name bo m items in - let impl, intf = string_of_items ~signature_only bo m items in let make ~ext body = if String.is_empty body then None else diff --git a/engine/hax-engine.opam b/engine/hax-engine.opam index 72ba3a4c3..dfa6b8be5 100644 --- a/engine/hax-engine.opam +++ b/engine/hax-engine.opam @@ -60,4 +60,4 @@ build: [ dev-repo: "git+https://github.com/hacspec/hax.git" depexts: [ ["nodejs"] {} -] +] \ No newline at end of file diff --git a/test-harness/src/snapshots/toolchain__literals into-fstar.snap b/test-harness/src/snapshots/toolchain__literals into-fstar.snap index 15c8b19b3..1c0725e11 100644 --- a/test-harness/src/snapshots/toolchain__literals into-fstar.snap +++ b/test-harness/src/snapshots/toolchain__literals into-fstar.snap @@ -35,6 +35,12 @@ module Literals open Core open FStar.Mul +let _ = + (* This module has implicit dependencies, here we make them explicit. *) + (* The implicit dependencies arise from typeclasses instances. *) + let open Num_bigint.Bigint.Convert in + () + let casts (x8: u8) (x16: u16) (x32: u32) (x64: u64) (xs: usize) : Prims.unit = let (_: u64):u64 = ((((cast (x8 <: u8) <: u64) +! (cast (x16 <: u16) <: u64) <: u64) +! (cast (x32 <: u32) <: u64) diff --git a/test-harness/src/snapshots/toolchain__traits into-fstar.snap b/test-harness/src/snapshots/toolchain__traits into-fstar.snap index 5b8ac2c47..24a197840 100644 --- a/test-harness/src/snapshots/toolchain__traits into-fstar.snap +++ b/test-harness/src/snapshots/toolchain__traits into-fstar.snap @@ -116,6 +116,63 @@ let v__f (#v_X: Type0) (#[FStar.Tactics.Typeclasses.tcresolve ()] i1: t_Foo v_X let _:u8 = f_to_t #v_X #u8 x in () ''' +"Traits.Implicit_dependencies_issue_667_.Define_type.fst" = ''' +module Traits.Implicit_dependencies_issue_667_.Define_type +#set-options "--fuel 0 --ifuel 1 --z3rlimit 15" +open Core +open FStar.Mul + +type t_MyType = | MyType : t_MyType +''' +"Traits.Implicit_dependencies_issue_667_.Impl_type.fst" = ''' +module Traits.Implicit_dependencies_issue_667_.Impl_type +#set-options "--fuel 0 --ifuel 1 --z3rlimit 15" +open Core +open FStar.Mul + +[@@ FStar.Tactics.Typeclasses.tcinstance] +let impl: Traits.Implicit_dependencies_issue_667_.Trait_definition.t_MyTrait +Traits.Implicit_dependencies_issue_667_.Define_type.t_MyType = + { + f_my_method_pre + = + (fun (self: Traits.Implicit_dependencies_issue_667_.Define_type.t_MyType) -> true); + f_my_method_post + = + (fun (self: Traits.Implicit_dependencies_issue_667_.Define_type.t_MyType) (out: Prims.unit) -> + true); + f_my_method = fun (self: Traits.Implicit_dependencies_issue_667_.Define_type.t_MyType) -> () + } +''' +"Traits.Implicit_dependencies_issue_667_.Trait_definition.fst" = ''' +module Traits.Implicit_dependencies_issue_667_.Trait_definition +#set-options "--fuel 0 --ifuel 1 --z3rlimit 15" +open Core +open FStar.Mul + +class t_MyTrait (v_Self: Type0) = { + f_my_method_pre:v_Self -> bool; + f_my_method_post:v_Self -> Prims.unit -> bool; + f_my_method:x0: v_Self + -> Prims.Pure Prims.unit (f_my_method_pre x0) (fun result -> f_my_method_post x0 result) +} +''' +"Traits.Implicit_dependencies_issue_667_.Use_type.fst" = ''' +module Traits.Implicit_dependencies_issue_667_.Use_type +#set-options "--fuel 0 --ifuel 1 --z3rlimit 15" +open Core +open FStar.Mul + +let _ = + (* This module has implicit dependencies, here we make them explicit. *) + (* The implicit dependencies arise from typeclasses instances. *) + let open Traits.Implicit_dependencies_issue_667_.Impl_type in + () + +let some_function (x: Traits.Implicit_dependencies_issue_667_.Define_type.t_MyType) : Prims.unit = + Traits.Implicit_dependencies_issue_667_.Trait_definition.f_my_method #Traits.Implicit_dependencies_issue_667_.Define_type.t_MyType + x +''' "Traits.Unconstrainted_types_issue_677_.fst" = ''' module Traits.Unconstrainted_types_issue_677_ #set-options "--fuel 0 --ifuel 1 --z3rlimit 15" diff --git a/tests/traits/src/lib.rs b/tests/traits/src/lib.rs index 9f38e5e0e..9821c42d0 100644 --- a/tests/traits/src/lib.rs +++ b/tests/traits/src/lib.rs @@ -109,7 +109,6 @@ mod for_clauses { } } -// From issue #677 mod unconstrainted_types_issue_677 { trait PolyOp { fn op(x: u32, y: u32) -> u32; @@ -141,3 +140,26 @@ mod unconstrainted_types_issue_677 { assert!(both(10) == (20, 100)); } } + +// From issue_667 +mod implicit_dependencies_issue_667 { + mod trait_definition { + pub trait MyTrait { + fn my_method(self); + } + } + mod define_type { + pub struct MyType; + } + mod impl_type { + impl super::trait_definition::MyTrait for super::define_type::MyType { + fn my_method(self) {} + } + } + mod use_type { + fn some_function(x: super::define_type::MyType) { + use super::trait_definition::MyTrait; + x.my_method() + } + } +} From 792f200701d158799fcc777bdf9b758a6f77a571 Mon Sep 17 00:00:00 2001 From: Lucas Franceschino Date: Thu, 16 May 2024 09:37:49 +0200 Subject: [PATCH 2/2] feat(hax-lib): drop explicit dependency to `num_bigint` in interface --- hax-lib/src/int/mod.rs | 35 ++++++++++++++++--- .../toolchain__literals into-coq.snap | 16 ++++----- .../toolchain__literals into-fstar.snap | 22 +++++------- 3 files changed, 46 insertions(+), 27 deletions(-) diff --git a/hax-lib/src/int/mod.rs b/hax-lib/src/int/mod.rs index c7a1eea81..25e0939a0 100644 --- a/hax-lib/src/int/mod.rs +++ b/hax-lib/src/int/mod.rs @@ -89,13 +89,38 @@ pub trait Concretization { fn concretize(self) -> T; } -impl> Abstraction for T { - type AbstractType = Int; - fn lift(self) -> Self::AbstractType { - Int::new(self.into()) - } +/// Instead of defining one overloaded instance, which relies +/// explicitely on `num_bigint`: +/// +/// ```ignore +/// impl> Abstraction for T { +/// type AbstractType = Int; +/// fn lift(self) -> Self::AbstractType { +/// Int::new(self.into()) +/// } +/// } +/// ``` +/// +/// We define an instance per machine type: we don't want the +/// interface of this module to rely specifically on +/// `num_bigint`. This module should be a very thin layer. +macro_rules! implement_abstraction { + ($ty:ident) => { + impl Abstraction for $ty { + type AbstractType = Int; + fn lift(self) -> Self::AbstractType { + Int::new(num_bigint::BigInt::from(self)) + } + } + }; + ($($ty:ident)*) => { + $(implement_abstraction!($ty);)* + }; } +implement_abstraction!(u8 u16 u32 u64 u128 usize); +implement_abstraction!(i8 i16 i32 i64 i128 isize); + macro_rules! implement_concretize { ($ty:ident $method:ident) => { impl Concretization<$ty> for Int { diff --git a/test-harness/src/snapshots/toolchain__literals into-coq.snap b/test-harness/src/snapshots/toolchain__literals into-coq.snap index f1ba1ef5d..fa56c7eca 100644 --- a/test-harness/src/snapshots/toolchain__literals into-coq.snap +++ b/test-harness/src/snapshots/toolchain__literals into-coq.snap @@ -58,14 +58,6 @@ Definition fn_pointer_cast (_ : unit) : unit := x : int32 -> int32 in tt. -Definition numeric (_ : unit) : unit := - let (_ : uint_size) := (@repr WORDSIZE32 123) : uint_size in - let (_ : uint_size) := (@repr WORDSIZE32 42) : uint_size in - let (_ : uint_size) := (@repr WORDSIZE32 42) : uint_size in - let (_ : int32) := (@repr WORDSIZE32 42) : int32 in - let (_ : int128) := (@repr WORDSIZE128 22222222222222222222) : int128 in - tt. - Definition math_integers (x : t_Int_t) : int8 := let (_ : t_Int_t) := f_lift (@repr WORDSIZE32 3) : t_Int_t in let _ := (impl__Int___unsafe_from_str -340282366920938463463374607431768211455000)>.?(impl__Int___unsafe_from_str 340282366920938463463374607431768211455000) : bool in @@ -90,6 +82,14 @@ Definition math_integers (x : t_Int_t) : int8 := let (_ : uint_size) := impl__Int__to_usize x : uint_size in impl__Int__to_u8 (x.+(x.*x)). +Definition numeric (_ : unit) : unit := + let (_ : uint_size) := (@repr WORDSIZE32 123) : uint_size in + let (_ : uint_size) := (@repr WORDSIZE32 42) : uint_size in + let (_ : uint_size) := (@repr WORDSIZE32 42) : uint_size in + let (_ : int32) := (@repr WORDSIZE32 42) : int32 in + let (_ : int128) := (@repr WORDSIZE128 22222222222222222222) : int128 in + tt. + Definition empty_array (_ : unit) : unit := let (_ : seq int8) := unsize !TODO empty array! : seq int8 in tt. diff --git a/test-harness/src/snapshots/toolchain__literals into-fstar.snap b/test-harness/src/snapshots/toolchain__literals into-fstar.snap index 1c0725e11..f7bfd661b 100644 --- a/test-harness/src/snapshots/toolchain__literals into-fstar.snap +++ b/test-harness/src/snapshots/toolchain__literals into-fstar.snap @@ -35,12 +35,6 @@ module Literals open Core open FStar.Mul -let _ = - (* This module has implicit dependencies, here we make them explicit. *) - (* The implicit dependencies arise from typeclasses instances. *) - let open Num_bigint.Bigint.Convert in - () - let casts (x8: u8) (x16: u16) (x32: u32) (x64: u64) (xs: usize) : Prims.unit = let (_: u64):u64 = ((((cast (x8 <: u8) <: u64) +! (cast (x16 <: u16) <: u64) <: u64) +! (cast (x32 <: u32) <: u64) @@ -115,14 +109,6 @@ let fn_pointer_cast (_: Prims.unit) : Prims.unit = let (f: (u32 -> u32)): u32 -> u32 = fun x -> x in () -let numeric (_: Prims.unit) : Prims.unit = - let (_: usize):usize = sz 123 in - let (_: isize):isize = isz (-42) in - let (_: isize):isize = isz 42 in - let (_: i32):i32 = (-42l) in - let (_: u128):u128 = pub_u128 22222222222222222222 in - () - let math_integers (x: Hax_lib.Int.t_Int) : Prims.Pure u8 (requires x > (0 <: Hax_lib.Int.t_Int) && x < (16 <: Hax_lib.Int.t_Int)) @@ -153,6 +139,14 @@ let math_integers (x: Hax_lib.Int.t_Int) let (_: usize):usize = Hax_lib.Int.impl__Int__to_usize x in Hax_lib.Int.impl__Int__to_u8 (x + (x * x <: Hax_lib.Int.t_Int) <: Hax_lib.Int.t_Int) +let numeric (_: Prims.unit) : Prims.unit = + let (_: usize):usize = sz 123 in + let (_: isize):isize = isz (-42) in + let (_: isize):isize = isz 42 in + let (_: i32):i32 = (-42l) in + let (_: u128):u128 = pub_u128 22222222222222222222 in + () + let empty_array (_: Prims.unit) : Prims.unit = let (_: t_Slice u8):t_Slice u8 = Rust_primitives.unsize (let list:Prims.list u8 = [] in