check-rust: linear SSA for let mut reassignment (#1465)

## Summary

Implements straight-line `let mut` reassignment encoding for `assura
check-rust` (the residual called out after epic #1456).

### Why it was skipped in #1459 / PR #1464

- #1459 AC allowed **encode *or* residual rewrite hints**; demos closed
without needing `+=`
- Linear SSA is still a real encoder change with soundness edges
(CFG-shaped mutation)
- Epic batch prioritized demos/docs/interop over deeper body encode

### What this does

- Extend `fold_simple_lets` to apply `x = e` and `x += e` (and other
assign-ops) on a **straight-line** path
- Still BNM for assigns inside `if` / `match` / loops (no full CFG SSA)
- Unit + integration tests; docs residual tables updated

### Not in scope

- Full SSA / phi nodes / loop mutation
- Verus-level borrow modeling

## Test plan

- [x] `cargo test -p assura --lib --locked let_mut_`
- [x] `cargo test -p assura --test check_rust_body_ir --locked let_mut`
- [x] Manual: `assura check-rust` on `let mut y = x; y += 1; y` with
`@ensures result == x + 1` → verified

---------

Signed-off-by: Sebastien Tardif <sebtardif@ncf.ca>

Author: SebTardif

CONTRIBUTING.md

@@ -213,12 +213,12 @@ gaps):
 |-------|--------|
 | Panic paths (`/0`, `%0`, `/`/`%` with zero-including path divisors, `is_multiple_of(0)`, literal `0.ilog2()`) | Soundness: do not encode panic as free SMT div/mod |
 | `rem_euclid`/`div_euclid`/`div_ceil`/`next_multiple_of` with non-positive or zero-including divisors | Same soundness rule; use a positive const or `NonZeroU*` param |
-| `let mut y = x; y += 1; y` (reassignment) | Pure `let mut` fold only (#1343); mutation/SSA not modeled; rewrite to pure lets |
+| Assignments inside `if`/`match`/loops (not linear) | Linear SSA fold only; straight-line `let mut y = x; y += 1; y` is modeled |
 | Bare `checked_*` / `overflowing_*` without peel (Option or `(T, bool)` return as the result type) | Intentional: peel with `.unwrap_or` / `.unwrap_or_default` / `.is_some()` / `.is_none()` / `.0` / `.1`; full Option/tuple values are not IR types |
 
-CLI prints these rewrite hints on `body_not_modeled` exit (pointing at
-`docs/CHECK-RUST-SURFACE.md`). Full SSA mutation encode is tracked under
-the check-rust competitiveness epic, not required for residual honesty.
+CLI prints rewrite hints on `body_not_modeled` exit (pointing at
+`docs/CHECK-RUST-SURFACE.md`). Straight-line `let mut` reassignment is
+folded in `fold_simple_lets` (linear SSA); CFG-shaped mutation remains residual.
 
 Signed path-param `reverse_bits`/`swap_bytes`/`count_*`/`trailing_*`/`leading_*`
 use synthetic `2^64` bit-pattern map for full i64 (same as `count_ones`).

crates/assura-cli/src/check/check_rust.rs

@@ -496,10 +496,10 @@ pub(crate) fn run_check_rust(
         } else if total_body_not_modeled > 0 {
             eprintln!(
                 "{total_body_not_modeled} item(s) not proven against the Rust body \
-                 (body_not_modeled). Rewrite hints: prefer pure lets (no mut \
-                 reassignment); peel checked_*/overflowing_* with .unwrap_or / \
-                 .is_some() / .0; avoid panic div/mod. Or add co-located \
-                 {{Name}}.ir. Surface map: docs/CHECK-RUST-SURFACE.md"
+                 (body_not_modeled). Rewrite hints: keep mutation on a straight \
+                 line (no assign inside if/match/loop); peel checked_*/overflowing_* \
+                 with .unwrap_or / .is_some() / .0; avoid panic div/mod. Or add \
+                 co-located {{Name}}.ir. Surface map: docs/CHECK-RUST-SURFACE.md"
             );
             process::exit(1);
         } else if total_verified == 0 {

crates/assura-cli/src/check/rust_body_ir/mod.rs

@@ -102,40 +102,58 @@ fn body_return_from_block(block: &syn::Block) -> Option<String> {
     }
 }
 
-/// Fold `let a = e1; let b = a + 1; b` (or `return b`) into a single expression.
-/// Only simple `Pat::Ident` bindings without type ascriptions; `mut` is allowed
-/// when the binding is never reassigned (pure fold). Final stmt is
-/// path/return/expression that may reference prior binds.
+/// Fold simple statement sequences into a single expression via substitution
+/// (linear SSA, not a full CFG).
+///
+/// Supported:
+/// - `let a = e1; let b = a + 1; b` (pure lets; `mut` ok without reassignment)
+/// - `let mut y = x; y += 1; y` / `y = y + 1; y` (linear reassignment)
+/// - Final stmt: path / return / expression referencing prior binds
+///
+/// Not supported (returns None → body_not_modeled): assignments inside
+/// `if`/`match`/loops, multi-LHS patterns, type ascriptions on lets, bare
+/// mid-block expressions that are not assignments.
 fn fold_simple_lets(stmts: &[syn::Stmt]) -> Option<syn::Expr> {
     if stmts.len() < 2 {
         return None;
     }
-    // split_last -> (last_elem, prefix)
-    let (last, binds) = stmts.split_last()?;
+    let (last, prefix) = stmts.split_last()?;
+    // name → current expression (already substituted for earlier names)
     let mut env: Vec<(String, syn::Expr)> = Vec::new();
-    for stmt in binds {
-        let syn::Stmt::Local(local) = stmt else {
-            return None;
-        };
-        // Reject any later assignment to mut bindings (fold is pure substitute).
-        let name = match &local.pat {
-            syn::Pat::Ident(id) if id.by_ref.is_none() && id.subpat.is_none() => {
-                id.ident.to_string()
+    for stmt in prefix {
+        match stmt {
+            syn::Stmt::Local(local) => {
+                let name = match &local.pat {
+                    syn::Pat::Ident(id) if id.by_ref.is_none() && id.subpat.is_none() => {
+                        id.ident.to_string()
+                    }
+                    _ => return None,
+                };
+                let init = local.init.as_ref()?;
+                if init.diverge.is_some() {
+                    return None;
+                }
+                let mut init_expr = (*init.expr).clone();
+                for (n, e) in env.iter().rev() {
+                    init_expr = substitute_ident_expr(init_expr, n, e);
+                }
+                if let Some((_, slot)) = env.iter_mut().find(|(n, _)| n == &name) {
+                    *slot = init_expr;
+                } else {
+                    env.push((name, init_expr));
+                }
+            }
+            syn::Stmt::Expr(expr, _) => {
+                apply_linear_assignment(expr, &mut env)?;
             }
             _ => return None,
-        };
-        let init = local.init.as_ref()?;
-        if init.diverge.is_some() {
-            return None;
         }
-        env.push((name, (*init.expr).clone()));
     }
     let mut final_expr: syn::Expr = match last {
         syn::Stmt::Expr(syn::Expr::Return(ret), _) => (*ret.expr.as_ref()?.as_ref()).clone(),
         syn::Stmt::Expr(e, _) => e.clone(),
         _ => return None,
     };
-    // Substitute later binds first so earlier names expand fully.
     for (name, init) in env.into_iter().rev() {
         final_expr = substitute_ident_expr(final_expr, &name, &init);
     }
@@ -144,6 +162,67 @@ fn fold_simple_lets(stmts: &[syn::Stmt]) -> Option<syn::Expr> {
     Some(distribute_if_binary(paren_if_match_operands(final_expr)))
 }
 
+/// Apply `x = e` or `x += e` (etc.) to the linear env. Name must already be bound.
+fn apply_linear_assignment(expr: &syn::Expr, env: &mut [(String, syn::Expr)]) -> Option<()> {
+    match expr {
+        syn::Expr::Assign(a) => {
+            let name = expr_simple_ident_name(&a.left)?;
+            let mut rhs = (*a.right).clone();
+            for (n, e) in env.iter().rev() {
+                rhs = substitute_ident_expr(rhs, n, e);
+            }
+            let (_, slot) = env.iter_mut().find(|(n, _)| n == &name)?;
+            *slot = rhs;
+            Some(())
+        }
+        syn::Expr::Binary(b) => {
+            let plain = assign_op_to_bin_op(b.op)?;
+            let name = expr_simple_ident_name(&b.left)?;
+            let mut rhs = (*b.right).clone();
+            for (n, e) in env.iter().rev() {
+                rhs = substitute_ident_expr(rhs, n, e);
+            }
+            let cur = env.iter().find(|(n, _)| n == &name)?.1.clone();
+            let combined = syn::Expr::Binary(syn::ExprBinary {
+                attrs: Vec::new(),
+                left: Box::new(cur),
+                op: plain,
+                right: Box::new(rhs),
+            });
+            let (_, slot) = env.iter_mut().find(|(n, _)| n == &name)?;
+            *slot = combined;
+            Some(())
+        }
+        _ => None,
+    }
+}
+
+fn expr_simple_ident_name(expr: &syn::Expr) -> Option<String> {
+    match expr {
+        syn::Expr::Path(p) if p.path.segments.len() == 1 && p.qself.is_none() => {
+            Some(p.path.segments[0].ident.to_string())
+        }
+        syn::Expr::Paren(p) => expr_simple_ident_name(&p.expr),
+        _ => None,
+    }
+}
+
+fn assign_op_to_bin_op(op: syn::BinOp) -> Option<syn::BinOp> {
+    match op {
+        syn::BinOp::AddAssign(_) => Some(syn::parse_quote!(+)),
+        syn::BinOp::SubAssign(_) => Some(syn::parse_quote!(-)),
+        syn::BinOp::MulAssign(_) => Some(syn::parse_quote!(*)),
+        syn::BinOp::DivAssign(_) => Some(syn::parse_quote!(/)),
+        syn::BinOp::RemAssign(_) => Some(syn::parse_quote!(%)),
+        syn::BinOp::BitXorAssign(_) => Some(syn::parse_quote!(^)),
+        syn::BinOp::BitAndAssign(_) => Some(syn::parse_quote!(&)),
+        syn::BinOp::BitOrAssign(_) => Some(syn::parse_quote!(|)),
+        syn::BinOp::ShlAssign(_) => Some(syn::parse_quote!(<<)),
+        syn::BinOp::ShrAssign(_) => Some(syn::parse_quote!(>>)),
+        _ => None,
+    }
+}
+
 /// Lift if/match out of binary/unary/method so multi-block encode can fire.
 /// `(if c { a } else { b }) ⊕ r` → `if c { a ⊕ r } else { b ⊕ r }` (and right/match/unary).
 fn distribute_if_binary(expr: syn::Expr) -> syn::Expr {

crates/assura-cli/src/check/rust_body_ir/tests.rs

@@ -2071,6 +2071,52 @@ fn f(x: i64) -> i64 {
     assert!(ir.contains("arith add"), "body={body}\nir={ir}");
 }
 
+#[test]
+fn let_mut_add_assign_encodes() {
+    let src = r#"
+fn f(x: i64) -> i64 {
+    let mut y = x;
+    y += 1;
+    y
+}
+"#;
+    let body = extract_body_return(src, "f").expect("extract mut+=");
+    let ir = try_ir_from_rust_body("F", &px(), Some("i64"), &body).expect("encode");
+    assert!(ir.contains("arith add"), "body={body}\nir={ir}");
+}
+
+#[test]
+fn let_mut_plain_reassign_encodes() {
+    let src = r#"
+fn f(x: i64) -> i64 {
+    let mut y = x;
+    y = y + 1;
+    y
+}
+"#;
+    let body = extract_body_return(src, "f").expect("extract mut=");
+    let ir = try_ir_from_rust_body("F", &px(), Some("i64"), &body).expect("encode");
+    assert!(ir.contains("arith add"), "body={body}\nir={ir}");
+}
+
+#[test]
+fn let_mut_reassign_inside_if_still_bnm() {
+    // Control-flow mid-block is out of linear SSA scope.
+    let src = r#"
+fn f(x: i64) -> i64 {
+    let mut y = x;
+    if x > 0 {
+        y += 1;
+    }
+    y
+}
+"#;
+    assert!(
+        extract_body_return(src, "f").is_none(),
+        "if-with-assign should not fold"
+    );
+}
+
 #[test]
 fn checked_neg_unwrap_or_encodes() {
     let ir = try_ir_from_rust_body("N", &px(), Some("i64"), "x.checked_neg().unwrap_or(0)")

crates/assura-cli/tests/check_rust_body_ir.rs

@@ -2015,6 +2015,54 @@ fn f(x: i64) -> i64 {
     assert_eq!(v["body_not_modeled"], 0, "{stdout}");
 }
 
+/// Straight-line `let mut` + `+=` / `=` reassignment (linear SSA fold).
+#[test]
+fn check_rust_encodes_let_mut_reassign() {
+    let tmp = unique_temp("assura_check_rust_let_mut_re");
+    let _ = std::fs::remove_dir_all(&tmp);
+    std::fs::create_dir_all(&tmp).unwrap();
+    std::fs::write(
+        tmp.join("ok.rs"),
+        r#"
+/// @ensures result == x + 1
+fn f(x: i64) -> i64 {
+    let mut y = x;
+    y += 1;
+    y
+}
+"#,
+    )
+    .unwrap();
+    let out = Command::new(assura_bin())
+        .args(["check-rust", "--json", tmp.join("ok.rs").to_str().unwrap()])
+        .output()
+        .unwrap();
+    let stdout = String::from_utf8_lossy(&out.stdout);
+    assert!(out.status.success(), "mut+= should prove: {stdout}");
+    let v: serde_json::Value = serde_json::from_str(&stdout).expect("json");
+    assert_eq!(v["body_not_modeled"], 0, "{stdout}");
+    assert!(v["verified"].as_u64().unwrap_or(0) >= 1, "{stdout}");
+
+    std::fs::write(
+        tmp.join("ok2.rs"),
+        r#"
+/// @ensures result == x + 1
+fn g(x: i64) -> i64 {
+    let mut y = x;
+    y = y + 1;
+    y
+}
+"#,
+    )
+    .unwrap();
+    let out = Command::new(assura_bin())
+        .args(["check-rust", "--json", tmp.join("ok2.rs").to_str().unwrap()])
+        .output()
+        .unwrap();
+    let stdout = String::from_utf8_lossy(&out.stdout);
+    assert!(out.status.success(), "mut= should prove: {stdout}");
+}
+
 /// checked_neg().unwrap_or encodes (MIN → alt).
 #[test]
 fn check_rust_encodes_checked_neg_unwrap() {

docs/CHECK-RUST-SURFACE.md

@@ -55,7 +55,7 @@ counterexample. Width limits are typically **through 64 bits** unless noted.
 | Area | Examples |
 |------|----------|
 | Control | `if` / `else`, `match` |
-| Binding | Multi-`let`, pure `let mut` (no reassignment), `let y = if/match …; y + n` |
+| Binding | Multi-`let`, pure `let mut`, linear reassignment (`y += 1`, `y = y + 1` on a straight-line path), `let y = if/match …; y + n` |
 | Composition | if/match over binary ops (both sides), method-on-if receivers, cast-of-if |
 | References | Peel outer `&` / `*` layers |
 
@@ -99,7 +99,7 @@ reports `body_not_modeled` and exits **1**. They are not silent Verified.
 
 | Shape | Why / what to do |
 |-------|------------------|
-| `let mut y = x; y += 1; y` (reassignment) | Pure `let mut` fold only; mutation/SSA not modeled. Prefer pure expressions or immutable lets. |
+| Assignments inside `if` / `match` / loops | Linear SSA only (no CFG). Rewrite to pure expressions or branch-local values. |
 | Bare `checked_*` / `overflowing_*` as the **return type** (full `Option` / `(T, bool)`) | Peel: `.unwrap_or` / `.unwrap_or_default` / `.is_some()` / `.is_none()` / `.0` / `.1`. Full Option/tuple values are not IR result types. |
 | Bodies outside Bucket A (I/O, arbitrary methods, complex ADTs, …) | Supply a co-located `{Name}.ir`, simplify the body, or keep contracts on `.assura` + generated code. |