Add mut declarations and mutable-place checks

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");
                 }
             }

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,

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(

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))
         )
 
         (

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)
     }

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,

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,
 }