Fix #296

engine/backends/coq/coq/coq_backend.ml

@@ -40,7 +40,8 @@ module SubtypeToInputLanguage
              and type while_loop = Features.Off.while_loop
              and type for_index_loop = Features.Off.for_index_loop
              and type quote = Features.Off.quote
-             and type state_passing_loop = Features.Off.state_passing_loop) =
+             and type state_passing_loop = Features.Off.state_passing_loop
+             and type dyn = Features.Off.dyn) =
 struct
   module FB = InputLanguage
 
@@ -714,6 +715,7 @@ module TransformToInputLanguage =
   |> Phases.Reject.EarlyExit
   |> Phases.Functionalize_loops
   |> Phases.Reject.As_pattern
+  |> Phases.Reject.Dyn
   |> SubtypeToInputLanguage
   |> Identity
   ]

engine/backends/coq/ssprove/ssprove_backend.ml

@@ -40,7 +40,8 @@ module SubtypeToInputLanguage
              and type arbitrary_lhs = Features.Off.arbitrary_lhs
              and type nontrivial_lhs = Features.Off.nontrivial_lhs
              and type quote = Features.Off.quote
-             and type block = Features.Off.block) =
+             and type block = Features.Off.block
+             and type dyn = Features.Off.dyn) =
 struct
   module FB = InputLanguage
 
@@ -580,6 +581,7 @@ module TransformToInputLanguage (* : PHASE *) =
     |> Phases.Reject.EarlyExit
     (* |> Phases.Functionalize_loops *)
     |> Phases.Reject.As_pattern
+    |> Phases.Reject.Dyn
     |> SubtypeToInputLanguage
     |> Identity
   ]

engine/backends/easycrypt/easycrypt_backend.ml

@@ -58,6 +58,7 @@ module RejectNotEC (FA : Features.T) = struct
         let for_loop = reject
         let while_loop = reject
         let quote = reject
+        let dyn = reject
         let construct_base _ _ = Features.On.construct_base
         let for_index_loop _ _ = Features.On.for_index_loop
 

engine/backends/fstar/fstar_backend.ml

@@ -12,6 +12,7 @@ include
       include On.Macro
       include On.Construct_base
       include On.Quote
+      include On.Dyn
     end)
     (struct
       let backend = Diagnostics.Backend.FStar
@@ -54,6 +55,7 @@ struct
         include Features.SUBTYPE.On.Slice
         include Features.SUBTYPE.On.Macro
         include Features.SUBTYPE.On.Quote
+        include Features.SUBTYPE.On.Dyn
       end)
 
   let metadata = Phase_utils.Metadata.make (Reject (NotInBackendLang backend))
@@ -311,8 +313,28 @@ struct
                  (impl, F.lid [ U.Concrete_ident_view.to_definition_name item ])
         | None -> F.term @@ F.AST.Wild)
     | TOpaque s -> F.term @@ F.AST.Wild
+    | TDyn { goals; _ } ->
+        let traits = List.map ~f:(pdyn_trait_goal span) goals in
+        let dyn = F.AST.Var (F.lid [ "dyn" ]) |> F.term in
+        let length =
+          F.AST.Const
+            (FStar_Const.Const_int (List.length goals |> Int.to_string, None))
+          |> F.term
+        in
+        F.mk_e_app dyn (length :: traits)
     | _ -> .
 
+  and pdyn_trait_goal span (goal : dyn_trait_goal) =
+    (* This introduces a potential shadowing *)
+    let type_var = "z" in
+    let pat = F.pat @@ F.AST.PatVar (F.id type_var, None, []) in
+    let trait = F.AST.Var (pconcrete_ident goal.trait) |> F.term in
+    let args =
+      (F.AST.Var (F.lid [ type_var ]) |> F.term)
+      :: List.map ~f:(pgeneric_value span) goal.non_self_args
+    in
+    F.mk_e_abs [ pat ] (F.mk_e_app trait args)
+
   and pimpl_expr span (ie : impl_expr) =
     let some = Option.some in
     let hax_unstable_impl_exprs = false in

engine/backends/proverif/proverif_backend.ml

@@ -76,6 +76,7 @@ struct
         let monadic_action = reject
         let monadic_binding = reject
         let block = reject
+        let dyn = reject
         let metadata = Phase_reject.make_metadata (NotInBackendLang ProVerif)
       end)
 
@@ -900,6 +901,7 @@ module TransformToInputLanguage =
   |> Phases.Drop_needless_returns
   |> Phases.Local_mutation
   |> Phases.Reject.Continue
+  |> Phases.Reject.Dyn
   |> SubtypeToInputLanguage
   |> Identity
   ]

engine/lib/ast.ml

@@ -131,6 +131,7 @@ functor
       | TArrow of ty list * ty
       | TAssociatedType of { impl : impl_expr; item : concrete_ident }
       | TOpaque of concrete_ident
+      | TDyn of { witness : F.dyn; goals : dyn_trait_goal list }
 
     and generic_value =
       | GLifetime of { lt : todo; witness : F.lifetime }
@@ -156,6 +157,13 @@ functor
       `SomeTy: Foo<T0, ..., Tn>`). An `impl_expr` "inhabits" a
       `trait_goal`. *)
 
+    and dyn_trait_goal = {
+      trait : concrete_ident;
+      non_self_args : generic_value list;
+    }
+    (** A dyn trait: [Foo<_, T0, ..., Tn>]. The generic arguments are known 
+      but the actual type implementing the trait is known only dynamically. *)
+
     and impl_ident = { goal : trait_goal; name : string }
     (** An impl identifier [{goal; name}] can be:
           {ul

engine/lib/diagnostics.ml

@@ -15,6 +15,7 @@ module Phase = struct
       | RawOrMutPointer
       | EarlyExit
       | AsPattern
+      | Dyn
     [@@deriving show { with_path = false }, eq, yojson, compare, hash, sexp]
 
     let display = function

engine/lib/features.ml

@@ -23,7 +23,8 @@ loop,
   monadic_action,
   monadic_binding,
   quote,
-  block]
+  block,
+  dyn]
 
 module Full = On
 

engine/lib/generic_printer/generic_printer.ml

@@ -141,6 +141,7 @@ module Make (F : Features.T) (View : Concrete_ident.VIEW_API) = struct
             | TAssociatedType _ -> string "assoc_type!()"
             | TOpaque _ -> string "opaque_type!()"
             | TApp _ -> super#ty ctx ty
+            | TDyn _ -> string "" (* TODO *)
 
         method! expr' : par_state -> expr' fn =
           fun ctx e ->

engine/lib/import_thir.ml

@@ -1005,7 +1005,26 @@ end) : EXPR = struct
         (* TODO: [id] might not unique *)
         TParam { name; id = Local_ident.mk_id Typ (MyInt64.to_int_exn index) }
     | Error -> unimplemented [ span ] "type Error"
-    | Dynamic _ -> unimplemented [ span ] "type Dynamic"
+    | Dynamic (predicates, _region, Dyn) -> (
+        let goals, non_traits =
+          List.partition_map
+            ~f:(fun pred ->
+              match pred.value with
+              | Trait { args; def_id } ->
+                  let goal : dyn_trait_goal =
+                    {
+                      trait = Concrete_ident.of_def_id Trait def_id;
+                      non_self_args = List.map ~f:(c_generic_value span) args;
+                    }
+                  in
+                  First goal
+              | _ -> Second ())
+            predicates
+        in
+        match non_traits with
+        | [] -> TDyn { witness = W.dyn; goals }
+        | _ -> unimplemented [ span ] "type Dyn with non trait predicate")
+    | Dynamic (_, _, DynStar) -> unimplemented [ span ] "type DynStar"
     | Coroutine _ -> unimplemented [ span ] "type Coroutine"
     | Placeholder _ -> unimplemented [ span ] "type Placeholder"
     | Bound _ -> unimplemented [ span ] "type Bound"

engine/lib/phases/phase_drop_references.ml

@@ -51,6 +51,13 @@ struct
         args = List.filter_map ~f:(dgeneric_value span) r.args;
       }
 
+    and ddyn_trait_goal (span : span) (r : A.dyn_trait_goal) : B.dyn_trait_goal
+        =
+      {
+        trait = r.trait;
+        non_self_args = List.filter_map ~f:(dgeneric_value span) r.non_self_args;
+      }
+
     and dpat' (span : span) (p : A.pat') : B.pat' =
       match p with
       | [%inline_arms "dpat'.*" - PBinding - PDeref] -> auto

engine/lib/phases/phase_reject.ml

@@ -98,3 +98,21 @@ module As_pattern (FA : Features.T) = struct
         let metadata = make_metadata AsPattern
       end)
 end
+
+module Dyn (FA : Features.T) = struct
+  module FB = struct
+    include FA
+    include Features.Off.Dyn
+  end
+
+  include
+    Feature_gate.Make (FA) (FB)
+      (struct
+        module A = FA
+        module B = FB
+        include Feature_gate.DefaultSubtype
+
+        let dyn = reject
+        let metadata = make_metadata Dyn
+      end)
+end

engine/lib/print_rust.ml

@@ -166,6 +166,19 @@ module Raw = struct
         !"arrow!(" & arrow & !")"
     | TAssociatedType _ -> !"proj_asso_type!()"
     | TOpaque ident -> !(Concrete_ident_view.show ident)
+    | TDyn { goals; _ } ->
+        let goals =
+          concat ~sep:!" + " (List.map ~f:(pdyn_trait_goal span) goals)
+        in
+        !"dyn(" & goals & !")"
+
+  and pdyn_trait_goal span { trait; non_self_args } =
+    let ( ! ) = pure span in
+    let args =
+      List.map ~f:(pgeneric_value span) non_self_args |> concat ~sep:!", "
+    in
+    !(Concrete_ident_view.show trait)
+    & if List.is_empty args then empty else !"<" & args & !">"
 
   and pgeneric_value span (e : generic_value) : AnnotatedString.t =
     match e with

engine/lib/subtype.ml

@@ -47,6 +47,18 @@ struct
     | TOpaque ident -> TOpaque ident
     | TRawPointer { witness } ->
         TRawPointer { witness = S.raw_pointer span witness }
+    | TDyn { witness; goals } ->
+        TDyn
+          {
+            witness = S.dyn span witness;
+            goals = List.map ~f:(ddyn_trait_goal span) goals;
+          }
+
+  and ddyn_trait_goal (span : span) (r : A.dyn_trait_goal) : B.dyn_trait_goal =
+    {
+      trait = r.trait;
+      non_self_args = List.map ~f:(dgeneric_value span) r.non_self_args;
+    }
 
   and dtrait_goal (span : span) (r : A.trait_goal) : B.trait_goal =
     { trait = r.trait; args = List.map ~f:(dgeneric_value span) r.args }

test-harness/src/snapshots/toolchain__dyn into-fstar.snap

@@ -0,0 +1,83 @@
+---
+source: test-harness/src/harness.rs
+expression: snapshot
+info:
+  kind:
+    Translate:
+      backend: fstar
+  info:
+    name: dyn
+    manifest: dyn/Cargo.toml
+    description: ~
+  spec:
+    optional: false
+    broken: false
+    issue_id: ~
+    positive: true
+    snapshot:
+      stderr: false
+      stdout: true
+    include_flag: ~
+    backend_options: ~
+---
+exit = 0
+
+[stdout]
+diagnostics = []
+
+[stdout.files]
+"Dyn.fst" = '''
+module Dyn
+#set-options "--fuel 0 --ifuel 1 --z3rlimit 15"
+open Core
+open FStar.Mul
+
+class t_Printable (v_Self: Type0) (v_S: Type0) = {
+  f_stringify_pre:v_Self -> bool;
+  f_stringify_post:v_Self -> v_S -> bool;
+  f_stringify:x0: v_Self
+    -> Prims.Pure v_S (f_stringify_pre x0) (fun result -> f_stringify_post x0 result)
+}
+
+[@@ FStar.Tactics.Typeclasses.tcinstance]
+let impl: t_Printable i32 Alloc.String.t_String =
+  {
+    f_stringify_pre = (fun (self: i32) -> true);
+    f_stringify_post = (fun (self: i32) (out: Alloc.String.t_String) -> true);
+    f_stringify
+    =
+    fun (self: i32) -> Alloc.String.f_to_string #i32 #FStar.Tactics.Typeclasses.solve self
+  }
+
+let print
+      (a:
+          Alloc.Boxed.t_Box (dyn 1 (fun z -> t_Printable z Alloc.String.t_String))
+            Alloc.Alloc.t_Global)
+    : Prims.unit =
+  let _:Prims.unit =
+    Std.Io.Stdio.v__print (Core.Fmt.impl_2__new_v1 (sz 2)
+          (sz 1)
+          (let list = [""; "\n"] in
+            FStar.Pervasives.assert_norm (Prims.eq2 (List.Tot.length list) 2);
+            Rust_primitives.Hax.array_of_list 2 list)
+          (let list =
+              [
+                Core.Fmt.Rt.impl_1__new_display #Alloc.String.t_String
+                  (f_stringify #(dyn 1 (fun z -> t_Printable z Alloc.String.t_String))
+                      #Alloc.String.t_String
+                      #FStar.Tactics.Typeclasses.solve
+                      a
+                    <:
+                    Alloc.String.t_String)
+                <:
+                Core.Fmt.Rt.t_Argument
+              ]
+            in
+            FStar.Pervasives.assert_norm (Prims.eq2 (List.Tot.length list) 1);
+            Rust_primitives.Hax.array_of_list 1 list)
+        <:
+        Core.Fmt.t_Arguments)
+  in
+  let _:Prims.unit = () in
+  ()
+'''

tests/Cargo.toml

@@ -19,6 +19,7 @@ members = [
         "attribute-opaque",
         "raw-attributes",
         "traits",
+        "dyn",
         "reordering",
         "nested-derefs",
         "proverif-minimal",

tests/dyn/Cargo.toml

@@ -0,0 +1,9 @@
+[package]
+name = "dyn"
+version = "0.1.0"
+edition = "2021"
+
+[dependencies]
+
+[package.metadata.hax-tests]
+into."fstar" = { broken = false, snapshot = "stdout", issue_id = "296" }

tests/dyn/src/lib.rs

@@ -0,0 +1,15 @@
+#![allow(dead_code)]
+
+pub trait Printable<S> {
+    fn stringify(&self) -> S;
+}
+
+impl Printable<String> for i32 {
+    fn stringify(&self) -> String {
+        self.to_string()
+    }
+}
+
+pub fn print(a: Box<dyn Printable<String>>) {
+    println!("{}", a.stringify());
+}