diff --git a/engine/lib/dependencies.ml b/engine/lib/dependencies.ml index e46fcb555..0aa79f898 100644 --- a/engine/lib/dependencies.ml +++ b/engine/lib/dependencies.ml @@ -33,482 +33,557 @@ module Make (F : Features.T) = struct module Attrs = Attr_payloads.Make (F) (Error) - let uid_associated_items (items : item list) : attrs -> item list = - let open Attrs.WithItems (struct - let items = items - end) in - raw_associated_item >> List.map ~f:(snd >> item_of_uid) - - module ItemGraph = struct - module G = Graph.Persistent.Digraph.Concrete (Concrete_ident) - module Topological = Graph.Topological.Make_stable (G) - module Oper = Graph.Oper.P (G) - - let vertices_of_item (i : item) : G.V.t list = - let ( @ ) = Set.union in - let v = U.Reducers.collect_concrete_idents in - let concat_map f = - List.map ~f >> Set.union_list (module Concrete_ident) - in - let set = - match i.v with - | Fn { name = _; generics; body; params; _ } -> - v#visit_generics () generics - @ v#visit_expr () body - @ concat_map (v#visit_param ()) params - | TyAlias { name = _; generics; ty } -> - v#visit_generics () generics @ v#visit_ty () ty - | Type { name = _; generics; variants; is_struct = (_ : bool) } -> - v#visit_generics () generics - @ concat_map (v#visit_variant ()) variants - | IMacroInvokation { macro; argument = (_ : string); span; witness = _ } - -> - v#visit_concrete_ident () macro @ v#visit_span () span - | Trait { name = _; generics; items; safety = _ } -> - v#visit_generics () generics - @ concat_map (v#visit_trait_item ()) items - | Impl { generics; self_ty; of_trait; items; parent_bounds; safety = _ } - -> - v#visit_generics () generics - @ v#visit_ty () self_ty - @ v#visit_concrete_ident () (fst of_trait) - @ concat_map (v#visit_generic_value ()) (snd of_trait) - @ concat_map (v#visit_impl_item ()) items - @ concat_map - (fun (ie, ii) -> - v#visit_impl_expr () ie @ v#visit_impl_ident () ii) - parent_bounds - | Alias { name = _; item } -> v#visit_concrete_ident () item - | Use _ | Quote _ | HaxError _ | NotImplementedYet -> - Set.empty (module Concrete_ident) - in - set |> Set.to_list - - let vertices_of_items ~uid_associated_items (items : item list) : G.E.t list - = - List.concat_map - ~f:(fun i -> - let assoc = - uid_associated_items i.attrs |> List.map ~f:(fun i -> i.ident) + module type WITH_ITEMS = sig + val uid_associated_items : item list -> Ast.attrs -> item list + val bundle_cyclic_modules : item list -> item list + val sort : item list -> item list + val recursive_bundles : item list -> item list list * item list + + val filter_by_inclusion_clauses : + Types.inclusion_clause list -> item list -> item list + end + + module WithItems (CTX : sig + val items : item list + end) = + struct + let uid_associated_items : attrs -> item list = + let open Attrs.WithItems (struct + let items = CTX.items + end) in + raw_associated_item >> List.map ~f:(snd >> item_of_uid) + + (** `Ordered_concrete_ident` is just like `Concrete_ident`, but + the semantics of comparing two concrete idents is now defined in + term of which comes first in `CTX.items`. If we compare items not + present in `CTX.items` we revert to `Concrete_ident.compare`. *) + module Ordered_concrete_ident = struct + include Concrete_ident + + open struct + let order : t -> int option = + let table : (t, int) Hashtbl.t = + let table = Hashtbl.create (module Concrete_ident) in + List.iteri CTX.items ~f:(fun i item -> + Hashtbl.set ~key:item.ident ~data:i table); + table in - vertices_of_item i @ assoc |> List.map ~f:(Fn.const i.ident &&& Fn.id)) - items + Hashtbl.find table + end - let of_items ~original_items (items : item list) : G.t = - let init = - List.fold ~init:G.empty ~f:(fun g -> ident_of >> G.add_vertex g) items - in - let uid_associated_items = uid_associated_items original_items in - vertices_of_items ~uid_associated_items items - |> List.fold ~init ~f:(G.add_edge >> uncurry) - - let transitive_dependencies_of (g : G.t) (selection : Concrete_ident.t list) - : Concrete_ident.t Hash_set.t = - let set = Hash_set.create (module Concrete_ident) in - let rec visit vertex = - if Hash_set.mem set vertex |> not then ( - Hash_set.add set vertex; - G.iter_succ visit g vertex) - in - List.filter ~f:(G.mem_vertex g) selection |> List.iter ~f:visit; - set + let compare (a : t) (b : t) = + match (order a, order b) with + | Some a, Some b -> Int.compare a b + | Some _, None -> 1 + | None, Some _ -> -1 + | _ -> Concrete_ident.compare a b + end - let transitive_dependencies_of_items ~original_items (items : item list) - ?(graph = of_items ~original_items items) - (selection : Concrete_ident.t list) : item list = - let set = transitive_dependencies_of graph selection in - items |> List.filter ~f:(ident_of >> Hash_set.mem set) + module ItemGraph = struct + module G = Graph.Persistent.Digraph.Concrete (Ordered_concrete_ident) + module Topological = Graph.Topological.Make_stable (G) + module Oper = Graph.Oper.P (G) - module MutRec = struct - module Bundle = struct - type t = concrete_ident list + let vertices_of_item (i : item) : G.V.t list = + let ( @ ) = Set.union in + let v = U.Reducers.collect_concrete_idents in + let concat_map f = + List.map ~f >> Set.union_list (module Concrete_ident) + in + let set = + match i.v with + | Fn { name = _; generics; body; params; _ } -> + v#visit_generics () generics + @ v#visit_expr () body + @ concat_map (v#visit_param ()) params + | TyAlias { name = _; generics; ty } -> + v#visit_generics () generics @ v#visit_ty () ty + | Type { name = _; generics; variants; is_struct = (_ : bool) } -> + v#visit_generics () generics + @ concat_map (v#visit_variant ()) variants + | IMacroInvokation + { macro; argument = (_ : string); span; witness = _ } -> + v#visit_concrete_ident () macro @ v#visit_span () span + | Trait { name = _; generics; items; safety = _ } -> + v#visit_generics () generics + @ concat_map (v#visit_trait_item ()) items + | Impl + { generics; self_ty; of_trait; items; parent_bounds; safety = _ } + -> + v#visit_generics () generics + @ v#visit_ty () self_ty + @ v#visit_concrete_ident () (fst of_trait) + @ concat_map (v#visit_generic_value ()) (snd of_trait) + @ concat_map (v#visit_impl_item ()) items + @ concat_map + (fun (ie, ii) -> + v#visit_impl_expr () ie @ v#visit_impl_ident () ii) + parent_bounds + | Alias { name = _; item } -> v#visit_concrete_ident () item + | Use _ | Quote _ | HaxError _ | NotImplementedYet -> + Set.empty (module Concrete_ident) + in + set |> Set.to_list - let namespaces_of : t -> Namespace.Set.t = - List.map ~f:Namespace.of_concrete_ident - >> Set.of_list (module Namespace) + let vertices_of_items (items : item list) : G.E.t list = + List.concat_map + ~f:(fun i -> + let assoc = + uid_associated_items i.attrs |> List.map ~f:(fun i -> i.ident) + in + vertices_of_item i @ assoc + |> List.map ~f:(Fn.const i.ident &&& Fn.id)) + items - let homogeneous_namespace (ns : t) : bool = - Set.length (namespaces_of ns) <= 1 - end + let of_items (items : item list) : G.t = + let init = + List.fold ~init:G.empty ~f:(fun g -> ident_of >> G.add_vertex g) items + in + vertices_of_items items |> List.fold ~init ~f:(G.add_edge >> uncurry) + + let transitive_dependencies_of (g : G.t) + (selection : Concrete_ident.t list) : Concrete_ident.t Hash_set.t = + let set = Hash_set.create (module Concrete_ident) in + let rec visit vertex = + if Hash_set.mem set vertex |> not then ( + Hash_set.add set vertex; + G.iter_succ visit g vertex) + in + List.filter ~f:(G.mem_vertex g) selection |> List.iter ~f:visit; + set + + let transitive_dependencies_of_items (items : item list) + ?(graph = of_items items) (selection : Concrete_ident.t list) : + item list = + let set = transitive_dependencies_of graph selection in + items |> List.filter ~f:(ident_of >> Hash_set.mem set) + + module MutRec = struct + module Bundle = struct + type t = concrete_ident list + + let namespaces_of : t -> Namespace.Set.t = + List.map ~f:Namespace.of_concrete_ident + >> Set.of_list (module Namespace) + + let homogeneous_namespace (ns : t) : bool = + Set.length (namespaces_of ns) <= 1 + end + + type t = { + mut_rec_bundles : Bundle.t list; + non_mut_rec : concrete_ident list; + } + + module SCC = Graph.Components.Make (G) + + let of_graph (g : G.t) : t = + let is_mut_rec_with_itself x = G.mem_edge g x x in + let mut_rec_bundles, non_mut_rec = + SCC.scc_list g + |> List.partition_map ~f:(function + | [] -> failwith "scc_list returned empty cluster" + | [ x ] when is_mut_rec_with_itself x |> not -> Second x + | bundle -> First bundle) + in + { mut_rec_bundles; non_mut_rec } - type t = { - mut_rec_bundles : Bundle.t list; - non_mut_rec : concrete_ident list; - } + let all_homogeneous_namespace (g : G.t) = + List.for_all ~f:Bundle.homogeneous_namespace + (of_graph g).mut_rec_bundles + end - module SCC = Graph.Components.Make (G) + module CyclicDep = struct + module Bundle = struct + type t = Concrete_ident.t list + + module G = Graph.Persistent.Graph.Concrete (Ordered_concrete_ident) + module CC = Graph.Components.Undirected (G) + + let cycles g = CC.components_list g + end + + (* This is a solution that bundles together everything that belongs to the same module SCC. + It results in bundles that are much bigger than they could be but is a simple solution + to the problem described in https://github.com/hacspec/hax/issues/995#issuecomment-2411114404 *) + let of_mod_sccs (items : item list) + (mod_graph_cycles : Namespace.Set.t list) : Bundle.t list = + let item_names = List.map items ~f:(fun x -> x.ident) in + let cycles = + List.filter mod_graph_cycles ~f:(fun set -> + Prelude.Set.length set > 1) + in + let bundles = + List.map cycles ~f:(fun set -> + List.filter item_names ~f:(fun item -> + Prelude.Set.mem set (Namespace.of_concrete_ident item))) + in + bundles + end - let of_graph (g : G.t) : t = - let is_mut_rec_with_itself x = G.mem_edge g x x in - let mut_rec_bundles, non_mut_rec = - SCC.scc_list g - |> List.partition_map ~f:(function - | [] -> failwith "scc_list returned empty cluster" - | [ x ] when is_mut_rec_with_itself x |> not -> Second x - | bundle -> First bundle) - in - { mut_rec_bundles; non_mut_rec } + open Graph.Graphviz.Dot (struct + include G - let all_homogeneous_namespace (g : G.t) = - List.for_all ~f:Bundle.homogeneous_namespace - (of_graph g).mut_rec_bundles - end + let graph_attributes _ = [] + let default_vertex_attributes _ = [] + let vertex_name i = "\"" ^ Concrete_ident.show i ^ "\"" - module CyclicDep = struct - module Bundle = struct - type t = Concrete_ident.t list + let vertex_attributes i = + [ `Label (Concrete_ident.DefaultViewAPI.to_definition_name i) ] - module G = Graph.Persistent.Graph.Concrete (Concrete_ident) - module CC = Graph.Components.Undirected (G) + let get_subgraph i = + let ns = Namespace.of_concrete_ident i in + let sg_name = String.concat ~sep:"__" ns in + let label = String.concat ~sep:"::" ns in + let open Graph.Graphviz.DotAttributes in + Some { sg_name; sg_attributes = [ `Label label ]; sg_parent = None } - let cycles g = CC.components_list g - end + let default_edge_attributes _ = [] + let edge_attributes _ = [] + end) - (* This is a solution that bundles together everything that belongs to the same module SCC. - It results in bundles that are much bigger than they could be but is a simple solution - to the problem described in https://github.com/hacspec/hax/issues/995#issuecomment-2411114404 *) - let of_mod_sccs (items : item list) - (mod_graph_cycles : Namespace.Set.t list) : Bundle.t list = - let item_names = List.map items ~f:(fun x -> x.ident) in - let cycles = - List.filter mod_graph_cycles ~f:(fun set -> - Prelude.Set.length set > 1) - in - let bundles = - List.map cycles ~f:(fun set -> - List.filter item_names ~f:(fun item -> - Prelude.Set.mem set (Namespace.of_concrete_ident item))) - in - bundles + let print oc items = output_graph oc (of_items items) end - open Graph.Graphviz.Dot (struct - include G + module ModGraph = struct + module G = Graph.Persistent.Digraph.Concrete (Namespace) + + let of_items (items : item list) : G.t = + let ig = ItemGraph.of_items items in + List.map ~f:(ident_of >> (Namespace.of_concrete_ident &&& Fn.id)) items + |> Map.of_alist_multi (module Namespace) + |> Map.map + ~f: + (List.concat_map + ~f: + (ItemGraph.G.succ ig + >> List.map ~f:Namespace.of_concrete_ident) + >> Set.of_list (module Namespace) + >> Set.to_list) + |> Map.to_alist + |> List.concat_map ~f:(fun (x, ys) -> List.map ~f:(fun y -> (x, y)) ys) + |> List.fold ~init:G.empty ~f:(G.add_edge >> uncurry) - let graph_attributes _ = [] - let default_vertex_attributes _ = [] - let vertex_name i = "\"" ^ Concrete_ident.show i ^ "\"" + module SCC = Graph.Components.Make (G) - let vertex_attributes i = - [ `Label (Concrete_ident.DefaultViewAPI.to_definition_name i) ] + let cycles g : Namespace.Set.t list = + SCC.scc_list g |> List.map ~f:(Set.of_list (module Namespace)) - let get_subgraph i = - let ns = Namespace.of_concrete_ident i in - let sg_name = String.concat ~sep:"__" ns in - let label = String.concat ~sep:"::" ns in - let open Graph.Graphviz.DotAttributes in - Some { sg_name; sg_attributes = [ `Label label ]; sg_parent = None } + open Graph.Graphviz.Dot (struct + include G - let default_edge_attributes _ = [] - let edge_attributes _ = [] - end) + let graph_attributes _ = [] + let default_vertex_attributes _ = [] + let vertex_name ns = "\"" ^ String.concat ~sep:"::" ns ^ "\"" + let vertex_attributes _ = [] + let get_subgraph _ = None + let default_edge_attributes _ = [] + let edge_attributes _ = [] + end) - let print oc items = output_graph oc (of_items ~original_items:items items) - end + let print oc items = + let g = of_items items in + let complicated_ones = + SCC.scc_list g + |> List.concat_map ~f:(function [] | [ _ ] -> [] | bundle -> bundle) + in + let g = + List.concat_map + ~f:(fun ns -> + List.map + ~f:(fun y -> (ns, y)) + (G.succ g ns + |> List.filter + ~f:(List.mem ~equal:[%equal: Namespace.t] complicated_ones) + )) + complicated_ones + |> List.fold ~init:G.empty ~f:(G.add_edge >> uncurry) + in + output_graph oc g + end - module ModGraph = struct - module G = Graph.Persistent.Digraph.Concrete (Namespace) - - let of_items (items : item list) : G.t = - let ig = ItemGraph.of_items ~original_items:items items in - List.map ~f:(ident_of >> (Namespace.of_concrete_ident &&& Fn.id)) items - |> Map.of_alist_multi (module Namespace) - |> Map.map - ~f: - (List.concat_map - ~f: - (ItemGraph.G.succ ig - >> List.map ~f:Namespace.of_concrete_ident) - >> Set.of_list (module Namespace) - >> Set.to_list) - |> Map.to_alist - |> List.concat_map ~f:(fun (x, ys) -> List.map ~f:(fun y -> (x, y)) ys) - |> List.fold ~init:G.empty ~f:(G.add_edge >> uncurry) - - module SCC = Graph.Components.Make (G) - - let cycles g : Namespace.Set.t list = - SCC.scc_list g |> List.map ~f:(Set.of_list (module Namespace)) - - open Graph.Graphviz.Dot (struct - include G - - let graph_attributes _ = [] - let default_vertex_attributes _ = [] - let vertex_name ns = "\"" ^ String.concat ~sep:"::" ns ^ "\"" - let vertex_attributes _ = [] - let get_subgraph _ = None - let default_edge_attributes _ = [] - let edge_attributes _ = [] - end) - - let print oc items = - let g = of_items items in - let complicated_ones = - SCC.scc_list g - |> List.concat_map ~f:(function [] | [ _ ] -> [] | bundle -> bundle) - in - let g = - List.concat_map - ~f:(fun ns -> - List.map - ~f:(fun y -> (ns, y)) - (G.succ g ns - |> List.filter - ~f:(List.mem ~equal:[%equal: Namespace.t] complicated_ones))) - complicated_ones - |> List.fold ~init:G.empty ~f:(G.add_edge >> uncurry) - in - output_graph oc g - end + let ident_list_to_string = + List.map ~f:Concrete_ident.DefaultViewAPI.show >> String.concat ~sep:", " - let ident_list_to_string = - List.map ~f:Concrete_ident.DefaultViewAPI.show >> String.concat ~sep:", " - - let sort (items : item list) : item list = - let g = - ItemGraph.of_items ~original_items:items items |> ItemGraph.Oper.mirror - in - let lookup (name : concrete_ident) = - List.find ~f:(ident_of >> Concrete_ident.equal name) items - in - let items' = - ItemGraph.Topological.fold List.cons g [] - |> List.filter_map ~f:lookup |> List.rev - in - assert ( - let of_list = - List.map ~f:ident_of >> Set.of_list (module Concrete_ident) + let sort (items : item list) : item list = + let g = ItemGraph.of_items items |> ItemGraph.Oper.mirror in + let lookup (name : concrete_ident) = + List.find ~f:(ident_of >> Concrete_ident.equal name) items in - let items = of_list items in - let items' = of_list items' in - Set.equal items items'); - items' - - let filter_by_inclusion_clauses' ~original_items - (clauses : Types.inclusion_clause list) (items : item list) : - item list * Concrete_ident.t Hash_set.t = - let graph = ItemGraph.of_items ~original_items items in - let of_list = Set.of_list (module Concrete_ident) in - let selection = List.map ~f:ident_of items |> of_list in - let deps_of = - let to_set = Hash_set.to_list >> of_list in - Set.to_list >> ItemGraph.transitive_dependencies_of graph >> to_set - in - let show_ident_set = - Set.to_list - >> List.map ~f:Concrete_ident.DefaultViewAPI.show - >> List.map ~f:(fun s -> " - " ^ s) - >> String.concat ~sep:"\n" - in - let show_inclusion_clause Types.{ kind; namespace } = - (match kind with - | Excluded -> "-" - | SignatureOnly -> "+:" - | Included deps_kind -> ( - match deps_kind with - | Transitive -> "+" - | Shallow -> "+~" - | None' -> "+!")) - ^ "[" - ^ (List.map - ~f:(function Glob One -> "*" | Glob Many -> "**" | Exact s -> s) - namespace.chunks - |> String.concat ~sep:"::") - ^ "]" - in - let items_drop_body = Hash_set.create (module Concrete_ident) in - let apply_clause selection' (clause : Types.inclusion_clause) = - let matches = Concrete_ident.matches_namespace clause.Types.namespace in - let matched0 = Set.filter ~f:matches selection in - let with_deps, drop_bodies = - match clause.kind with - | Included Transitive -> (true, false) - | Included Shallow -> (true, true) - | Included None' -> (false, false) - | SignatureOnly -> (false, true) - | Excluded -> (false, false) + let items' = + ItemGraph.Topological.fold List.cons g [] + |> List.filter_map ~f:lookup |> List.rev in - let matched = matched0 |> if with_deps then deps_of else Fn.id in - if drop_bodies then ( - Set.iter ~f:(Hash_set.add items_drop_body) matched; - Set.iter ~f:(Hash_set.remove items_drop_body) matched0); - Logs.info (fun m -> - m "The clause [%s] will %s the following Rust items:\n%s" - (show_inclusion_clause clause) - (match clause.kind with Excluded -> "remove" | _ -> "add") - @@ show_ident_set matched); - let set_op = - match clause.kind with - | Included _ | SignatureOnly -> Set.union - | Excluded -> Set.diff + assert ( + let of_list = + List.map ~f:ident_of >> Set.of_list (module Concrete_ident) + in + let items = of_list items in + let items' = of_list items' in + Set.equal items items'); + items' + + let filter_by_inclusion_clauses' (clauses : Types.inclusion_clause list) + (items : item list) : item list * Concrete_ident.t Hash_set.t = + let graph = ItemGraph.of_items items in + let of_list = Set.of_list (module Concrete_ident) in + let selection = List.map ~f:ident_of items |> of_list in + let deps_of = + let to_set = Hash_set.to_list >> of_list in + Set.to_list >> ItemGraph.transitive_dependencies_of graph >> to_set in - let result = set_op selection' matched in - result - in - let selection = List.fold ~init:selection ~f:apply_clause clauses in - Logs.info (fun m -> - m "The following Rust items are going to be extracted:\n%s" - @@ show_ident_set selection); - (List.filter ~f:(ident_of >> Set.mem selection) items, items_drop_body) - - let filter_by_inclusion_clauses (clauses : Types.inclusion_clause list) - (items : item list) : item list = - let f = filter_by_inclusion_clauses' ~original_items:items clauses in - let selection = - let items', items_drop_body = f items in - let items', _ = - (* when one includes only shallow dependencies, we just remove bodies *) - List.map - ~f:(fun item -> - if Hash_set.mem items_drop_body (ident_of item) then - U.Mappers.drop_bodies#visit_item () item - else item) - items' - |> f + let show_ident_set = + Set.to_list + >> List.map ~f:Concrete_ident.DefaultViewAPI.show + >> List.map ~f:(fun s -> " - " ^ s) + >> String.concat ~sep:"\n" in - List.map ~f:ident_of items' |> Set.of_list (module Concrete_ident) - in - List.filter ~f:(ident_of >> Set.mem selection) items - - (* Construct the new item `f item` (say `item'`), and create a - "symbolic link" to `item'`. Returns a pair that consists in the - symbolic link and in `item'`. *) - let shallow_copy (f : item -> item) - (variants_renamings : - concrete_ident * concrete_ident -> - (concrete_ident * concrete_ident) list) (item : item) : item list = - let item' = f item in - let old_new = (ident_of item, ident_of item') in - let aliases = - List.map (old_new :: variants_renamings old_new) - ~f:(fun (old_ident, new_ident) -> - let attrs = - List.filter ~f:(fun att -> Attrs.late_skip [ att ]) item.attrs - in - - { item with v = Alias { name = old_ident; item = new_ident }; attrs }) - in - item' :: aliases - - let bundle_cyclic_modules (items : item list) : item list = - let from_ident ident : item option = - List.find ~f:(fun i -> [%equal: Concrete_ident.t] i.ident ident) items - in - let mut_rec_bundles = - let mod_graph_cycles = ModGraph.of_items items |> ModGraph.cycles in - (* `Use` items shouldn't be bundled as they have no dependencies - and they have dummy names. *) - let non_use_items = - List.filter - ~f:(fun item -> - match item.v with Use _ | NotImplementedYet -> false | _ -> true) - items + let show_inclusion_clause Types.{ kind; namespace } = + (match kind with + | Excluded -> "-" + | SignatureOnly -> "+:" + | Included deps_kind -> ( + match deps_kind with + | Transitive -> "+" + | Shallow -> "+~" + | None' -> "+!")) + ^ "[" + ^ (List.map + ~f:(function Glob One -> "*" | Glob Many -> "**" | Exact s -> s) + namespace.chunks + |> String.concat ~sep:"::") + ^ "]" in - let bundles = - ItemGraph.CyclicDep.of_mod_sccs non_use_items mod_graph_cycles + let items_drop_body = Hash_set.create (module Concrete_ident) in + let apply_clause selection' (clause : Types.inclusion_clause) = + let matches = Concrete_ident.matches_namespace clause.Types.namespace in + let matched0 = Set.filter ~f:matches selection in + let with_deps, drop_bodies = + match clause.kind with + | Included Transitive -> (true, false) + | Included Shallow -> (true, true) + | Included None' -> (false, false) + | SignatureOnly -> (false, true) + | Excluded -> (false, false) + in + let matched = matched0 |> if with_deps then deps_of else Fn.id in + if drop_bodies then ( + Set.iter ~f:(Hash_set.add items_drop_body) matched; + Set.iter ~f:(Hash_set.remove items_drop_body) matched0); + Logs.info (fun m -> + m "The clause [%s] will %s the following Rust items:\n%s" + (show_inclusion_clause clause) + (match clause.kind with Excluded -> "remove" | _ -> "add") + @@ show_ident_set matched); + let set_op = + match clause.kind with + | Included _ | SignatureOnly -> Set.union + | Excluded -> Set.diff + in + let result = set_op selection' matched in + result in - let f = List.filter_map ~f:from_ident in - List.map ~f bundles - in - - let transform (bundle : item list) = - let ns : Concrete_ident.t = - Concrete_ident.Create.fresh_module ~from:(List.map ~f:ident_of bundle) + let selection = List.fold ~init:selection ~f:apply_clause clauses in + Logs.info (fun m -> + m "The following Rust items are going to be extracted:\n%s" + @@ show_ident_set selection); + (List.filter ~f:(ident_of >> Set.mem selection) items, items_drop_body) + + let filter_by_inclusion_clauses (clauses : Types.inclusion_clause list) + (items : item list) : item list = + let f = filter_by_inclusion_clauses' clauses in + let selection = + let items', items_drop_body = f items in + let items', _ = + (* when one includes only shallow dependencies, we just remove bodies *) + List.map + ~f:(fun item -> + if Hash_set.mem items_drop_body (ident_of item) then + U.Mappers.drop_bodies#visit_item () item + else item) + items' + |> f + in + List.map ~f:ident_of items' |> Set.of_list (module Concrete_ident) in - let new_name_under_ns : Concrete_ident.t -> Concrete_ident.t = - Concrete_ident.Create.move_under ~new_parent:ns + List.filter ~f:(ident_of >> Set.mem selection) items + + (* Construct the new item `f item` (say `item'`), and create a + "symbolic link" to `item'`. Returns a pair that consists in the + symbolic link and in `item'`. *) + let shallow_copy (f : item -> item) + (variants_renamings : + concrete_ident * concrete_ident -> + (concrete_ident * concrete_ident) list) (item : item) : item list = + let item' = f item in + let old_new = (ident_of item, ident_of item') in + let aliases = + List.map (old_new :: variants_renamings old_new) + ~f:(fun (old_ident, new_ident) -> + let attrs = + List.filter ~f:(fun att -> Attrs.late_skip [ att ]) item.attrs + in + + { + item with + v = Alias { name = old_ident; item = new_ident }; + attrs; + }) in - let new_names = List.map ~f:(ident_of >> new_name_under_ns) bundle in - let duplicates = - new_names |> List.find_all_dups ~compare:Concrete_ident.compare + item' :: aliases + + let bundle_cyclic_modules (items : item list) : item list = + let from_ident ident : item option = + List.find ~f:(fun i -> [%equal: Concrete_ident.t] i.ident ident) items in - (* Verify name clashes *) - (* In case of clash, add hash *) - let add_prefix id = - if - not - (List.mem duplicates (new_name_under_ns id) - ~equal:Concrete_ident.equal) - then id - else - Concrete_ident.Create.map_last - ~f:(fun name -> name ^ (Concrete_ident.hash id |> Int.to_string)) - id + let mut_rec_bundles = + let mod_graph_cycles = ModGraph.of_items items |> ModGraph.cycles in + (* `Use` items shouldn't be bundled as they have no dependencies + and they have dummy names. *) + let non_use_items = + List.filter + ~f:(fun item -> + match item.v with Use _ | NotImplementedYet -> false | _ -> true) + items + in + let bundles = + ItemGraph.CyclicDep.of_mod_sccs non_use_items mod_graph_cycles + in + let f = List.filter_map ~f:from_ident in + List.map ~f bundles in - let renamings = - List.map - ~f:(ident_of >> (Fn.id &&& (add_prefix >> new_name_under_ns))) - bundle + + let transform (bundle : item list) = + let ns : Concrete_ident.t = + Concrete_ident.Create.fresh_module ~from:(List.map ~f:ident_of bundle) + in + let new_name_under_ns : Concrete_ident.t -> Concrete_ident.t = + Concrete_ident.Create.move_under ~new_parent:ns + in + let new_names = List.map ~f:(ident_of >> new_name_under_ns) bundle in + let duplicates = + new_names |> List.find_all_dups ~compare:Concrete_ident.compare + in + (* Verify name clashes *) + (* In case of clash, add hash *) + let add_prefix id = + if + not + (List.mem duplicates (new_name_under_ns id) + ~equal:Concrete_ident.equal) + then id + else + Concrete_ident.Create.map_last + ~f:(fun name -> name ^ (Concrete_ident.hash id |> Int.to_string)) + id + in + let renamings = + List.map + ~f:(ident_of >> (Fn.id &&& (add_prefix >> new_name_under_ns))) + bundle + in + let variants_renamings (previous_name, new_name) = + match from_ident previous_name with + | Some { v = Type { variants; is_struct = false; _ }; _ } -> + List.map variants ~f:(fun { name; _ } -> + ( name, + Concrete_ident.Create.move_under ~new_parent:new_name name + )) + | Some { v = Type { variants; is_struct = true; _ }; _ } -> + List.concat_map variants ~f:(fun { arguments; _ } -> + List.map arguments ~f:(fun (name, _, _) -> + ( name, + Concrete_ident.Create.move_under ~new_parent:new_name + name ))) + | _ -> [] + in + let variant_and_constructors_renamings = + List.concat_map ~f:variants_renamings renamings + |> List.concat_map ~f:(fun (old_name, new_name) -> + [ + (old_name, new_name); + ( Concrete_ident.Create.constructor old_name, + Concrete_ident.Create.constructor new_name ); + ]) + in + let renamings = + Map.of_alist_exn + (module Concrete_ident) + (renamings @ variant_and_constructors_renamings) + in + let rename = + let renamer _lvl i = + Map.find renamings i |> Option.value ~default:i + in + (U.Mappers.rename_concrete_idents renamer)#visit_item ExprLevel + in + fun it -> shallow_copy rename variants_renamings it in - let variants_renamings (previous_name, new_name) = - match from_ident previous_name with - | Some { v = Type { variants; is_struct = false; _ }; _ } -> - List.map variants ~f:(fun { name; _ } -> - ( name, - Concrete_ident.Create.move_under ~new_parent:new_name name )) - | Some { v = Type { variants; is_struct = true; _ }; _ } -> - List.concat_map variants ~f:(fun { arguments; _ } -> - List.map arguments ~f:(fun (name, _, _) -> - ( name, - Concrete_ident.Create.move_under ~new_parent:new_name name - ))) - | _ -> [] + let bundle_transforms = + List.concat_map mut_rec_bundles ~f:(fun bundle -> + let bundle_value = + ( List.map ~f:ident_of bundle + |> ItemGraph.MutRec.Bundle.homogeneous_namespace, + transform bundle ) + in + List.map bundle ~f:(fun item -> (item, bundle_value))) in - let variant_and_constructors_renamings = - List.concat_map ~f:variants_renamings renamings - |> List.concat_map ~f:(fun (old_name, new_name) -> - [ - (old_name, new_name); - ( Concrete_ident.Create.constructor old_name, - Concrete_ident.Create.constructor new_name ); - ]) + let module ComparableItem = struct + module T = struct + type t = item [@@deriving sexp_of, compare, hash] + end + + include T + include Comparable.Make (T) + end in + let bundle_of_item = + Hashtbl.of_alist_exn (module ComparableItem) bundle_transforms in - let renamings = - Map.of_alist_exn - (module Concrete_ident) - (renamings @ variant_and_constructors_renamings) + let maybe_transform_item item = + match Hashtbl.find bundle_of_item item with + | Some (homogeneous_bundle, transform_bundle) -> + if homogeneous_bundle then [ item ] else transform_bundle item + | None -> [ item ] in - let rename = - let renamer _lvl i = Map.find renamings i |> Option.value ~default:i in - (U.Mappers.rename_concrete_idents renamer)#visit_item ExprLevel + List.concat_map items ~f:maybe_transform_item + + let recursive_bundles (items : item list) : item list list * item list = + let g = ItemGraph.of_items items in + let bundles = ItemGraph.MutRec.of_graph g in + let from_ident ident : item option = + List.find ~f:(fun i -> [%equal: Concrete_ident.t] i.ident ident) items in - fun it -> shallow_copy rename variants_renamings it - in - let bundle_transforms = - List.concat_map mut_rec_bundles ~f:(fun bundle -> - let bundle_value = - ( List.map ~f:ident_of bundle - |> ItemGraph.MutRec.Bundle.homogeneous_namespace, - transform bundle ) - in - List.map bundle ~f:(fun item -> (item, bundle_value))) - in - let module ComparableItem = struct - module T = struct - type t = item [@@deriving sexp_of, compare, hash] - end + let f = List.filter_map ~f:from_ident in + (List.map ~f bundles.mut_rec_bundles, f bundles.non_mut_rec) + end - include T - include Comparable.Make (T) - end in - let bundle_of_item = - Hashtbl.of_alist_exn (module ComparableItem) bundle_transforms - in - let maybe_transform_item item = - match Hashtbl.find bundle_of_item item with - | Some (homogeneous_bundle, transform_bundle) -> - if homogeneous_bundle then [ item ] else transform_bundle item - | None -> [ item ] - in - List.concat_map items ~f:maybe_transform_item - - let recursive_bundles (items : item list) : item list list * item list = - let g = ItemGraph.of_items ~original_items:items items in - let bundles = ItemGraph.MutRec.of_graph g in - let from_ident ident : item option = - List.find ~f:(fun i -> [%equal: Concrete_ident.t] i.ident ident) items - in - let f = List.filter_map ~f:from_ident in - (List.map ~f bundles.mut_rec_bundles, f bundles.non_mut_rec) + let uid_associated_items items' = + let open WithItems (struct + let items = items' + end) in + uid_associated_items + + let bundle_cyclic_modules items' = + let open WithItems (struct + let items = items' + end) in + bundle_cyclic_modules items' + + let sort items' = + let open WithItems (struct + let items = items' + end) in + sort items' + + let recursive_bundles items' = + let open WithItems (struct + let items = items' + end) in + recursive_bundles items' + + let filter_by_inclusion_clauses clauses items' = + let open WithItems (struct + let items = items' + end) in + filter_by_inclusion_clauses clauses items' end diff --git a/test-harness/src/snapshots/toolchain__attribute-opaque into-fstar.snap b/test-harness/src/snapshots/toolchain__attribute-opaque into-fstar.snap index 2275da427..d45c9cb4d 100644 --- a/test-harness/src/snapshots/toolchain__attribute-opaque into-fstar.snap +++ b/test-harness/src/snapshots/toolchain__attribute-opaque into-fstar.snap @@ -35,7 +35,7 @@ module Attribute_opaque open Core open FStar.Mul -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_OpaqueEnum (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 index e65784071..aa8b73123 100644 --- a/test-harness/src/snapshots/toolchain__attributes into-fstar.snap +++ b/test-harness/src/snapshots/toolchain__attributes into-fstar.snap @@ -92,6 +92,8 @@ open FStar.Mul unfold type t_Int = int +unfold let add x y = x + y + unfold instance impl: Core.Ops.Arith.t_Sub t_Int t_Int = { f_Output = t_Int; @@ -99,8 +101,6 @@ unfold instance impl: Core.Ops.Arith.t_Sub t_Int t_Int = f_sub_post = (fun (self: t_Int) (other: t_Int) (out: t_Int) -> true); f_sub = fun (self: t_Int) (other: t_Int) -> self + other } - -unfold let add x y = x + y ''' "Attributes.Nested_refinement_elim.fst" = ''' module Attributes.Nested_refinement_elim @@ -118,11 +118,16 @@ module Attributes.Newtype_pattern open Core open FStar.Mul +let v_MAX: usize = sz 10 + type t_SafeIndex = { f_i:f_i: usize{f_i <. v_MAX} } -let impl__SafeIndex__as_usize (self: t_SafeIndex) : usize = self.f_i +let impl__SafeIndex__new (i: usize) : Core.Option.t_Option t_SafeIndex = + if i <. v_MAX + then Core.Option.Option_Some ({ f_i = i } <: t_SafeIndex) <: Core.Option.t_Option t_SafeIndex + else Core.Option.Option_None <: Core.Option.t_Option t_SafeIndex -let v_MAX: usize = sz 10 +let impl__SafeIndex__as_usize (self: t_SafeIndex) : usize = self.f_i [@@ FStar.Tactics.Typeclasses.tcinstance] let impl_1 (#v_T: Type0) : Core.Ops.Index.t_Index (t_Array v_T (sz 10)) t_SafeIndex = @@ -132,11 +137,6 @@ let impl_1 (#v_T: Type0) : Core.Ops.Index.t_Index (t_Array v_T (sz 10)) t_SafeIn f_index_post = (fun (self: t_Array v_T (sz 10)) (index: t_SafeIndex) (out: v_T) -> true); f_index = fun (self: t_Array v_T (sz 10)) (index: t_SafeIndex) -> self.[ index.f_i ] } - -let impl__SafeIndex__new (i: usize) : Core.Option.t_Option t_SafeIndex = - if i <. v_MAX - then Core.Option.Option_Some ({ f_i = i } <: t_SafeIndex) <: Core.Option.t_Option t_SafeIndex - else Core.Option.Option_None <: Core.Option.t_Option t_SafeIndex ''' "Attributes.Pre_post_on_traits_and_impls.fst" = ''' module Attributes.Pre_post_on_traits_and_impls @@ -162,13 +162,6 @@ class t_Operation (v_Self: Type0) = { f_double:x0: u8 -> Prims.Pure u8 (f_double_pre x0) (fun result -> f_double_post x0 result) } -class t_TraitWithRequiresAndEnsures (v_Self: Type0) = { - f_method_pre:self___: v_Self -> x: u8 -> pred: Type0{x <. 100uy ==> pred}; - f_method_post:self___: v_Self -> x: u8 -> r: u8 -> pred: Type0{pred ==> r >. 88uy}; - f_method:x0: v_Self -> x1: u8 - -> Prims.Pure u8 (f_method_pre x0 x1) (fun result -> f_method_post x0 x1 result) -} - type t_ViaAdd = | ViaAdd : t_ViaAdd type t_ViaMul = | ViaMul : t_ViaMul @@ -207,6 +200,13 @@ let impl_1: t_Operation t_ViaMul = f_double = fun (x: u8) -> x *! 2uy } +class t_TraitWithRequiresAndEnsures (v_Self: Type0) = { + f_method_pre:self___: v_Self -> x: u8 -> pred: Type0{x <. 100uy ==> pred}; + f_method_post:self___: v_Self -> x: u8 -> r: u8 -> pred: Type0{pred ==> r >. 88uy}; + f_method:x0: v_Self -> x1: u8 + -> Prims.Pure u8 (f_method_pre x0 x1) (fun result -> f_method_post x0 x1 result) +} + let test (#v_T: Type0) (#[FStar.Tactics.Typeclasses.tcresolve ()] i1: t_TraitWithRequiresAndEnsures v_T) @@ -247,10 +247,10 @@ module Attributes.Refined_indexes open Core open FStar.Mul -type t_MyArray = | MyArray : t_Array u8 (sz 10) -> t_MyArray - let v_MAX: usize = sz 10 +type t_MyArray = | MyArray : t_Array u8 (sz 10) -> t_MyArray + /// Triple dash comment (** Multiline double star comment Maecenas blandit accumsan feugiat. Done vitae ullamcorper est. @@ -288,27 +288,20 @@ module Attributes.Refinement_types open Core open FStar.Mul -/// Example of a specific constraint on a value -let t_CompressionFactor = x: u8{x =. 4uy || x =. 5uy || x =. 10uy || x =. 11uy} - let t_BoundedU8 (v_MIN v_MAX: u8) = x: u8{x >=. v_MIN && x <=. v_MAX} -/// A field element -let t_FieldElement = x: u16{x <=. 2347us} +let bounded_u8 (x: t_BoundedU8 12uy 15uy) (y: t_BoundedU8 10uy 11uy) : t_BoundedU8 1uy 23uy = + (x <: u8) +! (y <: u8) <: t_BoundedU8 1uy 23uy /// Even `u8` numbers. Constructing pub Even values triggers static /// proofs in the extraction. let t_Even = x: u8{(x %! 2uy <: u8) =. 0uy} -/// A modular mutliplicative inverse -let t_ModInverse (v_MOD: u32) = - n: - u32 - { (((cast (n <: u32) <: u128) *! (cast (v_MOD <: u32) <: u128) <: u128) %! - (cast (v_MOD <: u32) <: u128) - <: - u128) =. - pub_u128 1 } +let double (x: u8) : Prims.Pure t_Even (requires x <. 127uy) (fun _ -> Prims.l_True) = + x +! x <: t_Even + +let double_refine (x: u8) : Prims.Pure t_Even (requires x <. 127uy) (fun _ -> Prims.l_True) = + x +! x <: t_Even /// A string that contains no space. let t_NoE = @@ -330,14 +323,21 @@ let t_NoE = in ~.out } -let double_refine (x: u8) : Prims.Pure t_Even (requires x <. 127uy) (fun _ -> Prims.l_True) = - x +! x <: t_Even +/// A modular mutliplicative inverse +let t_ModInverse (v_MOD: u32) = + n: + u32 + { (((cast (n <: u32) <: u128) *! (cast (v_MOD <: u32) <: u128) <: u128) %! + (cast (v_MOD <: u32) <: u128) + <: + u128) =. + pub_u128 1 } -let bounded_u8 (x: t_BoundedU8 12uy 15uy) (y: t_BoundedU8 10uy 11uy) : t_BoundedU8 1uy 23uy = - (x <: u8) +! (y <: u8) <: t_BoundedU8 1uy 23uy +/// A field element +let t_FieldElement = x: u16{x <=. 2347us} -let double (x: u8) : Prims.Pure t_Even (requires x <. 127uy) (fun _ -> Prims.l_True) = - x +! x <: t_Even +/// Example of a specific constraint on a value +let t_CompressionFactor = x: u8{x =. 4uy || x =. 5uy || x =. 10uy || x =. 11uy} ''' "Attributes.Requires_mut.fst" = ''' module Attributes.Requires_mut @@ -417,6 +417,12 @@ module Attributes.Verifcation_status open Core open FStar.Mul +#push-options "--admit_smt_queries true" + +let a_function_which_only_laxes (_: Prims.unit) : Prims.unit = Hax_lib.v_assert false + +#pop-options + let a_panicfree_function (_: Prims.unit) : Prims.Pure u8 Prims.l_True @@ -441,12 +447,6 @@ let another_panicfree_function (_: Prims.unit) let nothing:i32 = 0l in let still_not_much:i32 = not_much +! nothing in admit () (* Panic freedom *) - -#push-options "--admit_smt_queries true" - -let a_function_which_only_laxes (_: Prims.unit) : Prims.unit = Hax_lib.v_assert false - -#pop-options ''' "Attributes.fst" = ''' module Attributes @@ -454,23 +454,20 @@ module Attributes open Core open FStar.Mul -type t_Foo = { - f_x:u32; - f_y:f_y: u32{f_y >. 3ul}; - f_z:f_z: u32{((f_y +! f_x <: u32) +! f_z <: u32) >. 3ul} -} - -let inlined_code__V: u8 = 12uy +let u32_max: u32 = 90000ul -let issue_844_ (v__x: u8) - : Prims.Pure u8 - Prims.l_True +/// A doc comment on `add3` +///another doc comment on add3 +let add3 (x y z: u32) + : Prims.Pure u32 + (requires x >. 10ul && y >. 10ul && z >. 10ul && ((x +! y <: u32) +! z <: u32) <. u32_max) (ensures - fun v__x_future -> - let v__x_future:u8 = v__x_future in - true) = v__x - -let u32_max: u32 = 90000ul + fun result -> + let result:u32 = result in + Hax_lib.implies true + (fun temp_0_ -> + let _:Prims.unit = temp_0_ in + result >. 32ul <: bool)) = (x +! y <: u32) +! z let swap_and_mut_req_ens (x y: u32) : Prims.Pure (u32 & u32 & u32) @@ -485,18 +482,13 @@ let swap_and_mut_req_ens (x y: u32) let hax_temp_output:u32 = x +! y in x, y, hax_temp_output <: (u32 & u32 & u32) -/// A doc comment on `add3` -///another doc comment on add3 -let add3 (x y z: u32) - : Prims.Pure u32 - (requires x >. 10ul && y >. 10ul && z >. 10ul && ((x +! y <: u32) +! z <: u32) <. u32_max) +let issue_844_ (v__x: u8) + : Prims.Pure u8 + Prims.l_True (ensures - fun result -> - let result:u32 = result in - Hax_lib.implies true - (fun temp_0_ -> - let _:Prims.unit = temp_0_ in - result >. 32ul <: bool)) = (x +! y <: u32) +! z + fun v__x_future -> + let v__x_future:u8 = v__x_future in + true) = v__x let add3_lemma (x: u32) : Lemma Prims.l_True @@ -504,6 +496,14 @@ let add3_lemma (x: u32) x <=. 10ul || x >=. (u32_max /! 3ul <: u32) || (add3 x x x <: u32) =. (x *! 3ul <: u32)) = () +type t_Foo = { + f_x:u32; + f_y:f_y: u32{f_y >. 3ul}; + f_z:f_z: u32{((f_y +! f_x <: u32) +! f_z <: u32) >. 3ul} +} + +let inlined_code__V: u8 = 12uy + let before_inlined_code = "example before" let inlined_code (foo: t_Foo) : Prims.unit = diff --git a/test-harness/src/snapshots/toolchain__constructor-as-closure into-fstar.snap b/test-harness/src/snapshots/toolchain__constructor-as-closure into-fstar.snap index 6f8919b71..57b89460f 100644 --- a/test-harness/src/snapshots/toolchain__constructor-as-closure into-fstar.snap +++ b/test-harness/src/snapshots/toolchain__constructor-as-closure into-fstar.snap @@ -32,15 +32,15 @@ module Constructor_as_closure open Core open FStar.Mul -type t_Context = - | Context_A : i32 -> t_Context - | Context_B : i32 -> t_Context - type t_Test = | Test : i32 -> t_Test let impl__Test__test (x: Core.Option.t_Option i32) : Core.Option.t_Option t_Test = Core.Option.impl__map #i32 #t_Test x Test +type t_Context = + | Context_A : i32 -> t_Context + | Context_B : i32 -> t_Context + let impl__Context__test (x: Core.Option.t_Option i32) : Core.Option.t_Option t_Context = Core.Option.impl__map #i32 #t_Context x Context_B ''' diff --git a/test-harness/src/snapshots/toolchain__cyclic-modules into-fstar.snap b/test-harness/src/snapshots/toolchain__cyclic-modules into-fstar.snap index af07fc045..32b65dbc7 100644 --- a/test-harness/src/snapshots/toolchain__cyclic-modules into-fstar.snap +++ b/test-harness/src/snapshots/toolchain__cyclic-modules into-fstar.snap @@ -122,32 +122,32 @@ module Cyclic_modules.Enums_a open Core open FStar.Mul -include Cyclic_modules.Enums_b.Rec_bundle_994866580 {t_T240131830 as t_T} +include Cyclic_modules.Enums_b.Rec_bundle_902271266 {t_T240131830 as t_T} -include Cyclic_modules.Enums_b.Rec_bundle_994866580 {T240131830_A as T_A} +include Cyclic_modules.Enums_b.Rec_bundle_902271266 {T240131830_A as T_A} -include Cyclic_modules.Enums_b.Rec_bundle_994866580 {T240131830_B as T_B} +include Cyclic_modules.Enums_b.Rec_bundle_902271266 {T240131830_B as T_B} -include Cyclic_modules.Enums_b.Rec_bundle_994866580 {T240131830_C as T_C} +include Cyclic_modules.Enums_b.Rec_bundle_902271266 {T240131830_C as T_C} -include Cyclic_modules.Enums_b.Rec_bundle_994866580 {T240131830_D as T_D} +include Cyclic_modules.Enums_b.Rec_bundle_902271266 {T240131830_D as T_D} ''' -"Cyclic_modules.Enums_b.Rec_bundle_994866580.fst" = ''' -module Cyclic_modules.Enums_b.Rec_bundle_994866580 +"Cyclic_modules.Enums_b.Rec_bundle_902271266.fst" = ''' +module Cyclic_modules.Enums_b.Rec_bundle_902271266 #set-options "--fuel 0 --ifuel 1 --z3rlimit 15" open Core open FStar.Mul -type t_T366415196 = - | T366415196_A : t_T366415196 - | T366415196_B : t_T366415196 - | T366415196_C : Alloc.Vec.t_Vec t_T240131830 Alloc.Alloc.t_Global -> t_T366415196 - -and t_U = +type t_U = | U_A : t_U | U_B : t_U | U_C : Alloc.Vec.t_Vec t_T240131830 Alloc.Alloc.t_Global -> t_U +and t_T366415196 = + | T366415196_A : t_T366415196 + | T366415196_B : t_T366415196 + | T366415196_C : Alloc.Vec.t_Vec t_T240131830 Alloc.Alloc.t_Global -> t_T366415196 + and t_T240131830 = | T240131830_A : t_T240131830 | T240131830_B : t_T240131830 @@ -162,23 +162,23 @@ module Cyclic_modules.Enums_b open Core open FStar.Mul -include Cyclic_modules.Enums_b.Rec_bundle_994866580 {t_T366415196 as t_T} +include Cyclic_modules.Enums_b.Rec_bundle_902271266 {t_U as t_U} -include Cyclic_modules.Enums_b.Rec_bundle_994866580 {T366415196_A as T_A} +include Cyclic_modules.Enums_b.Rec_bundle_902271266 {U_A as U_A} -include Cyclic_modules.Enums_b.Rec_bundle_994866580 {T366415196_B as T_B} +include Cyclic_modules.Enums_b.Rec_bundle_902271266 {U_B as U_B} -include Cyclic_modules.Enums_b.Rec_bundle_994866580 {T366415196_C as T_C} +include Cyclic_modules.Enums_b.Rec_bundle_902271266 {U_C as U_C} -include Cyclic_modules.Enums_b.Rec_bundle_994866580 {t_U as t_U} +include Cyclic_modules.Enums_b.Rec_bundle_902271266 {t_T366415196 as t_T} -include Cyclic_modules.Enums_b.Rec_bundle_994866580 {U_A as U_A} +include Cyclic_modules.Enums_b.Rec_bundle_902271266 {T366415196_A as T_A} -include Cyclic_modules.Enums_b.Rec_bundle_994866580 {U_B as U_B} +include Cyclic_modules.Enums_b.Rec_bundle_902271266 {T366415196_B as T_B} -include Cyclic_modules.Enums_b.Rec_bundle_994866580 {U_C as U_C} +include Cyclic_modules.Enums_b.Rec_bundle_902271266 {T366415196_C as T_C} -include Cyclic_modules.Enums_b.Rec_bundle_994866580 {f as f} +include Cyclic_modules.Enums_b.Rec_bundle_902271266 {f as f} ''' "Cyclic_modules.Late_skip_a.fst" = ''' module Cyclic_modules.Late_skip_a @@ -186,10 +186,10 @@ module Cyclic_modules.Late_skip_a open Core open FStar.Mul -include Cyclic_modules.Late_skip_b.Rec_bundle_447022631 {f749016415 as f} +include Cyclic_modules.Late_skip_b.Rec_bundle_862592093 {f749016415 as f} ''' -"Cyclic_modules.Late_skip_b.Rec_bundle_447022631.fst" = ''' -module Cyclic_modules.Late_skip_b.Rec_bundle_447022631 +"Cyclic_modules.Late_skip_b.Rec_bundle_862592093.fst" = ''' +module Cyclic_modules.Late_skip_b.Rec_bundle_862592093 #set-options "--fuel 0 --ifuel 1 --z3rlimit 15" open Core open FStar.Mul @@ -205,7 +205,7 @@ module Cyclic_modules.Late_skip_b open Core open FStar.Mul -include Cyclic_modules.Late_skip_b.Rec_bundle_447022631 {f377825240 as f} +include Cyclic_modules.Late_skip_b.Rec_bundle_862592093 {f377825240 as f} ''' "Cyclic_modules.M1.fst" = ''' module Cyclic_modules.M1 @@ -213,20 +213,20 @@ module Cyclic_modules.M1 open Core open FStar.Mul -include Cyclic_modules.M2.Rec_bundle_489499412 {a as a} +include Cyclic_modules.M2.Rec_bundle_423840416 {a as a} ''' -"Cyclic_modules.M2.Rec_bundle_489499412.fst" = ''' -module Cyclic_modules.M2.Rec_bundle_489499412 +"Cyclic_modules.M2.Rec_bundle_423840416.fst" = ''' +module Cyclic_modules.M2.Rec_bundle_423840416 #set-options "--fuel 0 --ifuel 1 --z3rlimit 15" open Core open FStar.Mul +let d (_: Prims.unit) : Prims.unit = () + let c (_: Prims.unit) : Prims.unit = () let a (_: Prims.unit) : Prims.unit = c () -let d (_: Prims.unit) : Prims.unit = () - let b (_: Prims.unit) : Prims.unit = let _:Prims.unit = a () in d () @@ -237,11 +237,11 @@ module Cyclic_modules.M2 open Core open FStar.Mul -include Cyclic_modules.M2.Rec_bundle_489499412 {c as c} +include Cyclic_modules.M2.Rec_bundle_423840416 {d as d} -include Cyclic_modules.M2.Rec_bundle_489499412 {d as d} +include Cyclic_modules.M2.Rec_bundle_423840416 {c as c} -include Cyclic_modules.M2.Rec_bundle_489499412 {b as b} +include Cyclic_modules.M2.Rec_bundle_423840416 {b as b} ''' "Cyclic_modules.Rec.fst" = ''' module Cyclic_modules.Rec diff --git a/test-harness/src/snapshots/toolchain__enum-repr into-coq.snap b/test-harness/src/snapshots/toolchain__enum-repr into-coq.snap index bfe3bcc0a..6209a1837 100644 --- a/test-harness/src/snapshots/toolchain__enum-repr into-coq.snap +++ b/test-harness/src/snapshots/toolchain__enum-repr into-coq.snap @@ -42,11 +42,7 @@ Import RecordSetNotations. -Definition discriminant_EnumWithRepr_ExplicitDiscr1 : t_u16 := - 1. - -Definition discriminant_EnumWithRepr_ExplicitDiscr2 : t_u16 := - 5. +(* NotImplementedYet *) Inductive t_EnumWithRepr : Type := | EnumWithRepr_ExplicitDiscr1 @@ -56,6 +52,12 @@ Inductive t_EnumWithRepr : Type := Arguments t_EnumWithRepr:clear implicits. Arguments t_EnumWithRepr. +Definition discriminant_EnumWithRepr_ExplicitDiscr1 : t_u16 := + 1. + +Definition discriminant_EnumWithRepr_ExplicitDiscr2 : t_u16 := + 5. + Definition t_EnumWithRepr_cast_to_repr (x : t_EnumWithRepr) : t_u16 := match x with | EnumWithRepr_ExplicitDiscr1 => @@ -68,8 +70,6 @@ Definition t_EnumWithRepr_cast_to_repr (x : t_EnumWithRepr) : t_u16 := t_Add_f_add (discriminant_EnumWithRepr_ExplicitDiscr2) (2) end. -(* NotImplementedYet *) - Definition f (_ : unit) : t_u32 := let v__x := cast (t_Add_f_add (discriminant_EnumWithRepr_ExplicitDiscr2) (0)) in t_Add_f_add (cast (t_EnumWithRepr_cast_to_repr (EnumWithRepr_ImplicitDiscrEmptyTuple))) (cast (t_EnumWithRepr_cast_to_repr (EnumWithRepr_ImplicitDiscrEmptyStruct))). @@ -77,9 +77,9 @@ Definition f (_ : unit) : t_u32 := Definition ff__CONST : t_u16 := cast (t_Add_f_add (discriminant_EnumWithRepr_ExplicitDiscr1) (0)). -Definition get_casted_repr (x : t_EnumWithRepr) : t_u64 := - cast (t_EnumWithRepr_cast_to_repr (x)). - Definition get_repr (x : t_EnumWithRepr) : t_u16 := t_EnumWithRepr_cast_to_repr (x). + +Definition get_casted_repr (x : t_EnumWithRepr) : t_u64 := + cast (t_EnumWithRepr_cast_to_repr (x)). ''' diff --git a/test-harness/src/snapshots/toolchain__enum-repr into-fstar.snap b/test-harness/src/snapshots/toolchain__enum-repr into-fstar.snap index 600085987..e9c50a747 100644 --- a/test-harness/src/snapshots/toolchain__enum-repr into-fstar.snap +++ b/test-harness/src/snapshots/toolchain__enum-repr into-fstar.snap @@ -33,16 +33,16 @@ module Enum_repr open Core open FStar.Mul -let discriminant_EnumWithRepr_ExplicitDiscr1: u16 = 1us - -let discriminant_EnumWithRepr_ExplicitDiscr2: u16 = 5us - type t_EnumWithRepr = | EnumWithRepr_ExplicitDiscr1 : t_EnumWithRepr | EnumWithRepr_ExplicitDiscr2 : t_EnumWithRepr | EnumWithRepr_ImplicitDiscrEmptyTuple : t_EnumWithRepr | EnumWithRepr_ImplicitDiscrEmptyStruct : t_EnumWithRepr +let discriminant_EnumWithRepr_ExplicitDiscr1: u16 = 1us + +let discriminant_EnumWithRepr_ExplicitDiscr2: u16 = 5us + let t_EnumWithRepr_cast_to_repr (x: t_EnumWithRepr) : u16 = match x with | EnumWithRepr_ExplicitDiscr1 -> discriminant_EnumWithRepr_ExplicitDiscr1 @@ -64,7 +64,7 @@ let f (_: Prims.unit) : u32 = let ff__CONST: u16 = cast (discriminant_EnumWithRepr_ExplicitDiscr1 +! 0us <: u16) <: u16 -let get_casted_repr (x: t_EnumWithRepr) : u64 = cast (t_EnumWithRepr_cast_to_repr x <: u16) <: u64 - let get_repr (x: t_EnumWithRepr) : u16 = t_EnumWithRepr_cast_to_repr x + +let get_casted_repr (x: t_EnumWithRepr) : u64 = cast (t_EnumWithRepr_cast_to_repr x <: u16) <: u64 ''' diff --git a/test-harness/src/snapshots/toolchain__enum-repr into-ssprove.snap b/test-harness/src/snapshots/toolchain__enum-repr into-ssprove.snap index d1e4e4c09..613f21e5e 100644 --- a/test-harness/src/snapshots/toolchain__enum-repr into-ssprove.snap +++ b/test-harness/src/snapshots/toolchain__enum-repr into-ssprove.snap @@ -54,15 +54,7 @@ Import choice.Choice.Exports. Obligation Tactic := (* try timeout 8 *) solve_ssprove_obligations. -Equations discriminant_EnumWithRepr_ExplicitDiscr1 {L : {fset Location}} {I : Interface} : both L I int16 := - discriminant_EnumWithRepr_ExplicitDiscr1 := - solve_lift (ret_both (1 : int16)) : both L I int16. -Fail Next Obligation. - -Equations discriminant_EnumWithRepr_ExplicitDiscr2 {L : {fset Location}} {I : Interface} : both L I int16 := - discriminant_EnumWithRepr_ExplicitDiscr2 := - solve_lift (ret_both (5 : int16)) : both L I int16. -Fail Next Obligation. +(*Not implemented yet? todo(item)*) Definition t_EnumWithRepr : choice_type := ('unit ∐ 'unit ∐ 'unit ∐ 'unit). @@ -87,6 +79,16 @@ Equations EnumWithRepr_ImplicitDiscrEmptyStruct {L : {fset Location}} {I : Inter solve_lift (ret_both (inr (tt : 'unit) : t_EnumWithRepr)) : both L I t_EnumWithRepr. Fail Next Obligation. +Equations discriminant_EnumWithRepr_ExplicitDiscr1 {L : {fset Location}} {I : Interface} : both L I int16 := + discriminant_EnumWithRepr_ExplicitDiscr1 := + solve_lift (ret_both (1 : int16)) : both L I int16. +Fail Next Obligation. + +Equations discriminant_EnumWithRepr_ExplicitDiscr2 {L : {fset Location}} {I : Interface} : both L I int16 := + discriminant_EnumWithRepr_ExplicitDiscr2 := + solve_lift (ret_both (5 : int16)) : both L I int16. +Fail Next Obligation. + Equations t_EnumWithRepr_cast_to_repr {L1 : {fset Location}} {I1 : Interface} (x : both L1 I1 t_EnumWithRepr) : both L1 I1 int16 := t_EnumWithRepr_cast_to_repr x := matchb x with @@ -101,8 +103,6 @@ Equations t_EnumWithRepr_cast_to_repr {L1 : {fset Location}} {I1 : Interface} (x end : both L1 I1 int16. Fail Next Obligation. -(*Not implemented yet? todo(item)*) - Equations f {L1 : {fset Location}} {I1 : Interface} (_ : both L1 I1 'unit) : both L1 I1 int32 := f _ := letb v__x := cast_int (WS2 := _) (discriminant_EnumWithRepr_ExplicitDiscr2 .+ (ret_both (0 : int16))) in @@ -114,13 +114,13 @@ Equations ff__CONST {L : {fset Location}} {I : Interface} : both L I int16 := solve_lift (cast_int (WS2 := _) (discriminant_EnumWithRepr_ExplicitDiscr1 .+ (ret_both (0 : int16)))) : both L I int16. Fail Next Obligation. -Equations get_casted_repr {L1 : {fset Location}} {I1 : Interface} (x : both L1 I1 t_EnumWithRepr) : both L1 I1 int64 := - get_casted_repr x := - solve_lift (cast_int (WS2 := _) (t_EnumWithRepr_cast_to_repr x)) : both L1 I1 int64. -Fail Next Obligation. - Equations get_repr {L1 : {fset Location}} {I1 : Interface} (x : both L1 I1 t_EnumWithRepr) : both L1 I1 int16 := get_repr x := solve_lift (t_EnumWithRepr_cast_to_repr x) : both L1 I1 int16. Fail Next Obligation. + +Equations get_casted_repr {L1 : {fset Location}} {I1 : Interface} (x : both L1 I1 t_EnumWithRepr) : both L1 I1 int64 := + get_casted_repr x := + solve_lift (cast_int (WS2 := _) (t_EnumWithRepr_cast_to_repr x)) : both L1 I1 int64. +Fail Next Obligation. ''' diff --git a/test-harness/src/snapshots/toolchain__generics into-fstar.snap b/test-harness/src/snapshots/toolchain__generics into-fstar.snap index fa558e443..8f3ecf5e7 100644 --- a/test-harness/src/snapshots/toolchain__generics into-fstar.snap +++ b/test-harness/src/snapshots/toolchain__generics into-fstar.snap @@ -43,26 +43,6 @@ 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 = - () - -type t_Bar = | Bar : t_Bar - -class t_Foo (v_Self: Type0) = { - f_const_add_pre:v_N: usize -> v_Self -> Type0; - f_const_add_post:v_N: usize -> v_Self -> usize -> Type0; - 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 = - { - 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 (#v_T: Type0) (#[FStar.Tactics.Typeclasses.tcresolve ()] i1: Core.Clone.t_Clone v_T) @@ -73,6 +53,30 @@ let dup <: (v_T & v_T) +let foo (v_LEN: usize) (arr: t_Array usize v_LEN) : usize = + let acc:usize = v_LEN +! sz 9 in + let acc:usize = + Rust_primitives.Hax.Folds.fold_range (sz 0) + v_LEN + (fun acc temp_1_ -> + let acc:usize = acc in + let _:usize = temp_1_ in + true) + acc + (fun acc i -> + let acc:usize = acc in + let i:usize = i in + acc +! (arr.[ i ] <: usize) <: usize) + in + acc + +let repeat + (v_LEN: usize) + (#v_T: Type0) + (#[FStar.Tactics.Typeclasses.tcresolve ()] i1: Core.Marker.t_Copy v_T) + (x: v_T) + : t_Array v_T v_LEN = Rust_primitives.Hax.repeat x v_LEN + 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 @@ -110,27 +114,23 @@ let call_g (_: Prims.unit) : usize = usize) +! sz 3 -let foo (v_LEN: usize) (arr: t_Array usize v_LEN) : usize = - let acc:usize = v_LEN +! sz 9 in - let acc:usize = - Rust_primitives.Hax.Folds.fold_range (sz 0) - v_LEN - (fun acc temp_1_ -> - let acc:usize = acc in - let _:usize = temp_1_ in - true) - acc - (fun acc i -> - let acc:usize = acc in - let i:usize = i in - acc +! (arr.[ i ] <: usize) <: usize) - in - acc +class t_Foo (v_Self: Type0) = { + f_const_add_pre:v_N: usize -> v_Self -> Type0; + f_const_add_post:v_N: usize -> v_Self -> usize -> Type0; + 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) +} -let repeat - (v_LEN: usize) - (#v_T: Type0) - (#[FStar.Tactics.Typeclasses.tcresolve ()] i1: Core.Marker.t_Copy v_T) - (x: v_T) - : t_Array v_T v_LEN = Rust_primitives.Hax.repeat x v_LEN +[@@ FStar.Tactics.Typeclasses.tcinstance] +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 + } + +type t_Bar = | Bar : t_Bar + +let impl__Bar__inherent_impl_generics (#v_T: Type0) (v_N: usize) (x: t_Array v_T v_N) : Prims.unit = + () ''' diff --git a/test-harness/src/snapshots/toolchain__guards into-coq.snap b/test-harness/src/snapshots/toolchain__guards into-coq.snap index abd2a3274..7755eb3aa 100644 --- a/test-harness/src/snapshots/toolchain__guards into-coq.snap +++ b/test-harness/src/snapshots/toolchain__guards into-coq.snap @@ -43,7 +43,7 @@ Import RecordSetNotations. (* NotImplementedYet *) -Definition equivalent (x : t_Option ((t_Result ((t_i32)) ((t_i32))))) : t_i32 := +Definition if_let_guard (x : t_Option ((t_Result ((t_i32)) ((t_i32))))) : t_i32 := match x with | Option_None => 0 @@ -59,8 +59,8 @@ Definition equivalent (x : t_Option ((t_Result ((t_i32)) ((t_i32))))) : t_i32 := | _ => Option_None end with - | Option_Some (y) => - y + | Option_Some (x) => + x | Option_None => match x with | Option_Some (Result_Err (y)) => @@ -71,25 +71,7 @@ Definition equivalent (x : t_Option ((t_Result ((t_i32)) ((t_i32))))) : t_i32 := end end. -Definition if_guard (x : t_Option ((t_i32))) : t_i32 := - match match x with - | Option_Some (v) => - match t_PartialOrd_f_gt (v) (0) with - | true => - Option_Some (v) - | _ => - Option_None - end - | _ => - Option_None - end with - | Option_Some (x) => - x - | Option_None => - 0 - end. - -Definition if_let_guard (x : t_Option ((t_Result ((t_i32)) ((t_i32))))) : t_i32 := +Definition equivalent (x : t_Option ((t_Result ((t_i32)) ((t_i32))))) : t_i32 := match x with | Option_None => 0 @@ -105,8 +87,8 @@ Definition if_let_guard (x : t_Option ((t_Result ((t_i32)) ((t_i32))))) : t_i32 | _ => Option_None end with - | Option_Some (x) => - x + | Option_Some (y) => + y | Option_None => match x with | Option_Some (Result_Err (y)) => @@ -159,4 +141,22 @@ Definition multiple_guards (x : t_Option ((t_Result ((t_i32)) ((t_i32))))) : t_i end end end. + +Definition if_guard (x : t_Option ((t_i32))) : t_i32 := + match match x with + | Option_Some (v) => + match t_PartialOrd_f_gt (v) (0) with + | true => + Option_Some (v) + | _ => + Option_None + end + | _ => + Option_None + end with + | Option_Some (x) => + x + | Option_None => + 0 + end. ''' diff --git a/test-harness/src/snapshots/toolchain__guards into-fstar.snap b/test-harness/src/snapshots/toolchain__guards into-fstar.snap index ff12f664a..d575e5eca 100644 --- a/test-harness/src/snapshots/toolchain__guards into-fstar.snap +++ b/test-harness/src/snapshots/toolchain__guards into-fstar.snap @@ -32,7 +32,7 @@ module Guards open Core open FStar.Mul -let equivalent (x: Core.Option.t_Option (Core.Result.t_Result i32 i32)) : i32 = +let if_let_guard (x: Core.Option.t_Option (Core.Result.t_Result i32 i32)) : i32 = match x with | Core.Option.Option_None -> 0l | _ -> @@ -44,25 +44,13 @@ let equivalent (x: Core.Option.t_Option (Core.Result.t_Result i32 i32)) : i32 = | _ -> Core.Option.Option_None <: Core.Option.t_Option i32) | _ -> Core.Option.Option_None <: Core.Option.t_Option i32 with - | Core.Option.Option_Some y -> y + | Core.Option.Option_Some x -> x | Core.Option.Option_None -> match x with | Core.Option.Option_Some (Core.Result.Result_Err y) -> y | _ -> 1l -let if_guard (x: Core.Option.t_Option i32) : i32 = - match - match x with - | Core.Option.Option_Some v -> - (match v >. 0l with - | true -> Core.Option.Option_Some v <: Core.Option.t_Option i32 - | _ -> Core.Option.Option_None <: Core.Option.t_Option i32) - | _ -> Core.Option.Option_None <: Core.Option.t_Option i32 - with - | Core.Option.Option_Some x -> x - | Core.Option.Option_None -> 0l - -let if_let_guard (x: Core.Option.t_Option (Core.Result.t_Result i32 i32)) : i32 = +let equivalent (x: Core.Option.t_Option (Core.Result.t_Result i32 i32)) : i32 = match x with | Core.Option.Option_None -> 0l | _ -> @@ -74,7 +62,7 @@ let if_let_guard (x: Core.Option.t_Option (Core.Result.t_Result i32 i32)) : i32 | _ -> Core.Option.Option_None <: Core.Option.t_Option i32) | _ -> Core.Option.Option_None <: Core.Option.t_Option i32 with - | Core.Option.Option_Some x -> x + | Core.Option.Option_Some y -> y | Core.Option.Option_None -> match x with | Core.Option.Option_Some (Core.Result.Result_Err y) -> y @@ -107,4 +95,16 @@ let multiple_guards (x: Core.Option.t_Option (Core.Result.t_Result i32 i32)) : i match x with | Core.Option.Option_Some (Core.Result.Result_Err y) -> y | _ -> 1l + +let if_guard (x: Core.Option.t_Option i32) : i32 = + match + match x with + | Core.Option.Option_Some v -> + (match v >. 0l with + | true -> Core.Option.Option_Some v <: Core.Option.t_Option i32 + | _ -> Core.Option.Option_None <: Core.Option.t_Option i32) + | _ -> Core.Option.Option_None <: Core.Option.t_Option i32 + with + | Core.Option.Option_Some x -> x + | Core.Option.Option_None -> 0l ''' diff --git a/test-harness/src/snapshots/toolchain__guards into-ssprove.snap b/test-harness/src/snapshots/toolchain__guards into-ssprove.snap index 57b079118..a499287d3 100644 --- a/test-harness/src/snapshots/toolchain__guards into-ssprove.snap +++ b/test-harness/src/snapshots/toolchain__guards into-ssprove.snap @@ -55,8 +55,8 @@ Obligation Tactic := (* try timeout 8 *) solve_ssprove_obligations. (*Not implemented yet? todo(item)*) -Equations equivalent {L1 : {fset Location}} {I1 : Interface} (x : both L1 I1 (t_Option (t_Result int32 int32))) : both L1 I1 int32 := - equivalent x := +Equations if_let_guard {L1 : {fset Location}} {I1 : Interface} (x : both L1 I1 (t_Option (t_Result int32 int32))) : both L1 I1 int32 := + if_let_guard x := matchb x with | Option_None_case => solve_lift (ret_both (0 : int32)) @@ -74,9 +74,9 @@ Equations equivalent {L1 : {fset Location}} {I1 : Interface} (x : both L1 I1 (t_ | _ => Option_None end with - | Option_Some_case y => - letb y := ret_both ((y) : (int32)) in - solve_lift y + | Option_Some_case x => + letb x := ret_both ((x) : (int32)) in + solve_lift x | Option_None_case => matchb x with | Option_Some_case Result_Err y => @@ -89,30 +89,8 @@ Equations equivalent {L1 : {fset Location}} {I1 : Interface} (x : both L1 I1 (t_ end : both L1 I1 int32. Fail Next Obligation. -Equations if_guard {L1 : {fset Location}} {I1 : Interface} (x : both L1 I1 (t_Option int32)) : both L1 I1 int32 := - if_guard x := - matchb matchb x with - | Option_Some_case v => - letb v := ret_both ((v) : (int32)) in - matchb v >.? (ret_both (0 : int32)) with - | true => - Option_Some (solve_lift v) - | _ => - Option_None - end - | _ => - Option_None - end with - | Option_Some_case x => - letb x := ret_both ((x) : (int32)) in - solve_lift x - | Option_None_case => - solve_lift (ret_both (0 : int32)) - end : both L1 I1 int32. -Fail Next Obligation. - -Equations if_let_guard {L1 : {fset Location}} {I1 : Interface} (x : both L1 I1 (t_Option (t_Result int32 int32))) : both L1 I1 int32 := - if_let_guard x := +Equations equivalent {L1 : {fset Location}} {I1 : Interface} (x : both L1 I1 (t_Option (t_Result int32 int32))) : both L1 I1 int32 := + equivalent x := matchb x with | Option_None_case => solve_lift (ret_both (0 : int32)) @@ -130,9 +108,9 @@ Equations if_let_guard {L1 : {fset Location}} {I1 : Interface} (x : both L1 I1 ( | _ => Option_None end with - | Option_Some_case x => - letb x := ret_both ((x) : (int32)) in - solve_lift x + | Option_Some_case y => + letb y := ret_both ((y) : (int32)) in + solve_lift y | Option_None_case => matchb x with | Option_Some_case Result_Err y => @@ -196,4 +174,26 @@ Equations multiple_guards {L1 : {fset Location}} {I1 : Interface} (x : both L1 I end end : both L1 I1 int32. Fail Next Obligation. + +Equations if_guard {L1 : {fset Location}} {I1 : Interface} (x : both L1 I1 (t_Option int32)) : both L1 I1 int32 := + if_guard x := + matchb matchb x with + | Option_Some_case v => + letb v := ret_both ((v) : (int32)) in + matchb v >.? (ret_both (0 : int32)) with + | true => + Option_Some (solve_lift v) + | _ => + Option_None + end + | _ => + Option_None + end with + | Option_Some_case x => + letb x := ret_both ((x) : (int32)) in + solve_lift x + | Option_None_case => + solve_lift (ret_both (0 : int32)) + end : both L1 I1 int32. +Fail Next Obligation. ''' diff --git a/test-harness/src/snapshots/toolchain__include-flag into-coq.snap b/test-harness/src/snapshots/toolchain__include-flag into-coq.snap index c86f3b275..04abbc64e 100644 --- a/test-harness/src/snapshots/toolchain__include-flag into-coq.snap +++ b/test-harness/src/snapshots/toolchain__include-flag into-coq.snap @@ -41,6 +41,8 @@ Import RecordSetNotations. +(* NotImplementedYet *) + Record t_Foo : Type := { }. @@ -60,14 +62,24 @@ Instance t_Trait_254780795 : t_Trait ((t_Foo)) := { }. -(* NotImplementedYet *) - Definition main_a_a (_ : unit) : unit := tt. +Definition main_b_a (_ : unit) : unit := + tt. + +Definition main_c_a (_ : unit) : unit := + tt. + Definition main_a_b (_ : unit) : unit := tt. +Definition main_b_b (_ : unit) : unit := + tt. + +Definition main_c_b (_ : unit) : unit := + tt. + Definition main_a_c (_ : unit) : unit := tt. @@ -77,12 +89,6 @@ Definition main_a `{v_T : Type} `{t_Sized (v_T)} `{t_Trait (v_T)} (x : v_T) : un let _ := main_a_c (tt) in tt. -Definition main_b_a (_ : unit) : unit := - tt. - -Definition main_b_b (_ : unit) : unit := - tt. - Definition main_b_c (_ : unit) : unit := tt. @@ -92,12 +98,6 @@ Definition main_b (_ : unit) : unit := let _ := main_b_c (tt) in tt. -Definition main_c_a (_ : unit) : unit := - tt. - -Definition main_c_b (_ : unit) : unit := - tt. - Definition main_c_c (_ : unit) : unit := tt. diff --git a/test-harness/src/snapshots/toolchain__include-flag into-fstar.snap b/test-harness/src/snapshots/toolchain__include-flag into-fstar.snap index 41cd2ac28..de9402027 100644 --- a/test-harness/src/snapshots/toolchain__include-flag into-fstar.snap +++ b/test-harness/src/snapshots/toolchain__include-flag into-fstar.snap @@ -42,8 +42,16 @@ let impl_Trait_for_Foo: t_Trait t_Foo = { __marker_trait = () } /// Indirect dependencies let main_a_a (_: Prims.unit) : Prims.unit = () +let main_b_a (_: Prims.unit) : Prims.unit = () + +let main_c_a (_: Prims.unit) : Prims.unit = () + let main_a_b (_: Prims.unit) : Prims.unit = () +let main_b_b (_: Prims.unit) : Prims.unit = () + +let main_c_b (_: Prims.unit) : Prims.unit = () + let main_a_c (_: Prims.unit) : Prims.unit = () /// Direct dependencies @@ -54,10 +62,6 @@ let main_a (#v_T: Type0) (#[FStar.Tactics.Typeclasses.tcresolve ()] i1: t_Trait let _:Prims.unit = main_a_c () in () -let main_b_a (_: Prims.unit) : Prims.unit = () - -let main_b_b (_: Prims.unit) : Prims.unit = () - let main_b_c (_: Prims.unit) : Prims.unit = () let main_b (_: Prims.unit) : Prims.unit = @@ -66,10 +70,6 @@ let main_b (_: Prims.unit) : Prims.unit = let _:Prims.unit = main_b_c () in () -let main_c_a (_: Prims.unit) : Prims.unit = () - -let main_c_b (_: Prims.unit) : Prims.unit = () - let main_c_c (_: Prims.unit) : Prims.unit = () let main_c (_: 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 index 9aaa938a6..7b58e61f3 100644 --- a/test-harness/src/snapshots/toolchain__interface-only into-fstar.snap +++ b/test-harness/src/snapshots/toolchain__interface-only into-fstar.snap @@ -33,11 +33,20 @@ module Interface_only open Core open FStar.Mul -type t_Bar = | Bar : t_Bar - -type t_Holder (v_T: Type0) = { f_value:Alloc.Vec.t_Vec v_T Alloc.Alloc.t_Global } +/// This item contains unsafe blocks and raw references, two features +/// not supported by hax. Thanks to the `-i` flag and the `+:` +/// modifier, `f` is still extractable as an interface. +/// Expressions within type are still extracted, as well as pre- and +/// post-conditions. +val f (x: u8) + : Prims.Pure (t_Array u8 (sz 4)) + (requires x <. 254uy) + (ensures + fun r -> + let r:t_Array u8 (sz 4) = r in + (r.[ sz 0 ] <: u8) >. x) -type t_Param (v_SIZE: usize) = { f_value:t_Array u8 v_SIZE } +type t_Bar = | Bar : t_Bar /// Non-inherent implementations are extracted, their bodies are not /// dropped. This might be a bit surprising: see @@ -51,22 +60,13 @@ val impl_1:Core.Convert.t_From t_Bar u8 val from__from: u8 -> Prims.Pure t_Bar Prims.l_True (fun _ -> Prims.l_True) +type t_Holder (v_T: Type0) = { f_value:Alloc.Vec.t_Vec v_T Alloc.Alloc.t_Global } + [@@ FStar.Tactics.Typeclasses.tcinstance] val impl_2 (#v_T: Type0) : Core.Convert.t_From (t_Holder v_T) Prims.unit +type t_Param (v_SIZE: usize) = { f_value:t_Array u8 v_SIZE } + [@@ FStar.Tactics.Typeclasses.tcinstance] val impl_3 (v_SIZE: usize) : Core.Convert.t_From (t_Param v_SIZE) Prims.unit - -/// This item contains unsafe blocks and raw references, two features -/// not supported by hax. Thanks to the `-i` flag and the `+:` -/// modifier, `f` is still extractable as an interface. -/// Expressions within type are still extracted, as well as pre- and -/// post-conditions. -val f (x: u8) - : Prims.Pure (t_Array u8 (sz 4)) - (requires x <. 254uy) - (ensures - fun r -> - let r:t_Array u8 (sz 4) = r in - (r.[ sz 0 ] <: u8) >. x) ''' diff --git a/test-harness/src/snapshots/toolchain__literals into-coq.snap b/test-harness/src/snapshots/toolchain__literals into-coq.snap index 77d4150c3..f0b5dc23a 100644 --- a/test-harness/src/snapshots/toolchain__literals into-coq.snap +++ b/test-harness/src/snapshots/toolchain__literals into-coq.snap @@ -42,39 +42,10 @@ Import RecordSetNotations. -From Literals Require Import Hax_lib (t_int). -Export Hax_lib (t_int). - -Record t_Foo : Type := - { - f_field : t_u8; - }. -Arguments t_Foo:clear implicits. -Arguments t_Foo. -Arguments Build_t_Foo. -#[export] Instance settable_t_Foo : Settable _ := - settable! (@Build_t_Foo) . - (* NotImplementedYet *) -Definition v_CONSTANT : t_Foo := - Build_t_Foo (3). - -Definition casts (x8 : t_u8) (x16 : t_u16) (x32 : t_u32) (x64 : t_u64) (xs : t_usize) : unit := - let _ : t_u64 := t_Add_f_add (t_Add_f_add (t_Add_f_add (t_Add_f_add (cast (x8)) (cast (x16))) (cast (x32))) (x64)) (cast (xs)) in - let _ : t_u32 := t_Add_f_add (t_Add_f_add (t_Add_f_add (t_Add_f_add (cast (x8)) (cast (x16))) (x32)) (cast (x64))) (cast (xs)) in - let _ : t_u16 := t_Add_f_add (t_Add_f_add (t_Add_f_add (t_Add_f_add (cast (x8)) (x16)) (cast (x32))) (cast (x64))) (cast (xs)) in - let _ : t_u8 := t_Add_f_add (t_Add_f_add (t_Add_f_add (t_Add_f_add (x8) (cast (x16))) (cast (x32))) (cast (x64))) (cast (xs)) in - let _ : t_i64 := t_Add_f_add (t_Add_f_add (t_Add_f_add (t_Add_f_add (cast (x8)) (cast (x16))) (cast (x32))) (cast (x64))) (cast (xs)) in - let _ : t_i32 := t_Add_f_add (t_Add_f_add (t_Add_f_add (t_Add_f_add (cast (x8)) (cast (x16))) (cast (x32))) (cast (x64))) (cast (xs)) in - let _ : t_i16 := t_Add_f_add (t_Add_f_add (t_Add_f_add (t_Add_f_add (cast (x8)) (cast (x16))) (cast (x32))) (cast (x64))) (cast (xs)) in - let _ : t_i8 := t_Add_f_add (t_Add_f_add (t_Add_f_add (t_Add_f_add (cast (x8)) (cast (x16))) (cast (x32))) (cast (x64))) (cast (xs)) in - tt. - -Definition fn_pointer_cast (_ : unit) : unit := - let f : t_u32 -> t_u32 := fun x => - x in - tt. +From Literals Require Import Hax_lib (t_int). +Export Hax_lib (t_int). Definition math_integers (x : t_Int) `{andb (f_gt (x) (impl__Int___unsafe_from_str ("0"%string))) (f_lt (x) (impl__Int___unsafe_from_str ("16"%string))) = true} : t_u8 := let _ : t_Int := f_lift (3) in @@ -100,6 +71,22 @@ Definition math_integers (x : t_Int) `{andb (f_gt (x) (impl__Int___unsafe_from_s let _ : t_usize := impl__Int__to_usize (x) in impl__Int__to_u8 (f_add (x) (f_mul (x) (x))). +Definition panic_with_msg (_ : unit) : unit := + never_to_any (panic_fmt (impl_2__new_const (["with msg"%string]))). + +Record t_Foo : Type := + { + f_field : t_u8; + }. +Arguments t_Foo:clear implicits. +Arguments t_Foo. +Arguments Build_t_Foo. +#[export] Instance settable_t_Foo : Settable _ := + settable! (@Build_t_Foo) . + +Definition v_CONSTANT : t_Foo := + Build_t_Foo (3). + Definition numeric (_ : unit) : unit := let _ : t_usize := 123 in let _ : t_isize := -42 in @@ -129,10 +116,23 @@ Definition patterns (_ : unit) : unit := end in tt. -Definition panic_with_msg (_ : unit) : unit := - never_to_any (panic_fmt (impl_2__new_const (["with msg"%string]))). +Definition casts (x8 : t_u8) (x16 : t_u16) (x32 : t_u32) (x64 : t_u64) (xs : t_usize) : unit := + let _ : t_u64 := t_Add_f_add (t_Add_f_add (t_Add_f_add (t_Add_f_add (cast (x8)) (cast (x16))) (cast (x32))) (x64)) (cast (xs)) in + let _ : t_u32 := t_Add_f_add (t_Add_f_add (t_Add_f_add (t_Add_f_add (cast (x8)) (cast (x16))) (x32)) (cast (x64))) (cast (xs)) in + let _ : t_u16 := t_Add_f_add (t_Add_f_add (t_Add_f_add (t_Add_f_add (cast (x8)) (x16)) (cast (x32))) (cast (x64))) (cast (xs)) in + let _ : t_u8 := t_Add_f_add (t_Add_f_add (t_Add_f_add (t_Add_f_add (x8) (cast (x16))) (cast (x32))) (cast (x64))) (cast (xs)) in + let _ : t_i64 := t_Add_f_add (t_Add_f_add (t_Add_f_add (t_Add_f_add (cast (x8)) (cast (x16))) (cast (x32))) (cast (x64))) (cast (xs)) in + let _ : t_i32 := t_Add_f_add (t_Add_f_add (t_Add_f_add (t_Add_f_add (cast (x8)) (cast (x16))) (cast (x32))) (cast (x64))) (cast (xs)) in + let _ : t_i16 := t_Add_f_add (t_Add_f_add (t_Add_f_add (t_Add_f_add (cast (x8)) (cast (x16))) (cast (x32))) (cast (x64))) (cast (xs)) in + let _ : t_i8 := t_Add_f_add (t_Add_f_add (t_Add_f_add (t_Add_f_add (cast (x8)) (cast (x16))) (cast (x32))) (cast (x64))) (cast (xs)) in + tt. Definition empty_array (_ : unit) : unit := let _ : t_Slice t_u8 := unsize ([]) in tt. + +Definition fn_pointer_cast (_ : unit) : unit := + let f : t_u32 -> t_u32 := fun x => + x 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 f6c262b10..60e23edb4 100644 --- a/test-harness/src/snapshots/toolchain__literals into-fstar.snap +++ b/test-harness/src/snapshots/toolchain__literals into-fstar.snap @@ -33,10 +33,86 @@ module Literals open Core open FStar.Mul +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)) + (fun _ -> Prims.l_True) = + let (_: Hax_lib.Int.t_Int):Hax_lib.Int.t_Int = Rust_primitives.Hax.Int.from_machine (sz 3) in + let _:bool = + ((-340282366920938463463374607431768211455000) <: Hax_lib.Int.t_Int) > + (340282366920938463463374607431768211455000 <: Hax_lib.Int.t_Int) + in + let _:bool = x < x in + let _:bool = x >= x in + let _:bool = x <= x in + let _:bool = x <> x in + let _:bool = x = x in + let _:Hax_lib.Int.t_Int = x + x in + let _:Hax_lib.Int.t_Int = x - x in + let _:Hax_lib.Int.t_Int = x * x in + let _:Hax_lib.Int.t_Int = x / x in + let (_: i16):i16 = Hax_lib.Int.impl__Int__to_i16 x in + let (_: i32):i32 = Hax_lib.Int.impl__Int__to_i32 x in + let (_: i64):i64 = Hax_lib.Int.impl__Int__to_i64 x in + let (_: i128):i128 = Hax_lib.Int.impl__Int__to_i128 x in + let (_: isize):isize = Hax_lib.Int.impl__Int__to_isize x in + let (_: u16):u16 = Hax_lib.Int.impl__Int__to_u16 x in + let (_: u32):u32 = Hax_lib.Int.impl__Int__to_u32 x in + let (_: u64):u64 = Hax_lib.Int.impl__Int__to_u64 x in + let (_: u128):u128 = Hax_lib.Int.impl__Int__to_u128 x in + 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 panic_with_msg (_: Prims.unit) : Prims.unit = + Rust_primitives.Hax.never_to_any (Core.Panicking.panic_fmt (Core.Fmt.impl_2__new_const (sz 1) + (let list = ["with msg"] in + FStar.Pervasives.assert_norm (Prims.eq2 (List.Tot.length list) 1); + Rust_primitives.Hax.array_of_list 1 list) + <: + Core.Fmt.t_Arguments) + <: + Rust_primitives.Hax.t_Never) + type t_Foo = { f_field:u8 } let v_CONSTANT: t_Foo = { f_field = 3uy } <: t_Foo +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 patterns (_: Prims.unit) : Prims.unit = + let _:Prims.unit = + match 1uy with + | 2uy -> () <: Prims.unit + | _ -> () <: Prims.unit + in + let _:Prims.unit = + match + "hello", + (123l, + (let list = ["a"; "b"] in + FStar.Pervasives.assert_norm (Prims.eq2 (List.Tot.length list) 2); + Rust_primitives.Hax.array_of_list 2 list) + <: + (i32 & t_Array string (sz 2))) + <: + (string & (i32 & t_Array string (sz 2))) + with + | "hello", (123l, v__todo) -> () <: Prims.unit + | _ -> () <: Prims.unit + in + let _:Prims.unit = + match { f_field = 4uy } <: t_Foo with + | { f_field = 3uy } -> () <: Prims.unit + | _ -> () <: Prims.unit + 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) @@ -106,87 +182,6 @@ let casts (x8: u8) (x16: u16) (x32: u32) (x64: u64) (xs: usize) : Prims.unit = in () -/// https://github.com/hacspec/hax/issues/500 -let fn_pointer_cast (_: Prims.unit) : Prims.unit = - let (f: (u32 -> u32)): u32 -> u32 = fun x -> x 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)) - (fun _ -> Prims.l_True) = - let (_: Hax_lib.Int.t_Int):Hax_lib.Int.t_Int = Rust_primitives.Hax.Int.from_machine (sz 3) in - let _:bool = - ((-340282366920938463463374607431768211455000) <: Hax_lib.Int.t_Int) > - (340282366920938463463374607431768211455000 <: Hax_lib.Int.t_Int) - in - let _:bool = x < x in - let _:bool = x >= x in - let _:bool = x <= x in - let _:bool = x <> x in - let _:bool = x = x in - let _:Hax_lib.Int.t_Int = x + x in - let _:Hax_lib.Int.t_Int = x - x in - let _:Hax_lib.Int.t_Int = x * x in - let _:Hax_lib.Int.t_Int = x / x in - let (_: i16):i16 = Hax_lib.Int.impl__Int__to_i16 x in - let (_: i32):i32 = Hax_lib.Int.impl__Int__to_i32 x in - let (_: i64):i64 = Hax_lib.Int.impl__Int__to_i64 x in - let (_: i128):i128 = Hax_lib.Int.impl__Int__to_i128 x in - let (_: isize):isize = Hax_lib.Int.impl__Int__to_isize x in - let (_: u16):u16 = Hax_lib.Int.impl__Int__to_u16 x in - let (_: u32):u32 = Hax_lib.Int.impl__Int__to_u32 x in - let (_: u64):u64 = Hax_lib.Int.impl__Int__to_u64 x in - let (_: u128):u128 = Hax_lib.Int.impl__Int__to_u128 x in - 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 patterns (_: Prims.unit) : Prims.unit = - let _:Prims.unit = - match 1uy with - | 2uy -> () <: Prims.unit - | _ -> () <: Prims.unit - in - let _:Prims.unit = - match - "hello", - (123l, - (let list = ["a"; "b"] in - FStar.Pervasives.assert_norm (Prims.eq2 (List.Tot.length list) 2); - Rust_primitives.Hax.array_of_list 2 list) - <: - (i32 & t_Array string (sz 2))) - <: - (string & (i32 & t_Array string (sz 2))) - with - | "hello", (123l, v__todo) -> () <: Prims.unit - | _ -> () <: Prims.unit - in - let _:Prims.unit = - match { f_field = 4uy } <: t_Foo with - | { f_field = 3uy } -> () <: Prims.unit - | _ -> () <: Prims.unit - in - () - -let panic_with_msg (_: Prims.unit) : Prims.unit = - Rust_primitives.Hax.never_to_any (Core.Panicking.panic_fmt (Core.Fmt.impl_2__new_const (sz 1) - (let list = ["with msg"] in - FStar.Pervasives.assert_norm (Prims.eq2 (List.Tot.length list) 1); - Rust_primitives.Hax.array_of_list 1 list) - <: - Core.Fmt.t_Arguments) - <: - Rust_primitives.Hax.t_Never) - let empty_array (_: Prims.unit) : Prims.unit = let (_: t_Slice u8):t_Slice u8 = (let list:Prims.list u8 = [] in @@ -196,4 +191,9 @@ let empty_array (_: Prims.unit) : Prims.unit = t_Slice u8 in () + +/// https://github.com/hacspec/hax/issues/500 +let fn_pointer_cast (_: Prims.unit) : Prims.unit = + let (f: (u32 -> u32)): u32 -> u32 = fun x -> x in + () ''' diff --git a/test-harness/src/snapshots/toolchain__loops into-fstar.snap b/test-harness/src/snapshots/toolchain__loops into-fstar.snap index 2c35945ca..ab5457375 100644 --- a/test-harness/src/snapshots/toolchain__loops into-fstar.snap +++ b/test-harness/src/snapshots/toolchain__loops into-fstar.snap @@ -33,80 +33,6 @@ module Loops.Control_flow open Core open FStar.Mul -type t_M = { f_m:Alloc.Vec.t_Vec u8 Alloc.Alloc.t_Global } - -let impl__M__decoded_message (self: t_M) - : Core.Option.t_Option (Alloc.Vec.t_Vec u8 Alloc.Alloc.t_Global) = - match - Rust_primitives.Hax.Folds.fold_range_return (sz 0) - (Alloc.Vec.impl_1__len #u8 #Alloc.Alloc.t_Global self.f_m <: usize) - (fun temp_0_ temp_1_ -> - let _:Prims.unit = temp_0_ in - let _:usize = temp_1_ in - true) - () - (fun temp_0_ i -> - let _:Prims.unit = temp_0_ in - let i:usize = i in - if i >. sz 5 <: bool - then - Core.Ops.Control_flow.ControlFlow_Break - (Core.Ops.Control_flow.ControlFlow_Break - (Core.Option.Option_None - <: - Core.Option.t_Option (Alloc.Vec.t_Vec u8 Alloc.Alloc.t_Global)) - <: - Core.Ops.Control_flow.t_ControlFlow - (Core.Option.t_Option (Alloc.Vec.t_Vec u8 Alloc.Alloc.t_Global)) - (Prims.unit & Prims.unit)) - <: - Core.Ops.Control_flow.t_ControlFlow - (Core.Ops.Control_flow.t_ControlFlow - (Core.Option.t_Option (Alloc.Vec.t_Vec u8 Alloc.Alloc.t_Global)) - (Prims.unit & Prims.unit)) Prims.unit - else - Core.Ops.Control_flow.ControlFlow_Continue () - <: - Core.Ops.Control_flow.t_ControlFlow - (Core.Ops.Control_flow.t_ControlFlow - (Core.Option.t_Option (Alloc.Vec.t_Vec u8 Alloc.Alloc.t_Global)) - (Prims.unit & Prims.unit)) Prims.unit) - with - | Core.Ops.Control_flow.ControlFlow_Break ret -> ret - | Core.Ops.Control_flow.ControlFlow_Continue _ -> - Core.Option.Option_Some - (Core.Clone.f_clone #(Alloc.Vec.t_Vec u8 Alloc.Alloc.t_Global) - #FStar.Tactics.Typeclasses.solve - self.f_m) - <: - Core.Option.t_Option (Alloc.Vec.t_Vec u8 Alloc.Alloc.t_Global) - -let bigger_power_2_ (x: i32) : i32 = - let pow:i32 = 1l in - Rust_primitives.f_while_loop_cf (fun pow -> - let pow:i32 = pow in - pow <. 1000000l <: bool) - pow - (fun pow -> - let pow:i32 = pow in - let pow:i32 = pow *! 2l in - if pow <. x - then - let pow:i32 = pow *! 3l in - if true - then - Core.Ops.Control_flow.ControlFlow_Break ((), pow <: (Prims.unit & i32)) - <: - Core.Ops.Control_flow.t_ControlFlow (Prims.unit & i32) i32 - else - Core.Ops.Control_flow.ControlFlow_Continue (pow *! 2l) - <: - Core.Ops.Control_flow.t_ControlFlow (Prims.unit & i32) i32 - else - Core.Ops.Control_flow.ControlFlow_Continue (pow *! 2l) - <: - Core.Ops.Control_flow.t_ControlFlow (Prims.unit & i32) i32) - let double_sum (_: Prims.unit) : i32 = let sum:i32 = 0l in let sum:i32 = @@ -160,6 +86,36 @@ let double_sum2 (_: Prims.unit) : i32 = in sum +! sum2 +let double_sum_return (v: t_Slice i32) : i32 = + let sum:i32 = 0l in + match + Rust_primitives.Hax.f_fold_return (Core.Iter.Traits.Collect.f_into_iter #(t_Slice i32) + #FStar.Tactics.Typeclasses.solve + v + <: + Core.Slice.Iter.t_Iter i32) + sum + (fun sum i -> + let sum:i32 = sum in + let i:i32 = i in + if i <. 0l <: bool + then + Core.Ops.Control_flow.ControlFlow_Break + (Core.Ops.Control_flow.ControlFlow_Break 0l + <: + Core.Ops.Control_flow.t_ControlFlow i32 (Prims.unit & i32)) + <: + Core.Ops.Control_flow.t_ControlFlow + (Core.Ops.Control_flow.t_ControlFlow i32 (Prims.unit & i32)) i32 + else + Core.Ops.Control_flow.ControlFlow_Continue (sum +! i <: i32) + <: + Core.Ops.Control_flow.t_ControlFlow + (Core.Ops.Control_flow.t_ControlFlow i32 (Prims.unit & i32)) i32) + with + | Core.Ops.Control_flow.ControlFlow_Break ret -> ret + | Core.Ops.Control_flow.ControlFlow_Continue sum -> sum *! 2l + let double_sum2_return (v: t_Slice i32) : i32 = let sum:i32 = 0l in let sum2:i32 = 0l in @@ -192,35 +148,79 @@ let double_sum2_return (v: t_Slice i32) : i32 = | Core.Ops.Control_flow.ControlFlow_Break ret -> ret | Core.Ops.Control_flow.ControlFlow_Continue (sum, sum2) -> sum +! sum2 -let double_sum_return (v: t_Slice i32) : i32 = - let sum:i32 = 0l in +let bigger_power_2_ (x: i32) : i32 = + let pow:i32 = 1l in + Rust_primitives.f_while_loop_cf (fun pow -> + let pow:i32 = pow in + pow <. 1000000l <: bool) + pow + (fun pow -> + let pow:i32 = pow in + let pow:i32 = pow *! 2l in + if pow <. x + then + let pow:i32 = pow *! 3l in + if true + then + Core.Ops.Control_flow.ControlFlow_Break ((), pow <: (Prims.unit & i32)) + <: + Core.Ops.Control_flow.t_ControlFlow (Prims.unit & i32) i32 + else + Core.Ops.Control_flow.ControlFlow_Continue (pow *! 2l) + <: + Core.Ops.Control_flow.t_ControlFlow (Prims.unit & i32) i32 + else + Core.Ops.Control_flow.ControlFlow_Continue (pow *! 2l) + <: + Core.Ops.Control_flow.t_ControlFlow (Prims.unit & i32) i32) + +type t_M = { f_m:Alloc.Vec.t_Vec u8 Alloc.Alloc.t_Global } + +let impl__M__decoded_message (self: t_M) + : Core.Option.t_Option (Alloc.Vec.t_Vec u8 Alloc.Alloc.t_Global) = match - Rust_primitives.Hax.f_fold_return (Core.Iter.Traits.Collect.f_into_iter #(t_Slice i32) - #FStar.Tactics.Typeclasses.solve - v - <: - Core.Slice.Iter.t_Iter i32) - sum - (fun sum i -> - let sum:i32 = sum in - let i:i32 = i in - if i <. 0l <: bool + Rust_primitives.Hax.Folds.fold_range_return (sz 0) + (Alloc.Vec.impl_1__len #u8 #Alloc.Alloc.t_Global self.f_m <: usize) + (fun temp_0_ temp_1_ -> + let _:Prims.unit = temp_0_ in + let _:usize = temp_1_ in + true) + () + (fun temp_0_ i -> + let _:Prims.unit = temp_0_ in + let i:usize = i in + if i >. sz 5 <: bool then Core.Ops.Control_flow.ControlFlow_Break - (Core.Ops.Control_flow.ControlFlow_Break 0l + (Core.Ops.Control_flow.ControlFlow_Break + (Core.Option.Option_None + <: + Core.Option.t_Option (Alloc.Vec.t_Vec u8 Alloc.Alloc.t_Global)) <: - Core.Ops.Control_flow.t_ControlFlow i32 (Prims.unit & i32)) + Core.Ops.Control_flow.t_ControlFlow + (Core.Option.t_Option (Alloc.Vec.t_Vec u8 Alloc.Alloc.t_Global)) + (Prims.unit & Prims.unit)) <: Core.Ops.Control_flow.t_ControlFlow - (Core.Ops.Control_flow.t_ControlFlow i32 (Prims.unit & i32)) i32 + (Core.Ops.Control_flow.t_ControlFlow + (Core.Option.t_Option (Alloc.Vec.t_Vec u8 Alloc.Alloc.t_Global)) + (Prims.unit & Prims.unit)) Prims.unit else - Core.Ops.Control_flow.ControlFlow_Continue (sum +! i <: i32) + Core.Ops.Control_flow.ControlFlow_Continue () <: Core.Ops.Control_flow.t_ControlFlow - (Core.Ops.Control_flow.t_ControlFlow i32 (Prims.unit & i32)) i32) + (Core.Ops.Control_flow.t_ControlFlow + (Core.Option.t_Option (Alloc.Vec.t_Vec u8 Alloc.Alloc.t_Global)) + (Prims.unit & Prims.unit)) Prims.unit) with | Core.Ops.Control_flow.ControlFlow_Break ret -> ret - | Core.Ops.Control_flow.ControlFlow_Continue sum -> sum *! 2l + | Core.Ops.Control_flow.ControlFlow_Continue _ -> + Core.Option.Option_Some + (Core.Clone.f_clone #(Alloc.Vec.t_Vec u8 Alloc.Alloc.t_Global) + #FStar.Tactics.Typeclasses.solve + self.f_m) + <: + Core.Option.t_Option (Alloc.Vec.t_Vec u8 Alloc.Alloc.t_Global) let nested (_: Prims.unit) : i32 = let sum:i32 = 0l in @@ -324,7 +324,94 @@ module Loops.For_loops open Core open FStar.Mul -let bool_returning (x: u8) : bool = x <. 10uy +let range1 (_: Prims.unit) : usize = + let acc:usize = sz 0 in + let acc:usize = + Rust_primitives.Hax.Folds.fold_range (sz 0) + (sz 15) + (fun acc temp_1_ -> + let acc:usize = acc in + let _:usize = temp_1_ in + true) + acc + (fun acc i -> + let acc:usize = acc in + let i:usize = i in + acc +! i <: usize) + in + acc + +let range2 (n: usize) : usize = + let acc:usize = sz 0 in + let acc:usize = + Rust_primitives.Hax.Folds.fold_range (sz 0) + (n +! sz 10 <: usize) + (fun acc temp_1_ -> + let acc:usize = acc in + let _:usize = temp_1_ in + true) + acc + (fun acc i -> + let acc:usize = acc in + let i:usize = i in + (acc +! i <: usize) +! sz 1 <: usize) + in + acc + +let composed_range (n: usize) : usize = + let acc:usize = sz 0 in + let acc:usize = + Core.Iter.Traits.Iterator.f_fold (Core.Iter.Traits.Collect.f_into_iter #(Core.Iter.Adapters.Chain.t_Chain + (Core.Ops.Range.t_Range usize) (Core.Ops.Range.t_Range usize)) + #FStar.Tactics.Typeclasses.solve + (Core.Iter.Traits.Iterator.f_chain #(Core.Ops.Range.t_Range usize) + #FStar.Tactics.Typeclasses.solve + #(Core.Ops.Range.t_Range usize) + ({ Core.Ops.Range.f_start = sz 0; Core.Ops.Range.f_end = n } + <: + Core.Ops.Range.t_Range usize) + ({ + Core.Ops.Range.f_start = n +! sz 10 <: usize; + Core.Ops.Range.f_end = n +! sz 50 <: usize + } + <: + Core.Ops.Range.t_Range usize) + <: + Core.Iter.Adapters.Chain.t_Chain (Core.Ops.Range.t_Range usize) + (Core.Ops.Range.t_Range usize)) + <: + Core.Iter.Adapters.Chain.t_Chain (Core.Ops.Range.t_Range usize) + (Core.Ops.Range.t_Range usize)) + acc + (fun acc i -> + let acc:usize = acc in + let i:usize = i in + (acc +! i <: usize) +! sz 1 <: usize) + in + acc + +let rev_range (n: usize) : usize = + let acc:usize = sz 0 in + let acc:usize = + Core.Iter.Traits.Iterator.f_fold (Core.Iter.Traits.Collect.f_into_iter #(Core.Iter.Adapters.Rev.t_Rev + (Core.Ops.Range.t_Range usize)) + #FStar.Tactics.Typeclasses.solve + (Core.Iter.Traits.Iterator.f_rev #(Core.Ops.Range.t_Range usize) + #FStar.Tactics.Typeclasses.solve + ({ Core.Ops.Range.f_start = sz 0; Core.Ops.Range.f_end = n } + <: + Core.Ops.Range.t_Range usize) + <: + Core.Iter.Adapters.Rev.t_Rev (Core.Ops.Range.t_Range usize)) + <: + Core.Iter.Adapters.Rev.t_Rev (Core.Ops.Range.t_Range usize)) + acc + (fun acc i -> + let acc:usize = acc in + let i:usize = i in + (acc +! i <: usize) +! sz 1 <: usize) + in + acc let chunks (v_CHUNK_LEN: usize) (arr: Alloc.Vec.t_Vec usize Alloc.Alloc.t_Global) : usize = let acc:usize = sz 0 in @@ -382,94 +469,6 @@ let chunks (v_CHUNK_LEN: usize) (arr: Alloc.Vec.t_Vec usize Alloc.Alloc.t_Global in acc -let composed_range (n: usize) : usize = - let acc:usize = sz 0 in - let acc:usize = - Core.Iter.Traits.Iterator.f_fold (Core.Iter.Traits.Collect.f_into_iter #(Core.Iter.Adapters.Chain.t_Chain - (Core.Ops.Range.t_Range usize) (Core.Ops.Range.t_Range usize)) - #FStar.Tactics.Typeclasses.solve - (Core.Iter.Traits.Iterator.f_chain #(Core.Ops.Range.t_Range usize) - #FStar.Tactics.Typeclasses.solve - #(Core.Ops.Range.t_Range usize) - ({ Core.Ops.Range.f_start = sz 0; Core.Ops.Range.f_end = n } - <: - Core.Ops.Range.t_Range usize) - ({ - Core.Ops.Range.f_start = n +! sz 10 <: usize; - Core.Ops.Range.f_end = n +! sz 50 <: usize - } - <: - Core.Ops.Range.t_Range usize) - <: - Core.Iter.Adapters.Chain.t_Chain (Core.Ops.Range.t_Range usize) - (Core.Ops.Range.t_Range usize)) - <: - Core.Iter.Adapters.Chain.t_Chain (Core.Ops.Range.t_Range usize) - (Core.Ops.Range.t_Range usize)) - acc - (fun acc i -> - let acc:usize = acc in - let i:usize = i in - (acc +! i <: usize) +! sz 1 <: usize) - in - acc - -let enumerate_chunks (arr: Alloc.Vec.t_Vec usize Alloc.Alloc.t_Global) : usize = - let acc:usize = sz 0 in - let acc:usize = - Core.Iter.Traits.Iterator.f_fold (Core.Iter.Traits.Collect.f_into_iter #(Core.Iter.Adapters.Enumerate.t_Enumerate - (Core.Slice.Iter.t_Chunks usize)) - #FStar.Tactics.Typeclasses.solve - (Core.Iter.Traits.Iterator.f_enumerate #(Core.Slice.Iter.t_Chunks usize) - #FStar.Tactics.Typeclasses.solve - (Core.Slice.impl__chunks #usize - (Core.Ops.Deref.f_deref #(Alloc.Vec.t_Vec usize Alloc.Alloc.t_Global) - #FStar.Tactics.Typeclasses.solve - arr - <: - t_Slice usize) - (sz 4) - <: - Core.Slice.Iter.t_Chunks usize) - <: - Core.Iter.Adapters.Enumerate.t_Enumerate (Core.Slice.Iter.t_Chunks usize)) - <: - Core.Iter.Adapters.Enumerate.t_Enumerate (Core.Slice.Iter.t_Chunks usize)) - acc - (fun acc temp_1_ -> - let acc:usize = acc in - let i, chunk:(usize & t_Slice usize) = temp_1_ in - Rust_primitives.Hax.Folds.fold_enumerated_slice chunk - (fun acc temp_1_ -> - let acc:usize = acc in - let _:usize = temp_1_ in - true) - acc - (fun acc temp_1_ -> - let acc:usize = acc in - let j, x:(usize & usize) = temp_1_ in - (i +! j <: usize) +! x <: usize) - <: - usize) - in - acc - -let f (_: Prims.unit) : u8 = - let acc:u8 = 0uy in - Rust_primitives.Hax.Folds.fold_range 1uy - 10uy - (fun acc temp_1_ -> - let acc:u8 = acc in - let _:u8 = temp_1_ in - true) - acc - (fun acc i -> - let acc:u8 = acc in - let i:u8 = i in - let acc:u8 = acc +! i in - let _:bool = bool_returning i in - acc) - let iterator (arr: Alloc.Vec.t_Vec usize Alloc.Alloc.t_Global) : usize = let acc:usize = sz 0 in let acc:usize = @@ -581,62 +580,63 @@ let pattern (arr: Alloc.Vec.t_Vec (usize & usize) Alloc.Alloc.t_Global) : usize in acc -let range1 (_: Prims.unit) : usize = - let acc:usize = sz 0 in - let acc:usize = - Rust_primitives.Hax.Folds.fold_range (sz 0) - (sz 15) - (fun acc temp_1_ -> - let acc:usize = acc in - let _:usize = temp_1_ in - true) - acc - (fun acc i -> - let acc:usize = acc in - let i:usize = i in - acc +! i <: usize) - in - acc - -let range2 (n: usize) : usize = - let acc:usize = sz 0 in - let acc:usize = - Rust_primitives.Hax.Folds.fold_range (sz 0) - (n +! sz 10 <: usize) - (fun acc temp_1_ -> - let acc:usize = acc in - let _:usize = temp_1_ in - true) - acc - (fun acc i -> - let acc:usize = acc in - let i:usize = i in - (acc +! i <: usize) +! sz 1 <: usize) - in - acc - -let rev_range (n: usize) : usize = +let enumerate_chunks (arr: Alloc.Vec.t_Vec usize Alloc.Alloc.t_Global) : usize = let acc:usize = sz 0 in let acc:usize = - Core.Iter.Traits.Iterator.f_fold (Core.Iter.Traits.Collect.f_into_iter #(Core.Iter.Adapters.Rev.t_Rev - (Core.Ops.Range.t_Range usize)) + Core.Iter.Traits.Iterator.f_fold (Core.Iter.Traits.Collect.f_into_iter #(Core.Iter.Adapters.Enumerate.t_Enumerate + (Core.Slice.Iter.t_Chunks usize)) #FStar.Tactics.Typeclasses.solve - (Core.Iter.Traits.Iterator.f_rev #(Core.Ops.Range.t_Range usize) + (Core.Iter.Traits.Iterator.f_enumerate #(Core.Slice.Iter.t_Chunks usize) #FStar.Tactics.Typeclasses.solve - ({ Core.Ops.Range.f_start = sz 0; Core.Ops.Range.f_end = n } + (Core.Slice.impl__chunks #usize + (Core.Ops.Deref.f_deref #(Alloc.Vec.t_Vec usize Alloc.Alloc.t_Global) + #FStar.Tactics.Typeclasses.solve + arr + <: + t_Slice usize) + (sz 4) <: - Core.Ops.Range.t_Range usize) + Core.Slice.Iter.t_Chunks usize) <: - Core.Iter.Adapters.Rev.t_Rev (Core.Ops.Range.t_Range usize)) + Core.Iter.Adapters.Enumerate.t_Enumerate (Core.Slice.Iter.t_Chunks usize)) <: - Core.Iter.Adapters.Rev.t_Rev (Core.Ops.Range.t_Range usize)) + Core.Iter.Adapters.Enumerate.t_Enumerate (Core.Slice.Iter.t_Chunks usize)) acc - (fun acc i -> + (fun acc temp_1_ -> let acc:usize = acc in - let i:usize = i in - (acc +! i <: usize) +! sz 1 <: usize) + let i, chunk:(usize & t_Slice usize) = temp_1_ in + Rust_primitives.Hax.Folds.fold_enumerated_slice chunk + (fun acc temp_1_ -> + let acc:usize = acc in + let _:usize = temp_1_ in + true) + acc + (fun acc temp_1_ -> + let acc:usize = acc in + let j, x:(usize & usize) = temp_1_ in + (i +! j <: usize) +! x <: usize) + <: + usize) in acc + +let bool_returning (x: u8) : bool = x <. 10uy + +let f (_: Prims.unit) : u8 = + let acc:u8 = 0uy in + Rust_primitives.Hax.Folds.fold_range 1uy + 10uy + (fun acc temp_1_ -> + let acc:u8 = acc in + let _:u8 = temp_1_ in + true) + acc + (fun acc i -> + let acc:u8 = acc in + let i:u8 = i in + let acc:u8 = acc +! i in + let _:bool = bool_returning i in + acc) ''' "Loops.Recognized_loops.fst" = ''' module Loops.Recognized_loops @@ -644,64 +644,64 @@ module Loops.Recognized_loops open Core open FStar.Mul -let enumerated_chunked_slice (#v_T: Type0) (slice: t_Slice v_T) : u64 = +let range (_: Prims.unit) : u64 = let count:u64 = 0uL in - Rust_primitives.Hax.Folds.fold_enumerated_chunked_slice (sz 3) - slice + Rust_primitives.Hax.Folds.fold_range 0uy + 10uy (fun count i -> let count:u64 = count in - let i:usize = i in - i <= Core.Slice.impl__len #v_T slice) + let i:u8 = i in + i <=. 10uy <: bool) count (fun count i -> let count:u64 = count in - let i:(usize & t_Slice v_T) = i in - let count:u64 = count +! 3uL in + let i:u8 = i in + let count:u64 = count +! 1uL in count) -let enumerated_slice (#v_T: Type0) (slice: t_Slice v_T) : u64 = +let range_step_by (_: Prims.unit) : u64 = let count:u64 = 0uL in - Rust_primitives.Hax.Folds.fold_enumerated_slice slice + Rust_primitives.Hax.Folds.fold_range_step_by 0uy + 10uy + (sz 2) (fun count i -> let count:u64 = count in - let i:usize = i in - i <=. sz 10 <: bool) + let i:u8 = i in + i <=. 10uy <: bool) count (fun count i -> let count:u64 = count in - let i:(usize & v_T) = i in - let count:u64 = count +! 2uL in + let i:u8 = i in + let count:u64 = count +! 1uL in count) -let range (_: Prims.unit) : u64 = +let enumerated_slice (#v_T: Type0) (slice: t_Slice v_T) : u64 = let count:u64 = 0uL in - Rust_primitives.Hax.Folds.fold_range 0uy - 10uy + Rust_primitives.Hax.Folds.fold_enumerated_slice slice (fun count i -> let count:u64 = count in - let i:u8 = i in - i <=. 10uy <: bool) + let i:usize = i in + i <=. sz 10 <: bool) count (fun count i -> let count:u64 = count in - let i:u8 = i in - let count:u64 = count +! 1uL in + let i:(usize & v_T) = i in + let count:u64 = count +! 2uL in count) -let range_step_by (_: Prims.unit) : u64 = +let enumerated_chunked_slice (#v_T: Type0) (slice: t_Slice v_T) : u64 = let count:u64 = 0uL in - Rust_primitives.Hax.Folds.fold_range_step_by 0uy - 10uy - (sz 2) + Rust_primitives.Hax.Folds.fold_enumerated_chunked_slice (sz 3) + slice (fun count i -> let count:u64 = count in - let i:u8 = i in - i <=. 10uy <: bool) + let i:usize = i in + i <= Core.Slice.impl__len #v_T slice) count (fun count i -> let count:u64 = count in - let i:u8 = i in - let count:u64 = count +! 1uL in + let i:(usize & t_Slice v_T) = i in + let count:u64 = count +! 3uL in count) ''' "Loops.While_loops.fst" = ''' 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 index fee5eaadb..f1ffe9f82 100644 --- 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,102 +32,8 @@ module Mut_ref_functionalization open Core open FStar.Mul -type t_Bar = { - f_a:u8; - f_b:u8 -} - -type t_Foo = { f_field:Alloc.Vec.t_Vec u8 Alloc.Alloc.t_Global } - -class t_FooTrait (v_Self: Type0) = { - f_z_pre:v_Self -> Type0; - f_z_post:v_Self -> v_Self -> Type0; - f_z:x0: v_Self -> Prims.Pure v_Self (f_z_pre x0) (fun result -> f_z_post x0 result) -} - -[@@ FStar.Tactics.Typeclasses.tcinstance] -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); - f_z = fun (self: t_Foo) -> self - } - -type t_Pair (v_T: Type0) = { - f_a:v_T; - f_b:t_Foo -} - type t_S = { f_b:t_Array u8 (sz 5) } -let impl__S__update (self: t_S) (x: u8) : t_S = - let self:t_S = - { - self with - f_b = Rust_primitives.Hax.Monomorphized_update_at.update_at_usize self.f_b (sz 0) x - } - <: - t_S - in - self - -let array (x: t_Array u8 (sz 10)) : t_Array u8 (sz 10) = - let x:t_Array u8 (sz 10) = - Rust_primitives.Hax.Monomorphized_update_at.update_at_usize x (sz 1) (x.[ sz 2 ] <: u8) - in - x - -let f (_: Prims.unit) : Alloc.Vec.t_Vec u8 Alloc.Alloc.t_Global = - let vec:Alloc.Vec.t_Vec u8 Alloc.Alloc.t_Global = Alloc.Vec.impl__new #u8 () in - let vec:Alloc.Vec.t_Vec u8 Alloc.Alloc.t_Global = - Alloc.Vec.impl_1__push #u8 #Alloc.Alloc.t_Global vec 1uy - in - let vec:Alloc.Vec.t_Vec u8 Alloc.Alloc.t_Global = - Alloc.Vec.impl_1__push #u8 #Alloc.Alloc.t_Global vec 2uy - in - let vec:Alloc.Vec.t_Vec u8 Alloc.Alloc.t_Global = Core.Slice.impl__swap #u8 vec (sz 0) (sz 1) in - let vec:Alloc.Vec.t_Vec u8 Alloc.Alloc.t_Global = Core.Slice.impl__swap #u8 vec (sz 0) (sz 1) in - vec - -let h (x: u8) : u8 = - let x:u8 = x +! 10uy in - x - -let i (bar: t_Bar) : (t_Bar & u8) = - let bar:t_Bar = { bar with f_b = bar.f_b +! bar.f_a } <: t_Bar in - let bar:t_Bar = { bar with f_a = h bar.f_a } <: t_Bar in - let hax_temp_output:u8 = bar.f_a +! bar.f_b in - bar, hax_temp_output <: (t_Bar & u8) - -let j (x: t_Bar) : (t_Bar & u8) = - let out:u8 = 123uy in - let tmp0, out1:(t_Bar & u8) = i x in - let x:t_Bar = tmp0 in - let hax_temp_output:u8 = out1 +! out in - x, hax_temp_output <: (t_Bar & u8) - -let k - (vec: Alloc.Vec.t_Vec u8 Alloc.Alloc.t_Global) - (arg_1_wild3: u16) - (arg_1_wild: u8) - (arg_3_wild2: Prims.unit) - : (Alloc.Vec.t_Vec u8 Alloc.Alloc.t_Global & u16 & Prims.unit & u64) = - let arg_1_wild2:u8 = vec.[ sz 1 ] in - let arg_3_wild:u8 = vec.[ sz 2 ] in - let arg_1_wild1:u8 = vec.[ sz 3 ] in - let arg_3_wild1:u8 = vec.[ sz 4 ] in - let vec:Alloc.Vec.t_Vec u8 Alloc.Alloc.t_Global = - Rust_primitives.Hax.Monomorphized_update_at.update_at_usize vec - (sz 0) - ((((arg_1_wild +! arg_3_wild <: u8) +! arg_1_wild1 <: u8) +! arg_3_wild1 <: u8) +! arg_1_wild - <: - u8) - in - let hax_temp_output:u64 = 12345uL in - vec, arg_1_wild3, arg_3_wild2, hax_temp_output - <: - (Alloc.Vec.t_Vec u8 Alloc.Alloc.t_Global & u16 & Prims.unit & u64) - let foo (lhs rhs: t_S) : t_S = let lhs:t_S = Rust_primitives.Hax.Folds.fold_range (sz 0) @@ -155,56 +61,16 @@ let foo (lhs rhs: t_S) : t_S = in lhs -let g (x: t_Pair (Alloc.Vec.t_Vec u8 Alloc.Alloc.t_Global)) - : Alloc.Vec.t_Vec u8 Alloc.Alloc.t_Global = - let x:t_Pair (Alloc.Vec.t_Vec u8 Alloc.Alloc.t_Global) = x in - let x:t_Pair (Alloc.Vec.t_Vec u8 Alloc.Alloc.t_Global) = - Rust_primitives.Hax.Folds.fold_range 1uy - 10uy - (fun x temp_1_ -> - let x:t_Pair (Alloc.Vec.t_Vec u8 Alloc.Alloc.t_Global) = x in - let _:u8 = temp_1_ in - true) - x - (fun x i -> - let x:t_Pair (Alloc.Vec.t_Vec u8 Alloc.Alloc.t_Global) = x in - let i:u8 = i in - { - x with - f_a - = - Alloc.Vec.impl_1__push #u8 #Alloc.Alloc.t_Global x.f_a i - <: - Alloc.Vec.t_Vec u8 Alloc.Alloc.t_Global - } - <: - t_Pair (Alloc.Vec.t_Vec u8 Alloc.Alloc.t_Global)) - in - let x:t_Pair (Alloc.Vec.t_Vec u8 Alloc.Alloc.t_Global) = - { x with f_a = Core.Slice.impl__swap #u8 x.f_a (sz 0) (sz 1) } - <: - t_Pair (Alloc.Vec.t_Vec u8 Alloc.Alloc.t_Global) - in - let x:t_Pair (Alloc.Vec.t_Vec u8 Alloc.Alloc.t_Global) = +let impl__S__update (self: t_S) (x: u8) : t_S = + let self:t_S = { - x with - f_b = { x.f_b with f_field = Core.Slice.impl__swap #u8 x.f_b.f_field (sz 0) (sz 1) } <: t_Foo + self with + f_b = Rust_primitives.Hax.Monomorphized_update_at.update_at_usize self.f_b (sz 0) x } <: - t_Pair (Alloc.Vec.t_Vec u8 Alloc.Alloc.t_Global) + t_S in - x.f_a - -let build_vec (_: Prims.unit) : Alloc.Vec.t_Vec u8 Alloc.Alloc.t_Global = - Alloc.Slice.impl__into_vec #u8 - #Alloc.Alloc.t_Global - (Rust_primitives.unsize (Rust_primitives.Hax.box_new (let list = [1uy; 2uy; 3uy] in - FStar.Pervasives.assert_norm (Prims.eq2 (List.Tot.length list) 3); - Rust_primitives.Hax.array_of_list 3 list) - <: - Alloc.Boxed.t_Box (t_Array u8 (sz 3)) Alloc.Alloc.t_Global) - <: - Alloc.Boxed.t_Box (t_Slice u8) Alloc.Alloc.t_Global) + self let index_mutation (x: Core.Ops.Range.t_Range usize) (a: t_Slice u8) : Prims.unit = let v:Alloc.Vec.t_Vec u8 Alloc.Alloc.t_Global = @@ -250,6 +116,17 @@ let index_mutation_unsize (x: t_Array u8 (sz 12)) : u8 = in 42uy +let build_vec (_: Prims.unit) : Alloc.Vec.t_Vec u8 Alloc.Alloc.t_Global = + Alloc.Slice.impl__into_vec #u8 + #Alloc.Alloc.t_Global + (Rust_primitives.unsize (Rust_primitives.Hax.box_new (let list = [1uy; 2uy; 3uy] in + FStar.Pervasives.assert_norm (Prims.eq2 (List.Tot.length list) 3); + Rust_primitives.Hax.array_of_list 3 list) + <: + Alloc.Boxed.t_Box (t_Array u8 (sz 3)) Alloc.Alloc.t_Global) + <: + Alloc.Boxed.t_Box (t_Slice u8) Alloc.Alloc.t_Global) + let test_append (_: Prims.unit) : Alloc.Vec.t_Vec u8 Alloc.Alloc.t_Global = let vec1:Alloc.Vec.t_Vec u8 Alloc.Alloc.t_Global = Alloc.Vec.impl__new #u8 () in let vec2:Alloc.Vec.t_Vec u8 Alloc.Alloc.t_Global = @@ -277,4 +154,127 @@ let test_append (_: Prims.unit) : Alloc.Vec.t_Vec u8 Alloc.Alloc.t_Global = (build_vec () <: Alloc.Vec.t_Vec u8 Alloc.Alloc.t_Global) in vec1 + +let f (_: Prims.unit) : Alloc.Vec.t_Vec u8 Alloc.Alloc.t_Global = + let vec:Alloc.Vec.t_Vec u8 Alloc.Alloc.t_Global = Alloc.Vec.impl__new #u8 () in + let vec:Alloc.Vec.t_Vec u8 Alloc.Alloc.t_Global = + Alloc.Vec.impl_1__push #u8 #Alloc.Alloc.t_Global vec 1uy + in + let vec:Alloc.Vec.t_Vec u8 Alloc.Alloc.t_Global = + Alloc.Vec.impl_1__push #u8 #Alloc.Alloc.t_Global vec 2uy + in + let vec:Alloc.Vec.t_Vec u8 Alloc.Alloc.t_Global = Core.Slice.impl__swap #u8 vec (sz 0) (sz 1) in + let vec:Alloc.Vec.t_Vec u8 Alloc.Alloc.t_Global = Core.Slice.impl__swap #u8 vec (sz 0) (sz 1) in + vec + +type t_Foo = { f_field:Alloc.Vec.t_Vec u8 Alloc.Alloc.t_Global } + +type t_Pair (v_T: Type0) = { + f_a:v_T; + f_b:t_Foo +} + +let g (x: t_Pair (Alloc.Vec.t_Vec u8 Alloc.Alloc.t_Global)) + : Alloc.Vec.t_Vec u8 Alloc.Alloc.t_Global = + let x:t_Pair (Alloc.Vec.t_Vec u8 Alloc.Alloc.t_Global) = x in + let x:t_Pair (Alloc.Vec.t_Vec u8 Alloc.Alloc.t_Global) = + Rust_primitives.Hax.Folds.fold_range 1uy + 10uy + (fun x temp_1_ -> + let x:t_Pair (Alloc.Vec.t_Vec u8 Alloc.Alloc.t_Global) = x in + let _:u8 = temp_1_ in + true) + x + (fun x i -> + let x:t_Pair (Alloc.Vec.t_Vec u8 Alloc.Alloc.t_Global) = x in + let i:u8 = i in + { + x with + f_a + = + Alloc.Vec.impl_1__push #u8 #Alloc.Alloc.t_Global x.f_a i + <: + Alloc.Vec.t_Vec u8 Alloc.Alloc.t_Global + } + <: + t_Pair (Alloc.Vec.t_Vec u8 Alloc.Alloc.t_Global)) + in + let x:t_Pair (Alloc.Vec.t_Vec u8 Alloc.Alloc.t_Global) = + { x with f_a = Core.Slice.impl__swap #u8 x.f_a (sz 0) (sz 1) } + <: + t_Pair (Alloc.Vec.t_Vec u8 Alloc.Alloc.t_Global) + in + let x:t_Pair (Alloc.Vec.t_Vec u8 Alloc.Alloc.t_Global) = + { + x with + f_b = { x.f_b with f_field = Core.Slice.impl__swap #u8 x.f_b.f_field (sz 0) (sz 1) } <: t_Foo + } + <: + t_Pair (Alloc.Vec.t_Vec u8 Alloc.Alloc.t_Global) + in + x.f_a + +let h (x: u8) : u8 = + let x:u8 = x +! 10uy in + x + +type t_Bar = { + f_a:u8; + f_b:u8 +} + +let i (bar: t_Bar) : (t_Bar & u8) = + let bar:t_Bar = { bar with f_b = bar.f_b +! bar.f_a } <: t_Bar in + let bar:t_Bar = { bar with f_a = h bar.f_a } <: t_Bar in + let hax_temp_output:u8 = bar.f_a +! bar.f_b in + bar, hax_temp_output <: (t_Bar & u8) + +let j (x: t_Bar) : (t_Bar & u8) = + let out:u8 = 123uy in + let tmp0, out1:(t_Bar & u8) = i x in + let x:t_Bar = tmp0 in + let hax_temp_output:u8 = out1 +! out in + x, hax_temp_output <: (t_Bar & u8) + +let k + (vec: Alloc.Vec.t_Vec u8 Alloc.Alloc.t_Global) + (arg_1_wild3: u16) + (arg_1_wild: u8) + (arg_3_wild2: Prims.unit) + : (Alloc.Vec.t_Vec u8 Alloc.Alloc.t_Global & u16 & Prims.unit & u64) = + let arg_1_wild2:u8 = vec.[ sz 1 ] in + let arg_3_wild:u8 = vec.[ sz 2 ] in + let arg_1_wild1:u8 = vec.[ sz 3 ] in + let arg_3_wild1:u8 = vec.[ sz 4 ] in + let vec:Alloc.Vec.t_Vec u8 Alloc.Alloc.t_Global = + Rust_primitives.Hax.Monomorphized_update_at.update_at_usize vec + (sz 0) + ((((arg_1_wild +! arg_3_wild <: u8) +! arg_1_wild1 <: u8) +! arg_3_wild1 <: u8) +! arg_1_wild + <: + u8) + in + let hax_temp_output:u64 = 12345uL in + vec, arg_1_wild3, arg_3_wild2, hax_temp_output + <: + (Alloc.Vec.t_Vec u8 Alloc.Alloc.t_Global & u16 & Prims.unit & u64) + +class t_FooTrait (v_Self: Type0) = { + f_z_pre:v_Self -> Type0; + f_z_post:v_Self -> v_Self -> Type0; + f_z:x0: v_Self -> Prims.Pure v_Self (f_z_pre x0) (fun result -> f_z_post x0 result) +} + +[@@ FStar.Tactics.Typeclasses.tcinstance] +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); + f_z = fun (self: t_Foo) -> self + } + +let array (x: t_Array u8 (sz 10)) : t_Array u8 (sz 10) = + let x:t_Array u8 (sz 10) = + Rust_primitives.Hax.Monomorphized_update_at.update_at_usize x (sz 1) (x.[ sz 2 ] <: u8) + in + x ''' diff --git a/test-harness/src/snapshots/toolchain__naming into-fstar.snap b/test-harness/src/snapshots/toolchain__naming into-fstar.snap index f25ae1575..903e5db34 100644 --- a/test-harness/src/snapshots/toolchain__naming into-fstar.snap +++ b/test-harness/src/snapshots/toolchain__naming into-fstar.snap @@ -94,41 +94,46 @@ module Naming open Core open FStar.Mul -type t_Arity1 (v_T: Type0) = | Arity1 : v_T -> t_Arity1 v_T - -type t_B = | B : t_B - -let impl__B__f (self: t_B) : t_B = B <: t_B - -type t_C = { f_x:usize } - type t_Foo = | Foo_A : t_Foo | Foo_B { f_x:usize }: t_Foo -let impl__Foo__f (self: t_Foo) : t_Foo = Foo_A <: t_Foo - type t_Foo2 = | Foo2_A : t_Foo2 | Foo2_B { f_x:usize }: t_Foo2 -class t_FooTrait (v_Self: Type0) = { f_ASSOCIATED_CONSTANT:usize } +type t_B = | B : t_B + +type t_C = { f_x:usize } + +type t_X = | X : t_X + +let mk_c (_: Prims.unit) : t_C = + let _:t_Foo = Foo_B ({ Naming.Foo.f_x = sz 3 }) <: t_Foo in + let _:t_X = X <: t_X in + { f_x = sz 3 } <: t_C + +let impl__Foo__f (self: t_Foo) : t_Foo = Foo_A <: t_Foo + +let impl__B__f (self: t_B) : t_B = B <: t_B type t_Foobar = { f_a:t_Foo } -type t_StructA = { f_a:usize } +let ff__g (_: Prims.unit) : Prims.unit = () -type t_StructB = { - f_a:usize; - f_b:usize -} +let ff__g__impl__g (self: t_B) : usize = sz 0 -type t_StructC = { f_a:usize } +type t_f__g__impl__g__Foo = + | C_f__g__impl__g__Foo_A : t_f__g__impl__g__Foo + | C_f__g__impl__g__Foo_B { f_x:usize }: t_f__g__impl__g__Foo -type t_StructD = { - f_a:usize; - f_b:usize -} +let ff__g__impl_1__g (self: t_Foo) : usize = sz 1 + +let f (x: t_Foobar) : usize = ff__g__impl_1__g x.f_a + +let reserved_names (v_val v_noeq v_of: u8) : u8 = (v_val +! v_noeq <: u8) +! v_of + +type t_Arity1 (v_T: Type0) = | Arity1 : v_T -> t_Arity1 v_T class t_T1 (v_Self: Type0) = { __marker_trait_t_T1:Prims.unit } @@ -149,16 +154,19 @@ 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 = () } -type t_X = | X : t_X +type t_StructA = { f_a:usize } -let v_INHERENT_CONSTANT: usize = sz 3 +type t_StructB = { + f_a:usize; + f_b:usize +} -let constants - (#v_T: Type0) - (#[FStar.Tactics.Typeclasses.tcresolve ()] i1: t_FooTrait v_T) - (_: Prims.unit) - : usize = - (f_ASSOCIATED_CONSTANT #FStar.Tactics.Typeclasses.solve <: usize) +! v_INHERENT_CONSTANT +type t_StructC = { f_a:usize } + +type t_StructD = { + f_a:usize; + f_b:usize +} let construct_structs (a b: usize) : Prims.unit = let _:t_StructA = { f_a = a } <: t_StructA in @@ -167,24 +175,16 @@ let construct_structs (a b: usize) : Prims.unit = let _:t_StructD = { f_a = a; f_b = b } <: t_StructD in () -let ff__g (_: Prims.unit) : Prims.unit = () - -let ff__g__impl__g (self: t_B) : usize = sz 0 - -type t_f__g__impl__g__Foo = - | C_f__g__impl__g__Foo_A : t_f__g__impl__g__Foo - | C_f__g__impl__g__Foo_B { f_x:usize }: t_f__g__impl__g__Foo - -let ff__g__impl_1__g (self: t_Foo) : usize = sz 1 - -let f (x: t_Foobar) : usize = ff__g__impl_1__g x.f_a +let v_INHERENT_CONSTANT: usize = sz 3 -let mk_c (_: Prims.unit) : t_C = - let _:t_Foo = Foo_B ({ Naming.Foo.f_x = sz 3 }) <: t_Foo in - let _:t_X = X <: t_X in - { f_x = sz 3 } <: t_C +class t_FooTrait (v_Self: Type0) = { f_ASSOCIATED_CONSTANT:usize } -let reserved_names (v_val v_noeq v_of: u8) : u8 = (v_val +! v_noeq <: u8) +! v_of +let constants + (#v_T: Type0) + (#[FStar.Tactics.Typeclasses.tcresolve ()] i1: t_FooTrait v_T) + (_: Prims.unit) + : usize = + (f_ASSOCIATED_CONSTANT #FStar.Tactics.Typeclasses.solve <: usize) +! v_INHERENT_CONSTANT /// From issue https://github.com/hacspec/hax/issues/839 let string_shadows (v_string n: string) : Prims.unit = () diff --git a/test-harness/src/snapshots/toolchain__pattern-or into-coq.snap b/test-harness/src/snapshots/toolchain__pattern-or into-coq.snap index f4b3cbfe0..470b72517 100644 --- a/test-harness/src/snapshots/toolchain__pattern-or into-coq.snap +++ b/test-harness/src/snapshots/toolchain__pattern-or into-coq.snap @@ -42,6 +42,8 @@ Import RecordSetNotations. +(* NotImplementedYet *) + Inductive t_E : Type := | E_A | E_B. @@ -56,8 +58,6 @@ Definition t_E_cast_to_repr (x : t_E) : t_isize := 1 end. -(* NotImplementedYet *) - Definition bar (x : t_E) : unit := match x with | E_A @@ -65,6 +65,17 @@ Definition bar (x : t_E) : unit := tt end. +Definition nested (x : t_Option ((t_i32))) : t_i32 := + match x with + | Option_Some (1 + | 2) => + 1 + | Option_Some (x) => + x + | Option_None => + 0 + end. + Definition deep (x : (t_i32*t_Option ((t_i32)))) : t_i32 := match x with | (1 @@ -75,18 +86,6 @@ Definition deep (x : (t_i32*t_Option ((t_i32)))) : t_i32 := x end. -Definition deep_capture (x : t_Result (((t_i32*t_i32))) (((t_i32*t_i32)))) : t_i32 := - match x with - | Result_Ok ((1 - | 2,x)) - | Result_Err ((3 - | 4,x)) => - x - | Result_Ok ((x,_)) - | Result_Err ((x,_)) => - x - end. - Definition equivalent (x : (t_i32*t_Option ((t_i32)))) : t_i32 := match x with | (1,Option_Some (3)) @@ -98,14 +97,15 @@ Definition equivalent (x : (t_i32*t_Option ((t_i32)))) : t_i32 := x end. -Definition nested (x : t_Option ((t_i32))) : t_i32 := +Definition deep_capture (x : t_Result (((t_i32*t_i32))) (((t_i32*t_i32)))) : t_i32 := match x with - | Option_Some (1 - | 2) => - 1 - | Option_Some (x) => + | Result_Ok ((1 + | 2,x)) + | Result_Err ((3 + | 4,x)) => + x + | Result_Ok ((x,_)) + | Result_Err ((x,_)) => x - | Option_None => - 0 end. ''' diff --git a/test-harness/src/snapshots/toolchain__pattern-or into-fstar.snap b/test-harness/src/snapshots/toolchain__pattern-or into-fstar.snap index 9fdc477aa..16d56d8f9 100644 --- a/test-harness/src/snapshots/toolchain__pattern-or into-fstar.snap +++ b/test-harness/src/snapshots/toolchain__pattern-or into-fstar.snap @@ -44,6 +44,12 @@ let t_E_cast_to_repr (x: t_E) : isize = let bar (x: t_E) : Prims.unit = match x with | E_A | E_B -> () <: Prims.unit +let nested (x: Core.Option.t_Option i32) : i32 = + match x with + | Core.Option.Option_Some 1l | Core.Option.Option_Some 2l -> 1l + | Core.Option.Option_Some x -> x + | Core.Option.Option_None -> 0l + let deep (x: (i32 & Core.Option.t_Option i32)) : i32 = match x with | 1l, Core.Option.Option_Some 3l @@ -52,14 +58,6 @@ let deep (x: (i32 & Core.Option.t_Option i32)) : i32 = | 2l, Core.Option.Option_Some 4l -> 0l | x, _ -> x -let deep_capture (x: Core.Result.t_Result (i32 & i32) (i32 & i32)) : i32 = - match x with - | Core.Result.Result_Ok (1l, x) - | Core.Result.Result_Ok (2l, x) - | Core.Result.Result_Err (3l, x) - | Core.Result.Result_Err (4l, x) -> x - | Core.Result.Result_Ok (x, _) | Core.Result.Result_Err (x, _) -> x - let equivalent (x: (i32 & Core.Option.t_Option i32)) : i32 = match x with | 1l, Core.Option.Option_Some 3l @@ -68,9 +66,11 @@ let equivalent (x: (i32 & Core.Option.t_Option i32)) : i32 = | 2l, Core.Option.Option_Some 4l -> 0l | x, _ -> x -let nested (x: Core.Option.t_Option i32) : i32 = +let deep_capture (x: Core.Result.t_Result (i32 & i32) (i32 & i32)) : i32 = match x with - | Core.Option.Option_Some 1l | Core.Option.Option_Some 2l -> 1l - | Core.Option.Option_Some x -> x - | Core.Option.Option_None -> 0l + | Core.Result.Result_Ok (1l, x) + | Core.Result.Result_Ok (2l, x) + | Core.Result.Result_Err (3l, x) + | Core.Result.Result_Err (4l, x) -> x + | Core.Result.Result_Ok (x, _) | Core.Result.Result_Err (x, _) -> x ''' diff --git a/test-harness/src/snapshots/toolchain__reordering into-coq.snap b/test-harness/src/snapshots/toolchain__reordering into-coq.snap index d3b0567d8..4890d697f 100644 --- a/test-harness/src/snapshots/toolchain__reordering into-coq.snap +++ b/test-harness/src/snapshots/toolchain__reordering into-coq.snap @@ -41,12 +41,23 @@ Import RecordSetNotations. +(* NotImplementedYet *) + +Definition no_dependency_1_ (_ : unit) : unit := + tt. + +Definition no_dependency_2_ (_ : unit) : unit := + tt. + Inductive t_Foo : Type := | Foo_A | Foo_B. Arguments t_Foo:clear implicits. Arguments t_Foo. +Definition f (_ : t_u32) : t_Foo := + Foo_A. + Record t_Bar : Type := { 0 : t_Foo; @@ -57,6 +68,9 @@ Arguments Build_t_Bar. #[export] Instance settable_t_Bar : Settable _ := settable! (@Build_t_Bar) <0>. +Definition g (_ : unit) : t_Bar := + Build_t_Bar (f (32)). + Definition t_Foo_cast_to_repr (x : t_Foo) : t_isize := match x with | Foo_A => @@ -66,16 +80,83 @@ Definition t_Foo_cast_to_repr (x : t_Foo) : t_isize := end. (* NotImplementedYet *) +''' +"Reordering_No_alpha_sorting.v" = ''' +(* File automatically generated by Hacspec *) +From Coq Require Import ZArith. +Require Import List. +Import List.ListNotations. +Open Scope Z_scope. +Open Scope bool_scope. +Require Import Ascii. +Require Import String. +Require Import Coq.Floats.Floats. +From RecordUpdate Require Import RecordSet. +Import RecordSetNotations. -Definition f (_ : t_u32) : t_Foo := - Foo_A. +Definition u01 (_ : unit) : unit := + tt. -Definition g (_ : unit) : t_Bar := - Build_t_Bar (f (32)). +Definition r02 (_ : unit) : unit := + tt. -Definition no_dependency_1_ (_ : unit) : unit := +Definition b03 (_ : unit) : unit := tt. -Definition no_dependency_2_ (_ : unit) : unit := +Definition f04 (_ : unit) : unit := + tt. + +Definition h05 (_ : unit) : unit := + tt. + +Definition i06 (_ : unit) : unit := + tt. + +Definition c07 (_ : unit) : unit := + tt. + +Definition k08 (_ : unit) : unit := + tt. + +Definition d09 (_ : unit) : unit := + tt. + +Definition e10 (_ : unit) : unit := + tt. + +Definition g11 (_ : unit) : unit := + tt. + +Definition j12 (_ : unit) : unit := + tt. + +Definition o13 (_ : unit) : unit := + tt. + +Definition a14 (_ : unit) : unit := + tt. + +Definition q15 (_ : unit) : unit := + tt. + +Definition m16 (_ : unit) : unit := + tt. + +Definition l17 (_ : unit) : unit := + tt. + +Definition n18 (_ : unit) : unit := + tt. + +Definition v19 (_ : unit) : unit := + tt. + +Definition s20 (_ : unit) : unit := + tt. + +Definition p21 (_ : unit) : unit := + tt. + +Definition t22 (_ : unit) : unit := tt. ''' diff --git a/test-harness/src/snapshots/toolchain__reordering into-fstar.snap b/test-harness/src/snapshots/toolchain__reordering into-fstar.snap index 385642dd2..dec2f94bb 100644 --- a/test-harness/src/snapshots/toolchain__reordering into-fstar.snap +++ b/test-harness/src/snapshots/toolchain__reordering into-fstar.snap @@ -26,28 +26,78 @@ exit = 0 diagnostics = [] [stdout.files] +"Reordering.No_alpha_sorting.fst" = ''' +module Reordering.No_alpha_sorting +#set-options "--fuel 0 --ifuel 1 --z3rlimit 15" +open Core +open FStar.Mul + +let u01 (_: Prims.unit) : Prims.unit = () + +let r02 (_: Prims.unit) : Prims.unit = () + +let b03 (_: Prims.unit) : Prims.unit = () + +let f04 (_: Prims.unit) : Prims.unit = () + +let h05 (_: Prims.unit) : Prims.unit = () + +let i06 (_: Prims.unit) : Prims.unit = () + +let c07 (_: Prims.unit) : Prims.unit = () + +let k08 (_: Prims.unit) : Prims.unit = () + +let d09 (_: Prims.unit) : Prims.unit = () + +let e10 (_: Prims.unit) : Prims.unit = () + +let g11 (_: Prims.unit) : Prims.unit = () + +let j12 (_: Prims.unit) : Prims.unit = () + +let o13 (_: Prims.unit) : Prims.unit = () + +let a14 (_: Prims.unit) : Prims.unit = () + +let q15 (_: Prims.unit) : Prims.unit = () + +let m16 (_: Prims.unit) : Prims.unit = () + +let l17 (_: Prims.unit) : Prims.unit = () + +let n18 (_: Prims.unit) : Prims.unit = () + +let v19 (_: Prims.unit) : Prims.unit = () + +let s20 (_: Prims.unit) : Prims.unit = () + +let p21 (_: Prims.unit) : Prims.unit = () + +let t22 (_: Prims.unit) : Prims.unit = () +''' "Reordering.fst" = ''' module Reordering #set-options "--fuel 0 --ifuel 1 --z3rlimit 15" open Core open FStar.Mul +let no_dependency_1_ (_: Prims.unit) : Prims.unit = () + +let no_dependency_2_ (_: Prims.unit) : Prims.unit = () + type t_Foo = | Foo_A : t_Foo | Foo_B : t_Foo +let f (_: u32) : t_Foo = Foo_A <: t_Foo + type t_Bar = | Bar : t_Foo -> t_Bar +let g (_: Prims.unit) : t_Bar = Bar (f 32ul) <: t_Bar + let t_Foo_cast_to_repr (x: t_Foo) : isize = match x with | Foo_A -> isz 0 | Foo_B -> isz 1 - -let f (_: u32) : t_Foo = Foo_A <: t_Foo - -let g (_: Prims.unit) : t_Bar = Bar (f 32ul) <: t_Bar - -let no_dependency_1_ (_: Prims.unit) : Prims.unit = () - -let no_dependency_2_ (_: Prims.unit) : Prims.unit = () ''' diff --git a/test-harness/src/snapshots/toolchain__reordering into-ssprove.snap b/test-harness/src/snapshots/toolchain__reordering into-ssprove.snap index b6655f747..884bc8a78 100644 --- a/test-harness/src/snapshots/toolchain__reordering into-ssprove.snap +++ b/test-harness/src/snapshots/toolchain__reordering into-ssprove.snap @@ -53,6 +53,18 @@ Import choice.Choice.Exports. Obligation Tactic := (* try timeout 8 *) solve_ssprove_obligations. +(*Not implemented yet? todo(item)*) + +Equations no_dependency_1_ {L1 : {fset Location}} {I1 : Interface} (_ : both L1 I1 'unit) : both L1 I1 'unit := + no_dependency_1_ _ := + solve_lift (ret_both (tt : 'unit)) : both L1 I1 'unit. +Fail Next Obligation. + +Equations no_dependency_2_ {L1 : {fset Location}} {I1 : Interface} (_ : both L1 I1 'unit) : both L1 I1 'unit := + no_dependency_2_ _ := + solve_lift (ret_both (tt : 'unit)) : both L1 I1 'unit. +Fail Next Obligation. + Definition t_Foo : choice_type := ('unit ∐ 'unit). Notation "'Foo_A_case'" := (inl tt) (at level 100). @@ -66,6 +78,11 @@ Equations Foo_B {L : {fset Location}} {I : Interface} : both L I t_Foo := solve_lift (ret_both (inr (tt : 'unit) : t_Foo)) : both L I t_Foo. Fail Next Obligation. +Equations f {L1 : {fset Location}} {I1 : Interface} (_ : both L1 I1 int32) : both L1 I1 t_Foo := + f _ := + Foo_A : both L1 I1 t_Foo. +Fail Next Obligation. + Definition t_Bar : choice_type := (t_Foo). Equations 0 {L : {fset Location}} {I : Interface} (s : both L I t_Bar) : both L I t_Foo := @@ -80,6 +97,11 @@ Equations Build_t_Bar {L0 : {fset Location}} {I0 : Interface} {0 : both L0 I0 t_ Fail Next Obligation. Notation "'Build_t_Bar' '[' x ']' '(' '0' ':=' y ')'" := (Build_t_Bar (0 := y)). +Equations g {L1 : {fset Location}} {I1 : Interface} (_ : both L1 I1 'unit) : both L1 I1 t_Bar := + g _ := + Bar (solve_lift (f (ret_both (32 : int32)))) : both L1 I1 t_Bar. +Fail Next Obligation. + Equations t_Foo_cast_to_repr {L1 : {fset Location}} {I1 : Interface} (x : both L1 I1 t_Foo) : both L1 I1 uint_size := t_Foo_cast_to_repr x := matchb x with @@ -91,24 +113,141 @@ Equations t_Foo_cast_to_repr {L1 : {fset Location}} {I1 : Interface} (x : both L Fail Next Obligation. (*Not implemented yet? todo(item)*) +''' +"Reordering_No_alpha_sorting.v" = ''' +(* File automatically generated by Hacspec *) +Set Warnings "-notation-overridden,-ambiguous-paths". +From Crypt Require Import choice_type Package Prelude. +Import PackageNotation. +From extructures Require Import ord fset. +From mathcomp Require Import word_ssrZ word. +From Jasmin Require Import word. -Equations f {L1 : {fset Location}} {I1 : Interface} (_ : both L1 I1 int32) : both L1 I1 t_Foo := - f _ := - Foo_A : both L1 I1 t_Foo. +From Coq Require Import ZArith. +From Coq Require Import Strings.String. +Import List.ListNotations. +Open Scope list_scope. +Open Scope Z_scope. +Open Scope bool_scope. + +From Hacspec Require Import ChoiceEquality. +From Hacspec Require Import LocationUtility. +From Hacspec Require Import Hacspec_Lib_Comparable. +From Hacspec Require Import Hacspec_Lib_Pre. +From Hacspec Require Import Hacspec_Lib. + +Open Scope hacspec_scope. +Import choice.Choice.Exports. + +Obligation Tactic := (* try timeout 8 *) solve_ssprove_obligations. + +Equations u01 {L1 : {fset Location}} {I1 : Interface} (_ : both L1 I1 'unit) : both L1 I1 'unit := + u01 _ := + solve_lift (ret_both (tt : 'unit)) : both L1 I1 'unit. Fail Next Obligation. -Equations g {L1 : {fset Location}} {I1 : Interface} (_ : both L1 I1 'unit) : both L1 I1 t_Bar := - g _ := - Bar (solve_lift (f (ret_both (32 : int32)))) : both L1 I1 t_Bar. +Equations r02 {L1 : {fset Location}} {I1 : Interface} (_ : both L1 I1 'unit) : both L1 I1 'unit := + r02 _ := + solve_lift (ret_both (tt : 'unit)) : both L1 I1 'unit. Fail Next Obligation. -Equations no_dependency_1_ {L1 : {fset Location}} {I1 : Interface} (_ : both L1 I1 'unit) : both L1 I1 'unit := - no_dependency_1_ _ := +Equations b03 {L1 : {fset Location}} {I1 : Interface} (_ : both L1 I1 'unit) : both L1 I1 'unit := + b03 _ := solve_lift (ret_both (tt : 'unit)) : both L1 I1 'unit. Fail Next Obligation. -Equations no_dependency_2_ {L1 : {fset Location}} {I1 : Interface} (_ : both L1 I1 'unit) : both L1 I1 'unit := - no_dependency_2_ _ := +Equations f04 {L1 : {fset Location}} {I1 : Interface} (_ : both L1 I1 'unit) : both L1 I1 'unit := + f04 _ := + solve_lift (ret_both (tt : 'unit)) : both L1 I1 'unit. +Fail Next Obligation. + +Equations h05 {L1 : {fset Location}} {I1 : Interface} (_ : both L1 I1 'unit) : both L1 I1 'unit := + h05 _ := + solve_lift (ret_both (tt : 'unit)) : both L1 I1 'unit. +Fail Next Obligation. + +Equations i06 {L1 : {fset Location}} {I1 : Interface} (_ : both L1 I1 'unit) : both L1 I1 'unit := + i06 _ := + solve_lift (ret_both (tt : 'unit)) : both L1 I1 'unit. +Fail Next Obligation. + +Equations c07 {L1 : {fset Location}} {I1 : Interface} (_ : both L1 I1 'unit) : both L1 I1 'unit := + c07 _ := + solve_lift (ret_both (tt : 'unit)) : both L1 I1 'unit. +Fail Next Obligation. + +Equations k08 {L1 : {fset Location}} {I1 : Interface} (_ : both L1 I1 'unit) : both L1 I1 'unit := + k08 _ := + solve_lift (ret_both (tt : 'unit)) : both L1 I1 'unit. +Fail Next Obligation. + +Equations d09 {L1 : {fset Location}} {I1 : Interface} (_ : both L1 I1 'unit) : both L1 I1 'unit := + d09 _ := + solve_lift (ret_both (tt : 'unit)) : both L1 I1 'unit. +Fail Next Obligation. + +Equations e10 {L1 : {fset Location}} {I1 : Interface} (_ : both L1 I1 'unit) : both L1 I1 'unit := + e10 _ := + solve_lift (ret_both (tt : 'unit)) : both L1 I1 'unit. +Fail Next Obligation. + +Equations g11 {L1 : {fset Location}} {I1 : Interface} (_ : both L1 I1 'unit) : both L1 I1 'unit := + g11 _ := + solve_lift (ret_both (tt : 'unit)) : both L1 I1 'unit. +Fail Next Obligation. + +Equations j12 {L1 : {fset Location}} {I1 : Interface} (_ : both L1 I1 'unit) : both L1 I1 'unit := + j12 _ := + solve_lift (ret_both (tt : 'unit)) : both L1 I1 'unit. +Fail Next Obligation. + +Equations o13 {L1 : {fset Location}} {I1 : Interface} (_ : both L1 I1 'unit) : both L1 I1 'unit := + o13 _ := + solve_lift (ret_both (tt : 'unit)) : both L1 I1 'unit. +Fail Next Obligation. + +Equations a14 {L1 : {fset Location}} {I1 : Interface} (_ : both L1 I1 'unit) : both L1 I1 'unit := + a14 _ := + solve_lift (ret_both (tt : 'unit)) : both L1 I1 'unit. +Fail Next Obligation. + +Equations q15 {L1 : {fset Location}} {I1 : Interface} (_ : both L1 I1 'unit) : both L1 I1 'unit := + q15 _ := + solve_lift (ret_both (tt : 'unit)) : both L1 I1 'unit. +Fail Next Obligation. + +Equations m16 {L1 : {fset Location}} {I1 : Interface} (_ : both L1 I1 'unit) : both L1 I1 'unit := + m16 _ := + solve_lift (ret_both (tt : 'unit)) : both L1 I1 'unit. +Fail Next Obligation. + +Equations l17 {L1 : {fset Location}} {I1 : Interface} (_ : both L1 I1 'unit) : both L1 I1 'unit := + l17 _ := + solve_lift (ret_both (tt : 'unit)) : both L1 I1 'unit. +Fail Next Obligation. + +Equations n18 {L1 : {fset Location}} {I1 : Interface} (_ : both L1 I1 'unit) : both L1 I1 'unit := + n18 _ := + solve_lift (ret_both (tt : 'unit)) : both L1 I1 'unit. +Fail Next Obligation. + +Equations v19 {L1 : {fset Location}} {I1 : Interface} (_ : both L1 I1 'unit) : both L1 I1 'unit := + v19 _ := + solve_lift (ret_both (tt : 'unit)) : both L1 I1 'unit. +Fail Next Obligation. + +Equations s20 {L1 : {fset Location}} {I1 : Interface} (_ : both L1 I1 'unit) : both L1 I1 'unit := + s20 _ := + solve_lift (ret_both (tt : 'unit)) : both L1 I1 'unit. +Fail Next Obligation. + +Equations p21 {L1 : {fset Location}} {I1 : Interface} (_ : both L1 I1 'unit) : both L1 I1 'unit := + p21 _ := + solve_lift (ret_both (tt : 'unit)) : both L1 I1 'unit. +Fail Next Obligation. + +Equations t22 {L1 : {fset Location}} {I1 : Interface} (_ : both L1 I1 'unit) : both L1 I1 'unit := + t22 _ := solve_lift (ret_both (tt : 'unit)) : both L1 I1 'unit. Fail Next Obligation. ''' diff --git a/test-harness/src/snapshots/toolchain__side-effects into-fstar.snap b/test-harness/src/snapshots/toolchain__side-effects into-fstar.snap index a2038278d..08362b003 100644 --- a/test-harness/src/snapshots/toolchain__side-effects into-fstar.snap +++ b/test-harness/src/snapshots/toolchain__side-effects into-fstar.snap @@ -72,8 +72,8 @@ let test (x y: Core.Option.t_Option i32) : Core.Option.t_Option i32 = (fun i -> let i:i32 = i in match y with - | Core.Option.Option_Some hoist1 -> - Core.Option.Option_Some (i +! hoist1 <: i32) <: Core.Option.t_Option i32 + | Core.Option.Option_Some hoist38 -> + Core.Option.Option_Some (i +! hoist38 <: i32) <: Core.Option.t_Option i32 | Core.Option.Option_None -> Core.Option.Option_None <: Core.Option.t_Option i32) with | Core.Option.Option_Some some -> some @@ -85,150 +85,10 @@ module Side_effects open Core open FStar.Mul -type t_A = | A : t_A - -type t_B = | B : t_B - -type t_Bar = { - f_a:bool; - f_b:(t_Array (bool & bool) (sz 6) & bool) -} - -type t_Foo = { - f_x:bool; - f_y:(bool & Alloc.Vec.t_Vec t_Bar Alloc.Alloc.t_Global); - f_z:t_Array t_Bar (sz 6); - f_bar:t_Bar -} - /// Helper function let add3 (x y z: u32) : u32 = Core.Num.impl__u32__wrapping_add (Core.Num.impl__u32__wrapping_add x y <: u32) z -/// Test assignation on non-trivial places -let assign_non_trivial_lhs (foo: t_Foo) : t_Foo = - let foo:t_Foo = { foo with f_x = true } <: t_Foo in - let foo:t_Foo = { foo with f_bar = { foo.f_bar with f_a = true } <: t_Bar } <: t_Foo in - let foo:t_Foo = - { - foo with - f_bar - = - { - foo.f_bar with - f_b - = - { - foo.f_bar.f_b with - _1 - = - Rust_primitives.Hax.Monomorphized_update_at.update_at_usize foo.f_bar.f_b._1 - (sz 3) - ({ (foo.f_bar.f_b._1.[ sz 3 ] <: (bool & bool)) with _2 = true } <: (bool & bool)) - } - <: - (t_Array (bool & bool) (sz 6) & bool) - } - <: - t_Bar - } - <: - t_Foo - in - let foo:t_Foo = - { - foo with - f_z - = - Rust_primitives.Hax.Monomorphized_update_at.update_at_usize foo.f_z - (sz 3) - ({ (foo.f_z.[ sz 3 ] <: t_Bar) with f_a = true } <: t_Bar) - } - <: - t_Foo - in - let foo:t_Foo = - { - foo with - f_y - = - { - foo.f_y with - _2 - = - Rust_primitives.Hax.Monomorphized_update_at.update_at_usize foo.f_y._2 - (sz 3) - ({ - (foo.f_y._2.[ sz 3 ] <: t_Bar) with - f_b - = - { - (foo.f_y._2.[ sz 3 ] <: t_Bar).f_b with - _1 - = - Rust_primitives.Hax.Monomorphized_update_at.update_at_usize (foo.f_y._2.[ sz 3 ] - <: - t_Bar) - .f_b - ._1 - (sz 5) - ({ - ((foo.f_y._2.[ sz 3 ] <: t_Bar).f_b._1.[ sz 5 ] <: (bool & bool)) with - _1 = true - } - <: - (bool & bool)) - <: - t_Array (bool & bool) (sz 6) - } - <: - (t_Array (bool & bool) (sz 6) & bool) - } - <: - t_Bar) - } - <: - (bool & Alloc.Vec.t_Vec t_Bar Alloc.Alloc.t_Global) - } - <: - t_Foo - in - foo - -/// Question mark without error coercion -let direct_result_question_mark (y: Core.Result.t_Result Prims.unit u32) - : Core.Result.t_Result i8 u32 = - match y with - | Core.Result.Result_Ok _ -> Core.Result.Result_Ok 0y <: Core.Result.t_Result i8 u32 - | Core.Result.Result_Err err -> Core.Result.Result_Err err <: Core.Result.t_Result i8 u32 - -/// Question mark with an error coercion -let direct_result_question_mark_coercion (y: Core.Result.t_Result i8 u16) - : Core.Result.t_Result i8 u32 = - match y with - | Core.Result.Result_Ok hoist5 -> Core.Result.Result_Ok hoist5 <: Core.Result.t_Result i8 u32 - | Core.Result.Result_Err err -> - Core.Result.Result_Err (Core.Convert.f_from #u32 #u16 #FStar.Tactics.Typeclasses.solve err) - <: - Core.Result.t_Result i8 u32 - -/// Exercise early returns with control flow and loops -let early_returns (x: u32) : u32 = - if x >. 3ul - then 0ul - else - if x >. 30ul - then - match true with - | true -> 34ul - | _ -> - let x, hoist9:(u32 & u32) = x, 3ul <: (u32 & u32) in - Core.Num.impl__u32__wrapping_add (Core.Num.impl__u32__wrapping_add 123ul hoist9 <: u32) x - else - let x:u32 = x +! 9ul in - let x, hoist9:(u32 & u32) = x, x +! 1ul <: (u32 & u32) in - Core.Num.impl__u32__wrapping_add (Core.Num.impl__u32__wrapping_add 123ul hoist9 <: u32) x - /// Exercise local mutation with control flow and loops let local_mutation (x: u32) : u32 = let y:u32 = 0ul in @@ -255,7 +115,7 @@ let local_mutation (x: u32) : u32 = in Core.Num.impl__u32__wrapping_add x y else - let (x, y), hoist19:((u32 & u32) & u32) = + let (x, y), hoist7:((u32 & u32) & u32) = match x with | 12ul -> let y:u32 = Core.Num.impl__u32__wrapping_add x y in @@ -267,47 +127,97 @@ let local_mutation (x: u32) : u32 = ((u32 & u32) & u32) | _ -> (x, y <: (u32 & u32)), 0ul <: ((u32 & u32) & u32) in - let x:u32 = hoist19 in + let x:u32 = hoist7 in Core.Num.impl__u32__wrapping_add x y -/// Combine `?` and early return -let monad_lifting (x: u8) : Core.Result.t_Result t_A t_B = - if x >. 123uy +/// Exercise early returns with control flow and loops +let early_returns (x: u32) : u32 = + if x >. 3ul + then 0ul + else + if x >. 30ul + then + match true with + | true -> 34ul + | _ -> + let x, hoist11:(u32 & u32) = x, 3ul <: (u32 & u32) in + Core.Num.impl__u32__wrapping_add (Core.Num.impl__u32__wrapping_add 123ul hoist11 <: u32) x + else + let x:u32 = x +! 9ul in + let x, hoist11:(u32 & u32) = x, x +! 1ul <: (u32 & u32) in + Core.Num.impl__u32__wrapping_add (Core.Num.impl__u32__wrapping_add 123ul hoist11 <: u32) x + +let simplifiable_return (c1 c2 c3: bool) : i32 = + let x:i32 = 0l in + if c1 then - match Core.Result.Result_Err (B <: t_B) <: Core.Result.t_Result t_A t_B with - | Core.Result.Result_Ok hoist20 -> Core.Result.Result_Ok hoist20 <: Core.Result.t_Result t_A t_B - | Core.Result.Result_Err err -> Core.Result.Result_Err err <: Core.Result.t_Result t_A t_B - else Core.Result.Result_Ok (A <: t_A) <: Core.Result.t_Result t_A t_B + if c2 + then + let x:i32 = x +! 10l in + if c3 then 1l else x +! 1l + else x +! 1l + else x + +let simplifiable_question_mark (c: bool) (x: Core.Option.t_Option i32) : Core.Option.t_Option i32 = + if c + then + match x with + | Core.Option.Option_Some hoist16 -> + let a:i32 = hoist16 +! 10l in + let b:i32 = 20l in + Core.Option.Option_Some (a +! b) <: Core.Option.t_Option i32 + | Core.Option.Option_None -> Core.Option.Option_None <: Core.Option.t_Option i32 + else + let a:i32 = 0l in + let b:i32 = 20l in + Core.Option.Option_Some (a +! b) <: Core.Option.t_Option i32 + +/// Question mark without error coercion +let direct_result_question_mark (y: Core.Result.t_Result Prims.unit u32) + : Core.Result.t_Result i8 u32 = + match y with + | Core.Result.Result_Ok _ -> Core.Result.Result_Ok 0y <: Core.Result.t_Result i8 u32 + | Core.Result.Result_Err err -> Core.Result.Result_Err err <: Core.Result.t_Result i8 u32 + +/// Question mark with an error coercion +let direct_result_question_mark_coercion (y: Core.Result.t_Result i8 u16) + : Core.Result.t_Result i8 u32 = + match y with + | Core.Result.Result_Ok hoist17 -> Core.Result.Result_Ok hoist17 <: Core.Result.t_Result i8 u32 + | Core.Result.Result_Err err -> + Core.Result.Result_Err (Core.Convert.f_from #u32 #u16 #FStar.Tactics.Typeclasses.solve err) + <: + Core.Result.t_Result i8 u32 /// Test question mark on `Option`s with some control flow let options (x y: Core.Option.t_Option u8) (z: Core.Option.t_Option u64) : Core.Option.t_Option u8 = match x with - | Core.Option.Option_Some hoist26 -> - if hoist26 >. 10uy + | Core.Option.Option_Some hoist21 -> + if hoist21 >. 10uy then match x with - | Core.Option.Option_Some hoist28 -> + | Core.Option.Option_Some hoist23 -> (match - Core.Option.Option_Some (Core.Num.impl__u8__wrapping_add hoist28 3uy) + Core.Option.Option_Some (Core.Num.impl__u8__wrapping_add hoist23 3uy) <: Core.Option.t_Option u8 with - | Core.Option.Option_Some hoist34 -> - (match hoist34 with + | Core.Option.Option_Some hoist29 -> + (match hoist29 with | 3uy -> (match Core.Option.Option_None <: Core.Option.t_Option u8 with | Core.Option.Option_Some some -> let v:u8 = some in (match x with - | Core.Option.Option_Some hoist35 -> + | Core.Option.Option_Some hoist30 -> (match y with - | Core.Option.Option_Some hoist36 -> + | Core.Option.Option_Some hoist31 -> Core.Option.Option_Some (Core.Num.impl__u8__wrapping_add (Core.Num.impl__u8__wrapping_add v - hoist35 + hoist30 <: u8) - hoist36) + hoist31) <: Core.Option.t_Option u8 | Core.Option.Option_None -> @@ -317,18 +227,18 @@ let options (x y: Core.Option.t_Option u8) (z: Core.Option.t_Option u64) : Core. | Core.Option.Option_None -> Core.Option.Option_None <: Core.Option.t_Option u8) | 4uy -> (match z with - | Core.Option.Option_Some hoist23 -> - let v:u8 = 4uy +! (if hoist23 >. 4uL <: bool then 0uy else 3uy) in + | Core.Option.Option_Some hoist18 -> + let v:u8 = 4uy +! (if hoist18 >. 4uL <: bool then 0uy else 3uy) in (match x with - | Core.Option.Option_Some hoist35 -> + | Core.Option.Option_Some hoist30 -> (match y with - | Core.Option.Option_Some hoist36 -> + | Core.Option.Option_Some hoist31 -> Core.Option.Option_Some (Core.Num.impl__u8__wrapping_add (Core.Num.impl__u8__wrapping_add v - hoist35 + hoist30 <: u8) - hoist36) + hoist31) <: Core.Option.t_Option u8 | Core.Option.Option_None -> @@ -339,14 +249,14 @@ let options (x y: Core.Option.t_Option u8) (z: Core.Option.t_Option u64) : Core. | _ -> let v:u8 = 12uy in match x with - | Core.Option.Option_Some hoist35 -> + | Core.Option.Option_Some hoist30 -> (match y with - | Core.Option.Option_Some hoist36 -> + | Core.Option.Option_Some hoist31 -> Core.Option.Option_Some - (Core.Num.impl__u8__wrapping_add (Core.Num.impl__u8__wrapping_add v hoist35 + (Core.Num.impl__u8__wrapping_add (Core.Num.impl__u8__wrapping_add v hoist30 <: u8) - hoist36) + hoist31) <: Core.Option.t_Option u8 | Core.Option.Option_None -> Core.Option.Option_None <: Core.Option.t_Option u8 @@ -356,30 +266,30 @@ let options (x y: Core.Option.t_Option u8) (z: Core.Option.t_Option u64) : Core. | Core.Option.Option_None -> Core.Option.Option_None <: Core.Option.t_Option u8 else (match x with - | Core.Option.Option_Some hoist31 -> + | Core.Option.Option_Some hoist26 -> (match y with - | Core.Option.Option_Some hoist30 -> + | Core.Option.Option_Some hoist25 -> (match - Core.Option.Option_Some (Core.Num.impl__u8__wrapping_add hoist31 hoist30) + Core.Option.Option_Some (Core.Num.impl__u8__wrapping_add hoist26 hoist25) <: Core.Option.t_Option u8 with - | Core.Option.Option_Some hoist34 -> - (match hoist34 with + | Core.Option.Option_Some hoist29 -> + (match hoist29 with | 3uy -> (match Core.Option.Option_None <: Core.Option.t_Option u8 with | Core.Option.Option_Some some -> let v:u8 = some in (match x with - | Core.Option.Option_Some hoist35 -> + | Core.Option.Option_Some hoist30 -> (match y with - | Core.Option.Option_Some hoist36 -> + | Core.Option.Option_Some hoist31 -> Core.Option.Option_Some (Core.Num.impl__u8__wrapping_add (Core.Num.impl__u8__wrapping_add v - hoist35 + hoist30 <: u8) - hoist36) + hoist31) <: Core.Option.t_Option u8 | Core.Option.Option_None -> @@ -390,18 +300,18 @@ let options (x y: Core.Option.t_Option u8) (z: Core.Option.t_Option u64) : Core. Core.Option.Option_None <: Core.Option.t_Option u8) | 4uy -> (match z with - | Core.Option.Option_Some hoist23 -> - let v:u8 = 4uy +! (if hoist23 >. 4uL <: bool then 0uy else 3uy) in + | Core.Option.Option_Some hoist18 -> + let v:u8 = 4uy +! (if hoist18 >. 4uL <: bool then 0uy else 3uy) in (match x with - | Core.Option.Option_Some hoist35 -> + | Core.Option.Option_Some hoist30 -> (match y with - | Core.Option.Option_Some hoist36 -> + | Core.Option.Option_Some hoist31 -> Core.Option.Option_Some (Core.Num.impl__u8__wrapping_add (Core.Num.impl__u8__wrapping_add v - hoist35 + hoist30 <: u8) - hoist36) + hoist31) <: Core.Option.t_Option u8 | Core.Option.Option_None -> @@ -413,15 +323,15 @@ let options (x y: Core.Option.t_Option u8) (z: Core.Option.t_Option u64) : Core. | _ -> let v:u8 = 12uy in match x with - | Core.Option.Option_Some hoist35 -> + | Core.Option.Option_Some hoist30 -> (match y with - | Core.Option.Option_Some hoist36 -> + | Core.Option.Option_Some hoist31 -> Core.Option.Option_Some (Core.Num.impl__u8__wrapping_add (Core.Num.impl__u8__wrapping_add v - hoist35 + hoist30 <: u8) - hoist36) + hoist31) <: Core.Option.t_Option u8 | Core.Option.Option_None -> @@ -457,28 +367,118 @@ let question_mark (x: u32) : Core.Result.t_Result u32 u32 = else Core.Result.Result_Ok (Core.Num.impl__u32__wrapping_add 3ul x) <: Core.Result.t_Result u32 u32 -let simplifiable_question_mark (c: bool) (x: Core.Option.t_Option i32) : Core.Option.t_Option i32 = - if c - then - match x with - | Core.Option.Option_Some hoist40 -> - let a:i32 = hoist40 +! 10l in - let b:i32 = 20l in - Core.Option.Option_Some (a +! b) <: Core.Option.t_Option i32 - | Core.Option.Option_None -> Core.Option.Option_None <: Core.Option.t_Option i32 - else - let a:i32 = 0l in - let b:i32 = 20l in - Core.Option.Option_Some (a +! b) <: Core.Option.t_Option i32 +type t_A = | A : t_A -let simplifiable_return (c1 c2 c3: bool) : i32 = - let x:i32 = 0l in - if c1 +type t_B = | B : t_B + +/// Combine `?` and early return +let monad_lifting (x: u8) : Core.Result.t_Result t_A t_B = + if x >. 123uy then - if c2 - then - let x:i32 = x +! 10l in - if c3 then 1l else x +! 1l - else x +! 1l - else x + match Core.Result.Result_Err (B <: t_B) <: Core.Result.t_Result t_A t_B with + | Core.Result.Result_Ok hoist35 -> Core.Result.Result_Ok hoist35 <: Core.Result.t_Result t_A t_B + | Core.Result.Result_Err err -> Core.Result.Result_Err err <: Core.Result.t_Result t_A t_B + else Core.Result.Result_Ok (A <: t_A) <: Core.Result.t_Result t_A t_B + +type t_Bar = { + f_a:bool; + f_b:(t_Array (bool & bool) (sz 6) & bool) +} + +type t_Foo = { + f_x:bool; + f_y:(bool & Alloc.Vec.t_Vec t_Bar Alloc.Alloc.t_Global); + f_z:t_Array t_Bar (sz 6); + f_bar:t_Bar +} + +/// Test assignation on non-trivial places +let assign_non_trivial_lhs (foo: t_Foo) : t_Foo = + let foo:t_Foo = { foo with f_x = true } <: t_Foo in + let foo:t_Foo = { foo with f_bar = { foo.f_bar with f_a = true } <: t_Bar } <: t_Foo in + let foo:t_Foo = + { + foo with + f_bar + = + { + foo.f_bar with + f_b + = + { + foo.f_bar.f_b with + _1 + = + Rust_primitives.Hax.Monomorphized_update_at.update_at_usize foo.f_bar.f_b._1 + (sz 3) + ({ (foo.f_bar.f_b._1.[ sz 3 ] <: (bool & bool)) with _2 = true } <: (bool & bool)) + } + <: + (t_Array (bool & bool) (sz 6) & bool) + } + <: + t_Bar + } + <: + t_Foo + in + let foo:t_Foo = + { + foo with + f_z + = + Rust_primitives.Hax.Monomorphized_update_at.update_at_usize foo.f_z + (sz 3) + ({ (foo.f_z.[ sz 3 ] <: t_Bar) with f_a = true } <: t_Bar) + } + <: + t_Foo + in + let foo:t_Foo = + { + foo with + f_y + = + { + foo.f_y with + _2 + = + Rust_primitives.Hax.Monomorphized_update_at.update_at_usize foo.f_y._2 + (sz 3) + ({ + (foo.f_y._2.[ sz 3 ] <: t_Bar) with + f_b + = + { + (foo.f_y._2.[ sz 3 ] <: t_Bar).f_b with + _1 + = + Rust_primitives.Hax.Monomorphized_update_at.update_at_usize (foo.f_y._2.[ sz 3 ] + <: + t_Bar) + .f_b + ._1 + (sz 5) + ({ + ((foo.f_y._2.[ sz 3 ] <: t_Bar).f_b._1.[ sz 5 ] <: (bool & bool)) with + _1 = true + } + <: + (bool & bool)) + <: + t_Array (bool & bool) (sz 6) + } + <: + (t_Array (bool & bool) (sz 6) & bool) + } + <: + t_Bar) + } + <: + (bool & Alloc.Vec.t_Vec t_Bar Alloc.Alloc.t_Global) + } + <: + t_Foo + in + foo ''' diff --git a/test-harness/src/snapshots/toolchain__side-effects into-ssprove.snap b/test-harness/src/snapshots/toolchain__side-effects into-ssprove.snap index 2f2304adb..4f1746a23 100644 --- a/test-harness/src/snapshots/toolchain__side-effects into-ssprove.snap +++ b/test-harness/src/snapshots/toolchain__side-effects into-ssprove.snap @@ -54,6 +54,163 @@ Import choice.Choice.Exports. Obligation Tactic := (* try timeout 8 *) solve_ssprove_obligations. +(*Not implemented yet? todo(item)*) + +Equations add3 {L1 : {fset Location}} {L2 : {fset Location}} {L3 : {fset Location}} {I1 : Interface} {I2 : Interface} {I3 : Interface} (x : both L1 I1 int32) (y : both L2 I2 int32) (z : both L3 I3 int32) : both (L1 :|: L2 :|: L3) (I1 :|: I2 :|: I3) int32 := + add3 x y z := + solve_lift (impl__u32__wrapping_add (impl__u32__wrapping_add x y) z) : both (L1 :|: L2 :|: L3) (I1 :|: I2 :|: I3) int32. +Fail Next Obligation. + +Definition y_loc : Location := + (int32;0%nat). +Definition y_loc : Location := + (int32;1%nat). +Equations local_mutation {L1 : {fset Location}} {I1 : Interface} (x : both L1 I1 int32) : both (L1 :|: fset [y_loc;y_loc]) I1 int32 := + local_mutation x := + letb y loc(y_loc) := ret_both (0 : int32) in + letb _ := assign todo(term) in + letb hoist1 := x >.? (ret_both (3 : int32)) in + solve_lift (ifb hoist1 + then letb _ := assign todo(term) in + letb y loc(y_loc) := x ./ (ret_both (2 : int32)) in + letb _ := assign todo(term) in + letb hoist2 := ret_both (0 : int32) in + letb hoist3 := Build_t_Range (f_start := hoist2) (f_end := ret_both (10 : int32)) in + letb hoist4 := f_into_iter hoist3 in + letb _ := foldi_both_list hoist4 (fun i => + ssp (fun _ => + assign todo(term) : (both (*0*)(L1:|:fset []) (I1) 'unit))) (ret_both (tt : 'unit)) in + impl__u32__wrapping_add x y + else letb hoist7 := matchb x with + | 12 => + letb _ := assign todo(term) in + solve_lift (ret_both (3 : int32)) + | 13 => + letb hoist6 := x in + letb _ := assign todo(term) in + letb hoist5 := impl__u32__wrapping_add (ret_both (123 : int32)) x in + solve_lift (add3 hoist6 hoist5 x) + | _ => + solve_lift (ret_both (0 : int32)) + end in + letb _ := assign todo(term) in + impl__u32__wrapping_add x y) : both (L1 :|: fset [y_loc;y_loc]) I1 int32. +Fail Next Obligation. + +Equations early_returns {L1 : {fset Location}} {I1 : Interface} (x : both L1 I1 int32) : both L1 I1 int32 := + early_returns x := + solve_lift (run (letm[choice_typeMonad.result_bind_code int32] _ := ifb x >.? (ret_both (3 : int32)) + then letm[choice_typeMonad.result_bind_code int32] hoist8 := ControlFlow_Break (ret_both (0 : int32)) in + ControlFlow_Continue (never_to_any hoist8) + else () in + letb hoist9 := x >.? (ret_both (30 : int32)) in + letm[choice_typeMonad.result_bind_code int32] hoist11 := ifb hoist9 + then matchb ret_both (true : 'bool) with + | true => + letm[choice_typeMonad.result_bind_code int32] hoist10 := ControlFlow_Break (ret_both (34 : int32)) in + ControlFlow_Continue (solve_lift (never_to_any hoist10)) + | _ => + ControlFlow_Continue (solve_lift (ret_both (3 : int32))) + end + else ControlFlow_Continue (letb _ := assign todo(term) in + x .+ (ret_both (1 : int32))) in + letb hoist12 := impl__u32__wrapping_add (ret_both (123 : int32)) hoist11 in + letb hoist13 := impl__u32__wrapping_add hoist12 x in + letm[choice_typeMonad.result_bind_code int32] hoist14 := ControlFlow_Break hoist13 in + ControlFlow_Continue (never_to_any hoist14))) : both L1 I1 int32. +Fail Next Obligation. + +Definition x_loc : Location := + (int32;2%nat). +Equations simplifiable_return {L1 : {fset Location}} {L2 : {fset Location}} {L3 : {fset Location}} {I1 : Interface} {I2 : Interface} {I3 : Interface} (c1 : both L1 I1 'bool) (c2 : both L2 I2 'bool) (c3 : both L3 I3 'bool) : both (L1 :|: L2 :|: L3 :|: fset [x_loc]) (I1 :|: I2 :|: I3) int32 := + simplifiable_return c1 c2 c3 := + solve_lift (run (letb x loc(x_loc) := ret_both (0 : int32) in + letm[choice_typeMonad.result_bind_code int32] _ := ifb c1 + then letm[choice_typeMonad.result_bind_code int32] _ := ifb c2 + then letb _ := assign todo(term) in + ifb c3 + then letm[choice_typeMonad.result_bind_code int32] hoist15 := ControlFlow_Break (ret_both (1 : int32)) in + ControlFlow_Continue (never_to_any hoist15) + else () + else () in + ControlFlow_Continue (letb _ := assign todo(term) in + ret_both (tt : 'unit)) + else () in + ControlFlow_Continue x)) : both (L1 :|: L2 :|: L3 :|: fset [x_loc]) (I1 :|: I2 :|: I3) int32. +Fail Next Obligation. + +Equations simplifiable_question_mark {L1 : {fset Location}} {L2 : {fset Location}} {I1 : Interface} {I2 : Interface} (c : both L1 I1 'bool) (x : both L2 I2 (t_Option int32)) : both (L1 :|: L2) (I1 :|: I2) (t_Option int32) := + simplifiable_question_mark c x := + solve_lift (run (letm[choice_typeMonad.option_bind_code] a := ifb c + then letm[choice_typeMonad.option_bind_code] hoist16 := x in + Option_Some (hoist16 .+ (ret_both (10 : int32))) + else Option_Some (ret_both (0 : int32)) in + Option_Some (letb b := ret_both (20 : int32) in + Option_Some (a .+ b)))) : both (L1 :|: L2) (I1 :|: I2) (t_Option int32). +Fail Next Obligation. + +Equations direct_result_question_mark {L1 : {fset Location}} {I1 : Interface} (y : both L1 I1 (t_Result 'unit int32)) : both L1 I1 (t_Result int8 int32) := + direct_result_question_mark y := + solve_lift (run (letm[choice_typeMonad.result_bind_code int32] _ := y in + Result_Ok (Result_Ok (ret_both (0 : int8))))) : both L1 I1 (t_Result int8 int32). +Fail Next Obligation. + +Equations direct_result_question_mark_coercion {L1 : {fset Location}} {I1 : Interface} (y : both L1 I1 (t_Result int8 int16)) : both L1 I1 (t_Result int8 int32) := + direct_result_question_mark_coercion y := + solve_lift (run (letm[choice_typeMonad.result_bind_code int32] hoist17 := impl__map_err y f_from in + Result_Ok (Result_Ok hoist17))) : both L1 I1 (t_Result int8 int32). +Fail Next Obligation. + +Equations options {L1 : {fset Location}} {L2 : {fset Location}} {L3 : {fset Location}} {I1 : Interface} {I2 : Interface} {I3 : Interface} (x : both L1 I1 (t_Option int8)) (y : both L2 I2 (t_Option int8)) (z : both L3 I3 (t_Option int64)) : both (L1 :|: L2 :|: L3) (I1 :|: I2 :|: I3) (t_Option int8) := + options x y z := + solve_lift (run (letm[choice_typeMonad.option_bind_code] hoist21 := x in + letb hoist22 := hoist21 >.? (ret_both (10 : int8)) in + letm[choice_typeMonad.option_bind_code] hoist28 := ifb hoist22 + then letm[choice_typeMonad.option_bind_code] hoist23 := x in + Option_Some (letb hoist24 := impl__u8__wrapping_add hoist23 (ret_both (3 : int8)) in + Option_Some hoist24) + else letm[choice_typeMonad.option_bind_code] hoist26 := x in + letm[choice_typeMonad.option_bind_code] hoist25 := y in + Option_Some (letb hoist27 := impl__u8__wrapping_add hoist26 hoist25 in + Option_Some hoist27) in + letm[choice_typeMonad.option_bind_code] hoist29 := hoist28 in + letm[choice_typeMonad.option_bind_code] v := matchb hoist29 with + | 3 => + Option_None + | 4 => + letm[choice_typeMonad.option_bind_code] hoist18 := z in + Option_Some (letb hoist19 := hoist18 >.? (ret_both (4 : int64)) in + letb hoist20 := ifb hoist19 + then ret_both (0 : int8) + else ret_both (3 : int8) in + solve_lift ((ret_both (4 : int8)) .+ hoist20)) + | _ => + Option_Some (solve_lift (ret_both (12 : int8))) + end in + letm[choice_typeMonad.option_bind_code] hoist30 := x in + letb hoist32 := impl__u8__wrapping_add v hoist30 in + letm[choice_typeMonad.option_bind_code] hoist31 := y in + Option_Some (letb hoist33 := impl__u8__wrapping_add hoist32 hoist31 in + Option_Some hoist33))) : both (L1 :|: L2 :|: L3) (I1 :|: I2 :|: I3) (t_Option int8). +Fail Next Obligation. + +Definition y_loc : Location := + (int32;3%nat). +Equations question_mark {L1 : {fset Location}} {I1 : Interface} (x : both L1 I1 int32) : both (L1 :|: fset [y_loc]) I1 (t_Result int32 int32) := + question_mark x := + solve_lift (run (letm[choice_typeMonad.result_bind_code int32] _ := ifb x >.? (ret_both (40 : int32)) + then letb y loc(y_loc) := ret_both (0 : int32) in + letb _ := assign todo(term) in + letb _ := assign todo(term) in + letb _ := assign todo(term) in + letb hoist34 := x >.? (ret_both (90 : int32)) in + ifb hoist34 + then impl__map_err (Result_Err (ret_both (12 : int8))) f_from + else () + else () in + Result_Ok (Result_Ok (impl__u32__wrapping_add (ret_both (3 : int32)) x)))) : both (L1 :|: fset [y_loc]) I1 (t_Result int32 int32). +Fail Next Obligation. + Definition t_A : choice_type := 'unit. Equations Build_t_A : both (fset []) (fset []) (t_A) := @@ -68,6 +225,16 @@ Equations Build_t_B : both (fset []) (fset []) (t_B) := solve_lift (ret_both (tt (* Empty tuple *) : (t_B))) : both (fset []) (fset []) (t_B). Fail Next Obligation. +Equations monad_lifting {L1 : {fset Location}} {I1 : Interface} (x : both L1 I1 int8) : both L1 I1 (t_Result t_A t_B) := + monad_lifting x := + solve_lift (run (ifb x >.? (ret_both (123 : int8)) + then letm[choice_typeMonad.result_bind_code (t_Result t_A t_B)] hoist35 := ControlFlow_Continue (Result_Err B) in + letb hoist36 := Result_Ok hoist35 in + letm[choice_typeMonad.result_bind_code (t_Result t_A t_B)] hoist37 := ControlFlow_Break hoist36 in + ControlFlow_Continue (never_to_any hoist37) + else ControlFlow_Continue (Result_Ok A))) : both L1 I1 (t_Result t_A t_B). +Fail Next Obligation. + Definition t_Bar : choice_type := ('bool × nseq ('bool × 'bool) 6 × 'bool). Equations f_a {L : {fset Location}} {I : Interface} (s : both L I t_Bar) : both L I 'bool := @@ -124,17 +291,6 @@ Notation "'Build_t_Foo' '[' x ']' '(' 'f_y' ':=' y ')'" := (Build_t_Foo (f_x := Notation "'Build_t_Foo' '[' x ']' '(' 'f_z' ':=' y ')'" := (Build_t_Foo (f_x := f_x x) (f_y := f_y x) (f_z := y) (f_bar := f_bar x)). Notation "'Build_t_Foo' '[' x ']' '(' 'f_bar' ':=' y ')'" := (Build_t_Foo (f_x := f_x x) (f_y := f_y x) (f_z := f_z x) (f_bar := y)). -(*Not implemented yet? todo(item)*) - -(*Not implemented yet? todo(item)*) - -(*Not implemented yet? todo(item)*) - -Equations add3 {L1 : {fset Location}} {L2 : {fset Location}} {L3 : {fset Location}} {I1 : Interface} {I2 : Interface} {I3 : Interface} (x : both L1 I1 int32) (y : both L2 I2 int32) (z : both L3 I3 int32) : both (L1 :|: L2 :|: L3) (I1 :|: I2 :|: I3) int32 := - add3 x y z := - solve_lift (impl__u32__wrapping_add (impl__u32__wrapping_add x y) z) : both (L1 :|: L2 :|: L3) (I1 :|: I2 :|: I3) int32. -Fail Next Obligation. - Equations assign_non_trivial_lhs {L1 : {fset Location}} {I1 : Interface} (foo : both L1 I1 t_Foo) : both L1 I1 t_Foo := assign_non_trivial_lhs foo := letb _ := assign todo(term) in @@ -145,165 +301,9 @@ Equations assign_non_trivial_lhs {L1 : {fset Location}} {I1 : Interface} (foo : solve_lift foo : both L1 I1 t_Foo. Fail Next Obligation. -Equations direct_result_question_mark {L1 : {fset Location}} {I1 : Interface} (y : both L1 I1 (t_Result 'unit int32)) : both L1 I1 (t_Result int8 int32) := - direct_result_question_mark y := - solve_lift (run (letm[choice_typeMonad.result_bind_code int32] _ := y in - Result_Ok (Result_Ok (ret_both (0 : int8))))) : both L1 I1 (t_Result int8 int32). -Fail Next Obligation. - -Equations direct_result_question_mark_coercion {L1 : {fset Location}} {I1 : Interface} (y : both L1 I1 (t_Result int8 int16)) : both L1 I1 (t_Result int8 int32) := - direct_result_question_mark_coercion y := - solve_lift (run (letm[choice_typeMonad.result_bind_code int32] hoist5 := impl__map_err y f_from in - Result_Ok (Result_Ok hoist5))) : both L1 I1 (t_Result int8 int32). -Fail Next Obligation. - -Equations early_returns {L1 : {fset Location}} {I1 : Interface} (x : both L1 I1 int32) : both L1 I1 int32 := - early_returns x := - solve_lift (run (letm[choice_typeMonad.result_bind_code int32] _ := ifb x >.? (ret_both (3 : int32)) - then letm[choice_typeMonad.result_bind_code int32] hoist6 := ControlFlow_Break (ret_both (0 : int32)) in - ControlFlow_Continue (never_to_any hoist6) - else () in - letb hoist7 := x >.? (ret_both (30 : int32)) in - letm[choice_typeMonad.result_bind_code int32] hoist9 := ifb hoist7 - then matchb ret_both (true : 'bool) with - | true => - letm[choice_typeMonad.result_bind_code int32] hoist8 := ControlFlow_Break (ret_both (34 : int32)) in - ControlFlow_Continue (solve_lift (never_to_any hoist8)) - | _ => - ControlFlow_Continue (solve_lift (ret_both (3 : int32))) - end - else ControlFlow_Continue (letb _ := assign todo(term) in - x .+ (ret_both (1 : int32))) in - letb hoist10 := impl__u32__wrapping_add (ret_both (123 : int32)) hoist9 in - letb hoist11 := impl__u32__wrapping_add hoist10 x in - letm[choice_typeMonad.result_bind_code int32] hoist12 := ControlFlow_Break hoist11 in - ControlFlow_Continue (never_to_any hoist12))) : both L1 I1 int32. -Fail Next Obligation. - -Definition y_loc : Location := - (int32;0%nat). -Definition y_loc : Location := - (int32;1%nat). -Equations local_mutation {L1 : {fset Location}} {I1 : Interface} (x : both L1 I1 int32) : both (L1 :|: fset [y_loc;y_loc]) I1 int32 := - local_mutation x := - letb y loc(y_loc) := ret_both (0 : int32) in - letb _ := assign todo(term) in - letb hoist13 := x >.? (ret_both (3 : int32)) in - solve_lift (ifb hoist13 - then letb _ := assign todo(term) in - letb y loc(y_loc) := x ./ (ret_both (2 : int32)) in - letb _ := assign todo(term) in - letb hoist14 := ret_both (0 : int32) in - letb hoist15 := Build_t_Range (f_start := hoist14) (f_end := ret_both (10 : int32)) in - letb hoist16 := f_into_iter hoist15 in - letb _ := foldi_both_list hoist16 (fun i => - ssp (fun _ => - assign todo(term) : (both (*0*)(L1:|:fset []) (I1) 'unit))) (ret_both (tt : 'unit)) in - impl__u32__wrapping_add x y - else letb hoist19 := matchb x with - | 12 => - letb _ := assign todo(term) in - solve_lift (ret_both (3 : int32)) - | 13 => - letb hoist18 := x in - letb _ := assign todo(term) in - letb hoist17 := impl__u32__wrapping_add (ret_both (123 : int32)) x in - solve_lift (add3 hoist18 hoist17 x) - | _ => - solve_lift (ret_both (0 : int32)) - end in - letb _ := assign todo(term) in - impl__u32__wrapping_add x y) : both (L1 :|: fset [y_loc;y_loc]) I1 int32. -Fail Next Obligation. - -Equations monad_lifting {L1 : {fset Location}} {I1 : Interface} (x : both L1 I1 int8) : both L1 I1 (t_Result t_A t_B) := - monad_lifting x := - solve_lift (run (ifb x >.? (ret_both (123 : int8)) - then letm[choice_typeMonad.result_bind_code (t_Result t_A t_B)] hoist20 := ControlFlow_Continue (Result_Err B) in - letb hoist21 := Result_Ok hoist20 in - letm[choice_typeMonad.result_bind_code (t_Result t_A t_B)] hoist22 := ControlFlow_Break hoist21 in - ControlFlow_Continue (never_to_any hoist22) - else ControlFlow_Continue (Result_Ok A))) : both L1 I1 (t_Result t_A t_B). -Fail Next Obligation. - -Equations options {L1 : {fset Location}} {L2 : {fset Location}} {L3 : {fset Location}} {I1 : Interface} {I2 : Interface} {I3 : Interface} (x : both L1 I1 (t_Option int8)) (y : both L2 I2 (t_Option int8)) (z : both L3 I3 (t_Option int64)) : both (L1 :|: L2 :|: L3) (I1 :|: I2 :|: I3) (t_Option int8) := - options x y z := - solve_lift (run (letm[choice_typeMonad.option_bind_code] hoist26 := x in - letb hoist27 := hoist26 >.? (ret_both (10 : int8)) in - letm[choice_typeMonad.option_bind_code] hoist33 := ifb hoist27 - then letm[choice_typeMonad.option_bind_code] hoist28 := x in - Option_Some (letb hoist29 := impl__u8__wrapping_add hoist28 (ret_both (3 : int8)) in - Option_Some hoist29) - else letm[choice_typeMonad.option_bind_code] hoist31 := x in - letm[choice_typeMonad.option_bind_code] hoist30 := y in - Option_Some (letb hoist32 := impl__u8__wrapping_add hoist31 hoist30 in - Option_Some hoist32) in - letm[choice_typeMonad.option_bind_code] hoist34 := hoist33 in - letm[choice_typeMonad.option_bind_code] v := matchb hoist34 with - | 3 => - Option_None - | 4 => - letm[choice_typeMonad.option_bind_code] hoist23 := z in - Option_Some (letb hoist24 := hoist23 >.? (ret_both (4 : int64)) in - letb hoist25 := ifb hoist24 - then ret_both (0 : int8) - else ret_both (3 : int8) in - solve_lift ((ret_both (4 : int8)) .+ hoist25)) - | _ => - Option_Some (solve_lift (ret_both (12 : int8))) - end in - letm[choice_typeMonad.option_bind_code] hoist35 := x in - letb hoist37 := impl__u8__wrapping_add v hoist35 in - letm[choice_typeMonad.option_bind_code] hoist36 := y in - Option_Some (letb hoist38 := impl__u8__wrapping_add hoist37 hoist36 in - Option_Some hoist38))) : both (L1 :|: L2 :|: L3) (I1 :|: I2 :|: I3) (t_Option int8). -Fail Next Obligation. - -Definition y_loc : Location := - (int32;2%nat). -Equations question_mark {L1 : {fset Location}} {I1 : Interface} (x : both L1 I1 int32) : both (L1 :|: fset [y_loc]) I1 (t_Result int32 int32) := - question_mark x := - solve_lift (run (letm[choice_typeMonad.result_bind_code int32] _ := ifb x >.? (ret_both (40 : int32)) - then letb y loc(y_loc) := ret_both (0 : int32) in - letb _ := assign todo(term) in - letb _ := assign todo(term) in - letb _ := assign todo(term) in - letb hoist39 := x >.? (ret_both (90 : int32)) in - ifb hoist39 - then impl__map_err (Result_Err (ret_both (12 : int8))) f_from - else () - else () in - Result_Ok (Result_Ok (impl__u32__wrapping_add (ret_both (3 : int32)) x)))) : both (L1 :|: fset [y_loc]) I1 (t_Result int32 int32). -Fail Next Obligation. - -Equations simplifiable_question_mark {L1 : {fset Location}} {L2 : {fset Location}} {I1 : Interface} {I2 : Interface} (c : both L1 I1 'bool) (x : both L2 I2 (t_Option int32)) : both (L1 :|: L2) (I1 :|: I2) (t_Option int32) := - simplifiable_question_mark c x := - solve_lift (run (letm[choice_typeMonad.option_bind_code] a := ifb c - then letm[choice_typeMonad.option_bind_code] hoist40 := x in - Option_Some (hoist40 .+ (ret_both (10 : int32))) - else Option_Some (ret_both (0 : int32)) in - Option_Some (letb b := ret_both (20 : int32) in - Option_Some (a .+ b)))) : both (L1 :|: L2) (I1 :|: I2) (t_Option int32). -Fail Next Obligation. +(*Not implemented yet? todo(item)*) -Definition x_loc : Location := - (int32;3%nat). -Equations simplifiable_return {L1 : {fset Location}} {L2 : {fset Location}} {L3 : {fset Location}} {I1 : Interface} {I2 : Interface} {I3 : Interface} (c1 : both L1 I1 'bool) (c2 : both L2 I2 'bool) (c3 : both L3 I3 'bool) : both (L1 :|: L2 :|: L3 :|: fset [x_loc]) (I1 :|: I2 :|: I3) int32 := - simplifiable_return c1 c2 c3 := - solve_lift (run (letb x loc(x_loc) := ret_both (0 : int32) in - letm[choice_typeMonad.result_bind_code int32] _ := ifb c1 - then letm[choice_typeMonad.result_bind_code int32] _ := ifb c2 - then letb _ := assign todo(term) in - ifb c3 - then letm[choice_typeMonad.result_bind_code int32] hoist41 := ControlFlow_Break (ret_both (1 : int32)) in - ControlFlow_Continue (never_to_any hoist41) - else () - else () in - ControlFlow_Continue (letb _ := assign todo(term) in - ret_both (tt : 'unit)) - else () in - ControlFlow_Continue x)) : both (L1 :|: L2 :|: L3 :|: fset [x_loc]) (I1 :|: I2 :|: I3) int32. -Fail Next Obligation. +(*Not implemented yet? todo(item)*) ''' "Side_effects_Issue_1083_.v" = ''' (* File automatically generated by Hacspec *) @@ -380,11 +380,11 @@ Obligation Tactic := (* try timeout 8 *) solve_ssprove_obligations. Equations test {L1 : {fset Location}} {L2 : {fset Location}} {I1 : Interface} {I2 : Interface} (x : both L1 I1 (t_Option int32)) (y : both L2 I2 (t_Option int32)) : both (L1 :|: L2) (I1 :|: I2) (t_Option int32) := test x y := - solve_lift (run (letb hoist3 := fun i => - letm[choice_typeMonad.option_bind_code] hoist1 := y in - Option_Some (letb hoist2 := i .+ hoist1 in - Option_Some hoist2) in - letb hoist4 := impl__map x hoist3 in - hoist4)) : both (L1 :|: L2) (I1 :|: I2) (t_Option int32). + solve_lift (run (letb hoist40 := fun i => + letm[choice_typeMonad.option_bind_code] hoist38 := y in + Option_Some (letb hoist39 := i .+ hoist38 in + Option_Some hoist39) in + letb hoist41 := impl__map x hoist40 in + hoist41)) : both (L1 :|: L2) (I1 :|: I2) (t_Option int32). Fail Next Obligation. ''' diff --git a/test-harness/src/snapshots/toolchain__traits into-fstar.snap b/test-harness/src/snapshots/toolchain__traits into-fstar.snap index fcc166dc9..bcb0821fb 100644 --- a/test-harness/src/snapshots/toolchain__traits into-fstar.snap +++ b/test-harness/src/snapshots/toolchain__traits into-fstar.snap @@ -79,33 +79,6 @@ module Traits.For_clauses.Issue_495_ open Core open FStar.Mul -let minimized_1_ (list: Alloc.Vec.t_Vec u8 Alloc.Alloc.t_Global) - : Alloc.Vec.t_Vec u8 Alloc.Alloc.t_Global = - Core.Iter.Traits.Iterator.f_collect #(Core.Iter.Adapters.Filter.t_Filter - (Core.Ops.Range.t_Range u8) (u8 -> bool)) - #FStar.Tactics.Typeclasses.solve - #(Alloc.Vec.t_Vec u8 Alloc.Alloc.t_Global) - (Core.Iter.Traits.Iterator.f_filter #(Core.Ops.Range.t_Range u8) - #FStar.Tactics.Typeclasses.solve - ({ Core.Ops.Range.f_start = 0uy; Core.Ops.Range.f_end = 5uy } <: Core.Ops.Range.t_Range u8) - (fun temp_0_ -> - let _:u8 = temp_0_ in - true) - <: - Core.Iter.Adapters.Filter.t_Filter (Core.Ops.Range.t_Range u8) (u8 -> bool)) - -let minimized_2_ (it: Core.Iter.Adapters.Filter.t_Filter (Core.Ops.Range.t_Range u8) (u8 -> bool)) - : Prims.unit = - let (v__indices: Alloc.Vec.t_Vec u8 Alloc.Alloc.t_Global):Alloc.Vec.t_Vec u8 Alloc.Alloc.t_Global - = - Core.Iter.Traits.Iterator.f_collect #(Core.Iter.Adapters.Filter.t_Filter - (Core.Ops.Range.t_Range u8) (u8 -> bool)) - #FStar.Tactics.Typeclasses.solve - #(Alloc.Vec.t_Vec u8 Alloc.Alloc.t_Global) - it - in - () - let original_function_from_495_ (list: Alloc.Vec.t_Vec u8 Alloc.Alloc.t_Global) : Prims.unit = let (v__indices: Alloc.Vec.t_Vec u8 Alloc.Alloc.t_Global):Alloc.Vec.t_Vec u8 Alloc.Alloc.t_Global = @@ -139,6 +112,33 @@ let original_function_from_495_ (list: Alloc.Vec.t_Vec u8 Alloc.Alloc.t_Global) Core.Iter.Adapters.Filter.t_Filter (Core.Ops.Range.t_Range u8) (u8 -> bool)) in () + +let minimized_1_ (list: Alloc.Vec.t_Vec u8 Alloc.Alloc.t_Global) + : Alloc.Vec.t_Vec u8 Alloc.Alloc.t_Global = + Core.Iter.Traits.Iterator.f_collect #(Core.Iter.Adapters.Filter.t_Filter + (Core.Ops.Range.t_Range u8) (u8 -> bool)) + #FStar.Tactics.Typeclasses.solve + #(Alloc.Vec.t_Vec u8 Alloc.Alloc.t_Global) + (Core.Iter.Traits.Iterator.f_filter #(Core.Ops.Range.t_Range u8) + #FStar.Tactics.Typeclasses.solve + ({ Core.Ops.Range.f_start = 0uy; Core.Ops.Range.f_end = 5uy } <: Core.Ops.Range.t_Range u8) + (fun temp_0_ -> + let _:u8 = temp_0_ in + true) + <: + Core.Iter.Adapters.Filter.t_Filter (Core.Ops.Range.t_Range u8) (u8 -> bool)) + +let minimized_2_ (it: Core.Iter.Adapters.Filter.t_Filter (Core.Ops.Range.t_Range u8) (u8 -> bool)) + : Prims.unit = + let (v__indices: Alloc.Vec.t_Vec u8 Alloc.Alloc.t_Global):Alloc.Vec.t_Vec u8 Alloc.Alloc.t_Global + = + Core.Iter.Traits.Iterator.f_collect #(Core.Iter.Adapters.Filter.t_Filter + (Core.Ops.Range.t_Range u8) (u8 -> bool)) + #FStar.Tactics.Typeclasses.solve + #(Alloc.Vec.t_Vec u8 Alloc.Alloc.t_Global) + it + in + () ''' "Traits.For_clauses.fst" = ''' module Traits.For_clauses @@ -342,7 +342,7 @@ let impl (#v_TypeArg: Type0) (v_ConstArg: usize) : t_Trait Prims.unit v_TypeArg () } -let associated_function_caller +let method_caller (#v_MethodTypeArg #v_TypeArg: Type0) (v_ConstArg v_MethodConstArg: usize) (#v_ImplTrait: Type0) @@ -352,7 +352,7 @@ let associated_function_caller (value_Type: t_Type v_TypeArg v_ConstArg) : Prims.unit = let _:Prims.unit = - f_associated_function #v_ImplTrait + f_method #v_ImplTrait #v_TypeArg #v_ConstArg #FStar.Tactics.Typeclasses.solve @@ -364,7 +364,7 @@ let associated_function_caller in () -let method_caller +let associated_function_caller (#v_MethodTypeArg #v_TypeArg: Type0) (v_ConstArg v_MethodConstArg: usize) (#v_ImplTrait: Type0) @@ -374,7 +374,7 @@ let method_caller (value_Type: t_Type v_TypeArg v_ConstArg) : Prims.unit = let _:Prims.unit = - f_method #v_ImplTrait + f_associated_function #v_ImplTrait #v_TypeArg #v_ConstArg #FStar.Tactics.Typeclasses.solve @@ -491,14 +491,14 @@ module Traits.Unconstrainted_types_issue_677_ open Core open FStar.Mul -type t_Plus = | Plus : t_Plus - class t_PolyOp (v_Self: Type0) = { f_op_pre:u32 -> u32 -> Type0; f_op_post:u32 -> u32 -> u32 -> Type0; f_op:x0: u32 -> x1: u32 -> Prims.Pure u32 (f_op_pre x0 x1) (fun result -> f_op_post x0 x1 result) } +type t_Plus = | Plus : t_Plus + [@@ FStar.Tactics.Typeclasses.tcinstance] let impl: t_PolyOp t_Plus = { @@ -528,26 +528,6 @@ module Traits open Core open FStar.Mul -class t_Bar (v_Self: Type0) = { - f_bar_pre:v_Self -> Type0; - f_bar_post:v_Self -> Prims.unit -> Type0; - f_bar:x0: v_Self -> Prims.Pure Prims.unit (f_bar_pre x0) (fun result -> f_bar_post x0 result) -} - -let impl_2__method (#v_T: Type0) (#[FStar.Tactics.Typeclasses.tcresolve ()] i1: t_Bar v_T) (x: v_T) - : Prims.unit = f_bar #v_T #FStar.Tactics.Typeclasses.solve x - -type t_Error = | Error_Fail : t_Error - -let impl__Error__for_application_callback (_: Prims.unit) : Prims.unit -> t_Error = - fun temp_0_ -> - let _:Prims.unit = temp_0_ in - Error_Fail <: t_Error - -let t_Error_cast_to_repr (x: t_Error) : isize = match x with | Error_Fail -> isz 0 - -type t_Struct = | Struct : t_Struct - class t_SuperTrait (v_Self: Type0) = { [@@@ FStar.Tactics.Typeclasses.no_method]_super_9442900250278684536:Core.Clone.t_Clone v_Self; f_function_of_super_trait_pre:v_Self -> Type0; @@ -567,6 +547,17 @@ let impl_SuperTrait_for_i32: t_SuperTrait i32 = f_function_of_super_trait = fun (self: i32) -> cast (Core.Num.impl__i32__abs self <: i32) <: u32 } +type t_Struct = | Struct : t_Struct + +class t_Bar (v_Self: Type0) = { + f_bar_pre:v_Self -> Type0; + f_bar_post:v_Self -> Prims.unit -> Type0; + f_bar:x0: v_Self -> Prims.Pure Prims.unit (f_bar_pre x0) (fun result -> f_bar_post x0 result) +} + +let impl_2__method (#v_T: Type0) (#[FStar.Tactics.Typeclasses.tcresolve ()] i1: t_Bar v_T) (x: v_T) + : Prims.unit = f_bar #v_T #FStar.Tactics.Typeclasses.solve x + let closure_impl_expr (#v_I: Type0) (#[FStar.Tactics.Typeclasses.tcresolve ()] i1: Core.Iter.Traits.Iterator.t_Iterator v_I) @@ -597,6 +588,15 @@ let closure_impl_expr_fngen <: Core.Iter.Adapters.Map.t_Map v_I v_F) +type t_Error = | Error_Fail : t_Error + +let t_Error_cast_to_repr (x: t_Error) : isize = match x with | Error_Fail -> isz 0 + +let impl__Error__for_application_callback (_: Prims.unit) : Prims.unit -> t_Error = + fun temp_0_ -> + let _:Prims.unit = temp_0_ in + Error_Fail <: t_Error + let iter_option (#v_T: Type0) (x: Core.Option.t_Option v_T) : Core.Option.t_IntoIter v_T = Core.Iter.Traits.Collect.f_into_iter #(Core.Option.t_Option v_T) #FStar.Tactics.Typeclasses.solve @@ -632,6 +632,13 @@ class t_Foo (v_Self: Type0) = { (fun result -> f_assoc_type_post #i3 x0 result) } +let f (#v_T: Type0) (#[FStar.Tactics.Typeclasses.tcresolve ()] i1: t_Foo v_T) (x: v_T) : Prims.unit = + let _:Prims.unit = f_assoc_f #v_T #FStar.Tactics.Typeclasses.solve () in + f_method_f #v_T #FStar.Tactics.Typeclasses.solve x + +let g (#v_T: Type0) (#[FStar.Tactics.Typeclasses.tcresolve ()] i1: t_Foo v_T) (x: i1.f_AssocType) + : u32 = f_function_of_super_trait #i1.f_AssocType #FStar.Tactics.Typeclasses.solve x + class t_Lang (v_Self: Type0) = { f_Var:Type0; f_s_pre:v_Self -> i32 -> Type0; @@ -640,13 +647,6 @@ class t_Lang (v_Self: Type0) = { -> Prims.Pure (v_Self & f_Var) (f_s_pre x0 x1) (fun result -> f_s_post x0 x1 result) } -let f (#v_T: Type0) (#[FStar.Tactics.Typeclasses.tcresolve ()] i1: t_Foo v_T) (x: v_T) : Prims.unit = - let _:Prims.unit = f_assoc_f #v_T #FStar.Tactics.Typeclasses.solve () in - f_method_f #v_T #FStar.Tactics.Typeclasses.solve x - -let g (#v_T: Type0) (#[FStar.Tactics.Typeclasses.tcresolve ()] i1: t_Foo v_T) (x: i1.f_AssocType) - : u32 = f_function_of_super_trait #i1.f_AssocType #FStar.Tactics.Typeclasses.solve x - [@@ FStar.Tactics.Typeclasses.tcinstance] let impl_Foo_for_tuple_: t_Foo Prims.unit = { diff --git a/test-harness/src/snapshots/toolchain__unsafe into-fstar.snap b/test-harness/src/snapshots/toolchain__unsafe into-fstar.snap index 310e2d094..2fba5a2b7 100644 --- a/test-harness/src/snapshots/toolchain__unsafe into-fstar.snap +++ b/test-harness/src/snapshots/toolchain__unsafe into-fstar.snap @@ -37,13 +37,13 @@ type t_Impossible = let t_Impossible_cast_to_repr (x: t_Impossible) : Rust_primitives.Hax.t_Never = match x with -let get_unchecked_example (slice: t_Slice u8) - : Prims.Pure u8 - (requires (Core.Slice.impl__len #u8 slice <: usize) >. sz 10) - (fun _ -> Prims.l_True) = Core.Slice.impl__get_unchecked #u8 #usize slice (sz 6) - let impossible (_: Prims.unit) : Prims.Pure t_Impossible (requires false) (fun _ -> Prims.l_True) = Rust_primitives.Hax.never_to_any (Core.Hint.unreachable_unchecked () <: Rust_primitives.Hax.t_Never) + +let get_unchecked_example (slice: t_Slice u8) + : Prims.Pure u8 + (requires (Core.Slice.impl__len #u8 slice <: usize) >. sz 10) + (fun _ -> Prims.l_True) = Core.Slice.impl__get_unchecked #u8 #usize slice (sz 6) ''' diff --git a/tests/reordering/src/lib.rs b/tests/reordering/src/lib.rs index 03e4d0ea8..2be238457 100644 --- a/tests/reordering/src/lib.rs +++ b/tests/reordering/src/lib.rs @@ -17,3 +17,28 @@ enum Foo { A, B, } + +mod no_alpha_sorting { + fn u01() {} + fn r02() {} + fn b03() {} + fn f04() {} + fn h05() {} + fn i06() {} + fn c07() {} + fn k08() {} + fn d09() {} + fn e10() {} + fn g11() {} + fn j12() {} + fn o13() {} + fn a14() {} + fn q15() {} + fn m16() {} + fn l17() {} + fn n18() {} + fn v19() {} + fn s20() {} + fn p21() {} + fn t22() {} +}