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

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

(1) FIXES SEMANTIC BUG in PR #111's 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) PROVES IDEMPOTENCE FOR ALL CASES (including slash-slash) via the
    closure lemma bodyIsFixedPoint:

        stripLineComments (stripLineCommentBody cs)
          = stripLineCommentBody cs

    Proved by mutual induction with the main theorem
    stripLineCommentsIdempotent. The two cases of bodyIsFixedPoint:

      * c == nl: body returns nl :: stripLineComments rest. Outer strip
        on that = nl :: stripLineComments (stripLineComments rest)
                = nl :: stripLineComments rest    [by main IH on rest]
                = body output.                    ✓

      * c /= nl: body returns sp :: stripLineCommentBody rest. Outer
        strip on that = sp :: stripLineComments (stripLineCommentBody rest)
                      = sp :: stripLineCommentBody rest    [by body IH on rest]
                      = body output.              ✓

(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 model would have failed: two comments separated by a
newline, both correctly stripped.

PROOF-NEEDS.md updated:
  - '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: the
    stripIsIdentityOnStrippedBody item 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); issue #114 (the next
Layer-1.0 slice — block + strings + composition + position-
preservation).

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 |