Support non-indented comments in Anneal annotations?

## Context
Currently, Anneal enforces strict indentation for all lines within a [anneal](cci:1://file:///usr/local/google/home/joshlf/workspace/zerocopy/hermes/tools/hermes/src/parse/mod.rs:499:8-507:9) block relative to the first keyword. This creates a poor user experience for comments, which often naturally appear at the same indentation level as keywords (e.g., when temporarily commenting out a [requires](cci:1://file:///usr/local/google/home/joshlf/workspace/zerocopy/hermes/tools/hermes/src/generate.rs:800:4-817:5) clause) or even unindented (e.g., commenting out a whole block).

## Proposed Change
Modify the Anneal parser ([src/parse/attr.rs](cci:7://file:///usr/local/google/home/joshlf/workspace/zerocopy/hermes/tools/hermes/src/parse/attr.rs:0:0-0:0)) to **exempt** lines starting with `--`, `/-`, or `/--` from indentation checks. These lines should be treated as "transparent" or "attached" flexibility, allowing them to appear anywhere without triggering an "Invalid indentation" error.

## Edge Cases & Subtleties

### 1. Attribution (Preceding Block)
* **Issue:** A comment appearing at the same indentation level as a keyword (e.g., `ensures`) is ambiguous regarding which section it belongs to if purely based on indentation/keywords.
* **Resolution:** Comments should always attach to the **current active section** (the preceding keyword) effectively "falling through" to the content accumulated so far.
* **Example:**
```lean
requires x > 0
-- This should attach to `requires`, not float or start a new mysterious block
ensures y > 0
```

### 2. Baseline Indentation
* **Issue:** If the *first* line of a spec body is a comment, it must not mistakenly establish the `baseline_indent` for the rest of the block.
* **Resolution:** `baseline_indent` must only be established by the first **non-comment** line (typically the first keyword). Comments appearing before the first keyword should either be ignored for indentation calculation or treated as part of the "header".

### 3. Block Comments (`/- ... -/`)
* **Issue:** Lean block comments can span multiple lines.
* **Resolution:**
* **Simple:** Exempt any line starting with `/-` or `/--`.
* **Robust:** Ideally, track state to exempt *all* lines between `/-` and `-/-`, but in practice, simply exempting lines that *start* with comment tokens covers 99% of use cases (including single-line block comments) and is likely sufficient for Anneal's line-based parser.

### 4. "Empty" Proof Blocks
* **Issue:** Anneal automatically generates `by sorry` if a [proof](cci:1://file:///usr/local/google/home/joshlf/workspace/zerocopy/hermes/tools/hermes/src/generate.rs:1147:4-1162:5) block is empty. If a [proof](cci:1://file:///usr/local/google/home/joshlf/workspace/zerocopy/hermes/tools/hermes/src/generate.rs:1147:4-1162:5) block contains *only* comments, `lines.is_empty()` will be false, preventing the automatic `sorry`.
* **Consequence:** Generates `by \n -- comment`, which is a Lean syntax error (expected tactic).
* **Resolution:** [generate.rs](cci:7://file:///usr/local/google/home/joshlf/workspace/zerocopy/hermes/tools/hermes/src/generate.rs:0:0-0:0) (or the parsing step) must filter out comment-only lines when determining if a block is "semantically empty" to correctly trigger the fallback `sorry` generation.

### 5. Operator False Positives
* **Issue:** `-` is a subtraction/negation operator.
* **Resolution:** The check must be strict: `line.trim().starts_with("--")`.
* `x - - y` (valid code) does not start with `--` after trimming (unless `x` is missing, which is already invalid).
* Double-check that we don't accidentally match `---` or other sequences if they aren't comments (though `---` is usually a comment header).

### 6. Interaction with Multi-line Code (Strings)
* **Issue:** A multi-line string in Lean might contain a line starting with `--`.
```lean
let s := "
-- is this a comment?
"
```
* **Resolution:** It is **safe and correct** to exempt these from indentation checks. Anneal passes content verbatim to Lean.
* If Anneal treats it as a "comment" (exempt from indentation), it passes the line to Lean.
* Lean parses it as part of the string.
* **Result:** Correct behavior. The exemption makes the parser *more permissive* for strings, which is desirable.

### 7. Unindented Comments
* **Issue:** Users often paste comments at column 0 or comment out large blocks by prefixing `--` without adjusting indentation.
* **Resolution:** Explicitly allow comments to have **less** indentation than the baseline.