docs: clarify check-rust vs Verus on COMPARE page (#1455)

## Summary

- Update [docs/COMPARE.md](docs/COMPARE.md) so Verus comparison matches
product reality: Assura supports **inline** `/// @requires` / `@ensures`
via `assura check-rust`, not only `.assura` files.
- Keep the honest split: Verus is still preferred for deep borrow-aware
proofs of existing Rust; Assura `check-rust` has a partial body model
and fails closed with `body_not_modeled`.

## Why

Launch messaging said "not Verus-in-place" so strongly that it sounded
like Assura cannot annotate existing Rust at all. That is wrong and
confuses HN/Reddit answers.

## Test plan

- [x] Read COMPARE.md for accuracy against README `check-rust` and
CONTRIBUTING body-proof section
- [ ] Docs site rebuild (mdBook) on merge / CI

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

Author: SebTardif

docs/COMPARE.md

@@ -11,27 +11,57 @@ just Dafny / Verus / Liquid Haskell / better unit tests?*
 
 | | Assura | Dafny | Verus | Liquid Haskell | Unit / property tests |
 |--|--------|-------|-------|----------------|------------------------|
-| **Primary surface** | Dedicated `.assura` contracts | Dafny language | Annotations on Rust | Liquid types / refinements on Haskell | Tests in host language |
+| **Primary surface** | `.assura` contracts; optional `/// @requires` / `@ensures` on Rust via `check-rust` | Dafny language | Specs and proofs as annotations on Rust | Liquid types / refinements on Haskell | Tests in host language |
 | **Implementation author** | Often AI (IR / auto-implement / check-rust) | Human (or AI as ordinary code) | Human-written Rust | Human-written Haskell | Human or AI |
 | **Proof backend** | Z3 / CVC5 via Assura pipeline | Boogie / Z3 | VIR / Z3 | Liquid Fixpoint / SMT | None (sampling) |
 | **Default emit** | Rust source (`rustc` / WASM) | C#, Go, JS, Java, Python, … | Stays Rust | Stays Haskell | N/A |
 | **AI agent loop** | First-class (MCP, check-rust, auto-implement) | Possible but not the product shape | Possible | Possible | Common, no proof |
-| **What "success" means** | No counterexample for modeled clauses; layers 0–2 | Verified method / module | Verified function | Type-checked refinements | Tests green |
+| **What "success" means** | No counterexample for modeled clauses; layers 0–2; unmodeled Rust bodies are `body_not_modeled`, not silent success | Verified method / module | Verified function under Verus's Rust model | Type-checked refinements | Tests green |
+
+## Assura on existing Rust vs Verus
+
+Assura can annotate **existing Rust** without a separate `.assura` file per
+function: put contracts in doc comments and run `assura check-rust`
+(human or LLM can add the annotations). Example shape:
+
+```rust
+/// @requires x >= 0
+/// @ensures result >= 0
+pub fn abs_i64(x: i64) -> i64 { /* ... */ }
+```
+
+That is real, but it is **not** the same product as Verus:
+
+| | Assura `check-rust` | Verus |
+|--|---------------------|-------|
+| **How you attach specs** | `/// @requires` / `@ensures` (and related) on Rust items | Verus attributes / proof blocks in Rust |
+| **What is modeled** | Growing but intentional subset of bodies (arith, control flow, wrapping/bitops, …) or a co-located `.ir` sidecar | Deep model of Rust (including ownership/borrow patterns Verus supports) |
+| **Unmodeled code** | Reports `body_not_modeled` (not treated as verified) | Outside Verus's supported surface, or unfinished proof, as Verus defines |
+| **Primary story** | Contracts first; AI loop; also annotate-and-check | Prove the Rust you keep writing in place |
+
+**Prefer Verus** when the goal is fine-grained, borrow-aware proofs of
+**existing Rust crates** as the long-term source of truth.
+
+**Prefer Assura** when you want a separate contract language and/or an
+agent-friendly check loop, including optional inline annotations on Rust
+with honest body modeling limits (see [What we prove](WHAT-WE-PROVE.md)
+and CONTRIBUTING "check-rust body proof").
 
 ## When Assura is a better fit
 
 - You want **specs separate from host-language syntax** so agents and humans
-  share a stable contract surface.
+  share a stable contract surface (`.assura`), or light `/// @…` contracts
+  on Rust via `check-rust`.
 - You care about an **AI write → SMT check → fix** loop with structured
-  results (counterexample vs unknown vs verified).
-- You want **Rust as the ship format** without requiring the implementation
-  to be authored as verified Rust-in-place first.
+  results (counterexample vs unknown vs verified vs body_not_modeled).
+- You want **Rust as the ship format** without requiring Verus-style
+  verified Rust-in-place as the only workflow.
 
 ## When another tool is a better fit
 
 | Need | Prefer |
 |------|--------|
-| Verify **existing Rust** in place with fine-grained borrow-aware proofs | [Verus](https://github.com/verus-lang/verus) |
+| Deep **borrow-aware** proofs of existing Rust as the main workflow | [Verus](https://github.com/verus-lang/verus) |
 | Mature multi-target verified language with large libraries | [Dafny](https://dafny.org/) |
 | Refinement types inside Haskell | [Liquid Haskell](https://ucsd-progsys.github.io/liquidhaskell/) |
 | Fast feedback without SMT, or non-modeled effects | Property tests / fuzzing (still useful *with* Assura) |
@@ -42,7 +72,10 @@ Assura does **not** claim:
 
 - That every clause is always decided (see [What we prove](WHAT-WE-PROVE.md)).
 - That it replaces human review for product requirements.
-- That it is a drop-in Verus substitute for verifying arbitrary Rust crates.
+- That `check-rust` is a drop-in Verus substitute for verifying arbitrary
+  Rust crates (partial body model; unmodeled paths fail closed as
+  `body_not_modeled`).
+- That every green check means full mathematical coverage of all features.
 
 For competitive research notes (internal depth), see
 [INVESTIGATION.md](INVESTIGATION.md). For a short public pitch, start with