Add `mut` declarations and mutable-place checks

[nikomatsakis]

Description

Currently, formality doesn't distinguish between let x and let mut x. All variables are implicitly mutable. We need to:

1. Add mut as an optional annotation on let declarations in the grammar
2. Add "mut place" checks into the borrow checker rules — when performing a mutable access (assignment, &mut borrow), verify that the target place is mutable:
   • A local variable and the data it owns is mut if declared let mut x
   • When passing through a deref, deref of & is not mut, but deref of &mut is

Mentoring notes

Where to start:

1. Grammar: Look at crates/formality-rust/src/grammar/expr/mod.rs for how local variable declarations work. You'll need to add a Mutability field (or just a bool) to the let statement representation.

2. Borrow checker: Look at crates/formality-rust/src/check/borrow_check/ — when an assignment or &mut borrow is processed, add a check that the target local was declared mut.

3. Existing tests: The existing borrow check tests in tests/borrowck.rs will need updating — they'll need mut annotations where variables are mutated.

Steps:

1. Add Mutability enum (Mut/Not) to the grammar for local declarations
2. Thread it through parsing/lowering
3. Create a judgment prove_place_is_mut(place) => () with rules:
   • A local variable x is mut if declared let mut x
   • A deref of &mut T is mut
   • A deref of &T is NOT mut
   • A field access place.field is mut if place is mut
4. In the borrow checker, when you see a write to a place or a &mut borrow of a place, call prove_place_is_mut
5. Add test cases: mutable access to non-mut variable (should error), mutable access to mut variable (should pass), write through &mut (should pass), write through & (should error)
6. Update all existing tests that mutate variables to use mut

[bit-aloo]

@rustbot claim