docs: check-rust onboarding discoverability + CotW draft (#1467)

## Summary

MPI session batch (gate + End User / QA / Product perspectives).

- Surface `demos/check-rust` from `demos/README`, GETTING-STARTED, root
README
- Add `inc_mut.rs` linear `let mut` demo; raise `check_rust_demos` floor
to 4
- CotW nomination draft: `docs/launch/crate-of-the-week.md`
- Filed **#1466** for CFG SSA residual (mut inside if/match)

### Gate notes

| Issue | Status |
|-------|--------|
| #1410 #1411 | Human outreach (partially done); not agent-closable |
| #436 | Blocked on upstream cvc5-rs |
| #1396 | Still wait metrics/discussion for big lists |

## Test plan

- [x] `cargo test -p assura --test check_rust_demos --locked`
- [x] `bash scripts/check-rust-demos.sh`
- [x] `assura check-rust demos/check-rust/ok` → 4 verified

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

Author: SebTardif

README.md

@@ -181,8 +181,9 @@ assura check-rust src/
 #   1) co-located {Name}.ir
 #   2) encoded Rust body (arith/if/match/wrapping/bitops/…; see docs/CHECK-RUST-SURFACE.md)
 # Otherwise ensures are body_not_modeled (not silent verified/skipped).
-# User map: docs/CHECK-RUST-SURFACE.md  |  contributor detail: CONTRIBUTING "check-rust body proof"
+# User map: docs/CHECK-RUST-SURFACE.md  |  demos: demos/check-rust/  |  interop: examples/interop-rust/
 assura check-rust src/ --json
+assura check-rust demos/check-rust/ok   # prove demos (expect exit 0)
 
 # Suggest contracts for unannotated functions
 assura check-rust src/ --suggest

crates/assura-cli/tests/check_rust_demos.rs

@@ -20,7 +20,7 @@ fn check_rust_demos_ok_tree_proves() {
     );
     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) >= 3, "{stdout}");
+    assert!(v["verified"].as_u64().unwrap_or(0) >= 4, "{stdout}");
     assert_eq!(v["errors"], 0, "{stdout}");
 }
 

demos/README.md

@@ -31,8 +31,17 @@ assura check demos/heartbleed.assura
 
 # Result-bearing ensures: many shapes synthesize in memory (no hand IR).
 assura check demos/showcase-echo.assura
+
+# Inline Rust annotations (/// @ensures), not .assura files:
+assura check-rust demos/check-rust/ok
+# Intentional counterexample (expect non-zero exit):
+assura check-rust demos/check-rust/fail/clamp_wrong.rs
 ```
 
+Full map: [check-rust/README.md](check-rust/README.md) and
+[docs/CHECK-RUST-SURFACE.md](../docs/CHECK-RUST-SURFACE.md). Interop sample
+crate: [examples/interop-rust](../examples/interop-rust).
+
 Do **not** start with `demos/*-audit.assura` or `defi-audit.assura` unless you
 are studying expected failures.
 

demos/check-rust/README.md

@@ -11,13 +11,15 @@ assura check-rust demos/check-rust/ok
 assura check-rust demos/check-rust/ok/clamp.rs
 assura check-rust demos/check-rust/ok/inc.rs
 assura check-rust demos/check-rust/ok/abs.rs
+assura check-rust demos/check-rust/ok/inc_mut.rs
 ```
 
 | File | Point |
 |------|--------|
 | `ok/clamp.rs` | if/else + `result >= 0` |
 | `ok/inc.rs` | pure `let` + `result == x + 1` |
 | `ok/abs.rs` | `x.abs()` method body |
+| `ok/inc_mut.rs` | linear `let mut` + `+=` |
 
 ## Fail intentionally (expect exit non-zero)
 

demos/check-rust/ok/inc_mut.rs

@@ -0,0 +1,9 @@
+// Demo: straight-line let mut + += (linear SSA fold).
+// Run: assura check-rust demos/check-rust/ok/inc_mut.rs
+
+/// @ensures result == x + 1
+pub fn inc_mut(x: i64) -> i64 {
+    let mut y = x;
+    y += 1;
+    y
+}

docs/GETTING-STARTED.md

@@ -14,7 +14,15 @@ For broader language coverage, see [TUTORIAL.md](TUTORIAL.md) and
 
 After your first successful check, read [What we prove](WHAT-WE-PROVE.md)
 so Verified / Unknown / Counterexample (and vacuous success) are not
-confused. AI-oriented workflow: [AI-AGENTS.md](AI-AGENTS.md).
+confused. AI-oriented workflow: [AI-AGENTS.md](AI-AGENTS.md) and
+[AGENT-LOOP.md](AGENT-LOOP.md).
+
+**Existing Rust with doc-comment contracts:** see
+[CHECK-RUST-SURFACE.md](CHECK-RUST-SURFACE.md) and try:
+
+```bash
+assura check-rust demos/check-rust/ok
+```
 
 ## 1. Install
 

docs/launch/README.md

@@ -89,6 +89,7 @@ Only after: polished gallery (GIF), maker bio, docs URL not confused with assura
 | [../COMPARE.md](../COMPARE.md) | Assura vs Verus / Dafny (includes check-rust) |
 | [../CHECK-RUST-SURFACE.md](../CHECK-RUST-SURFACE.md) | What check-rust can prove on Rust |
 | [../AGENT-LOOP.md](../AGENT-LOOP.md) | Agent JSON branch policy |
+| [crate-of-the-week.md](crate-of-the-week.md) | TWiR CotW nomination draft (next outreach) |
 
 ## Pre-post checklist
 

docs/launch/crate-of-the-week.md

@@ -0,0 +1,22 @@
+# This Week in Rust — Crate of the Week nomination (draft)
+
+Post as a reply on:
+https://users.rust-lang.org/t/crate-of-the-week/2704
+
+Disclosure: I maintain Assura.
+
+```
+I'd like to nominate **assura** (https://crates.io/crates/assura):
+
+Contract-first verification language that uses Z3/CVC5 and emits Rust.
+Also `assura check-rust` for /// @requires / @ensures on existing Rust
+(modeled body surface; fail closed on body_not_modeled). Aimed at AI
+implement loops with structured Verified / Counterexample / Unknown.
+
+Docs: https://assura-lang.github.io/assura/
+Compare (vs Verus/Dafny): https://assura-lang.github.io/assura/COMPARE.html
+```
+
+Do not open a full TWiR Projects/Tooling PR with only a repo link (they
+reject bare crate dumps). Prefer this CotW nomination and/or a long-form
+post first.