From cb097c2002f65e185d0518bf5559db2ed841436d Mon Sep 17 00:00:00 2001
From: Lucas Franceschino <lucas@cryspen.com>
Date: Mon, 4 Mar 2024 15:52:05 +0100
Subject: [PATCH 01/24] feat(engine/attrs): introduce `to_attr`

---
 engine/lib/attr_payloads.ml | 11 +++++++++++
 1 file changed, 11 insertions(+)

diff --git a/engine/lib/attr_payloads.ml b/engine/lib/attr_payloads.ml
index e1e308346..3e00f7b61 100644
--- a/engine/lib/attr_payloads.ml
+++ b/engine/lib/attr_payloads.ml
@@ -1,6 +1,7 @@
 open! Prelude
 open Ast
 
+(** Parse [_hax::json] attributes *)
 let payloads : attrs -> (Types.ha_payload * span) list =
   let parse =
     (* we have to parse ["JSON"]: first a string, then a ha_payload *)
@@ -19,6 +20,16 @@ let payloads : attrs -> (Types.ha_payload * span) list =
       | _ -> None)
   >> List.map ~f:(map_fst (Yojson.Safe.from_string >> parse))
 
+(** Create a attribute out of a [payload] *)
+let to_attr (payload : Types.ha_payload) (span : span) : attr =
+  let json =
+    `String (Yojson.Safe.to_string (Types.to_json_ha_payload payload))
+  in
+  let kind : attr_kind =
+    Tool { path = "_hax::json"; tokens = Yojson.Safe.to_string json }
+  in
+  { kind; span }
+
 module UId = struct
   module T = struct
     type t = UId of string [@@deriving show, yojson, compare, sexp, eq]

From af309f5183fe074b28a450c188b33fcba40c634c Mon Sep 17 00:00:00 2001
From: Lucas Franceschino <lucas@cryspen.com>
Date: Mon, 4 Mar 2024 15:53:50 +0100
Subject: [PATCH 02/24] feat(backend/fstar): FStarBinder: `of_typ` & `to_term`

---
 engine/backends/fstar/fstar_backend.ml | 7 +++++++
 1 file changed, 7 insertions(+)

diff --git a/engine/backends/fstar/fstar_backend.ml b/engine/backends/fstar/fstar_backend.ml
index 2ac772572..e5b816f49 100644
--- a/engine/backends/fstar/fstar_backend.ml
+++ b/engine/backends/fstar/fstar_backend.ml
@@ -578,6 +578,10 @@ struct
       List.map ~f:(of_generic_param ~kind span) generics.params
       @ List.mapi ~f:(of_generic_constraint span) generics.constraints
 
+    let of_typ span (nth : int) typ : t =
+      let ident = F.id ("x" ^ Int.to_string nth) in
+      { kind = Explicit; ident; typ = pty span typ }
+
     let to_pattern (x : t) : F.AST.pattern =
       let subpat =
         match x.kind with
@@ -599,6 +603,9 @@ struct
     let to_typ (x : t) : F.AST.term = x.typ
     let to_ident (x : t) : F.Ident.ident = x.ident
 
+    let to_term (x : t) : F.AST.term =
+      F.term @@ F.AST.Var (FStar_Ident.lid_of_ns_and_id [] (to_ident x))
+
     let to_binder (x : t) : F.AST.binder =
       F.AST.
         {

From 84b8d0379a8e17974625eeabb7f63926592a3be2 Mon Sep 17 00:00:00 2001
From: Lucas Franceschino <lucas@cryspen.com>
Date: Mon, 4 Mar 2024 15:54:37 +0100
Subject: [PATCH 03/24] feat(engine): concrete idents: intro. `map_last`

---
 engine/lib/concrete_ident/concrete_ident.ml  | 29 ++++++++++++++------
 engine/lib/concrete_ident/concrete_ident.mli |  4 +++
 2 files changed, 25 insertions(+), 8 deletions(-)

diff --git a/engine/lib/concrete_ident/concrete_ident.ml b/engine/lib/concrete_ident/concrete_ident.ml
index fecef6406..14e8ed1a4 100644
--- a/engine/lib/concrete_ident/concrete_ident.ml
+++ b/engine/lib/concrete_ident/concrete_ident.ml
@@ -64,15 +64,20 @@ module Imported = struct
         | _ -> path);
     }
 
+  let map_def_path_item_string ~(f : string -> string) :
+      def_path_item -> def_path_item = function
+    | TypeNs s -> TypeNs (f s)
+    | ValueNs s -> ValueNs (f s)
+    | MacroNs s -> MacroNs (f s)
+    | LifetimeNs s -> LifetimeNs (f s)
+    | other -> other
+
+  let map_disambiguated_def_path_item_string ~(f : string -> string)
+      (x : disambiguated_def_path_item) : disambiguated_def_path_item =
+    { x with data = map_def_path_item_string ~f x.data }
+
   let map_path_strings ~(f : string -> string) (did : def_id) : def_id =
-    let f : def_path_item -> def_path_item = function
-      | TypeNs s -> TypeNs (f s)
-      | ValueNs s -> ValueNs (f s)
-      | MacroNs s -> MacroNs (f s)
-      | LifetimeNs s -> LifetimeNs (f s)
-      | other -> other
-    in
-    let f x = { x with data = f x.data } in
+    let f = map_disambiguated_def_path_item_string ~f in
     { did with path = List.map ~f did.path }
 
   module AssociatedItem : sig
@@ -595,6 +600,14 @@ module Create = struct
           path = new_parent.path @ [ List.last_exn old.def_id.path ];
         };
     }
+
+  let map_last ~f old =
+    let last =
+      List.last_exn old.def_id.path
+      |> Imported.map_disambiguated_def_path_item_string ~f
+    in
+    let path = List.drop_last_exn old.def_id.path @ [ last ] in
+    { old with def_id = { old.def_id with path } }
 end
 
 let lookup_raw_impl_info (impl : t) : Types.impl_infos option =
diff --git a/engine/lib/concrete_ident/concrete_ident.mli b/engine/lib/concrete_ident/concrete_ident.mli
index b4abcd70a..1160da3be 100644
--- a/engine/lib/concrete_ident/concrete_ident.mli
+++ b/engine/lib/concrete_ident/concrete_ident.mli
@@ -27,6 +27,10 @@ val to_debug_string : t -> string
 module Create : sig
   val fresh_module : from:t list -> t
   val move_under : new_parent:t -> t -> t
+
+  val map_last : f:(string -> string) -> t -> t
+  (** [map_last f ident] applies [f] on the last chunk of [ident]'s
+      path if it holds a string *)
 end
 
 type view = { crate : string; path : string list; definition : string }

From fa2c4f1813ffe5c6037eab954ce1542d4b947614 Mon Sep 17 00:00:00 2001
From: Lucas Franceschino <lucas@cryspen.com>
Date: Mon, 4 Mar 2024 15:55:21 +0100
Subject: [PATCH 04/24] fix(engine/phase-utils): remove stale item

---
 engine/lib/phase_utils.ml | 1 -
 1 file changed, 1 deletion(-)

diff --git a/engine/lib/phase_utils.ml b/engine/lib/phase_utils.ml
index 95addb55f..b052e17ae 100644
--- a/engine/lib/phase_utils.ml
+++ b/engine/lib/phase_utils.ml
@@ -37,7 +37,6 @@ module MakePhaseImplemT (A : Ast.T) (B : Ast.T) = struct
   module type T = sig
     val metadata : Metadata.t
     val ditems : A.item list -> B.item list
-    val dexpr : A.expr -> B.expr
   end
 end
 

From f76b2f73c47134ac04df079cd1336fb840dcd8ca Mon Sep 17 00:00:00 2001
From: Lucas Franceschino <lucas@cryspen.com>
Date: Mon, 4 Mar 2024 15:59:07 +0100
Subject: [PATCH 05/24] feat(engine/ast-utils): introduce utils for monomorphic
 phases

---
 engine/lib/phase_utils.ml | 55 +++++++++++++++++++++++++++++++++++++++
 1 file changed, 55 insertions(+)

diff --git a/engine/lib/phase_utils.ml b/engine/lib/phase_utils.ml
index b052e17ae..80eb807df 100644
--- a/engine/lib/phase_utils.ml
+++ b/engine/lib/phase_utils.ml
@@ -40,6 +40,61 @@ module MakePhaseImplemT (A : Ast.T) (B : Ast.T) = struct
   end
 end
 
+(** Functor that produces module types of monomorphic phases *)
+module MAKE_MONOMORPHIC_PHASE (F : Features.T) = struct
+  module type ARG = sig
+    val phase_id : Diagnostics.Phase.t
+    val ditems : Ast.Make(F).item list -> Ast.Make(F).item list
+  end
+
+  module type T = sig
+    include module type of struct
+      module FB = F
+      module A = Ast.Make (F)
+      module B = Ast.Make (FB)
+      module ImplemT = MakePhaseImplemT (A) (B)
+      module FA = F
+    end
+
+    include ImplemT.T
+  end
+end
+
+(** Make a monomorphic phase: a phase that transform an AST with
+feature set [F] into an AST with the same feature set [F] *)
+module MakeMonomorphicPhase (F : Features.T) (M : MAKE_MONOMORPHIC_PHASE(F).ARG) :
+  MAKE_MONOMORPHIC_PHASE(F).T = struct
+  module FA = F
+  module FB = F
+  module A = Ast.Make (F)
+  module B = Ast.Make (FB)
+  module ImplemT = MakePhaseImplemT (A) (B)
+
+  module Implem = struct
+    let metadata = Metadata.make M.phase_id
+
+    include M
+
+    let subtype (l : A.item list) : B.item list = Stdlib.Obj.magic l
+    let ditems (l : A.item list) : B.item list = ditems l |> subtype
+  end
+
+  include Implem
+end
+
+(** Type of an unconstrainted (forall feature sets) monomorphic phases *)
+module type UNCONSTRAINTED_MONOMORPHIC_PHASE = functor (F : Features.T) -> sig
+  include module type of struct
+    module FB = F
+    module A = Ast.Make (F)
+    module B = Ast.Make (FB)
+    module ImplemT = MakePhaseImplemT (A) (B)
+    module FA = F
+  end
+
+  include ImplemT.T
+end
+
 exception ReportError of Diagnostics.kind
 
 module type ERROR = sig

From 0794804ba6d4b8b2777a34e90e435aadfe990926 Mon Sep 17 00:00:00 2001
From: Lucas Franceschino <lucas@cryspen.com>
Date: Mon, 4 Mar 2024 16:00:56 +0100
Subject: [PATCH 06/24] feat(engine/phases): add `traits_specs` phase

---
 engine/lib/phases.ml                     |   1 +
 engine/lib/phases/phase_traits_specs.ml  | 126 +++++++++++++++++++++++
 engine/lib/phases/phase_traits_specs.mli |   4 +
 hax-lib-macros/types/src/lib.rs          |   1 +
 4 files changed, 132 insertions(+)
 create mode 100644 engine/lib/phases/phase_traits_specs.ml
 create mode 100644 engine/lib/phases/phase_traits_specs.mli

diff --git a/engine/lib/phases.ml b/engine/lib/phases.ml
index 21fa02b62..74ecc879d 100644
--- a/engine/lib/phases.ml
+++ b/engine/lib/phases.ml
@@ -10,3 +10,4 @@ module Cf_into_monads = Phase_cf_into_monads.Make
 module Functionalize_loops = Phase_functionalize_loops.Make
 module Reject = Phase_reject
 module Local_mutation = Phase_local_mutation.Make
+module Traits_specs = Phase_traits_specs.Make
diff --git a/engine/lib/phases/phase_traits_specs.ml b/engine/lib/phases/phase_traits_specs.ml
new file mode 100644
index 000000000..f9d4a74d9
--- /dev/null
+++ b/engine/lib/phases/phase_traits_specs.ml
@@ -0,0 +1,126 @@
+open! Prelude
+
+module Make (F : Features.T) =
+  Phase_utils.MakeMonomorphicPhase
+    (F)
+    (struct
+      let phase_id = Diagnostics.Phase.DummyA
+
+      module A = Ast.Make (F)
+      module FB = F
+      module B = Ast.Make (F)
+      module U = Ast_utils.Make (F)
+      module BVisitors = Ast_visitors.Make (F)
+      open A
+
+      module Error = Phase_utils.MakeError (struct
+        let ctx = Diagnostics.Context.Phase phase_id
+      end)
+
+      let mk_name ident (kind : string) =
+        Concrete_ident.Create.map_last ~f:(fun s -> s ^ "_" ^ kind) ident
+
+      module Attrs = Attr_payloads.Make (F) (Error)
+
+      let ditems (l : A.item list) : B.item list =
+        let (module Attrs) = Attrs.with_items l in
+        let f (item : item) : item =
+          let v =
+            match item.v with
+            | Trait { name; generics; items } ->
+                let f (item : trait_item) =
+                  let mk kind =
+                    let ti_ident = mk_name item.ti_ident kind in
+                    {
+                      item with
+                      ti_ident;
+                      ti_attrs =
+                        [
+                          Attr_payloads.to_attr TraitMethodNoPrePost
+                            item.ti_span;
+                        ];
+                    }
+                  in
+                  match item.ti_v with
+                  | TIFn (TArrow (inputs, output)) ->
+                      [
+                        { (mk "pre") with ti_v = TIFn (TArrow (inputs, TBool)) };
+                        {
+                          (mk "post") with
+                          ti_v = TIFn (TArrow (inputs @ [ output ], TBool));
+                        };
+                      ]
+                  | TIFn _ -> [ (* REFINEMENTS FOR CONSTANTS? *) ]
+                  | TIType _ -> [ (* TODO REFINEMENTS FOR TYPES *) ]
+                in
+                let items =
+                  List.concat_map ~f:(fun item -> f item @ [ item ]) items
+                in
+                Trait { name; generics; items }
+            | Impl { generics; self_ty; of_trait; items } ->
+                let f (item : impl_item) =
+                  let mk kind =
+                    let ii_ident = mk_name item.ii_ident kind in
+                    { item with ii_ident }
+                  in
+                  let default =
+                    {
+                      e = Literal (Bool true);
+                      span = item.ii_span;
+                      typ = TBool;
+                    }
+                  in
+                  match item.ii_v with
+                  | IIFn { params = []; _ } -> []
+                  | IIFn { body; params } ->
+                      let out_ident =
+                        U.fresh_local_ident_in
+                          (U.Reducers.collect_local_idents#visit_impl_item ()
+                             item
+                          |> Set.to_list)
+                          "out"
+                      in
+                      let out =
+                        {
+                          pat = U.make_var_pat out_ident body.typ body.span;
+                          typ = body.typ;
+                          typ_span = None;
+                          attrs = [];
+                        }
+                      in
+                      [
+                        {
+                          (mk "pre") with
+                          ii_v =
+                            IIFn
+                              {
+                                body =
+                                  Attrs.associated_expr Requires item.ii_attrs
+                                  |> Option.value ~default;
+                                params;
+                              };
+                        };
+                        {
+                          (mk "post") with
+                          ii_v =
+                            IIFn
+                              {
+                                body =
+                                  Attrs.associated_expr Ensures item.ii_attrs
+                                  |> Option.value ~default;
+                                params = params @ [ out ];
+                              };
+                        };
+                      ]
+                  | IIType _ -> []
+                in
+                let items =
+                  List.concat_map ~f:(fun item -> f item @ [ item ]) items
+                in
+                Impl { generics; self_ty; of_trait; items }
+            | v -> v
+          in
+          { item with v }
+        in
+        List.map ~f l
+    end)
diff --git a/engine/lib/phases/phase_traits_specs.mli b/engine/lib/phases/phase_traits_specs.mli
new file mode 100644
index 000000000..ba77c15ab
--- /dev/null
+++ b/engine/lib/phases/phase_traits_specs.mli
@@ -0,0 +1,4 @@
+(** This phase adds specification to traits. For each method `f` in a
+trait, we add a `f_pre` and a `f_post`. *)
+
+module Make : Phase_utils.UNCONSTRAINTED_MONOMORPHIC_PHASE
diff --git a/hax-lib-macros/types/src/lib.rs b/hax-lib-macros/types/src/lib.rs
index f7fd1d5e7..9422f8b16 100644
--- a/hax-lib-macros/types/src/lib.rs
+++ b/hax-lib-macros/types/src/lib.rs
@@ -75,6 +75,7 @@ pub enum AttrPayload {
     ProcessWrite,
     ProcessInit,
     ProtocolMessages,
+    TraitMethodNoPrePost,
     /// Make a type opaque
     OpaqueType,
 }

From 04d941eb872f9628d2991cfcc1e95f965f71270a Mon Sep 17 00:00:00 2001
From: Lucas Franceschino <lucas@cryspen.com>
Date: Mon, 4 Mar 2024 16:01:59 +0100
Subject: [PATCH 07/24] feat(backends/fstar): pre/post for traits

---
 engine/backends/fstar/fstar_backend.ml | 34 ++++++++++++++++++++++++++
 1 file changed, 34 insertions(+)

diff --git a/engine/backends/fstar/fstar_backend.ml b/engine/backends/fstar/fstar_backend.ml
index e5b816f49..ab781777e 100644
--- a/engine/backends/fstar/fstar_backend.ml
+++ b/engine/backends/fstar/fstar_backend.ml
@@ -1081,6 +1081,39 @@ struct
                              [],
                              F.mk_e_app base args ))
                          bounds
+                | TIFn (TArrow (inputs, output))
+                  when Attrs.find_unique_attr i.ti_attrs ~f:(function
+                         | TraitMethodNoPrePost -> Some ()
+                         | _ -> None)
+                       |> Option.is_none ->
+                    let inputs =
+                      List.mapi ~f:(FStarBinder.of_typ e.span) inputs
+                    in
+                    let inputs = generics @ inputs in
+                    let output = pty e.span output in
+                    let ty_pre_post =
+                      let inputs = List.map ~f:FStarBinder.to_term inputs in
+                      let pre =
+                        F.mk_e_app (F.term_of_lid [ name ^ "_pre" ]) inputs
+                      in
+                      let result = F.term_of_lid [ "result" ] in
+                      let post =
+                        F.mk_e_app
+                          (F.term_of_lid [ name ^ "_post" ])
+                          (inputs @ [ result ])
+                      in
+                      let post =
+                        F.mk_e_abs
+                          [ F.pat @@ F.AST.PatVar (F.id "result", None, []) ]
+                          post
+                      in
+                      F.mk_e_app
+                        (F.term_of_lid [ "Prims"; "Pure" ])
+                        [ output; pre; post ]
+                    in
+                    let inputs = List.map ~f:FStarBinder.to_binder inputs in
+                    let ty = F.term @@ F.AST.Product (inputs, ty_pre_post) in
+                    [ (F.id name, None, [], ty) ]
                 | TIFn ty ->
                     let ty = pty e.span ty in
                     let ty =
@@ -1302,6 +1335,7 @@ module TransformToInputLanguage =
   |> Phases.Reject.EarlyExit
   |> Phases.Functionalize_loops
   |> Phases.Reject.As_pattern
+  |> Phases.Traits_specs
   |> SubtypeToInputLanguage
   |> Identity
   ]

From 335c785511556a10948d454c8152e1516a91e71c Mon Sep 17 00:00:00 2001
From: Lucas Franceschino <lucas@cryspen.com>
Date: Mon, 4 Mar 2024 17:14:32 +0100
Subject: [PATCH 08/24] feat(proof-libs/fstar): pre/post for index trait

---
 proof-libs/fstar/core/Core.Ops.Index.fst      |  5 ++--
 proof-libs/fstar/core/Core.Ops.Range.fsti     | 30 ++++++++++++-------
 proof-libs/fstar/core/Core.Ops.fst            |  4 +--
 proof-libs/fstar/core/Core.Slice.fsti         |  3 +-
 .../rust_primitives/Rust_primitives.Hax.fst   |  7 +++--
 5 files changed, 30 insertions(+), 19 deletions(-)

diff --git a/proof-libs/fstar/core/Core.Ops.Index.fst b/proof-libs/fstar/core/Core.Ops.Index.fst
index 200d1e250..9fe2f6b82 100644
--- a/proof-libs/fstar/core/Core.Ops.Index.fst
+++ b/proof-libs/fstar/core/Core.Ops.Index.fst
@@ -2,7 +2,8 @@ module Core.Ops.Index
 
 class t_Index t_Self t_Idx = {
   f_Output: Type0;
-  in_range: t_Self -> t_Idx -> Type0;
-  f_index: s:t_Self -> i:t_Idx{in_range s i} -> f_Output;
+  f_index_pre: s:t_Self -> i:t_Idx -> Type0;
+  f_index_post: s:t_Self -> i:t_Idx -> f_Output -> Type0;
+  f_index: s:t_Self -> i:t_Idx -> Pure f_Output (f_index_pre s i) (fun r -> f_index_post s i r);
 }
 
diff --git a/proof-libs/fstar/core/Core.Ops.Range.fsti b/proof-libs/fstar/core/Core.Ops.Range.fsti
index 2ad1ee5ec..fffe32635 100644
--- a/proof-libs/fstar/core/Core.Ops.Range.fsti
+++ b/proof-libs/fstar/core/Core.Ops.Range.fsti
@@ -38,7 +38,8 @@ open Core.Ops.Index
 
 instance impl_index_range_slice t n : t_Index (t_Slice t) (t_Range (int_t n)) 
   = { f_Output = t_Slice t
-    ; in_range = (fun (s: t_Slice t) {f_start; f_end} -> 
+    ; f_index_post = (fun _ _ _ -> true)
+    ; f_index_pre = (fun (s: t_Slice t) {f_start; f_end} -> 
          let len = Rust_primitives.length s in
          v f_start >= 0 /\ v f_start <= v len /\ v f_end <= v len)
     ; f_index = (fun s {f_start; f_end} -> 
@@ -47,13 +48,15 @@ instance impl_index_range_slice t n : t_Index (t_Slice t) (t_Range (int_t n))
 
 instance impl_index_range_to_slice t n : t_Index (t_Slice t) (t_RangeTo (int_t n)) 
   = { f_Output = t_Slice t
-    ; in_range = (fun (s: t_Slice t) ({f_end}: t_RangeTo (int_t n)) -> 
+    ; f_index_post = (fun _ _ _ -> true)
+    ; f_index_pre = (fun (s: t_Slice t) ({f_end}: t_RangeTo (int_t n)) -> 
          let len = Rust_primitives.length s in v f_end <= v len)
     ; f_index = (fun s {f_end} -> if 0 < v f_end then Seq.slice s 0 (v f_end) else Seq.empty)}
 
 instance impl_index_range_from_slice t n : t_Index (t_Slice t) (t_RangeFrom (int_t n)) 
   = { f_Output = t_Slice t
-    ; in_range = (fun (s: t_Slice t) ({f_start}: t_RangeFrom (int_t n)) -> 
+    ; f_index_post = (fun _ _ _ -> true)
+    ; f_index_pre = (fun (s: t_Slice t) ({f_start}: t_RangeFrom (int_t n)) -> 
          let len = Rust_primitives.length s in v f_start >= 0 /\ v f_start <= v len)
     ; f_index = (fun s {f_start} -> 
          let len = Rust_primitives.length s in
@@ -61,31 +64,36 @@ instance impl_index_range_from_slice t n : t_Index (t_Slice t) (t_RangeFrom (int
          
 instance impl_index_range_full_slice t : t_Index (t_Slice t) t_RangeFull
   = { f_Output = t_Slice t
-    ; in_range = (fun (s: t_Slice t) _ -> True)
+    ; f_index_post = (fun _ _ _ -> true)
+    ; f_index_pre = (fun (s: t_Slice t) _ -> True)
     ; f_index = (fun s _ -> s)}
 
 instance impl_range_index_array t len n : t_Index (t_Array t len) (t_Range (int_t n)) = 
   let i = impl_index_range_slice t n in
   { f_Output = i.f_Output
-  ; in_range = (fun (s: t_Array t len) r -> i.in_range s r)
+  ; f_index_post = (fun _ _ _ -> true)
+  ; f_index_pre = (fun (s: t_Array t len) r -> i.f_index_pre s r)
   ; f_index = (fun s r -> i.f_index s r) }
   
 instance impl_range_to_index_array t len n : t_Index (t_Array t len) (t_RangeTo (int_t n)) = 
   let i = impl_index_range_to_slice t n in
   { f_Output = i.f_Output
-  ; in_range = (fun (s: t_Array t len) r -> i.in_range s r)
+  ; f_index_post = (fun _ _ _ -> true)
+  ; f_index_pre = (fun (s: t_Array t len) r -> i.f_index_pre s r)
   ; f_index = (fun s r -> i.f_index s r) }
 
 instance impl_range_from_index_array t len n : t_Index (t_Array t len) (t_RangeFrom (int_t n)) = 
   let i = impl_index_range_from_slice t n in
   { f_Output = i.f_Output
-  ; in_range = (fun (s: t_Array t len) r -> i.in_range s r)
+  ; f_index_post = (fun _ _ _ -> true)
+  ; f_index_pre = (fun (s: t_Array t len) r -> i.f_index_pre s r)
   ; f_index = (fun s r -> i.f_index s r) }
 
 instance impl_range_full_index_array t len : t_Index (t_Array t len) t_RangeFull = 
   let i = impl_index_range_full_slice t in
   { f_Output = i.f_Output
-  ; in_range = (fun (s: t_Array t len) r -> i.in_range s r)
+  ; f_index_post = (fun _ _ _ -> true)
+  ; f_index_pre = (fun (s: t_Array t len) r -> i.f_index_pre s r)
   ; f_index = (fun s r -> i.f_index s r) }
 
 open Rust_primitives.Hax
@@ -100,13 +108,13 @@ let update_at_tc_array_range_full_super t l: t_Index (t_Array t l) t_RangeFull
   = FStar.Tactics.Typeclasses.solve
 
 val update_at_array_range t l n
-  (s: t_Array t l) (i: t_Range (int_t n) {(update_at_tc_array_range_super t l n).in_range s i})
+  (s: t_Array t l) (i: t_Range (int_t n) {(update_at_tc_array_range_super t l n).f_index_pre s i})
   : (update_at_tc_array_range_super t l n).f_Output -> t_Array t l
 val update_at_array_range_to t l n
-  (s: t_Array t l) (i: t_RangeTo (int_t n) {(update_at_tc_array_range_to_super t l n).in_range s i})
+  (s: t_Array t l) (i: t_RangeTo (int_t n) {(update_at_tc_array_range_to_super t l n).f_index_pre s i})
   : (update_at_tc_array_range_to_super t l n).f_Output -> t_Array t l
 val update_at_array_range_from t l n
-  (s: t_Array t l) (i: t_RangeFrom (int_t n) {(update_at_tc_array_range_from_super t l n).in_range s i})
+  (s: t_Array t l) (i: t_RangeFrom (int_t n) {(update_at_tc_array_range_from_super t l n).f_index_pre s i})
   : (update_at_tc_array_range_from_super t l n).f_Output -> t_Array t l
 val update_at_array_range_full t l
   (s: t_Array t l) (i: t_RangeFull)
diff --git a/proof-libs/fstar/core/Core.Ops.fst b/proof-libs/fstar/core/Core.Ops.fst
index a1110181f..3d72f9e7b 100644
--- a/proof-libs/fstar/core/Core.Ops.fst
+++ b/proof-libs/fstar/core/Core.Ops.fst
@@ -22,6 +22,6 @@ instance negation_for_bool: negation_tc bool = {
 open Core.Ops.Index
 
 let ( .[] ) #self #idx {| inst: t_Index self idx |}
-  : s:self -> i:idx{in_range s i} -> inst.f_Output
-  = f_index
+  (s:self) (i:idx{f_index_pre s i}): inst.f_Output
+  = f_index s i
 
diff --git a/proof-libs/fstar/core/Core.Slice.fsti b/proof-libs/fstar/core/Core.Slice.fsti
index 6851d96bd..295bba734 100644
--- a/proof-libs/fstar/core/Core.Slice.fsti
+++ b/proof-libs/fstar/core/Core.Slice.fsti
@@ -21,7 +21,8 @@ open Core.Ops.Index
 
 instance impl__index t n: t_Index (t_Slice t) (int_t n)
   = { f_Output = t;
-      in_range = (fun (s: t_Slice t) (i: int_t n) -> v i >= 0 && v i < v (length s));
+      f_index_pre = (fun (s: t_Slice t) (i: int_t n) -> v i >= 0 && v i < v (length s));
+      f_index_post = (fun _ _ _ -> true);
       f_index = (fun s i -> Seq.index s (v i));
     }
 
diff --git a/proof-libs/fstar/rust_primitives/Rust_primitives.Hax.fst b/proof-libs/fstar/rust_primitives/Rust_primitives.Hax.fst
index 39436f5c4..48718bd0b 100644
--- a/proof-libs/fstar/rust_primitives/Rust_primitives.Hax.fst
+++ b/proof-libs/fstar/rust_primitives/Rust_primitives.Hax.fst
@@ -13,14 +13,15 @@ open Core.Ops.Index
 class update_at_tc self idx = {
   [@@@FStar.Tactics.Typeclasses.tcinstance]
   super_index: t_Index self idx;
-  update_at: s: self -> i: idx {in_range s i} -> super_index.f_Output -> self;
+  update_at: s: self -> i: idx {f_index_pre s i} -> super_index.f_Output -> self;
 }
 
 open Core.Slice
 
 instance impl__index t l n: t_Index (t_Array t l) (int_t n)
   = { f_Output = t;
-      in_range = (fun (s: t_Array t l) (i: int_t n) -> v i >= 0 && v i < v l);
+      f_index_pre = (fun (s: t_Array t l) (i: int_t n) -> v i >= 0 && v i < v l);
+      f_index_post = (fun _ _ _ -> true);
       f_index = (fun s i -> Seq.index s (v i));
     }
 
@@ -29,7 +30,7 @@ instance update_at_tc_array t l n: update_at_tc (t_Array t l) (int_t n) = {
   update_at = (fun arr i x -> FStar.Seq.upd arr (v i) x);
 }
 
-let (.[]<-) #self #idx {| update_at_tc self idx |} (s: self) (i: idx {in_range s i})
+let (.[]<-) #self #idx {| update_at_tc self idx |} (s: self) (i: idx {f_index_pre s i})
   = update_at s i
 
 let array_of_list #t = Rust_primitives.Arrays.of_list #t

From 135c935154ab23bfaf5c0473002758595f5968ff Mon Sep 17 00:00:00 2001
From: Lucas Franceschino <lucas@cryspen.com>
Date: Tue, 5 Mar 2024 12:27:20 +0100
Subject: [PATCH 09/24] feat(engine/ast-utils): introduce more `Expect` helpers

---
 engine/lib/ast_utils.ml | 17 +++++++++++++++++
 1 file changed, 17 insertions(+)

diff --git a/engine/lib/ast_utils.ml b/engine/lib/ast_utils.ml
index 1316ae12b..9bb33a356 100644
--- a/engine/lib/ast_utils.ml
+++ b/engine/lib/ast_utils.ml
@@ -60,6 +60,23 @@ module Make (F : Features.T) = struct
           Some e
       | _ -> None
 
+    let closure (e : expr) : (pat list * expr) option =
+      match e.e with
+      | Closure { params; body; _ } -> Some (params, body)
+      | _ -> None
+
+    let app (e : expr) :
+        (expr * expr list * generic_value list * impl_expr option) option =
+      match e.e with
+      | App { f; args; generic_args; impl } -> Some (f, args, generic_args, impl)
+      | _ -> None
+
+    let pbinding_simple (p : pat) : (local_ident * ty) option =
+      match p.p with
+      | PBinding { mut = Immutable; mode = _; var; typ; subpat = None } ->
+          Some (var, typ)
+      | _ -> None
+
     let concrete_app1 (f : Concrete_ident.name) (e : expr) : expr option =
       match e.e with
       | App

From eee9a7b0a9345a696d8bf92da2b9b738db780936 Mon Sep 17 00:00:00 2001
From: Lucas Franceschino <lucas@cryspen.com>
Date: Tue, 5 Mar 2024 12:27:36 +0100
Subject: [PATCH 10/24] feat(engine/ast-utils): mappers: introduce
 `replace_local_variable`

---
 engine/lib/ast_utils.ml | 13 +++++++++++++
 1 file changed, 13 insertions(+)

diff --git a/engine/lib/ast_utils.ml b/engine/lib/ast_utils.ml
index 9bb33a356..7d6d1d018 100644
--- a/engine/lib/ast_utils.ml
+++ b/engine/lib/ast_utils.ml
@@ -248,6 +248,19 @@ module Make (F : Features.T) = struct
           | _ -> super#visit_item' () item'
       end
 
+    (** [replace_local_variable var replacement] returns a visitor
+      that maps any type of the AST replacing every occurence of the
+      expression [LocalVar var] by [replacement]. *)
+    let replace_local_variable (var : local_ident) (replacement : expr) =
+      object
+        inherit [_] Visitors.map as super
+
+        method! visit_expr () e =
+          match e.e with
+          | LocalVar var' when [%eq: local_ident] var var' -> replacement
+          | _ -> super#visit_expr () e
+      end
+
     let rename_local_idents (f : local_ident -> local_ident) =
       object
         inherit [_] Visitors.map as _super

From 850561c5a1e876453ba592af759d0665d1346b22 Mon Sep 17 00:00:00 2001
From: Lucas Franceschino <lucas@cryspen.com>
Date: Tue, 5 Mar 2024 12:27:57 +0100
Subject: [PATCH 11/24] feat(engine/ast-utils): introduce
 `beta_reduce1_closure`

---
 engine/lib/ast_utils.ml | 13 +++++++++++++
 1 file changed, 13 insertions(+)

diff --git a/engine/lib/ast_utils.ml b/engine/lib/ast_utils.ml
index 7d6d1d018..268d52374 100644
--- a/engine/lib/ast_utils.ml
+++ b/engine/lib/ast_utils.ml
@@ -673,6 +673,19 @@ module Make (F : Features.T) = struct
         e
     | _ -> e
 
+  let beta_reduce1_closure_opt (e : expr) : expr option =
+    let* f, args, _, _ = Expect.app e in
+    let* pats, body = Expect.closure f in
+    match (pats, args) with
+    | [ pat ], [ arg ] ->
+        let* var, _ = Expect.pbinding_simple pat in
+        Some ((Mappers.replace_local_variable var arg)#visit_expr () body)
+    | _ -> None
+
+  (** reduce a `(|x| body)(e)` into `body[x/e]` *)
+  let beta_reduce1_closure (e : expr) : expr =
+    beta_reduce1_closure_opt e |> Option.value ~default:e
+
   (* let rec remove_empty_tap *)
 
   let is_unit_typ : ty -> bool =

From 0fec16caa0595b310e5f37d79951dc18582e3b8e Mon Sep 17 00:00:00 2001
From: Lucas Franceschino <lucas@cryspen.com>
Date: Tue, 5 Mar 2024 12:29:12 +0100
Subject: [PATCH 12/24] fix(backends/F*): rename `out` binder in impl.
 postconditions

---
 engine/lib/phases/phase_traits_specs.ml | 26 +++++++++++++++----------
 1 file changed, 16 insertions(+), 10 deletions(-)

diff --git a/engine/lib/phases/phase_traits_specs.ml b/engine/lib/phases/phase_traits_specs.ml
index f9d4a74d9..8c97284ac 100644
--- a/engine/lib/phases/phase_traits_specs.ml
+++ b/engine/lib/phases/phase_traits_specs.ml
@@ -80,13 +80,21 @@ module Make (F : Features.T) =
                           |> Set.to_list)
                           "out"
                       in
-                      let out =
-                        {
-                          pat = U.make_var_pat out_ident body.typ body.span;
-                          typ = body.typ;
-                          typ_span = None;
-                          attrs = [];
-                        }
+                      let pat = U.make_var_pat out_ident body.typ body.span in
+                      let typ = body.typ in
+                      let out = { pat; typ; typ_span = None; attrs = [] } in
+                      let post =
+                        let f =
+                          Attrs.associated_expr ~keep_last_args:1 Ensures
+                            item.ii_attrs
+                          |> Option.value ~default
+                        in
+                        let span = f.span in
+                        let args = [ { span; typ; e = LocalVar out_ident } ] in
+                        let e =
+                          App { f; args; generic_args = []; impl = None }
+                        in
+                        { f with e } |> U.beta_reduce1_closure
                       in
                       [
                         {
@@ -105,9 +113,7 @@ module Make (F : Features.T) =
                           ii_v =
                             IIFn
                               {
-                                body =
-                                  Attrs.associated_expr Ensures item.ii_attrs
-                                  |> Option.value ~default;
+                                body = post |> U.beta_reduce1_closure;
                                 params = params @ [ out ];
                               };
                         };

From 9a1b897d8a0b326ebb040ac19b3b359a46d4bc4c Mon Sep 17 00:00:00 2001
From: Lucas Franceschino <lucas@cryspen.com>
Date: Tue, 5 Mar 2024 12:30:49 +0100
Subject: [PATCH 13/24] fix(proof-libs): errors in `fst`s

---
 .../fstar/rust_primitives/Rust_primitives.BitVectors.fst      | 4 ++--
 proof-libs/fstar/rust_primitives/Rust_primitives.Integers.fst | 2 +-
 2 files changed, 3 insertions(+), 3 deletions(-)

diff --git a/proof-libs/fstar/rust_primitives/Rust_primitives.BitVectors.fst b/proof-libs/fstar/rust_primitives/Rust_primitives.BitVectors.fst
index c86d373e0..b6477f73b 100644
--- a/proof-libs/fstar/rust_primitives/Rust_primitives.BitVectors.fst
+++ b/proof-libs/fstar/rust_primitives/Rust_primitives.BitVectors.fst
@@ -22,8 +22,8 @@ let pow2_minus_one_mod_lemma2 (n: nat) (m: nat {n <= m})
   = Math.Lemmas.pow2_le_compat m n;
     Math.Lemmas.small_div (pow2 n - 1) (pow2 m)
 
-let bit_vec_to_int_arr d bv = admit () // see issue #423
-let bit_vec_to_nat_arr d bv = admit () // see issue #423
+let bit_vec_to_int_t_array d bv = admit () // see issue #423
+let bit_vec_to_nat_array d bv = admit () // see issue #423
 
 let get_bit_pow2_minus_one #t n nth
   = reveal_opaque (`%get_bit) (get_bit (mk_int #t (pow2 n - 1)) nth);
diff --git a/proof-libs/fstar/rust_primitives/Rust_primitives.Integers.fst b/proof-libs/fstar/rust_primitives/Rust_primitives.Integers.fst
index 5dbd8bc36..2fce084a2 100644
--- a/proof-libs/fstar/rust_primitives/Rust_primitives.Integers.fst
+++ b/proof-libs/fstar/rust_primitives/Rust_primitives.Integers.fst
@@ -57,7 +57,7 @@ let rotate_left_equiv_lemma #t a b = ()
 
 let abs_int_equiv_lemma #t a = admit() // see issue #423
 
-let neg_equiv_lemma #_ _ = ()
+let neg_equiv_lemma #_ _ = admit ()
 
 let get_bit_and _x _y _i = admit () // see issue #423
 let get_bit_or _x _y _i = admit () // see issue #423

From 4e885f960e3a255bc76414c010a816aceb808f54 Mon Sep 17 00:00:00 2001
From: Lucas Franceschino <lucas@cryspen.com>
Date: Tue, 5 Mar 2024 12:45:55 +0100
Subject: [PATCH 14/24] chore(tests snaps): pre/post on traits

---
 .../toolchain__generics into-fstar.snap       | 14 ++++++-
 ..._mut-ref-functionalization into-fstar.snap | 14 ++++++-
 .../toolchain__traits into-fstar.snap         | 39 ++++++++++++++++---
 3 files changed, 57 insertions(+), 10 deletions(-)

diff --git a/test-harness/src/snapshots/toolchain__generics into-fstar.snap b/test-harness/src/snapshots/toolchain__generics into-fstar.snap
index f207970c5..87e599a7e 100644
--- a/test-harness/src/snapshots/toolchain__generics into-fstar.snap	
+++ b/test-harness/src/snapshots/toolchain__generics into-fstar.snap	
@@ -18,6 +18,7 @@ info:
       stderr: true
       stdout: true
     include_flag: ~
+    backend_options: ~
 ---
 exit = 0
 stderr = '''
@@ -41,11 +42,20 @@ let impl__Bar__inherent_impl_generics
       (x: t_Array v_T v_N)
     : Prims.unit = ()
 
-class t_Foo (v_Self: Type) = { f_const_add:v_N: usize -> v_Self -> usize }
+class t_Foo (v_Self: Type) = {
+  f_const_add_pre:v_N: usize -> v_Self -> bool;
+  f_const_add_post:v_N: usize -> v_Self -> usize -> bool;
+  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 = fun (v_N: usize) (self: usize) -> self +! v_N }
+  {
+    f_const_add_pre = (fun (v_N: usize) (self: usize) -> true);
+    f_const_add_post = (fun (v_N: usize) (self: usize) (out: usize) -> true out);
+    f_const_add = fun (v_N: usize) (self: usize) -> self +! v_N
+  }
 
 let dup
       (#v_T: Type)
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 9b3730cd1..57c5fc76f 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	
@@ -18,6 +18,7 @@ info:
       stderr: false
       stdout: true
     include_flag: ~
+    backend_options: ~
 ---
 exit = 0
 
@@ -31,7 +32,11 @@ module Mut_ref_functionalization
 open Core
 open FStar.Mul
 
-class t_FooTrait (v_Self: Type) = { f_z:v_Self -> v_Self }
+class t_FooTrait (v_Self: Type) = {
+  f_z_pre:v_Self -> bool;
+  f_z_post:v_Self -> v_Self -> bool;
+  f_z:x0: v_Self -> Prims.Pure v_Self (f_z_pre x0) (fun result -> f_z_post x0 result)
+}
 
 let array (x: t_Array u8 (sz 10)) : t_Array u8 (sz 10) =
   let x:t_Array u8 (sz 10) =
@@ -163,7 +168,12 @@ type t_Bar = {
 type t_Foo = { f_field:Alloc.Vec.t_Vec u8 Alloc.Alloc.t_Global }
 
 [@@ FStar.Tactics.Typeclasses.tcinstance]
-let impl_FooTrait_for_Foo: t_FooTrait t_Foo = { f_z = fun (self: t_Foo) -> self }
+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 out);
+    f_z = fun (self: t_Foo) -> self
+  }
 
 type t_S = { f_b:t_Array u8 (sz 5) }
 
diff --git a/test-harness/src/snapshots/toolchain__traits into-fstar.snap b/test-harness/src/snapshots/toolchain__traits into-fstar.snap
index 2cdb39727..534828741 100644
--- a/test-harness/src/snapshots/toolchain__traits into-fstar.snap	
+++ b/test-harness/src/snapshots/toolchain__traits into-fstar.snap	
@@ -35,7 +35,11 @@ module Traits
 open Core
 open FStar.Mul
 
-class t_Bar (v_Self: Type) = { f_bar:v_Self -> Prims.unit }
+class t_Bar (v_Self: Type) = {
+  f_bar_pre:v_Self -> bool;
+  f_bar_post:v_Self -> Prims.unit -> bool;
+  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: Type)
@@ -48,17 +52,27 @@ class t_Lang (v_Self: Type) = {
   [@@@ FStar.Tactics.Typeclasses.no_method]_super_8328838127052049456:Core.Marker.t_Sized v_Self;
   f_Var:Type;
   f_Var_6601305896307871948:Core.Marker.t_Sized f_Var;
-  f_s:v_Self -> i32 -> (v_Self & f_Var)
+  f_s_pre:v_Self -> i32 -> bool;
+  f_s_post:v_Self -> i32 -> (v_Self & f_Var) -> bool;
+  f_s:x0: v_Self -> x1: i32
+    -> Prims.Pure (v_Self & f_Var) (f_s_pre x0 x1) (fun result -> f_s_post x0 x1 result)
 }
 
 class t_SuperTrait (v_Self: Type) = {
   [@@@ FStar.Tactics.Typeclasses.no_method]_super_2101570567305961368:Core.Clone.t_Clone v_Self;
-  f_function_of_super_trait:v_Self -> u32
+  f_function_of_super_trait_pre:v_Self -> bool;
+  f_function_of_super_trait_post:v_Self -> u32 -> bool;
+  f_function_of_super_trait:x0: v_Self
+    -> Prims.Pure u32
+        (f_function_of_super_trait_pre x0)
+        (fun result -> f_function_of_super_trait_post x0 result)
 }
 
 [@@ FStar.Tactics.Typeclasses.tcinstance]
 let impl_SuperTrait_for_i32: t_SuperTrait i32 =
   {
+    f_function_of_super_trait_pre = (fun (self: i32) -> true);
+    f_function_of_super_trait_post = (fun (self: i32) (out: u32) -> true out);
     f_function_of_super_trait = fun (self: i32) -> cast (Core.Num.impl__i32__abs self <: i32) <: u32
   }
 
@@ -68,9 +82,18 @@ class t_Foo (v_Self: Type) = {
   f_AssocType_1499648403794240798:Core.Clone.t_Clone f_AssocType;
   f_AssocType_3786252681321530780:Core.Marker.t_Sized f_AssocType;
   f_N:usize;
-  f_assoc_f:Prims.unit -> Prims.unit;
-  f_method_f:v_Self -> Prims.unit;
-  f_assoc_type:{| i3: Core.Marker.t_Copy f_AssocType |} -> f_AssocType -> Prims.unit
+  f_assoc_f_pre:Prims.unit -> bool;
+  f_assoc_f_post:Prims.unit -> Prims.unit -> bool;
+  f_assoc_f:x0: Prims.unit
+    -> Prims.Pure Prims.unit (f_assoc_f_pre x0) (fun result -> f_assoc_f_post x0 result);
+  f_method_f_pre:v_Self -> bool;
+  f_method_f_post:v_Self -> Prims.unit -> bool;
+  f_method_f:x0: v_Self
+    -> Prims.Pure Prims.unit (f_method_f_pre x0) (fun result -> f_method_f_post x0 result);
+  f_assoc_type_pre:{| i3: Core.Marker.t_Copy f_AssocType |} -> f_AssocType -> bool;
+  f_assoc_type_post:{| i3: Core.Marker.t_Copy f_AssocType |} -> f_AssocType -> Prims.unit -> bool;
+  f_assoc_type:{| i3: Core.Marker.t_Copy f_AssocType |} -> x0: f_AssocType
+    -> Prims.Pure Prims.unit (f_assoc_type_pre i3 x0) (fun result -> f_assoc_type_post i3 x0 result)
 }
 
 let closure_impl_expr
@@ -118,7 +141,11 @@ let impl_Foo_for_tuple_: t_Foo Prims.unit =
     f_AssocType = i32;
     f_N = sz 32;
     f_assoc_f = () <: Prims.unit;
+    f_method_f_pre = (fun (self: Prims.unit) -> true);
+    f_method_f_post = (fun (self: Prims.unit) (out: Prims.unit) -> true out);
     f_method_f = (fun (self: Prims.unit) -> f_assoc_f ());
+    f_assoc_type_pre = (fun (_: i32) -> true);
+    f_assoc_type_post = (fun (_: i32) (out: Prims.unit) -> true out);
     f_assoc_type = fun (_: i32) -> ()
   }
 

From 410de0779c86d0768294f727313f8e43a498e1bb Mon Sep 17 00:00:00 2001
From: Lucas Franceschino <lucas@cryspen.com>
Date: Tue, 5 Mar 2024 13:05:32 +0100
Subject: [PATCH 15/24] feat(proof-libs/fstar): pre/post for as_ref trait

---
 proof-libs/fstar/core/Core.Convert.fst | 2 ++
 1 file changed, 2 insertions(+)

diff --git a/proof-libs/fstar/core/Core.Convert.fst b/proof-libs/fstar/core/Core.Convert.fst
index 826fe9f82..36e885d28 100644
--- a/proof-libs/fstar/core/Core.Convert.fst
+++ b/proof-libs/fstar/core/Core.Convert.fst
@@ -53,5 +53,7 @@ instance from_id a: t_From a a = {
 }
 
 class t_AsRef self t = {
+  f_as_ref_pre: self -> bool;
+  f_as_ref_post: self -> t -> bool;
   f_as_ref:  self -> t;
 }

From c6cc24d113f91d767ca901db7d5a3ba40787b887 Mon Sep 17 00:00:00 2001
From: Lucas Franceschino <lucas@cryspen.com>
Date: Tue, 5 Mar 2024 14:06:09 +0100
Subject: [PATCH 16/24] test(traits,attrs): add `refined_indexes` &
 `newtype_pattern`

---
 .../toolchain__attributes into-fstar.snap     | 48 +++++++++++++++++++
 tests/attributes/src/lib.rs                   | 44 +++++++++++++++++
 2 files changed, 92 insertions(+)

diff --git a/test-harness/src/snapshots/toolchain__attributes into-fstar.snap b/test-harness/src/snapshots/toolchain__attributes into-fstar.snap
index c64863555..dc9139ebe 100644
--- a/test-harness/src/snapshots/toolchain__attributes into-fstar.snap	
+++ b/test-harness/src/snapshots/toolchain__attributes into-fstar.snap	
@@ -17,6 +17,8 @@ info:
     snapshot:
       stderr: false
       stdout: true
+    include_flag: ~
+    backend_options: ~
 ---
 exit = 0
 
@@ -24,6 +26,52 @@ exit = 0
 diagnostics = []
 
 [stdout.files]
+"Attributes.Newtype_pattern.fst" = '''
+module Attributes.Newtype_pattern
+#set-options "--fuel 0 --ifuel 1 --z3rlimit 15"
+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
+
+[@@ FStar.Tactics.Typeclasses.tcinstance]
+let impl_1 (#v_T: Type) (#[FStar.Tactics.Typeclasses.tcresolve ()] i0: Core.Marker.t_Sized v_T)
+    : Core.Ops.Index.t_Index (t_Array v_T (sz 10)) t_SafeIndex =
+  {
+    f_Output = v_T;
+    f_index_pre = (fun (self: t_Array v_T (sz 10)) (index: t_SafeIndex) -> true);
+    f_index_post = (fun (self: t_Array v_T (sz 10)) (index: t_SafeIndex) (out: v_T) -> true out);
+    f_index = fun (self: t_Array v_T (sz 10)) (index: t_SafeIndex) -> self.[ index.f_i ]
+  }
+'''
+"Attributes.Refined_indexes.fst" = '''
+module Attributes.Refined_indexes
+#set-options "--fuel 0 --ifuel 1 --z3rlimit 15"
+open Core
+open FStar.Mul
+
+let v_MAX: usize = sz 10
+
+type t_MyArray = | MyArray : t_Array u8 (sz 10) -> t_MyArray
+
+[@@ FStar.Tactics.Typeclasses.tcinstance]
+let impl: Core.Ops.Index.t_Index t_MyArray usize =
+  {
+    f_Output = u8;
+    f_index_pre = (fun (self: t_MyArray) (index: usize) -> index <. v_MAX);
+    f_index_post = (fun (self: t_MyArray) (index: usize) (out: u8) -> true out);
+    f_index = fun (self: t_MyArray) (index: usize) -> self.[ index ]
+  }
+'''
 "Attributes.fst" = '''
 module Attributes
 #set-options "--fuel 0 --ifuel 1 --z3rlimit 15"
diff --git a/tests/attributes/src/lib.rs b/tests/attributes/src/lib.rs
index c069aeaea..90299c046 100644
--- a/tests/attributes/src/lib.rs
+++ b/tests/attributes/src/lib.rs
@@ -39,3 +39,47 @@ impl Foo {
     #[hax::exclude]
     fn h(&self) {}
 }
+
+mod refined_indexes {
+    use hax_lib_macros as hax;
+    const MAX: usize = 10;
+    struct MyArray(pub [u8; MAX]);
+
+    #[hax::attributes]
+    impl std::ops::Index<usize> for MyArray {
+        type Output = u8;
+        #[requires(index < MAX)]
+        fn index(&self, index: usize) -> &Self::Output {
+            &self[index]
+        }
+    }
+}
+mod newtype_pattern {
+    use hax_lib_macros as hax;
+
+    const MAX: usize = 10;
+    #[hax::attributes]
+    struct SafeIndex {
+        #[refine(i < MAX)]
+        i: usize,
+    }
+    impl SafeIndex {
+        fn new(i: usize) -> Option<Self> {
+            if i < MAX {
+                Some(Self { i })
+            } else {
+                None
+            }
+        }
+        fn as_usize(&self) -> usize {
+            self.i
+        }
+    }
+
+    impl<T> std::ops::Index<SafeIndex> for [T; MAX] {
+        type Output = T;
+        fn index(&self, index: SafeIndex) -> &Self::Output {
+            &self[index.i]
+        }
+    }
+}

From ba5b10f2cdb0e2bc07c74c0bb8c645e5343e3f3a Mon Sep 17 00:00:00 2001
From: Lucas Franceschino <lucas@cryspen.com>
Date: Tue, 5 Mar 2024 14:20:46 +0100
Subject: [PATCH 17/24] fix(engine/phase): traits specs: default for post

---
 engine/lib/phases/phase_traits_specs.ml             | 13 ++++++++++++-
 .../snapshots/toolchain__attributes into-fstar.snap |  4 ++--
 .../snapshots/toolchain__generics into-fstar.snap   |  2 +-
 ...chain__mut-ref-functionalization into-fstar.snap |  2 +-
 .../src/snapshots/toolchain__traits into-fstar.snap |  6 +++---
 5 files changed, 19 insertions(+), 8 deletions(-)

diff --git a/engine/lib/phases/phase_traits_specs.ml b/engine/lib/phases/phase_traits_specs.ml
index 8c97284ac..ba5b01342 100644
--- a/engine/lib/phases/phase_traits_specs.ml
+++ b/engine/lib/phases/phase_traits_specs.ml
@@ -87,7 +87,18 @@ module Make (F : Features.T) =
                         let f =
                           Attrs.associated_expr ~keep_last_args:1 Ensures
                             item.ii_attrs
-                          |> Option.value ~default
+                          |> Option.value
+                               ~default:
+                                 {
+                                   default with
+                                   e =
+                                     Closure
+                                       {
+                                         params = [ pat ];
+                                         body = default;
+                                         captures = [];
+                                       };
+                                 }
                         in
                         let span = f.span in
                         let args = [ { span; typ; e = LocalVar out_ident } ] in
diff --git a/test-harness/src/snapshots/toolchain__attributes into-fstar.snap b/test-harness/src/snapshots/toolchain__attributes into-fstar.snap
index dc9139ebe..bd83f3e65 100644
--- a/test-harness/src/snapshots/toolchain__attributes into-fstar.snap	
+++ b/test-harness/src/snapshots/toolchain__attributes into-fstar.snap	
@@ -49,7 +49,7 @@ let impl_1 (#v_T: Type) (#[FStar.Tactics.Typeclasses.tcresolve ()] i0: Core.Mark
   {
     f_Output = v_T;
     f_index_pre = (fun (self: t_Array v_T (sz 10)) (index: t_SafeIndex) -> true);
-    f_index_post = (fun (self: t_Array v_T (sz 10)) (index: t_SafeIndex) (out: v_T) -> true out);
+    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 ]
   }
 '''
@@ -68,7 +68,7 @@ let impl: Core.Ops.Index.t_Index t_MyArray usize =
   {
     f_Output = u8;
     f_index_pre = (fun (self: t_MyArray) (index: usize) -> index <. v_MAX);
-    f_index_post = (fun (self: t_MyArray) (index: usize) (out: u8) -> true out);
+    f_index_post = (fun (self: t_MyArray) (index: usize) (out: u8) -> true);
     f_index = fun (self: t_MyArray) (index: usize) -> self.[ index ]
   }
 '''
diff --git a/test-harness/src/snapshots/toolchain__generics into-fstar.snap b/test-harness/src/snapshots/toolchain__generics into-fstar.snap
index 87e599a7e..cf808168b 100644
--- a/test-harness/src/snapshots/toolchain__generics into-fstar.snap	
+++ b/test-harness/src/snapshots/toolchain__generics into-fstar.snap	
@@ -53,7 +53,7 @@ class t_Foo (v_Self: Type) = {
 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 out);
+    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
   }
 
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 57c5fc76f..8413dde0e 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	
@@ -171,7 +171,7 @@ type t_Foo = { f_field:Alloc.Vec.t_Vec u8 Alloc.Alloc.t_Global }
 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 out);
+    f_z_post = (fun (self: t_Foo) (out: t_Foo) -> true);
     f_z = fun (self: t_Foo) -> self
   }
 
diff --git a/test-harness/src/snapshots/toolchain__traits into-fstar.snap b/test-harness/src/snapshots/toolchain__traits into-fstar.snap
index 534828741..d0962e381 100644
--- a/test-harness/src/snapshots/toolchain__traits into-fstar.snap	
+++ b/test-harness/src/snapshots/toolchain__traits into-fstar.snap	
@@ -72,7 +72,7 @@ class t_SuperTrait (v_Self: Type) = {
 let impl_SuperTrait_for_i32: t_SuperTrait i32 =
   {
     f_function_of_super_trait_pre = (fun (self: i32) -> true);
-    f_function_of_super_trait_post = (fun (self: i32) (out: u32) -> true out);
+    f_function_of_super_trait_post = (fun (self: i32) (out: u32) -> true);
     f_function_of_super_trait = fun (self: i32) -> cast (Core.Num.impl__i32__abs self <: i32) <: u32
   }
 
@@ -142,10 +142,10 @@ let impl_Foo_for_tuple_: t_Foo Prims.unit =
     f_N = sz 32;
     f_assoc_f = () <: Prims.unit;
     f_method_f_pre = (fun (self: Prims.unit) -> true);
-    f_method_f_post = (fun (self: Prims.unit) (out: Prims.unit) -> true out);
+    f_method_f_post = (fun (self: Prims.unit) (out: Prims.unit) -> true);
     f_method_f = (fun (self: Prims.unit) -> f_assoc_f ());
     f_assoc_type_pre = (fun (_: i32) -> true);
-    f_assoc_type_post = (fun (_: i32) (out: Prims.unit) -> true out);
+    f_assoc_type_post = (fun (_: i32) (out: Prims.unit) -> true);
     f_assoc_type = fun (_: i32) -> ()
   }
 

From 864a4f541475a62dbba5c97320e89ab634465a8f Mon Sep 17 00:00:00 2001
From: Lucas Franceschino <lucas@cryspen.com>
Date: Tue, 5 Mar 2024 14:37:30 +0100
Subject: [PATCH 18/24] feat(proof-libs/fstar): pre/post `from`/`into`/etc

---
 proof-libs/fstar/core/Core.Convert.fst | 18 ++++++++++++++++--
 1 file changed, 16 insertions(+), 2 deletions(-)

diff --git a/proof-libs/fstar/core/Core.Convert.fst b/proof-libs/fstar/core/Core.Convert.fst
index 36e885d28..0d708ae86 100644
--- a/proof-libs/fstar/core/Core.Convert.fst
+++ b/proof-libs/fstar/core/Core.Convert.fst
@@ -26,34 +26,48 @@ instance impl_6_refined (t: Type0) (len: usize): try_into_tc (s: t_Slice t {Core
 }
 
 class t_Into self t = {
+  f_into_pre: self -> bool;
+  f_into_post: self -> t -> bool;
   f_into: self -> t;
 }
 
 class t_From self t = {
+  f_from_pre: t -> bool;
+  f_from_post: t -> self -> bool;
   f_from: t -> self;
 }
 
 class t_TryFrom self t = {
   [@@@FStar.Tactics.Typeclasses.no_method]
   f_Error: Type0;
+  f_try_from_pre: t -> bool;
+  f_try_from_post: t -> Core.Result.t_Result self f_Error -> bool;
   f_try_from: t -> Core.Result.t_Result self f_Error;
 }
 
 instance integer_into
   (t:inttype) (t':inttype { minint t >= minint t' /\ maxint t <= maxint t' })
   : t_From (int_t t') (int_t t)
-  = { f_from = (fun (x: int_t t) -> Rust_primitives.Integers.cast #t #t' x) }
+  = {
+      f_from_pre = (fun _ -> true);
+      f_from_post = (fun _ _ -> true);
+      f_from = (fun (x: int_t t) -> Rust_primitives.Integers.cast #t #t' x);
+    }
 
 instance into_from_from a b {| t_From a b |}: t_Into b a = {
+  f_into_pre = (fun _ -> true);
+  f_into_post = (fun _ _ -> true);
   f_into = (fun x -> f_from x)
 }
 
 instance from_id a: t_From a a = {
+  f_from_pre = (fun _ -> true);
+  f_from_post = (fun _ _ -> true);
   f_from = (fun x -> x)
 }
 
 class t_AsRef self t = {
   f_as_ref_pre: self -> bool;
   f_as_ref_post: self -> t -> bool;
-  f_as_ref:  self -> t;
+  f_as_ref: self -> t;
 }

From c3bda1246bee9383b1e45b8532ca71d6d593c05d Mon Sep 17 00:00:00 2001
From: Lucas Franceschino <lucas@cryspen.com>
Date: Wed, 6 Mar 2024 11:10:39 +0100
Subject: [PATCH 19/24] feat(engine/utils): intro `sequence`

---
 engine/lib/utils.ml | 6 ++++++
 1 file changed, 6 insertions(+)

diff --git a/engine/lib/utils.ml b/engine/lib/utils.ml
index 0222ff516..262b5be8f 100644
--- a/engine/lib/utils.ml
+++ b/engine/lib/utils.ml
@@ -71,6 +71,12 @@ let inits (type a) (l : a list) : (a list * a) list =
     l
   |> snd
 
+let sequence (l : 'a option list) : 'a list option =
+  List.fold_right
+    ~f:(fun x acc ->
+      match (acc, x) with Some acc, Some x -> Some (x :: acc) | _ -> None)
+    ~init:(Some []) l
+
 let tabsize = 2
 let newline_indent depth : string = "\n" ^ String.make (tabsize * depth) ' '
 

From fe13f01b8b36974f3dc84501501e5268166ed5eb Mon Sep 17 00:00:00 2001
From: Lucas Franceschino <lucas@cryspen.com>
Date: Wed, 6 Mar 2024 11:07:35 +0100
Subject: [PATCH 20/24] feat(engine/ast-utils): introduce
 `replace_local_variables`

---
 engine/lib/ast_utils.ml | 14 +++++++++-----
 1 file changed, 9 insertions(+), 5 deletions(-)

diff --git a/engine/lib/ast_utils.ml b/engine/lib/ast_utils.ml
index 268d52374..ac4406f3b 100644
--- a/engine/lib/ast_utils.ml
+++ b/engine/lib/ast_utils.ml
@@ -248,19 +248,23 @@ module Make (F : Features.T) = struct
           | _ -> super#visit_item' () item'
       end
 
-    (** [replace_local_variable var replacement] returns a visitor
-      that maps any type of the AST replacing every occurence of the
-      expression [LocalVar var] by [replacement]. *)
-    let replace_local_variable (var : local_ident) (replacement : expr) =
+    let replace_local_variables (map : (local_ident, expr, _) Map.t) =
       object
         inherit [_] Visitors.map as super
 
         method! visit_expr () e =
           match e.e with
-          | LocalVar var' when [%eq: local_ident] var var' -> replacement
+          | LocalVar var -> Map.find map var |> Option.value ~default:e
           | _ -> super#visit_expr () e
       end
 
+    (** [replace_local_variable var replacement] returns a visitor
+      that maps any type of the AST replacing every occurence of the
+      expression [LocalVar var] by [replacement]. *)
+    let replace_local_variable (var : local_ident) (replacement : expr) =
+      replace_local_variables
+        (Map.of_alist_exn (module Local_ident) [ (var, replacement) ])
+
     let rename_local_idents (f : local_ident -> local_ident) =
       object
         inherit [_] Visitors.map as _super

From 0dbf8a80b79bca47fdfa968f2ca6ec09844c8473 Mon Sep 17 00:00:00 2001
From: Lucas Franceschino <lucas@cryspen.com>
Date: Wed, 6 Mar 2024 11:08:04 +0100
Subject: [PATCH 21/24] feat(engine/ast-utils): generalize
 `beta_reduce1_closure_opt` into `beta_reduce_closure_opt `

---
 engine/lib/ast_utils.ml | 23 ++++++++++++-----------
 1 file changed, 12 insertions(+), 11 deletions(-)

diff --git a/engine/lib/ast_utils.ml b/engine/lib/ast_utils.ml
index ac4406f3b..369901163 100644
--- a/engine/lib/ast_utils.ml
+++ b/engine/lib/ast_utils.ml
@@ -677,20 +677,21 @@ module Make (F : Features.T) = struct
         e
     | _ -> e
 
-  let beta_reduce1_closure_opt (e : expr) : expr option =
+  (** See [beta_reduce_closure]'s documentation. *)
+  let beta_reduce_closure_opt (e : expr) : expr option =
     let* f, args, _, _ = Expect.app e in
     let* pats, body = Expect.closure f in
-    match (pats, args) with
-    | [ pat ], [ arg ] ->
-        let* var, _ = Expect.pbinding_simple pat in
-        Some ((Mappers.replace_local_variable var arg)#visit_expr () body)
-    | _ -> None
-
-  (** reduce a `(|x| body)(e)` into `body[x/e]` *)
-  let beta_reduce1_closure (e : expr) : expr =
-    beta_reduce1_closure_opt e |> Option.value ~default:e
+    let* vars = List.map ~f:Expect.pbinding_simple pats |> sequence in
+    let vars = List.map ~f:fst vars in
+    let replacements =
+      List.zip_exn vars args |> Map.of_alist_exn (module Local_ident)
+    in
+    Some ((Mappers.replace_local_variables replacements)#visit_expr () body)
 
-  (* let rec remove_empty_tap *)
+  (** Reduces a [(|x1, ..., xN| body)(e1, ..., eN)] to [body[x1/e1, ..., xN/eN]].
+        This assumes the arities are right: [(|x, y| ...)(e1)]. *)
+  let beta_reduce_closure (e : expr) : expr =
+    beta_reduce_closure_opt e |> Option.value ~default:e
 
   let is_unit_typ : ty -> bool =
     remove_tuple1 >> [%matches? TApp { ident = `TupleType 0; _ }]

From 004b386946e5acc92d57fc9ef6206a21389bbc25 Mon Sep 17 00:00:00 2001
From: Lucas Franceschino <lucas@cryspen.com>
Date: Wed, 6 Mar 2024 11:09:39 +0100
Subject: [PATCH 22/24] feat(engine/attr-payloads): intro.
 `associated_expr_rebinding`

---
 engine/lib/attr_payloads.ml | 57 +++++++++++++++++++++++++++----------
 1 file changed, 42 insertions(+), 15 deletions(-)

diff --git a/engine/lib/attr_payloads.ml b/engine/lib/attr_payloads.ml
index 3e00f7b61..b2be72b80 100644
--- a/engine/lib/attr_payloads.ml
+++ b/engine/lib/attr_payloads.ml
@@ -146,7 +146,23 @@ module Make (F : Features.T) (Error : Phase_utils.ERROR) = struct
     val associated_expr :
       ?keep_last_args:int -> AssocRole.t -> attrs -> expr option
 
+    val associated_expr_rebinding :
+      pat list -> AssocRole.t -> attrs -> expr option
+    (** Looks up an expression but takes care of rebinding free variables. *)
+
     val associated_refinement_in_type : string list -> attrs -> expr option
+    (** For type, there is a special treatment. The name of fields are
+        global identifiers, and thus are subject to rewriting by
+        [Concrete_ident] at the moment of printing. In contrast, in the
+        refinement `fn` item generated by the proc-macros, the
+        arguments are local identifiers, and thus are rewrited in a
+        different manner.
+
+        Thus, [associated_refinement_in_type] takes a list of
+        [free_variables]: those are already formatted strings as
+        printed by the backend. Then, we rewrite identities in the
+        refinement formula to match exactly this print policy, using
+        *final* local identifiers (see `Local_ident.make_final`). *)
 
     include module type of MakeBase (Error)
   end
@@ -209,30 +225,41 @@ module Make (F : Features.T) (Error : Phase_utils.ERROR) = struct
                Error.assertion_failure span
                  "this associated item was expected to be a `fn` item")
 
+    (** Looks up an associated expression, optionally keeping `keep_last_args` last arguments. If keep_last_args is negative, then all arguments are kept. *)
     let associated_expr ?(keep_last_args = 0) (role : AssocRole.t) :
         attrs -> expr option =
       associated_fn role
       >> Option.map ~f:(fun (_generics, params, body) ->
-             let params =
-               List.drop params (List.length params - keep_last_args)
-               |> List.map ~f:(fun p -> p.pat)
+             let n =
+               if keep_last_args < 0 then 0
+               else List.length params - keep_last_args
              in
+             let params = List.drop params n |> List.map ~f:(fun p -> p.pat) in
              match params with
              | [] -> body
              | _ -> { body with e = Closure { params; body; captures = [] } })
 
-    (* For type, there is a special treatment. The name of fields are
-       global identifiers, and thus are subject to rewriting by
-       [Concrete_ident] at the moment of printing. In contrast, in the
-       refinement `fn` item generated by the proc-macros, the
-       arguments are local identifiers, and thus are rewrited in a
-       different manner.
-
-       Thus, [associated_refinement_in_type] takes a list of
-       [free_variables]: those are already formatted strings as
-       printed by the backend. Then, we rewrite identities in the
-       refinement formula to match exactly this print policy, using
-       *final* local identifiers (see `Local_ident.make_final`). *)
+    let associated_expr_rebinding (params : pat list) (role : AssocRole.t)
+        (attrs : attrs) : expr option =
+      let* _, original_params, body = associated_fn role attrs in
+      let original_params =
+        List.map ~f:(fun param -> param.pat) original_params
+      in
+      let vars_of_pat =
+        U.Reducers.collect_local_idents#visit_pat () >> Set.to_list
+      in
+      let original_vars = List.concat_map ~f:vars_of_pat original_params in
+      let target_vars = List.concat_map ~f:vars_of_pat params in
+      let replacements =
+        List.zip_exn original_vars target_vars
+        |> Map.of_alist_exn (module Local_ident)
+      in
+      Some
+        ((U.Mappers.rename_local_idents (fun v ->
+              Map.find replacements v |> Option.value ~default:v))
+           #visit_expr
+           () body)
+
     let associated_refinement_in_type (free_variables : string list) :
         attrs -> expr option =
       associated_fn Refine

From 8c76ca2286c74c3d4cc893d32970fee4cf7f21e2 Mon Sep 17 00:00:00 2001
From: Lucas Franceschino <lucas@cryspen.com>
Date: Wed, 6 Mar 2024 11:10:18 +0100
Subject: [PATCH 23/24] feat(engine/phase): trait specs: use
 `associated_expr_rebinding`

---
 engine/lib/phases/phase_traits_specs.ml | 35 +++++++------------------
 1 file changed, 9 insertions(+), 26 deletions(-)

diff --git a/engine/lib/phases/phase_traits_specs.ml b/engine/lib/phases/phase_traits_specs.ml
index ba5b01342..b0a552243 100644
--- a/engine/lib/phases/phase_traits_specs.ml
+++ b/engine/lib/phases/phase_traits_specs.ml
@@ -80,33 +80,12 @@ module Make (F : Features.T) =
                           |> Set.to_list)
                           "out"
                       in
+                      let params_pat =
+                        List.map ~f:(fun param -> param.pat) params
+                      in
                       let pat = U.make_var_pat out_ident body.typ body.span in
                       let typ = body.typ in
                       let out = { pat; typ; typ_span = None; attrs = [] } in
-                      let post =
-                        let f =
-                          Attrs.associated_expr ~keep_last_args:1 Ensures
-                            item.ii_attrs
-                          |> Option.value
-                               ~default:
-                                 {
-                                   default with
-                                   e =
-                                     Closure
-                                       {
-                                         params = [ pat ];
-                                         body = default;
-                                         captures = [];
-                                       };
-                                 }
-                        in
-                        let span = f.span in
-                        let args = [ { span; typ; e = LocalVar out_ident } ] in
-                        let e =
-                          App { f; args; generic_args = []; impl = None }
-                        in
-                        { f with e } |> U.beta_reduce1_closure
-                      in
                       [
                         {
                           (mk "pre") with
@@ -114,7 +93,8 @@ module Make (F : Features.T) =
                             IIFn
                               {
                                 body =
-                                  Attrs.associated_expr Requires item.ii_attrs
+                                  Attrs.associated_expr_rebinding params_pat
+                                    Requires item.ii_attrs
                                   |> Option.value ~default;
                                 params;
                               };
@@ -124,7 +104,10 @@ module Make (F : Features.T) =
                           ii_v =
                             IIFn
                               {
-                                body = post |> U.beta_reduce1_closure;
+                                body =
+                                  Attrs.associated_expr_rebinding
+                                    (params_pat @ [ pat ]) Ensures item.ii_attrs
+                                  |> Option.value ~default;
                                 params = params @ [ out ];
                               };
                         };

From b049b24e7d67d18cbd702614dca68ed606163411 Mon Sep 17 00:00:00 2001
From: Lucas Franceschino <lucas@cryspen.com>
Date: Wed, 6 Mar 2024 11:06:05 +0100
Subject: [PATCH 24/24] feat(macros/example): refined arithmetic traits

---
 proof-libs/fstar/core/Core.Ops.Arith.fsti     | 31 +++++++++++++++----
 .../toolchain__attributes into-fstar.snap     | 28 +++++++++++++++++
 tests/attributes/src/lib.rs                   | 24 ++++++++++++++
 3 files changed, 77 insertions(+), 6 deletions(-)

diff --git a/proof-libs/fstar/core/Core.Ops.Arith.fsti b/proof-libs/fstar/core/Core.Ops.Arith.fsti
index 8ebc5c42a..1df19aed9 100644
--- a/proof-libs/fstar/core/Core.Ops.Arith.fsti
+++ b/proof-libs/fstar/core/Core.Ops.Arith.fsti
@@ -3,14 +3,33 @@ open Rust_primitives
 
 
 class t_Add self rhs = {
-   add_output: Type;
-   add_in_bounds: self -> rhs -> Type0;
-   ( +! ): x:self -> y:rhs {add_in_bounds x y} -> add_output;
+   [@@@ Tactics.Typeclasses.no_method]
+   f_Output: Type;
+   f_add_pre: self -> rhs -> bool;
+   f_add_post: self -> rhs -> f_Output -> bool;
+   f_add: x:self -> y:rhs -> Pure f_Output (f_add_pre x y) (fun r -> f_add_post x y r);
 }
 
 class t_Sub self rhs = {
-   sub_output: Type;
-   sub_in_bounds: self -> rhs -> Type0;
-   ( -! ): x:self -> y:rhs {sub_in_bounds x y} -> sub_output;
+   [@@@ Tactics.Typeclasses.no_method]
+   f_Output: Type;
+   f_sub_pre: self -> rhs -> bool;
+   f_sub_post: self -> rhs -> f_Output -> bool;
+   f_sub: x:self -> y:rhs -> Pure f_Output (f_sub_pre x y) (fun r -> f_sub_post x y r);
 }
 
+class t_Mul self rhs = {
+   [@@@ Tactics.Typeclasses.no_method]
+   f_Output: Type;
+   f_mul_pre: self -> rhs -> bool;
+   f_mul_post: self -> rhs -> f_Output -> bool;
+   f_mul: x:self -> y:rhs -> Pure f_Output (f_mul_pre x y) (fun r -> f_mul_post x y r);
+}
+
+class t_Div self rhs = {
+   [@@@ Tactics.Typeclasses.no_method]
+   f_Output: Type;
+   f_div_pre: self -> rhs -> bool;
+   f_div_post: self -> rhs -> f_Output -> bool;
+   f_div: x:self -> y:rhs -> Pure f_Output (f_div_pre x y) (fun r -> f_div_post x y r);
+}
diff --git a/test-harness/src/snapshots/toolchain__attributes into-fstar.snap b/test-harness/src/snapshots/toolchain__attributes into-fstar.snap
index bd83f3e65..8fbe4552b 100644
--- a/test-harness/src/snapshots/toolchain__attributes into-fstar.snap	
+++ b/test-harness/src/snapshots/toolchain__attributes into-fstar.snap	
@@ -53,6 +53,34 @@ let impl_1 (#v_T: Type) (#[FStar.Tactics.Typeclasses.tcresolve ()] i0: Core.Mark
     f_index = fun (self: t_Array v_T (sz 10)) (index: t_SafeIndex) -> self.[ index.f_i ]
   }
 '''
+"Attributes.Refined_arithmetic.fst" = '''
+module Attributes.Refined_arithmetic
+#set-options "--fuel 0 --ifuel 1 --z3rlimit 15"
+open Core
+open FStar.Mul
+
+type t_Foo = | Foo : u8 -> t_Foo
+
+[@@ FStar.Tactics.Typeclasses.tcinstance]
+let impl: Core.Ops.Arith.t_Add t_Foo t_Foo =
+  {
+    f_Output = t_Foo;
+    f_add_pre = (fun (self: t_Foo) (rhs: t_Foo) -> self._0 <. (255uy -! rhs._0 <: u8));
+    f_add_post = (fun (self: t_Foo) (rhs: t_Foo) (out: t_Foo) -> true);
+    f_add = fun (self: t_Foo) (rhs: t_Foo) -> Foo (self._0 +! rhs._0) <: t_Foo
+  }
+
+[@@ FStar.Tactics.Typeclasses.tcinstance]
+let impl_1: Core.Ops.Arith.t_Mul t_Foo t_Foo =
+  {
+    f_Output = t_Foo;
+    f_mul_pre
+    =
+    (fun (self: t_Foo) (rhs: t_Foo) -> rhs._0 =. 0uy || self._0 <. (255uy /! rhs._0 <: u8));
+    f_mul_post = (fun (self: t_Foo) (rhs: t_Foo) (out: t_Foo) -> true);
+    f_mul = fun (self: t_Foo) (rhs: t_Foo) -> Foo (self._0 *! rhs._0) <: t_Foo
+  }
+'''
 "Attributes.Refined_indexes.fst" = '''
 module Attributes.Refined_indexes
 #set-options "--fuel 0 --ifuel 1 --z3rlimit 15"
diff --git a/tests/attributes/src/lib.rs b/tests/attributes/src/lib.rs
index 90299c046..24705f8ce 100644
--- a/tests/attributes/src/lib.rs
+++ b/tests/attributes/src/lib.rs
@@ -40,6 +40,30 @@ impl Foo {
     fn h(&self) {}
 }
 
+#[hax::attributes]
+mod refined_arithmetic {
+    use core::ops::{Add, Mul};
+    use hax_lib_macros as hax;
+
+    struct Foo(u8);
+
+    impl Add for Foo {
+        type Output = Foo;
+        #[requires(self.0 < 255 - rhs.0)]
+        fn add(self, rhs: Foo) -> Foo {
+            Foo(self.0 + rhs.0)
+        }
+    }
+
+    impl Mul for Foo {
+        type Output = Foo;
+        #[requires(rhs.0 == 0 || self.0 < 255 / rhs.0)]
+        fn mul(self, rhs: Foo) -> Foo {
+            Foo(self.0 * rhs.0)
+        }
+    }
+}
+
 mod refined_indexes {
     use hax_lib_macros as hax;
     const MAX: usize = 10;