proofs(Layer 1.0): close slash-slash inductive case via mutual recursion (#113) (#119)

## Summary

Closes the open obligation left by PR #111 (issue #113). Two substantive
corrections + the closure proof.

## 1. Semantic-bug fix to PR #111 model

The previous `stripLineCommentBody` returned `nl :: rest` where `rest`
was the ORIGINAL TAIL — meaning only the FIRST comment in the input was
stripped. **The Rust pass at `src/assail/analyzer.rs:931` strips ALL
comments.** New model uses mutual recursion: `stripLineCommentBody`
calls back into `stripLineComments` at each preserved newline, so the
entire input is processed in one pass.

## 2. Closure proof — 

```idris
bodyIsFixedPoint : (cs : List Char) ->
    stripLineComments (stripLineCommentBody cs) = stripLineCommentBody cs
```

Proved by **mutual induction** with `stripLineCommentsIdempotent`. Two
constructor cases:

- `c == nl`: body returns `nl :: stripLineComments rest`. Outer strip on
that = `nl :: stripLineComments (stripLineComments rest)` = `nl ::
stripLineComments rest` by the main IH on `rest`. ✓
- `c /= nl`: body returns `sp :: stripLineCommentBody rest`. Outer strip
on that = `sp :: stripLineComments (stripLineCommentBody rest)` = `sp ::
stripLineCommentBody rest` by the body IH on `rest`. ✓

## 3. No `believe_me` / `assert_total` / holes

Idris2's totality checker validates the mutual recursion: both functions
consume strictly-smaller inputs on each call.

## New sanity check

`sanityTwoComments` specifically exercises the case PR #111's broken
single-comment model would have failed:

```
"//a\n//b" → "   \n   " (both comments stripped, newline preserved)
```

## PROOF-NEEDS.md changes

- 'Completed Proofs' row for `Stripping.idr` updated to reflect the
multi-comment correction + slash-slash Qed.
- 'What Still Needs Proving' Layer-1.0 row collapsed:
`stripIsIdentityOnStrippedBody` is now Qed; only the block / strings /
composition / position-preservation slice remains, recorded under issue
#114.

## Refs

- PROOF-PROGRAMME.md row 1 (Layer 1.0)
- PR #111 (the foundation this closes)
- Issue #113 (the obligation — closes)
- Issue #114 (the next Layer-1.0 slice — remains open)

Author: hyperpolymath

PROOF-NEEDS.md

@@ -2,7 +2,7 @@
 
 ## Current State
 
-- **src/abi/*.idr**: 4 files — `Types.idr`, `PatternCompleteness.idr` (PA1 ✅ 2026-04-11), `ClassificationSoundness.idr` (PA2 ✅ 2026-04-11), `Stripping.idr` (PROOF-PROGRAMME Layer 1.0 partial — base cases proved, slash-slash inductive open)
+- **src/abi/*.idr**: 4 files — `Types.idr`, `PatternCompleteness.idr` (PA1 ✅ 2026-04-11), `ClassificationSoundness.idr` (PA2 ✅ 2026-04-11), `Stripping.idr` (PROOF-PROGRAMME Layer 1.0 line-comment slice ✅ 2026-06-02 — multi-comment semantics + slash-slash closure both Qed via mutual-recursive `bodyIsFixedPoint`)
 - **Dangerous patterns**: 0 in own code (3 references are in the analyzer that DETECTS believe_me in other repos); 282 `unwrap()` calls
 - **LOC**: ~31,700 (Rust)
 - **ABI layer**: Idris2 with completeness + soundness proofs + Layer-1.0 stripping foundation
@@ -13,15 +13,13 @@
 |-------|------|---------------|
 | PA1 Pattern detection completeness | `src/abi/PatternCompleteness.idr` | All 49 `Lang` constructors have an analyzer; all 20 `WPCategory` constructors have at least one detector; cross-language checks applied unconditionally to all languages. `completeScanForAll` is the top-level theorem. |
 | PA2 Classification soundness | `src/abi/ClassificationSoundness.idr` | Severity (Low/Medium/High/Critical) is totally ordered (`LTE`); `maxSeverity` is commutative and idempotent; numeric ABI encoding preserves the ordering. |
-| Layer 1.0 partial — stripping foundation | `src/abi/Stripping.idr` | (a) `stripLineCommentBody` always produces `IsStrippedBody`-shaped output (Qed); (b) base cases of `stripLineCommentsIdempotent`: empty input + non-`/`-headed input (Qed). Three concrete sanity-check theorems. Open: the slash-slash inductive case below. |
+| Layer 1.0 line-comment idempotence | `src/abi/Stripping.idr` | **2026-06-02 close-out (issue #113)**: corrects PR #111's single-comment model to multi-comment via mutual recursion (`stripLineComments ↔ stripLineCommentBody` — body calls back into main after each preserved newline). Qed-closes `stripLineCommentsIdempotent` for ALL cases including the slash-slash inductive via the load-bearing `bodyIsFixedPoint` lemma proved by mutual induction with the main theorem. 7 sanity-check theorems including the two-comments-on-different-lines case PR #111 silently mis-stripped. |
 
 ## What Still Needs Proving
 
 | Component | What | Why |
 |-----------|------|-----|
-| **Layer 1.0 — stripIsIdentityOnStrippedBody (slash-slash closure)** | `stripLineComments` applied to any `IsStrippedBody xs` returns `xs` unchanged | Required to close the `'/' :: '/' :: rest` case of `stripLineCommentsIdempotent`. Without it, all Layer-1.1..1.25 per-category proofs would have to re-verify that comments don't re-introduce themselves. |
-| **Layer 1.0 — stripBlockComments + Strings** | Block-comment (`/* */`) and string-literal (`"..."`) strippers with the same shape lemma + idempotence. Composition theorem. | Three slices: `Stripping_Block.idr`, `Stripping_Strings.idr`, `Stripping_Composition.idr`. |
-| **Layer 1.0 — position preservation** | For every index `i` where `cs[i]` is OUTSIDE every comment/string, `strip cs ! i = cs[i]` | Justifies the analyzer reporting locations against the stripped view as if they were original source. |
+| **Layer 1.0 — stripBlockComments + Strings + Composition + Position-Preservation** (issue #114) | Block-comment (`/* */`) and string-literal (`"..."`) strippers with same mutual-recursive shape; composition theorem proving the full pipeline is idempotent given each component is; position-preservation theorem justifying analyzer location-reporting against the stripped view as if it were original-source. | Four slices: `Stripping_Block.idr`, `Stripping_Strings.idr`, `Stripping_Composition.idr`, `Stripping_PositionPreservation.idr`. |
 | Bridge reachability soundness | Reachability analysis is sound (no reachable dep wrongly classified as phantom) | Unreachable code marked reachable wastes effort; reachable missed = security gap |
 | Attestation chain unforgeability | Intent/evidence/seal triple is cryptographically bound; tampering detectable | Tampered attestations break trust chain |
 | Kanren taint analysis | Taint propagation tracks all tainted data flows | Missed taint flow means missed vulnerability |