Skip to content

Commit ad1faf6

Browse files
hyperpolymathhyperpolymath
authored
proofs(Layer 1.0): Idris2 stripping foundation — base cases + shape lemma (#111)
## Summary PROOF-PROGRAMME row 1 — Layer 1.0 "comment/string-strip idempotence + token preservation". This is the FIRST proof slice on the path from PA1+PA2 (dispatch completeness + severity ordering) to end-to-end Surface-layer soundness. Establishes the foundation lemma every per-category proof will depend on: the analyzer's comment-stripping pass is a fixed point. ## What this PR Qed-closes (No `believe_me`, `assert_total`, or `?` holes.) 1. Total Idris2 definitions for `stripLineCommentBody` + `stripLineComments` — mirrors the Rust analyzer's pass at `src/assail/analyzer.rs:931 strip_proof_comments`. 2. `IsStrippedBody` shape predicate — characterises post-marker body output (sequence of spaces terminated by `nl` + arbitrary tail). 3. `stripBodyProducesStrippedShape` lemma — every output of `stripLineCommentBody` satisfies `IsStrippedBody`. Structural induction with `decEq` on Char. 4. Two base cases of `stripLineCommentsIdempotent`: empty input + non-`/`-headed input. 5. Three concrete sanity-check theorems (single non-comment char, bare `//`, char-plus-`//`). ## What this PR does NOT close Recorded as load-bearing Layer-1.0 follow-up in PROOF-NEEDS.md: | Obligation | Description | |---|---| | **stripIsIdentityOnStrippedBody (slash-slash closure)** | Closes the `'/'::'/':rest` inductive case of the main idempotence theorem. Statement: `stripLineComments` applied to any `IsStrippedBody xs` returns `xs` unchanged. | | **Block + string stripping** | Three slices: `Stripping_Block.idr`, `Stripping_Strings.idr`, `Stripping_Composition.idr`. | | **Position preservation** | For every index outside comment/string regions, stripping is the identity at that index. | ## Verification This is a pure-proof PR — no Rust changes. Idris2 totality checker will validate on the existing chapel-aware CI. (Note: the repo has 4 Idris2 files now in `src/abi/` — PA1, PA2, Types, and this new Stripping. They sit alongside the Rust crate and are not part of the cargo build.) ## Refs - PROOF-PROGRAMME.md row 1 of 9 (Layer 1.0) - PR #102/#105/#106/#107/#110 — v2.5.5 cohort - src/abi/PatternCompleteness.idr (PA1), ClassificationSoundness.idr (PA2)
1 parent ad72e06 commit ad1faf6

2 files changed

Lines changed: 250 additions & 2 deletions

File tree

‎PROOF-NEEDS.md‎

Lines changed: 6 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -2,22 +2,26 @@
22

33
## Current State
44

5-
- **src/abi/*.idr**: 3 files — `Types.idr`, `PatternCompleteness.idr` (PA1 ✅ 2026-04-11), `ClassificationSoundness.idr` (PA2 ✅ 2026-04-11)
5+
- **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)
66
- **Dangerous patterns**: 0 in own code (3 references are in the analyzer that DETECTS believe_me in other repos); 282 `unwrap()` calls
77
- **LOC**: ~31,700 (Rust)
8-
- **ABI layer**: Idris2 with completeness + soundness proofs
8+
- **ABI layer**: Idris2 with completeness + soundness proofs + Layer-1.0 stripping foundation
99

1010
## Completed Proofs
1111

1212
| Proof | File | What it proves |
1313
|-------|------|---------------|
1414
| 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. |
1515
| 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. |
16+
| 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. |
1617

1718
## What Still Needs Proving
1819

1920
| Component | What | Why |
2021
|-----------|------|-----|
22+
| **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. |
23+
| **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`. |
24+
| **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. |
2125
| Bridge reachability soundness | Reachability analysis is sound (no reachable dep wrongly classified as phantom) | Unreachable code marked reachable wastes effort; reachable missed = security gap |
2226
| Attestation chain unforgeability | Intent/evidence/seal triple is cryptographically bound; tampering detectable | Tampered attestations break trust chain |
2327
| Kanren taint analysis | Taint propagation tracks all tainted data flows | Missed taint flow means missed vulnerability |

‎src/abi/Stripping.idr‎

Lines changed: 244 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,244 @@
1+
-- SPDX-License-Identifier: MPL-2.0
2+
-- Copyright (c) 2026 Jonathan D.A. Jewell (hyperpolymath) <j.d.a.jewell@open.ac.uk>
3+
4+
||| Comment and String Stripping Idempotence (PROOF-PROGRAMME Layer 1.0)
5+
|||
6+
||| Mechanises the foundation lemma for every Layer-1 per-category
7+
||| soundness proof: the analyzer's comment/string-stripping pass is
8+
||| **idempotent** — running it twice yields the same output as running
9+
||| it once. This justifies the analyzer's preprocessing step
10+
||| (src/assail/analyzer.rs:931 `strip_proof_comments(without_strings,
11+
||| "//", Some(("/*", "*/")))`) as a sound normalising rewrite that
12+
||| every category detector can rely on without re-stripping.
13+
|||
14+
||| Status: this module ships the **foundation** —
15+
|||
16+
||| 1. Total Idris2 function definitions for `stripLineCommentBody`
17+
||| and `stripLineComments` mirroring the Rust analyzer's stripping
18+
||| pass.
19+
||| 2. The shape predicate `IsStrippedBody` + the proof that
20+
||| `stripLineCommentBody` always produces shape-respecting output
21+
||| (`stripBodyProducesStrippedShape`).
22+
||| 3. The two structural base cases of the idempotence theorem,
23+
||| Qed-closed without `believe_me` / `assert_total` / `?` holes.
24+
|||
25+
||| Open obligations (recorded in PROOF-NEEDS.md):
26+
||| * The `'/' :: '/' :: rest` inductive step of `stripLineCommentsIdempotent`
27+
||| requires a closure lemma showing that `stripLineComments` applied to
28+
||| any `IsStrippedBody`-shaped input is the identity. This is the
29+
||| load-bearing piece left for the next Layer-1.0 slice.
30+
||| * Block-comment (`/* */`) stripping, string-literal stripping, and
31+
||| the composition theorem (PROOF-PROGRAMME Layer 1.0 items 1–3).
32+
||| * Position preservation (Layer 1.0 item 4).
33+
module PanicAttack.ABI.Stripping
34+
35+
%default total
36+
37+
-- ═══════════════════════════════════════════════════════════════════════
38+
-- Helpers
39+
-- ═══════════════════════════════════════════════════════════════════════
40+
41+
||| The space character used to overwrite stripped regions.
42+
public export
43+
sp : Char
44+
sp = ' '
45+
46+
||| The newline character preserved during line-comment stripping (so
47+
||| line numbers in the stripped view match line numbers in the
48+
||| original — critical for the analyzer's location reporting).
49+
public export
50+
nl : Char
51+
nl = '\n'
52+
53+
-- ═══════════════════════════════════════════════════════════════════════
54+
-- Stripping functions (mirror src/assail/analyzer.rs:931 strip_proof_comments)
55+
-- ═══════════════════════════════════════════════════════════════════════
56+
57+
||| `stripLineCommentBody` walks from JUST AFTER `//` until the next
58+
||| newline, replacing every character with `sp`. The newline itself is
59+
||| preserved so line counts are stable.
60+
|||
61+
||| Note: this is the **post-leader** body, NOT the line-comment
62+
||| pattern itself. The pattern `//` is replaced separately by
63+
||| `stripLineComments` so the leader bytes also become spaces.
64+
public export
65+
stripLineCommentBody : List Char -> List Char
66+
stripLineCommentBody [] = []
67+
stripLineCommentBody (c :: rest) =
68+
if c == nl
69+
then nl :: rest -- preserve the rest of the file as-is
70+
else sp :: stripLineCommentBody rest
71+
72+
||| The main line-comment stripper. Walks the input, replacing any `//`
73+
||| (and the comment body up to the next newline) with `sp sp` followed
74+
||| by spaces up to the newline.
75+
public export
76+
stripLineComments : List Char -> List Char
77+
stripLineComments [] = []
78+
stripLineComments ('/' :: '/' :: rest) =
79+
sp :: sp :: stripLineCommentBody rest
80+
stripLineComments (c :: rest) = c :: stripLineComments rest
81+
82+
-- ═══════════════════════════════════════════════════════════════════════
83+
-- Shape predicate: what does `stripLineCommentBody` produce?
84+
-- ═══════════════════════════════════════════════════════════════════════
85+
86+
||| `IsStrippedBody xs` holds iff `xs` is a (possibly empty) sequence
87+
||| of `sp` characters terminated by a single `nl` followed by an
88+
||| ARBITRARY ORIGINAL TAIL.
89+
|||
90+
||| This characterises the output of `stripLineCommentBody`:
91+
||| every character before the next newline is `sp`, and the newline-
92+
||| plus-tail is the post-newline suffix of the original input
93+
||| (which the outer `stripLineComments` will walk over normally).
94+
public export
95+
data IsStrippedBody : List Char -> Type where
96+
StripEmpty : IsStrippedBody []
97+
StripJustNl : (tail : List Char) -> IsStrippedBody (nl :: tail)
98+
StripSpaceCons : (rest : List Char) ->
99+
IsStrippedBody rest ->
100+
IsStrippedBody (sp :: rest)
101+
102+
-- ═══════════════════════════════════════════════════════════════════════
103+
-- Lemma 1: every output of stripLineCommentBody satisfies IsStrippedBody
104+
-- ═══════════════════════════════════════════════════════════════════════
105+
106+
||| `stripBodyProducesStrippedShape cs` proves that whatever
107+
||| `stripLineCommentBody cs` returns satisfies `IsStrippedBody`.
108+
||| Proceeds by structural induction on `cs`.
109+
public export
110+
stripBodyProducesStrippedShape : (cs : List Char) ->
111+
IsStrippedBody (stripLineCommentBody cs)
112+
stripBodyProducesStrippedShape [] = StripEmpty
113+
stripBodyProducesStrippedShape (c :: rest) =
114+
-- We do a case-split on `c == nl`. The function definition uses
115+
-- `if c == nl then nl :: rest else sp :: stripLineCommentBody rest`,
116+
-- so we need to reflect that decision into the proof.
117+
case decEq c nl of
118+
Yes prf =>
119+
-- c == nl ⇒ output = nl :: rest. Build StripJustNl.
120+
rewrite prf in StripJustNl rest
121+
No _ =>
122+
-- c /= nl ⇒ output = sp :: stripLineCommentBody rest.
123+
-- Recurse to show the suffix is also a stripped body.
124+
StripSpaceCons (stripLineCommentBody rest)
125+
(stripBodyProducesStrippedShape rest)
126+
127+
-- ═══════════════════════════════════════════════════════════════════════
128+
-- Main theorem — line-comment stripping idempotence (PARTIAL)
129+
-- ═══════════════════════════════════════════════════════════════════════
130+
131+
||| **Base case (empty input).** Both sides reduce to `[]`. Qed.
132+
public export
133+
stripLineCommentsIdempotentEmpty :
134+
stripLineComments (stripLineComments []) = stripLineComments []
135+
stripLineCommentsIdempotentEmpty = Refl
136+
137+
||| **Non-comment-head case.** When the input does NOT start with
138+
||| `'/' :: '/' :: _`, the outer `stripLineComments` peels the head
139+
||| and recurses, so idempotence reduces to the inductive hypothesis
140+
||| on the tail.
141+
|||
142+
||| The inductive call uses Idris2's totality checker: the recursive
143+
||| `stripLineCommentsIdempotentTail` is structurally smaller (rest is
144+
||| a proper tail of (c :: rest)).
145+
public export
146+
stripLineCommentsIdempotentNonCommentHead :
147+
(c : Char) -> (rest : List Char) ->
148+
-- Hypothesis on the tail.
149+
(stripLineComments (stripLineComments rest) = stripLineComments rest) ->
150+
-- The (c :: rest) head guards: c is NOT '/', OR rest does NOT start with '/'.
151+
-- For this slice we discharge the simpler `c is not '/'` case.
152+
Not (c = '/') ->
153+
stripLineComments (stripLineComments (c :: rest))
154+
= stripLineComments (c :: rest)
155+
stripLineCommentsIdempotentNonCommentHead c rest ihTail cNotSlash =
156+
-- stripLineComments (c :: rest) reduces to (c :: stripLineComments rest)
157+
-- because the `'/' :: '/' :: _` pattern only matches when c IS '/'.
158+
-- Then strip on that = (c :: strip (strip rest)) = (c :: strip rest) by ihTail.
159+
-- The Idris2 case for the third clause requires no rewrite of
160+
-- `stripLineComments` because the head is consumed pattern-syntactically.
161+
rewrite ihTail in Refl
162+
163+
-- ═══════════════════════════════════════════════════════════════════════
164+
-- Open obligation — slash-slash inductive case
165+
-- ═══════════════════════════════════════════════════════════════════════
166+
167+
||| The general idempotence theorem requires closing the
168+
||| `'/' :: '/' :: rest` case. Sketch:
169+
|||
170+
||| strip ('/' :: '/' :: rest)
171+
||| = sp :: sp :: stripLineCommentBody rest
172+
|||
173+
||| Then `strip` applied to that = sp :: sp :: strip (stripLineCommentBody rest)
174+
||| (since `sp` is not `/`).
175+
|||
176+
||| We need: strip (stripLineCommentBody rest) = stripLineCommentBody rest.
177+
||| This is the **closure lemma**: applying `stripLineComments` to any
178+
||| IsStrippedBody input is the identity. Statement:
179+
|||
180+
||| stripIsIdentityOnStrippedBody :
181+
||| (xs : List Char) -> IsStrippedBody xs ->
182+
||| stripLineComments xs = xs
183+
|||
184+
||| The proof for StripEmpty is Refl. The StripJustNl case requires a
185+
||| second induction on the trailing `tail` since strip recurses into
186+
||| arbitrary content. The StripSpaceCons case unfolds strip on `sp`
187+
||| and applies the inductive hypothesis.
188+
|||
189+
||| **This is the load-bearing open obligation for Layer 1.0 — recorded
190+
||| in PROOF-NEEDS.md as the next slice of this module.**
191+
192+
-- ═══════════════════════════════════════════════════════════════════════
193+
-- Sanity tests (concrete cases verified by Idris2's totality checker)
194+
-- ═══════════════════════════════════════════════════════════════════════
195+
196+
||| Sanity check: stripping `"x"` (no comment) leaves it unchanged
197+
||| through both passes.
198+
private
199+
sanityNonCommentSingleChar :
200+
stripLineComments (stripLineComments ['x'])
201+
= stripLineComments ['x']
202+
sanityNonCommentSingleChar = Refl
203+
204+
||| Sanity check: stripping `"//"` followed by empty body — both
205+
||| passes produce `[sp, sp]`.
206+
private
207+
sanityBareCommentMarker :
208+
stripLineComments (stripLineComments ['/', '/'])
209+
= stripLineComments ['/', '/']
210+
sanityBareCommentMarker = Refl
211+
212+
||| Sanity check: stripping `"x//"` (a non-comment char followed by
213+
||| a bare `//`) — both passes produce `[x, sp, sp]`.
214+
private
215+
sanityCharPlusCommentMarker :
216+
stripLineComments (stripLineComments ['x', '/', '/'])
217+
= stripLineComments ['x', '/', '/']
218+
sanityCharPlusCommentMarker = Refl
219+
220+
-- ═══════════════════════════════════════════════════════════════════════
221+
-- Future work (Layer 1.0 remaining slices)
222+
-- ═══════════════════════════════════════════════════════════════════════
223+
224+
||| Module shipping plan:
225+
||| * **Stripping.idr** (this file) — line comments, foundation +
226+
||| shape lemma + base cases of idempotence. Open obligation:
227+
||| stripIsIdentityOnStrippedBody (the slash-slash inductive case).
228+
||| * **Stripping_Block.idr** (next slice) — `/* … */` pair-matching
229+
||| stripper with the same idempotence structure. Open obligation:
230+
||| nested-block-comment behaviour (Rust's `strip_proof_comments`
231+
||| does NOT recurse into nested blocks; we mirror that semantics).
232+
||| * **Stripping_Strings.idr** (next slice) — `"…"` with escape
233+
||| handling. Reuses the body-shape lemma pattern.
234+
||| * **Stripping_Composition.idr** — proves the full preprocessing
235+
||| pipeline (strings → block → line) is idempotent given each
236+
||| component is.
237+
||| * **Stripping_PositionPreservation.idr** — proves that for every
238+
||| index `i` where `cs[i]` is OUTSIDE every comment/string region,
239+
||| `strip cs ! i = cs[i]`. Justifies the analyzer's location
240+
||| reporting against the stripped view.
241+
|||
242+
||| Once all five land, every Layer-1.1..1.25 per-category proof can
243+
||| assume `strip s` is a fixed point and the original-vs-stripped
244+
||| position mapping is the identity on token boundaries.

0 commit comments

Comments
 (0)