Merge branch 'main' into transparent-integers

engine/backends/coq/coq/coq_backend.ml

@@ -810,6 +810,7 @@ module TransformToInputLanguage =
   |> Phases.Reject.Dyn
   |> Phases.Reject.Trait_item_default
   |> Phases.Bundle_cycles
+  |> Phases.Sort_items
   |> SubtypeToInputLanguage
   |> Identity
   ]

engine/backends/coq/ssprove/ssprove_backend.ml

@@ -592,6 +592,7 @@ module TransformToInputLanguage (* : PHASE *) =
     |> Phases.Reject.Dyn
     |> Phases.Reject.Trait_item_default
     |> Phases.Bundle_cycles
+    |> Phases.Sort_items
     |> SubtypeToInputLanguage
     |> Identity
   ]

engine/backends/easycrypt/easycrypt_backend.ml

@@ -353,7 +353,7 @@ module TransformToInputLanguage =
   |> Phases.And_mut_defsite |> Phases.Reconstruct_asserts
   |> Phases.Reconstruct_for_loops |> Phases.Direct_and_mut |> Phases.Drop_blocks
   |> Phases.Reject.Continue |> Phases.Drop_references |> Phases.Bundle_cycles
-  |> RejectNotEC]
+  |> Phases.Sort_items |> RejectNotEC]
 
 let apply_phases (_bo : BackendOptions.t) (items : Ast.Rust.item list) :
     AST.item list =

engine/backends/fstar/fstar_backend.ml

@@ -1820,6 +1820,7 @@ module TransformToInputLanguage =
   |> Phases.Newtype_as_refinement
   |> Phases.Reject.Trait_item_default
   |> Phases.Bundle_cycles
+  |> Phases.Sort_items
   |> SubtypeToInputLanguage
   |> Identity
   ]

engine/backends/proverif/proverif_backend.ml

@@ -900,6 +900,7 @@ module TransformToInputLanguage =
   |> Phases.Reject.Continue
   |> Phases.Reject.Dyn
   |> Phases.Bundle_cycles
+  |> Phases.Sort_items
   |> SubtypeToInputLanguage
   |> Identity
   ]

engine/bin/lib.ml

@@ -75,7 +75,6 @@ let import_thir_items (include_clauses : Types.inclusion_clause list)
   in
   Hax_io.write
     (ItemProcessed (List.filter_map ~f:(fun i -> Span.owner_hint i.span) items));
-  let items = Deps.sort items in
   (* Extract error reports for the items we actually extract *)
   let reports =
     List.concat_map

engine/lib/ast_utils.ml

@@ -1285,22 +1285,25 @@ module Make (F : Features.T) = struct
     include U
     module Map = Map.M (U)
   end
-end
-
-module MakeWithNamePolicy (F : Features.T) (NP : Concrete_ident.NAME_POLICY) =
-struct
-  include Make (F)
-  open AST
-  module Concrete_ident_view = Concrete_ident.MakeViewAPI (NP)
 
-  let group_items_by_namespace (items : item list) : item list StringList.Map.t
-      =
+  let group_items_by_namespace_generic to_namespace (items : item list) :
+      item list StringList.Map.t =
     let h = Hashtbl.create (module StringList) in
     List.iter items ~f:(fun item ->
-        let ns = Concrete_ident_view.to_namespace item.ident in
+        let ns = to_namespace item.ident in
         let items = Hashtbl.find_or_add h ns ~default:(fun _ -> ref []) in
         items := !items @ [ item ]);
     Map.of_iteri_exn
       (module StringList)
       ~iteri:(Hashtbl.map h ~f:( ! ) |> Hashtbl.iteri)
 end
+
+module MakeWithNamePolicy (F : Features.T) (NP : Concrete_ident.NAME_POLICY) =
+struct
+  include Make (F)
+  open AST
+  module Concrete_ident_view = Concrete_ident.MakeViewAPI (NP)
+
+  let group_items_by_namespace : item list -> item list StringList.Map.t =
+    group_items_by_namespace_generic Concrete_ident_view.to_namespace
+end

engine/lib/attr_payloads.ml

@@ -154,6 +154,7 @@ module Make (F : Features.T) (Error : Phase_utils.ERROR) = struct
   (* TODO: Maybe rename me `graph` or something? *)
   module type WITH_ITEMS = sig
     val item_uid_map : item UId.Map.t
+    val try_item_of_uid : UId.t -> item option
     val item_of_uid : UId.t -> item
     val associated_items_per_roles : attrs -> item list AssocRole.Map.t
     val associated_item : AssocRole.t -> attrs -> item option
@@ -222,8 +223,10 @@ module Make (F : Features.T) (Error : Phase_utils.ERROR) = struct
       in
       map_of_alist (module UId) l ~dup
 
+    let try_item_of_uid (uid : UId.t) : item option = Map.find item_uid_map uid
+
     let item_of_uid (uid : UId.t) : item =
-      Map.find item_uid_map uid
+      try_item_of_uid uid
       |> Option.value_or_thunk ~default:(fun () ->
              Error.assertion_failure (Span.dummy ())
              @@ "Could not find item with UID "

engine/lib/concrete_ident/concrete_ident.ml

@@ -631,6 +631,18 @@ module Create = struct
     let path = List.drop_last_exn old.def_id.path @ [ last ] in
     { old with def_id = { old.def_id with path } }
 
+  let replace_last old chunk =
+    {
+      old with
+      def_id =
+        {
+          old.def_id with
+          path =
+            List.drop_last_exn old.def_id.path
+            @ [ { data = Imported.ValueNs chunk; disambiguator = 0 } ];
+        };
+    }
+
   let constructor name =
     let path = name.def_id.path @ [ { data = Ctor; disambiguator = 0 } ] in
     { name with def_id = { name.def_id with path } }

engine/lib/concrete_ident/concrete_ident.mli

@@ -39,6 +39,9 @@ module Create : sig
   (** [map_last f ident] applies [f] on the last chunk of [ident]'s
       path if it holds a string *)
 
+  val replace_last : t -> string -> t
+  (** [replace_last ident chunk] repalces the last chunk of [ident] by [chunk] *)
+
   val add_disambiguator : t -> int -> t
   (** [add_disambiguator ident d] changes the disambiguator on
       the last chunk of [ident]'s path to [d] *)

engine/lib/dependencies.ml

@@ -37,11 +37,19 @@ module Make (F : Features.T) = struct
     let open Attrs.WithItems (struct
       let items = items
     end) in
-    raw_associated_item >> List.map ~f:(snd >> item_of_uid)
+    raw_associated_item >> List.filter_map ~f:(snd >> try_item_of_uid)
 
   module ItemGraph = struct
     module G = Graph.Persistent.Digraph.Concrete (Concrete_ident)
-    module Topological = Graph.Topological.Make_stable (G)
+
+    module GInt = struct
+      include Graph.Persistent.Digraph.Concrete (Int)
+
+      let empty () = empty
+    end
+
+    module Topological = Graph.Topological.Make_stable (GInt)
+    module Map_G_GInt = Graph.Gmap.Edge (G) (GInt)
     module Oper = Graph.Oper.P (G)
 
     let vertices_of_item (i : item) : G.V.t list =
@@ -212,6 +220,10 @@ module Make (F : Features.T) = struct
 
     let of_items (items : item list) : G.t =
       let ig = ItemGraph.of_items ~original_items:items items in
+      let vertices =
+        List.fold items ~init:G.empty ~f:(fun g item ->
+            G.add_vertex g (Namespace.of_concrete_ident item.ident))
+      in
       List.map ~f:(ident_of >> (Namespace.of_concrete_ident &&& Fn.id)) items
       |> Map.of_alist_multi (module Namespace)
       |> Map.map
@@ -224,13 +236,18 @@ module Make (F : Features.T) = struct
              >> 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)
+      |> List.fold ~init:vertices ~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))
 
+    (** Returns the namespaces in topological order *)
+    let order g : Namespace.t list =
+      let module ModTopo = Graph.Topological.Make_stable (G) in
+      ModTopo.fold List.cons g []
+
     open Graph.Graphviz.Dot (struct
       include G
 
@@ -270,13 +287,81 @@ module Make (F : Features.T) = struct
     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
+    let stable_g =
+      let to_index =
+        items
+        |> List.mapi ~f:(fun i item -> (item.ident, i))
+        |> Map.of_alist_exn (module Concrete_ident)
+        |> Map.find
+      in
+      ItemGraph.Map_G_GInt.filter_map
+        (to_index *** to_index >> uncurry Option.both)
+        g
+    in
+    let stable_g =
+      List.foldi items ~init:stable_g ~f:(fun i g _ ->
+          ItemGraph.GInt.add_vertex g i)
+    in
+    let items' =
+      let items_array = Array.of_list items in
+      let lookup (index : int) = items_array.(index) in
+      ItemGraph.Topological.fold List.cons stable_g [] |> List.map ~f:lookup
     in
+    (* Stable topological sort doesn't guarantee to group cycles together.
+       We make this correction to ensure mutually recursive items are grouped. *)
     let items' =
-      ItemGraph.Topological.fold List.cons g []
-      |> List.filter_map ~f:lookup |> List.rev
+      let cycles =
+        ItemGraph.MutRec.SCC.scc_list g
+        |> List.filter ~f:(fun cycle -> List.length cycle > 1)
+      in
+      (* TODO: This can be optimized by using a set or a map
+         to avoid traversing all cycles at each iteration. *)
+      List.fold items' ~init:[] ~f:(fun acc item ->
+          match
+            List.find cycles ~f:(fun cycle ->
+                List.mem cycle item.ident ~equal:[%eq: concrete_ident])
+          with
+          | Some _
+            when List.exists acc ~f:(fun els ->
+                     List.mem els item ~equal:[%eq: item]) ->
+              [] :: acc
+          | Some cycle ->
+              List.map cycle ~f:(fun ident ->
+                  List.find_exn items ~f:(fun item ->
+                      [%eq: concrete_ident] item.ident ident))
+              :: acc
+          | None -> [ item ] :: acc)
+      |> List.concat
+    in
+    (* Quote items must be placed right before or after their origin *)
+    let items' =
+      let before_quotes, after_quotes, _ =
+        List.partition3_map items' ~f:(fun item ->
+            match item.v with
+            | Quote { origin; _ } -> (
+                match origin.position with
+                | `Before -> `Fst (origin, item)
+                | `After -> `Snd (origin, item)
+                | `Replace -> `Trd ())
+            | _ -> `Trd ())
+      in
+      let move_quote before origin quote_item =
+        List.concat_map ~f:(fun item ->
+            if [%eq: concrete_ident] origin.item_ident item.ident then
+              if before then [ quote_item; item ] else [ item; quote_item ]
+            else if [%eq: concrete_ident] quote_item.ident item.ident then []
+            else [ item ])
+      in
+      let before_quotes = List.rev before_quotes in
+      let items' =
+        List.fold before_quotes ~init:items'
+          ~f:(fun items' (origin, quote_item) ->
+            move_quote true origin quote_item items')
+      in
+      List.fold after_quotes ~init:items' ~f:(fun items' (origin, quote_item) ->
+          move_quote false origin quote_item items')
     in
+
     assert (
       let of_list =
         List.map ~f:ident_of >> Set.of_list (module Concrete_ident)
@@ -286,6 +371,22 @@ module Make (F : Features.T) = struct
       Set.equal items items');
     items'
 
+  let global_sort (items : item list) : item list =
+    let sorted_by_namespace =
+      U.group_items_by_namespace_generic
+        Concrete_ident.DefaultViewAPI.to_namespace items
+      |> Map.data
+      |> List.map ~f:(fun items -> sort items)
+    in
+    let sorted_namespaces = ModGraph.order (ModGraph.of_items items) in
+    List.concat_map sorted_namespaces ~f:(fun namespace ->
+        List.find sorted_by_namespace ~f:(fun items ->
+            List.exists items ~f:(fun item ->
+                Namespace.equal
+                  (Namespace.of_concrete_ident item.ident)
+                  namespace))
+        |> Option.value ~default:[])
+
   let filter_by_inclusion_clauses' ~original_items
       (clauses : Types.inclusion_clause list) (items : item list) :
       item list * Concrete_ident.t Hash_set.t =
@@ -388,7 +489,12 @@ module Make (F : Features.T) = struct
             List.filter ~f:(fun att -> Attrs.late_skip [ att ]) item.attrs
           in
 
-          { item with v = Alias { name = old_ident; item = new_ident }; attrs })
+          {
+            item with
+            v = Alias { name = old_ident; item = new_ident };
+            attrs;
+            ident = old_ident;
+          })
     in
     item' :: aliases
 

engine/lib/dependencies.mli

@@ -3,7 +3,7 @@ module Make (F : Features.T) : sig
 
   val uid_associated_items : AST.item list -> Ast.attrs -> AST.item list
   val bundle_cyclic_modules : AST.item list -> AST.item list
-  val sort : AST.item list -> AST.item list
+  val global_sort : AST.item list -> AST.item list
   val recursive_bundles : AST.item list -> AST.item list list * AST.item list
 
   val filter_by_inclusion_clauses :

engine/lib/phases/phase_sort_items.ml

@@ -0,0 +1,20 @@
+open! Prelude
+
+module Make (F : Features.T) =
+  Phase_utils.MakeMonomorphicPhase
+    (F)
+    (struct
+      let phase_id = [%auto_phase_name auto]
+
+      module A = Ast.Make (F)
+
+      module Error = Phase_utils.MakeError (struct
+        let ctx = Diagnostics.Context.Phase phase_id
+      end)
+
+      module Attrs = Attr_payloads.MakeBase (Error)
+
+      let ditems items =
+        let module Deps = Dependencies.Make (F) in
+        Deps.global_sort items
+    end)

engine/lib/phases/phase_sort_items.mli

@@ -0,0 +1,6 @@
+(** This phase sorts items so that each item comes after the items it depends on.
+    This is done by sorting namespaces with the same property, and then sorting 
+    items within each namespace, trying as much as possible to respect the 
+    original order. *)
+
+module Make : Phase_utils.UNCONSTRAINTED_MONOMORPHIC_PHASE

engine/lib/phases/phase_transform_hax_lib_inline.ml

@@ -71,6 +71,8 @@ module%inlined_contents Make (F : Features.T) = struct
     let first_global_ident (pat : B.pat) : global_ident option =
       UB.Reducers.collect_global_idents#visit_pat () pat |> Set.choose
 
+    let counter = ref 0
+
     let rec dexpr' span (expr : A.expr') : B.expr' =
       quote_of_expr' span expr
       |> Option.map ~f:(fun quote : B.expr' -> B.Quote quote)
@@ -206,7 +208,18 @@ module%inlined_contents Make (F : Features.T) = struct
                      Quote { quote; origin }
                    in
                    let attrs = [ Attr_payloads.to_attr attr assoc_item.span ] in
-                   (B.{ v; span; ident = item.ident; attrs }, position))
+                   counter := !counter + 1;
+                   ( B.
+                       {
+                         v;
+                         span;
+                         ident =
+                           (* TODO: Replace with a proper unique ident. *)
+                           Concrete_ident.Create.replace_last item.ident
+                             ("__hax_quote__" ^ Int.to_string !counter);
+                         attrs;
+                       },
+                     position ))
             |> List.partition_tf ~f:(snd >> [%matches? Types.Before])
             |> map_fst *** map_fst
           with Diagnostics.SpanFreeError.Exn (Data (context, kind)) ->

examples/kyber_compress/proofs/fstar/extraction/Makefile

@@ -53,7 +53,7 @@ all:
 	rm -f .depend && $(MAKE) .depend
 	$(MAKE) verify
 
-HAX_CLI = "cargo hax into fstar --z3rlimit 200"
+HAX_CLI = "cargo hax into fstar --z3rlimit 500"
 
 # If $HACL_HOME doesn't exist, clone it
 ${HACL_HOME}:
@@ -114,6 +114,7 @@ FSTAR_FLAGS = --cmi \
   --warn_error -331 \
   --cache_checked_modules --cache_dir $(CACHE_DIR) \
   --already_cached "+Prims+FStar+LowStar+C+Spec.Loops+TestLib" \
+  --ext context_pruning \
   $(addprefix --include ,$(FSTAR_INCLUDE_DIRS))
 
 FSTAR = $(FSTAR_BIN) $(FSTAR_FLAGS)