diff --git a/PROOF-NEEDS.adoc b/PROOF-NEEDS.adoc index e09653d..ff07dae 100644 --- a/PROOF-NEEDS.adoc +++ b/PROOF-NEEDS.adoc @@ -1,102 +1,206 @@ -== PROOF-NEEDS.md — panic-attack - -=== Current State - -* **src/abi/*.idr**: 5 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+`), -`+AttestationUnforgeability.idr+` (PROOF-PROGRAMME §3.2 ✅ 2026-06-04 — -conditional unforgeability from Ed25519 EUF-CMA + chain-hash -collision-resistance hypotheses) -* *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 - -=== Completed Proofs - -[width="100%",cols="26%,21%,53%",options="header",] += Proof status: panic-attack + +This file records each proof obligation in panic-attack, the verifier it +belongs to, and its status. The rules are the estate proof policy, +https://github.com/metadatastician/standards/blob/9bdf864cc7f2c8e24b4df84bf00d04158eee3ad5/3-practice/PROOF-POLICY.adoc[`standards/3-practice/PROOF-POLICY.adoc` +at `9bdf864cc7f2c8e24b4df84bf00d04158eee3ad5`]. Statuses use its closed §5 +vocabulary: `PROVEN`, `PROVEN-WITH-AXIOMS`, `TESTED`, `ASSUMED`, `OPEN`. + +None of these obligations is a theory theorem (§1), so none carries a Proof +Witness Grade. + +== Where each kind of obligation belongs + +* *Behaviour of first-party Rust code* (stripping, reachability, taint + propagation, dispatch): Creusot with Pearlite contracts, and Verus, on the + implementation (§1.2). An Idris2 model of a Rust function is not evidence + that the function is correct (§1, §2.2). +* *Interfaces, ABI encodings and cross-language protocols* (the attestation + chain, the C integer encodings): Idris2. +* *Statements true of any implementation* (for example, a taint lattice + and its fixed point stated abstractly): Agda, rechecked in Rocq and Lean + (§2). + +No Kani obligation arises (§4.1). With `unsafe_code` forbidden, +`cargo clippy --lib --bins --tests --benches --all-features -- -F unsafe_code` +compiles at `f2a6a70eaec0cb02331e3264e05f185b5faab0f7`. The only `unsafe` +is in `examples/vulnerable_program.rs`, a deliberately buggy program that +exists to be scanned. + +== Receipt for the Idris2 modules + +* *Checker:* Idris2 0.7.0, the version `proven-tests.yml` pins, built from + tag `v0.7.0` (`27780073c8631826d846499840b3857d9b9a4fd5`) on Chez Scheme + 9.5.8. +* *Source:* `src/abi/*.idr` at + `3dc4728762f37c1e5bebdb988783c7683c50fb55`. `Stripping.idr` was rechecked + after the comment-only edits in `ab0fdb2107e034e99b4b4f2fd7fb7366750d536e` + and still passes; the other four modules are unchanged since `3dc4728`. +* *Invocation:* the modules are named `PanicAttack.ABI.` but live in + `src/abi/`, so `idris2 --check src/abi/.idr` fails on a module-name + mismatch from any directory. Each was checked from a tree that places + `src/abi/.idr` at `PanicAttack/ABI/.idr`, with + `idris2 --check PanicAttack/ABI/.idr`. A pass is exit 0 *and* no + `Error:` line, because `idris2 --check` can exit 0 while printing an + error. +* *Result:* all five modules pass. Every module sets `%default total` and + uses no `believe_me`, `assert_total`, `postulate` or holes. +* *Negative controls:* a planted false lemma and a planted non-terminating + definition in `Stripping.idr` were both rejected, so the check can fail. +* *Gate:* no CI job runs this check. That obligation is `OPEN` below. Until + it closes, the statuses here rest on this one local run, and any change + to `src/abi/` invalidates them. + +== Ledger + +[cols="3,2,2,5",options="header"] |=== -|Proof |File |What it proves -|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 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. - -|Attestation chain unforgeability -|`+src/abi/AttestationUnforgeability.idr+` |*PROOF-PROGRAMME §3.2 -(2026-06-04, issue #123)*: models the intent→evidence→seal chain -(`+chain_hash = H(intent‖evidence‖report)+`, Ed25519-signed) with the -cryptographic facts as a `+parameters+` block (hypotheses, *not* -`+postulate+`). Under `+%default total+` Qed-closes `+integrity+` -(tampering any phase invalidates the seal), `+authenticity+` (a -verifying seal comes from the matching secret key), `+nonRepudiation+` -(a genuine seal verifies), plus 2 corollaries. Conditional on chain-hash -collision-resistance + Ed25519 EUF-CMA (message- and signer-binding) + -signature correctness. - -|Hexad↔Octad persistence round-trip |`+src/storage/mod.rs+` (proptest) -|*PROOF-PROGRAMME §3.1 (2026-06-04, #122)*: -`+hexad_json_roundtrip_is_identity+` tests an in-memory -`+serde_json::Value+` serialize/deserialize/serialize round-trip on generated -samples, not by a universal theorem. It does not call `+write_*_hexad+` or -`+load_hexad_dir+`; on-disk persistence correspondence remains a separate -obligation. The gateway octad projection is lossy by design, so this property -also does not establish a faithful hexad↔octad map. +|Obligation |Artefact |Status |Trust boundary and notes + +|Severity order: `Low < Medium < High < Critical` is a total order; +`sevMax` is an upper bound; the numeric encoding is monotone (PA2) +|`src/abi/ClassificationSoundness.idr` +|`PROVEN` (model) +|The model's `Severity` matches the variant names and order of +`src/types.rs`; that correspondence is `ASSUMED` (a hand transcription). +The Rust order itself comes from `#[derive(PartialOrd, Ord)]`. + +|Line-comment stripping is idempotent: `strip (strip s) = strip s` +|`src/abi/Stripping.idr` +|`PROVEN` (model) +|Did not compile on `main` before `3dc4728`; repaired there without +changing the theorem. The repaired model equals the previous one: +`TESTED`, exhaustively on all 349,525 strings of length at most 9 over +`/`, newline, `x` and space. That comparison is model against model, not +model against Rust. + +The model does *not* match `strip_proof_comments`, so it is evidence about +the model only. It replaces comment characters with spaces and keeps every +newline. The Rust function deletes comment text and drops a trailing +newline: on `//x` the model gives three spaces and Rust gives the empty +string. The model also covers line comments only; block comments and string +literals are not modelled. + +|Attestation chain: integrity, authenticity, non-repudiation +|`src/abi/AttestationUnforgeability.idr` +|`PROVEN` (model), relative to the `ASSUMED` hypotheses listed here +|The module's `parameters` block assumes: + +* `chainCR`: the chain hash is *injective*. +* `sigCorrect`: an honest signature verifies. +* `sigBindsMessage`: a signature verifies only on the message signed. +* `sigOnlySigner`: for every verifying signature there is a secret key + whose public key is the verifying key and whose signature on that digest + is that signature. + +`sigOnlySigner` says such a key *exists*. It says nothing about who +produced the signature, so `authenticity` inherits that limit: it shows the +seal equals one a matching key would make, not that the key holder made it. +`chainCR` and `sigOnlySigner` are idealisations, stronger than collision +resistance and EUF-CMA, and false of any real fixed-length hash or +signature scheme. So these are theorems of a symbolic (Dolev-Yao style) +model, not a computational security reduction. Model to +`src/attestation/`: `ASSUMED`. A computational proof is not claimed. + +|Every language reaches an analyzer; every weak-point category has a +detector; cross-language checks run on every file (PA1) +|`src/abi/PatternCompleteness.idr` +|`PROVEN` (model); supports no claim about the Rust code +|The theorem is vacuous: `GenericAnalyzer : HasAnalyzer lang` inhabits +the witness type for every language, so it holds whatever the dispatch +does. Rust gives the narrower guarantee that actually holds: +`match file_lang` in `src/assail/analyzer.rs` ends in +`_ => analyze_generic`, and `rustc` checks the match is exhaustive. That +covers every file that reaches the match. A file with no source language +and no configuration adapter (`Language::Unknown`, no adapter) is marked +`unsupported` in the coverage ledger and skipped first, so not every file +reaches an analyzer. + +The model has also drifted. Its `Lang` has 50 constructors and +`src/types.rs` has 52; `C` and `Php` are missing. `crossLangAlwaysApplied` +says cross-language checks run on every file, but the Rust code skips them +when `configuration.is_some()`. That model claim is false of the +implementation. + +|Declarations for the ABI-facing types and their C integer encodings +|`src/abi/Types.idr` +|No theorem +|Repaired in `3dc4728` so it compiles. It contains no proof and nothing +imports it. Drift: its `Severity` is `Info / Warning / Error / Critical` +where `src/types.rs` has `Low / Medium / High / Critical`, and `LangId` is +bounded at 47 against 52 variants. + +|Hexad JSON round-trip is the identity +|`src/storage/mod.rs`, `hexad_json_roundtrip_is_identity` (proptest) +|`TESTED` +|A serialize, deserialize, serialize round trip on proptest-generated +hexads, compared as `serde_json::Value`. Bounds: proptest's default 256 +cases (the repository sets no override). `id` and `program_path` are 0 to +48 characters from `[A-Za-z0-9:_./-]`; `language` 0 to 12 lowercase +letters; `version` 1 to 8 characters from `[0-9.]`; the four counts are +below 10,000; `robustness_score` is in [0, 1]; `categories` holds 0 to 5 +strings of 1 to 16 letters; `attestation_hash` is absent or up to 64 hex +digits. Fixed, not generated: `schema`, `created_at`, `tool`, and +`document` (`{"weak_points": [], "n": total}`), and the `migration`, +`finding`, `campaign` and `crosslang` facets are all `None`. It does not call +`write_*_hexad` or `load_hexad_dir`, so on-disk persistence is a separate +obligation. The gateway octad projection is lossy by design, so this does +not establish a faithful hexad-to-octad map. |=== -=== What Still Needs Proving +== Open obligations -[width="100%",cols="51%,27%,22%",options="header",] +[cols="3,2,5",options="header"] |=== -|Component |What |Why -|*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 - -|Kanren taint analysis |Taint propagation tracks all tainted data flows -|Missed taint flow means missed vulnerability +|Obligation |Verifier (§1, §1.2) |Notes + +|Gate the Idris2 modules in CI +|CI +|Run the receipt's invocation on every change to `src/abi/`, failing on +any `Error:` line. Moving the files to `src/abi/PanicAttack/ABI/` would +let a plain `idris2 --check` work. + +|`strip_proof_comments` is idempotent and preserves positions outside +comments and strings +|Fix the implementation first; then Creusot/Pearlite and Verus +|Neither property holds of the current Rust function, so neither can be +proved until it changes. All three cases below were run against the +function as it is on `main`: + +* Not idempotent: `a//*x*/*b*/c` gives `a/*b*/c`, and a second pass gives + `ac`. +* Positions move: `a/*x*/b` gives `ab`, moving `b` from offset 6 to 1. +* Ordering bug: block comments are stripped before line comments, so a + block opener inside a line comment swallows the code after it. + `code // see /* note`, then `hidden();`, then `*/ tail`, gives `code `. + The callers that pass both a line and a block marker are affected: + `analyze_rust`, `is_rust_ffi_safe_wrapper`, `analyze_idris`, + `analyze_lean` and `analyze_agda`. In the Idris, Lean and Agda ProofDrift + detectors such a comment can hide a later `sorry`, `believe_me` or + postulate. `analyze_isabelle` and `analyze_coq` pass no line marker and + are not affected. + +The Idris2 model above can guide the contracts once the function is +fixed; it does not discharge them. The model's own remaining slices +(block comments, strings, composition, position preservation; issue #114) +are optional once the implementation proof exists. + +|Patch Bridge reachability is sound: no reachable dependency is classified +as phantom +|Creusot/Pearlite and Verus +|`src/bridge/reachability.rs`. A missed reachable dependency is a security +gap. + +|Kanren taint analysis tracks every tainted flow +|Creusot/Pearlite and Verus; Agda for the abstract theory +|Any implementation-independent statement (the lattice, monotonicity, the +fixed point) is theory and belongs in Agda with Rocq and Lean rechecks. +Its realisation in `src/kanren/` is a Rust obligation. + +|Replace or retire PA1 +|Creusot/Pearlite and Verus, or retire +|A non-vacuous statement would be, for example, that each language with +a dedicated analyzer is routed to it. If that is not wanted, retire the +module, because `rustc`'s exhaustiveness check already gives the current +guarantee. |=== - -=== Recommended Prover - -*Idris2* — Already in use. Taint analysis correctness proofs could use -*Agda* with relational semantics. The 282 unwrap() calls are a -significant debt (but separate from the proof obligations). - -=== Priority - -*MEDIUM* (was HIGH) — PA1 and PA2 completed 2026-04-11. The highest-risk -false-negative scenario (analyzer dispatch completeness) is now formally -proved. Remaining proofs are deeper semantic properties. diff --git a/src/abi/Stripping.idr b/src/abi/Stripping.idr index 115fdef..ecc6496 100644 --- a/src/abi/Stripping.idr +++ b/src/abi/Stripping.idr @@ -4,34 +4,34 @@ ||| Comment and String Stripping Idempotence (PROOF-PROGRAMME Layer 1.0) ||| -||| Closes the slash-slash inductive case left open by PR #111 (issue #113). +||| Models the line-comment slice of the analyzer's comment-stripping pass, +||| `src/assail/analyzer.rs` `strip_proof_comments(without_strings, "//", +||| Some(("/*", "*/")))`, and proves the model **idempotent**: running it +||| twice yields the same output as running it once. ||| -||| Mechanises the foundation lemma for every Layer-1 per-category -||| soundness proof: the analyzer's comment-stripping pass is -||| **idempotent** — running it twice yields the same output as running -||| it once. This justifies the analyzer's preprocessing step at -||| `src/assail/analyzer.rs:931 strip_proof_comments(without_strings, -||| "//", Some(("/*", "*/")))` as a sound normalising rewrite that -||| every category detector can rely on without re-stripping. +||| What this establishes, and what it does not: ||| -||| Differences from the PR #111 model: +||| * The theorem is about this Idris2 model, not the Rust function, and the +||| model does not reproduce the Rust output. The model replaces comment +||| characters with spaces and keeps every newline; the Rust pass deletes +||| comment text and drops a trailing newline (`//x` gives three spaces +||| here and the empty string in Rust). Block comments and string literals +||| are not modelled. See PROOF-NEEDS.adoc for the Rust function's own +||| status. +||| * Multi-comment semantics: every `//` comment is stripped, not only the +||| first (the PR #111 model's error). `stripLineCommentBody` hands +||| control back to `stripLineComments` after each preserved newline. ||| -||| 1. **Multi-comment semantics.** PR #111's model only stripped the -||| first `//` comment encountered — subsequent comments after a -||| newline were preserved unstripped. The Rust pass strips ALL -||| comments in the input. This module uses mutual recursion -||| (`stripLineComments` ↔ `stripLineCommentBody`) so that the -||| body-stripper calls back into the main stripper after each -||| preserved newline. -||| -||| 2. **Idempotence is now provable by structural induction** because -||| both functions consume strictly-smaller inputs on each call. -||| Idris2's totality checker validates the recursion. -||| -||| 3. **Slash-slash case Qed-closes** via `bodyIsFixedPoint` — -||| the closure lemma `stripLineComments (stripLineCommentBody xs) -||| = stripLineCommentBody xs` proved by simultaneous induction on -||| the main theorem and the body theorem. +||| Proof shape. Matching on a `Char` literal only reduces when the +||| character is itself a literal, so a proof over a variable character +||| gets stuck. Each character is therefore classified once (`cls`), and +||| every step dispatches on the class. The proofs carry the class as an +||| explicit argument together with the equation `cls c = k`, so each +||| case reduces. `stripLineComments` and `stripLineCommentBody` compute +||| the same function as the earlier pattern-matching Idris2 definitions; +||| that was checked exhaustively on every string of length at most 9 over +||| `/`, newline, `x` and space (349,525 inputs, no mismatch). That check +||| compares two Idris2 models; it is not a comparison with Rust. module PanicAttack.ABI.Stripping %default total @@ -52,39 +52,70 @@ public export nl : Char nl = '\n' +||| The only distinctions the stripper makes between characters. +public export +data Cls = Slash | Newline | Other + +public export +cls : Char -> Cls +cls '/' = Slash +cls '\n' = Newline +cls _ = Other + -- ═══════════════════════════════════════════════════════════════════════ --- Stripping functions (mirror src/assail/analyzer.rs:931 strip_proof_comments) +-- Stripping functions: a model of the line-comment slice of +-- src/assail/analyzer.rs strip_proof_comments. The model keeps spaces and +-- newlines where the Rust function deletes comment text and drops a +-- trailing newline. -- --- Mutual recursion: stripLineComments handles non-comment input and --- delegates comment bodies to stripLineCommentBody; stripLineCommentBody --- walks until the next newline and then returns control to the main --- stripper for the post-newline tail. +-- `stripStep`, `slashStep` and `bodyStep` take the class of the character +-- in hand, so each recursive call is on a strict sub-list and the +-- totality checker accepts the definition. -- ═══════════════════════════════════════════════════════════════════════ mutual - ||| The main line-comment stripper. Walks the input, replacing any - ||| `//` (and the comment body up to the next newline) with `sp sp` - ||| followed by spaces up to the newline, then continuing past the - ||| newline with another stripping pass. + ||| The main line-comment stripper. Replaces each `//` and the comment + ||| body up to the next newline with spaces, keeps the newline, and + ||| continues stripping after it. public export stripLineComments : List Char -> List Char stripLineComments [] = [] - stripLineComments ('/' :: '/' :: rest) = - sp :: sp :: stripLineCommentBody rest - stripLineComments (c :: rest) = c :: stripLineComments rest - - ||| `stripLineCommentBody` walks from JUST AFTER `//` until the - ||| next newline, replacing every character with `sp`. At the - ||| newline (or end of input) it returns control to - ||| `stripLineComments` for the remainder, so the entire input is - ||| processed in one pass. + stripLineComments (c :: rest) = stripStep (cls c) c rest + + ||| One step of `stripLineComments`, given the class of the head. + public export + stripStep : Cls -> Char -> List Char -> List Char + stripStep Slash c [] = [c] + stripStep Slash c (d :: r) = slashStep (cls d) c d r + stripStep Newline c rest = c :: stripLineComments rest + stripStep Other c rest = c :: stripLineComments rest + + ||| A `/` followed by `d`: a comment opens only when `d` is `/` too. + public export + slashStep : Cls -> Char -> Char -> List Char -> List Char + slashStep Slash c d r = sp :: sp :: stripLineCommentBody r + slashStep Newline c d r = c :: stripStep Newline d r + slashStep Other c d r = c :: stripStep Other d r + + ||| Walks from just after `//` to the next newline, replacing every + ||| character with `sp`, then hands the rest back to + ||| `stripLineComments`. public export stripLineCommentBody : List Char -> List Char stripLineCommentBody [] = [] - stripLineCommentBody (c :: rest) = - if c == nl - then nl :: stripLineComments rest - else sp :: stripLineCommentBody rest + stripLineCommentBody (c :: rest) = bodyStep (cls c) rest + + ||| One step of `stripLineCommentBody`, given the class of the head. + public export + bodyStep : Cls -> List Char -> List Char + bodyStep Newline rest = nl :: stripLineComments rest + bodyStep Slash rest = sp :: stripLineCommentBody rest + bodyStep Other rest = sp :: stripLineCommentBody rest + +||| `stripLineComments` on a cons cell, unfolded one step. +stripCons : (c : Char) -> (x : List Char) -> + stripLineComments (c :: x) = stripStep (cls c) c x +stripCons c x = Refl -- ═══════════════════════════════════════════════════════════════════════ -- Idempotence — main theorem + body fixed-point lemma, mutual induction @@ -97,66 +128,55 @@ mutual stripLineCommentsIdempotent : (cs : List Char) -> stripLineComments (stripLineComments cs) = stripLineComments cs stripLineCommentsIdempotent [] = Refl - stripLineCommentsIdempotent ('/' :: '/' :: rest) = - -- LHS = strip (strip ('/' :: '/' :: rest)) - -- = strip (sp :: sp :: stripBody rest) [by definition] - -- = sp :: strip (sp :: stripBody rest) [sp /= '/'] - -- = sp :: sp :: strip (stripBody rest) [sp /= '/'] - -- = sp :: sp :: stripBody rest [by bodyIsFixedPoint] - -- RHS = sp :: sp :: stripBody rest [by definition] - cong (\xs => sp :: sp :: xs) (bodyIsFixedPoint rest) - stripLineCommentsIdempotent ('/' :: c :: rest) = - -- Not a comment marker (c is not the immediate-second '/'). - -- The third clause of stripLineComments applies: the head '/' - -- is preserved and recursion continues on (c :: rest). - case c of - '/' => Refl -- impossible: the prior clause matched - _ => cong ('/' ::) (stripLineCommentsIdempotent (c :: rest)) - stripLineCommentsIdempotent (c :: rest) = - -- Generic non-comment-head case: c is not `/`. The outer strip - -- preserves the head and recurses, so idempotence reduces to - -- the inductive hypothesis. - case c of - '/' => case rest of - [] => Refl - _ :: _ => Refl -- covered by the prior two clauses - _ => cong (c ::) (stripLineCommentsIdempotent rest) + stripLineCommentsIdempotent (c :: rest) = stepIdem (cls c) c Refl rest + + ||| Idempotence of one step, for a head `c` of class `k`. + stepIdem : (k : Cls) -> (c : Char) -> cls c = k -> (rest : List Char) -> + stripLineComments (stripStep k c rest) = stripStep k c rest + stepIdem Slash c p [] = + rewrite stripCons c [] in rewrite p in Refl + stepIdem Slash c p (d :: r) = slashIdem (cls d) c p d Refl r + stepIdem Newline c p rest = + rewrite stripCons c (stripLineComments rest) in rewrite p in + cong (c ::) (stripLineCommentsIdempotent rest) + stepIdem Other c p rest = + rewrite stripCons c (stripLineComments rest) in rewrite p in + cong (c ::) (stripLineCommentsIdempotent rest) + + ||| Idempotence after a `/`, for a next character `d` of class `j`. + ||| When `j` is `Slash` a comment opens and the body lemma applies; + ||| otherwise the `/` is kept, and it still cannot pair with `d` on + ||| the second pass. + slashIdem : (j : Cls) -> (c : Char) -> cls c = Slash -> + (d : Char) -> cls d = j -> (r : List Char) -> + stripLineComments (slashStep j c d r) = slashStep j c d r + slashIdem Slash c p d q r = + cong (\xs => sp :: sp :: xs) (bodyIsFixedPoint r) + slashIdem Newline c p d q r = + rewrite stripCons c (d :: stripLineComments r) in rewrite p in + rewrite q in + cong (\xs => c :: d :: xs) (stripLineCommentsIdempotent r) + slashIdem Other c p d q r = + rewrite stripCons c (d :: stripLineComments r) in rewrite p in + rewrite q in + cong (\xs => c :: d :: xs) (stripLineCommentsIdempotent r) ||| **Body fixed-point lemma.** Applying the line-comment stripper - ||| to the output of the body-stripper is a no-op — the body - ||| output's pre-newline region is all `sp` (no further `//` can - ||| form), and the post-newline tail is whatever the body-stripper - ||| recursively passed to `stripLineComments`, which is already - ||| a fixed point by the main theorem. + ||| to the output of the body-stripper is a no-op: the pre-newline + ||| region is all `sp`, so no `//` can form, and the post-newline + ||| tail is already a fixed point by the main theorem. public export bodyIsFixedPoint : (cs : List Char) -> stripLineComments (stripLineCommentBody cs) = stripLineCommentBody cs bodyIsFixedPoint [] = Refl - bodyIsFixedPoint (c :: rest) = - -- Case split on whether c is the newline. - case decEq c nl of - Yes prf => - -- c = nl. Body returns `nl :: stripLineComments rest`. - -- strip applied to that = `nl :: strip (stripLineComments rest)` - -- (nl /= '/'). By main theorem on `rest`, that = - -- `nl :: stripLineComments rest`. - rewrite prf in - cong (nl ::) (stripLineCommentsIdempotent rest) - No cNotNl => - -- c /= nl. Body returns `sp :: stripLineCommentBody rest`. - -- strip applied to that = `sp :: strip (stripLineCommentBody rest)` - -- (sp /= '/'). By the body IH, that = `sp :: stripLineCommentBody rest`. - let - -- Establish that the body output starts with sp - -- under the c /= nl case. - bodyOutputShape : stripLineCommentBody (c :: rest) - = sp :: stripLineCommentBody rest - bodyOutputShape = case decEq c nl of - Yes y => absurd (cNotNl y) - No _ => Refl - in - rewrite bodyOutputShape in - cong (sp ::) (bodyIsFixedPoint rest) + bodyIsFixedPoint (c :: rest) = bodyStepFixed (cls c) rest + + ||| The body lemma for one step, for a head of class `k`. + bodyStepFixed : (k : Cls) -> (rest : List Char) -> + stripLineComments (bodyStep k rest) = bodyStep k rest + bodyStepFixed Newline rest = cong (nl ::) (stripLineCommentsIdempotent rest) + bodyStepFixed Slash rest = cong (sp ::) (bodyIsFixedPoint rest) + bodyStepFixed Other rest = cong (sp ::) (bodyIsFixedPoint rest) -- ═══════════════════════════════════════════════════════════════════════ -- Sanity tests @@ -219,27 +239,27 @@ sanityTwoComments = Refl -- What still remains (Layer 1.0 future slices) -- ═══════════════════════════════════════════════════════════════════════ -||| Future Layer-1.0 work (recorded in PROOF-NEEDS.md + issue #114): -||| -||| 1. **Stripping_Block.idr** — `/* … */` block-comment stripper. Same -||| mutual-recursion shape. The closing `*/` plays the role newlines -||| played here. -||| -||| 2. **Stripping_Strings.idr** — `"…"` string-literal stripper with -||| `\"` escape handling. Same mutual-recursion shape. -||| -||| 3. **Stripping_Composition.idr** — `strip = stripLineComments . -||| stripBlockComments . stripStrings` is itself idempotent given -||| each component is. Requires cross-component lemmas (e.g. line- -||| stripping the output of block-stripping doesn't introduce new -||| `/*` tokens). -||| -||| 4. **Stripping_PositionPreservation.idr** — for every index `i` -||| where `cs[i]` is OUTSIDE every comment/string region, -||| `strip cs ! i = cs[i]`. Justifies the analyzer reporting -||| locations against the stripped view as original-source -||| locations. -||| -||| Once all five land, every Layer-1.1..1.25 per-category proof can -||| assume `strip s` is a fixed point and the original-vs-stripped -||| position mapping is the identity on token boundaries. +-- Future Layer-1.0 work (recorded in PROOF-NEEDS.adoc + issue #114): +-- +-- 1. **Stripping_Block.idr** — `/* … */` block-comment stripper. Same +-- mutual-recursion shape. The closing `*/` plays the role newlines +-- played here. +-- +-- 2. **Stripping_Strings.idr** — `"…"` string-literal stripper with +-- `\"` escape handling. Same mutual-recursion shape. +-- +-- 3. **Stripping_Composition.idr** — `strip = stripLineComments . +-- stripBlockComments . stripStrings` is itself idempotent given +-- each component is. Requires cross-component lemmas (e.g. line- +-- stripping the output of block-stripping doesn't introduce new +-- `/*` tokens). +-- +-- 4. **Stripping_PositionPreservation.idr** — for every index `i` +-- where `cs[i]` is OUTSIDE every comment/string region, +-- `strip cs ! i = cs[i]`. Justifies the analyzer reporting +-- locations against the stripped view as original-source +-- locations. +-- +-- Once all five land, every Layer-1.1..1.25 per-category proof can +-- assume `strip s` is a fixed point and the original-vs-stripped +-- position mapping is the identity on token boundaries. diff --git a/src/abi/Types.idr b/src/abi/Types.idr index ee997b1..9cebcfe 100644 --- a/src/abi/Types.idr +++ b/src/abi/Types.idr @@ -3,11 +3,13 @@ -- Copyright (c) 2026 Jonathan D.A. Jewell (hyperpolymath) ||| ABI Types for panic-attack static analysis engine ||| -||| Defines the formal interface for the scanner's operations. -||| Proves that: -||| 1. Severity levels are totally ordered -||| 2. Scan results cannot be fabricated (constructive) -||| 3. Language coverage is bounded +||| Declares ABI-facing types and their C integer encodings. It contains no +||| theorems, and no other module imports it. The severity order is proved +||| in ClassificationSoundness.idr, over its own Severity type. +||| +||| Known drift (see PROOF-NEEDS.adoc): this Severity type does not match +||| src/types.rs, and LangId is bounded at 47 while src/types.rs has 52 +||| Language variants. module PanicAttack.ABI.Types import Data.Fin @@ -18,6 +20,14 @@ import Data.Fin public export data Severity = Info | Warning | Error | Critical +public export +Eq Severity where + Info == Info = True + Warning == Warning = True + Error == Error = True + Critical == Critical = True + _ == _ = False + ||| Total ordering on severity public export Ord Severity where @@ -43,7 +53,7 @@ data ScanOp ||| Language identifier (47 supported, bounded) public export -data LangId = MkLangId (n : Fin 47) +data LangId = MkLangId (Fin 47) -- ═══════════════════════════════════════════════════════════════════════ -- C ABI Exports