From 85341eecdc896ed40285fd885b243770fc4d7908 Mon Sep 17 00:00:00 2001
From: Jonathan Protzenko <protz@microsoft.com>
Date: Wed, 10 Jul 2024 09:51:01 -0700
Subject: [PATCH 01/52] A test, some thoughts, and a removal of mut by default
 in preparation for the new mut-inference phase

---
 lib/AstToMiniRust.ml    | 28 +++++++++++++---------------
 lib/OptimizeMiniRust.ml | 30 ++++++++++++++++++++++++++++++
 test/Rust7.fst          | 23 +++++++++++++++++++++++
 3 files changed, 66 insertions(+), 15 deletions(-)
 create mode 100644 lib/OptimizeMiniRust.ml
 create mode 100644 test/Rust7.fst

diff --git a/lib/AstToMiniRust.ml b/lib/AstToMiniRust.ml
index dc64d70b..07dd12f9 100644
--- a/lib/AstToMiniRust.ml
+++ b/lib/AstToMiniRust.ml
@@ -411,10 +411,7 @@ let translate_unknown_lid (m, n) =
   List.map String.lowercase_ascii m @ [ n ]
 
 let borrow_kind_of_bool b: MiniRust.borrow_kind =
-  if b (* const *) then
-    Shared
-  else
-    Mut
+  Shared
 
 type config = {
   box: bool;
@@ -615,9 +612,9 @@ and translate_expr_with_type (env: env) (e: Ast.expr) (t_ret: MiniRust.typ): env
            do retain them in our Function type -- so we need to relax the comparison here *)
         x
     (* More conversions due to box-ing types. *)
-    | _, App (Name (["Box"], _), [Slice _]), Ref (_, Mut, Slice _) ->
-        Borrow (Mut, Deref x)
-    | _, Ref (_, Mut, Slice _), App (Name (["Box"], _), [Slice _]) ->
+    | _, App (Name (["Box"], _), [Slice _]), Ref (_, k, Slice _) ->
+        Borrow (k, Deref x)
+    | _, Ref (_, _, Slice _), App (Name (["Box"], _), [Slice _]) ->
         MethodCall (Borrow (Shared, Deref x), ["into"], [])
     | _, Ref (_, Shared, Slice _), App (Name (["Box"], _), [Slice _]) ->
         MethodCall (x, ["into"], [])
@@ -625,8 +622,7 @@ and translate_expr_with_type (env: env) (e: Ast.expr) (t_ret: MiniRust.typ): env
         MethodCall (MethodCall (x, ["try_into"], []), ["unwrap"], [])
 
     (* More conversions due to vec-ing types *)
-    | _, Ref (_, Mut, Slice _), Vec _
-    | _, Ref (_, Shared, Slice _), Vec _ ->
+    | _, Ref (_, _, Slice _), Vec _ ->
         MethodCall (x, ["to_vec"], [])
     | _, Array _, Vec _ ->
         Call (Name ["Vec"; "from"], [], [x])
@@ -644,8 +640,8 @@ and translate_expr_with_type (env: env) (e: Ast.expr) (t_ret: MiniRust.typ): env
     | _, Ref (_, _, t), t' when t = t' ->
       Deref x
 
-    | Borrow (Mut, e) , Ref (_, _, t), Ref (_, _, Slice t') when t = t' ->
-        Borrow (Mut, Array (List [ e ]))
+    | Borrow (k, e) , Ref (_, _, t), Ref (_, _, Slice t') when t = t' ->
+        Borrow (k, Array (List [ e ]))
 
     | _ ->
         (* If we reach this case, we perform one last try by erasing the lifetime
@@ -832,7 +828,7 @@ and translate_expr_with_type (env: env) (e: Ast.expr) (t_ret: MiniRust.typ): env
 
       let env, e1, t = translate_array env false init in
       (* KPrint.bprintf "Let %s: %a\n" b.node.name PrintMiniRust.ptyp t; *)
-      let binding: MiniRust.binding = { name = b.node.name; typ = t; mut = true } in
+      let binding: MiniRust.binding = { name = b.node.name; typ = t; mut = false } in
       let env = push env binding in
       env0, Let (binding, e1, snd (translate_expr_with_type env e2 t_ret))
 
@@ -847,6 +843,8 @@ and translate_expr_with_type (env: env) (e: Ast.expr) (t_ret: MiniRust.typ): env
         | TQualified lid when Idents.LidSet.mem lid env.heap_structs -> true
         | _ -> false
       in
+      (* TODO how does this play out with the new "translate as non-mut by
+         default" strategy? *)
       let mut = b.node.mut || is_owned_struct in
       (* Here, the idea is to detect forbidden move-outs that are certain to result in a compilation
          error. Typically, selecting a field, dereferencing an array, etc. when the underlying type
@@ -858,7 +856,7 @@ and translate_expr_with_type (env: env) (e: Ast.expr) (t_ret: MiniRust.typ): env
          cannot be mutated in place in Low*, so it's ok to borrow instead of copy. *)
       let e1, t = match e1 with
         | (Field _ | Index _) when is_owned_struct ->
-            MiniRust.(Borrow (Mut, e1), Ref (None, Mut, t))
+            MiniRust.(Borrow (Shared, e1), Ref (None, Shared, t))
         | _ ->
             e1, t
       in
@@ -907,7 +905,7 @@ and translate_expr_with_type (env: env) (e: Ast.expr) (t_ret: MiniRust.typ): env
       in
       let env, e1 = translate_expr env e1 in
       let env, e2 = translate_expr_with_type env e2 (Constant SizeT) in
-      env, Borrow ((if is_const_tbuf then Shared else Mut), Index (e1, Range (Some e2, None, false)))
+      env, Borrow (Shared, Index (e1, Range (Some e2, None, false)))
   | EBufDiff _ ->
       failwith "unexpected: EBufDiff"
   (* Silly pattern in Low*: for historical reasons, the blit operations takes a
@@ -944,7 +942,7 @@ and translate_expr_with_type (env: env) (e: Ast.expr) (t_ret: MiniRust.typ): env
       (* Rather than error out, we do nothing, as some functions may allocate then free. *)
       env, Unit
   | EBufNull ->
-      env, possibly_convert (Borrow (Mut, Array (List []))) (translate_type env e.typ)
+      env, possibly_convert (Borrow (Shared, Array (List []))) (translate_type env e.typ)
   | EPushFrame ->
       failwith "unexpected: EPushFrame"
   | EPopFrame ->
diff --git a/lib/OptimizeMiniRust.ml b/lib/OptimizeMiniRust.ml
new file mode 100644
index 00000000..76ec9115
--- /dev/null
+++ b/lib/OptimizeMiniRust.ml
@@ -0,0 +1,30 @@
+(* AstToMiniRust generates code that only uses shared borrows; that is obviously
+   incorrect, and so the purpose of this phase is to infer the minimum number of
+   variables that need to be marked as `mut`, and the minimum number of borrows
+   that need themselves to be `&mut`.
+
+   This improves on an earlier iteration of the compilation scheme where
+   everything was marked as mutable by default, a conservative, but suboptimal
+   choice.
+
+   We proceed as follows. We carry two sets of variables:
+   - V stands for mutable variables, i.e. the set of variables that need to
+     marked as mut using `let mut x = ...`. A variable needs to be marked as mut
+     if it is mutably-borrowed, i.e. if `&mut x` occurs.
+   - R stands for mutable references, i.e. the set of variables that have type
+     `&mut T`. R is initially populated with function parameters.
+   This is the state of our transformation, and as such, we return an augmented
+   state after performing our inference, so that the callee can mark variables
+   accordingly.
+
+   An environment keeps track of the functions that have been visited already,
+   along with their updated types.
+
+   Finally, the transformation receives a mode as an input parameter; if the
+   mode is Mut, then the subexpression being visited (e.g. &x) needs to return a
+   mutable borrow, meaning it gets rewritten (e.g. into &mut x) and the set V
+   increases (because the Rust rule is that you can only write `&mut x` if `x`
+   itself is declared with `let mut`).
+*)
+
+let rec infer_mut_borrows = false
diff --git a/test/Rust7.fst b/test/Rust7.fst
new file mode 100644
index 00000000..e147d622
--- /dev/null
+++ b/test/Rust7.fst
@@ -0,0 +1,23 @@
+module Rust7
+
+module U32 = FStar.UInt32
+module B = LowStar.Buffer
+
+open FStar.HyperStack.ST
+
+val add_carry_u32:
+  x:U32.t
+  -> y:U32.t
+  -> r:B.lbuffer U32.t 1 ->
+  Stack U32.t
+  (requires fun h -> B.live h r)
+  (ensures  fun h0 c h1 -> True)
+    // modifies1 r h0 h1 /\ v c <= 1 /\
+    // (let r = Seq.index (as_seq h1 r) 0 in
+    // v r + v c * pow2 (bits t) == v x + v y + v cin))
+
+let add_carry_u32 x y r =
+  let res = U32.add_mod x y in
+  // let c = (U32.shift_right res 32ul) in
+  B.upd r 0ul res;
+  0ul

From 64a869437887e71d8c6ffc28021f54c022b19e72 Mon Sep 17 00:00:00 2001
From: Jonathan Protzenko <protz@microsoft.com>
Date: Wed, 10 Jul 2024 10:08:49 -0700
Subject: [PATCH 02/52] Locally nameless name management for MiniRust, too

---
 lib/AstToMiniRust.ml |  12 ++---
 lib/MiniRust.ml      | 117 ++++++++++++++++++++++++++++++-------------
 lib/PrintMiniRust.ml |   2 +
 3 files changed, 88 insertions(+), 43 deletions(-)

diff --git a/lib/AstToMiniRust.ml b/lib/AstToMiniRust.ml
index 07dd12f9..ac850ba6 100644
--- a/lib/AstToMiniRust.ml
+++ b/lib/AstToMiniRust.ml
@@ -410,7 +410,7 @@ let translate_unknown_lid (m, n) =
   let m = compress_prefix m in
   List.map String.lowercase_ascii m @ [ n ]
 
-let borrow_kind_of_bool b: MiniRust.borrow_kind =
+let borrow_kind_of_bool _b: MiniRust.borrow_kind =
   Shared
 
 type config = {
@@ -587,7 +587,7 @@ and translate_array (env: env) is_toplevel (init: Ast.expr): env * MiniRust.expr
    necessitate the insertion of conversions *)
 and translate_expr_with_type (env: env) (e: Ast.expr) (t_ret: MiniRust.typ): env * MiniRust.expr =
   let erase_lifetime_info = (object(self)
-    inherit [_] MiniRust.map
+    inherit [_] MiniRust.DeBruijn.map
     method! visit_Ref env _ bk t = Ref (None, bk, self#visit_typ env t)
     method! visit_tname _ n _ = Name (n, [])
   end)#visit_typ ()
@@ -616,8 +616,8 @@ and translate_expr_with_type (env: env) (e: Ast.expr) (t_ret: MiniRust.typ): env
         Borrow (k, Deref x)
     | _, Ref (_, _, Slice _), App (Name (["Box"], _), [Slice _]) ->
         MethodCall (Borrow (Shared, Deref x), ["into"], [])
-    | _, Ref (_, Shared, Slice _), App (Name (["Box"], _), [Slice _]) ->
-        MethodCall (x, ["into"], [])
+    (* | _, Ref (_, Shared, Slice _), App (Name (["Box"], _), [Slice _]) -> *)
+    (*     MethodCall (x, ["into"], []) *)
     | _, Vec _, App (Name (["Box"], _), [Slice _]) ->
         MethodCall (MethodCall (x, ["try_into"], []), ["unwrap"], [])
 
@@ -899,10 +899,6 @@ and translate_expr_with_type (env: env) (e: Ast.expr) (t_ret: MiniRust.typ): env
       (* This is a fallback for the analysis above. Happens if, for instance, the pointer arithmetic
          appears in subexpression position (like, function call), in which case there's a chance
          this might still work! *)
-      let is_const_tbuf = match e1.typ with
-        | TBuf (_, b) -> b
-        | _ -> false
-      in
       let env, e1 = translate_expr env e1 in
       let env, e2 = translate_expr_with_type env e2 (Constant SizeT) in
       env, Borrow (Shared, Index (e1, Range (Some e2, None, false)))
diff --git a/lib/MiniRust.ml b/lib/MiniRust.ml
index 0fc57af7..eba20cbc 100644
--- a/lib/MiniRust.ml
+++ b/lib/MiniRust.ml
@@ -90,6 +90,7 @@ and expr =
 
   (* Place expressions *)
   | Var of db_index
+  | Open of open_var
   | Index of expr * expr
   | Field of expr * string
 
@@ -104,6 +105,12 @@ and pat =
   | Wildcard
   | StructP of name (* TODO *)
 
+and open_var = {
+  name: string;
+  atom: atom_t
+}
+
+and atom_t = Atom.t [@ visitors.opaque]
 
 (* TODO: visitors incompatible with inline records *)
 type decl =
@@ -158,48 +165,88 @@ and trait =
 
 (* Some visitors for name management *)
 
-(* A usable map where the user can hook up to extend, called every time a new
-   binding is added to the environment *)
-class ['self] map = object (self: 'self)
-  inherit [_] map_expr as super
-
-  (* To be overridden by the user *)
-  method extend env _ = env
+module DeBruijn = struct
+
+  (* A usable map where the user can hook up to extend, called every time a new
+     binding is added to the environment *)
+  class ['self] map = object (self: 'self)
+    inherit [_] map_expr as super
+
+    (* To be overridden by the user *)
+    method extend env _ = env
+
+    (* We list all binding nodes and feed those binders to the environment *)
+    method! visit_Let env b e1 e2 =
+      super#visit_Let (self#extend env b) b e1 e2
+
+    method! visit_For env b e1 e2 =
+      super#visit_For (self#extend env b) b e1 e2
+  end
+
+  class map_counting = object
+    (* The environment [i] has type [int]. *)
+    inherit [_] map
+
+    (* The environment [i] keeps track of how many binders have been
+       entered. It is incremented at each binder. *)
+    method! extend (i: int) (_: binding) =
+      i + 1
+  end
+
+  class lift (k: int) = object
+    inherit map_counting
+    (* A local variable (one that is less than [i]) is unaffected;
+       a free variable is lifted up by [k]. *)
+    method! visit_Var i j =
+      if j < i then
+        Var j
+      else
+        Var (j + k)
+  end
+
+  class close (a: Atom.t) (e: expr) = object
+    inherit map_counting
+
+    method! visit_Open i ({ atom; _ } as v) =
+      if Atom.equal a atom then
+        (new lift i)#visit_expr 0 e
+      else
+        Open v
+  end
+
+  class subst e2 = object
+    inherit map_counting
+
+    method! visit_Var i j =
+      if j = i then
+        (new lift i)#visit_expr 0 e2
+      else
+        Var (if j < i then j else j - 1)
+  end
 
-  (* We list all binding nodes and feed those binders to the environment *)
-  method! visit_Let env b e1 e2 =
-    super#visit_Let (self#extend env b) b e1 e2
-
-  method! visit_For env b e1 e2 =
-    super#visit_For (self#extend env b) b e1 e2
-end
-
-class map_counting = object
-  (* The environment [i] has type [int]. *)
-  inherit [_] map
-
-  (* The environment [i] keeps track of how many binders have been
-     entered. It is incremented at each binder. *)
-  method! extend (i: int) (_: binding) =
-    i + 1
-end
-
-class lift (k: int) = object
-  inherit map_counting
-  (* A local variable (one that is less than [i]) is unaffected;
-     a free variable is lifted up by [k]. *)
-  method! visit_Var i j =
-    if j < i then
-      Var j
-    else
-      Var (j + k)
 end
 
+(* Lift `expr` by `k` places so as to place it underneath `k` additional
+   binders. *)
 let lift (k: int) (expr: expr): expr =
   if k = 0 then
     expr
   else
-    (new lift k)#visit_expr 0 expr
+    (new DeBruijn.lift k)#visit_expr 0 expr
+
+(* Close `a`, replacing it on the fly with `e2` in `e1` *)
+let close a e2 e1 =
+  (new DeBruijn.close a e2)#visit_expr 0 e1
+
+(* Substitute `e2` for bound variable `i` in `e1` *)
+let subst e2 i e1 =
+  (new DeBruijn.subst e2)#visit_expr i e1
+
+(* Open b in e2, replacing occurrences of a bound variable with the
+   corresponding atom. *)
+let open_ (b: binding) e2 =
+  let atom = Atom.fresh () in
+  atom, subst (Open { atom; name = b.name }) 0 e2
 
 (* Helpers *)
 
diff --git a/lib/PrintMiniRust.ml b/lib/PrintMiniRust.ml
index 744ca0aa..6a119e65 100644
--- a/lib/PrintMiniRust.ml
+++ b/lib/PrintMiniRust.ml
@@ -442,6 +442,8 @@ and print_expr env (context: int) (e: expr): document =
           group (print_pat env p ^/^ string "=>") ^^ group (nest 2 (break1 ^^ print_expr env max_int e))
       ) patexprs)
 
+  | Open { name; _ } -> string name
+
 and print_pat env (p: pat) =
   match p with
   | Literal c -> print_constant c

From b7e3c2ea01fd8f772bf3e7e45e53cf724c103ed8 Mon Sep 17 00:00:00 2001
From: Jonathan Protzenko <protz@microsoft.com>
Date: Wed, 10 Jul 2024 14:07:57 -0700
Subject: [PATCH 03/52] WIP

---
 lib/AstToMiniRust.ml    |  8 ++--
 lib/MiniRust.ml         |  9 ++++-
 lib/OptimizeMiniRust.ml | 88 ++++++++++++++++++++++++++++++++++++++---
 3 files changed, 94 insertions(+), 11 deletions(-)

diff --git a/lib/AstToMiniRust.ml b/lib/AstToMiniRust.ml
index ac850ba6..2b6d7770 100644
--- a/lib/AstToMiniRust.ml
+++ b/lib/AstToMiniRust.ml
@@ -723,8 +723,9 @@ and translate_expr_with_type (env: env) (e: Ast.expr) (t_ret: MiniRust.typ): env
 
   | EApp ({ node = EQualified ([ "LowStar"; "BufferOps" ], s); _ }, e1 :: e2 :: _ ) when KString.starts_with s "op_Star_Equals__" ->
       let env, e1 = translate_expr env e1 in
+      let t2 = translate_type env e2.typ in
       let env, e2 = translate_expr env e2 in
-      env, Assign (Index (e1, MiniRust.zero_usize), e2)
+      env, Assign (Index (e1, MiniRust.zero_usize), e2, t2)
 
   | EApp ({ node = ETApp (e, cgs, cgs', ts); _ }, es) ->
       assert (cgs @ cgs' = []);
@@ -881,7 +882,7 @@ and translate_expr_with_type (env: env) (e: Ast.expr) (t_ret: MiniRust.typ): env
       in
       let env, e1 = translate_expr_with_type env e1 lvalue_type in
       let env, e2 = translate_expr_with_type env e2 lvalue_type in
-      env, Assign (e1, e2)
+      env, Assign (e1, e2, translate_type env lvalue_type)
   | EBufCreate _ ->
       failwith "unexpected: EBufCreate"
   | EBufCreateL _ ->
@@ -893,8 +894,9 @@ and translate_expr_with_type (env: env) (e: Ast.expr) (t_ret: MiniRust.typ): env
   | EBufWrite (e1, e2, e3) ->
       let env, e1 = translate_expr env e1 in
       let env, e2 = translate_expr_with_type env e2 (Constant SizeT) in
+      let t3 = translate_type env e3.typ in
       let env, e3 = translate_expr env e3 in
-      env, Assign (Index (e1, e2), e3)
+      env, Assign (Index (e1, e2), e3, t3)
   | EBufSub (e1, e2) ->
       (* This is a fallback for the analysis above. Happens if, for instance, the pointer arithmetic
          appears in subexpression position (like, function call), in which case there's a chance
diff --git a/lib/MiniRust.ml b/lib/MiniRust.ml
index eba20cbc..b81b00cb 100644
--- a/lib/MiniRust.ml
+++ b/lib/MiniRust.ml
@@ -1,5 +1,10 @@
 (* A minimalistic representation of Rust *)
 
+module Name = struct
+  type t = string list
+  let compare = compare
+end
+
 type borrow_kind_ = Mut | Shared
 [@@deriving show]
 
@@ -7,7 +12,7 @@ type borrow_kind = borrow_kind_ [@ opaque ]
 and constant = Constant.t [@ opaque ]
 and width = Constant.width [@ opaque ]
 and op = Constant.op [@ opaque ]
-and name = string list [@ opaque ]
+and name = Name.t [@ opaque ]
 
 (* Some design choices.
    - We don't intend to perform any deep semantic transformations on this Rust
@@ -79,7 +84,7 @@ and expr =
   | Unit
   | Panic of string
   | IfThenElse of expr * expr * expr option
-  | Assign of expr * expr
+  | Assign of expr * expr * typ
   | As of expr * typ
   | For of binding * expr * expr
   | While of expr * expr
diff --git a/lib/OptimizeMiniRust.ml b/lib/OptimizeMiniRust.ml
index 76ec9115..051e5d9f 100644
--- a/lib/OptimizeMiniRust.ml
+++ b/lib/OptimizeMiniRust.ml
@@ -20,11 +20,87 @@
    An environment keeps track of the functions that have been visited already,
    along with their updated types.
 
-   Finally, the transformation receives a mode as an input parameter; if the
-   mode is Mut, then the subexpression being visited (e.g. &x) needs to return a
-   mutable borrow, meaning it gets rewritten (e.g. into &mut x) and the set V
-   increases (because the Rust rule is that you can only write `&mut x` if `x`
-   itself is declared with `let mut`).
+   Finally, the transformation receives a contextual flag as an input parameter;
+   the flag indicates whether the subexpression being visited (e.g. &x) needs to
+   return a mutable borrow, meaning it gets rewritten (e.g. into &mut x) and the
+   set V increases (because the Rust rule is that you can only write `&mut x` if
+   `x` itself is declared with `let mut`).
 *)
 
-let rec infer_mut_borrows = false
+open MiniRust
+
+module NameMap = Map.Make(Name)
+module VarSet = Set.Make(Atom)
+
+type env = {
+  seen: typ list NameMap.t
+}
+
+type known = {
+  v: VarSet.t;
+  r: VarSet.t;
+}
+
+let add_mut_var a known =
+  { known with v = VarSet.add a v }
+
+let add_mut_borrow a known =
+  { known with r = VarSet.add a r }
+
+let want_mut_var a known =
+  VarSet.mem a known.v
+
+let want_mut_borrow a known =
+  VarSet.mem a known.r
+
+let is_mut_borrow = function
+  | Borrow (Mut, _) -> true
+  | _ -> false
+
+let make_mut_borrow = function
+  | Borrow (_, t) -> Borrow (Mut, t)
+  | _ -> failwith "impossible: make_mut_borrow"
+
+let assert_borrow = function
+  | Borrow (_, t) -> t
+  | _ -> failwith "impossible: assert_borrow"
+
+let rec infer (env: env) (expected: typ) (known: known) (e: expr): known * expr =
+  match expr with
+  | Borrow (k, e) ->
+      (* If we expect this borrow to be a mutable borrow, then we make it a mutable borrow
+         (obviously!), and also remember that the variable x itself needs to be `let mut` *)
+      if is_mut_borrow expected then
+        match e with
+        | Var _ ->
+            failwith "impossible: missing open"
+        | Open { atom; _ } ->
+            add_mut_var atom known, Borrow (Mut, e)
+        | _ ->
+            failwith "TODO: borrowing something other than a variable"
+      else
+        let known, e = infer env (assert_borrow expected) known e in
+        known, Borrow (k, e)
+
+  | Open { atom; _ } ->
+      (* If we expect this variable to be a mutable borrow, then we remember it and let the caller
+         act accordingly. *)
+      if need = MakeMut then
+        add_mut_borrow atom known, expr
+      else
+        expr
+
+  | Let (b, e1, e2) ->
+      let a, e2 = open_ b e2 in
+      let known, e2 = infer env need known e2 in
+      let mut = want_mut_var a known in
+      let t1 = if want_mut_borrow a known then make_mut_borrow b.typ else b.typ in
+      let known, e1 = infer env typ e1 in
+      known, Let ({ b with mut; typ = t1 }, e1, close a (Var 0) e2)
+
+  | Call (Name n, targs, es) ->
+      if NameMap.mem env.seen n then
+        let ts = NameMap.find env.seen n in
+        let known, es = List.fold_left (fun (known, es) e ->
+          let known, e = 
+

From cdbe9e16815d04e6c59a0f31b3c45d9defd82866 Mon Sep 17 00:00:00 2001
From: Jonathan Protzenko <protz@microsoft.com>
Date: Thu, 11 Jul 2024 13:32:21 -0700
Subject: [PATCH 04/52] wip

---
 lib/AstToMiniRust.ml    | 12 +++---
 lib/MiniRust.ml         |  1 +
 lib/OptimizeMiniRust.ml | 95 +++++++++++++++++++++++++++++++++--------
 lib/PrintMiniRust.ml    |  3 +-
 src/Karamel.ml          |  1 +
 5 files changed, 87 insertions(+), 25 deletions(-)

diff --git a/lib/AstToMiniRust.ml b/lib/AstToMiniRust.ml
index 2b6d7770..4222baf4 100644
--- a/lib/AstToMiniRust.ml
+++ b/lib/AstToMiniRust.ml
@@ -725,7 +725,7 @@ and translate_expr_with_type (env: env) (e: Ast.expr) (t_ret: MiniRust.typ): env
       let env, e1 = translate_expr env e1 in
       let t2 = translate_type env e2.typ in
       let env, e2 = translate_expr env e2 in
-      env, Assign (Index (e1, MiniRust.zero_usize), e2, t2)
+      env, Assign (IndexMut (e1, MiniRust.zero_usize), e2, t2)
 
   | EApp ({ node = ETApp (e, cgs, cgs', ts); _ }, es) ->
       assert (cgs @ cgs' = []);
@@ -882,7 +882,7 @@ and translate_expr_with_type (env: env) (e: Ast.expr) (t_ret: MiniRust.typ): env
       in
       let env, e1 = translate_expr_with_type env e1 lvalue_type in
       let env, e2 = translate_expr_with_type env e2 lvalue_type in
-      env, Assign (e1, e2, translate_type env lvalue_type)
+      env, Assign (e1, e2, lvalue_type)
   | EBufCreate _ ->
       failwith "unexpected: EBufCreate"
   | EBufCreateL _ ->
@@ -896,7 +896,7 @@ and translate_expr_with_type (env: env) (e: Ast.expr) (t_ret: MiniRust.typ): env
       let env, e2 = translate_expr_with_type env e2 (Constant SizeT) in
       let t3 = translate_type env e3.typ in
       let env, e3 = translate_expr env e3 in
-      env, Assign (Index (e1, e2), e3, t3)
+      env, Assign (IndexMut (e1, e2), e3, t3)
   | EBufSub (e1, e2) ->
       (* This is a fallback for the analysis above. Happens if, for instance, the pointer arithmetic
          appears in subexpression position (like, function call), in which case there's a chance
@@ -919,7 +919,7 @@ and translate_expr_with_type (env: env) (e: Ast.expr) (t_ret: MiniRust.typ): env
       let env, dst_index = translate_expr_with_type env dst_index (Constant SizeT) in
       let env, len = translate_expr_with_type env len (Constant SizeT) in
       env, MethodCall (
-        Index (dst, H.range_with_len dst_index len),
+        IndexMut (dst, H.range_with_len dst_index len),
         [ "copy_from_slice" ],
         [ Borrow (Shared, Index (src, H.range_with_len src_index len)) ])
   | EBufFill (dst, elt, len) ->
@@ -928,12 +928,12 @@ and translate_expr_with_type (env: env) (e: Ast.expr) (t_ret: MiniRust.typ): env
       let env, len = translate_expr_with_type env len (Constant SizeT) in
       if H.is_const len then
         env, MethodCall (
-          Index (dst, H.range_with_len (Constant (SizeT, "0")) len),
+          IndexMut (dst, H.range_with_len (Constant (SizeT, "0")) len),
           [ "copy_from_slice" ],
           [ Borrow (Shared, Array (Repeat (elt, len))) ])
       else
         env, MethodCall (
-          Index (dst, H.range_with_len (Constant (SizeT, "0")) len),
+          IndexMut (dst, H.range_with_len (Constant (SizeT, "0")) len),
           [ "copy_from_slice" ],
           [ Borrow (Shared, VecNew (Repeat (elt, len))) ])
   | EBufFree _ ->
diff --git a/lib/MiniRust.ml b/lib/MiniRust.ml
index b81b00cb..d7a1f64d 100644
--- a/lib/MiniRust.ml
+++ b/lib/MiniRust.ml
@@ -97,6 +97,7 @@ and expr =
   | Var of db_index
   | Open of open_var
   | Index of expr * expr
+  | IndexMut of expr * expr
   | Field of expr * string
 
   (* Operator expressions *)
diff --git a/lib/OptimizeMiniRust.ml b/lib/OptimizeMiniRust.ml
index 051e5d9f..f9122c06 100644
--- a/lib/OptimizeMiniRust.ml
+++ b/lib/OptimizeMiniRust.ml
@@ -42,10 +42,10 @@ type known = {
 }
 
 let add_mut_var a known =
-  { known with v = VarSet.add a v }
+  { known with v = VarSet.add a known.v }
 
 let add_mut_borrow a known =
-  { known with r = VarSet.add a r }
+  { known with r = VarSet.add a known.r }
 
 let want_mut_var a known =
   VarSet.mem a known.v
@@ -54,19 +54,19 @@ let want_mut_borrow a known =
   VarSet.mem a known.r
 
 let is_mut_borrow = function
-  | Borrow (Mut, _) -> true
+  | Ref (_, Mut, _) -> true
   | _ -> false
 
 let make_mut_borrow = function
-  | Borrow (_, t) -> Borrow (Mut, t)
+  | Ref (l, _, t) -> Ref (l, Mut, t)
   | _ -> failwith "impossible: make_mut_borrow"
 
 let assert_borrow = function
-  | Borrow (_, t) -> t
+  | Ref (_, _, t) -> t
   | _ -> failwith "impossible: assert_borrow"
 
 let rec infer (env: env) (expected: typ) (known: known) (e: expr): known * expr =
-  match expr with
+  match e with
   | Borrow (k, e) ->
       (* If we expect this borrow to be a mutable borrow, then we make it a mutable borrow
          (obviously!), and also remember that the variable x itself needs to be `let mut` *)
@@ -82,25 +82,84 @@ let rec infer (env: env) (expected: typ) (known: known) (e: expr): known * expr
         let known, e = infer env (assert_borrow expected) known e in
         known, Borrow (k, e)
 
-  | Open { atom; _ } ->
+  | Open { atom; _ } ->
       (* If we expect this variable to be a mutable borrow, then we remember it and let the caller
          act accordingly. *)
-      if need = MakeMut then
-        add_mut_borrow atom known, expr
+      if is_mut_borrow expected then
+        add_mut_borrow atom known, e
       else
-        expr
+        known, e
 
   | Let (b, e1, e2) ->
       let a, e2 = open_ b e2 in
-      let known, e2 = infer env need known e2 in
+      let known, e2 = infer env expected known e2 in
       let mut = want_mut_var a known in
       let t1 = if want_mut_borrow a known then make_mut_borrow b.typ else b.typ in
-      let known, e1 = infer env typ e1 in
-      known, Let ({ b with mut; typ = t1 }, e1, close a (Var 0) e2)
+      let known, e1 = infer env t1 known e1 in
+      known, Let ({ b with mut; typ = t1 }, e1, close a (Var 0) (lift 1 e2))
 
   | Call (Name n, targs, es) ->
-      if NameMap.mem env.seen n then
-        let ts = NameMap.find env.seen n in
-        let known, es = List.fold_left (fun (known, es) e ->
-          let known, e = 
-
+      if NameMap.mem n env.seen then
+        (* TODO: substitute targs in ts -- for now, we assume we don't have a type-polymorphic
+           function that gets instantiated with a reference type *)
+        let ts = NameMap.find n env.seen in
+        let known, es = List.fold_left2 (fun (known, es) e t ->
+            let known, e = infer env t known e in
+            known, e :: es
+          ) (known, []) es ts
+        in
+        let es = List.rev es in
+        known, Call (Name n, targs, es)
+      else
+        failwith "TODO: recursion"
+
+
+  | Assign (Open { atom; _ }, e3, t) ->
+      let known, e3 = infer env t known e3 in
+      add_mut_var atom known, e3
+
+  | Assign (IndexMut (Open { atom; _ } as e1, e2), e3, t) ->
+      let known = add_mut_borrow atom known in
+      let known, e2 = infer env usize known e2 in
+      let known, e3 = infer env t known e3 in
+      known, Assign (IndexMut (e1, e2), e3, t)
+
+  | Assign _ ->
+      failwith "TODO: unknown assignment"
+
+  | _ ->
+      failwith "TODO"
+
+let infer_mut_borrows files =
+  let env = { seen = NameMap.empty } in
+  let known = { v = VarSet.empty; r = VarSet.empty } in
+  let _, files =
+    List.fold_left (fun (env, files) (filename, decls) ->
+      let env, decls = List.fold_left (fun (env, decls) decl ->
+        match decl with
+        | Function ({ name; body; return_type; parameters; _ } as f) ->
+            let atoms, body =
+              List.fold_right (fun binder (atoms, e) ->
+                let a, e = open_ binder e in
+                a :: atoms, e
+              ) parameters ([], body)
+            in
+            let known, body = infer env return_type known body in
+            let parameters, body =
+              List.fold_right2 (fun (binder: binding) atom (parameters, e) ->
+                let e = close atom (Var 0) (lift 1 e) in
+                let mut = want_mut_var atom known in
+                let typ = if want_mut_borrow atom known then make_mut_borrow binder.typ else binder.typ in
+                { binder with mut; typ } :: parameters, e
+              ) parameters atoms ([], body)
+            in
+            let env = { seen = NameMap.add name (List.map (fun (x: binding) -> x.typ) parameters) env.seen } in
+            env, Function { f with body; parameters } :: decls
+        | _ ->
+            env, decl :: decls
+      ) (env, []) decls in
+      let decls = List.rev decls in
+      env, (filename, decls) :: files
+    ) (env, []) files
+  in
+  List.rev files
diff --git a/lib/PrintMiniRust.ml b/lib/PrintMiniRust.ml
index 6a119e65..ab0b5df6 100644
--- a/lib/PrintMiniRust.ml
+++ b/lib/PrintMiniRust.ml
@@ -372,7 +372,7 @@ and print_expr env (context: int) (e: expr): document =
       | None ->
           empty
       end
-  | Assign (e1, e2) ->
+  | Assign (e1, e2, _) ->
       let mine, left, right = 18, 17, 18 in
       paren_if mine @@
       group (print_expr env left e1 ^^ space ^^ equals ^^
@@ -423,6 +423,7 @@ and print_expr env (context: int) (e: expr): document =
       | `GoneUnit -> print env; failwith "unexpected: unit-returning computation was let-bound and used"
       end
 
+  | IndexMut (p, e)
   | Index (p, e) ->
       let mine = 4 in
       paren_if mine @@
diff --git a/src/Karamel.ml b/src/Karamel.ml
index 55f9104a..ec7eae24 100644
--- a/src/Karamel.ml
+++ b/src/Karamel.ml
@@ -750,6 +750,7 @@ Supported options:|}
     if Options.debug "rs" then
       print PrintAst.print_files files;
     let files = AstToMiniRust.translate_files files in
+    let files = OptimizeMiniRust.infer_mut_borrows files in
     OutputRust.write_all files
 
   else

From bbe0d0d360cf39b843655be6cd3d256f3fedd21a Mon Sep 17 00:00:00 2001
From: Jonathan Protzenko <protz@microsoft.com>
Date: Thu, 11 Jul 2024 14:03:55 -0700
Subject: [PATCH 05/52] WIP, need to debug stupid substitution functions sigh

---
 lib/AstToMiniRust.ml    | 10 ++---
 lib/MiniRust.ml         |  1 -
 lib/OptimizeMiniRust.ml | 81 +++++++++++++++++++++++++++++++++++++----
 lib/PrintMiniRust.ml    |  1 -
 4 files changed, 79 insertions(+), 14 deletions(-)

diff --git a/lib/AstToMiniRust.ml b/lib/AstToMiniRust.ml
index 4222baf4..96db52dc 100644
--- a/lib/AstToMiniRust.ml
+++ b/lib/AstToMiniRust.ml
@@ -725,7 +725,7 @@ and translate_expr_with_type (env: env) (e: Ast.expr) (t_ret: MiniRust.typ): env
       let env, e1 = translate_expr env e1 in
       let t2 = translate_type env e2.typ in
       let env, e2 = translate_expr env e2 in
-      env, Assign (IndexMut (e1, MiniRust.zero_usize), e2, t2)
+      env, Assign (Index (e1, MiniRust.zero_usize), e2, t2)
 
   | EApp ({ node = ETApp (e, cgs, cgs', ts); _ }, es) ->
       assert (cgs @ cgs' = []);
@@ -896,7 +896,7 @@ and translate_expr_with_type (env: env) (e: Ast.expr) (t_ret: MiniRust.typ): env
       let env, e2 = translate_expr_with_type env e2 (Constant SizeT) in
       let t3 = translate_type env e3.typ in
       let env, e3 = translate_expr env e3 in
-      env, Assign (IndexMut (e1, e2), e3, t3)
+      env, Assign (Index (e1, e2), e3, t3)
   | EBufSub (e1, e2) ->
       (* This is a fallback for the analysis above. Happens if, for instance, the pointer arithmetic
          appears in subexpression position (like, function call), in which case there's a chance
@@ -919,7 +919,7 @@ and translate_expr_with_type (env: env) (e: Ast.expr) (t_ret: MiniRust.typ): env
       let env, dst_index = translate_expr_with_type env dst_index (Constant SizeT) in
       let env, len = translate_expr_with_type env len (Constant SizeT) in
       env, MethodCall (
-        IndexMut (dst, H.range_with_len dst_index len),
+        Index (dst, H.range_with_len dst_index len),
         [ "copy_from_slice" ],
         [ Borrow (Shared, Index (src, H.range_with_len src_index len)) ])
   | EBufFill (dst, elt, len) ->
@@ -928,12 +928,12 @@ and translate_expr_with_type (env: env) (e: Ast.expr) (t_ret: MiniRust.typ): env
       let env, len = translate_expr_with_type env len (Constant SizeT) in
       if H.is_const len then
         env, MethodCall (
-          IndexMut (dst, H.range_with_len (Constant (SizeT, "0")) len),
+          Index (dst, H.range_with_len (Constant (SizeT, "0")) len),
           [ "copy_from_slice" ],
           [ Borrow (Shared, Array (Repeat (elt, len))) ])
       else
         env, MethodCall (
-          IndexMut (dst, H.range_with_len (Constant (SizeT, "0")) len),
+          Index (dst, H.range_with_len (Constant (SizeT, "0")) len),
           [ "copy_from_slice" ],
           [ Borrow (Shared, VecNew (Repeat (elt, len))) ])
   | EBufFree _ ->
diff --git a/lib/MiniRust.ml b/lib/MiniRust.ml
index d7a1f64d..b81b00cb 100644
--- a/lib/MiniRust.ml
+++ b/lib/MiniRust.ml
@@ -97,7 +97,6 @@ and expr =
   | Var of db_index
   | Open of open_var
   | Index of expr * expr
-  | IndexMut of expr * expr
   | Field of expr * string
 
   (* Operator expressions *)
diff --git a/lib/OptimizeMiniRust.ml b/lib/OptimizeMiniRust.ml
index f9122c06..6b8af704 100644
--- a/lib/OptimizeMiniRust.ml
+++ b/lib/OptimizeMiniRust.ml
@@ -45,9 +45,11 @@ let add_mut_var a known =
   { known with v = VarSet.add a known.v }
 
 let add_mut_borrow a known =
+  KPrint.bprintf "%s is &mut\n" (Ast.show_atom_t a);
   { known with r = VarSet.add a known.r }
 
 let want_mut_var a known =
+  KPrint.bprintf "%s is let mut\n" (Ast.show_atom_t a);
   VarSet.mem a known.v
 
 let want_mut_borrow a known =
@@ -93,10 +95,14 @@ let rec infer (env: env) (expected: typ) (known: known) (e: expr): known * expr
   | Let (b, e1, e2) ->
       let a, e2 = open_ b e2 in
       let known, e2 = infer env expected known e2 in
-      let mut = want_mut_var a known in
-      let t1 = if want_mut_borrow a known then make_mut_borrow b.typ else b.typ in
+      let mut_var = want_mut_var a known in
+      let mut_borrow = want_mut_borrow a known in
+      KPrint.bprintf "[infer-mut,let] %s[%s]: %a let mut ? %b &mut ? %b\n" b.name
+        (show_atom_t a)
+        PrintMiniRust.ptyp b.typ mut_var mut_borrow;
+      let t1 = if mut_borrow then make_mut_borrow b.typ else b.typ in
       let known, e1 = infer env t1 known e1 in
-      known, Let ({ b with mut; typ = t1 }, e1, close a (Var 0) (lift 1 e2))
+      known, Let ({ b with mut = mut_var; typ = t1 }, e1, close a (Var 0) (lift 1 e2))
 
   | Call (Name n, targs, es) ->
       if NameMap.mem n env.seen then
@@ -113,22 +119,81 @@ let rec infer (env: env) (expected: typ) (known: known) (e: expr): known * expr
       else
         failwith "TODO: recursion"
 
+  | Call _ ->
+      failwith "TODO: Call"
 
   | Assign (Open { atom; _ }, e3, t) ->
+      KPrint.bprintf "[infer-mut,assign] %a\n" PrintMiniRust.pexpr e;
       let known, e3 = infer env t known e3 in
       add_mut_var atom known, e3
 
-  | Assign (IndexMut (Open { atom; _ } as e1, e2), e3, t) ->
+  | Assign (Index (Open { atom; _ } as e1, e2), e3, t) ->
+      KPrint.bprintf "[infer-mut,assign] %a\n" PrintMiniRust.pexpr e;
       let known = add_mut_borrow atom known in
       let known, e2 = infer env usize known e2 in
       let known, e3 = infer env t known e3 in
-      known, Assign (IndexMut (e1, e2), e3, t)
+      known, Assign (Index (e1, e2), e3, t)
 
   | Assign _ ->
       failwith "TODO: unknown assignment"
 
-  | _ ->
-      failwith "TODO"
+  | Var _
+  | Array _
+  | VecNew _
+  | Name _
+  | Constant _
+  | ConstantString _
+  | Unit
+  | Panic _
+  | Operator _ ->
+      known, e
+
+  | IfThenElse (e1, e2, e3) ->
+      let known, e1 = infer env bool known e1 in
+      let known, e2 = infer env expected known e2 in
+      let known, e3 =
+        match e3 with
+        | Some e3 ->
+            let known, e3 = infer env expected known e3 in
+            known, Some e3
+        | None ->
+            known, None
+      in
+      known, IfThenElse (e1, e2, e3)
+
+  | As (e, t) ->
+      (* Not really correct, but As is only used for integer casts *)
+      let known, e = infer env t known e in
+      known, As (e, t)
+
+  | For (b, e1, e2) ->
+      let known, e2 = infer env Unit known e2 in
+      known, For (b, e1, e2)
+
+  | While (e1, e2) ->
+      let known, e2 = infer env Unit known e2 in
+      known, While (e1, e2)
+
+  | MethodCall _ ->
+      failwith "TODO: MethodCall"
+
+  | Range (e1, e2, b) ->
+      known, Range (e1, e2, b)
+
+  | Struct _ ->
+      failwith "TODO: Struct"
+
+  | Match _ ->
+      failwith "TODO: Match"
+
+  | Index _ ->
+      failwith "TODO: Index"
+
+  | Field _ ->
+      failwith "TODO: Field"
+
+  | Deref _ ->
+      failwith "TODO: Deref"
 
 let infer_mut_borrows files =
   let env = { seen = NameMap.empty } in
@@ -138,6 +203,8 @@ let infer_mut_borrows files =
       let env, decls = List.fold_left (fun (env, decls) decl ->
         match decl with
         | Function ({ name; body; return_type; parameters; _ } as f) ->
+            KPrint.bprintf "[infer-mut] visiting %s\n%a\n" (String.concat "." name)
+              PrintMiniRust.pexpr body;
             let atoms, body =
               List.fold_right (fun binder (atoms, e) ->
                 let a, e = open_ binder e in
diff --git a/lib/PrintMiniRust.ml b/lib/PrintMiniRust.ml
index ab0b5df6..68fb5b7c 100644
--- a/lib/PrintMiniRust.ml
+++ b/lib/PrintMiniRust.ml
@@ -423,7 +423,6 @@ and print_expr env (context: int) (e: expr): document =
       | `GoneUnit -> print env; failwith "unexpected: unit-returning computation was let-bound and used"
       end
 
-  | IndexMut (p, e)
   | Index (p, e) ->
       let mine = 4 in
       paren_if mine @@

From 586aba5715a55af8f5f3168ef2d7e8fc29d8a676 Mon Sep 17 00:00:00 2001
From: Jonathan Protzenko <protz@microsoft.com>
Date: Fri, 12 Jul 2024 09:40:00 -0700
Subject: [PATCH 06/52] Fix substitution functions (how did this ever work?)

---
 lib/MiniRust.ml         | 10 +++++++---
 lib/OptimizeMiniRust.ml |  7 ++++++-
 lib/PrintMiniRust.ml    |  3 ++-
 3 files changed, 15 insertions(+), 5 deletions(-)

diff --git a/lib/MiniRust.ml b/lib/MiniRust.ml
index b81b00cb..033f5e34 100644
--- a/lib/MiniRust.ml
+++ b/lib/MiniRust.ml
@@ -175,17 +175,21 @@ module DeBruijn = struct
   (* A usable map where the user can hook up to extend, called every time a new
      binding is added to the environment *)
   class ['self] map = object (self: 'self)
-    inherit [_] map_expr as super
+    inherit [_] map_expr as _super
 
     (* To be overridden by the user *)
     method extend env _ = env
 
     (* We list all binding nodes and feed those binders to the environment *)
     method! visit_Let env b e1 e2 =
-      super#visit_Let (self#extend env b) b e1 e2
+      let e1 = self#visit_expr env e1 in
+      let e2 = self#visit_expr (self#extend env b) e2 in
+      Let (b, e1, e2)
 
     method! visit_For env b e1 e2 =
-      super#visit_For (self#extend env b) b e1 e2
+      let e1 = self#visit_expr env e1 in
+      let e2 = self#visit_expr (self#extend env b) e2 in
+      For (b, e1, e2)
   end
 
   class map_counting = object
diff --git a/lib/OptimizeMiniRust.ml b/lib/OptimizeMiniRust.ml
index 6b8af704..707465cb 100644
--- a/lib/OptimizeMiniRust.ml
+++ b/lib/OptimizeMiniRust.ml
@@ -93,7 +93,9 @@ let rec infer (env: env) (expected: typ) (known: known) (e: expr): known * expr
         known, e
 
   | Let (b, e1, e2) ->
+      KPrint.bprintf "[infer-mut,let] %a\n" PrintMiniRust.pexpr e;
       let a, e2 = open_ b e2 in
+      KPrint.bprintf "[infer-mut,let] %a\n" PrintMiniRust.pexpr e2;
       let known, e2 = infer env expected known e2 in
       let mut_var = want_mut_var a known in
       let mut_borrow = want_mut_borrow a known in
@@ -204,13 +206,16 @@ let infer_mut_borrows files =
         match decl with
         | Function ({ name; body; return_type; parameters; _ } as f) ->
             KPrint.bprintf "[infer-mut] visiting %s\n%a\n" (String.concat "." name)
-              PrintMiniRust.pexpr body;
+              PrintMiniRust.pdecl decl;
             let atoms, body =
               List.fold_right (fun binder (atoms, e) ->
                 let a, e = open_ binder e in
+                KPrint.bprintf "[infer-mut] opened %s\n%a\n" binder.name PrintMiniRust.pexpr e;
                 a :: atoms, e
               ) parameters ([], body)
             in
+            KPrint.bprintf "[infer-mut] done opening %s\n%a\n" (String.concat "." name)
+              PrintMiniRust.pexpr body;
             let known, body = infer env return_type known body in
             let parameters, body =
               List.fold_right2 (fun (binder: binding) atom (parameters, e) ->
diff --git a/lib/PrintMiniRust.ml b/lib/PrintMiniRust.ml
index 68fb5b7c..5a383ca5 100644
--- a/lib/PrintMiniRust.ml
+++ b/lib/PrintMiniRust.ml
@@ -442,7 +442,7 @@ and print_expr env (context: int) (e: expr): document =
           group (print_pat env p ^/^ string "=>") ^^ group (nest 2 (break1 ^^ print_expr env max_int e))
       ) patexprs)
 
-  | Open { name; _ } -> string name
+  | Open { name; _ } -> at ^^ string name
 
 and print_pat env (p: pat) =
   match p with
@@ -546,3 +546,4 @@ let print_decls ns ds =
 
 let pexpr = printf_of_pprint (print_expr debug max_int)
 let ptyp = printf_of_pprint (print_typ debug)
+let pdecl = printf_of_pprint (fun x -> snd (print_decl debug x))

From abe67f8729c0f417504f96f134f0c3030558820a Mon Sep 17 00:00:00 2001
From: Jonathan Protzenko <protz@microsoft.com>
Date: Fri, 12 Jul 2024 11:08:30 -0700
Subject: [PATCH 07/52] First trivial example works, fixed the substitutions

---
 lib/OptimizeMiniRust.ml | 28 ++++++++++++++++++++--------
 1 file changed, 20 insertions(+), 8 deletions(-)

diff --git a/lib/OptimizeMiniRust.ml b/lib/OptimizeMiniRust.ml
index 707465cb..bf5014ac 100644
--- a/lib/OptimizeMiniRust.ml
+++ b/lib/OptimizeMiniRust.ml
@@ -42,6 +42,7 @@ type known = {
 }
 
 let add_mut_var a known =
+  KPrint.bprintf "%s is let mut\n" (Ast.show_atom_t a);
   { known with v = VarSet.add a known.v }
 
 let add_mut_borrow a known =
@@ -49,7 +50,6 @@ let add_mut_borrow a known =
   { known with r = VarSet.add a known.r }
 
 let want_mut_var a known =
-  KPrint.bprintf "%s is let mut\n" (Ast.show_atom_t a);
   VarSet.mem a known.v
 
 let want_mut_borrow a known =
@@ -95,11 +95,11 @@ let rec infer (env: env) (expected: typ) (known: known) (e: expr): known * expr
   | Let (b, e1, e2) ->
       KPrint.bprintf "[infer-mut,let] %a\n" PrintMiniRust.pexpr e;
       let a, e2 = open_ b e2 in
-      KPrint.bprintf "[infer-mut,let] %a\n" PrintMiniRust.pexpr e2;
+      KPrint.bprintf "[infer-mut,let] opened %s[%s]\n" b.name (show_atom_t a);
       let known, e2 = infer env expected known e2 in
       let mut_var = want_mut_var a known in
       let mut_borrow = want_mut_borrow a known in
-      KPrint.bprintf "[infer-mut,let] %s[%s]: %a let mut ? %b &mut ? %b\n" b.name
+      KPrint.bprintf "[infer-mut,let-done-e2] %s[%s]: %a let mut ? %b &mut ? %b\n" b.name
         (show_atom_t a)
         PrintMiniRust.ptyp b.typ mut_var mut_borrow;
       let t1 = if mut_borrow then make_mut_borrow b.typ else b.typ in
@@ -176,8 +176,18 @@ let rec infer (env: env) (expected: typ) (known: known) (e: expr): known * expr
       let known, e2 = infer env Unit known e2 in
       known, While (e1, e2)
 
-  | MethodCall _ ->
-      failwith "TODO: MethodCall"
+  | MethodCall (e1, m, e2) ->
+      (* There are only a few instances of these generated by AstToMiniRust, so we just review them
+         all here. Note that there are two possible strategies: AstToMiniRust could use an IndexMut
+         AST node to indicate e.g. that the destination of `copy_from_slice` ought to be mutable, or
+         we just bake that knowledge in right here. *)
+      begin match m with
+      | [ "wrapping_add" ] ->
+          known, MethodCall (e1, m, e2)
+      | _ ->
+          KPrint.bprintf "%a\n" PrintMiniRust.pexpr e;
+          failwith "TODO: MethodCall"
+      end
 
   | Range (e1, e2, b) ->
       known, Range (e1, e2, b)
@@ -210,7 +220,7 @@ let infer_mut_borrows files =
             let atoms, body =
               List.fold_right (fun binder (atoms, e) ->
                 let a, e = open_ binder e in
-                KPrint.bprintf "[infer-mut] opened %s\n%a\n" binder.name PrintMiniRust.pexpr e;
+                KPrint.bprintf "[infer-mut] opened %s[%s]\n%a\n" binder.name (show_atom_t a) PrintMiniRust.pexpr e;
                 a :: atoms, e
               ) parameters ([], body)
             in
@@ -218,14 +228,16 @@ let infer_mut_borrows files =
               PrintMiniRust.pexpr body;
             let known, body = infer env return_type known body in
             let parameters, body =
-              List.fold_right2 (fun (binder: binding) atom (parameters, e) ->
+              List.fold_left2 (fun (parameters, e) (binder: binding) atom ->
                 let e = close atom (Var 0) (lift 1 e) in
+                KPrint.bprintf "[infer-mut] closed %s[%s]\n%a\n" binder.name (show_atom_t atom) PrintMiniRust.pexpr e;
                 let mut = want_mut_var atom known in
                 let typ = if want_mut_borrow atom known then make_mut_borrow binder.typ else binder.typ in
                 { binder with mut; typ } :: parameters, e
-              ) parameters atoms ([], body)
+              ) ([], body) parameters atoms
             in
             let env = { seen = NameMap.add name (List.map (fun (x: binding) -> x.typ) parameters) env.seen } in
+            let parameters = List.rev parameters in
             env, Function { f with body; parameters } :: decls
         | _ ->
             env, decl :: decls

From 41231dec9717d977db37b6fc9ff483f06b69cbc0 Mon Sep 17 00:00:00 2001
From: Aymeric Fromherz <aymeric.fromherz@inria.fr>
Date: Mon, 15 Jul 2024 15:57:11 +0200
Subject: [PATCH 08/52] Support simple array access + extend test

---
 lib/OptimizeMiniRust.ml | 11 +++++++++--
 test/Rust7.fst          | 25 ++++++++++++++++++++++---
 2 files changed, 31 insertions(+), 5 deletions(-)

diff --git a/lib/OptimizeMiniRust.ml b/lib/OptimizeMiniRust.ml
index bf5014ac..5e33538c 100644
--- a/lib/OptimizeMiniRust.ml
+++ b/lib/OptimizeMiniRust.ml
@@ -118,8 +118,10 @@ let rec infer (env: env) (expected: typ) (known: known) (e: expr): known * expr
         in
         let es = List.rev es in
         known, Call (Name n, targs, es)
-      else
+      else (
+        KPrint.bprintf "[infer-mut,call] recursing on %s\n" (String.concat " :: " n);
         failwith "TODO: recursion"
+      )
 
   | Call _ ->
       failwith "TODO: Call"
@@ -198,8 +200,13 @@ let rec infer (env: env) (expected: typ) (known: known) (e: expr): known * expr
   | Match _ ->
       failwith "TODO: Match"
 
+  | Index (Open {atom; _} as e1, e2) ->
+      let known = if is_mut_borrow expected then add_mut_borrow atom known else known in
+      let known, e2 = infer env usize known e2 in
+      known, Index (e1, e2)
+
   | Index _ ->
-      failwith "TODO: Index"
+      failwith "TODO: Complex Index"
 
   | Field _ ->
       failwith "TODO: Field"
diff --git a/test/Rust7.fst b/test/Rust7.fst
index e147d622..94fecd9f 100644
--- a/test/Rust7.fst
+++ b/test/Rust7.fst
@@ -2,22 +2,41 @@ module Rust7
 
 module U32 = FStar.UInt32
 module B = LowStar.Buffer
+open LowStar.BufferOps
 
+open FStar
 open FStar.HyperStack.ST
 
 val add_carry_u32:
   x:U32.t
   -> y:U32.t
-  -> r:B.lbuffer U32.t 1 ->
+  -> r:B.lbuffer U32.t 1
+  -> p:B.lbuffer U32.t 1 ->
   Stack U32.t
-  (requires fun h -> B.live h r)
+  (requires fun h -> B.live h r /\ B.live h p)
   (ensures  fun h0 c h1 -> True)
     // modifies1 r h0 h1 /\ v c <= 1 /\
     // (let r = Seq.index (as_seq h1 r) 0 in
     // v r + v c * pow2 (bits t) == v x + v y + v cin))
 
-let add_carry_u32 x y r =
+let add_carry_u32 x y r p =
+  let z = B.index p 0ul in
   let res = U32.add_mod x y in
+  let res = U32.add_mod res z in
   // let c = (U32.shift_right res 32ul) in
   B.upd r 0ul res;
   0ul
+
+
+// // simple for loop example - note that there is no framing
+// let loop ()  : Stack UInt32.t
+//   (requires (fun h0 -> True))
+//   (ensures (fun h0 r h1 -> True)) =
+//   push_frame();
+//   let ptr = B.alloca 0ul 10ul in
+//   let _ = C.Loops.for 0ul 9ul
+//     (fun h i -> B.live h ptr)
+//     (fun i -> ptr.(i) <- 1ul) in
+//   let sum = ptr.(0ul) in
+//   pop_frame();
+//   sum

From 27dda355205d57c2d577693e47b8fa29cbb6933e Mon Sep 17 00:00:00 2001
From: Aymeric Fromherz <aymeric.fromherz@inria.fr>
Date: Mon, 15 Jul 2024 18:01:16 +0200
Subject: [PATCH 09/52] Add support for builtins in Rust mut-infer translation

---
 lib/OptimizeMiniRust.ml | 9 ++++++++-
 1 file changed, 8 insertions(+), 1 deletion(-)

diff --git a/lib/OptimizeMiniRust.ml b/lib/OptimizeMiniRust.ml
index 5e33538c..fabc517b 100644
--- a/lib/OptimizeMiniRust.ml
+++ b/lib/OptimizeMiniRust.ml
@@ -214,8 +214,15 @@ let rec infer (env: env) (expected: typ) (known: known) (e: expr): known * expr
   | Deref _ ->
       failwith "TODO: Deref"
 
+(* We store here a list of builtins, with the types of their arguments *)
+let builtins : (name * typ list) list = [
+  (* Constants are ignored by infer, we can give them any type *)
+  ["krml"; "unroll_for!"], [Unit; Unit; Unit; Unit; Unit];
+]
+
 let infer_mut_borrows files =
-  let env = { seen = NameMap.empty } in
+  (* Map.of_list is only available from OCaml 5.1 onwards *)
+  let env = { seen = List.to_seq builtins |> NameMap.of_seq } in
   let known = { v = VarSet.empty; r = VarSet.empty } in
   let _, files =
     List.fold_left (fun (env, files) (filename, decls) ->

From be03fa8e25d35875dac1472ab67876e30e44d601 Mon Sep 17 00:00:00 2001
From: Aymeric Fromherz <aymeric.fromherz@inria.fr>
Date: Mon, 15 Jul 2024 18:34:08 +0200
Subject: [PATCH 10/52] Move loop unrolling after mutability inference to avoid
 issues with substitutions

---
 lib/AstToMiniRust.ml | 64 +++-----------------------------------------
 lib/RustMacroize.ml  | 54 +++++++++++++++++++++++++++++++++++++
 src/Karamel.ml       |  1 +
 test/Rust7.fst       | 26 +++++++++++++++---
 4 files changed, 81 insertions(+), 64 deletions(-)
 create mode 100644 lib/RustMacroize.ml

diff --git a/lib/AstToMiniRust.ml b/lib/AstToMiniRust.ml
index 96db52dc..9ca87c39 100644
--- a/lib/AstToMiniRust.ml
+++ b/lib/AstToMiniRust.ml
@@ -1007,66 +1007,10 @@ and translate_expr_with_type (env: env) (e: Ast.expr) (t_ret: MiniRust.typ): env
   | EWhile _ ->
       failwith "TODO: EWhile"
 
-  (* Loop with all constant bounds. *)
-  | EFor (b,
-    ({ node = EConstant (UInt32, init as k_init); _ } as e_init),
-    { node = EApp (
-      { node = EOp (Lt, UInt32); _ },
-      [{ node = EBound 0; _ };
-      ({ node = EConstant (UInt32, max); _ })]); _},
-    { node = EAssign (
-      { node = EBound 0; _ },
-      { node = EApp (
-        { node = EOp (Add, UInt32); _ },
-        [{ node = EBound 0; _ };
-        ({ node = EConstant (UInt32, incr as k_incr); _ })]); _}); _},
-    body)
-    when (
-      let init = int_of_string init in
-      let max = int_of_string max in
-      let incr = int_of_string incr in
-      let n_loops = (max - init + incr - 1) / incr in
-      n_loops <= !Options.unroll_loops
-    )
-    ->
-      (* Keep initial environment to return after translation *)
-      let env0 = env in
-
-      let init = int_of_string init in
-      let max = int_of_string max in
-      let incr = int_of_string incr in
-      let n_loops = (max - init + incr - 1) / incr in
-
-      if n_loops = 0 then
-        env, Unit
-
-      else if n_loops = 1 then
-        let body = DeBruijn.subst e_init 0 body in
-        translate_expr env body
-
-      else begin
-        let unused = snd !(b.node.mark) = AtMost 3 in
-        (* We do an ad-hoc thing since this didn't go through lowstar.ignore
-           insertion. Rust uses the OCaml convention (which I recall I did suggest
-           to Graydon back in 2010). *)
-        let unused = if unused then "_" else "" in
-        let b: MiniRust.binding = { name = unused ^ b.node.name; typ = translate_type env b.typ; mut = false } in
-        let _, body = translate_expr (push env b) body in
-
-        (* This is a weird node, because it contains a binder, but does not rely
-           on a MiniRust.binding to encode that fact. For that reason, the
-           printer needs to be kept in sync and catch this special application
-           node. We could do this rewrite on the fly when pretty-printing, but
-           we'd have to retain the number of uses (above) in the node to figure
-           out whether to make the binder ignored or not. *)
-        env0, Call (Name ["krml"; "unroll_for!"], [], [
-          Constant (CInt, string_of_int n_loops);
-          ConstantString b.name;
-          Constant k_init;
-          Constant k_incr;
-          body ])
-      end
-
+  (* The introduction of the unroll_loops macro requires a "fake" binder
+     for the iterated value, which messes up with variable substitutions
+     mutability inference. We instead perform it in RustMacroize, after
+     all substitutions are done. *)
   | EFor (b, e_start, e_test, e_incr, e_body) ->
       (* Keep initial environment to return after translation *)
       let env0 = env in
diff --git a/lib/RustMacroize.ml b/lib/RustMacroize.ml
new file mode 100644
index 00000000..bb8e86d4
--- /dev/null
+++ b/lib/RustMacroize.ml
@@ -0,0 +1,54 @@
+(* Rewritings on the Rust AST after translation and mutability inference *) 
+
+open MiniRust
+
+(* Loop unrolling introduces an implicit binder that does not interact well
+   with the substitutions occurring in mutability inference.
+   We perform it after the translation *)
+let unroll_loops = object
+  inherit [_] map_expr as super
+  method! visit_For _ b e1 e2 =
+    let e2 = super#visit_expr () e2 in 
+
+    match e1 with
+    | Range (Some (Constant (UInt32, init as k_init) as e_init), Some (Constant (UInt32, max as k_max)), false)
+      when (
+        let init = int_of_string init in
+        let max = int_of_string max in
+        let n_loops = max - init in
+        n_loops <= !Options.unroll_loops
+      ) ->
+        let init = int_of_string init in
+        let max = int_of_string max in
+        let n_loops = max - init in 
+
+        if n_loops = 0 then Unit
+
+        else if n_loops = 1 then subst e_init 0 e2
+
+        else Call (Name ["krml"; "unroll_for!"], [], [
+          Constant (CInt, string_of_int n_loops);
+          ConstantString b.name;
+          Constant k_init;
+          Constant k_max;
+          e2
+        ])
+
+    | _ -> For (b, e1, e2)
+end 
+
+let macroize files =
+  let files =
+    List.fold_left (fun files (filename, decls) ->
+      let decls = List.fold_left (fun decls decl ->
+        match decl with
+        | Function ({ body; _ } as f) ->
+          let body = unroll_loops#visit_expr () body in
+          Function {f with body} :: decls
+        | _ -> decl :: decls
+      ) [] decls in
+      let decls = List.rev decls in
+      (filename, decls) :: files
+    ) [] files
+  in
+  List.rev files
diff --git a/src/Karamel.ml b/src/Karamel.ml
index ec7eae24..2fcbb7a0 100644
--- a/src/Karamel.ml
+++ b/src/Karamel.ml
@@ -751,6 +751,7 @@ Supported options:|}
       print PrintAst.print_files files;
     let files = AstToMiniRust.translate_files files in
     let files = OptimizeMiniRust.infer_mut_borrows files in
+    let files = RustMacroize.macroize files in
     OutputRust.write_all files
 
   else
diff --git a/test/Rust7.fst b/test/Rust7.fst
index 94fecd9f..7bdadc6d 100644
--- a/test/Rust7.fst
+++ b/test/Rust7.fst
@@ -27,16 +27,34 @@ let add_carry_u32 x y r p =
   B.upd r 0ul res;
   0ul
 
+// simple for loop example - note that there is no framing
+let loop (ptr:B.lbuffer U32.t 10)  : Stack UInt32.t
+  (requires (fun h0 -> B.live h0 ptr))
+  (ensures (fun h0 r h1 -> True)) =
+  push_frame();
+  C.Loops.for 0ul 0ul
+    (fun h i -> B.live h ptr)
+    (fun i -> B.upd ptr i 1ul);
+  C.Loops.for 0ul 1ul
+    (fun h i -> B.live h ptr)
+    (fun i -> B.upd ptr i 1ul);
+  C.Loops.for 0ul 10ul
+    (fun h i -> B.live h ptr)
+    (fun i -> B.upd ptr i 1ul);
+  let sum = B.index ptr 0ul in
+  pop_frame();
+  sum
+
 
 // // simple for loop example - note that there is no framing
-// let loop ()  : Stack UInt32.t
+// let loop_alloc ()  : Stack UInt32.t
 //   (requires (fun h0 -> True))
 //   (ensures (fun h0 r h1 -> True)) =
 //   push_frame();
 //   let ptr = B.alloca 0ul 10ul in
-//   let _ = C.Loops.for 0ul 9ul
+//   C.Loops.for 0ul 9ul
 //     (fun h i -> B.live h ptr)
-//     (fun i -> ptr.(i) <- 1ul) in
-//   let sum = ptr.(0ul) in
+//     (fun i -> B.upd ptr i 1ul);
+//   let sum = B.index ptr 0ul in
 //   pop_frame();
 //   sum

From 6a0fcca01052129a502499ed37d4705ff560d1b4 Mon Sep 17 00:00:00 2001
From: Aymeric Fromherz <aymeric.fromherz@inria.fr>
Date: Mon, 15 Jul 2024 18:57:15 +0200
Subject: [PATCH 11/52] Mutify assignments under a borrow

---
 lib/OptimizeMiniRust.ml |  7 +++++++
 test/Rust7.fst          | 11 ++++++++++-
 2 files changed, 17 insertions(+), 1 deletion(-)

diff --git a/lib/OptimizeMiniRust.ml b/lib/OptimizeMiniRust.ml
index fabc517b..d3c84fc1 100644
--- a/lib/OptimizeMiniRust.ml
+++ b/lib/OptimizeMiniRust.ml
@@ -138,6 +138,13 @@ let rec infer (env: env) (expected: typ) (known: known) (e: expr): known * expr
       let known, e3 = infer env t known e3 in
       known, Assign (Index (e1, e2), e3, t)
 
+  | Assign (Index (Borrow (_, (Open { atom; _ } as e1)), e2), e3, t) ->
+      KPrint.bprintf "[infer-mut,assign] %a\n" PrintMiniRust.pexpr e;
+      let known = add_mut_var atom known in
+      let known, e2 = infer env usize known e2 in
+      let known, e3 = infer env t known e3 in
+      known, Assign (Index (Borrow (Mut, e1), e2), e3, t)
+
   | Assign _ ->
       failwith "TODO: unknown assignment"
 
diff --git a/test/Rust7.fst b/test/Rust7.fst
index 7bdadc6d..80f854c1 100644
--- a/test/Rust7.fst
+++ b/test/Rust7.fst
@@ -27,6 +27,16 @@ let add_carry_u32 x y r p =
   B.upd r 0ul res;
   0ul
 
+let test_alloca (x: UInt32.t)  : Stack UInt32.t
+  (requires (fun h0 -> True))
+  (ensures (fun h0 r h1 -> True)) =
+  push_frame();
+  let ptr = B.alloca 0ul 10ul in
+  B.upd ptr 0ul x;
+  let res = B.index ptr 0ul in
+  pop_frame();
+  x
+
 // simple for loop example - note that there is no framing
 let loop (ptr:B.lbuffer U32.t 10)  : Stack UInt32.t
   (requires (fun h0 -> B.live h0 ptr))
@@ -46,7 +56,6 @@ let loop (ptr:B.lbuffer U32.t 10)  : Stack UInt32.t
   sum
 
 
-// // simple for loop example - note that there is no framing
 // let loop_alloc ()  : Stack UInt32.t
 //   (requires (fun h0 -> True))
 //   (ensures (fun h0 r h1 -> True)) =

From aa7d35de6e1bb3ceb2d2d76fe8c4b1a237c4af3a Mon Sep 17 00:00:00 2001
From: Aymeric Fromherz <aymeric.fromherz@inria.fr>
Date: Mon, 15 Jul 2024 19:01:37 +0200
Subject: [PATCH 12/52] Support reading under a borrow

---
 lib/OptimizeMiniRust.ml |  7 ++++++-
 test/Rust7.fst          | 22 +++++++++++-----------
 2 files changed, 17 insertions(+), 12 deletions(-)

diff --git a/lib/OptimizeMiniRust.ml b/lib/OptimizeMiniRust.ml
index d3c84fc1..1a1cacea 100644
--- a/lib/OptimizeMiniRust.ml
+++ b/lib/OptimizeMiniRust.ml
@@ -212,8 +212,13 @@ let rec infer (env: env) (expected: typ) (known: known) (e: expr): known * expr
       let known, e2 = infer env usize known e2 in
       known, Index (e1, e2)
 
+  | Index (Borrow (k, (Open { atom; _ } as e1)), e2) ->
+      let kind, known = if is_mut_borrow expected then Mut, add_mut_var atom known else k, known in
+      let known, e2 = infer env usize known e2 in
+      known, Index (Borrow (kind, e1), e2)
+
   | Index _ ->
-      failwith "TODO: Complex Index"
+      failwith "TODO: unknown Index"
 
   | Field _ ->
       failwith "TODO: Field"
diff --git a/test/Rust7.fst b/test/Rust7.fst
index 80f854c1..c1f6b930 100644
--- a/test/Rust7.fst
+++ b/test/Rust7.fst
@@ -56,14 +56,14 @@ let loop (ptr:B.lbuffer U32.t 10)  : Stack UInt32.t
   sum
 
 
-// let loop_alloc ()  : Stack UInt32.t
-//   (requires (fun h0 -> True))
-//   (ensures (fun h0 r h1 -> True)) =
-//   push_frame();
-//   let ptr = B.alloca 0ul 10ul in
-//   C.Loops.for 0ul 9ul
-//     (fun h i -> B.live h ptr)
-//     (fun i -> B.upd ptr i 1ul);
-//   let sum = B.index ptr 0ul in
-//   pop_frame();
-//   sum
+let loop_alloc ()  : Stack UInt32.t
+  (requires (fun h0 -> True))
+  (ensures (fun h0 r h1 -> True)) =
+  push_frame();
+  let ptr = B.alloca 0ul 10ul in
+  C.Loops.for 0ul 9ul
+    (fun h i -> B.live h ptr)
+    (fun i -> B.upd ptr i 1ul);
+  let sum = B.index ptr 0ul in
+  pop_frame();
+  sum

From ecc0c85f1a3d4d82a6ef2de050b55a1dd16154c2 Mon Sep 17 00:00:00 2001
From: Aymeric Fromherz <aymeric.fromherz@inria.fr>
Date: Mon, 15 Jul 2024 19:11:51 +0200
Subject: [PATCH 13/52] Small example of failing array split

---
 test/Rust7.fst | 124 +++++++++++++++++++++++++++----------------------
 1 file changed, 69 insertions(+), 55 deletions(-)

diff --git a/test/Rust7.fst b/test/Rust7.fst
index c1f6b930..d410a736 100644
--- a/test/Rust7.fst
+++ b/test/Rust7.fst
@@ -7,63 +7,77 @@ open LowStar.BufferOps
 open FStar
 open FStar.HyperStack.ST
 
-val add_carry_u32:
-  x:U32.t
-  -> y:U32.t
-  -> r:B.lbuffer U32.t 1
-  -> p:B.lbuffer U32.t 1 ->
-  Stack U32.t
-  (requires fun h -> B.live h r /\ B.live h p)
-  (ensures  fun h0 c h1 -> True)
-    // modifies1 r h0 h1 /\ v c <= 1 /\
-    // (let r = Seq.index (as_seq h1 r) 0 in
-    // v r + v c * pow2 (bits t) == v x + v y + v cin))
+// val add_carry_u32:
+//   x:U32.t
+//   -> y:U32.t
+//   -> r:B.lbuffer U32.t 1
+//   -> p:B.lbuffer U32.t 1 ->
+//   Stack U32.t
+//   (requires fun h -> B.live h r /\ B.live h p)
+//   (ensures  fun h0 c h1 -> True)
+//     // modifies1 r h0 h1 /\ v c <= 1 /\
+//     // (let r = Seq.index (as_seq h1 r) 0 in
+//     // v r + v c * pow2 (bits t) == v x + v y + v cin))
 
-let add_carry_u32 x y r p =
-  let z = B.index p 0ul in
-  let res = U32.add_mod x y in
-  let res = U32.add_mod res z in
-  // let c = (U32.shift_right res 32ul) in
-  B.upd r 0ul res;
-  0ul
+// let add_carry_u32 x y r p =
+//   let z = B.index p 0ul in
+//   let res = U32.add_mod x y in
+//   let res = U32.add_mod res z in
+//   // let c = (U32.shift_right res 32ul) in
+//   B.upd r 0ul res;
+//   0ul
 
-let test_alloca (x: UInt32.t)  : Stack UInt32.t
-  (requires (fun h0 -> True))
-  (ensures (fun h0 r h1 -> True)) =
-  push_frame();
-  let ptr = B.alloca 0ul 10ul in
-  B.upd ptr 0ul x;
-  let res = B.index ptr 0ul in
-  pop_frame();
-  x
+// let test_alloca (x: UInt32.t)  : Stack UInt32.t
+//   (requires (fun h0 -> True))
+//   (ensures (fun h0 r h1 -> True)) =
+//   push_frame();
+//   let ptr = B.alloca 0ul 10ul in
+//   B.upd ptr 0ul x;
+//   let res = B.index ptr 0ul in
+//   pop_frame();
+//   x
 
-// simple for loop example - note that there is no framing
-let loop (ptr:B.lbuffer U32.t 10)  : Stack UInt32.t
-  (requires (fun h0 -> B.live h0 ptr))
-  (ensures (fun h0 r h1 -> True)) =
-  push_frame();
-  C.Loops.for 0ul 0ul
-    (fun h i -> B.live h ptr)
-    (fun i -> B.upd ptr i 1ul);
-  C.Loops.for 0ul 1ul
-    (fun h i -> B.live h ptr)
-    (fun i -> B.upd ptr i 1ul);
-  C.Loops.for 0ul 10ul
-    (fun h i -> B.live h ptr)
-    (fun i -> B.upd ptr i 1ul);
-  let sum = B.index ptr 0ul in
-  pop_frame();
-  sum
+// // simple for loop example - note that there is no framing
+// let loop (ptr:B.lbuffer U32.t 10)  : Stack UInt32.t
+//   (requires (fun h0 -> B.live h0 ptr))
+//   (ensures (fun h0 r h1 -> True)) =
+//   push_frame();
+//   C.Loops.for 0ul 0ul
+//     (fun h i -> B.live h ptr)
+//     (fun i -> B.upd ptr i 1ul);
+//   C.Loops.for 0ul 1ul
+//     (fun h i -> B.live h ptr)
+//     (fun i -> B.upd ptr i 1ul);
+//   C.Loops.for 0ul 10ul
+//     (fun h i -> B.live h ptr)
+//     (fun i -> B.upd ptr i 1ul);
+//   let sum = B.index ptr 0ul in
+//   pop_frame();
+//   sum
 
 
-let loop_alloc ()  : Stack UInt32.t
-  (requires (fun h0 -> True))
-  (ensures (fun h0 r h1 -> True)) =
-  push_frame();
-  let ptr = B.alloca 0ul 10ul in
-  C.Loops.for 0ul 9ul
-    (fun h i -> B.live h ptr)
-    (fun i -> B.upd ptr i 1ul);
-  let sum = B.index ptr 0ul in
-  pop_frame();
-  sum
+// let loop_alloc ()  : Stack UInt32.t
+//   (requires (fun h0 -> True))
+//   (ensures (fun h0 r h1 -> True)) =
+//   push_frame();
+//   let ptr = B.alloca 0ul 10ul in
+//   C.Loops.for 0ul 9ul
+//     (fun h i -> B.live h ptr)
+//     (fun i -> B.upd ptr i 1ul);
+//   let sum = B.index ptr 0ul in
+//   pop_frame();
+//   sum
+
+let root_alias (): Stack unit (fun _ -> True) (fun _ _ _ -> True) =
+  push_frame ();
+  let x = B.alloca 0UL 6ul in
+  let x0 = B.sub x 0ul 2ul in
+  // let x1 = B.sub x 2ul 2ul in
+
+  // let x00 = B.sub x0 0ul 1ul in
+  // let x01 = B.sub x0 1ul 1ul in
+
+  // B.upd x00 0ul 2UL;
+  B.upd x0 0ul 2UL;
+  // B.upd x 0ul 4UL;
+  pop_frame()

From 9aaf0c6d88e7787fb88ad64f66ef2a398117fd38 Mon Sep 17 00:00:00 2001
From: Jonathan Protzenko <protz@microsoft.com>
Date: Mon, 15 Jul 2024 16:41:52 -0700
Subject: [PATCH 14/52] Enable more tests

---
 test/Makefile  |   4 +-
 test/Rust7.fst | 124 +++++++++++++++++++++++++------------------------
 2 files changed, 65 insertions(+), 63 deletions(-)

diff --git a/test/Makefile b/test/Makefile
index efab490f..d92247c3 100644
--- a/test/Makefile
+++ b/test/Makefile
@@ -88,7 +88,7 @@ FSTAR		= $(FSTAR_EXE) --cache_checked_modules \
   --trivial_pre_for_unannotated_effectful_fns false \
   --cmi --warn_error -274
 
-all: $(FILES) $(RUST_FILES) $(WASM_FILES) $(CUSTOM) ctypes-test sepcomp-test
+all: $(FILES) rust $(WASM_FILES) $(CUSTOM) ctypes-test sepcomp-test
 
 # Needs node
 wasm: $(WASM_FILES)
@@ -300,7 +300,7 @@ WasmTrap.wasm-test: NEGATIVE = true
 %.rs: $(ALL_KRML_FILES) $(KRML_BIN)
 	$(KRML) -minimal -bundle $(notdir $*)=\* \
 	  -backend rust $(EXTRA) -tmpdir $(dir $@) $(filter %.krml,$^)
-	$(SED) -i 's/\(assignments..\)/\1\nmod lowstar { pub mod ignore { pub fn ignore<T>(_x: T) {}}}\n/' $@
+	$(SED) -i 's/\(mutation..\)/\1\nmod lowstar { pub mod ignore { pub fn ignore<T>(_x: T) {}}}\n/' $@
 	echo 'fn main () { let r = main_ (); if r != 0 { println!("main_ returned: {}\\n", r); panic!() } }' >> $@
 
 %.rust-test: $(OUTPUT_DIR)/%.rs
diff --git a/test/Rust7.fst b/test/Rust7.fst
index d410a736..ee7b3515 100644
--- a/test/Rust7.fst
+++ b/test/Rust7.fst
@@ -7,77 +7,79 @@ open LowStar.BufferOps
 open FStar
 open FStar.HyperStack.ST
 
-// val add_carry_u32:
-//   x:U32.t
-//   -> y:U32.t
-//   -> r:B.lbuffer U32.t 1
-//   -> p:B.lbuffer U32.t 1 ->
-//   Stack U32.t
-//   (requires fun h -> B.live h r /\ B.live h p)
-//   (ensures  fun h0 c h1 -> True)
-//     // modifies1 r h0 h1 /\ v c <= 1 /\
-//     // (let r = Seq.index (as_seq h1 r) 0 in
-//     // v r + v c * pow2 (bits t) == v x + v y + v cin))
+val add_carry_u32:
+  x:U32.t
+  -> y:U32.t
+  -> r:B.lbuffer U32.t 1
+  -> p:B.lbuffer U32.t 1 ->
+  Stack U32.t
+  (requires fun h -> B.live h r /\ B.live h p)
+  (ensures  fun h0 c h1 -> True)
+    // modifies1 r h0 h1 /\ v c <= 1 /\
+    // (let r = Seq.index (as_seq h1 r) 0 in
+    // v r + v c * pow2 (bits t) == v x + v y + v cin))
 
-// let add_carry_u32 x y r p =
-//   let z = B.index p 0ul in
-//   let res = U32.add_mod x y in
-//   let res = U32.add_mod res z in
-//   // let c = (U32.shift_right res 32ul) in
-//   B.upd r 0ul res;
-//   0ul
+let add_carry_u32 x y r p =
+  let z = B.index p 0ul in
+  let res = U32.add_mod x y in
+  let res = U32.add_mod res z in
+  // let c = (U32.shift_right res 32ul) in
+  B.upd r 0ul res;
+  0ul
 
-// let test_alloca (x: UInt32.t)  : Stack UInt32.t
-//   (requires (fun h0 -> True))
-//   (ensures (fun h0 r h1 -> True)) =
-//   push_frame();
-//   let ptr = B.alloca 0ul 10ul in
-//   B.upd ptr 0ul x;
-//   let res = B.index ptr 0ul in
-//   pop_frame();
-//   x
+let test_alloca (x: UInt32.t)  : Stack UInt32.t
+  (requires (fun h0 -> True))
+  (ensures (fun h0 r h1 -> True)) =
+  push_frame();
+  let ptr = B.alloca 0ul 10ul in
+  B.upd ptr 0ul x;
+  let res = B.index ptr 0ul in
+  pop_frame();
+  x
 
-// // simple for loop example - note that there is no framing
-// let loop (ptr:B.lbuffer U32.t 10)  : Stack UInt32.t
-//   (requires (fun h0 -> B.live h0 ptr))
-//   (ensures (fun h0 r h1 -> True)) =
-//   push_frame();
-//   C.Loops.for 0ul 0ul
-//     (fun h i -> B.live h ptr)
-//     (fun i -> B.upd ptr i 1ul);
-//   C.Loops.for 0ul 1ul
-//     (fun h i -> B.live h ptr)
-//     (fun i -> B.upd ptr i 1ul);
-//   C.Loops.for 0ul 10ul
-//     (fun h i -> B.live h ptr)
-//     (fun i -> B.upd ptr i 1ul);
-//   let sum = B.index ptr 0ul in
-//   pop_frame();
-//   sum
+// simple for loop example - note that there is no framing
+let loop (ptr:B.lbuffer U32.t 10)  : Stack UInt32.t
+  (requires (fun h0 -> B.live h0 ptr))
+  (ensures (fun h0 r h1 -> True)) =
+  push_frame();
+  C.Loops.for 0ul 0ul
+    (fun h i -> B.live h ptr)
+    (fun i -> B.upd ptr i 1ul);
+  C.Loops.for 0ul 1ul
+    (fun h i -> B.live h ptr)
+    (fun i -> B.upd ptr i 1ul);
+  C.Loops.for 0ul 10ul
+    (fun h i -> B.live h ptr)
+    (fun i -> B.upd ptr i 1ul);
+  let sum = B.index ptr 0ul in
+  pop_frame();
+  sum
 
 
-// let loop_alloc ()  : Stack UInt32.t
-//   (requires (fun h0 -> True))
-//   (ensures (fun h0 r h1 -> True)) =
-//   push_frame();
-//   let ptr = B.alloca 0ul 10ul in
-//   C.Loops.for 0ul 9ul
-//     (fun h i -> B.live h ptr)
-//     (fun i -> B.upd ptr i 1ul);
-//   let sum = B.index ptr 0ul in
-//   pop_frame();
-//   sum
+let loop_alloc ()  : Stack UInt32.t
+  (requires (fun h0 -> True))
+  (ensures (fun h0 r h1 -> True)) =
+  push_frame();
+  let ptr = B.alloca 0ul 10ul in
+  C.Loops.for 0ul 9ul
+    (fun h i -> B.live h ptr)
+    (fun i -> B.upd ptr i 1ul);
+  let sum = B.index ptr 0ul in
+  pop_frame();
+  sum
 
 let root_alias (): Stack unit (fun _ -> True) (fun _ _ _ -> True) =
   push_frame ();
   let x = B.alloca 0UL 6ul in
   let x0 = B.sub x 0ul 2ul in
-  // let x1 = B.sub x 2ul 2ul in
+  let x1 = B.sub x 2ul 2ul in
 
-  // let x00 = B.sub x0 0ul 1ul in
-  // let x01 = B.sub x0 1ul 1ul in
+  let x00 = B.sub x0 0ul 1ul in
+  let x01 = B.sub x0 1ul 1ul in
 
-  // B.upd x00 0ul 2UL;
-  B.upd x0 0ul 2UL;
-  // B.upd x 0ul 4UL;
+  B.upd x00 0ul 2UL;
+  (* B.upd x0 0ul 2UL; *)
+  (* B.upd x 0ul 4UL; *)
   pop_frame()
+
+let main_ () = 0l

From 8fd080b71edf900b4e616d70da752893be626918 Mon Sep 17 00:00:00 2001
From: Jonathan Protzenko <protz@microsoft.com>
Date: Mon, 15 Jul 2024 16:54:03 -0700
Subject: [PATCH 15/52] An ad-hoc treatment of ignore -- because missing
 handling of type substitutions in MiniRust

---
 lib/OptimizeMiniRust.ml | 8 ++++++--
 test/Rust7.fst          | 2 +-
 2 files changed, 7 insertions(+), 3 deletions(-)

diff --git a/lib/OptimizeMiniRust.ml b/lib/OptimizeMiniRust.ml
index 1a1cacea..4bc248a2 100644
--- a/lib/OptimizeMiniRust.ml
+++ b/lib/OptimizeMiniRust.ml
@@ -118,6 +118,12 @@ let rec infer (env: env) (expected: typ) (known: known) (e: expr): known * expr
         in
         let es = List.rev es in
         known, Call (Name n, targs, es)
+      else if n = ["lowstar";"ignore";"ignore"] then
+        (* Since we do not have type-level substitutions in MiniRust, we special-case ignore here.
+           Ideally, it would be added to builtins with `Bound 0` as a suitable type for the
+           argument. *)
+        let known, e = infer env (KList.one targs) known (KList.one es) in
+        known, Call (Name n, targs, [ e ])
       else (
         KPrint.bprintf "[infer-mut,call] recursing on %s\n" (String.concat " :: " n);
         failwith "TODO: recursion"
@@ -228,8 +234,6 @@ let rec infer (env: env) (expected: typ) (known: known) (e: expr): known * expr
 
 (* We store here a list of builtins, with the types of their arguments *)
 let builtins : (name * typ list) list = [
-  (* Constants are ignored by infer, we can give them any type *)
-  ["krml"; "unroll_for!"], [Unit; Unit; Unit; Unit; Unit];
 ]
 
 let infer_mut_borrows files =
diff --git a/test/Rust7.fst b/test/Rust7.fst
index ee7b3515..4a5c1f2a 100644
--- a/test/Rust7.fst
+++ b/test/Rust7.fst
@@ -77,7 +77,7 @@ let root_alias (): Stack unit (fun _ -> True) (fun _ _ _ -> True) =
   let x00 = B.sub x0 0ul 1ul in
   let x01 = B.sub x0 1ul 1ul in
 
-  B.upd x00 0ul 2UL;
+  (* B.upd x00 0ul 2UL; *)
   (* B.upd x0 0ul 2UL; *)
   (* B.upd x 0ul 4UL; *)
   pop_frame()

From 55e56715f5452f6473de988e8b8a56637c38f92d Mon Sep 17 00:00:00 2001
From: Jonathan Protzenko <protz@microsoft.com>
Date: Mon, 15 Jul 2024 16:58:27 -0700
Subject: [PATCH 16/52] Trigger the field case, and then a comment

---
 lib/OptimizeMiniRust.ml | 3 +++
 test/Rust7.fst          | 8 ++++++++
 2 files changed, 11 insertions(+)

diff --git a/lib/OptimizeMiniRust.ml b/lib/OptimizeMiniRust.ml
index 4bc248a2..19f15ad1 100644
--- a/lib/OptimizeMiniRust.ml
+++ b/lib/OptimizeMiniRust.ml
@@ -227,6 +227,9 @@ let rec infer (env: env) (expected: typ) (known: known) (e: expr): known * expr
       failwith "TODO: unknown Index"
 
   | Field _ ->
+      (* We should be able to ignore this case, on the basis that we are not going to get any
+         mutability constraints from a field expression. However, we need to modify all of the cases
+         above (such as assignment) to handle the case where the assignee is a field. *)
       failwith "TODO: Field"
 
   | Deref _ ->
diff --git a/test/Rust7.fst b/test/Rust7.fst
index 4a5c1f2a..04e4f6bc 100644
--- a/test/Rust7.fst
+++ b/test/Rust7.fst
@@ -68,6 +68,9 @@ let loop_alloc ()  : Stack UInt32.t
   pop_frame();
   sum
 
+let touch (#a: Type) (x: a): Stack unit (fun _ -> True) (fun _ _ _ -> True) =
+  ()
+
 let root_alias (): Stack unit (fun _ -> True) (fun _ _ _ -> True) =
   push_frame ();
   let x = B.alloca 0UL 6ul in
@@ -77,6 +80,11 @@ let root_alias (): Stack unit (fun _ -> True) (fun _ _ _ -> True) =
   let x00 = B.sub x0 0ul 1ul in
   let x01 = B.sub x0 1ul 1ul in
 
+  touch x0;
+  touch x1;
+  touch x00;
+  touch x01;
+
   (* B.upd x00 0ul 2UL; *)
   (* B.upd x0 0ul 2UL; *)
   (* B.upd x 0ul 4UL; *)

From 2571c9387d66da52f0b449cdf8d770dcdee4403d Mon Sep 17 00:00:00 2001
From: Aymeric Fromherz <aymeric.fromherz@inria.fr>
Date: Wed, 17 Jul 2024 10:42:11 +0200
Subject: [PATCH 17/52] Rewrite splits into split_at_muts when needed

---
 lib/AstToMiniRust.ml    |  2 +-
 lib/OptimizeMiniRust.ml | 27 ++++++++++++++++++++++++++-
 test/Rust7.fst          | 14 +++++++-------
 3 files changed, 34 insertions(+), 9 deletions(-)

diff --git a/lib/AstToMiniRust.ml b/lib/AstToMiniRust.ml
index 9ca87c39..0d8504f9 100644
--- a/lib/AstToMiniRust.ml
+++ b/lib/AstToMiniRust.ml
@@ -805,7 +805,7 @@ and translate_expr_with_type (env: env) (e: Ast.expr) (t_ret: MiniRust.typ): env
           env, MiniRust.(Field (find 0 env.vars, Splits.string_of_path_elem path_elem))
       in
 
-      let split_at = match b.typ with TBuf (_, true) -> "split_at" | _ -> "split_at_mut" in
+      let split_at = "split_at" in
       let e1 = MiniRust.MethodCall (e_nearest , [split_at], [ index ]) in
       let t = translate_type env b.typ in
       let binding : MiniRust.binding * Splits.info =
diff --git a/lib/OptimizeMiniRust.ml b/lib/OptimizeMiniRust.ml
index 19f15ad1..2157ea90 100644
--- a/lib/OptimizeMiniRust.ml
+++ b/lib/OptimizeMiniRust.ml
@@ -57,16 +57,23 @@ let want_mut_borrow a known =
 
 let is_mut_borrow = function
   | Ref (_, Mut, _) -> true
+  (* Special-case for tuples; they should only occur with array slices *)
+  | Tuple [Ref (_, Mut, _); Ref (_, Mut, _)] -> true
   | _ -> false
 
 let make_mut_borrow = function
   | Ref (l, _, t) -> Ref (l, Mut, t)
+  | Tuple [Ref (l1, _, t1); Ref (l2, _, t2)] -> Tuple [Ref (l1, Mut, t1); Ref (l2, Mut, t2)]
   | _ -> failwith "impossible: make_mut_borrow"
 
 let assert_borrow = function
   | Ref (_, _, t) -> t
   | _ -> failwith "impossible: assert_borrow"
 
+let retrieve_pair_type = function
+  | Tuple [e1; e2] -> assert (e1 = e2); e1
+  | _ -> failwith "impossible: retrieve_pair_type"
+
 let rec infer (env: env) (expected: typ) (known: known) (e: expr): known * expr =
   match e with
   | Borrow (k, e) ->
@@ -137,7 +144,16 @@ let rec infer (env: env) (expected: typ) (known: known) (e: expr): known * expr
       let known, e3 = infer env t known e3 in
       add_mut_var atom known, e3
 
-  | Assign (Index (Open { atom; _ } as e1, e2), e3, t) ->
+  | Assign (Index (Open { atom; _ } as e1, e2), e3, t) 
+  (* Special-case when we perform a field assignment that comes from
+     a slice. This is the only case where we use native Rust tuples.
+     In this case, we mark the atom as mutable, and will replace
+     the corresponding call to split by split_at_mut when we reach
+      let-binding.
+   *)
+  | Assign (Index (Field (Open {atom;_}, "0") as e1, e2), e3, t)
+  | Assign (Index (Field (Open {atom;_}, "1") as e1, e2), e3, t)
+  ->
       KPrint.bprintf "[infer-mut,assign] %a\n" PrintMiniRust.pexpr e;
       let known = add_mut_borrow atom known in
       let known, e2 = infer env usize known e2 in
@@ -199,6 +215,15 @@ let rec infer (env: env) (expected: typ) (known: known) (e: expr): known * expr
       begin match m with
       | [ "wrapping_add" ] ->
           known, MethodCall (e1, m, e2)
+      | ["split_at"] ->
+          assert (List.length e2 = 1);
+          let known, e2 = infer env usize known (List.hd e2) in
+          let t1 = retrieve_pair_type expected in
+          let known, e1 = infer env t1 known e1 in
+          if is_mut_borrow expected then
+            known, MethodCall (e1, ["split_at_mut"], [e2])
+          else
+            known, MethodCall (e1, m, [e2])
       | _ ->
           KPrint.bprintf "%a\n" PrintMiniRust.pexpr e;
           failwith "TODO: MethodCall"
diff --git a/test/Rust7.fst b/test/Rust7.fst
index 04e4f6bc..33046557 100644
--- a/test/Rust7.fst
+++ b/test/Rust7.fst
@@ -77,16 +77,16 @@ let root_alias (): Stack unit (fun _ -> True) (fun _ _ _ -> True) =
   let x0 = B.sub x 0ul 2ul in
   let x1 = B.sub x 2ul 2ul in
 
-  let x00 = B.sub x0 0ul 1ul in
-  let x01 = B.sub x0 1ul 1ul in
+  // let x00 = B.sub x0 0ul 1ul in
+  // let x01 = B.sub x0 1ul 1ul in
 
-  touch x0;
-  touch x1;
-  touch x00;
-  touch x01;
+  // touch x0;
+  // touch x1;
+  // touch x00;
+  // touch x01;
 
   (* B.upd x00 0ul 2UL; *)
-  (* B.upd x0 0ul 2UL; *)
+  B.upd x0 0ul 2UL;
   (* B.upd x 0ul 4UL; *)
   pop_frame()
 

From 91b951cba288076dc72d47ff6913d3d6b867af4f Mon Sep 17 00:00:00 2001
From: Aymeric Fromherz <aymeric.fromherz@inria.fr>
Date: Wed, 17 Jul 2024 10:55:22 +0200
Subject: [PATCH 18/52] Support for calling functions with slices

---
 lib/OptimizeMiniRust.ml |  7 +++++++
 test/Rust7.fst          | 32 +++++++++++++++++++++++---------
 2 files changed, 30 insertions(+), 9 deletions(-)

diff --git a/lib/OptimizeMiniRust.ml b/lib/OptimizeMiniRust.ml
index 2157ea90..f54cdf81 100644
--- a/lib/OptimizeMiniRust.ml
+++ b/lib/OptimizeMiniRust.ml
@@ -251,6 +251,13 @@ let rec infer (env: env) (expected: typ) (known: known) (e: expr): known * expr
   | Index _ ->
       failwith "TODO: unknown Index"
 
+  (* Special case for array slices. This occurs, e.g., when calling a function with 
+     a struct field *)
+  | Field (Open { atom; _ }, "0") | Field (Open { atom; _}, "1") ->
+      if is_mut_borrow expected then
+        add_mut_borrow atom known, e
+      else known, e
+
   | Field _ ->
       (* We should be able to ignore this case, on the basis that we are not going to get any
          mutability constraints from a field expression. However, we need to modify all of the cases
diff --git a/test/Rust7.fst b/test/Rust7.fst
index 33046557..9243ef02 100644
--- a/test/Rust7.fst
+++ b/test/Rust7.fst
@@ -71,23 +71,37 @@ let loop_alloc ()  : Stack UInt32.t
 let touch (#a: Type) (x: a): Stack unit (fun _ -> True) (fun _ _ _ -> True) =
   ()
 
+let upd (x: B.buffer UInt64.t): Stack unit (fun h -> B.live h x /\ B.length x >= 1)
+  (fun h0 _ h1 -> B.modifies (B.loc_buffer x) h0 h1) =
+  B.upd x 0ul 0UL
+
 let root_alias (): Stack unit (fun _ -> True) (fun _ _ _ -> True) =
   push_frame ();
   let x = B.alloca 0UL 6ul in
   let x0 = B.sub x 0ul 2ul in
   let x1 = B.sub x 2ul 2ul in
 
-  // let x00 = B.sub x0 0ul 1ul in
-  // let x01 = B.sub x0 1ul 1ul in
+  let x00 = B.sub x0 0ul 1ul in
+  let x01 = B.sub x0 1ul 1ul in
+
+  touch x0;
+  touch x1;
+  touch x00;
+  touch x01;
+
+  pop_frame()
+
+let slice_upd (): Stack unit (fun _ -> True) (fun _ _ _ -> True) =
+  push_frame ();
+  let x = B.alloca 0UL 6ul in
+  let x0 = B.sub x 0ul 2ul in
+  let x1 = B.sub x 2ul 2ul in
+
+  let x00 = B.sub x0 0ul 1ul in
+  let x01 = B.sub x0 1ul 1ul in
 
-  // touch x0;
-  // touch x1;
-  // touch x00;
-  // touch x01;
+  upd x00;
 
-  (* B.upd x00 0ul 2UL; *)
-  B.upd x0 0ul 2UL;
-  (* B.upd x 0ul 4UL; *)
   pop_frame()
 
 let main_ () = 0l

From e8294b0b3ba48f9a8406ec145436ca4746f853d9 Mon Sep 17 00:00:00 2001
From: Aymeric Fromherz <aymeric.fromherz@inria.fr>
Date: Wed, 17 Jul 2024 11:24:10 +0200
Subject: [PATCH 19/52] Add support for more operators

---
 lib/OptimizeMiniRust.ml | 12 +++++++++++-
 1 file changed, 11 insertions(+), 1 deletion(-)

diff --git a/lib/OptimizeMiniRust.ml b/lib/OptimizeMiniRust.ml
index f54cdf81..048aef97 100644
--- a/lib/OptimizeMiniRust.ml
+++ b/lib/OptimizeMiniRust.ml
@@ -136,6 +136,14 @@ let rec infer (env: env) (expected: typ) (known: known) (e: expr): known * expr
         failwith "TODO: recursion"
       )
 
+  | Call (Operator o, [], _) -> begin match o with
+      (* Most operators are wrapping and were translated to a methodcall.
+         We list the few remaining ones here *)
+      | BOr | BAnd | BXor | BNot | And | Or | Xor | Not -> known, e
+      | _ ->
+        failwith "TODO: operator not supported"
+    end
+
   | Call _ ->
       failwith "TODO: Call"
 
@@ -213,7 +221,9 @@ let rec infer (env: env) (expected: typ) (known: known) (e: expr): known * expr
          AST node to indicate e.g. that the destination of `copy_from_slice` ought to be mutable, or
          we just bake that knowledge in right here. *)
       begin match m with
-      | [ "wrapping_add" ] ->
+      | [ "wrapping_add" ] | [ "wrapping_div" ] | [ "wrapping_mul" ] 
+      | [ "wrapping_neg" ] | [ "wrapping_rem" ] | [ "wrapping_shl" ]
+      | [ "wrapping_shr" ] | [ "wrapping_sub" ] ->
           known, MethodCall (e1, m, e2)
       | ["split_at"] ->
           assert (List.length e2 = 1);

From e37f83ebe8c6906358b5602eb0ca4ad7e7b20f9d Mon Sep 17 00:00:00 2001
From: Aymeric Fromherz <aymeric.fromherz@inria.fr>
Date: Wed, 17 Jul 2024 11:51:06 +0200
Subject: [PATCH 20/52] Simplify and generalize handling of indices

---
 lib/OptimizeMiniRust.ml | 16 ++++++----------
 1 file changed, 6 insertions(+), 10 deletions(-)

diff --git a/lib/OptimizeMiniRust.ml b/lib/OptimizeMiniRust.ml
index 048aef97..9f4b91d8 100644
--- a/lib/OptimizeMiniRust.ml
+++ b/lib/OptimizeMiniRust.ml
@@ -248,19 +248,15 @@ let rec infer (env: env) (expected: typ) (known: known) (e: expr): known * expr
   | Match _ ->
       failwith "TODO: Match"
 
-  | Index (Open {atom; _} as e1, e2) ->
-      let known = if is_mut_borrow expected then add_mut_borrow atom known else known in
+  | Index (e1, e2) ->
+      (* The cases where we perform an assignment on an index should be caught
+         earlier. This should therefore only occur when accessing a variable
+         in an array *)
+      let expected = Ref (None, Shared, expected) in
+      let known, e1 = infer env expected known e1 in
       let known, e2 = infer env usize known e2 in
       known, Index (e1, e2)
 
-  | Index (Borrow (k, (Open { atom; _ } as e1)), e2) ->
-      let kind, known = if is_mut_borrow expected then Mut, add_mut_var atom known else k, known in
-      let known, e2 = infer env usize known e2 in
-      known, Index (Borrow (kind, e1), e2)
-
-  | Index _ ->
-      failwith "TODO: unknown Index"
-
   (* Special case for array slices. This occurs, e.g., when calling a function with 
      a struct field *)
   | Field (Open { atom; _ }, "0") | Field (Open { atom; _}, "1") ->

From aeb113b44d82067035932e0977a7585c614198c5 Mon Sep 17 00:00:00 2001
From: Aymeric Fromherz <aymeric.fromherz@inria.fr>
Date: Wed, 17 Jul 2024 12:04:41 +0200
Subject: [PATCH 21/52] Add support for copy_from_slice

---
 lib/OptimizeMiniRust.ml | 12 ++++++++++++
 test/Rust7.fst          | 19 +++++++++++++++++++
 2 files changed, 31 insertions(+)

diff --git a/lib/OptimizeMiniRust.ml b/lib/OptimizeMiniRust.ml
index 9f4b91d8..960abcfc 100644
--- a/lib/OptimizeMiniRust.ml
+++ b/lib/OptimizeMiniRust.ml
@@ -234,6 +234,18 @@ let rec infer (env: env) (expected: typ) (known: known) (e: expr): known * expr
             known, MethodCall (e1, ["split_at_mut"], [e2])
           else
             known, MethodCall (e1, m, [e2])
+      | ["copy_from_slice"] -> begin match e1 with
+          | Index (dst, range) ->
+            assert (List.length e2 = 1);
+            (* We do not have access to the types of e1 and e2. However, the concrete
+               type should not matter during mut inference, we thus use Unit as a default *)
+            let known, dst = infer env (Ref (None, Mut, Unit)) known dst in
+            let known, e2 = infer env (Ref (None, Shared, Unit)) known (List.hd e2) in
+            known, MethodCall (Index (dst, range), m, [e2])
+          (* The AstToMiniRust translation should always introduce an index
+              as the left argument of copy_from_slice *)
+          | _ -> failwith "ill-formed copy_from_slice"
+          end
       | _ ->
           KPrint.bprintf "%a\n" PrintMiniRust.pexpr e;
           failwith "TODO: MethodCall"
diff --git a/test/Rust7.fst b/test/Rust7.fst
index 9243ef02..519360d9 100644
--- a/test/Rust7.fst
+++ b/test/Rust7.fst
@@ -104,4 +104,23 @@ let slice_upd (): Stack unit (fun _ -> True) (fun _ _ _ -> True) =
 
   pop_frame()
 
+let basic_copy1 (): Stack unit (fun _ -> True) (fun _ _ _ -> True) =
+  push_frame ();
+  let x = B.alloca 0ul 6ul in
+  let y = B.alloca 1ul 6ul in
+  B.blit y 0ul x 0ul 6ul;
+  pop_frame()
+
+let basic_copy2 (): Stack unit (fun _ -> True) (fun _ _ _ -> True) =
+  push_frame ();
+  let x = B.alloca 0ul 6ul in
+  let y = B.alloca 1ul 6ul in
+  let x0 = B.sub x 0ul 2ul in
+  let x1 = B.sub x0 0ul 1ul in
+
+  B.upd x1 0ul 5ul;
+  B.blit x0 0ul y 0ul 2ul;
+  pop_frame()
+
+
 let main_ () = 0l

From 06eb67a1b718953d9d0e59f53b154e7c43c02659 Mon Sep 17 00:00:00 2001
From: Aymeric Fromherz <aymeric.fromherz@inria.fr>
Date: Wed, 17 Jul 2024 12:25:54 +0200
Subject: [PATCH 22/52] Add a few builtins

---
 lib/OptimizeMiniRust.ml | 7 +++++++
 1 file changed, 7 insertions(+)

diff --git a/lib/OptimizeMiniRust.ml b/lib/OptimizeMiniRust.ml
index 960abcfc..f107f29a 100644
--- a/lib/OptimizeMiniRust.ml
+++ b/lib/OptimizeMiniRust.ml
@@ -287,6 +287,13 @@ let rec infer (env: env) (expected: typ) (known: known) (e: expr): known * expr
 
 (* We store here a list of builtins, with the types of their arguments *)
 let builtins : (name * typ list) list = [
+  (* FStar.UInt128 *)
+  [ "fstar"; "uint128"; "uint128_to_uint64" ], [Name (["fstar"; "uint128"; "uint128"], [])];
+  [ "fstar"; "uint128"; "shift_right" ],
+      [Name (["fstar"; "uint128"; "uint128"], []); Constant UInt32];
+
+  (* LowStar.Endianness *)
+  [ "lowstar"; "endianness"; "load64_le" ], [Ref (None, Shared, Constant UInt8)];
 ]
 
 let infer_mut_borrows files =

From 05aa2749f57fb6516059a8375432ed0452e1def3 Mon Sep 17 00:00:00 2001
From: Aymeric Fromherz <aymeric.fromherz@inria.fr>
Date: Wed, 17 Jul 2024 16:27:03 +0200
Subject: [PATCH 23/52] Fix order of function parameters in env, add more
 operators and memzero

---
 lib/OptimizeMiniRust.ml | 26 ++++++++++++++++++++------
 lib/lib/KList.ml        |  5 +++++
 2 files changed, 25 insertions(+), 6 deletions(-)

diff --git a/lib/OptimizeMiniRust.ml b/lib/OptimizeMiniRust.ml
index f107f29a..547f435c 100644
--- a/lib/OptimizeMiniRust.ml
+++ b/lib/OptimizeMiniRust.ml
@@ -131,7 +131,15 @@ let rec infer (env: env) (expected: typ) (known: known) (e: expr): known * expr
            argument. *)
         let known, e = infer env (KList.one targs) known (KList.one es) in
         known, Call (Name n, targs, [ e ])
-      else (
+      else if n = [ "lib"; "memzero0"; "memzero" ] then (
+        (* Same as ignore above *)
+        assert (List.length es = 2);
+        let e1, e2 = KList.two es in
+        KPrint.bprintf "[infer-mut, call-memzero] %a \n" PrintMiniRust.pexpr e;
+        let known, e1 = infer env (Ref (None, Mut, Slice (KList.one targs))) known e1 in
+        let known, e2 = infer env (Constant UInt32) known e2 in
+        known, Call (Name n, targs, [ e1; e2 ])
+      ) else (
         KPrint.bprintf "[infer-mut,call] recursing on %s\n" (String.concat " :: " n);
         failwith "TODO: recursion"
       )
@@ -139,7 +147,9 @@ let rec infer (env: env) (expected: typ) (known: known) (e: expr): known * expr
   | Call (Operator o, [], _) -> begin match o with
       (* Most operators are wrapping and were translated to a methodcall.
          We list the few remaining ones here *)
-      | BOr | BAnd | BXor | BNot | And | Or | Xor | Not -> known, e
+      | BOr | BAnd | BXor | BNot
+      | Eq | Neq | Lt | Lte | Gt | Gte
+      | And | Or | Xor | Not -> known, e
       | _ ->
         failwith "TODO: operator not supported"
     end
@@ -255,7 +265,9 @@ let rec infer (env: env) (expected: typ) (known: known) (e: expr): known * expr
       known, Range (e1, e2, b)
 
   | Struct _ ->
-      failwith "TODO: Struct"
+      (* TODO: This should very likely be modified depending on the current struct
+         in known. *)
+      known, e
 
   | Match _ ->
       failwith "TODO: Match"
@@ -280,12 +292,14 @@ let rec infer (env: env) (expected: typ) (known: known) (e: expr): known * expr
       (* We should be able to ignore this case, on the basis that we are not going to get any
          mutability constraints from a field expression. However, we need to modify all of the cases
          above (such as assignment) to handle the case where the assignee is a field. *)
-      failwith "TODO: Field"
+      known, e
 
   | Deref _ ->
       failwith "TODO: Deref"
 
-(* We store here a list of builtins, with the types of their arguments *)
+(* We store here a list of builtins, with the types of their arguments.
+   Type substitutions are currently not supported, functions with generic
+   args should be added directly to Call in infer *)
 let builtins : (name * typ list) list = [
   (* FStar.UInt128 *)
   [ "fstar"; "uint128"; "uint128_to_uint64" ], [Name (["fstar"; "uint128"; "uint128"], [])];
@@ -326,8 +340,8 @@ let infer_mut_borrows files =
                 { binder with mut; typ } :: parameters, e
               ) ([], body) parameters atoms
             in
-            let env = { seen = NameMap.add name (List.map (fun (x: binding) -> x.typ) parameters) env.seen } in
             let parameters = List.rev parameters in
+            let env = { seen = NameMap.add name (List.map (fun (x: binding) -> x.typ) parameters) env.seen } in
             env, Function { f with body; parameters } :: decls
         | _ ->
             env, decl :: decls
diff --git a/lib/lib/KList.ml b/lib/lib/KList.ml
index 7cf08ba3..231a9ad9 100644
--- a/lib/lib/KList.ml
+++ b/lib/lib/KList.ml
@@ -72,6 +72,11 @@ let one l =
   | [ x ] -> x
   | _ -> invalid_arg ("one: argument is of length " ^ string_of_int (List.length l))
 
+let two l =
+  match l with
+  | [ x; y ] -> (x, y)
+  | _ -> invalid_arg ("one: argument is of length " ^ string_of_int (List.length l))
+
 (* NOTE: provided by {!Stdlib.List} in OCaml 5.1. *)
 let is_empty = function
   | [] -> true

From e18720e973603c618e64e19b6599407cbeb1b28b Mon Sep 17 00:00:00 2001
From: Aymeric Fromherz <aymeric.fromherz@inria.fr>
Date: Wed, 17 Jul 2024 16:35:33 +0200
Subject: [PATCH 24/52] More builtins

---
 lib/OptimizeMiniRust.ml | 5 ++++-
 1 file changed, 4 insertions(+), 1 deletion(-)

diff --git a/lib/OptimizeMiniRust.ml b/lib/OptimizeMiniRust.ml
index 547f435c..856a34b4 100644
--- a/lib/OptimizeMiniRust.ml
+++ b/lib/OptimizeMiniRust.ml
@@ -135,7 +135,6 @@ let rec infer (env: env) (expected: typ) (known: known) (e: expr): known * expr
         (* Same as ignore above *)
         assert (List.length es = 2);
         let e1, e2 = KList.two es in
-        KPrint.bprintf "[infer-mut, call-memzero] %a \n" PrintMiniRust.pexpr e;
         let known, e1 = infer env (Ref (None, Mut, Slice (KList.one targs))) known e1 in
         let known, e2 = infer env (Constant UInt32) known e2 in
         known, Call (Name n, targs, [ e1; e2 ])
@@ -302,12 +301,16 @@ let rec infer (env: env) (expected: typ) (known: known) (e: expr): known * expr
    args should be added directly to Call in infer *)
 let builtins : (name * typ list) list = [
   (* FStar.UInt128 *)
+  [ "fstar"; "uint128"; "uint64_to_uint128" ], [Constant UInt64];
   [ "fstar"; "uint128"; "uint128_to_uint64" ], [Name (["fstar"; "uint128"; "uint128"], [])];
+  [ "fstar"; "uint128"; "add_mod" ],
+      [Name (["fstar"; "uint128"; "uint128"], []); Name (["fstar"; "uint128"; "uint128"], [])];
   [ "fstar"; "uint128"; "shift_right" ],
       [Name (["fstar"; "uint128"; "uint128"], []); Constant UInt32];
 
   (* LowStar.Endianness *)
   [ "lowstar"; "endianness"; "load64_le" ], [Ref (None, Shared, Constant UInt8)];
+  [ "lowstar"; "endianness"; "store64_le" ], [Ref (None, Mut, Constant UInt8)];
 ]
 
 let infer_mut_borrows files =

From 65b74bbccc4a0986d8f7c9c992ff5d6e8778546b Mon Sep 17 00:00:00 2001
From: Aymeric Fromherz <aymeric.fromherz@inria.fr>
Date: Wed, 17 Jul 2024 17:01:58 +0200
Subject: [PATCH 25/52] Fix store64_le, add borrowing a range

---
 lib/OptimizeMiniRust.ml | 5 ++++-
 1 file changed, 4 insertions(+), 1 deletion(-)

diff --git a/lib/OptimizeMiniRust.ml b/lib/OptimizeMiniRust.ml
index 856a34b4..53ef764a 100644
--- a/lib/OptimizeMiniRust.ml
+++ b/lib/OptimizeMiniRust.ml
@@ -85,6 +85,9 @@ let rec infer (env: env) (expected: typ) (known: known) (e: expr): known * expr
             failwith "impossible: missing open"
         | Open { atom; _ } ->
             add_mut_var atom known, Borrow (Mut, e)
+        | Index (e1, (Range _ as r))  ->
+            let known, e1 = infer env expected known e1 in
+            known, Borrow (Mut, Index (e1, r))
         | _ ->
             failwith "TODO: borrowing something other than a variable"
       else
@@ -310,7 +313,7 @@ let builtins : (name * typ list) list = [
 
   (* LowStar.Endianness *)
   [ "lowstar"; "endianness"; "load64_le" ], [Ref (None, Shared, Constant UInt8)];
-  [ "lowstar"; "endianness"; "store64_le" ], [Ref (None, Mut, Constant UInt8)];
+  [ "lowstar"; "endianness"; "store64_le" ], [Ref (None, Mut, Constant UInt8); Constant UInt64];
 ]
 
 let infer_mut_borrows files =

From 901e4119eb8523dca2d33e8a13e64fbbf4329c06 Mon Sep 17 00:00:00 2001
From: Aymeric Fromherz <aymeric.fromherz@inria.fr>
Date: Wed, 17 Jul 2024 17:09:58 +0200
Subject: [PATCH 26/52] Support vec operations

---
 lib/OptimizeMiniRust.ml | 5 +++++
 test/Rust7.fst          | 6 ++++++
 2 files changed, 11 insertions(+)

diff --git a/lib/OptimizeMiniRust.ml b/lib/OptimizeMiniRust.ml
index 53ef764a..347a7aa7 100644
--- a/lib/OptimizeMiniRust.ml
+++ b/lib/OptimizeMiniRust.ml
@@ -258,6 +258,8 @@ let rec infer (env: env) (expected: typ) (known: known) (e: expr): known * expr
               as the left argument of copy_from_slice *)
           | _ -> failwith "ill-formed copy_from_slice"
           end
+      | [ "push" ] ->
+          known, MethodCall (e1, m, e2)
       | _ ->
           KPrint.bprintf "%a\n" PrintMiniRust.pexpr e;
           failwith "TODO: MethodCall"
@@ -314,6 +316,9 @@ let builtins : (name * typ list) list = [
   (* LowStar.Endianness *)
   [ "lowstar"; "endianness"; "load64_le" ], [Ref (None, Shared, Constant UInt8)];
   [ "lowstar"; "endianness"; "store64_le" ], [Ref (None, Mut, Constant UInt8); Constant UInt64];
+
+  (* Vec *)
+  [ "Vec"; "new" ], [];
 ]
 
 let infer_mut_borrows files =
diff --git a/test/Rust7.fst b/test/Rust7.fst
index 519360d9..187619f6 100644
--- a/test/Rust7.fst
+++ b/test/Rust7.fst
@@ -122,5 +122,11 @@ let basic_copy2 (): Stack unit (fun _ -> True) (fun _ _ _ -> True) =
   B.blit x0 0ul y 0ul 2ul;
   pop_frame()
 
+noeq
+type point = { x : B.lbuffer U32.t 1; y : B.lbuffer U32.t 1 }
+
+let struct_upd (p: point) : Stack UInt32.t (fun h -> B.live h p.x) (fun _ _ _ -> True) =
+  B.index p.x 0ul
+
 
 let main_ () = 0l

From e22b3dacf11a9899c7789b342f8c391ba0172158 Mon Sep 17 00:00:00 2001
From: Aymeric Fromherz <aymeric.fromherz@inria.fr>
Date: Wed, 17 Jul 2024 19:08:49 +0200
Subject: [PATCH 27/52] Store type of structure in Field node

---
 lib/AstToMiniRust.ml    | 7 ++++---
 lib/MiniRust.ml         | 5 ++++-
 lib/OptimizeMiniRust.ml | 7 ++++---
 lib/PrintMiniRust.ml    | 2 +-
 4 files changed, 13 insertions(+), 8 deletions(-)

diff --git a/lib/AstToMiniRust.ml b/lib/AstToMiniRust.ml
index 0d8504f9..d27a9dec 100644
--- a/lib/AstToMiniRust.ml
+++ b/lib/AstToMiniRust.ml
@@ -508,7 +508,7 @@ let lookup_split (env: env) (v_base: MiniRust.db_index) (path: Splits.root_or_pa
         | Some (v_base', path') when v_base' = v_base - ofs - 1 ->
             begin match Splits.accessible_via path path' with
             | Some pe ->
-                MiniRust.(Field (Var ofs, Splits.string_of_path_elem pe))
+                MiniRust.(Field (Var ofs, Splits.string_of_path_elem pe, None))
             | None ->
                 find (ofs + 1) bs
             end
@@ -802,7 +802,7 @@ and translate_expr_with_type (env: env) (e: Ast.expr) (t_ret: MiniRust.typ): env
             | [] ->
                 failwith "[ELet] unexpected: path not found"
           in
-          env, MiniRust.(Field (find 0 env.vars, Splits.string_of_path_elem path_elem))
+          env, MiniRust.(Field (find 0 env.vars, Splits.string_of_path_elem path_elem, None))
       in
 
       let split_at = "split_at" in
@@ -996,7 +996,8 @@ and translate_expr_with_type (env: env) (e: Ast.expr) (t_ret: MiniRust.typ): env
 
   | EField (e, f) ->
       let env, e_ = translate_expr env e in
-      env, possibly_convert (Field (e_, f)) (field_type env e f)
+      let t = translate_type env e.typ in
+      env, possibly_convert (Field (e_, f, Some t)) (field_type env e f)
 
   | EBreak ->
       failwith "TODO: EBreak"
diff --git a/lib/MiniRust.ml b/lib/MiniRust.ml
index 033f5e34..40293e9d 100644
--- a/lib/MiniRust.ml
+++ b/lib/MiniRust.ml
@@ -97,7 +97,10 @@ and expr =
   | Var of db_index
   | Open of open_var
   | Index of expr * expr
-  | Field of expr * string
+  (* The type corresponds to the structure we are accessing.
+     We will store None when accessing a native Rust tuple,
+     corresponding to an array slice *)
+  | Field of expr * string * typ option
 
   (* Operator expressions *)
   | Operator of op
diff --git a/lib/OptimizeMiniRust.ml b/lib/OptimizeMiniRust.ml
index 347a7aa7..8f71e138 100644
--- a/lib/OptimizeMiniRust.ml
+++ b/lib/OptimizeMiniRust.ml
@@ -89,6 +89,7 @@ let rec infer (env: env) (expected: typ) (known: known) (e: expr): known * expr
             let known, e1 = infer env expected known e1 in
             known, Borrow (Mut, Index (e1, r))
         | _ ->
+            KPrint.bprintf "[infer-mut, borrow] borrwing %a is not supported\n" PrintMiniRust.pexpr e;
             failwith "TODO: borrowing something other than a variable"
       else
         let known, e = infer env (assert_borrow expected) known e in
@@ -171,8 +172,8 @@ let rec infer (env: env) (expected: typ) (known: known) (e: expr): known * expr
      the corresponding call to split by split_at_mut when we reach
       let-binding.
    *)
-  | Assign (Index (Field (Open {atom;_}, "0") as e1, e2), e3, t)
-  | Assign (Index (Field (Open {atom;_}, "1") as e1, e2), e3, t)
+  | Assign (Index (Field (Open {atom;_}, "0", None) as e1, e2), e3, t)
+  | Assign (Index (Field (Open {atom;_}, "1", None) as e1, e2), e3, t)
   ->
       KPrint.bprintf "[infer-mut,assign] %a\n" PrintMiniRust.pexpr e;
       let known = add_mut_borrow atom known in
@@ -287,7 +288,7 @@ let rec infer (env: env) (expected: typ) (known: known) (e: expr): known * expr
 
   (* Special case for array slices. This occurs, e.g., when calling a function with 
      a struct field *)
-  | Field (Open { atom; _ }, "0") | Field (Open { atom; _}, "1") ->
+  | Field (Open { atom; _ }, "0", None) | Field (Open { atom; _}, "1", None) ->
       if is_mut_borrow expected then
         add_mut_borrow atom known, e
       else known, e
diff --git a/lib/PrintMiniRust.ml b/lib/PrintMiniRust.ml
index 5a383ca5..1922079a 100644
--- a/lib/PrintMiniRust.ml
+++ b/lib/PrintMiniRust.ml
@@ -427,7 +427,7 @@ and print_expr env (context: int) (e: expr): document =
       let mine = 4 in
       paren_if mine @@
       print_expr env mine p ^^ group (brackets (print_expr env max_int e))
-  | Field (e, s) ->
+  | Field (e, s, _) ->
       group (print_expr env 3 e ^^ dot ^^ string s)
   | Deref e ->
       let mine = 6 in

From bdb8a1648f2c312f8d7bbd5a04a068056ae71f9a Mon Sep 17 00:00:00 2001
From: Aymeric Fromherz <aymeric.fromherz@inria.fr>
Date: Wed, 17 Jul 2024 19:23:01 +0200
Subject: [PATCH 28/52] Keep track of field mutability in environment

---
 lib/OptimizeMiniRust.ml | 21 ++++++++++++++++-----
 1 file changed, 16 insertions(+), 5 deletions(-)

diff --git a/lib/OptimizeMiniRust.ml b/lib/OptimizeMiniRust.ml
index 8f71e138..ac59c395 100644
--- a/lib/OptimizeMiniRust.ml
+++ b/lib/OptimizeMiniRust.ml
@@ -33,10 +33,12 @@ module NameMap = Map.Make(Name)
 module VarSet = Set.Make(Atom)
 
 type env = {
-  seen: typ list NameMap.t
+  seen: typ list NameMap.t;
+  structs: MiniRust.struct_field list NameMap.t;
 }
 
 type known = {
+  structs: MiniRust.struct_field list NameMap.t;
   v: VarSet.t;
   r: VarSet.t;
 }
@@ -324,8 +326,8 @@ let builtins : (name * typ list) list = [
 
 let infer_mut_borrows files =
   (* Map.of_list is only available from OCaml 5.1 onwards *)
-  let env = { seen = List.to_seq builtins |> NameMap.of_seq } in
-  let known = { v = VarSet.empty; r = VarSet.empty } in
+  let env = { seen = List.to_seq builtins |> NameMap.of_seq; structs = NameMap.empty } in
+  let known = { structs = NameMap.empty; v = VarSet.empty; r = VarSet.empty } in
   let _, files =
     List.fold_left (fun (env, files) (filename, decls) ->
       let env, decls = List.fold_left (fun (env, decls) decl ->
@@ -342,7 +344,8 @@ let infer_mut_borrows files =
             in
             KPrint.bprintf "[infer-mut] done opening %s\n%a\n" (String.concat "." name)
               PrintMiniRust.pexpr body;
-            let known, body = infer env return_type known body in
+            (* Start the analysis with the current state of struct mutability *)
+            let known, body = infer env return_type {known with structs = env.structs} body in
             let parameters, body =
               List.fold_left2 (fun (parameters, e) (binder: binding) atom ->
                 let e = close atom (Var 0) (lift 1 e) in
@@ -353,8 +356,16 @@ let infer_mut_borrows files =
               ) ([], body) parameters atoms
             in
             let parameters = List.rev parameters in
-            let env = { seen = NameMap.add name (List.map (fun (x: binding) -> x.typ) parameters) env.seen } in
+            (* We update the environment in two ways. First, we add the function declaration,
+               with the mutability of the parameters inferred during the analysis.
+               Second, we propagate the information about the mutability of struct fields
+               inferred while traversing this function to the global environment. Note, since
+               the traversal does not add or remove any bindings, but only increases the
+               mutability, we can do a direct replacement instead of a more complex merge *)
+            let env = { seen = NameMap.add name (List.map (fun (x: binding) -> x.typ) parameters) env.seen; structs = known.structs } in
             env, Function { f with body; parameters } :: decls
+        | Struct ({name; fields; _}) ->
+          {env with structs = NameMap.add name fields env.structs}, decl :: decls
         | _ ->
             env, decl :: decls
       ) (env, []) decls in

From 9947edf9ad8b78c5e3b382f990fa099c5fd840cc Mon Sep 17 00:00:00 2001
From: Aymeric Fromherz <aymeric.fromherz@inria.fr>
Date: Wed, 17 Jul 2024 20:13:39 +0200
Subject: [PATCH 29/52] Add update of field mutability

---
 lib/OptimizeMiniRust.ml | 59 ++++++++++++++++++++++++++++++++++-------
 test/Rust7.fst          |  3 ++-
 2 files changed, 52 insertions(+), 10 deletions(-)

diff --git a/lib/OptimizeMiniRust.ml b/lib/OptimizeMiniRust.ml
index ac59c395..5dbdd0cf 100644
--- a/lib/OptimizeMiniRust.ml
+++ b/lib/OptimizeMiniRust.ml
@@ -43,6 +43,14 @@ type known = {
   r: VarSet.t;
 }
 
+let assert_borrow = function
+  | Ref (_, _, t) -> t
+  | _ -> failwith "impossible: assert_borrow"
+
+let assert_name (t: typ option) = match t with
+  | Some (Name (n, _)) -> n
+  | _ -> failwith "impossible: assert_name"
+
 let add_mut_var a known =
   KPrint.bprintf "%s is let mut\n" (Ast.show_atom_t a);
   { known with v = VarSet.add a known.v }
@@ -66,11 +74,16 @@ let is_mut_borrow = function
 let make_mut_borrow = function
   | Ref (l, _, t) -> Ref (l, Mut, t)
   | Tuple [Ref (l1, _, t1); Ref (l2, _, t2)] -> Tuple [Ref (l1, Mut, t1); Ref (l2, Mut, t2)]
+  | Vec t -> Vec t
   | _ -> failwith "impossible: make_mut_borrow"
 
-let assert_borrow = function
-  | Ref (_, _, t) -> t
-  | _ -> failwith "impossible: assert_borrow"
+let add_mut_field ty f known =
+  let n = assert_name ty in
+  let fields = NameMap.find n known.structs in
+  (* Update the mutability of the field element *)
+  let fields = List.map (fun (sf: MiniRust.struct_field) ->
+    if sf.name = f then {sf with typ = make_mut_borrow sf.typ} else sf) fields in
+  {known with structs = NameMap.add n fields known.structs}
 
 let retrieve_pair_type = function
   | Tuple [e1; e2] -> assert (e1 = e2); e1
@@ -90,6 +103,14 @@ let rec infer (env: env) (expected: typ) (known: known) (e: expr): known * expr
         | Index (e1, (Range _ as r))  ->
             let known, e1 = infer env expected known e1 in
             known, Borrow (Mut, Index (e1, r))
+
+        | Field (Open _, "0", None)
+        | Field (Open _, "1", None) -> failwith "TODO: borrowing slices"
+
+        | Field (_, f, t) ->
+            let known = add_mut_field t f known in
+            known, Borrow (Mut, e)
+
         | _ ->
             KPrint.bprintf "[infer-mut, borrow] borrwing %a is not supported\n" PrintMiniRust.pexpr e;
             failwith "TODO: borrowing something other than a variable"
@@ -175,14 +196,19 @@ let rec infer (env: env) (expected: typ) (known: known) (e: expr): known * expr
       let-binding.
    *)
   | Assign (Index (Field (Open {atom;_}, "0", None) as e1, e2), e3, t)
-  | Assign (Index (Field (Open {atom;_}, "1", None) as e1, e2), e3, t)
-  ->
+  | Assign (Index (Field (Open {atom;_}, "1", None) as e1, e2), e3, t) ->
       KPrint.bprintf "[infer-mut,assign] %a\n" PrintMiniRust.pexpr e;
       let known = add_mut_borrow atom known in
       let known, e2 = infer env usize known e2 in
       let known, e3 = infer env t known e3 in
       known, Assign (Index (e1, e2), e3, t)
 
+  | Assign (Index (Field (_, f, st) as e1, e2), e3, t) ->
+      let known = add_mut_field st f known in
+      let known, e2 = infer env usize known e2 in
+      let known, e3 = infer env t known e3 in
+      known, Assign (Index (e1, e2), e3, t)
+
   | Assign (Index (Borrow (_, (Open { atom; _ } as e1)), e2), e3, t) ->
       KPrint.bprintf "[infer-mut,assign] %a\n" PrintMiniRust.pexpr e;
       let known = add_mut_var atom known in
@@ -190,7 +216,12 @@ let rec infer (env: env) (expected: typ) (known: known) (e: expr): known * expr
       let known, e3 = infer env t known e3 in
       known, Assign (Index (Borrow (Mut, e1), e2), e3, t)
 
+  | Assign (Field (_, "0", None), _, _)
+  | Assign (Field (_, "1", None), _, _) ->
+      failwith "TODO: assignment on slice"
+
   | Assign _ ->
+      KPrint.bprintf "[infer-mut,assign] %a unsupported\n" PrintMiniRust.pexpr e;
       failwith "TODO: unknown assignment"
 
   | Var _
@@ -271,8 +302,11 @@ let rec infer (env: env) (expected: typ) (known: known) (e: expr): known * expr
   | Range (e1, e2, b) ->
       known, Range (e1, e2, b)
 
-  | Struct _ ->
-      (* TODO: This should very likely be modified depending on the current struct
+  | Struct (name, _es) ->
+      (* The declaration of the struct should have been traversed beforehand, hence
+         it should be in the map *)
+      let _fields_mut = NameMap.find name known.structs in
+      (* TODO: This should be modified depending on the current struct
          in known. *)
       known, e
 
@@ -328,7 +362,7 @@ let infer_mut_borrows files =
   (* Map.of_list is only available from OCaml 5.1 onwards *)
   let env = { seen = List.to_seq builtins |> NameMap.of_seq; structs = NameMap.empty } in
   let known = { structs = NameMap.empty; v = VarSet.empty; r = VarSet.empty } in
-  let _, files =
+  let env, files =
     List.fold_left (fun (env, files) (filename, decls) ->
       let env, decls = List.fold_left (fun (env, decls) decl ->
         match decl with
@@ -373,4 +407,11 @@ let infer_mut_borrows files =
       env, (filename, decls) :: files
     ) (env, []) files
   in
-  List.rev files
+
+  (* We traverse all declarations again, and update the structure decls
+     with the new mutability info *)
+  List.map (fun (filename, decls) -> filename, List.map (function
+    | Struct ({ name; _ } as s) -> Struct { s with fields = NameMap.find name env.structs }
+    | x -> x
+    ) decls
+  ) (List.rev files)
diff --git a/test/Rust7.fst b/test/Rust7.fst
index 187619f6..707d6772 100644
--- a/test/Rust7.fst
+++ b/test/Rust7.fst
@@ -126,7 +126,8 @@ noeq
 type point = { x : B.lbuffer U32.t 1; y : B.lbuffer U32.t 1 }
 
 let struct_upd (p: point) : Stack UInt32.t (fun h -> B.live h p.x) (fun _ _ _ -> True) =
-  B.index p.x 0ul
+  B.upd p.x 0ul 0ul;
+  0ul
 
 
 let main_ () = 0l

From f9814a5496a951ce1b148f0055e6ddd8ca3a3dd8 Mon Sep 17 00:00:00 2001
From: Aymeric Fromherz <aymeric.fromherz@inria.fr>
Date: Wed, 17 Jul 2024 20:24:13 +0200
Subject: [PATCH 30/52] Support more field assignments

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

diff --git a/lib/OptimizeMiniRust.ml b/lib/OptimizeMiniRust.ml
index 5dbdd0cf..2031f13a 100644
--- a/lib/OptimizeMiniRust.ml
+++ b/lib/OptimizeMiniRust.ml
@@ -220,6 +220,12 @@ let rec infer (env: env) (expected: typ) (known: known) (e: expr): known * expr
   | Assign (Field (_, "1", None), _, _) ->
       failwith "TODO: assignment on slice"
 
+  | Assign (Field (Index ((Open {atom; _} as e1), e2), f, st), e3, t) ->
+      let known = add_mut_borrow atom known in
+      let known, e2 = infer env usize known e2 in
+      let known, e3 = infer env t known e3 in
+      known, Assign (Field (Index (e1, e2), f, st), e3, t)
+
   | Assign _ ->
       KPrint.bprintf "[infer-mut,assign] %a unsupported\n" PrintMiniRust.pexpr e;
       failwith "TODO: unknown assignment"

From 8b8414b09bfc3cf319a4a3a235df3925da90c8be Mon Sep 17 00:00:00 2001
From: Aymeric Fromherz <aymeric.fromherz@inria.fr>
Date: Wed, 17 Jul 2024 20:40:29 +0200
Subject: [PATCH 31/52] Add some builtins for intvector intrinsics

---
 lib/OptimizeMiniRust.ml | 34 ++++++++++++++++++++++++++++++++++
 1 file changed, 34 insertions(+)

diff --git a/lib/OptimizeMiniRust.ml b/lib/OptimizeMiniRust.ml
index 2031f13a..a0f59372 100644
--- a/lib/OptimizeMiniRust.ml
+++ b/lib/OptimizeMiniRust.ml
@@ -356,7 +356,41 @@ let builtins : (name * typ list) list = [
   [ "fstar"; "uint128"; "shift_right" ],
       [Name (["fstar"; "uint128"; "uint128"], []); Constant UInt32];
 
+  (* Lib.IntVector_intrinsics, Vec128 *)
+  [ "lib"; "intvector_intrinsics"; "vec128_add32"],
+    [Name (["lib"; "intvector_intrinsics"; "vec128"], []);
+     Name (["lib"; "intvector_intrinsics"; "vec128"], [])];
+  [ "lib"; "intvector_intrinsics"; "vec128_load32s"],
+    [ Constant UInt32; Constant UInt32; Constant UInt32; Constant UInt32];
+  [ "lib"; "intvector_intrinsics"; "vec128_rotate_right32"],
+    [Name (["lib"; "intvector_intrinsics"; "vec128"], []); Constant UInt32];
+  [ "lib"; "intvector_intrinsics"; "vec128_rotate_right_lanes32"],
+    [Name (["lib"; "intvector_intrinsics"; "vec128"], []); Constant UInt32];
+  [ "lib"; "intvector_intrinsics"; "vec128_store32_le"],
+    [Ref (None, Mut, Constant UInt8); Name (["lib"; "intvector_intrinsics"; "vec128"], [])];
+  [ "lib"; "intvector_intrinsics"; "vec128_xor"],
+    [Name (["lib"; "intvector_intrinsics"; "vec128"], []);
+     Name (["lib"; "intvector_intrinsics"; "vec128"], [])];
+
+  (* Lib.IntVector_intrinsics, Vec256 *)
+  [ "lib"; "intvector_intrinsics"; "vec256_add64"],
+    [Name (["lib"; "intvector_intrinsics"; "vec256"], []);
+     Name (["lib"; "intvector_intrinsics"; "vec256"], [])];
+  [ "lib"; "intvector_intrinsics"; "vec256_load64s"],
+    [ Constant UInt64; Constant UInt64; Constant UInt64; Constant UInt64];
+  [ "lib"; "intvector_intrinsics"; "vec256_rotate_right64"],
+    [Name (["lib"; "intvector_intrinsics"; "vec256"], []); Constant UInt32];
+  [ "lib"; "intvector_intrinsics"; "vec256_rotate_right_lanes64"],
+    [Name (["lib"; "intvector_intrinsics"; "vec256"], []); Constant UInt32];
+  [ "lib"; "intvector_intrinsics"; "vec256_store64_le"],
+    [Ref (None, Mut, Constant UInt8); Name (["lib"; "intvector_intrinsics"; "vec256"], [])];
+  [ "lib"; "intvector_intrinsics"; "vec256_xor"],
+    [Name (["lib"; "intvector_intrinsics"; "vec256"], []);
+     Name (["lib"; "intvector_intrinsics"; "vec256"], [])];
+
   (* LowStar.Endianness *)
+  [ "lowstar"; "endianness"; "load32_le" ], [Ref (None, Shared, Constant UInt8)];
+  [ "lowstar"; "endianness"; "store32_le" ], [Ref (None, Mut, Constant UInt8); Constant UInt32];
   [ "lowstar"; "endianness"; "load64_le" ], [Ref (None, Shared, Constant UInt8)];
   [ "lowstar"; "endianness"; "store64_le" ], [Ref (None, Mut, Constant UInt8); Constant UInt64];
 

From a81029648d43574bf193433daaab884583619e73 Mon Sep 17 00:00:00 2001
From: Aymeric Fromherz <aymeric.fromherz@inria.fr>
Date: Thu, 18 Jul 2024 13:30:41 +0200
Subject: [PATCH 32/52] Add support for match

---
 lib/OptimizeMiniRust.ml | 13 +++++++++++--
 1 file changed, 11 insertions(+), 2 deletions(-)

diff --git a/lib/OptimizeMiniRust.ml b/lib/OptimizeMiniRust.ml
index a0f59372..c2d311c3 100644
--- a/lib/OptimizeMiniRust.ml
+++ b/lib/OptimizeMiniRust.ml
@@ -316,8 +316,17 @@ let rec infer (env: env) (expected: typ) (known: known) (e: expr): known * expr
          in known. *)
       known, e
 
-  | Match _ ->
-      failwith "TODO: Match"
+  | Match (e, arms) ->
+      (* For now, all pattern-matching occur on simple terms, e.g., an enum for an
+         alg, hence we do not mutify the scrutinee. If this happens to be needed,
+         we would need to add the expected type of the scrutinee to the Match node,
+         similar to what is done for Assign and Field, in order to recurse on
+         the scrutinee *)
+      let known, arms = List.fold_left_map (fun known (pat, e) ->
+          let known, e = infer env expected known e in
+          known, (pat, e)
+        ) known arms in
+      known, Match (e, arms) 
 
   | Index (e1, e2) ->
       (* The cases where we perform an assignment on an index should be caught

From 5769d437e93354b8fbdc360024c4c834353f6bb0 Mon Sep 17 00:00:00 2001
From: Aymeric Fromherz <aymeric.fromherz@inria.fr>
Date: Thu, 18 Jul 2024 13:50:20 +0200
Subject: [PATCH 33/52] More builtins

---
 lib/OptimizeMiniRust.ml | 51 +++++++++++++++++++++++++++++++++++++++++
 1 file changed, 51 insertions(+)

diff --git a/lib/OptimizeMiniRust.ml b/lib/OptimizeMiniRust.ml
index c2d311c3..81e162a4 100644
--- a/lib/OptimizeMiniRust.ml
+++ b/lib/OptimizeMiniRust.ml
@@ -360,8 +360,12 @@ let builtins : (name * typ list) list = [
   (* FStar.UInt128 *)
   [ "fstar"; "uint128"; "uint64_to_uint128" ], [Constant UInt64];
   [ "fstar"; "uint128"; "uint128_to_uint64" ], [Name (["fstar"; "uint128"; "uint128"], [])];
+  [ "fstar"; "uint128"; "add" ],
+      [Name (["fstar"; "uint128"; "uint128"], []); Name (["fstar"; "uint128"; "uint128"], [])];
   [ "fstar"; "uint128"; "add_mod" ],
       [Name (["fstar"; "uint128"; "uint128"], []); Name (["fstar"; "uint128"; "uint128"], [])];
+  [ "fstar"; "uint128"; "shift_left" ],
+      [Name (["fstar"; "uint128"; "uint128"], []); Constant UInt32];
   [ "fstar"; "uint128"; "shift_right" ],
       [Name (["fstar"; "uint128"; "uint128"], []); Constant UInt32];
 
@@ -369,8 +373,22 @@ let builtins : (name * typ list) list = [
   [ "lib"; "intvector_intrinsics"; "vec128_add32"],
     [Name (["lib"; "intvector_intrinsics"; "vec128"], []);
      Name (["lib"; "intvector_intrinsics"; "vec128"], [])];
+  [ "lib"; "intvector_intrinsics"; "vec128_interleave_low32"],
+    [Name (["lib"; "intvector_intrinsics"; "vec128"], []);
+     Name (["lib"; "intvector_intrinsics"; "vec128"], [])];
+  [ "lib"; "intvector_intrinsics"; "vec128_interleave_low64"],
+    [Name (["lib"; "intvector_intrinsics"; "vec128"], []);
+     Name (["lib"; "intvector_intrinsics"; "vec128"], [])];
+  [ "lib"; "intvector_intrinsics"; "vec128_interleave_high32"],
+    [Name (["lib"; "intvector_intrinsics"; "vec128"], []);
+     Name (["lib"; "intvector_intrinsics"; "vec128"], [])];
+  [ "lib"; "intvector_intrinsics"; "vec128_interleave_high64"],
+    [Name (["lib"; "intvector_intrinsics"; "vec128"], []);
+     Name (["lib"; "intvector_intrinsics"; "vec128"], [])];
+  [ "lib"; "intvector_intrinsics"; "vec128_load32"], [Constant UInt32];
   [ "lib"; "intvector_intrinsics"; "vec128_load32s"],
     [ Constant UInt32; Constant UInt32; Constant UInt32; Constant UInt32];
+  [ "lib"; "intvector_intrinsics"; "vec128_load32_be"], [Ref (None, Shared, Constant UInt8)];
   [ "lib"; "intvector_intrinsics"; "vec128_rotate_right32"],
     [Name (["lib"; "intvector_intrinsics"; "vec128"], []); Constant UInt32];
   [ "lib"; "intvector_intrinsics"; "vec128_rotate_right_lanes32"],
@@ -385,12 +403,39 @@ let builtins : (name * typ list) list = [
   [ "lib"; "intvector_intrinsics"; "vec256_add64"],
     [Name (["lib"; "intvector_intrinsics"; "vec256"], []);
      Name (["lib"; "intvector_intrinsics"; "vec256"], [])];
+  [ "lib"; "intvector_intrinsics"; "vec256_and"],
+    [Name (["lib"; "intvector_intrinsics"; "vec256"], []);
+     Name (["lib"; "intvector_intrinsics"; "vec256"], [])];
+  [ "lib"; "intvector_intrinsics"; "vec256_interleave_low64"],
+    [Name (["lib"; "intvector_intrinsics"; "vec256"], []);
+     Name (["lib"; "intvector_intrinsics"; "vec256"], [])];
+  [ "lib"; "intvector_intrinsics"; "vec256_interleave_low128"],
+    [Name (["lib"; "intvector_intrinsics"; "vec256"], []);
+     Name (["lib"; "intvector_intrinsics"; "vec256"], [])];
+  [ "lib"; "intvector_intrinsics"; "vec256_interleave_high64"],
+    [Name (["lib"; "intvector_intrinsics"; "vec256"], []);
+     Name (["lib"; "intvector_intrinsics"; "vec256"], [])];
+  [ "lib"; "intvector_intrinsics"; "vec256_interleave_high128"],
+    [Name (["lib"; "intvector_intrinsics"; "vec256"], []);
+     Name (["lib"; "intvector_intrinsics"; "vec256"], [])];
+  [ "lib"; "intvector_intrinsics"; "vec256_load64"], [Constant UInt64];
   [ "lib"; "intvector_intrinsics"; "vec256_load64s"],
     [ Constant UInt64; Constant UInt64; Constant UInt64; Constant UInt64];
+  [ "lib"; "intvector_intrinsics"; "vec256_load64_be"], [Ref (None, Shared, Constant UInt8)];
+  [ "lib"; "intvector_intrinsics"; "vec256_load64_le"], [Ref (None, Shared, Constant UInt8)];
+  [ "lib"; "intvector_intrinsics"; "vec256_lognot"],
+    [Name (["lib"; "intvector_intrinsics"; "vec256"], [])];
+  [ "lib"; "intvector_intrinsics"; "vec256_or"],
+    [Name (["lib"; "intvector_intrinsics"; "vec256"], []);
+     Name (["lib"; "intvector_intrinsics"; "vec256"], [])];
   [ "lib"; "intvector_intrinsics"; "vec256_rotate_right64"],
     [Name (["lib"; "intvector_intrinsics"; "vec256"], []); Constant UInt32];
   [ "lib"; "intvector_intrinsics"; "vec256_rotate_right_lanes64"],
     [Name (["lib"; "intvector_intrinsics"; "vec256"], []); Constant UInt32];
+  [ "lib"; "intvector_intrinsics"; "vec256_shift_left64"],
+    [Name (["lib"; "intvector_intrinsics"; "vec256"], []); Constant UInt32];
+  [ "lib"; "intvector_intrinsics"; "vec256_shift_right64"],
+    [Name (["lib"; "intvector_intrinsics"; "vec256"], []); Constant UInt32];
   [ "lib"; "intvector_intrinsics"; "vec256_store64_le"],
     [Ref (None, Mut, Constant UInt8); Name (["lib"; "intvector_intrinsics"; "vec256"], [])];
   [ "lib"; "intvector_intrinsics"; "vec256_xor"],
@@ -398,10 +443,16 @@ let builtins : (name * typ list) list = [
      Name (["lib"; "intvector_intrinsics"; "vec256"], [])];
 
   (* LowStar.Endianness *)
+  [ "lowstar"; "endianness"; "load32_be" ], [Ref (None, Shared, Constant UInt8)];
   [ "lowstar"; "endianness"; "load32_le" ], [Ref (None, Shared, Constant UInt8)];
+  [ "lowstar"; "endianness"; "store32_be" ], [Ref (None, Mut, Constant UInt8); Constant UInt32];
   [ "lowstar"; "endianness"; "store32_le" ], [Ref (None, Mut, Constant UInt8); Constant UInt32];
+  [ "lowstar"; "endianness"; "load64_be" ], [Ref (None, Shared, Constant UInt8)];
   [ "lowstar"; "endianness"; "load64_le" ], [Ref (None, Shared, Constant UInt8)];
+  [ "lowstar"; "endianness"; "store64_be" ], [Ref (None, Mut, Constant UInt8); Constant UInt64];
   [ "lowstar"; "endianness"; "store64_le" ], [Ref (None, Mut, Constant UInt8); Constant UInt64];
+  [ "lowstar"; "endianness"; "store128_be" ],
+    [Ref (None, Mut, Constant UInt8); Name (["fstar"; "uint128"; "uint128"], [])];
 
   (* Vec *)
   [ "Vec"; "new" ], [];

From 170b0a947fbd7e97a48e70bea963118235d0bad7 Mon Sep 17 00:00:00 2001
From: Aymeric Fromherz <aymeric.fromherz@inria.fr>
Date: Thu, 18 Jul 2024 14:23:27 +0200
Subject: [PATCH 34/52] More builtins, handle borrowing globals

---
 lib/OptimizeMiniRust.ml | 43 ++++++++++++++++++++++++++---------------
 1 file changed, 27 insertions(+), 16 deletions(-)

diff --git a/lib/OptimizeMiniRust.ml b/lib/OptimizeMiniRust.ml
index 81e162a4..a765f756 100644
--- a/lib/OptimizeMiniRust.ml
+++ b/lib/OptimizeMiniRust.ml
@@ -52,11 +52,11 @@ let assert_name (t: typ option) = match t with
   | _ -> failwith "impossible: assert_name"
 
 let add_mut_var a known =
-  KPrint.bprintf "%s is let mut\n" (Ast.show_atom_t a);
+  (* KPrint.bprintf "%s is let mut\n" (Ast.show_atom_t a); *)
   { known with v = VarSet.add a known.v }
 
 let add_mut_borrow a known =
-  KPrint.bprintf "%s is &mut\n" (Ast.show_atom_t a);
+  (* KPrint.bprintf "%s is &mut\n" (Ast.show_atom_t a); *)
   { known with r = VarSet.add a known.r }
 
 let want_mut_var a known =
@@ -127,15 +127,15 @@ let rec infer (env: env) (expected: typ) (known: known) (e: expr): known * expr
         known, e
 
   | Let (b, e1, e2) ->
-      KPrint.bprintf "[infer-mut,let] %a\n" PrintMiniRust.pexpr e;
+      (* KPrint.bprintf "[infer-mut,let] %a\n" PrintMiniRust.pexpr e; *)
       let a, e2 = open_ b e2 in
-      KPrint.bprintf "[infer-mut,let] opened %s[%s]\n" b.name (show_atom_t a);
+      (* KPrint.bprintf "[infer-mut,let] opened %s[%s]\n" b.name (show_atom_t a); *)
       let known, e2 = infer env expected known e2 in
       let mut_var = want_mut_var a known in
       let mut_borrow = want_mut_borrow a known in
-      KPrint.bprintf "[infer-mut,let-done-e2] %s[%s]: %a let mut ? %b &mut ? %b\n" b.name
+      (* KPrint.bprintf "[infer-mut,let-done-e2] %s[%s]: %a let mut ? %b &mut ? %b\n" b.name
         (show_atom_t a)
-        PrintMiniRust.ptyp b.typ mut_var mut_borrow;
+        PrintMiniRust.ptyp b.typ mut_var mut_borrow; *)
       let t1 = if mut_borrow then make_mut_borrow b.typ else b.typ in
       let known, e1 = infer env t1 known e1 in
       known, Let ({ b with mut = mut_var; typ = t1 }, e1, close a (Var 0) (lift 1 e2))
@@ -184,7 +184,7 @@ let rec infer (env: env) (expected: typ) (known: known) (e: expr): known * expr
       failwith "TODO: Call"
 
   | Assign (Open { atom; _ }, e3, t) ->
-      KPrint.bprintf "[infer-mut,assign] %a\n" PrintMiniRust.pexpr e;
+      (* KPrint.bprintf "[infer-mut,assign] %a\n" PrintMiniRust.pexpr e; *)
       let known, e3 = infer env t known e3 in
       add_mut_var atom known, e3
 
@@ -197,7 +197,7 @@ let rec infer (env: env) (expected: typ) (known: known) (e: expr): known * expr
    *)
   | Assign (Index (Field (Open {atom;_}, "0", None) as e1, e2), e3, t)
   | Assign (Index (Field (Open {atom;_}, "1", None) as e1, e2), e3, t) ->
-      KPrint.bprintf "[infer-mut,assign] %a\n" PrintMiniRust.pexpr e;
+      (* KPrint.bprintf "[infer-mut,assign] %a\n" PrintMiniRust.pexpr e; *)
       let known = add_mut_borrow atom known in
       let known, e2 = infer env usize known e2 in
       let known, e3 = infer env t known e3 in
@@ -210,7 +210,7 @@ let rec infer (env: env) (expected: typ) (known: known) (e: expr): known * expr
       known, Assign (Index (e1, e2), e3, t)
 
   | Assign (Index (Borrow (_, (Open { atom; _ } as e1)), e2), e3, t) ->
-      KPrint.bprintf "[infer-mut,assign] %a\n" PrintMiniRust.pexpr e;
+      (* KPrint.bprintf "[infer-mut,assign] %a\n" PrintMiniRust.pexpr e; *)
       let known = add_mut_var atom known in
       let known, e2 = infer env usize known e2 in
       let known, e3 = infer env t known e3 in
@@ -226,6 +226,12 @@ let rec infer (env: env) (expected: typ) (known: known) (e: expr): known * expr
       let known, e3 = infer env t known e3 in
       known, Assign (Field (Index (e1, e2), f, st), e3, t)
 
+  | Assign (Index (Borrow (_, Name n), e2), e3, t) ->
+      (* This case should only occur for globals. For now, we simply mutably borrow it *)
+      let known, e2 = infer env usize known e2 in
+      let known, e3 = infer env t known e3 in
+      known, Assign (Index (Borrow (Mut, Name n), e2), e3, t)
+
   | Assign _ ->
       KPrint.bprintf "[infer-mut,assign] %a unsupported\n" PrintMiniRust.pexpr e;
       failwith "TODO: unknown assignment"
@@ -301,7 +307,7 @@ let rec infer (env: env) (expected: typ) (known: known) (e: expr): known * expr
       | [ "push" ] ->
           known, MethodCall (e1, m, e2)
       | _ ->
-          KPrint.bprintf "%a\n" PrintMiniRust.pexpr e;
+          KPrint.bprintf "%a unsupported\n" PrintMiniRust.pexpr e;
           failwith "TODO: MethodCall"
       end
 
@@ -357,6 +363,11 @@ let rec infer (env: env) (expected: typ) (known: known) (e: expr): known * expr
    Type substitutions are currently not supported, functions with generic
    args should be added directly to Call in infer *)
 let builtins : (name * typ list) list = [
+  (* EverCrypt.TargetConfig. The following two functions are handwritten,
+     while the rest of EverCrypt is generated *)
+  [ "evercrypt"; "targetconfig"; "has_vec128_not_avx" ], [];
+  [ "evercrypt"; "targetconfig"; "has_vec256_not_avx2" ], [];
+
   (* FStar.UInt128 *)
   [ "fstar"; "uint128"; "uint64_to_uint128" ], [Constant UInt64];
   [ "fstar"; "uint128"; "uint128_to_uint64" ], [Name (["fstar"; "uint128"; "uint128"], [])];
@@ -467,23 +478,23 @@ let infer_mut_borrows files =
       let env, decls = List.fold_left (fun (env, decls) decl ->
         match decl with
         | Function ({ name; body; return_type; parameters; _ } as f) ->
-            KPrint.bprintf "[infer-mut] visiting %s\n%a\n" (String.concat "." name)
-              PrintMiniRust.pdecl decl;
+            (* KPrint.bprintf "[infer-mut] visiting %s\n%a\n" (String.concat "." name)
+              PrintMiniRust.pdecl decl; *)
             let atoms, body =
               List.fold_right (fun binder (atoms, e) ->
                 let a, e = open_ binder e in
-                KPrint.bprintf "[infer-mut] opened %s[%s]\n%a\n" binder.name (show_atom_t a) PrintMiniRust.pexpr e;
+                (* KPrint.bprintf "[infer-mut] opened %s[%s]\n%a\n" binder.name (show_atom_t a) PrintMiniRust.pexpr e; *)
                 a :: atoms, e
               ) parameters ([], body)
             in
-            KPrint.bprintf "[infer-mut] done opening %s\n%a\n" (String.concat "." name)
-              PrintMiniRust.pexpr body;
+            (* KPrint.bprintf "[infer-mut] done opening %s\n%a\n" (String.concat "." name)
+              PrintMiniRust.pexpr body; *)
             (* Start the analysis with the current state of struct mutability *)
             let known, body = infer env return_type {known with structs = env.structs} body in
             let parameters, body =
               List.fold_left2 (fun (parameters, e) (binder: binding) atom ->
                 let e = close atom (Var 0) (lift 1 e) in
-                KPrint.bprintf "[infer-mut] closed %s[%s]\n%a\n" binder.name (show_atom_t atom) PrintMiniRust.pexpr e;
+                (* KPrint.bprintf "[infer-mut] closed %s[%s]\n%a\n" binder.name (show_atom_t atom) PrintMiniRust.pexpr e; *)
                 let mut = want_mut_var atom known in
                 let typ = if want_mut_borrow atom known then make_mut_borrow binder.typ else binder.typ in
                 { binder with mut; typ } :: parameters, e

From 081369d2adec21c79e620ca12fda76a31953e6a9 Mon Sep 17 00:00:00 2001
From: Aymeric Fromherz <aymeric.fromherz@inria.fr>
Date: Thu, 18 Jul 2024 14:31:45 +0200
Subject: [PATCH 35/52] Fix builtin types when taking slices

---
 lib/MiniRust.ml         |  1 +
 lib/OptimizeMiniRust.ml | 34 ++++++++++++++++++++--------------
 2 files changed, 21 insertions(+), 14 deletions(-)

diff --git a/lib/MiniRust.ml b/lib/MiniRust.ml
index 40293e9d..786db34e 100644
--- a/lib/MiniRust.ml
+++ b/lib/MiniRust.ml
@@ -53,6 +53,7 @@ let box t =
   App (Name (["Box"], []), [t])
 
 let bool = Constant Bool
+let u8 = Constant UInt8
 let u32 = Constant UInt32
 let usize = Constant SizeT
 
diff --git a/lib/OptimizeMiniRust.ml b/lib/OptimizeMiniRust.ml
index a765f756..2011f5b8 100644
--- a/lib/OptimizeMiniRust.ml
+++ b/lib/OptimizeMiniRust.ml
@@ -399,13 +399,13 @@ let builtins : (name * typ list) list = [
   [ "lib"; "intvector_intrinsics"; "vec128_load32"], [Constant UInt32];
   [ "lib"; "intvector_intrinsics"; "vec128_load32s"],
     [ Constant UInt32; Constant UInt32; Constant UInt32; Constant UInt32];
-  [ "lib"; "intvector_intrinsics"; "vec128_load32_be"], [Ref (None, Shared, Constant UInt8)];
+  [ "lib"; "intvector_intrinsics"; "vec128_load32_be"], [Ref (None, Shared, Slice u8)];
   [ "lib"; "intvector_intrinsics"; "vec128_rotate_right32"],
     [Name (["lib"; "intvector_intrinsics"; "vec128"], []); Constant UInt32];
   [ "lib"; "intvector_intrinsics"; "vec128_rotate_right_lanes32"],
     [Name (["lib"; "intvector_intrinsics"; "vec128"], []); Constant UInt32];
   [ "lib"; "intvector_intrinsics"; "vec128_store32_le"],
-    [Ref (None, Mut, Constant UInt8); Name (["lib"; "intvector_intrinsics"; "vec128"], [])];
+    [Ref (None, Mut, Slice u8); Name (["lib"; "intvector_intrinsics"; "vec128"], [])];
   [ "lib"; "intvector_intrinsics"; "vec128_xor"],
     [Name (["lib"; "intvector_intrinsics"; "vec128"], []);
      Name (["lib"; "intvector_intrinsics"; "vec128"], [])];
@@ -432,8 +432,8 @@ let builtins : (name * typ list) list = [
   [ "lib"; "intvector_intrinsics"; "vec256_load64"], [Constant UInt64];
   [ "lib"; "intvector_intrinsics"; "vec256_load64s"],
     [ Constant UInt64; Constant UInt64; Constant UInt64; Constant UInt64];
-  [ "lib"; "intvector_intrinsics"; "vec256_load64_be"], [Ref (None, Shared, Constant UInt8)];
-  [ "lib"; "intvector_intrinsics"; "vec256_load64_le"], [Ref (None, Shared, Constant UInt8)];
+  [ "lib"; "intvector_intrinsics"; "vec256_load64_be"], [Ref (None, Shared, Slice u8)];
+  [ "lib"; "intvector_intrinsics"; "vec256_load64_le"], [Ref (None, Shared, Slice u8)];
   [ "lib"; "intvector_intrinsics"; "vec256_lognot"],
     [Name (["lib"; "intvector_intrinsics"; "vec256"], [])];
   [ "lib"; "intvector_intrinsics"; "vec256_or"],
@@ -448,25 +448,31 @@ let builtins : (name * typ list) list = [
   [ "lib"; "intvector_intrinsics"; "vec256_shift_right64"],
     [Name (["lib"; "intvector_intrinsics"; "vec256"], []); Constant UInt32];
   [ "lib"; "intvector_intrinsics"; "vec256_store64_le"],
-    [Ref (None, Mut, Constant UInt8); Name (["lib"; "intvector_intrinsics"; "vec256"], [])];
+    [Ref (None, Mut, Slice u8); Name (["lib"; "intvector_intrinsics"; "vec256"], [])];
   [ "lib"; "intvector_intrinsics"; "vec256_xor"],
     [Name (["lib"; "intvector_intrinsics"; "vec256"], []);
      Name (["lib"; "intvector_intrinsics"; "vec256"], [])];
 
   (* LowStar.Endianness *)
-  [ "lowstar"; "endianness"; "load32_be" ], [Ref (None, Shared, Constant UInt8)];
-  [ "lowstar"; "endianness"; "load32_le" ], [Ref (None, Shared, Constant UInt8)];
-  [ "lowstar"; "endianness"; "store32_be" ], [Ref (None, Mut, Constant UInt8); Constant UInt32];
-  [ "lowstar"; "endianness"; "store32_le" ], [Ref (None, Mut, Constant UInt8); Constant UInt32];
-  [ "lowstar"; "endianness"; "load64_be" ], [Ref (None, Shared, Constant UInt8)];
-  [ "lowstar"; "endianness"; "load64_le" ], [Ref (None, Shared, Constant UInt8)];
-  [ "lowstar"; "endianness"; "store64_be" ], [Ref (None, Mut, Constant UInt8); Constant UInt64];
-  [ "lowstar"; "endianness"; "store64_le" ], [Ref (None, Mut, Constant UInt8); Constant UInt64];
+  [ "lowstar"; "endianness"; "load32_be" ], [Ref (None, Shared, Slice u8)];
+  [ "lowstar"; "endianness"; "load32_le" ], [Ref (None, Shared, Slice u8)];
+  [ "lowstar"; "endianness"; "store32_be" ], [Ref (None, Mut, Slice u8); Constant UInt32];
+  [ "lowstar"; "endianness"; "store32_le" ], [Ref (None, Mut, Slice u8); Constant UInt32];
+  [ "lowstar"; "endianness"; "load64_be" ], [Ref (None, Shared, Slice u8)];
+  [ "lowstar"; "endianness"; "load64_le" ], [Ref (None, Shared, Slice u8)];
+  [ "lowstar"; "endianness"; "store64_be" ], [Ref (None, Mut, Slice u8); Constant UInt64];
+  [ "lowstar"; "endianness"; "store64_le" ], [Ref (None, Mut, Slice u8); Constant UInt64];
   [ "lowstar"; "endianness"; "store128_be" ],
-    [Ref (None, Mut, Constant UInt8); Name (["fstar"; "uint128"; "uint128"], [])];
+    [Ref (None, Mut, Slice u8); Name (["fstar"; "uint128"; "uint128"], [])];
 
   (* Vec *)
   [ "Vec"; "new" ], [];
+
+  (* Vale assembly functions marked as extern. This should probably be handled earlier *)
+  [ "vale"; "stdcalls_x64_sha"; "sha256_update"], [
+    Ref (None, Mut, Slice u32); Ref (None, Shared, Slice u8); u32;
+    Ref (None, Shared, Slice u32)  
+  ];
 ]
 
 let infer_mut_borrows files =

From 72e742a34bb33acf175d0602dc22835c7165a0e9 Mon Sep 17 00:00:00 2001
From: Aymeric Fromherz <aymeric.fromherz@inria.fr>
Date: Thu, 18 Jul 2024 14:44:30 +0200
Subject: [PATCH 36/52] more builtins

---
 lib/MiniRust.ml         |  2 ++
 lib/OptimizeMiniRust.ml | 25 +++++++++++++++++++++++++
 2 files changed, 27 insertions(+)

diff --git a/lib/MiniRust.ml b/lib/MiniRust.ml
index 786db34e..c2f07500 100644
--- a/lib/MiniRust.ml
+++ b/lib/MiniRust.ml
@@ -54,7 +54,9 @@ let box t =
 
 let bool = Constant Bool
 let u8 = Constant UInt8
+let u16 = Constant UInt16
 let u32 = Constant UInt32
+let u64 = Constant UInt64
 let usize = Constant SizeT
 
 type binding = { name: string; typ: typ; mut: bool }
diff --git a/lib/OptimizeMiniRust.ml b/lib/OptimizeMiniRust.ml
index 2011f5b8..78c3fcba 100644
--- a/lib/OptimizeMiniRust.ml
+++ b/lib/OptimizeMiniRust.ml
@@ -368,6 +368,23 @@ let builtins : (name * typ list) list = [
   [ "evercrypt"; "targetconfig"; "has_vec128_not_avx" ], [];
   [ "evercrypt"; "targetconfig"; "has_vec256_not_avx2" ], [];
 
+  (* FStar.UInt8 *)
+  [ "fstar"; "uint8"; "eq_mask" ], [ u8; u8 ];
+  [ "fstar"; "uint8"; "gte_mask" ], [ u8; u8 ];
+
+  (* FStar.UInt16 *)
+  [ "fstar"; "uint16"; "eq_mask" ], [ u16; u16 ];
+  [ "fstar"; "uint16"; "gte_mask" ], [ u16; u16 ];
+
+  (* FStar.UInt32 *)
+  [ "fstar"; "uint32"; "eq_mask" ], [ u32; u32 ];
+  [ "fstar"; "uint32"; "gte_mask" ], [ u32; u32 ];
+
+  (* FStar.UInt64 *)
+  [ "fstar"; "uint64"; "eq_mask" ], [ u64; u64 ];
+  [ "fstar"; "uint64"; "gte_mask" ], [ u64; u64 ];
+
+
   (* FStar.UInt128 *)
   [ "fstar"; "uint128"; "uint64_to_uint128" ], [Constant UInt64];
   [ "fstar"; "uint128"; "uint128_to_uint64" ], [Name (["fstar"; "uint128"; "uint128"], [])];
@@ -375,11 +392,19 @@ let builtins : (name * typ list) list = [
       [Name (["fstar"; "uint128"; "uint128"], []); Name (["fstar"; "uint128"; "uint128"], [])];
   [ "fstar"; "uint128"; "add_mod" ],
       [Name (["fstar"; "uint128"; "uint128"], []); Name (["fstar"; "uint128"; "uint128"], [])];
+  [ "fstar"; "uint128"; "mul_wide" ], [Constant UInt64; Constant UInt64];
   [ "fstar"; "uint128"; "shift_left" ],
       [Name (["fstar"; "uint128"; "uint128"], []); Constant UInt32];
   [ "fstar"; "uint128"; "shift_right" ],
       [Name (["fstar"; "uint128"; "uint128"], []); Constant UInt32];
 
+  (* Lib.Inttypes_Intrinsics *)
+  [ "lib"; "inttypes_intrinsics"; "add_carry_u32"], [ u32; u32; u32; Ref (None, Mut, Slice u32) ];
+  [ "lib"; "inttypes_intrinsics"; "sub_borrow_u32"], [ u32; u32; u32; Ref (None, Mut, Slice u32) ];
+  [ "lib"; "inttypes_intrinsics"; "add_carry_u64"], [ u64; u64; u64; Ref (None, Mut, Slice u64) ];
+  [ "lib"; "inttypes_intrinsics"; "sub_borrow_u64"], [ u64; u64; u64; Ref (None, Mut, Slice u64) ];
+
+
   (* Lib.IntVector_intrinsics, Vec128 *)
   [ "lib"; "intvector_intrinsics"; "vec128_add32"],
     [Name (["lib"; "intvector_intrinsics"; "vec128"], []);

From c9f9d1b2a9b3e590383720063b76f1bd4b9f506b Mon Sep 17 00:00:00 2001
From: Aymeric Fromherz <aymeric.fromherz@inria.fr>
Date: Thu, 18 Jul 2024 17:32:41 +0200
Subject: [PATCH 37/52] Mark vale functions as builtins for now

---
 lib/OptimizeMiniRust.ml | 84 ++++++++++++++++++++++++++++++++++++++++-
 1 file changed, 83 insertions(+), 1 deletion(-)

diff --git a/lib/OptimizeMiniRust.ml b/lib/OptimizeMiniRust.ml
index 78c3fcba..7fb9f4cf 100644
--- a/lib/OptimizeMiniRust.ml
+++ b/lib/OptimizeMiniRust.ml
@@ -173,10 +173,12 @@ let rec infer (env: env) (expected: typ) (known: known) (e: expr): known * expr
   | Call (Operator o, [], _) -> begin match o with
       (* Most operators are wrapping and were translated to a methodcall.
          We list the few remaining ones here *)
+      | Add | Sub
       | BOr | BAnd | BXor | BNot
       | Eq | Neq | Lt | Lte | Gt | Gte
       | And | Or | Xor | Not -> known, e
       | _ ->
+        KPrint.bprintf "[infer-mut,call] %a not supported\n" PrintMiniRust.pexpr e;
         failwith "TODO: operator not supported"
     end
 
@@ -281,7 +283,8 @@ let rec infer (env: env) (expected: typ) (known: known) (e: expr): known * expr
       begin match m with
       | [ "wrapping_add" ] | [ "wrapping_div" ] | [ "wrapping_mul" ] 
       | [ "wrapping_neg" ] | [ "wrapping_rem" ] | [ "wrapping_shl" ]
-      | [ "wrapping_shr" ] | [ "wrapping_sub" ] ->
+      | [ "wrapping_shr" ] | [ "wrapping_sub" ]
+      | [ "to_vec" ] ->
           known, MethodCall (e1, m, e2)
       | ["split_at"] ->
           assert (List.length e2 = 1);
@@ -498,6 +501,85 @@ let builtins : (name * typ list) list = [
     Ref (None, Mut, Slice u32); Ref (None, Shared, Slice u8); u32;
     Ref (None, Shared, Slice u32)  
   ];
+  [ "vale"; "inline_x64_fadd_inline"; "add_scalar" ], [
+    Ref (None, Mut, Slice u64); Ref (None, Shared, Slice u64); Ref (None, Shared, Slice u64)
+  ];
+  [ "vale"; "stdcalls_x64_fadd"; "add_scalar_e" ], [
+    Ref (None, Mut, Slice u64); Ref (None, Shared, Slice u64); Ref (None, Shared, Slice u64)
+  ];
+  [ "vale"; "inline_x64_fadd_inline"; "fadd" ], [
+    Ref (None, Mut, Slice u64); Ref (None, Shared, Slice u64); Ref (None, Shared, Slice u64)
+  ];
+  [ "vale"; "stdcalls_x64_fadd"; "fadd_e" ], [
+    Ref (None, Mut, Slice u64); Ref (None, Shared, Slice u64); Ref (None, Shared, Slice u64)
+  ];
+  [ "vale"; "inline_x64_fadd_inline"; "fsub" ], [
+    Ref (None, Mut, Slice u64); Ref (None, Shared, Slice u64); Ref (None, Shared, Slice u64)
+  ];
+  [ "vale"; "stdcalls_x64_fsub"; "fsub_e" ], [
+    Ref (None, Mut, Slice u64); Ref (None, Shared, Slice u64); Ref (None, Shared, Slice u64)
+  ];
+  [ "vale"; "inline_x64_fmul_inline"; "fmul" ], [
+    Ref (None, Mut, Slice u64); Ref (None, Shared, Slice u64);
+    Ref (None, Shared, Slice u64); Ref (None, Mut, Slice u64);
+  ];
+  [ "vale"; "stdcalls_x64_fmul"; "fmul_e" ], [
+    Ref (None, Mut, Slice u64); Ref (None, Shared, Slice u64);
+    Ref (None, Shared, Slice u64); Ref (None, Mut, Slice u64);
+  ];
+  [ "vale"; "inline_x64_fmul_inline"; "fmul2" ], [
+    Ref (None, Mut, Slice u64); Ref (None, Shared, Slice u64);
+    Ref (None, Shared, Slice u64); Ref (None, Mut, Slice u64);
+  ];
+  [ "vale"; "stdcalls_x64_fmul"; "fmul2_e" ], [
+    Ref (None, Mut, Slice u64); Ref (None, Shared, Slice u64);
+    Ref (None, Shared, Slice u64); Ref (None, Mut, Slice u64);
+  ];
+  [ "vale"; "inline_x64_fmul_inline"; "fmul_scalar" ], [
+    Ref (None, Mut, Slice u64); Ref (None, Shared, Slice u64); u64
+  ];
+  [ "vale"; "stdcalls_x64_fmul"; "fmul_scalar_e" ], [
+    Ref (None, Mut, Slice u64); Ref (None, Shared, Slice u64); u64
+  ];
+  [ "vale"; "inline_x64_fsqr_inline"; "fsqr" ], [
+    Ref (None, Mut, Slice u64); Ref (None, Shared, Slice u64); Ref (None, Mut, Slice u64)
+  ];
+  [ "vale"; "stdcalls_x64_fsqr"; "fsqr_e" ], [
+    Ref (None, Mut, Slice u64); Ref (None, Shared, Slice u64); Ref (None, Mut, Slice u64)
+  ];
+  [ "vale"; "inline_x64_fsqr_inline"; "fsqr2" ], [
+    Ref (None, Mut, Slice u64); Ref (None, Shared, Slice u64); Ref (None, Mut, Slice u64)
+  ];
+  [ "vale"; "stdcalls_x64_fsqr"; "fsqr2_e" ], [
+    Ref (None, Mut, Slice u64); Ref (None, Shared, Slice u64); Ref (None, Mut, Slice u64)
+  ];
+  [ "vale"; "inline_x64_fswap_inline"; "cswap2" ], [
+    u64; Ref (None, Mut, Slice u64); Ref (None, Mut, Slice u64)
+  ];
+  [ "vale"; "stdcalls_x64_fswap"; "cswap2_e" ], [
+    u64; Ref (None, Mut, Slice u64); Ref (None, Mut, Slice u64)
+  ];
+
+  (* TODO: These functions are recursive, and should be handled properly.
+     For now, we hardcode their expected type and mutability in HACL *)
+  [ "hacl"; "bignum"; "bn_karatsuba_mul_uint32"], [
+      u32; Ref (None, Shared, Slice u32); Ref (None, Shared, Slice u32);
+      Ref (None, Mut, Slice u32); Ref (None, Mut, Slice u32)
+  ];
+  [ "hacl"; "bignum"; "bn_karatsuba_mul_uint64"], [
+      u64; Ref (None, Shared, Slice u64); Ref (None, Shared, Slice u64);
+      Ref (None, Mut, Slice u64); Ref (None, Mut, Slice u64)
+  ];
+  [ "hacl"; "bignum"; "bn_karatsuba_sqr_uint32"], [
+      u32; Ref (None, Shared, Slice u32);
+      Ref (None, Mut, Slice u32); Ref (None, Mut, Slice u32)
+  ];
+  [ "hacl"; "bignum"; "bn_karatsuba_sqr_uint64"], [
+      u64; Ref (None, Shared, Slice u64);
+      Ref (None, Mut, Slice u64); Ref (None, Mut, Slice u64)
+  ];
+    
+
 ]
 
 let infer_mut_borrows files =

From c06f8259661ac4d2a8a6f62149796612596af1f0 Mon Sep 17 00:00:00 2001
From: Aymeric Fromherz <aymeric.fromherz@inria.fr>
Date: Thu, 18 Jul 2024 17:59:00 +0200
Subject: [PATCH 38/52] More Intvector intrinsics

---
 lib/OptimizeMiniRust.ml | 68 +++++++++++++++++++++++++++++++++++++++++
 1 file changed, 68 insertions(+)

diff --git a/lib/OptimizeMiniRust.ml b/lib/OptimizeMiniRust.ml
index 7fb9f4cf..2ac17beb 100644
--- a/lib/OptimizeMiniRust.ml
+++ b/lib/OptimizeMiniRust.ml
@@ -412,6 +412,22 @@ let builtins : (name * typ list) list = [
   [ "lib"; "intvector_intrinsics"; "vec128_add32"],
     [Name (["lib"; "intvector_intrinsics"; "vec128"], []);
      Name (["lib"; "intvector_intrinsics"; "vec128"], [])];
+  [ "lib"; "intvector_intrinsics"; "vec128_add64"],
+    [Name (["lib"; "intvector_intrinsics"; "vec128"], []);
+     Name (["lib"; "intvector_intrinsics"; "vec128"], [])];
+  [ "lib"; "intvector_intrinsics"; "vec128_and"],
+    [Name (["lib"; "intvector_intrinsics"; "vec128"], []);
+     Name (["lib"; "intvector_intrinsics"; "vec128"], [])];
+  [ "lib"; "intvector_intrinsics"; "vec128_eq64"],
+    [Name (["lib"; "intvector_intrinsics"; "vec128"], []);
+     Name (["lib"; "intvector_intrinsics"; "vec128"], [])];
+  [ "lib"; "intvector_intrinsics"; "vec128_extract64"],
+    [Name (["lib"; "intvector_intrinsics"; "vec128"], []); Constant UInt32];
+  [ "lib"; "intvector_intrinsics"; "vec128_gt64"],
+    [Name (["lib"; "intvector_intrinsics"; "vec128"], []);
+     Name (["lib"; "intvector_intrinsics"; "vec128"], [])];
+  [ "lib"; "intvector_intrinsics"; "vec128_insert64"],
+    [Name (["lib"; "intvector_intrinsics"; "vec128"], []); u64; u32];
   [ "lib"; "intvector_intrinsics"; "vec128_interleave_low32"],
     [Name (["lib"; "intvector_intrinsics"; "vec128"], []);
      Name (["lib"; "intvector_intrinsics"; "vec128"], [])];
@@ -428,23 +444,63 @@ let builtins : (name * typ list) list = [
   [ "lib"; "intvector_intrinsics"; "vec128_load32s"],
     [ Constant UInt32; Constant UInt32; Constant UInt32; Constant UInt32];
   [ "lib"; "intvector_intrinsics"; "vec128_load32_be"], [Ref (None, Shared, Slice u8)];
+  [ "lib"; "intvector_intrinsics"; "vec128_load32_le"], [Ref (None, Shared, Slice u8)];
+  [ "lib"; "intvector_intrinsics"; "vec128_load64"], [u64];
+  [ "lib"; "intvector_intrinsics"; "vec128_load64_le"], [Ref (None, Shared, Slice u8)];
+  [ "lib"; "intvector_intrinsics"; "vec128_lognot"],
+    [Name (["lib"; "intvector_intrinsics"; "vec128"], [])];
+  [ "lib"; "intvector_intrinsics"; "vec128_mul32"],
+    [Name (["lib"; "intvector_intrinsics"; "vec128"], []);
+     Name (["lib"; "intvector_intrinsics"; "vec128"], [])];
+  [ "lib"; "intvector_intrinsics"; "vec128_mul64"],
+    [Name (["lib"; "intvector_intrinsics"; "vec128"], []);
+     Name (["lib"; "intvector_intrinsics"; "vec128"], [])];
+  [ "lib"; "intvector_intrinsics"; "vec128_or"],
+    [Name (["lib"; "intvector_intrinsics"; "vec128"], []);
+     Name (["lib"; "intvector_intrinsics"; "vec128"], [])];
+  [ "lib"; "intvector_intrinsics"; "vec128_rotate_left32"],
+    [Name (["lib"; "intvector_intrinsics"; "vec128"], []); Constant UInt32];
   [ "lib"; "intvector_intrinsics"; "vec128_rotate_right32"],
     [Name (["lib"; "intvector_intrinsics"; "vec128"], []); Constant UInt32];
   [ "lib"; "intvector_intrinsics"; "vec128_rotate_right_lanes32"],
     [Name (["lib"; "intvector_intrinsics"; "vec128"], []); Constant UInt32];
+  [ "lib"; "intvector_intrinsics"; "vec128_shift_left64"],
+    [Name (["lib"; "intvector_intrinsics"; "vec128"], []); Constant UInt32];
+  [ "lib"; "intvector_intrinsics"; "vec128_shift_right64"],
+    [Name (["lib"; "intvector_intrinsics"; "vec128"], []); Constant UInt32];
+  [ "lib"; "intvector_intrinsics"; "vec128_smul64"],
+    [Name (["lib"; "intvector_intrinsics"; "vec128"], []); u64];
+  [ "lib"; "intvector_intrinsics"; "vec128_store32_be"],
+    [Ref (None, Mut, Slice u8); Name (["lib"; "intvector_intrinsics"; "vec128"], [])];
   [ "lib"; "intvector_intrinsics"; "vec128_store32_le"],
     [Ref (None, Mut, Slice u8); Name (["lib"; "intvector_intrinsics"; "vec128"], [])];
+  [ "lib"; "intvector_intrinsics"; "vec128_sub64"],
+    [Name (["lib"; "intvector_intrinsics"; "vec128"], []);
+     Name (["lib"; "intvector_intrinsics"; "vec128"], [])];
   [ "lib"; "intvector_intrinsics"; "vec128_xor"],
     [Name (["lib"; "intvector_intrinsics"; "vec128"], []);
      Name (["lib"; "intvector_intrinsics"; "vec128"], [])];
 
   (* Lib.IntVector_intrinsics, Vec256 *)
+  [ "lib"; "intvector_intrinsics"; "vec256_add32"],
+    [Name (["lib"; "intvector_intrinsics"; "vec256"], []);
+     Name (["lib"; "intvector_intrinsics"; "vec256"], [])];
   [ "lib"; "intvector_intrinsics"; "vec256_add64"],
     [Name (["lib"; "intvector_intrinsics"; "vec256"], []);
      Name (["lib"; "intvector_intrinsics"; "vec256"], [])];
   [ "lib"; "intvector_intrinsics"; "vec256_and"],
     [Name (["lib"; "intvector_intrinsics"; "vec256"], []);
      Name (["lib"; "intvector_intrinsics"; "vec256"], [])];
+  [ "lib"; "intvector_intrinsics"; "vec256_eq64"],
+    [Name (["lib"; "intvector_intrinsics"; "vec256"], []);
+     Name (["lib"; "intvector_intrinsics"; "vec256"], [])];
+  [ "lib"; "intvector_intrinsics"; "vec256_extract64"],
+    [Name (["lib"; "intvector_intrinsics"; "vec256"], []); u32];
+  [ "lib"; "intvector_intrinsics"; "vec256_gt64"],
+    [Name (["lib"; "intvector_intrinsics"; "vec256"], []);
+     Name (["lib"; "intvector_intrinsics"; "vec256"], [])];
+  [ "lib"; "intvector_intrinsics"; "vec256_insert64"],
+    [Name (["lib"; "intvector_intrinsics"; "vec256"], []); u64; u32];
   [ "lib"; "intvector_intrinsics"; "vec256_interleave_low64"],
     [Name (["lib"; "intvector_intrinsics"; "vec256"], []);
      Name (["lib"; "intvector_intrinsics"; "vec256"], [])];
@@ -464,6 +520,9 @@ let builtins : (name * typ list) list = [
   [ "lib"; "intvector_intrinsics"; "vec256_load64_le"], [Ref (None, Shared, Slice u8)];
   [ "lib"; "intvector_intrinsics"; "vec256_lognot"],
     [Name (["lib"; "intvector_intrinsics"; "vec256"], [])];
+  [ "lib"; "intvector_intrinsics"; "vec256_mul64"],
+    [Name (["lib"; "intvector_intrinsics"; "vec256"], []);
+     Name (["lib"; "intvector_intrinsics"; "vec256"], [])];
   [ "lib"; "intvector_intrinsics"; "vec256_or"],
     [Name (["lib"; "intvector_intrinsics"; "vec256"], []);
      Name (["lib"; "intvector_intrinsics"; "vec256"], [])];
@@ -473,10 +532,19 @@ let builtins : (name * typ list) list = [
     [Name (["lib"; "intvector_intrinsics"; "vec256"], []); Constant UInt32];
   [ "lib"; "intvector_intrinsics"; "vec256_shift_left64"],
     [Name (["lib"; "intvector_intrinsics"; "vec256"], []); Constant UInt32];
+  [ "lib"; "intvector_intrinsics"; "vec256_shift_right"],
+    [Name (["lib"; "intvector_intrinsics"; "vec256"], []); Constant UInt32];
   [ "lib"; "intvector_intrinsics"; "vec256_shift_right64"],
     [Name (["lib"; "intvector_intrinsics"; "vec256"], []); Constant UInt32];
+  [ "lib"; "intvector_intrinsics"; "vec256_smul64"],
+    [Name (["lib"; "intvector_intrinsics"; "vec256"], []); u64];
+  [ "lib"; "intvector_intrinsics"; "vec256_store64_be"],
+    [Ref (None, Mut, Slice u8); Name (["lib"; "intvector_intrinsics"; "vec256"], [])];
   [ "lib"; "intvector_intrinsics"; "vec256_store64_le"],
     [Ref (None, Mut, Slice u8); Name (["lib"; "intvector_intrinsics"; "vec256"], [])];
+  [ "lib"; "intvector_intrinsics"; "vec256_sub64"],
+    [Name (["lib"; "intvector_intrinsics"; "vec256"], []);
+     Name (["lib"; "intvector_intrinsics"; "vec256"], [])];
   [ "lib"; "intvector_intrinsics"; "vec256_xor"],
     [Name (["lib"; "intvector_intrinsics"; "vec256"], []);
      Name (["lib"; "intvector_intrinsics"; "vec256"], [])];

From 14165a0d807a53a9528737eb1f71618582de9c3b Mon Sep 17 00:00:00 2001
From: Aymeric Fromherz <aymeric.fromherz@inria.fr>
Date: Thu, 18 Jul 2024 18:06:46 +0200
Subject: [PATCH 39/52] More Intvector intrinsics

---
 lib/OptimizeMiniRust.ml | 18 ++++++++++++++++++
 1 file changed, 18 insertions(+)

diff --git a/lib/OptimizeMiniRust.ml b/lib/OptimizeMiniRust.ml
index 2ac17beb..9d560264 100644
--- a/lib/OptimizeMiniRust.ml
+++ b/lib/OptimizeMiniRust.ml
@@ -501,18 +501,28 @@ let builtins : (name * typ list) list = [
      Name (["lib"; "intvector_intrinsics"; "vec256"], [])];
   [ "lib"; "intvector_intrinsics"; "vec256_insert64"],
     [Name (["lib"; "intvector_intrinsics"; "vec256"], []); u64; u32];
+  [ "lib"; "intvector_intrinsics"; "vec256_interleave_low32"],
+    [Name (["lib"; "intvector_intrinsics"; "vec256"], []);
+     Name (["lib"; "intvector_intrinsics"; "vec256"], [])];
   [ "lib"; "intvector_intrinsics"; "vec256_interleave_low64"],
     [Name (["lib"; "intvector_intrinsics"; "vec256"], []);
      Name (["lib"; "intvector_intrinsics"; "vec256"], [])];
   [ "lib"; "intvector_intrinsics"; "vec256_interleave_low128"],
     [Name (["lib"; "intvector_intrinsics"; "vec256"], []);
      Name (["lib"; "intvector_intrinsics"; "vec256"], [])];
+  [ "lib"; "intvector_intrinsics"; "vec256_interleave_high32"],
+    [Name (["lib"; "intvector_intrinsics"; "vec256"], []);
+     Name (["lib"; "intvector_intrinsics"; "vec256"], [])];
   [ "lib"; "intvector_intrinsics"; "vec256_interleave_high64"],
     [Name (["lib"; "intvector_intrinsics"; "vec256"], []);
      Name (["lib"; "intvector_intrinsics"; "vec256"], [])];
   [ "lib"; "intvector_intrinsics"; "vec256_interleave_high128"],
     [Name (["lib"; "intvector_intrinsics"; "vec256"], []);
      Name (["lib"; "intvector_intrinsics"; "vec256"], [])];
+  [ "lib"; "intvector_intrinsics"; "vec256_load32"], [u32];
+  [ "lib"; "intvector_intrinsics"; "vec256_load32s"], [u32; u32; u32; u32; u32; u32; u32; u32]; 
+  [ "lib"; "intvector_intrinsics"; "vec256_load32_be"], [Ref (None, Shared, Slice u8)];
+  [ "lib"; "intvector_intrinsics"; "vec256_load32_le"], [Ref (None, Shared, Slice u8)];
   [ "lib"; "intvector_intrinsics"; "vec256_load64"], [Constant UInt64];
   [ "lib"; "intvector_intrinsics"; "vec256_load64s"],
     [ Constant UInt64; Constant UInt64; Constant UInt64; Constant UInt64];
@@ -526,6 +536,10 @@ let builtins : (name * typ list) list = [
   [ "lib"; "intvector_intrinsics"; "vec256_or"],
     [Name (["lib"; "intvector_intrinsics"; "vec256"], []);
      Name (["lib"; "intvector_intrinsics"; "vec256"], [])];
+  [ "lib"; "intvector_intrinsics"; "vec256_rotate_left32"],
+    [Name (["lib"; "intvector_intrinsics"; "vec256"], []); Constant UInt32];
+  [ "lib"; "intvector_intrinsics"; "vec256_rotate_right32"],
+    [Name (["lib"; "intvector_intrinsics"; "vec256"], []); Constant UInt32];
   [ "lib"; "intvector_intrinsics"; "vec256_rotate_right64"],
     [Name (["lib"; "intvector_intrinsics"; "vec256"], []); Constant UInt32];
   [ "lib"; "intvector_intrinsics"; "vec256_rotate_right_lanes64"],
@@ -538,6 +552,10 @@ let builtins : (name * typ list) list = [
     [Name (["lib"; "intvector_intrinsics"; "vec256"], []); Constant UInt32];
   [ "lib"; "intvector_intrinsics"; "vec256_smul64"],
     [Name (["lib"; "intvector_intrinsics"; "vec256"], []); u64];
+  [ "lib"; "intvector_intrinsics"; "vec256_store32_be"],
+    [Ref (None, Mut, Slice u8); Name (["lib"; "intvector_intrinsics"; "vec256"], [])];
+  [ "lib"; "intvector_intrinsics"; "vec256_store32_le"],
+    [Ref (None, Mut, Slice u8); Name (["lib"; "intvector_intrinsics"; "vec256"], [])];
   [ "lib"; "intvector_intrinsics"; "vec256_store64_be"],
     [Ref (None, Mut, Slice u8); Name (["lib"; "intvector_intrinsics"; "vec256"], [])];
   [ "lib"; "intvector_intrinsics"; "vec256_store64_le"],

From f55b9f0904b129b6171f734285d7f2489eab6b83 Mon Sep 17 00:00:00 2001
From: Aymeric Fromherz <aymeric.fromherz@inria.fr>
Date: Thu, 18 Jul 2024 18:08:36 +0200
Subject: [PATCH 40/52] More Lowstar.endianness builtins

---
 lib/OptimizeMiniRust.ml | 15 ++++++++++-----
 1 file changed, 10 insertions(+), 5 deletions(-)

diff --git a/lib/OptimizeMiniRust.ml b/lib/OptimizeMiniRust.ml
index 9d560264..7131d66f 100644
--- a/lib/OptimizeMiniRust.ml
+++ b/lib/OptimizeMiniRust.ml
@@ -567,15 +567,20 @@ let builtins : (name * typ list) list = [
     [Name (["lib"; "intvector_intrinsics"; "vec256"], []);
      Name (["lib"; "intvector_intrinsics"; "vec256"], [])];
 
-  (* LowStar.Endianness *)
-  [ "lowstar"; "endianness"; "load32_be" ], [Ref (None, Shared, Slice u8)];
+  (* LowStar.Endianness, little-endian *)
+  [ "lowstar"; "endianness"; "load16_le" ], [Ref (None, Shared, Slice u8)];
+  [ "lowstar"; "endianness"; "store16_le" ], [Ref (None, Mut, Slice u8); u16];
   [ "lowstar"; "endianness"; "load32_le" ], [Ref (None, Shared, Slice u8)];
+  [ "lowstar"; "endianness"; "store32_le" ], [Ref (None, Mut, Slice u8); u32];
+  [ "lowstar"; "endianness"; "load64_le" ], [Ref (None, Shared, Slice u8)];
+  [ "lowstar"; "endianness"; "store64_le" ], [Ref (None, Mut, Slice u8); u64];
+
+  (* LowStar.Endianness, big-endian *)
+  [ "lowstar"; "endianness"; "load32_be" ], [Ref (None, Shared, Slice u8)];
   [ "lowstar"; "endianness"; "store32_be" ], [Ref (None, Mut, Slice u8); Constant UInt32];
-  [ "lowstar"; "endianness"; "store32_le" ], [Ref (None, Mut, Slice u8); Constant UInt32];
   [ "lowstar"; "endianness"; "load64_be" ], [Ref (None, Shared, Slice u8)];
-  [ "lowstar"; "endianness"; "load64_le" ], [Ref (None, Shared, Slice u8)];
   [ "lowstar"; "endianness"; "store64_be" ], [Ref (None, Mut, Slice u8); Constant UInt64];
-  [ "lowstar"; "endianness"; "store64_le" ], [Ref (None, Mut, Slice u8); Constant UInt64];
+  [ "lowstar"; "endianness"; "load128_be" ], [Ref (None, Shared, Slice u8)];
   [ "lowstar"; "endianness"; "store128_be" ],
     [Ref (None, Mut, Slice u8); Name (["fstar"; "uint128"; "uint128"], [])];
 

From 70b391ea0094a7cd5b93e49ad0e93bb347e12906 Mon Sep 17 00:00:00 2001
From: Aymeric Fromherz <aymeric.fromherz@inria.fr>
Date: Thu, 18 Jul 2024 18:15:21 +0200
Subject: [PATCH 41/52] fstar uint128 builtins

---
 lib/OptimizeMiniRust.ml | 36 +++++++++++++++++++++++++++++++++---
 1 file changed, 33 insertions(+), 3 deletions(-)

diff --git a/lib/OptimizeMiniRust.ml b/lib/OptimizeMiniRust.ml
index 7131d66f..e244acf4 100644
--- a/lib/OptimizeMiniRust.ml
+++ b/lib/OptimizeMiniRust.ml
@@ -389,17 +389,44 @@ let builtins : (name * typ list) list = [
 
 
   (* FStar.UInt128 *)
-  [ "fstar"; "uint128"; "uint64_to_uint128" ], [Constant UInt64];
-  [ "fstar"; "uint128"; "uint128_to_uint64" ], [Name (["fstar"; "uint128"; "uint128"], [])];
   [ "fstar"; "uint128"; "add" ],
       [Name (["fstar"; "uint128"; "uint128"], []); Name (["fstar"; "uint128"; "uint128"], [])];
   [ "fstar"; "uint128"; "add_mod" ],
       [Name (["fstar"; "uint128"; "uint128"], []); Name (["fstar"; "uint128"; "uint128"], [])];
-  [ "fstar"; "uint128"; "mul_wide" ], [Constant UInt64; Constant UInt64];
+  [ "fstar"; "uint128"; "sub" ],
+      [Name (["fstar"; "uint128"; "uint128"], []); Name (["fstar"; "uint128"; "uint128"], [])];
+  [ "fstar"; "uint128"; "sub_mod" ],
+      [Name (["fstar"; "uint128"; "uint128"], []); Name (["fstar"; "uint128"; "uint128"], [])];
+  [ "fstar"; "uint128"; "logand" ],
+      [Name (["fstar"; "uint128"; "uint128"], []); Name (["fstar"; "uint128"; "uint128"], [])];
+  [ "fstar"; "uint128"; "logxor" ],
+      [Name (["fstar"; "uint128"; "uint128"], []); Name (["fstar"; "uint128"; "uint128"], [])];
+  [ "fstar"; "uint128"; "logor" ],
+      [Name (["fstar"; "uint128"; "uint128"], []); Name (["fstar"; "uint128"; "uint128"], [])];
+  [ "fstar"; "uint128"; "lognot" ],
+      [Name (["fstar"; "uint128"; "uint128"], [])];
   [ "fstar"; "uint128"; "shift_left" ],
       [Name (["fstar"; "uint128"; "uint128"], []); Constant UInt32];
   [ "fstar"; "uint128"; "shift_right" ],
       [Name (["fstar"; "uint128"; "uint128"], []); Constant UInt32];
+  [ "fstar"; "uint128"; "eq" ],
+      [Name (["fstar"; "uint128"; "uint128"], []); Name (["fstar"; "uint128"; "uint128"], [])];
+  [ "fstar"; "uint128"; "gt" ],
+      [Name (["fstar"; "uint128"; "uint128"], []); Name (["fstar"; "uint128"; "uint128"], [])];
+  [ "fstar"; "uint128"; "lt" ],
+      [Name (["fstar"; "uint128"; "uint128"], []); Name (["fstar"; "uint128"; "uint128"], [])];
+  [ "fstar"; "uint128"; "gte" ],
+      [Name (["fstar"; "uint128"; "uint128"], []); Name (["fstar"; "uint128"; "uint128"], [])];
+  [ "fstar"; "uint128"; "lte" ],
+      [Name (["fstar"; "uint128"; "uint128"], []); Name (["fstar"; "uint128"; "uint128"], [])];
+  [ "fstar"; "uint128"; "eq_mask" ],
+      [Name (["fstar"; "uint128"; "uint128"], []); Name (["fstar"; "uint128"; "uint128"], [])];
+  [ "fstar"; "uint128"; "gte_mask" ],
+      [Name (["fstar"; "uint128"; "uint128"], []); Name (["fstar"; "uint128"; "uint128"], [])];
+  [ "fstar"; "uint128"; "uint64_to_uint128" ], [Constant UInt64];
+  [ "fstar"; "uint128"; "uint128_to_uint64" ], [Name (["fstar"; "uint128"; "uint128"], [])];
+  [ "fstar"; "uint128"; "mul32" ], [u64; u32];
+  [ "fstar"; "uint128"; "mul_wide" ], [u64; u32];
 
   (* Lib.Inttypes_Intrinsics *)
   [ "lib"; "inttypes_intrinsics"; "add_carry_u32"], [ u32; u32; u32; Ref (None, Mut, Slice u32) ];
@@ -567,6 +594,9 @@ let builtins : (name * typ list) list = [
     [Name (["lib"; "intvector_intrinsics"; "vec256"], []);
      Name (["lib"; "intvector_intrinsics"; "vec256"], [])];
 
+  (* Lib.RandomBuffer_System *)
+  [ "lib"; "randombuffer_system"; "randombytes"], [Ref (None, Mut, Slice u8); u32]; 
+
   (* LowStar.Endianness, little-endian *)
   [ "lowstar"; "endianness"; "load16_le" ], [Ref (None, Shared, Slice u8)];
   [ "lowstar"; "endianness"; "store16_le" ], [Ref (None, Mut, Slice u8); u16];

From 44c47148bf9e869b73b78b0c3e590348d24b6a63 Mon Sep 17 00:00:00 2001
From: Aymeric Fromherz <aymeric.fromherz@inria.fr>
Date: Thu, 18 Jul 2024 18:18:01 +0200
Subject: [PATCH 42/52] Missing endianness builtin

---
 lib/OptimizeMiniRust.ml | 5 +++--
 1 file changed, 3 insertions(+), 2 deletions(-)

diff --git a/lib/OptimizeMiniRust.ml b/lib/OptimizeMiniRust.ml
index e244acf4..a5f73750 100644
--- a/lib/OptimizeMiniRust.ml
+++ b/lib/OptimizeMiniRust.ml
@@ -606,10 +606,11 @@ let builtins : (name * typ list) list = [
   [ "lowstar"; "endianness"; "store64_le" ], [Ref (None, Mut, Slice u8); u64];
 
   (* LowStar.Endianness, big-endian *)
+  [ "lowstar"; "endianness"; "store16_be" ], [Ref (None, Mut, Slice u8); u16];
   [ "lowstar"; "endianness"; "load32_be" ], [Ref (None, Shared, Slice u8)];
-  [ "lowstar"; "endianness"; "store32_be" ], [Ref (None, Mut, Slice u8); Constant UInt32];
+  [ "lowstar"; "endianness"; "store32_be" ], [Ref (None, Mut, Slice u8); u32];
   [ "lowstar"; "endianness"; "load64_be" ], [Ref (None, Shared, Slice u8)];
-  [ "lowstar"; "endianness"; "store64_be" ], [Ref (None, Mut, Slice u8); Constant UInt64];
+  [ "lowstar"; "endianness"; "store64_be" ], [Ref (None, Mut, Slice u8); u64];
   [ "lowstar"; "endianness"; "load128_be" ], [Ref (None, Shared, Slice u8)];
   [ "lowstar"; "endianness"; "store128_be" ],
     [Ref (None, Mut, Slice u8); Name (["fstar"; "uint128"; "uint128"], [])];

From 2ebd49d607026c0a9d03bad85210f1573aba9f7b Mon Sep 17 00:00:00 2001
From: Aymeric Fromherz <aymeric.fromherz@inria.fr>
Date: Thu, 18 Jul 2024 18:32:53 +0200
Subject: [PATCH 43/52] complex assignment

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

diff --git a/lib/OptimizeMiniRust.ml b/lib/OptimizeMiniRust.ml
index a5f73750..b3b78be7 100644
--- a/lib/OptimizeMiniRust.ml
+++ b/lib/OptimizeMiniRust.ml
@@ -185,19 +185,24 @@ let rec infer (env: env) (expected: typ) (known: known) (e: expr): known * expr
   | Call _ ->
       failwith "TODO: Call"
 
+  (* atom = e3 *)
   | Assign (Open { atom; _ }, e3, t) ->
       (* KPrint.bprintf "[infer-mut,assign] %a\n" PrintMiniRust.pexpr e; *)
       let known, e3 = infer env t known e3 in
       add_mut_var atom known, e3
 
+  (* atom[e2] = e2 *)
   | Assign (Index (Open { atom; _ } as e1, e2), e3, t) 
+
   (* Special-case when we perform a field assignment that comes from
      a slice. This is the only case where we use native Rust tuples.
      In this case, we mark the atom as mutable, and will replace
      the corresponding call to split by split_at_mut when we reach
       let-binding.
    *)
+  (* atom.0[e2] = e3 *)
   | Assign (Index (Field (Open {atom;_}, "0", None) as e1, e2), e3, t)
+  (* atom.1[e2] = e3 *)
   | Assign (Index (Field (Open {atom;_}, "1", None) as e1, e2), e3, t) ->
       (* KPrint.bprintf "[infer-mut,assign] %a\n" PrintMiniRust.pexpr e; *)
       let known = add_mut_borrow atom known in
@@ -205,12 +210,14 @@ let rec infer (env: env) (expected: typ) (known: known) (e: expr): known * expr
       let known, e3 = infer env t known e3 in
       known, Assign (Index (e1, e2), e3, t)
 
+  (* x.f[e2] = e3 *)
   | Assign (Index (Field (_, f, st) as e1, e2), e3, t) ->
       let known = add_mut_field st f known in
       let known, e2 = infer env usize known e2 in
       let known, e3 = infer env t known e3 in
       known, Assign (Index (e1, e2), e3, t)
 
+  (* (&atom)[e2] = e3 *)
   | Assign (Index (Borrow (_, (Open { atom; _ } as e1)), e2), e3, t) ->
       (* KPrint.bprintf "[infer-mut,assign] %a\n" PrintMiniRust.pexpr e; *)
       let known = add_mut_var atom known in
@@ -222,18 +229,28 @@ let rec infer (env: env) (expected: typ) (known: known) (e: expr): known * expr
   | Assign (Field (_, "1", None), _, _) ->
       failwith "TODO: assignment on slice"
 
+  (* (atom.f)[e2] = e3 *)
   | Assign (Field (Index ((Open {atom; _} as e1), e2), f, st), e3, t) ->
       let known = add_mut_borrow atom known in
       let known, e2 = infer env usize known e2 in
       let known, e3 = infer env t known e3 in
       known, Assign (Field (Index (e1, e2), f, st), e3, t)
 
+  (* (&n)[e2] = e3 *)
   | Assign (Index (Borrow (_, Name n), e2), e3, t) ->
       (* This case should only occur for globals. For now, we simply mutably borrow it *)
       let known, e2 = infer env usize known e2 in
       let known, e3 = infer env t known e3 in
       known, Assign (Index (Borrow (Mut, Name n), e2), e3, t)
 
+  (* (&(&atom)[e2])[e3] = e4 *)
+  | Assign (Index (Borrow (_, Index (Borrow (_, (Open {atom; _} as e1)), e2)), e3), e4, t) ->
+      let known = add_mut_var atom known in
+      let known, e2 = infer env usize known e2 in
+      let known, e3 = infer env usize known e3 in
+      let known, e4 = infer env t known e4 in
+      known, Assign (Index (Borrow (Mut, Index (Borrow (Mut, e1), e2)), e3), e4, t)
+
   | Assign _ ->
       KPrint.bprintf "[infer-mut,assign] %a unsupported\n" PrintMiniRust.pexpr e;
       failwith "TODO: unknown assignment"

From 9b3f2782b970bab0117166ec1bd8200b767115e2 Mon Sep 17 00:00:00 2001
From: Aymeric Fromherz <aymeric.fromherz@inria.fr>
Date: Thu, 18 Jul 2024 18:35:59 +0200
Subject: [PATCH 44/52] more builtins, replace Constant by abbreviations

---
 lib/OptimizeMiniRust.ml | 48 +++++++++++++++++++++--------------------
 1 file changed, 25 insertions(+), 23 deletions(-)

diff --git a/lib/OptimizeMiniRust.ml b/lib/OptimizeMiniRust.ml
index b3b78be7..9613a0ab 100644
--- a/lib/OptimizeMiniRust.ml
+++ b/lib/OptimizeMiniRust.ml
@@ -163,7 +163,7 @@ let rec infer (env: env) (expected: typ) (known: known) (e: expr): known * expr
         assert (List.length es = 2);
         let e1, e2 = KList.two es in
         let known, e1 = infer env (Ref (None, Mut, Slice (KList.one targs))) known e1 in
-        let known, e2 = infer env (Constant UInt32) known e2 in
+        let known, e2 = infer env u32 known e2 in
         known, Call (Name n, targs, [ e1; e2 ])
       ) else (
         KPrint.bprintf "[infer-mut,call] recursing on %s\n" (String.concat " :: " n);
@@ -423,9 +423,9 @@ let builtins : (name * typ list) list = [
   [ "fstar"; "uint128"; "lognot" ],
       [Name (["fstar"; "uint128"; "uint128"], [])];
   [ "fstar"; "uint128"; "shift_left" ],
-      [Name (["fstar"; "uint128"; "uint128"], []); Constant UInt32];
+      [Name (["fstar"; "uint128"; "uint128"], []); u32];
   [ "fstar"; "uint128"; "shift_right" ],
-      [Name (["fstar"; "uint128"; "uint128"], []); Constant UInt32];
+      [Name (["fstar"; "uint128"; "uint128"], []); u32];
   [ "fstar"; "uint128"; "eq" ],
       [Name (["fstar"; "uint128"; "uint128"], []); Name (["fstar"; "uint128"; "uint128"], [])];
   [ "fstar"; "uint128"; "gt" ],
@@ -440,7 +440,7 @@ let builtins : (name * typ list) list = [
       [Name (["fstar"; "uint128"; "uint128"], []); Name (["fstar"; "uint128"; "uint128"], [])];
   [ "fstar"; "uint128"; "gte_mask" ],
       [Name (["fstar"; "uint128"; "uint128"], []); Name (["fstar"; "uint128"; "uint128"], [])];
-  [ "fstar"; "uint128"; "uint64_to_uint128" ], [Constant UInt64];
+  [ "fstar"; "uint128"; "uint64_to_uint128" ], [u64];
   [ "fstar"; "uint128"; "uint128_to_uint64" ], [Name (["fstar"; "uint128"; "uint128"], [])];
   [ "fstar"; "uint128"; "mul32" ], [u64; u32];
   [ "fstar"; "uint128"; "mul_wide" ], [u64; u32];
@@ -466,7 +466,7 @@ let builtins : (name * typ list) list = [
     [Name (["lib"; "intvector_intrinsics"; "vec128"], []);
      Name (["lib"; "intvector_intrinsics"; "vec128"], [])];
   [ "lib"; "intvector_intrinsics"; "vec128_extract64"],
-    [Name (["lib"; "intvector_intrinsics"; "vec128"], []); Constant UInt32];
+    [Name (["lib"; "intvector_intrinsics"; "vec128"], []); u32];
   [ "lib"; "intvector_intrinsics"; "vec128_gt64"],
     [Name (["lib"; "intvector_intrinsics"; "vec128"], []);
      Name (["lib"; "intvector_intrinsics"; "vec128"], [])];
@@ -484,9 +484,8 @@ let builtins : (name * typ list) list = [
   [ "lib"; "intvector_intrinsics"; "vec128_interleave_high64"],
     [Name (["lib"; "intvector_intrinsics"; "vec128"], []);
      Name (["lib"; "intvector_intrinsics"; "vec128"], [])];
-  [ "lib"; "intvector_intrinsics"; "vec128_load32"], [Constant UInt32];
-  [ "lib"; "intvector_intrinsics"; "vec128_load32s"],
-    [ Constant UInt32; Constant UInt32; Constant UInt32; Constant UInt32];
+  [ "lib"; "intvector_intrinsics"; "vec128_load32"], [u32];
+  [ "lib"; "intvector_intrinsics"; "vec128_load32s"], [u32; u32; u32; u32];
   [ "lib"; "intvector_intrinsics"; "vec128_load32_be"], [Ref (None, Shared, Slice u8)];
   [ "lib"; "intvector_intrinsics"; "vec128_load32_le"], [Ref (None, Shared, Slice u8)];
   [ "lib"; "intvector_intrinsics"; "vec128_load64"], [u64];
@@ -503,15 +502,17 @@ let builtins : (name * typ list) list = [
     [Name (["lib"; "intvector_intrinsics"; "vec128"], []);
      Name (["lib"; "intvector_intrinsics"; "vec128"], [])];
   [ "lib"; "intvector_intrinsics"; "vec128_rotate_left32"],
-    [Name (["lib"; "intvector_intrinsics"; "vec128"], []); Constant UInt32];
+    [Name (["lib"; "intvector_intrinsics"; "vec128"], []); u32];
   [ "lib"; "intvector_intrinsics"; "vec128_rotate_right32"],
-    [Name (["lib"; "intvector_intrinsics"; "vec128"], []); Constant UInt32];
+    [Name (["lib"; "intvector_intrinsics"; "vec128"], []); u32];
   [ "lib"; "intvector_intrinsics"; "vec128_rotate_right_lanes32"],
-    [Name (["lib"; "intvector_intrinsics"; "vec128"], []); Constant UInt32];
+    [Name (["lib"; "intvector_intrinsics"; "vec128"], []); u32];
   [ "lib"; "intvector_intrinsics"; "vec128_shift_left64"],
-    [Name (["lib"; "intvector_intrinsics"; "vec128"], []); Constant UInt32];
+    [Name (["lib"; "intvector_intrinsics"; "vec128"], []); u32];
+  [ "lib"; "intvector_intrinsics"; "vec128_shift_right32"],
+    [Name (["lib"; "intvector_intrinsics"; "vec128"], []); u32];
   [ "lib"; "intvector_intrinsics"; "vec128_shift_right64"],
-    [Name (["lib"; "intvector_intrinsics"; "vec128"], []); Constant UInt32];
+    [Name (["lib"; "intvector_intrinsics"; "vec128"], []); u32];
   [ "lib"; "intvector_intrinsics"; "vec128_smul64"],
     [Name (["lib"; "intvector_intrinsics"; "vec128"], []); u64];
   [ "lib"; "intvector_intrinsics"; "vec128_store32_be"],
@@ -567,9 +568,8 @@ let builtins : (name * typ list) list = [
   [ "lib"; "intvector_intrinsics"; "vec256_load32s"], [u32; u32; u32; u32; u32; u32; u32; u32]; 
   [ "lib"; "intvector_intrinsics"; "vec256_load32_be"], [Ref (None, Shared, Slice u8)];
   [ "lib"; "intvector_intrinsics"; "vec256_load32_le"], [Ref (None, Shared, Slice u8)];
-  [ "lib"; "intvector_intrinsics"; "vec256_load64"], [Constant UInt64];
-  [ "lib"; "intvector_intrinsics"; "vec256_load64s"],
-    [ Constant UInt64; Constant UInt64; Constant UInt64; Constant UInt64];
+  [ "lib"; "intvector_intrinsics"; "vec256_load64"], [u64];
+  [ "lib"; "intvector_intrinsics"; "vec256_load64s"], [u64; u64; u64; u64];
   [ "lib"; "intvector_intrinsics"; "vec256_load64_be"], [Ref (None, Shared, Slice u8)];
   [ "lib"; "intvector_intrinsics"; "vec256_load64_le"], [Ref (None, Shared, Slice u8)];
   [ "lib"; "intvector_intrinsics"; "vec256_lognot"],
@@ -581,19 +581,21 @@ let builtins : (name * typ list) list = [
     [Name (["lib"; "intvector_intrinsics"; "vec256"], []);
      Name (["lib"; "intvector_intrinsics"; "vec256"], [])];
   [ "lib"; "intvector_intrinsics"; "vec256_rotate_left32"],
-    [Name (["lib"; "intvector_intrinsics"; "vec256"], []); Constant UInt32];
+    [Name (["lib"; "intvector_intrinsics"; "vec256"], []); u32];
   [ "lib"; "intvector_intrinsics"; "vec256_rotate_right32"],
-    [Name (["lib"; "intvector_intrinsics"; "vec256"], []); Constant UInt32];
+    [Name (["lib"; "intvector_intrinsics"; "vec256"], []); u32];
   [ "lib"; "intvector_intrinsics"; "vec256_rotate_right64"],
-    [Name (["lib"; "intvector_intrinsics"; "vec256"], []); Constant UInt32];
+    [Name (["lib"; "intvector_intrinsics"; "vec256"], []); u32];
   [ "lib"; "intvector_intrinsics"; "vec256_rotate_right_lanes64"],
-    [Name (["lib"; "intvector_intrinsics"; "vec256"], []); Constant UInt32];
+    [Name (["lib"; "intvector_intrinsics"; "vec256"], []); u32];
   [ "lib"; "intvector_intrinsics"; "vec256_shift_left64"],
-    [Name (["lib"; "intvector_intrinsics"; "vec256"], []); Constant UInt32];
+    [Name (["lib"; "intvector_intrinsics"; "vec256"], []); u32];
   [ "lib"; "intvector_intrinsics"; "vec256_shift_right"],
-    [Name (["lib"; "intvector_intrinsics"; "vec256"], []); Constant UInt32];
+    [Name (["lib"; "intvector_intrinsics"; "vec256"], []); u32];
+  [ "lib"; "intvector_intrinsics"; "vec256_shift_right32"],
+    [Name (["lib"; "intvector_intrinsics"; "vec256"], []); u32];
   [ "lib"; "intvector_intrinsics"; "vec256_shift_right64"],
-    [Name (["lib"; "intvector_intrinsics"; "vec256"], []); Constant UInt32];
+    [Name (["lib"; "intvector_intrinsics"; "vec256"], []); u32];
   [ "lib"; "intvector_intrinsics"; "vec256_smul64"],
     [Name (["lib"; "intvector_intrinsics"; "vec256"], []); u64];
   [ "lib"; "intvector_intrinsics"; "vec256_store32_be"],

From 6940038b3450578248eb3c299afbad645bbcb7a4 Mon Sep 17 00:00:00 2001
From: Aymeric Fromherz <aymeric.fromherz@inria.fr>
Date: Thu, 18 Jul 2024 18:40:21 +0200
Subject: [PATCH 45/52] Fix handling of push

---
 lib/OptimizeMiniRust.ml | 6 ++++--
 1 file changed, 4 insertions(+), 2 deletions(-)

diff --git a/lib/OptimizeMiniRust.ml b/lib/OptimizeMiniRust.ml
index 9613a0ab..63d7eb31 100644
--- a/lib/OptimizeMiniRust.ml
+++ b/lib/OptimizeMiniRust.ml
@@ -324,8 +324,10 @@ let rec infer (env: env) (expected: typ) (known: known) (e: expr): known * expr
               as the left argument of copy_from_slice *)
           | _ -> failwith "ill-formed copy_from_slice"
           end
-      | [ "push" ] ->
-          known, MethodCall (e1, m, e2)
+      | [ "push" ] -> begin match e1 with
+          | Open {atom; _} -> add_mut_var atom known, MethodCall (e1, m, e2)
+          | _ -> failwith "TODO: push on complex expressions"
+          end
       | _ ->
           KPrint.bprintf "%a unsupported\n" PrintMiniRust.pexpr e;
           failwith "TODO: MethodCall"

From f216ff60d8ac7755f01eecebe2aec96d6630e60d Mon Sep 17 00:00:00 2001
From: Aymeric Fromherz <aymeric.fromherz@inria.fr>
Date: Thu, 18 Jul 2024 18:52:53 +0200
Subject: [PATCH 46/52] Correct unroll_for transformation

---
 lib/RustMacroize.ml | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

diff --git a/lib/RustMacroize.ml b/lib/RustMacroize.ml
index bb8e86d4..30263c6b 100644
--- a/lib/RustMacroize.ml
+++ b/lib/RustMacroize.ml
@@ -11,7 +11,7 @@ let unroll_loops = object
     let e2 = super#visit_expr () e2 in 
 
     match e1 with
-    | Range (Some (Constant (UInt32, init as k_init) as e_init), Some (Constant (UInt32, max as k_max)), false)
+    | Range (Some (Constant (UInt32, init as k_init) as e_init), Some (Constant (UInt32, max)), false)
       when (
         let init = int_of_string init in
         let max = int_of_string max in
@@ -30,7 +30,7 @@ let unroll_loops = object
           Constant (CInt, string_of_int n_loops);
           ConstantString b.name;
           Constant k_init;
-          Constant k_max;
+          Constant (UInt32, "1");
           e2
         ])
 

From 64f3c9e7f563ecfa0ea139dda8e94c1aaa83d48f Mon Sep 17 00:00:00 2001
From: Aymeric Fromherz <aymeric.fromherz@inria.fr>
Date: Fri, 19 Jul 2024 16:06:09 +0200
Subject: [PATCH 47/52] attempt to fix CI

---
 test/Rust4.fst | 1 +
 test/Rust5.fst | 1 +
 test/Rust6.fst | 1 +
 test/Rust7.fst | 1 +
 4 files changed, 4 insertions(+)

diff --git a/test/Rust4.fst b/test/Rust4.fst
index 6e65a448..8d047dda 100644
--- a/test/Rust4.fst
+++ b/test/Rust4.fst
@@ -2,6 +2,7 @@ module Rust4
 
 let f (): HyperStack.ST.St UInt32.t = 1ul
 
+
 let main_ () =
   if not (f () = 0ul) then
     0l
diff --git a/test/Rust5.fst b/test/Rust5.fst
index e3f85643..3f02573c 100644
--- a/test/Rust5.fst
+++ b/test/Rust5.fst
@@ -6,6 +6,7 @@ module B = LowStar.Buffer
 
 let ignore #a (x: a): Stack unit (fun h0 -> True) (fun h0 r h1 -> h0 == h1) = ()
 
+
 let main_ (): St Int32.t =
   push_frame ();
   let base = B.alloca 0l 2ul in
diff --git a/test/Rust6.fst b/test/Rust6.fst
index 81815bc7..d09cea3c 100644
--- a/test/Rust6.fst
+++ b/test/Rust6.fst
@@ -6,6 +6,7 @@ module B = LowStar.Buffer
 module C = LowStar.ConstBuffer
 module HS = FStar.HyperStack
 
+
 inline_for_extraction noextract
 val sub_len:
   b: C.const_buffer UInt32.t ->
diff --git a/test/Rust7.fst b/test/Rust7.fst
index 707d6772..dd3a84d4 100644
--- a/test/Rust7.fst
+++ b/test/Rust7.fst
@@ -7,6 +7,7 @@ open LowStar.BufferOps
 open FStar
 open FStar.HyperStack.ST
 
+
 val add_carry_u32:
   x:U32.t
   -> y:U32.t

From 08811beaf860c02d5764fefd4cdd31cb03fd7d1c Mon Sep 17 00:00:00 2001
From: Aymeric Fromherz <aymeric.fromherz@inria.fr>
Date: Fri, 19 Jul 2024 16:10:20 +0200
Subject: [PATCH 48/52] lowercase rust test files

---
 test/Makefile                 | 6 +++---
 test/{Rust1.fst => rust1.fst} | 0
 test/{Rust2.fst => rust2.fst} | 0
 test/{Rust3.fst => rust3.fst} | 0
 test/{Rust4.fst => rust4.fst} | 0
 test/{Rust5.fst => rust5.fst} | 0
 test/{Rust6.fst => rust6.fst} | 0
 test/{Rust7.fst => rust7.fst} | 0
 8 files changed, 3 insertions(+), 3 deletions(-)
 rename test/{Rust1.fst => rust1.fst} (100%)
 rename test/{Rust2.fst => rust2.fst} (100%)
 rename test/{Rust3.fst => rust3.fst} (100%)
 rename test/{Rust4.fst => rust4.fst} (100%)
 rename test/{Rust5.fst => rust5.fst} (100%)
 rename test/{Rust6.fst => rust6.fst} (100%)
 rename test/{Rust7.fst => rust7.fst} (100%)

diff --git a/test/Makefile b/test/Makefile
index d92247c3..4b5eed75 100644
--- a/test/Makefile
+++ b/test/Makefile
@@ -39,7 +39,7 @@ BROKEN		= \
   HigherOrder6.fst ForwardDecl.fst BlitNull.fst \
   Ctypes1.fst Ctypes2.fst Ctypes3.fst Ctypes4.fst \
   AbstractStructAbstract.fst MonomorphizationSeparate1.fst \
-  Layered.fst GlobalInit2.fst $(wildcard Rust*.fst)
+  Layered.fst GlobalInit2.fst $(wildcard rust*.fst)
 
 # Lowlevel is not really broken, but its test shouldn't be run since it's a
 # special file and doesn't have a main.
@@ -306,6 +306,6 @@ WasmTrap.wasm-test: NEGATIVE = true
 %.rust-test: $(OUTPUT_DIR)/%.rs
 	rustc $< && ./$*
 
-rust: $(RUST_FILES) $(patsubst %.fst,%.rust-test,$(filter-out Rust1.fst Rust2.fst Rust3.fst,$(wildcard Rust*.fst)))
+rust: $(RUST_FILES) $(patsubst %.fst,%.rust-test,$(filter-out rust1.fst rust2.fst rust3.fst,$(wildcard rust*.fst)))
 
-RUST_FILES = $(patsubst %.rs,%.rust-test,$(wildcard Rust*.fst))
+RUST_FILES = $(patsubst %.rs,%.rust-test,$(wildcard rust*.fst))
diff --git a/test/Rust1.fst b/test/rust1.fst
similarity index 100%
rename from test/Rust1.fst
rename to test/rust1.fst
diff --git a/test/Rust2.fst b/test/rust2.fst
similarity index 100%
rename from test/Rust2.fst
rename to test/rust2.fst
diff --git a/test/Rust3.fst b/test/rust3.fst
similarity index 100%
rename from test/Rust3.fst
rename to test/rust3.fst
diff --git a/test/Rust4.fst b/test/rust4.fst
similarity index 100%
rename from test/Rust4.fst
rename to test/rust4.fst
diff --git a/test/Rust5.fst b/test/rust5.fst
similarity index 100%
rename from test/Rust5.fst
rename to test/rust5.fst
diff --git a/test/Rust6.fst b/test/rust6.fst
similarity index 100%
rename from test/Rust6.fst
rename to test/rust6.fst
diff --git a/test/Rust7.fst b/test/rust7.fst
similarity index 100%
rename from test/Rust7.fst
rename to test/rust7.fst

From 155f485faa375a2d1df16b8094bf1a0eda320179 Mon Sep 17 00:00:00 2001
From: Aymeric Fromherz <aymeric.fromherz@inria.fr>
Date: Fri, 19 Jul 2024 16:22:03 +0200
Subject: [PATCH 49/52] Revert "lowercase rust test files"

This reverts commit 08811beaf860c02d5764fefd4cdd31cb03fd7d1c.
---
 test/Makefile                 | 6 +++---
 test/{rust1.fst => Rust1.fst} | 0
 test/{rust2.fst => Rust2.fst} | 0
 test/{rust3.fst => Rust3.fst} | 0
 test/{rust4.fst => Rust4.fst} | 0
 test/{rust5.fst => Rust5.fst} | 0
 test/{rust6.fst => Rust6.fst} | 0
 test/{rust7.fst => Rust7.fst} | 0
 8 files changed, 3 insertions(+), 3 deletions(-)
 rename test/{rust1.fst => Rust1.fst} (100%)
 rename test/{rust2.fst => Rust2.fst} (100%)
 rename test/{rust3.fst => Rust3.fst} (100%)
 rename test/{rust4.fst => Rust4.fst} (100%)
 rename test/{rust5.fst => Rust5.fst} (100%)
 rename test/{rust6.fst => Rust6.fst} (100%)
 rename test/{rust7.fst => Rust7.fst} (100%)

diff --git a/test/Makefile b/test/Makefile
index 4b5eed75..d92247c3 100644
--- a/test/Makefile
+++ b/test/Makefile
@@ -39,7 +39,7 @@ BROKEN		= \
   HigherOrder6.fst ForwardDecl.fst BlitNull.fst \
   Ctypes1.fst Ctypes2.fst Ctypes3.fst Ctypes4.fst \
   AbstractStructAbstract.fst MonomorphizationSeparate1.fst \
-  Layered.fst GlobalInit2.fst $(wildcard rust*.fst)
+  Layered.fst GlobalInit2.fst $(wildcard Rust*.fst)
 
 # Lowlevel is not really broken, but its test shouldn't be run since it's a
 # special file and doesn't have a main.
@@ -306,6 +306,6 @@ WasmTrap.wasm-test: NEGATIVE = true
 %.rust-test: $(OUTPUT_DIR)/%.rs
 	rustc $< && ./$*
 
-rust: $(RUST_FILES) $(patsubst %.fst,%.rust-test,$(filter-out rust1.fst rust2.fst rust3.fst,$(wildcard rust*.fst)))
+rust: $(RUST_FILES) $(patsubst %.fst,%.rust-test,$(filter-out Rust1.fst Rust2.fst Rust3.fst,$(wildcard Rust*.fst)))
 
-RUST_FILES = $(patsubst %.rs,%.rust-test,$(wildcard rust*.fst))
+RUST_FILES = $(patsubst %.rs,%.rust-test,$(wildcard Rust*.fst))
diff --git a/test/rust1.fst b/test/Rust1.fst
similarity index 100%
rename from test/rust1.fst
rename to test/Rust1.fst
diff --git a/test/rust2.fst b/test/Rust2.fst
similarity index 100%
rename from test/rust2.fst
rename to test/Rust2.fst
diff --git a/test/rust3.fst b/test/Rust3.fst
similarity index 100%
rename from test/rust3.fst
rename to test/Rust3.fst
diff --git a/test/rust4.fst b/test/Rust4.fst
similarity index 100%
rename from test/rust4.fst
rename to test/Rust4.fst
diff --git a/test/rust5.fst b/test/Rust5.fst
similarity index 100%
rename from test/rust5.fst
rename to test/Rust5.fst
diff --git a/test/rust6.fst b/test/Rust6.fst
similarity index 100%
rename from test/rust6.fst
rename to test/Rust6.fst
diff --git a/test/rust7.fst b/test/Rust7.fst
similarity index 100%
rename from test/rust7.fst
rename to test/Rust7.fst

From 2913c8a8e6af3b410bdda1ae5cb0cdf9a145cc64 Mon Sep 17 00:00:00 2001
From: Aymeric Fromherz <aymeric.fromherz@inria.fr>
Date: Fri, 19 Jul 2024 16:33:06 +0200
Subject: [PATCH 50/52] Attempt another Rust test Makefile fix

---
 test/Makefile | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/test/Makefile b/test/Makefile
index d92247c3..6d73f095 100644
--- a/test/Makefile
+++ b/test/Makefile
@@ -306,6 +306,6 @@ WasmTrap.wasm-test: NEGATIVE = true
 %.rust-test: $(OUTPUT_DIR)/%.rs
 	rustc $< && ./$*
 
-rust: $(RUST_FILES) $(patsubst %.fst,%.rust-test,$(filter-out Rust1.fst Rust2.fst Rust3.fst,$(wildcard Rust*.fst)))
+rust: $(RUST_FILES) $(patsubst Rust%.fst,Rust%.rust-test,$(filter-out Rust1.fst Rust2.fst Rust3.fst,$(wildcard Rust*.fst)))
 
 RUST_FILES = $(patsubst %.rs,%.rust-test,$(wildcard Rust*.fst))

From bec3963fbb50314548056af644be4226c1d33093 Mon Sep 17 00:00:00 2001
From: Aymeric Fromherz <aymeric.fromherz@inria.fr>
Date: Fri, 19 Jul 2024 16:49:31 +0200
Subject: [PATCH 51/52] More attempts to workaround case-sensitivity on CI
 machine

---
 test/Makefile | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

diff --git a/test/Makefile b/test/Makefile
index 6d73f095..30b48487 100644
--- a/test/Makefile
+++ b/test/Makefile
@@ -298,7 +298,7 @@ WasmTrap.wasm-test: NEGATIVE = true
 
 .PRECIOUS: %.rs
 %.rs: $(ALL_KRML_FILES) $(KRML_BIN)
-	$(KRML) -minimal -bundle $(notdir $*)=\* \
+	$(KRML) -minimal -bundle $(notdir $(subst rust,Rust,$*))=\* \
 	  -backend rust $(EXTRA) -tmpdir $(dir $@) $(filter %.krml,$^)
 	$(SED) -i 's/\(mutation..\)/\1\nmod lowstar { pub mod ignore { pub fn ignore<T>(_x: T) {}}}\n/' $@
 	echo 'fn main () { let r = main_ (); if r != 0 { println!("main_ returned: {}\\n", r); panic!() } }' >> $@
@@ -306,6 +306,6 @@ WasmTrap.wasm-test: NEGATIVE = true
 %.rust-test: $(OUTPUT_DIR)/%.rs
 	rustc $< && ./$*
 
-rust: $(RUST_FILES) $(patsubst Rust%.fst,Rust%.rust-test,$(filter-out Rust1.fst Rust2.fst Rust3.fst,$(wildcard Rust*.fst)))
+rust: $(RUST_FILES) $(patsubst Rust%.fst,rust%.rust-test,$(filter-out Rust1.fst Rust2.fst Rust3.fst,$(wildcard Rust*.fst)))
 
 RUST_FILES = $(patsubst %.rs,%.rust-test,$(wildcard Rust*.fst))

From 4514866a61d843e30a87c46a3b51bbb6283b2d13 Mon Sep 17 00:00:00 2001
From: Aymeric Fromherz <aymeric.fromherz@inria.fr>
Date: Fri, 19 Jul 2024 17:11:19 +0200
Subject: [PATCH 52/52] Improve several patterns for mutable borrowing

---
 lib/OptimizeMiniRust.ml | 11 ++++++++---
 1 file changed, 8 insertions(+), 3 deletions(-)

diff --git a/lib/OptimizeMiniRust.ml b/lib/OptimizeMiniRust.ml
index 63d7eb31..494d77e3 100644
--- a/lib/OptimizeMiniRust.ml
+++ b/lib/OptimizeMiniRust.ml
@@ -107,9 +107,14 @@ let rec infer (env: env) (expected: typ) (known: known) (e: expr): known * expr
         | Field (Open _, "0", None)
         | Field (Open _, "1", None) -> failwith "TODO: borrowing slices"
 
-        | Field (_, f, t) ->
-            let known = add_mut_field t f known in
-            known, Borrow (Mut, e)
+        | Field (Open {atom; _}, _, _) ->
+            add_mut_var atom known, Borrow (Mut, e)
+
+        | Field (Deref (Open {atom; _}), _, _) ->
+            add_mut_borrow atom known, Borrow (Mut, e)
+
+        | Field (Index (Open {atom; _}, _), _, _) ->
+            add_mut_borrow atom known, Borrow (Mut, e)
 
         | _ ->
             KPrint.bprintf "[infer-mut, borrow] borrwing %a is not supported\n" PrintMiniRust.pexpr e;