proofs(Layer 1.0 follow-up): block-comment + string-literal stripping + composition + position-preservation #114

Context

PR #111 covered LINE-comment stripping foundation. Layer 1.0 has three more slices before the foundation is complete:

Modules to ship (each its own PR)

src/abi/Stripping_Block.idr — block-comment (/* … */) stripping

Mirror the line-comment proof structure:

• Total stripBlockCommentBody + stripBlockComments functions matching src/assail/analyzer.rs.
• Shape lemma analogous to IsStrippedBody (block bodies are spaces terminated by */, not by \n).
• Idempotence theorem closing all cases.

Note: Rust's strip_proof_comments does NOT recurse into nested blocks — mirror that semantics. /* outer /* inner */ tail \*/ strips to the first */; the trailing tail */ is preserved.

src/abi/Stripping_Strings.idr — "…" literals with escape handling

Same shape:

• stripStringBody walks until unescaped closing ", replacing chars with sp.
• Shape lemma: output is sp* terminated by " + arbitrary tail.
• Idempotence.

Escape semantics: \" inside a string does NOT terminate. \\" does (the second ` literal). Mirror Rust's behaviour exactly.

src/abi/Stripping_Composition.idr — composition theorem

Given the three component theorems, prove the full preprocessing pipeline is idempotent:

strip : List Char -> List Char
strip = stripLineComments . stripBlockComments . stripStrings

stripIdempotent : (cs : List Char) -> strip (strip cs) = strip cs

This requires showing that each component's output is a fixed point of the others — i.e., stripLineComments applied to stripStrings-output doesn't introduce new // (and similar for the other pairings).

src/abi/Stripping_PositionPreservation.idr — non-token position identity

For every index i where cs[i] is OUTSIDE every comment/string region (per a separate OutsideRegion predicate), prove strip cs ! i = cs[i]. Justifies the analyzer reporting locations against the stripped view as if they were original-source locations.

Acceptance

Per slice: no believe_me / assert_total / holes. PROOF-NEEDS.md rows for each module move to 'Completed Proofs'.

Refs

• PROOF-PROGRAMME.md row 1 (Layer 1.0)
• PR proofs(Layer 1.0): Idris2 stripping foundation — base cases + shape lemma #111 (line-comment foundation)
• src/assail/analyzer.rs:931 strip_proof_comments (the Rust pass being mechanised)