Merge remote-tracking branch 'origin/main' into son/features

.github/workflows/ci.yml

@@ -39,18 +39,14 @@ jobs:
       - run: nix build -L .#checks.x86_64-linux.aeneas-check-tidiness
       - run: nix build -L .#checks.x86_64-linux.check-charon-pin
       - run: nix build -L .#aeneas
-      - run: nix build -L .#checks.x86_64-linux.aeneas-tests
-      - run: nix build -L .#checks.x86_64-linux.aeneas-verify-fstar
-      - run: nix build -L .#checks.x86_64-linux.aeneas-verify-coq
-      - run: nix build -L .#checks.x86_64-linux.aeneas-verify-hol4
-      # Lean cannot run its tests in the sandbox because `elan` will download things
-      #- run: nix build -L .#checks.x86_64-linux.aeneas-verify-lean
+      - run: nix build -L .#checks.x86_64-linux.default
 
   lean:
     runs-on: [self-hosted, linux, nix]
     needs: check_if_skip_duplicate_job
     if: needs.check_if_skip_duplicate_job.outputs.should_skip != 'true'
     steps:
+      # Lean cannot run its tests in the sandbox because `elan` will download things
       - uses: actions/checkout@v4
       - run: nix develop --command bash -c "cd tests/lean && make"
 

flake.nix

@@ -7,18 +7,17 @@
     charon.url = "github:aeneasverif/charon";
     flake-utils.follows = "charon/flake-utils";
     nixpkgs.follows = "charon/nixpkgs";
-    hacl-nix.url = "github:hacl-star/hacl-nix";
+    fstar.url = "github:FStarLang/fstar";
     flake-compat.url = "github:nix-community/flake-compat";
   };
 
   # Remark: keep the list of outputs in sync with the list of inputs above
   # (see above remark)
-  outputs = { self, charon, flake-utils, nixpkgs, hacl-nix, flake-compat }:
+  outputs = { self, charon, flake-utils, nixpkgs, fstar, ... }:
     flake-utils.lib.eachDefaultSystem (system:
       let
         pkgs = import nixpkgs { inherit system; };
         ocamlPackages = pkgs.ocamlPackages;
-        coqPackages = pkgs.coqPackages;
         easy_logging = ocamlPackages.buildDunePackage rec {
           pname = "easy_logging";
           version = "0.8.2";
@@ -153,7 +152,7 @@
         aeneas-verify-fstar = pkgs.stdenv.mkDerivation {
           name = "aeneas_verify_fstar";
           src = ./tests/fstar;
-          FSTAR_EXE = "${hacl-nix.packages.${system}.fstar}/bin/fstar.exe";
+          FSTAR_EXE = "${fstar.packages.${system}.fstar}/bin/fstar.exe";
           buildPhase = ''
             make prepare-projects
             make verify -j $NIX_BUILD_CORES
@@ -199,6 +198,14 @@
           installPhase = "touch $out";
         };
 
+        aeneas-checks = pkgs.runCommand "aeneas-checks" { } ''
+          echo ${aeneas-tests}
+          echo ${aeneas-verify-coq}
+          echo ${aeneas-verify-fstar}
+          echo ${aeneas-verify-hol4}
+          touch $out
+        '';
+
         check-charon-pin = pkgs.runCommand "aeneas-check-charon-pin"
           {
             buildInputs = [ pkgs.jq ];
@@ -241,12 +248,8 @@
           ];
         };
         checks = {
-          inherit aeneas aeneas-tests
-            aeneas-verify-fstar
-            aeneas-verify-coq
-            aeneas-verify-hol4
-            aeneas-check-tidiness
-            check-charon-pin;
+          default = aeneas-checks;
+          inherit aeneas-check-tidiness check-charon-pin;
         };
       });
 }

src/interp/Interpreter.ml

@@ -125,96 +125,11 @@ let normalize_inst_fun_sig (span : Meta.span) (ctx : eval_ctx)
     normalize because a trait clause was instantiated with a specific trait ref).
  *)
 let symbolic_instantiate_fun_sig (span : Meta.span) (ctx : eval_ctx)
-    (sg : fun_sig) (regions_hierarchy : region_var_groups) (kind : item_kind) :
+    (sg : fun_sig) (regions_hierarchy : region_var_groups) (_kind : item_kind) :
     eval_ctx * inst_fun_sig =
-  let tr_self =
-    match kind with
-    | RegularItem | TraitImplItem _ -> UnknownTrait __FUNCTION__
-    | TraitDeclItem _ -> Self
-  in
+  let tr_self = Self in
   let generics =
-    let { regions; types; const_generics; trait_clauses; _ } = sg.generics in
-    let regions = List.map (fun _ -> RErased) regions in
-    let types = List.map (fun (v : type_var) -> TVar v.index) types in
-    let const_generics =
-      List.map (fun (v : const_generic_var) -> CgVar v.index) const_generics
-    in
-    (* Annoying that we have to generate this substitution here *)
-    let r_subst _ = craise __FILE__ __LINE__ span "Unexpected region" in
-    let ty_subst =
-      Substitute.make_type_subst_from_vars sg.generics.types types
-    in
-    let cg_subst =
-      Substitute.make_const_generic_subst_from_vars sg.generics.const_generics
-        const_generics
-    in
-    (* TODO: some clauses may use the types of other clauses, so we may have to
-       reorder them.
-
-       Example:
-       If in Rust we write:
-       {[
-         pub fn use_get<'a, T: Get>(x: &'a mut T) -> u32
-         where
-             T::Item: ToU32,
-         {
-             x.get().to_u32()
-         }
-       ]}
-
-       In LLBC we get:
-       {[
-         fn demo::use_get<'a, T>(@1: &'a mut (T)) -> u32
-         where
-             [@TraitClause0]: demo::Get<T>,
-             [@TraitClause1]: demo::ToU32<@TraitClause0::Item>, // HERE
-         {
-             ... // Omitted
-         }
-       ]}
-    *)
-    (* We will need to update the trait refs map while we perform the instantiations *)
-    let mk_tr_subst (tr_map : trait_instance_id TraitClauseId.Map.t) clause_id :
-        trait_instance_id =
-      match TraitClauseId.Map.find_opt clause_id tr_map with
-      | Some tr -> tr
-      | None -> craise __FILE__ __LINE__ span "Local trait clause not found"
-    in
-    let mk_subst tr_map =
-      let tr_subst = mk_tr_subst tr_map in
-      { Substitute.r_subst; ty_subst; cg_subst; tr_subst; tr_self }
-    in
-    let _, trait_refs =
-      List.fold_left_map
-        (fun tr_map (c : trait_clause) ->
-          let subst = mk_subst tr_map in
-          (* *)
-          sanity_check __FILE__ __LINE__ (c.trait.binder_regions = []) span;
-          let { trait_decl_id; decl_generics; _ } = c.trait.binder_value in
-          let generics =
-            Substitute.generic_args_substitute subst decl_generics
-          in
-          let trait_decl_ref = { trait_decl_id; decl_generics = generics } in
-          (* Note that because we directly refer to the clause, we give it
-             empty generics *)
-          let trait_id = Clause c.clause_id in
-          let trait_ref =
-            {
-              trait_id;
-              trait_decl_ref =
-                {
-                  (* Empty list of bound regions: we don't support the other cases for now *)
-                  binder_regions = [];
-                  binder_value = trait_decl_ref;
-                };
-            }
-          in
-          (* Update the traits map *)
-          let tr_map = TraitClauseId.Map.add c.clause_id trait_id tr_map in
-          (tr_map, trait_ref))
-        TraitClauseId.Map.empty trait_clauses
-    in
-    { regions; types; const_generics; trait_refs }
+    Substitute.generic_args_of_params_erase_regions (Some span) sg.generics
   in
   let inst_sg =
     instantiate_fun_sig span ctx generics tr_self sg regions_hierarchy

src/llbc/Builtin.ml

@@ -126,15 +126,15 @@ module Sig = struct
       borrow.
    *)
   let mk_array_slice_borrow_sig (cgs : const_generic_var list)
-      (input_ty : TypeVarId.id -> ty) (index_ty : ty option)
-      (output_ty : TypeVarId.id -> ty) (is_mut : bool) : fun_sig =
+      (input_ty : ty -> ty) (index_ty : ty option) (output_ty : ty -> ty)
+      (is_mut : bool) : fun_sig =
     let generics =
       mk_generic_params [ region_param_0 ] [ type_param_0 ] cgs (* <'a, T> *)
     in
     let inputs =
       [
         mk_ref_ty rvar_0
-          (input_ty type_param_0.index)
+          (input_ty (TVar type_param_0.index))
           is_mut (* &'a (mut) input_ty<T> *);
       ]
     in
@@ -146,20 +146,20 @@ module Sig = struct
     in
     let output =
       mk_ref_ty rvar_0
-        (output_ty type_param_0.index)
+        (output_ty (TVar type_param_0.index))
         is_mut (* &'a (mut) output_ty<T> *)
     in
     mk_sig generics inputs output
 
   let mk_array_slice_index_sig (is_array : bool) (is_mut : bool) : fun_sig =
     (* Array<T, N> *)
-    let input_ty id =
-      if is_array then mk_array_ty (TVar id) cgvar_0 else mk_slice_ty (TVar id)
+    let input_ty ty =
+      if is_array then mk_array_ty ty cgvar_0 else mk_slice_ty ty
     in
     (* usize *)
     let index_ty = usize_ty in
     (* T *)
-    let output_ty id = TVar id in
+    let output_ty ty = ty in
     let cgs = if is_array then [ cg_param_0 ] else [] in
     mk_array_slice_borrow_sig cgs input_ty (Some index_ty) output_ty is_mut
 
@@ -168,9 +168,9 @@ module Sig = struct
 
   let array_to_slice_sig (is_mut : bool) : fun_sig =
     (* Array<T, N> *)
-    let input_ty id = mk_array_ty (TVar id) cgvar_0 in
+    let input_ty ty = mk_array_ty ty cgvar_0 in
     (* Slice<T> *)
-    let output_ty id = mk_slice_ty (TVar id) in
+    let output_ty ty = mk_slice_ty ty in
     let cgs = [ cg_param_0 ] in
     mk_array_slice_borrow_sig cgs input_ty None output_ty is_mut