From ac248beb1ad2ce575703459b698565e4843fdd24 Mon Sep 17 00:00:00 2001
From: bit-aloo <sshourya17@gmail.com>
Date: Thu, 27 Aug 2026 05:04:24 +0530
Subject: [PATCH 1/7] Add mutability to let statements

---
 crates/formality-rust/src/grammar/expr/mod.rs | 11 ++++++-
 crates/formality-rust/src/test.rs             | 33 ++++++++++++++++++-
 crates/formality-rust/src/to_rust/expr.rs     | 15 +++++----
 3 files changed, 50 insertions(+), 9 deletions(-)

diff --git a/crates/formality-rust/src/grammar/expr/mod.rs b/crates/formality-rust/src/grammar/expr/mod.rs
index aee375aba..32d55dfba 100644
--- a/crates/formality-rust/src/grammar/expr/mod.rs
+++ b/crates/formality-rust/src/grammar/expr/mod.rs
@@ -8,6 +8,14 @@ use crate::grammar::{
 
 mod parse_expr;
 
+#[term]
+pub enum Mutability {
+    #[grammar(mut)]
+    Mut,
+    #[grammar()]
+    Not,
+}
+
 id!(LabelId, regex = "'[a-zA-Z_][a-zA-Z0-9_]*");
 
 #[term($id :)]
@@ -73,8 +81,9 @@ pub enum Stmt {
     /// in the named block and dropped when that block exits.
     /// If no initializer is given, the variable is uninitialized
     /// and must be assigned before use.
-    #[grammar(let $?label $id : $ty $?init ;)]
+    #[grammar(let $mutability $?label $id : $ty $?init ;)]
     Let {
+        mutability: Mutability,
         label: Option<Label>,
         id: ValueId,
         ty: Ty,
diff --git a/crates/formality-rust/src/test.rs b/crates/formality-rust/src/test.rs
index 89306b957..21ff7761f 100644
--- a/crates/formality-rust/src/test.rs
+++ b/crates/formality-rust/src/test.rs
@@ -3,7 +3,7 @@
 use crate::rust::{term, try_term};
 use formality_macros::test;
 
-use crate::grammar::expr::{Expr, Literal, PlaceExpr};
+use crate::grammar::expr::{Expr, Literal, PlaceExpr, Stmt};
 use crate::grammar::{Crates, Fallible, ScalarId};
 
 #[test]
@@ -302,3 +302,34 @@ fn test_parse_literals() {
     let expr_data: Expr = try_term("true").unwrap();
     assert!(matches!(expr_data, Expr::True));
 }
+
+#[test]
+fn test_let_statement_mutability() {
+    let p: Stmt = term("let mut b: u32;");
+    expect_test::expect![[r#"
+        Let {
+            mutability: Mut,
+            label: None,
+            id: b,
+            ty: RigidTy(
+                u32,
+            ),
+            init: None,
+        }
+    "#]]
+    .assert_debug_eq(&p);
+
+    let p: Stmt = term("let b: u32;");
+    expect_test::expect![[r#"
+        Let {
+            mutability: Not,
+            label: None,
+            id: b,
+            ty: RigidTy(
+                u32,
+            ),
+            init: None,
+        }
+    "#]]
+    .assert_debug_eq(&p);
+}
diff --git a/crates/formality-rust/src/to_rust/expr.rs b/crates/formality-rust/src/to_rust/expr.rs
index 6814eefb9..a1a103712 100644
--- a/crates/formality-rust/src/to_rust/expr.rs
+++ b/crates/formality-rust/src/to_rust/expr.rs
@@ -2,7 +2,7 @@ use std::ops::Deref;
 
 use crate::{
     grammar::{
-        expr::{Block, Expr, FieldExpr, Init, Label, Literal, PlaceExpr, Stmt},
+        expr::{Block, Expr, FieldExpr, Init, Label, Literal, Mutability, PlaceExpr, Stmt},
         Binder, Fallible, FieldName, Lt, Parameter, RefKind, Ty, ValueId, Variable,
     },
     to_rust::context::Wrapped,
@@ -23,11 +23,12 @@ pub fn lower_block(ctx: &mut Context, block: &Block) -> Fallible<syntax::Block>
 pub fn lower_stmt(ctx: &mut Context, stmt: &Stmt) -> Fallible<syntax::Stmt> {
     match stmt {
         Stmt::Let {
+            mutability,
             label,
             id,
             ty,
             init,
-        } => lower_let(ctx, label.as_ref(), id, ty, init.as_ref()),
+        } => lower_let(ctx, mutability, label.as_ref(), id, ty, init.as_ref()),
         Stmt::If {
             condition,
             then_block,
@@ -59,14 +60,14 @@ pub fn lower_stmt(ctx: &mut Context, stmt: &Stmt) -> Fallible<syntax::Stmt> {
 
 pub fn lower_let(
     ctx: &mut Context,
+    mutable: &Mutability,
     _label: Option<&Label>,
     id: &ValueId,
     ty: &Ty,
     init: Option<&Init>,
 ) -> Fallible<syntax::Stmt> {
     Ok(syntax::Stmt::Let {
-        // TODO: is there a way to know, if the variable must be mutable or not?
-        mutable: true,
+        mutable: matches!(mutable, Mutability::Mut),
         name: id.deref().clone(),
         ty: tys::lower_ty(ctx, ty)?,
         init: init.map(|init| lower_expr(ctx, &init.expr)).transpose()?,
@@ -213,7 +214,7 @@ mod test {
             ],
             expect_test::expect![[r#"
 pub fn foo() -> u32 {
-    let mut x: u32;
+    let x: u32;
     return x;
 }"#
                                   ]]
@@ -259,8 +260,8 @@ pub fn foo() -> () {
             expect_test::expect![[r#"
                 pub fn foo() -> u32 {
                     {
-                        let mut v1: u32 = 0_u32;
-                        let mut v2: &'_ mut u32 = &mut v1;
+                        let v1: u32 = 0_u32;
+                        let v2: &'_ mut u32 = &mut v1;
                         return *v2;
                     }
                 }"#]]

From abaa911f20066631154502ff7f957b9e93124ae4 Mon Sep 17 00:00:00 2001
From: bit-aloo <sshourya17@gmail.com>
Date: Thu, 27 Aug 2026 05:04:24 +0530
Subject: [PATCH 2/7] Add mutability to fn argument lists

---
 crates/formality-rust/src/grammar/fns.rs     |  5 +++--
 crates/formality-rust/src/to_rust/context.rs |  4 ++--
 crates/formality-rust/src/to_rust/fns.rs     | 10 +++++-----
 crates/formality-rust/src/to_rust/mod.rs     |  6 +++---
 4 files changed, 13 insertions(+), 12 deletions(-)

diff --git a/crates/formality-rust/src/grammar/fns.rs b/crates/formality-rust/src/grammar/fns.rs
index 8d59f2f6c..32eafd0b2 100644
--- a/crates/formality-rust/src/grammar/fns.rs
+++ b/crates/formality-rust/src/grammar/fns.rs
@@ -1,4 +1,4 @@
-use crate::grammar::expr::Block;
+use crate::grammar::expr::{Block, Mutability};
 use crate::grammar::{Binder, Ty, ValueId, WhereClause};
 use crate::prove::Safety;
 use formality_core::term;
@@ -18,8 +18,9 @@ pub struct FnBoundData {
     pub body: MaybeFnBody,
 }
 
-#[term($id : $ty)]
+#[term($mutability $id : $ty)]
 pub struct InputArg {
+    pub mutability: Mutability,
     pub id: ValueId,
     pub ty: Ty,
 }
diff --git a/crates/formality-rust/src/to_rust/context.rs b/crates/formality-rust/src/to_rust/context.rs
index 95d5cd465..e7dff69e6 100644
--- a/crates/formality-rust/src/to_rust/context.rs
+++ b/crates/formality-rust/src/to_rust/context.rs
@@ -351,8 +351,8 @@ mod tests {
             ],
             expect_test::expect![[r#"
                 pub trait Foo<T01> {
-                    fn blub<T10, T11>(mut k: T10, mut v: T11) -> T01;
-                    fn bar<T10, T11>(mut k: T10, mut v: T11) -> T01;
+                    fn blub<T10, T11>(k: T10, v: T11) -> T01;
+                    fn bar<T10, T11>(k: T10, v: T11) -> T01;
                 }"#]]
         );
     }
diff --git a/crates/formality-rust/src/to_rust/fns.rs b/crates/formality-rust/src/to_rust/fns.rs
index aa8abc491..2cf0bf49c 100644
--- a/crates/formality-rust/src/to_rust/fns.rs
+++ b/crates/formality-rust/src/to_rust/fns.rs
@@ -1,5 +1,6 @@
 use std::ops::Deref;
 
+use crate::grammar::expr::Mutability;
 use crate::grammar::{Fallible, Fn, FnBody, InputArg, MaybeFnBody};
 use crate::prove::Safety;
 
@@ -41,8 +42,7 @@ pub fn lower_fn(
 
 pub fn lower_fn_param(ctx: &mut Context, arg: &InputArg) -> Fallible<syntax::FnParam> {
     Ok(syntax::FnParam {
-        // TODO: Is there a way to know if a variable must be mutable?
-        mutable: true,
+        mutable: matches!(arg.mutability, Mutability::Mut),
         name: arg.id.deref().clone(),
         ty: tys::lower_ty(ctx, &arg.ty)?,
     })
@@ -87,7 +87,7 @@ mod test {
                 }
             ],
             expect_test::expect![[r#"
-                pub fn run(mut p1: i32, mut p2: i32) -> i32 {
+                pub fn run(p1: i32, p2: i32) -> i32 {
                     panic!("Trusted Fn Body")
                 }"#]]
         );
@@ -102,7 +102,7 @@ mod test {
                 }
             ],
             expect_test::expect![[r#"
-                pub fn run<T00>(mut p1: T00) -> T00 {
+                pub fn run<T00>(p1: T00) -> T00 {
                     panic!("Trusted Fn Body")
                 }"#]]
         );
@@ -120,7 +120,7 @@ mod test {
             expect_test::expect![[r#"
                 pub trait Bar { }
 
-                pub fn run<T00>(mut p1: T00) -> T00 where T00: Bar {
+                pub fn run<T00>(p1: T00) -> T00 where T00: Bar {
                     panic!("Trusted Fn Body")
                 }"#]]
         );
diff --git a/crates/formality-rust/src/to_rust/mod.rs b/crates/formality-rust/src/to_rust/mod.rs
index f4fa57af6..c5be6b015 100644
--- a/crates/formality-rust/src/to_rust/mod.rs
+++ b/crates/formality-rust/src/to_rust/mod.rs
@@ -299,7 +299,7 @@ mod test {
 
                 pub struct A<T00> where T00: Trait {}
 
-                pub fn valid<'a00, T01>(mut x: &'a00 A<T01>) -> () where T01: 'a00, T01: Trait {}"#]]
+                pub fn valid<'a00, T01>(x: &'a00 A<T01>) -> () where T01: 'a00, T01: Trait {}"#]]
         )
     }
 
@@ -316,8 +316,8 @@ mod test {
                 }
             ],
             expect_test::expect![[r#"
-                pub fn foo<'a00, 'a01>(mut a: &'a00 u32) -> &'a01 u32 where 'a00: 'a01 {
-                    let mut r: &'a01 u32 = identity::<&'a01 u32>(a);
+                pub fn foo<'a00, 'a01>(a: &'a00 u32) -> &'a01 u32 where 'a00: 'a01 {
+                    let r: &'a01 u32 = identity::<&'a01 u32>(a);
                     return r;
                 }"#]]
         )

From 1b6b795e7dad92c7fe6b02bf4f630ffbdc3eb3c6 Mon Sep 17 00:00:00 2001
From: bit-aloo <sshourya17@gmail.com>
Date: Thu, 27 Aug 2026 05:04:24 +0530
Subject: [PATCH 3/7] Track local mutability in borrow-check flow state

---
 .../src/check/borrow_check/flow_state.rs      | 67 ++++++++++++++-----
 .../src/check/borrow_check/liveness.rs        |  3 +-
 2 files changed, 53 insertions(+), 17 deletions(-)

diff --git a/crates/formality-rust/src/check/borrow_check/flow_state.rs b/crates/formality-rust/src/check/borrow_check/flow_state.rs
index 9f24e44b9..15ec3d00c 100644
--- a/crates/formality-rust/src/check/borrow_check/flow_state.rs
+++ b/crates/formality-rust/src/check/borrow_check/flow_state.rs
@@ -1,12 +1,19 @@
 use crate::check::borrow_check::liveness::LivePlaces;
 use crate::check::borrow_check::typed_place_expression::TypedPlaceExpr;
-use crate::grammar::expr::{Label, LabelId, PlaceExpr};
+use crate::grammar::expr::{Label, LabelId, Mutability, PlaceExpr};
 use crate::grammar::{InputArg, Lt, Parameter, Ty, ValueId};
 use crate::grammar::{RefKind, Variable};
 use crate::prove::{Env, MaxUniverse};
 use formality_core::visit::CoreVisit;
 use formality_core::{term, Fallible, Set, Union, Upcast, UpcastFrom};
 
+#[term($mutability $id : $ty)]
+pub struct LocalDecl {
+    pub mutability: Mutability,
+    pub id: ValueId,
+    pub ty: Ty,
+}
+
 /// A scope in the scope stack, tracking labeled blocks and loops.
 /// Scopes live in `PointFlowState` and track locals for drop purposes.
 /// The types are stored here so that type lookup can happen through the flow state.
@@ -26,10 +33,11 @@ pub struct Scope {
     /// If `None`, this is a plain block scope (no `continue` allowed).
     pub continue_live_places: Option<LivePlaces>,
 
-    /// Local variables declared in this scope, with their types.
-    /// Used for type lookup (name resolution). Searched by `local_variable`, `has_local`.
+    /// Local variables declared in this scope, with their types and mutability.
+    /// Used for type lookup (name resolution). Searched by `local_variable`,
+    /// `local_mutability`, `has_local`.
     /// Always added to the innermost scope, regardless of label.
-    pub locals: Vec<(ValueId, Ty)>,
+    pub locals: Vec<LocalDecl>,
 
     /// Local variables to drop when this scope exits.
     /// For `let 'a: x = ...`, `x` goes into the named scope `'a`'s `drop_locals`.
@@ -216,7 +224,13 @@ impl FlowState {
         };
 
         for input_arg in input_args {
-            this = this.with_local_in_scope(env, &None, &input_arg.id, &input_arg.ty)?;
+            this = this.with_local_in_scope(
+                env,
+                &None,
+                &input_arg.mutability,
+                &input_arg.id,
+                &input_arg.ty,
+            )?;
         }
 
         Ok(this)
@@ -359,6 +373,7 @@ impl FlowState {
         &self,
         env: &Env,
         label: &Option<Label>,
+        mutability: &Mutability,
         id: &ValueId,
         ty: &Ty,
     ) -> Fallible<Self> {
@@ -401,28 +416,47 @@ impl FlowState {
             .scopes
             .last_mut()
             .ok_or_else(|| anyhow::anyhow!("no scope to add local `{id:?}` to"))?;
-        innermost.locals.push((id.clone(), ty.clone()));
+        innermost.locals.push(LocalDecl {
+            mutability: mutability.clone(),
+            id: id.clone(),
+            ty: ty.clone(),
+        });
 
         Ok(this)
     }
 
-    /// Look up a local variable's type by searching scopes from innermost to outermost.
-    pub fn local_variable(&self, id: &ValueId) -> Fallible<Ty> {
+    /// Look up a local variable's declaration by searching scopes from innermost to outermost.
+    fn local_decl(&self, id: &ValueId) -> Fallible<&LocalDecl> {
         for scope in self.scopes.iter().rev() {
-            for (local_id, ty) in scope.locals.iter().rev() {
-                if local_id == id {
-                    return Ok(ty.clone());
+            for local in scope.locals.iter().rev() {
+                if local.id == *id {
+                    return Ok(local);
                 }
             }
         }
         anyhow::bail!("unknown local variable `{id:?}`")
     }
 
+    /// Look up a local variable's type by searching scopes from innermost to outermost.
+    pub fn local_variable(&self, id: &ValueId) -> Fallible<Ty> {
+        Ok(self.local_decl(id)?.ty.clone())
+    }
+
+    pub fn local_is_mut(&self, id: &ValueId) -> bool {
+        matches!(
+            self.local_decl(id),
+            Ok(LocalDecl {
+                mutability: Mutability::Mut,
+                ..
+            })
+        )
+    }
+
     /// Check if any scope contains a local with this id.
     pub fn has_local(&self, id: &ValueId) -> bool {
         self.scopes
             .iter()
-            .any(|s| s.locals.iter().any(|(local_id, _)| local_id == id))
+            .any(|s| s.locals.iter().any(|local| local.id == *id))
     }
 
     /// Check if any scope has the given label.
@@ -506,8 +540,8 @@ impl FlowState {
         }
 
         // Remove locals going out of scope from the uninit set
-        for (id, _) in &locals {
-            successor.uninit.remove(&PlaceExpr::Var(id.clone()));
+        for local in &locals {
+            successor.uninit.remove(&PlaceExpr::Var(local.id.clone()));
         }
 
         FlowState {
@@ -591,8 +625,9 @@ impl FlowState {
         let mut all_drop_places: Set<PlaceExpr> = Default::default();
 
         for scope in &self.scopes {
-            for (id, _ty) in &scope.locals {
-                if !all_local_places.insert(id.upcast()) {
+            for local in &scope.locals {
+                if !all_local_places.insert((&local.id).upcast()) {
+                    let id = &local.id;
                     panic!("local `{id:?}` appears in multiple scopes' locals");
                 }
             }
diff --git a/crates/formality-rust/src/check/borrow_check/liveness.rs b/crates/formality-rust/src/check/borrow_check/liveness.rs
index e06961ada..867e4dcab 100644
--- a/crates/formality-rust/src/check/borrow_check/liveness.rs
+++ b/crates/formality-rust/src/check/borrow_check/liveness.rs
@@ -116,7 +116,7 @@ impl IntoLivenessContext for FlowState {
             locals: self
                 .scopes
                 .iter()
-                .flat_map(|s| s.locals.iter().map(|(id, _)| id.clone()))
+                .flat_map(|s| s.locals.iter().map(|local| local.id.clone()))
                 .collect(),
         }
     }
@@ -265,6 +265,7 @@ impl LiveBefore for Stmt {
         match self {
             Stmt::Let {
                 label: _,
+                mutability: _,
                 id,
                 ty: _,
                 init,

From 26570d4e52163aa643d5055e4c8215cba34558bd Mon Sep 17 00:00:00 2001
From: bit-aloo <sshourya17@gmail.com>
Date: Thu, 27 Aug 2026 05:04:24 +0530
Subject: [PATCH 4/7] Thread mutability through codegen scope

---
 crates/formality-rust/src/codegen/mod.rs   |  8 ++++----
 crates/formality-rust/src/codegen/scope.rs | 12 ++++++++----
 2 files changed, 12 insertions(+), 8 deletions(-)

diff --git a/crates/formality-rust/src/codegen/mod.rs b/crates/formality-rust/src/codegen/mod.rs
index 8f83fc22a..e9c1f8c50 100644
--- a/crates/formality-rust/src/codegen/mod.rs
+++ b/crates/formality-rust/src/codegen/mod.rs
@@ -127,18 +127,18 @@ judgment_fn! {
 
         (
             (let (local, cfn) = cfn.alloc_temp(ty)?)
-            (let scope = scope.push_var(id, local, ty)?)
+            (let scope = scope.push_var(id, local, ty, mutability)?)
             (codegen_expr_into(global, cfn, scope, local, &init.expr) => (code, global, cfn))
             ---- ("let-init")
-            (codegen_stmt(global, cfn, scope, Stmt::Let { label: _, id, ty, init: Some(init) }) => (code, scope, global, cfn))
+            (codegen_stmt(global, cfn, scope, Stmt::Let { mutability, label: _, id, ty, init: Some(init) }) => (code, scope, global, cfn))
         )
 
         (
             (let (local, cfn) = cfn.alloc_temp(ty)?)
-            (let scope = scope.push_var(id, local, ty)?)
+            (let scope = scope.push_var(id, local, ty, mutability)?)
             (let code = cfn.fresh_code_block())
             ---- ("let-no-init")
-            (codegen_stmt(global, cfn, scope, Stmt::Let { label: _, id, ty, init: None }) => (code, scope, global, cfn))
+            (codegen_stmt(global, cfn, scope, Stmt::Let { mutability, label: _, id, ty, init: None }) => (code, scope, global, cfn))
         )
 
         (
diff --git a/crates/formality-rust/src/codegen/scope.rs b/crates/formality-rust/src/codegen/scope.rs
index 454ce09fb..ab537aa54 100644
--- a/crates/formality-rust/src/codegen/scope.rs
+++ b/crates/formality-rust/src/codegen/scope.rs
@@ -2,7 +2,10 @@
 
 use crate::check::borrow_check::env::TypeckEnv;
 use crate::check::borrow_check::flow_state::FlowState;
-use crate::grammar::{expr::LabelId, Crates, Fallible, Parameter, Ty, ValueId, Wcs};
+use crate::grammar::{
+    expr::{LabelId, Mutability},
+    Crates, Fallible, Parameter, Ty, ValueId, Wcs,
+};
 use crate::prove::{Env, Program};
 use formality_core::Upcast;
 use libspecr::prelude::Map;
@@ -236,14 +239,15 @@ impl CodegenScope {
         id: impl Upcast<ValueId>,
         local: impl Upcast<MiniRustLocal>,
         ty: impl Upcast<Ty>,
+        mutability: &Mutability,
     ) -> Fallible<Self> {
         let id: ValueId = id.upcast();
         let local: MiniRustLocal = local.upcast();
         let ty: Ty = ty.upcast();
         let mut s = self.clone();
-        s.flow_state = s
-            .flow_state
-            .with_local_in_scope(&Env::default(), &None, &id, &ty)?;
+        s.flow_state =
+            s.flow_state
+                .with_local_in_scope(&Env::default(), &None, mutability, &id, &ty)?;
         s.vars.push((id, local, ty));
         Ok(s)
     }

From 26179fe33b2b50c552faa9833bf84254412202af Mon Sep 17 00:00:00 2001
From: bit-aloo <sshourya17@gmail.com>
Date: Thu, 27 Aug 2026 05:04:24 +0530
Subject: [PATCH 5/7] Enforce mutability on assignments and mutable borrows

---
 .../src/check/borrow_check/nll.rs             | 90 ++++++++++++++++++-
 1 file changed, 88 insertions(+), 2 deletions(-)

diff --git a/crates/formality-rust/src/check/borrow_check/nll.rs b/crates/formality-rust/src/check/borrow_check/nll.rs
index adffe4be0..7a24835d0 100644
--- a/crates/formality-rust/src/check/borrow_check/nll.rs
+++ b/crates/formality-rust/src/check/borrow_check/nll.rs
@@ -199,10 +199,10 @@ judgment_fn! {
                     LiveBefore::live_before(&Assignment(id), env, &state, &places_live_on_exit),
                 ) => state))
 
-            (let state = state.with_local_in_scope(&env.env, label, id, ty)?)
+            (let state = state.with_local_in_scope(&env.env, label, mutability, id, ty)?)
             (let state = if init.is_none() { state.with_uninit(&PlaceExpr::Var(id.clone())) } else { state.with_initialized(&PlaceExpr::Var(id.clone())) })
             ------------------------------------------------------------ ("let")
-            (borrow_check_statement(env, assumptions, state, Stmt::Let { label, id, ty, init }, places_live_on_exit) => (env, state))
+            (borrow_check_statement(env, assumptions, state, Stmt::Let { mutability, label, id, ty, init }, places_live_on_exit) => (env, state))
         )
 
         (
@@ -401,6 +401,8 @@ judgment_fn! {
             // Prove subtyping: value_ty <: place_ty
             (prove_assignable(env, assumptions, state, value_ty, &place.ty) => state)
 
+            (prove_place_is_assignable(env, assumptions, state, place) => ())
+
             (access_permitted(
                 env,
                 assumptions,
@@ -470,6 +472,8 @@ judgment_fn! {
                 place,
             ) => (place, state))
 
+            (prove_borrow_mutability_ok(env, assumptions, state, kind, place) => ())
+
             // Check that the access required by the borrow is permitted
             (let access_kind = match kind {
                 RefKind::Shared => AccessKind::Read,
@@ -1022,6 +1026,88 @@ judgment_fn! {
     }
 }
 
+judgment_fn! {
+    fn prove_place_is_mut(
+        env: TypeckEnv,
+        assumptions: Wcs,
+        state: FlowState,
+        place: TypedPlaceExpr,
+    ) => () {
+        debug(place, state, assumptions, env)
+
+        (
+            (if state.local_is_mut(&local_id))
+            ------------------------------------------------------------ ("mut local")
+            (prove_place_is_mut(_env, _assumptions, state, TypedPlaceExpressionData::Local(local_id)) => ())
+        )
+
+        (
+            (prove_ty_is_rigid(env, assumptions, state, &prefix.ty) => (RigidTy { name: RigidName::Ref(kind), .. }, _state))
+            (if let RefKind::Mut = kind)
+            ------------------------------------------------------------ ("deref of &mut")
+            (prove_place_is_mut(env, assumptions, state, TypedPlaceExpressionData::Deref(prefix)) => ())
+        )
+
+        (
+            (prove_place_is_mut(env, assumptions, state, prefix) => ())
+            ------------------------------------------------------------ ("field")
+            (prove_place_is_mut(env, assumptions, state, TypedPlaceExpressionData::Field(prefix, _, _, _)) => ())
+        )
+
+        (
+            (prove_place_is_mut(env, assumptions, state, prefix) => ())
+            ------------------------------------------------------------ ("tuple field")
+            (prove_place_is_mut(env, assumptions, state, TypedPlaceExpressionData::TupleField(prefix, _)) => ())
+        )
+    }
+}
+
+judgment_fn! {
+    fn prove_borrow_mutability_ok(
+        env: TypeckEnv,
+        assumptions: Wcs,
+        state: FlowState,
+        kind: RefKind,
+        place: TypedPlaceExpr,
+    ) => () {
+        debug(kind, place, state, assumptions, env)
+
+        (
+            ------------------------------------------------------------ ("shared borrow")
+            (prove_borrow_mutability_ok(_env, _assumptions, _state, RefKind::Shared, _place) => ())
+        )
+
+        (
+            (prove_place_is_mut(env, assumptions, state, place) => ())
+            ------------------------------------------------------------ ("mutable borrow")
+            (prove_borrow_mutability_ok(env, assumptions, state, RefKind::Mut, place) => ())
+        )
+    }
+}
+
+judgment_fn! {
+    fn prove_place_is_assignable(
+        env: TypeckEnv,
+        assumptions: Wcs,
+        state: FlowState,
+        place: TypedPlaceExpr,
+    ) => () {
+        debug(place, state, assumptions, env)
+
+        (
+            (if !check_place_initialized(&state, &place.to_place_expression()))
+            ------------------------------------------------------------ ("deferred initialization")
+            (prove_place_is_assignable(_env, _assumptions, state, place) => ())
+        )
+
+        (
+            (prove_place_is_mut(env, assumptions, state, place) => ())
+            ------------------------------------------------------------ ("mutable place")
+            (prove_place_is_assignable(env, assumptions, state, place) => ())
+        )
+    }
+}
+
 judgment_fn! {
     /// Prove that any loans issued in thes value expressions (evaluated in this order) are respected.
     fn prove_ty_is_ref(

From b7e302c0950b926216266461ae907623689ea87e Mon Sep 17 00:00:00 2001
From: bit-aloo <sshourya17@gmail.com>
Date: Thu, 27 Aug 2026 05:04:31 +0530
Subject: [PATCH 6/7] Add mut to test programs that mutate locals

---
 tests/borrowck.rs   | 68 ++++++++++++++++++++++-----------------------
 tests/codegen.rs    |  8 +++---
 tests/mir_typeck.rs |  4 +--
 3 files changed, 40 insertions(+), 40 deletions(-)

diff --git a/tests/borrowck.rs b/tests/borrowck.rs
index 3eb80e36f..74cc144ea 100644
--- a/tests/borrowck.rs
+++ b/tests/borrowck.rs
@@ -222,7 +222,7 @@ fn conditional_init_both_branches() {
 fn if_without_else_ok() {
     FormalityTest::new(crates![crate Foo {
         fn foo() -> u32 {
-            let x: u32 = 1_u32;
+            let mut x: u32 = 1_u32;
             if true {
                 x = 2_u32;
             }
@@ -1288,7 +1288,7 @@ fn move_out_of_mut_ref() {
 
         fn foo() -> Datum {
             exists<'r0, 'r1> {
-                let x: Datum = Datum { value: 0_u32 };
+                let mut x: Datum = Datum { value: 0_u32 };
                 let r: &'r0 mut Datum = &'r1 mut x;
                 let y: Datum = *r;
                 return y;
@@ -2062,7 +2062,7 @@ fn mutable_ref_prevents_mutation() {
     FormalityTest::new(crates![crate Foo {
         fn foo() -> i32 {
             exists<'r0, 'r1> {
-                let v1: i32 = 0_i32;
+                let mut v1: i32 = 0_i32;
                 let v2: &'r0 mut i32 = &'r1 mut v1;
                 // This should result in an error
                 v1 = 1_i32;
@@ -2101,7 +2101,7 @@ fn shared_ref_prevents_mutation() {
     FormalityTest::new(crates![crate Foo {
         fn foo() -> i32 {
             exists<'r0, 'r1> {
-                let v1: i32 = 0_i32;
+                let mut v1: i32 = 0_i32;
                 let v2: &'r0 i32 = &'r1 v1;
                 v1 = 1_i32;
                 return *v2;
@@ -2282,7 +2282,7 @@ fn drop_while_mutably_borrowed() {
             exists<'r0, 'r1> {
                 let v2: &'r0 mut i32;
                 {
-                    let v1: i32 = 0_i32;
+                    let mut v1: i32 = 0_i32;
                     v2 = &'r1 mut v1;
                 }
                 return *v2;
@@ -2486,7 +2486,7 @@ fn problem_case_4() {
             value: u32,
          }
 
-        fn min_problem_case_4<'a>(list: &'a mut Map, list2: &'a mut Map) -> u32 {
+        fn min_problem_case_4<'a>(mut list: &'a mut Map, list2: &'a mut Map) -> u32 {
             exists<'r0> {
                 let num: &'r0 mut u32 = &'r0 mut (*list).value;
                 list = &'a mut *list2;
@@ -2613,13 +2613,13 @@ fn cfg_union_approx_cause_false_error() {
     FormalityTest::new(crates![crate Foo {
         fn foo () -> u32 {
             exists<'l_p, 'l_q, 'loan_0, 'loan_1, 'loan_2, 'loan_3> {
-                let a: u32 = 0_u32;
-                let b: u32 = 0_u32;
+                let mut a: u32 = 0_u32;
+                let mut b: u32 = 0_u32;
                 // In Rustc, the 1-tuple is needed for some reason
                 // Niko does not 100% understand, else rustc is able to
                 // see that this program is safe.
-                let q: &'l_q mut u32 = &'loan_0 mut a;
-                let p: &'l_p mut u32 = &'loan_1 mut a;
+                let mut q: &'l_q mut u32 = &'loan_0 mut a;
+                let mut p: &'l_p mut u32 = &'loan_1 mut a;
                 if true {
                     p = &'loan_1 mut a;
                     q = &'loan_2 mut b;
@@ -2883,7 +2883,7 @@ fn write_to_borrowed_before_continue() {
     FormalityTest::new(crates![crate Foo {
         fn foo() -> u32 {
             exists<'r0, 'r1> {
-                let a: u32 = 22_u32;
+                let mut a: u32 = 22_u32;
                 let p: &'r0 u32 = &'r1 a;
                 'l: loop {
                     if true {
@@ -3010,9 +3010,9 @@ fn write_to_borrowed_before_zero_iteration_loop() {
     FormalityTest::new(crates![crate Foo {
         fn foo() -> u32 {
             exists<'r0, 'r1, 'r2> {
-                let a: u32 = 22_u32;
+                let mut a: u32 = 22_u32;
                 let b: u32 = 22_u32;
-                let p: &'r0 u32 = &'r1 a;
+                let mut p: &'r0 u32 = &'r1 a;
                 a = 23_u32;
                 'l: loop {
                     p = &'r2 b;
@@ -3199,7 +3199,7 @@ fn call_mut_under_shared_borrow() {
 
         fn bar() -> u32 {
             exists<'r0, 'r1, 'r2> {
-                let v: u32 = 0_u32;
+                let mut v: u32 = 0_u32;
                 let p: &'r0 u32 = &'r1 v;
                 let _: u32 = foo::<'r2>(&'r2 mut v);
                 return *p;
@@ -3227,7 +3227,7 @@ fn struct_disjoint_field_borrows() {
         struct Point { x: u32, y: u32 }
         fn foo() -> u32 {
             exists<'r0, 'r1, 'r2, 'r3> {
-                let p: Point = Point { x: 0_u32, y: 0_u32 };
+                let mut p: Point = Point { x: 0_u32, y: 0_u32 };
                 let b1: &'r0 mut u32 = &'r1 mut p.x;
                 let b2: &'r2 mut u32 = &'r3 mut p.y;
                 *b1 = 1_u32;
@@ -3247,7 +3247,7 @@ fn struct_conflicting_field_borrows() {
         struct Point { x: u32, y: u32 }
         fn foo() -> u32 {
             exists<'r0, 'r1> {
-                let p: Point = Point { x: 0_u32, y: 0_u32 };
+                let mut p: Point = Point { x: 0_u32, y: 0_u32 };
                 let b1: &'r0 mut u32 = &'r1 mut p.x;
                 p.x = 1_u32;
                 return *b1;
@@ -3280,7 +3280,7 @@ fn struct_construction_with_borrowed_local() {
         }
         fn foo() -> u32 {
             exists<'r0, 'r1> {
-                let v1: u32 = 22_u32;
+                let mut v1: u32 = 22_u32;
                 let v2: &'r0 mut u32 = &'r1 mut v1;
                 let w: Wrapper = Wrapper { value: v1 };
                 return *v2;
@@ -3321,7 +3321,7 @@ fn struct_with_mutable_reference_locks_local() {
         }
         fn foo() -> u32 {
             exists<'r0> {
-                let v1: u32 = 0_u32;
+                let mut v1: u32 = 0_u32;
                 let w: Wrapper<'r0> = Wrapper::<'r0> { value: &'r0 mut v1 };
                 v1 = 1_u32;
                 return *(w.value);
@@ -3473,7 +3473,7 @@ fn loan_cannot_outlive_lifetime_fail() {
     FormalityTest::new(crates![crate Foo {
         fn foo() -> u32 {
             exists<'r0, 'r1, 'r2> {
-                let x: u32 = 22_u32;
+                let mut x: u32 = 22_u32;
                 let p: &'r1 u32 = &'r0 x;
                 let q: &'r2 u32 = p;
                 x = 1_u32;
@@ -3512,7 +3512,7 @@ fn loan_cannot_outlive_lifetime_pass() {
     FormalityTest::new(crates![crate Foo {
         fn foo() -> u32 {
             exists<'r0, 'r1, 'r2> {
-                let x: u32 = 22_u32;
+                let mut x: u32 = 22_u32;
                 let p: &'r1 u32 = &'r0 x;
                 let q: &'r2 u32 = p;
                 x = 1_u32;
@@ -3636,7 +3636,7 @@ fn local_shadowing_fn_name_stays_live() {
 
         fn foo() -> u32 {
             exists<'r0, 'r1> {
-                let x: u32 = 22_u32;
+                let mut x: u32 = 22_u32;
                 let helper: &'r1 u32 = &'r0 x;
                 x = 1_u32;
                 helper;
@@ -3837,7 +3837,7 @@ fn issue_63908_remove_last_node_iterative() {
 
         fn remove_last_node_iterative<'a>(node: &'a mut List) -> u32 {
             exists<'r0, 'r1> {
-                let cursor: &'r0 mut List = &'r0 mut *node;
+                let mut cursor: &'r0 mut List = &'r0 mut *node;
                 'l: loop {
                     let next: &'r1 mut List = &'r1 mut *cursor;
                     if true {
@@ -3898,8 +3898,8 @@ fn issue_57165_no_control_flow() {
 
         fn no_control_flow() -> u32 {
             exists<'r0, 'r1, 'r2, 'r3> {
-                let b: X = X { value: 0_u32 };
-                let p: &'r0 mut X = &'r1 mut b;
+                let mut b: X = X { value: 0_u32 };
+                let mut p: &'r0 mut X = &'r1 mut b;
                 'l: loop {
                     let now: &'r2 mut X = &'r2 mut *p;
                     if true {
@@ -3945,8 +3945,8 @@ fn issue_57165_conditional() {
 
         fn conditional() -> u32 {
             exists<'r0, 'r1, 'r2, 'r3> {
-                let b: X = X { value: 0_u32 };
-                let p: &'r0 mut X = &'r1 mut b;
+                let mut b: X = X { value: 0_u32 };
+                let mut p: &'r0 mut X = &'r1 mut b;
                 'l: loop {
                     let now: &'r2 mut X = &'r2 mut *p;
                     if true {
@@ -4034,8 +4034,8 @@ fn issue_57165_conditional_with_indirection() {
 
         fn conditional_with_indirection() -> u32 {
             exists<'r0, 'r1, 'r2, 'r3> {
-                let b: X = X { value: 0_u32 };
-                let p: &'r0 mut X = &'r1 mut b;
+                let mut b: X = X { value: 0_u32 };
+                let mut p: &'r0 mut X = &'r1 mut b;
                 'l: loop {
                     let now: &'r2 mut X = &'r2 mut *p;
                     if true {
@@ -4089,9 +4089,9 @@ fn issue_46859_to_refs() {
 
         fn next_from_field<'x>(n: &'x mut u32) -> &'x mut List { trusted }
 
-        fn to_refs<'a>(list: &'a mut List) -> &'a mut u32 {
+        fn to_refs<'a>(mut list: &'a mut List) -> &'a mut u32 {
             exists<'r0, 'r1> {
-                let result: &'a mut u32;
+                let mut result: &'a mut u32;
                 'l: loop {
                     result = &'r0 mut (*list).value;
                     if true {
@@ -4123,9 +4123,9 @@ fn issue_46859_to_refs2() {
 
         fn next_from_field<'x>(n: &'x mut u32) -> &'x mut List { trusted }
 
-        fn to_refs2<'a>(list: &'a mut List) -> &'a mut u32 {
+        fn to_refs2<'a>(mut list: &'a mut List) -> &'a mut u32 {
             exists<'r0, 'r1> {
-                let result: &'a mut u32;
+                let mut result: &'a mut u32;
                 'l: loop {
                     result = &'r0 mut (*list).value;
                     if true {
@@ -4172,8 +4172,8 @@ fn issue_46859_to_refs3() {
 
         fn to_refs3<'a>(list: &'a mut List) -> &'a mut u32 {
             exists<'r0, 'r1> {
-                let result: &'a mut u32;
-                let cursor: &'a mut List = &'a mut *list;
+                let mut result: &'a mut u32;
+                let mut cursor: &'a mut List = &'a mut *list;
                 'l: loop {
                     result = &'r0 mut (*cursor).value;
                     if true {
diff --git a/tests/codegen.rs b/tests/codegen.rs
index c640a987d..63ef22fd2 100644
--- a/tests/codegen.rs
+++ b/tests/codegen.rs
@@ -40,7 +40,7 @@ fn let_bindings() {
 fn assignment() {
     FormalityTest::new(crates![crate test {
         fn main() -> () {
-            let x: i32 = 1_i32;
+            let mut x: i32 = 1_i32;
             x = 2 _ i32;
             println!(x);
         }
@@ -360,7 +360,7 @@ fn if_else_inside_loop_with_breaks() {
 fn multiple_breaks_same_label() {
     FormalityTest::new(crates![crate test {
         fn main() -> () {
-            let x: i32 = 0_i32;
+            let mut x: i32 = 0_i32;
             'a: loop {
                 if false {
                     x = 1_i32;
@@ -431,7 +431,7 @@ fn exists_with_lifetime_parameterized_type() {
 fn return_from_inside_loop() {
     FormalityTest::new(crates![crate test {
         fn main() -> () {
-            let x: i32 = 0_i32;
+            let mut x: i32 = 0_i32;
             'a: loop {
                 x = 77_i32;
                 break 'a;
@@ -447,7 +447,7 @@ fn return_from_inside_loop() {
 fn return_from_nested_block_inside_loop() {
     FormalityTest::new(crates![crate test {
         fn main() -> () {
-            let x: i32 = 0_i32;
+            let mut x: i32 = 0_i32;
             'a: loop {
                 {
                     x = 88_i32;
diff --git a/tests/mir_typeck.rs b/tests/mir_typeck.rs
index e6753ceca..1d321d608 100644
--- a/tests/mir_typeck.rs
+++ b/tests/mir_typeck.rs
@@ -99,7 +99,7 @@ fn test_goto_terminator() {
 fn test_cyclic_goto() {
     FormalityTest::new(crates![crate Foo {
         fn foo() -> u32 {
-            let v0: u32 = 0_u32;
+            let mut v0: u32 = 0_u32;
             loop {
                 v0 = v0;
             }
@@ -249,7 +249,7 @@ fn test_struct() {
         }
 
         fn foo (v1: u32) -> u32 {
-            let v2: Dummy = Dummy { value: 1_u32, is_true: false };
+            let mut v2: Dummy = Dummy { value: 1_u32, is_true: false };
             v2.value = 2_u32;
             return v1;
         }

From 1a569dd0adfc0fcd3441fe70c00fd19dc5d4d9fe Mon Sep 17 00:00:00 2001
From: bit-aloo <sshourya17@gmail.com>
Date: Thu, 27 Aug 2026 05:04:31 +0530
Subject: [PATCH 7/7] Update expect strings for mutability output

---
 tests/borrowck.rs   | 12 +++---
 tests/mir_typeck.rs | 96 ++++++++++++++++++++++-----------------------
 2 files changed, 54 insertions(+), 54 deletions(-)

diff --git a/tests/borrowck.rs b/tests/borrowck.rs
index 74cc144ea..20c848d8a 100644
--- a/tests/borrowck.rs
+++ b/tests/borrowck.rs
@@ -3967,8 +3967,8 @@ fn issue_57165_conditional() {
         .borrowck_err(BorrowCheckFailure::Alpha, expect_test::expect![[r#"
             the rule "fixed-point" at (nll.rs) failed because
               condition evaluated to false: `state0 == state1`
-                state0 = flow_state([scope(none, None, {}, None, [], []), scope(none, None, {}, None, [], []), scope(some(U(4)), None, {}, None, [(b, X), (p, &?lt_1 mut X)], [b : X, p : &?lt_1 mut X]), scope(some(U(4)), Some('l), {}, Some({* p}), [], [])], point_flow_state({pending_outlives(?lt_2, ?lt_1)}, {loan(?lt_2, b : X, mut)}, {}), {}, {}, {pending_outlives(?lt_2, ?lt_1)})
-                state1 = flow_state([scope(none, None, {}, None, [], []), scope(none, None, {}, None, [], []), scope(some(U(4)), None, {}, None, [(b, X), (p, &?lt_1 mut X)], [b : X, p : &?lt_1 mut X]), scope(some(U(4)), Some('l), {}, Some({* p}), [], [])], point_flow_state({pending_outlives(?lt_1, ?lt_3), pending_outlives(?lt_2, ?lt_1), pending_outlives(?lt_3, ?lt_4), pending_outlives(?lt_4, ?lt_1)}, {loan(?lt_2, b : X, mut), loan(?lt_3, *(p : &?lt_1 mut X) : <&?lt_1 mut X as Derefable>::Target, mut)}, {}), {labeled_flow_state('l, point_flow_state({pending_outlives(?lt_1, ?lt_3), pending_outlives(?lt_2, ?lt_1)}, {loan(?lt_2, b : X, mut), loan(?lt_3, *(p : &?lt_1 mut X) : <&?lt_1 mut X as Derefable>::Target, mut)}, {}))}, {}, {pending_outlives(?lt_1, ?lt_3), pending_outlives(?lt_2, ?lt_1), pending_outlives(?lt_3, ?lt_4), pending_outlives(?lt_4, ?lt_1)})
+                state0 = flow_state([scope(none, None, {}, None, [], []), scope(none, None, {}, None, [], []), scope(some(U(4)), None, {}, None, [mut b : X, mut p : &?lt_1 mut X], [b : X, p : &?lt_1 mut X]), scope(some(U(4)), Some('l), {}, Some({* p}), [], [])], point_flow_state({pending_outlives(?lt_2, ?lt_1)}, {loan(?lt_2, b : X, mut)}, {}), {}, {}, {pending_outlives(?lt_2, ?lt_1)})
+                state1 = flow_state([scope(none, None, {}, None, [], []), scope(none, None, {}, None, [], []), scope(some(U(4)), None, {}, None, [mut b : X, mut p : &?lt_1 mut X], [b : X, p : &?lt_1 mut X]), scope(some(U(4)), Some('l), {}, Some({* p}), [], [])], point_flow_state({pending_outlives(?lt_1, ?lt_3), pending_outlives(?lt_2, ?lt_1), pending_outlives(?lt_3, ?lt_4), pending_outlives(?lt_4, ?lt_1)}, {loan(?lt_2, b : X, mut), loan(?lt_3, *(p : &?lt_1 mut X) : <&?lt_1 mut X as Derefable>::Target, mut)}, {}), {labeled_flow_state('l, point_flow_state({pending_outlives(?lt_1, ?lt_3), pending_outlives(?lt_2, ?lt_1)}, {loan(?lt_2, b : X, mut), loan(?lt_3, *(p : &?lt_1 mut X) : <&?lt_1 mut X as Derefable>::Target, mut)}, {}))}, {}, {pending_outlives(?lt_1, ?lt_3), pending_outlives(?lt_2, ?lt_1), pending_outlives(?lt_3, ?lt_4), pending_outlives(?lt_4, ?lt_1)})
 
             the rule "borrow of disjoint places" at (nll.rs) failed because
               condition evaluated to false: `place_disjoint_from_place(&loan.place, &access.place)`
@@ -4233,8 +4233,8 @@ fn issue_46859_decoder_next() {
         .borrowck_err(BorrowCheckFailure::Nll, expect_test::expect![[r#"
             the rule "fixed-point" at (nll.rs) failed because
               condition evaluated to false: `state0 == state1`
-                state0 = flow_state([scope(some(U(1)), None, {}, None, [(d, &!lt_1 mut Decoder)], [d : &!lt_1 mut Decoder]), scope(some(U(1)), None, {}, None, [], []), scope(some(U(3)), None, {}, None, [], []), scope(some(U(3)), Some('l), {}, Some({(* d) . buf_read}), [], [])], point_flow_state({pending_outlives(!lt_1, ?lt_2), pending_outlives(?lt_2, ?lt_3), pending_outlives(?lt_3, !lt_1)}, {}, {}), {}, {}, {pending_outlives(!lt_1, ?lt_2), pending_outlives(?lt_2, ?lt_3), pending_outlives(?lt_3, !lt_1)})
-                state1 = flow_state([scope(some(U(1)), None, {}, None, [(d, &!lt_1 mut Decoder)], [d : &!lt_1 mut Decoder]), scope(some(U(1)), None, {}, None, [], []), scope(some(U(3)), None, {}, None, [], []), scope(some(U(3)), Some('l), {}, Some({(* d) . buf_read}), [], [])], point_flow_state({pending_outlives(!lt_1, ?lt_2), pending_outlives(?lt_2, ?lt_3), pending_outlives(?lt_3, !lt_1)}, {loan(?lt_2, *(d : &!lt_1 mut Decoder) : <&!lt_1 mut Decoder as Derefable>::Target . buf_read[Decoder , struct] : u32, mut)}, {}), {}, {}, {pending_outlives(!lt_1, ?lt_2), pending_outlives(?lt_2, ?lt_3), pending_outlives(?lt_3, !lt_1)})
+                state0 = flow_state([scope(some(U(1)), None, {}, None, [ d : &!lt_1 mut Decoder], [d : &!lt_1 mut Decoder]), scope(some(U(1)), None, {}, None, [], []), scope(some(U(3)), None, {}, None, [], []), scope(some(U(3)), Some('l), {}, Some({(* d) . buf_read}), [], [])], point_flow_state({pending_outlives(!lt_1, ?lt_2), pending_outlives(?lt_2, ?lt_3), pending_outlives(?lt_3, !lt_1)}, {}, {}), {}, {}, {pending_outlives(!lt_1, ?lt_2), pending_outlives(?lt_2, ?lt_3), pending_outlives(?lt_3, !lt_1)})
+                state1 = flow_state([scope(some(U(1)), None, {}, None, [ d : &!lt_1 mut Decoder], [d : &!lt_1 mut Decoder]), scope(some(U(1)), None, {}, None, [], []), scope(some(U(3)), None, {}, None, [], []), scope(some(U(3)), Some('l), {}, Some({(* d) . buf_read}), [], [])], point_flow_state({pending_outlives(!lt_1, ?lt_2), pending_outlives(?lt_2, ?lt_3), pending_outlives(?lt_3, !lt_1)}, {loan(?lt_2, *(d : &!lt_1 mut Decoder) : <&!lt_1 mut Decoder as Derefable>::Target . buf_read[Decoder , struct] : u32, mut)}, {}), {}, {}, {pending_outlives(!lt_1, ?lt_2), pending_outlives(?lt_2, ?lt_3), pending_outlives(?lt_3, !lt_1)})
 
             the rule "borrow of disjoint places" at (nll.rs) failed because
               condition evaluated to false: `place_disjoint_from_place(&loan.place, &access.place)`
@@ -4356,8 +4356,8 @@ fn issue_92985_filtering_lending_iterator() {
         .borrowck_err(BorrowCheckFailure::Nll, expect_test::expect![[r#"
             the rule "fixed-point" at (nll.rs) failed because
               condition evaluated to false: `state0 == state1`
-                state0 = flow_state([scope(some(U(1)), None, {}, None, [(f, &!lt_1 mut Filter)], [f : &!lt_1 mut Filter]), scope(some(U(1)), None, {}, None, [], []), scope(some(U(4)), None, {}, None, [], []), scope(some(U(4)), Some('l), {}, Some({(* f) . iter, (* f) . predicate}), [], [])], point_flow_state({pending_outlives(!lt_1, ?lt_2), pending_outlives(!lt_1, ?lt_3), pending_outlives(?lt_2, !lt_1), pending_outlives(?lt_2, ?lt_4)}, {}, {}), {}, {}, {pending_outlives(!lt_1, ?lt_2), pending_outlives(!lt_1, ?lt_3), pending_outlives(?lt_2, !lt_1), pending_outlives(?lt_2, ?lt_4)})
-                state1 = flow_state([scope(some(U(1)), None, {}, None, [(f, &!lt_1 mut Filter)], [f : &!lt_1 mut Filter]), scope(some(U(1)), None, {}, None, [], []), scope(some(U(4)), None, {}, None, [], []), scope(some(U(4)), Some('l), {}, Some({(* f) . iter, (* f) . predicate}), [], [])], point_flow_state({pending_outlives(!lt_1, ?lt_2), pending_outlives(!lt_1, ?lt_3), pending_outlives(?lt_2, !lt_1), pending_outlives(?lt_2, ?lt_4)}, {loan(?lt_2, *(f : &!lt_1 mut Filter) : <&!lt_1 mut Filter as Derefable>::Target . iter[Filter , struct] : u32, mut), loan(?lt_3, *(f : &!lt_1 mut Filter) : <&!lt_1 mut Filter as Derefable>::Target . predicate[Filter , struct] : u32, mut)}, {}), {labeled_flow_state('l, point_flow_state({pending_outlives(!lt_1, ?lt_2), pending_outlives(!lt_1, ?lt_3), pending_outlives(?lt_2, !lt_1), pending_outlives(?lt_2, ?lt_4)}, {loan(?lt_2, *(f : &!lt_1 mut Filter) : <&!lt_1 mut Filter as Derefable>::Target . iter[Filter , struct] : u32, mut)}, {}))}, {}, {pending_outlives(!lt_1, ?lt_2), pending_outlives(!lt_1, ?lt_3), pending_outlives(?lt_2, !lt_1), pending_outlives(?lt_2, ?lt_4)})
+                state0 = flow_state([scope(some(U(1)), None, {}, None, [ f : &!lt_1 mut Filter], [f : &!lt_1 mut Filter]), scope(some(U(1)), None, {}, None, [], []), scope(some(U(4)), None, {}, None, [], []), scope(some(U(4)), Some('l), {}, Some({(* f) . iter, (* f) . predicate}), [], [])], point_flow_state({pending_outlives(!lt_1, ?lt_2), pending_outlives(!lt_1, ?lt_3), pending_outlives(?lt_2, !lt_1), pending_outlives(?lt_2, ?lt_4)}, {}, {}), {}, {}, {pending_outlives(!lt_1, ?lt_2), pending_outlives(!lt_1, ?lt_3), pending_outlives(?lt_2, !lt_1), pending_outlives(?lt_2, ?lt_4)})
+                state1 = flow_state([scope(some(U(1)), None, {}, None, [ f : &!lt_1 mut Filter], [f : &!lt_1 mut Filter]), scope(some(U(1)), None, {}, None, [], []), scope(some(U(4)), None, {}, None, [], []), scope(some(U(4)), Some('l), {}, Some({(* f) . iter, (* f) . predicate}), [], [])], point_flow_state({pending_outlives(!lt_1, ?lt_2), pending_outlives(!lt_1, ?lt_3), pending_outlives(?lt_2, !lt_1), pending_outlives(?lt_2, ?lt_4)}, {loan(?lt_2, *(f : &!lt_1 mut Filter) : <&!lt_1 mut Filter as Derefable>::Target . iter[Filter , struct] : u32, mut), loan(?lt_3, *(f : &!lt_1 mut Filter) : <&!lt_1 mut Filter as Derefable>::Target . predicate[Filter , struct] : u32, mut)}, {}), {labeled_flow_state('l, point_flow_state({pending_outlives(!lt_1, ?lt_2), pending_outlives(!lt_1, ?lt_3), pending_outlives(?lt_2, !lt_1), pending_outlives(?lt_2, ?lt_4)}, {loan(?lt_2, *(f : &!lt_1 mut Filter) : <&!lt_1 mut Filter as Derefable>::Target . iter[Filter , struct] : u32, mut)}, {}))}, {}, {pending_outlives(!lt_1, ?lt_2), pending_outlives(!lt_1, ?lt_3), pending_outlives(?lt_2, !lt_1), pending_outlives(?lt_2, ?lt_4)})
 
             the rule "borrow of disjoint places" at (nll.rs) failed because
               condition evaluated to false: `place_disjoint_from_place(&loan.place, &access.place)`
diff --git a/tests/mir_typeck.rs b/tests/mir_typeck.rs
index 1d321d608..76a9eced8 100644
--- a/tests/mir_typeck.rs
+++ b/tests/mir_typeck.rs
@@ -156,8 +156,8 @@ fn if_else_different_return_types() {
             error[E0308]: mismatched types
              --> lib.rs
               |
-            1 | pub fn foo(mut b: bool) -> u32 {
-              |                            --- expected `u32` because of return type
+            1 | pub fn foo(b: bool) -> u32 {
+              |                        --- expected `u32` because of return type
             ...
             5 |         return false;
               |                ^^^^^ expected `u32`, found `bool`
@@ -293,8 +293,8 @@ fn test_let_with_ill_formed_type() {
         error[E0277]: the trait bound `S1: Trait1` is not satisfied
           --> lib.rs
            |
-        13 |     let mut s2: S2<S1>;
-           |                 ^^^^^^ unsatisfied trait bound
+        13 |     let s2: S2<S1>;
+           |             ^^^^^^ unsatisfied trait bound
            |
         help: the trait `Trait1` is not implemented for `S1`
           --> lib.rs
@@ -336,8 +336,8 @@ fn test_call_invalid_fn() {
         error[E0425]: cannot find function `foo` in this scope
          --> lib.rs
           |
-        2 |     let mut v1: u32 = foo(0_u32);
-          |                       ^^^ not found in this scope
+        2 |     let v1: u32 = foo(0_u32);
+          |                   ^^^ not found in this scope
 
         For more information about this error, try `rustc --explain E0425`.
         error: could not compile `Foo` (lib) due to 1 previous error
@@ -367,24 +367,24 @@ fn test_pass_non_subtype_arg() {
             error[E0308]: mismatched types
              --> lib.rs
               |
-            6 |     let mut v0: () = foo(v1);
-              |                      --- ^^ expected `u32`, found `()`
-              |                      |
-              |                      arguments to this function are incorrect
+            6 |     let v0: () = foo(v1);
+              |                  --- ^^ expected `u32`, found `()`
+              |                  |
+              |                  arguments to this function are incorrect
               |
             note: function defined here
              --> lib.rs
               |
-            1 | pub fn foo(mut v1: u32) -> u32 {
-              |        ^^^ -----------
+            1 | pub fn foo(v1: u32) -> u32 {
+              |        ^^^ -------
 
             error[E0308]: mismatched types
              --> lib.rs
               |
-            6 |     let mut v0: () = foo(v1);
-              |                 --   ^^^^^^^ expected `()`, found `u32`
-              |                 |
-              |                 expected due to this
+            6 |     let v0: () = foo(v1);
+              |             --   ^^^^^^^ expected `()`, found `u32`
+              |             |
+              |             expected due to this
 
             For more information about this error, try `rustc --explain E0308`.
             error: could not compile `Foo` (lib) due to 2 previous errors
@@ -456,31 +456,31 @@ fn test_call_generic_fn_wrong_type_with_turbofish() {
             error[E0308]: mismatched types
              --> lib.rs
               |
-            6 |     let mut v0: u32 = identity::<bool>(v1);
-              |                       ---------------- ^^ expected `bool`, found `u32`
-              |                       |
-              |                       arguments to this function are incorrect
+            6 |     let v0: u32 = identity::<bool>(v1);
+              |                   ---------------- ^^ expected `bool`, found `u32`
+              |                   |
+              |                   arguments to this function are incorrect
               |
             help: the return type of this call is `u32` due to the type of the argument passed
              --> lib.rs
               |
-            6 |     let mut v0: u32 = identity::<bool>(v1);
-              |                       ^^^^^^^^^^^^^^^^^--^
-              |                                        |
-              |                                        this argument influences the return type of `identity`
+            6 |     let v0: u32 = identity::<bool>(v1);
+              |                   ^^^^^^^^^^^^^^^^^--^
+              |                                    |
+              |                                    this argument influences the return type of `identity`
             note: function defined here
              --> lib.rs
               |
-            1 | pub fn identity<T00>(mut v1: T00) -> T00 {
-              |        ^^^^^^^^      -----------
+            1 | pub fn identity<T00>(v1: T00) -> T00 {
+              |        ^^^^^^^^      -------
 
             error[E0308]: mismatched types
              --> lib.rs
               |
-            6 |     let mut v0: u32 = identity::<bool>(v1);
-              |                 ---   ^^^^^^^^^^^^^^^^^^^^ expected `u32`, found `bool`
-              |                 |
-              |                 expected due to this
+            6 |     let v0: u32 = identity::<bool>(v1);
+              |             ---   ^^^^^^^^^^^^^^^^^^^^ expected `u32`, found `bool`
+              |             |
+              |             expected due to this
 
             For more information about this error, try `rustc --explain E0308`.
             error: could not compile `Foo` (lib) due to 2 previous errors
@@ -512,18 +512,18 @@ fn test_call_generic_fn_wrong_parameters_number_with_turbofish() {
         error[E0061]: this function takes 1 argument but 2 arguments were supplied
          --> lib.rs
           |
-        6 |     let mut v0: u32 = identity::<u32>(v1, v1);
-          |                       ^^^^^^^^^^^^^^^     -- unexpected argument #2 of type `u32`
+        6 |     let v0: u32 = identity::<u32>(v1, v1);
+          |                   ^^^^^^^^^^^^^^^     -- unexpected argument #2 of type `u32`
           |
         note: function defined here
          --> lib.rs
           |
-        1 | pub fn identity<T00>(mut v1: T00) -> T00 {
+        1 | pub fn identity<T00>(v1: T00) -> T00 {
           |        ^^^^^^^^
         help: remove the extra argument
           |
-        6 -     let mut v0: u32 = identity::<u32>(v1, v1);
-        6 +     let mut v0: u32 = identity::<u32>(v1);
+        6 -     let v0: u32 = identity::<u32>(v1, v1);
+        6 +     let v0: u32 = identity::<u32>(v1);
           |
 
         For more information about this error, try `rustc --explain E0061`.
@@ -551,15 +551,15 @@ fn test_call_generic_fn_wrong_arity() {
         error[E0107]: function takes 1 generic argument but 2 generic arguments were supplied
          --> lib.rs
           |
-        6 |     let mut v0: u32 = identity::<u32, u32>(v1);
-          |                       ^^^^^^^^      ----- help: remove the unnecessary generic argument
-          |                       |
-          |                       expected 1 generic argument
+        6 |     let v0: u32 = identity::<u32, u32>(v1);
+          |                   ^^^^^^^^      ----- help: remove the unnecessary generic argument
+          |                   |
+          |                   expected 1 generic argument
           |
         note: function defined here, with 1 generic parameter: `T00`
          --> lib.rs
           |
-        1 | pub fn identity<T00>(mut v1: T00) -> T00 {
+        1 | pub fn identity<T00>(v1: T00) -> T00 {
           |        ^^^^^^^^ ---
 
         For more information about this error, try `rustc --explain E0107`.
@@ -590,8 +590,8 @@ fn test_incompatible_return_type() {
             error[E0308]: mismatched types
              --> lib.rs
               |
-            1 | pub fn foo(mut v1: ()) -> u32 {
-              |                           --- expected `u32` because of return type
+            1 | pub fn foo(v1: ()) -> u32 {
+              |                       --- expected `u32` because of return type
             2 |     return v1;
               |            ^^ expected `u32`, found `()`
 
@@ -818,8 +818,8 @@ fn test_field_projection_root_non_adt() {
             error: could not compile `Foo` (lib) due to 1 previous error
         "#]])
         .err(expect_test::expect![[r#"
-                the rule "struct field" at (nll.rs) failed because
-                  pattern `(RigidTy { name: RigidName::AdtId(adt_id), parameters }, state)` did not match value `(u32, flow_state([scope(none, None, {}, None, [(v1, u32)], [v1 : u32]), scope(none, None, {}, None, [(v2, Dummy)], [v2 : Dummy])], point_flow_state({}, {}, {}), {}, {}, {}))`"#]])
+            the rule "struct field" at (nll.rs) failed because
+              pattern `(RigidTy { name: RigidName::AdtId(adt_id), parameters }, state)` did not match value `(u32, flow_state([scope(none, None, {}, None, [ v1 : u32], [v1 : u32]), scope(none, None, {}, None, [ v2 : Dummy], [v2 : Dummy])], point_flow_state({}, {}, {}), {}, {}, {}))`"#]])
 }
 
 /// Test the behaviour of initialising the struct with wrong type.
@@ -839,8 +839,8 @@ fn test_struct_wrong_type_in_initialisation() {
             error[E0308]: mismatched types
              --> lib.rs
               |
-            6 |     let mut v2: Dummy = Dummy { value: false };
-              |                                        ^^^^^ expected `u32`, found `bool`
+            6 |     let v2: Dummy = Dummy { value: false };
+              |                                    ^^^^^ expected `u32`, found `bool`
 
             For more information about this error, try `rustc --explain E0308`.
             error: could not compile `Foo` (lib) due to 1 previous error
@@ -867,8 +867,8 @@ fn test_non_adt_ty_for_struct() {
         error[E0422]: cannot find struct, variant or union type `Nonexistent` in this scope
          --> lib.rs
           |
-        2 |     let mut v2: u32 = Nonexistent { value: false };
-          |                       ^^^^^^^^^^^ not found in this scope
+        2 |     let v2: u32 = Nonexistent { value: false };
+          |                   ^^^^^^^^^^^ not found in this scope
 
         For more information about this error, try `rustc --explain E0422`.
         error: could not compile `Foo` (lib) due to 1 previous error