diff --git a/.github/workflows/proven-tests.yml b/.github/workflows/proven-tests.yml index 82ab20c..dcaa3e6 100644 --- a/.github/workflows/proven-tests.yml +++ b/.github/workflows/proven-tests.yml @@ -22,6 +22,12 @@ # and it would make every contributor wait on a compiler that cannot change # for them. # +# `idris-abi` (every PR, blocking): type-checks this repo's own Idris2 ABI +# proofs in src/abi/. This is a departure from the rule above, made because +# these proofs are claims in PROOF-NEEDS.adoc and a claim needs a receipt on +# every change. Idris2 is built from source once and cached by version and +# commit, so after the first run a PR waits only for the check itself. +# # WHY THE REPORT IS A FILE, NOT A PARAGRAPH: docs/INTEROP-PANIC-ATTACK.adoc in # proven-tests-and-benches fixes the mapping in prose; a report plus a verifier # is the same mapping with something at stake. @@ -191,3 +197,54 @@ jobs: path: .proven-tests/build/report/*.json retention-days: 30 if-no-files-found: warn + + # The Idris2 ABI proofs in src/abi/ (PA1, PA2, Layer 1.0 stripping, + # attestation unforgeability, ABI types). Until this job, none was ever + # type-checked. scripts/ci/check-idris-abi.sh fails on any type error, + # a missing `%default total`, or an escape hatch. + # + # Deviation (PROOF-POLICY §6), state: open. Leg: Idris2 ABI proofs. Tool: + # Idris2 0.7.0 built from the v0.7.0 tag (commit checked below) with the + # runner's Chez Scheme. Why not Guix or the container: panic-attack's Guix + # manifest and container do not provide Idris2 yet. + idris-abi: + name: Idris2 ABI proofs type-check + runs-on: ubuntu-latest + timeout-minutes: 45 + env: + IDRIS2_COMMIT: 27780073c8631826d846499840b3857d9b9a4fd5 + steps: + - name: Checkout this repository + uses: actions/checkout@3d3c42e5aac5ba805825da76410c181273ba90b1 # v7.0.1 + with: + persist-credentials: false + + - name: Cache the Idris2 toolchain built from source + id: idris2-cache + uses: actions/cache@55cc8345863c7cc4c66a329aec7e433d2d1c52a9 # v6.1.0 + with: + path: ~/.idris2-src-build + key: idris2-src-${{ env.IDRIS2_VERSION }}-${{ env.IDRIS2_COMMIT }}-${{ runner.os }} + + - name: Build Idris2 from the pinned tag (cache miss only) + if: steps.idris2-cache.outputs.cache-hit != 'true' + shell: bash + run: | + set -euo pipefail + sudo apt-get update -qq + sudo apt-get install -y -qq chezscheme + src=$(mktemp -d) + git clone --quiet --depth 1 --branch "v${IDRIS2_VERSION}" \ + https://github.com/idris-lang/Idris2.git "$src" + test "$(git -C "$src" rev-parse HEAD)" = "$IDRIS2_COMMIT" + make -C "$src" bootstrap SCHEME=scheme PREFIX="$HOME/.idris2-src-build" + make -C "$src" install PREFIX="$HOME/.idris2-src-build" + + - name: Type-check every module in src/abi + shell: bash + run: | + set -euo pipefail + # The cached build still needs Chez Scheme at run time. + command -v scheme >/dev/null || { sudo apt-get update -qq && sudo apt-get install -y -qq chezscheme; } + export PATH="$HOME/.idris2-src-build/bin:$PATH" + bash scripts/ci/check-idris-abi.sh diff --git a/CHANGELOG.adoc b/CHANGELOG.adoc index 59d763f..6c93c73 100644 --- a/CHANGELOG.adoc +++ b/CHANGELOG.adoc @@ -2,6 +2,24 @@ === [Unreleased] +==== Fixed — the Idris2 ABI proofs are type-checked, and the stripping proof is re-proved + +* No CI job had ever type-checked `+src/abi/+`, and as committed none of its +five modules checked. A new `+idris-abi+` job (`+proven-tests.yml+`, using +`+scripts/ci/check-idris-abi.sh+`) now checks all five on every PR with Idris2 +0.7.0. It fails on a type error, on a missing `+%default total+`, or on +`+believe_me+`, `+assert_total+`, `+assert_smaller+`, `+postulate+` or +`+idris_crash+`. +* `+Stripping.idr+`: the 2026-06-02 proof of `+stripLineCommentsIdempotent+` +never type-checked, so it is re-proved through two facts: stripping is the +identity on text with no `+//+`, and the strippers' output has no `+//+`. The +strippers are restated with explicit `+Bool+` tests. An exhaustive run over +29,524 inputs shows they behave exactly as before. +* `+Types.idr+`: adds the missing `+Eq Severity+` that `+Ord+` needs, and fixes +the `+LangId+` declaration syntax. +* `+PROOF-NEEDS.adoc+` and `+EXPLAINME.adoc+` now say that the earlier claims had +no receipt. + ==== Added — `+assail --output-format kyaml+` writes a KYAML copy * With `+--output-format kyaml+` and `+--output report.json+`, `+assail+` writes diff --git a/EXPLAINME.adoc b/EXPLAINME.adoc index 8724d1f..caf3293 100644 --- a/EXPLAINME.adoc +++ b/EXPLAINME.adoc @@ -54,7 +54,7 @@ The README makes claims. This file backs them up. | `src/jit_context.rs` | JIT-framework classifier: Cranelift / Llvm / Wasm / Javascript / None; `transmute_targets_fn_ptr` recogniser for fn-ptr type-punning | `src/abi/PatternCompleteness.idr` | PA1 Idris2 proof — every Lang/Category has a detector | `src/abi/ClassificationSoundness.idr` | PA2 Idris2 proof — severity total order + maxSeverity commutativity -| `src/abi/Stripping.idr` | Layer 1.0 partial — line-comment-strip foundation (shape lemma + base cases of `stripLineCommentsIdempotent` Qed-closed) +| `src/abi/Stripping.idr` | Layer 1.0 — line-comment stripping is idempotent (`stripLineCommentsIdempotent`; re-proved 2026-11-09, type-checked by the `idris-abi` CI job) | `src/kanren/` | Logic engine (unification, fact database, taint, cross-lang) | `src/kanren/core.rs` | Term, substitution, unification, FactDB, forward chaining | `src/kanren/taint.rs` | Source→sink tracking (user input, network, deserialization) diff --git a/PROOF-NEEDS.adoc b/PROOF-NEEDS.adoc index e09653d..c86680d 100644 --- a/PROOF-NEEDS.adoc +++ b/PROOF-NEEDS.adoc @@ -2,12 +2,23 @@ === Current State +*Receipts (2026-11-09).* Until this date no CI job type-checked +`+src/abi/+`, and as committed none of the five modules checked: their module +names did not match their paths, `+Types.idr+` and `+Stripping.idr+` had syntax +errors, and `+Stripping.idr+`'s main theorem did not type-check at all. The ✅ +marks below therefore had no receipt before that date. Each module is now +checked on every PR by the `+idris-abi+` job in +`+.github/workflows/proven-tests.yml+` (`+scripts/ci/check-idris-abi.sh+`, Idris2 +0.7.0, `+%default total+`, no `+believe_me+`, `+assert_total+`, +`+assert_smaller+`, `+postulate+` or `+idris_crash+`). PROOF-POLICY §6 deviation, +state open: Idris2 is built from its v0.7.0 tag, because the repo's Guix +manifest and container do not provide it. + * **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+`), +(PROOF-PROGRAMME Layer 1.0 line-comment slice: claimed 2026-06-02 but +never checked; re-proved and checked 2026-11-09), `+AttestationUnforgeability.idr+` (PROOF-PROGRAMME §3.2 ✅ 2026-06-04 — conditional unforgeability from Ed25519 EUF-CMA + chain-hash collision-resistance hypotheses) @@ -34,15 +45,19 @@ top-level theorem. 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. +|*Re-proved 2026-11-09.* The 2026-06-02 proof (issue #113) never +type-checked: its `+//+` case relied on reductions that do not hold for a +variable character, and it used `+decEq+` without importing it. The new proof +shows `+stripLineCommentsIdempotent+` (stripping twice equals stripping once) +through two facts: stripping is the identity on text with no `+//+` +(`+stripIsIdOnClean+`), and the strippers' output has no `+//+` +(`+stripIsClean+`/`+bodyIsClean+`, by mutual induction). `+bodyIsFixedPoint+` +follows. The strippers are restated with explicit `+Bool+` tests. An +exhaustive differential run over every string of length up to 9 on +`+{/, x, \n}+` (29,524 inputs) found no difference from the previous +definitions. A mutant that blanks with `+/+` instead of a space is rejected. +Nine closed sanity theorems, including two comments on different lines and +`+///+`. |Attestation chain unforgeability |`+src/abi/AttestationUnforgeability.idr+` |*PROOF-PROGRAMME §3.2 diff --git a/scripts/ci/check-idris-abi.sh b/scripts/ci/check-idris-abi.sh new file mode 100755 index 0000000..ac6641a --- /dev/null +++ b/scripts/ci/check-idris-abi.sh @@ -0,0 +1,68 @@ +#!/usr/bin/env bash +# SPDX-License-Identifier: MPL-2.0 +# SPDX-FileCopyrightText: 2026 Jonathan D.A. Jewell +# +# Type-check every Idris2 module in src/abi/ and fail loudly on any error or +# escape hatch. This is the receipt for the ABI proofs listed in +# PROOF-NEEDS.adoc: until this ran, none of them had ever been checked. +# +# The files declare `module PanicAttack.ABI.` but live flat in +# src/abi/, and Idris2 requires a module's path to match its name. Moving +# them would break paths cited in legacy A2ML metadata, which agents may not +# edit, so this script stages a module-path view of the unchanged files as +# symbolic links and checks that. The bytes checked are the committed bytes. +# +# Requirements per module: +# * `idris2 --check` succeeds under the pinned Idris2 version; +# * the file states `%default total`; +# * no believe_me, assert_total, assert_smaller, postulate or idris_crash +# outside comments. +# +# Usage: scripts/ci/check-idris-abi.sh (idris2 0.7.0 on PATH) +set -euo pipefail + +IDRIS2_VERSION=0.7.0 +root=$(cd "$(dirname "$0")/../.." && pwd) +abi="$root/src/abi" + +version=$(idris2 --version) +[[ "$version" == "Idris 2, version $IDRIS2_VERSION"* ]] || + { echo "check-idris-abi: need Idris2 $IDRIS2_VERSION, got: $version" >&2; exit 2; } + +stage=$(mktemp -d) +trap 'rm -rf "$stage"' EXIT +mkdir -p "$stage/PanicAttack/ABI" + +failures=0 +shopt -s nullglob +files=("$abi"/*.idr) +[[ ${#files[@]} -gt 0 ]] || { echo "check-idris-abi: no modules in $abi" >&2; exit 2; } + +for file in "${files[@]}"; do + name=$(basename "$file" .idr) + declared=$(sed -n 's/^module[[:space:]]\{1,\}\([A-Za-z0-9_.]*\).*/\1/p' "$file" | head -1) + if [[ "$declared" != "PanicAttack.ABI.$name" ]]; then + echo "FAIL $name: declares module '$declared', expected PanicAttack.ABI.$name" + failures=$((failures + 1)); continue + fi + ln -s "$file" "$stage/PanicAttack/ABI/$name.idr" +done + +for file in "${files[@]}"; do + name=$(basename "$file" .idr) + [[ -L "$stage/PanicAttack/ABI/$name.idr" ]] || continue + # Code lines only: drop `--` and `|||` comment lines before searching. + code=$(grep -vE '^[[:space:]]*(--|\|\|\|)' "$file" || true) + if ! grep -qE '^%default[[:space:]]+total' <<<"$code"; then + echo "FAIL $name: missing %default total"; failures=$((failures + 1)); continue + fi + if hatch=$(grep -nE '\b(believe_me|assert_total|assert_smaller|postulate|idris_crash)\b' <<<"$code"); then + echo "FAIL $name: escape hatch: $hatch"; failures=$((failures + 1)); continue + fi + if out=$(cd "$stage" && idris2 --no-color --check "PanicAttack/ABI/$name.idr" 2>&1); then + echo "PASS $name" + else + echo "FAIL $name"; printf '%s\n' "$out" | sed -n '1,40p'; failures=$((failures + 1)) + fi +done +exit "$failures" diff --git a/src/abi/Stripping.idr b/src/abi/Stripping.idr index 115fdef..32bf438 100644 --- a/src/abi/Stripping.idr +++ b/src/abi/Stripping.idr @@ -2,42 +2,36 @@ -- SPDX-FileCopyrightText: 2026 Jonathan D.A. Jewell -- Copyright (c) 2026 Jonathan D.A. Jewell (hyperpolymath) -||| Comment and String Stripping Idempotence (PROOF-PROGRAMME Layer 1.0) -||| -||| Closes the slash-slash inductive case left open by PR #111 (issue #113). +||| Line-comment stripping idempotence (PROOF-PROGRAMME Layer 1.0) ||| ||| 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. +||| soundness proof: the analyzer's line-comment stripping pass is +||| **idempotent**, so running it twice gives the same output as running +||| it once. That justifies the preprocessing step at +||| `src/assail/analyzer.rs` `strip_proof_comments(without_strings, "//", …)` +||| as a normalising rewrite that every category detector can rely on +||| without re-stripping. ||| -||| Differences from the PR #111 model: +||| The model strips ALL `//` comments: `stripLineCommentBody` hands back +||| to `stripLineComments` after each preserved newline (issue #113). ||| -||| 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. +||| Re-proved 2026-11-09. The previous proof (PR #111, issue #113) never +||| type-checked: its `//` case relied on reductions that do not hold for a +||| variable character, and it used `decEq` without importing it. The proof +||| below goes through two facts instead: ||| -||| 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. +||| * `stripIsIdOnClean`: stripping is the identity on text with no `//`; +||| * `stripIsClean` / `bodyIsClean`: the strippers' output has no `//`. ||| -||| 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. +||| Their composition is `stripLineCommentsIdempotent`. No `believe_me`, +||| `assert_total` or `postulate`; checked by Idris2 0.7.0 under +||| `%default total`. module PanicAttack.ABI.Stripping %default total -- ═══════════════════════════════════════════════════════════════════════ --- Helpers +-- Characters -- ═══════════════════════════════════════════════════════════════════════ ||| The space character used to overwrite stripped regions. @@ -45,201 +39,218 @@ public export sp : Char sp = ' ' -||| The newline character preserved during line-comment stripping (so -||| line numbers in the stripped view match line numbers in the -||| original — critical for the analyzer's location reporting). +||| The newline preserved during stripping, so line numbers in the +||| stripped view match the original (the analyzer reports locations). public export nl : Char nl = '\n' +||| Is this the comment-marker character `/`? +public export +isSlash : Char -> Bool +isSlash c = c == '/' + +||| Is this the newline that ends a line comment? +public export +isNl : Char -> Bool +isNl c = c == nl + +||| Does the list start with `/`? +public export +headIsSlash : List Char -> Bool +headIsSlash [] = False +headIsSlash (d :: _) = isSlash d + -- ═══════════════════════════════════════════════════════════════════════ --- Stripping functions (mirror src/assail/analyzer.rs:931 strip_proof_comments) +-- Stripping functions (mirror strip_proof_comments for "//") -- --- 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. +-- `stripLineComments` copies input until it meets `//`, which it replaces +-- with two spaces before handing the comment body to +-- `stripLineCommentBody`. That blanks every character up to the next +-- newline, keeps the newline, and hands the rest back. Each call works on +-- a strictly smaller suffix of the input. -- ═══════════════════════════════════════════════════════════════════════ 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 line-comment stripper. 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 :: tl) = stripStep (isSlash c) (headIsSlash tl) c tl + + ||| One step on `c` followed by `tl`. The flags say whether `c`, and + ||| the head of `tl`, are `/`: only both together start a comment. + public export + stripStep : Bool -> Bool -> Char -> List Char -> List Char + stripStep True True _ (_ :: rest) = sp :: sp :: stripLineCommentBody rest + stripStep _ _ c tl = c :: stripLineComments tl + + ||| The comment body, from just after `//` to the next newline. 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 (isNl c) rest + + ||| One step of the body: keep the newline and hand back, or blank. + public export + bodyStep : Bool -> List Char -> List Char + bodyStep True rest = nl :: stripLineComments rest + bodyStep False rest = sp :: stripLineCommentBody rest + +-- ═══════════════════════════════════════════════════════════════════════ +-- "No `//`": text the stripper leaves unchanged +-- ═══════════════════════════════════════════════════════════════════════ + +||| `NoDoubleSlash xs`: no `/` in `xs` is immediately followed by `/`. +public export +data NoDoubleSlash : List Char -> Type where + NDSNil : NoDoubleSlash [] + NDSCons : (isSlash c = True -> headIsSlash tl = False) -> + NoDoubleSlash tl -> + NoDoubleSlash (c :: tl) + +spNeverSlash : isSlash Stripping.sp = True -> Void +spNeverSlash Refl impossible + +nlNeverSlash : isSlash Stripping.nl = True -> Void +nlNeverSlash Refl impossible + +-- ═══════════════════════════════════════════════════════════════════════ +-- Fact 1: stripping is the identity on text with no `//` +-- ═══════════════════════════════════════════════════════════════════════ + +||| The step agrees with consing when no comment starts at `c`. +stepIsCons : (b1, b2 : Bool) -> (c : Char) -> (tl : List Char) -> + (b1 = True -> b2 = False) -> + stripLineComments tl = tl -> + stripStep b1 b2 c tl = c :: tl +stepIsCons True True _ _ h _ = absurd (h Refl) +stepIsCons True False c tl _ ih = cong (c ::) ih +stepIsCons False _ c tl _ ih = cong (c ::) ih + +public export +stripIsIdOnClean : (xs : List Char) -> NoDoubleSlash xs -> stripLineComments xs = xs +stripIsIdOnClean [] NDSNil = Refl +stripIsIdOnClean (c :: tl) (NDSCons h rest) = + stepIsCons (isSlash c) (headIsSlash tl) c tl h (stripIsIdOnClean tl rest) -- ═══════════════════════════════════════════════════════════════════════ --- Idempotence — main theorem + body fixed-point lemma, mutual induction +-- Fact 2: the strippers' output has no `//` -- ═══════════════════════════════════════════════════════════════════════ +||| Stripping keeps a non-`/` head, so the output starts with no `/` either. +stripKeepsHead : (tl : List Char) -> headIsSlash tl = False -> + headIsSlash (stripLineComments tl) = False +stripKeepsHead [] _ = Refl +stripKeepsHead (d :: rest) pd = stepHead (isSlash d) (headIsSlash rest) d rest Refl pd + where + stepHead : (b1, b2 : Bool) -> (d : Char) -> (rest : List Char) -> + isSlash d = b1 -> b1 = False -> + headIsSlash (stripStep b1 b2 d rest) = False + stepHead False _ d rest pd' _ = pd' + stepHead True _ _ _ _ Refl impossible + mutual - ||| **Main theorem.** Applying the line-comment stripper twice - ||| equals applying it once. public export - 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) - - ||| **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. + stripIsClean : (xs : List Char) -> NoDoubleSlash (stripLineComments xs) + stripIsClean [] = NDSNil + stripIsClean (c :: tl) = + stepIsClean (isSlash c) (headIsSlash tl) c tl Refl Refl + + stepIsClean : (b1, b2 : Bool) -> (c : Char) -> (tl : List Char) -> + isSlash c = b1 -> headIsSlash tl = b2 -> + NoDoubleSlash (stripStep b1 b2 c tl) + stepIsClean True True _ (_ :: rest) _ _ = + NDSCons (\h => void (spNeverSlash h)) + (NDSCons (\h => void (spNeverSlash h)) (bodyIsClean rest)) + stepIsClean True True _ [] _ Refl impossible + stepIsClean True False c tl _ ptl = + NDSCons (\_ => stripKeepsHead tl ptl) (stripIsClean tl) + stepIsClean False _ c tl pc _ = + NDSCons (\h => absurd (trans (sym h) pc)) (stripIsClean tl) + 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) + bodyIsClean : (xs : List Char) -> NoDoubleSlash (stripLineCommentBody xs) + bodyIsClean [] = NDSNil + bodyIsClean (c :: rest) = bodyStepIsClean (isNl c) rest + + bodyStepIsClean : (b : Bool) -> (rest : List Char) -> + NoDoubleSlash (bodyStep b rest) + bodyStepIsClean True rest = + NDSCons (\h => void (nlNeverSlash h)) (stripIsClean rest) + bodyStepIsClean False rest = + NDSCons (\h => void (spNeverSlash h)) (bodyIsClean rest) -- ═══════════════════════════════════════════════════════════════════════ --- Sanity tests +-- Idempotence +-- ═══════════════════════════════════════════════════════════════════════ + +||| **Main theorem.** Stripping twice equals stripping once. +public export +stripLineCommentsIdempotent : (cs : List Char) -> + stripLineComments (stripLineComments cs) = stripLineComments cs +stripLineCommentsIdempotent cs = stripIsIdOnClean _ (stripIsClean cs) + +||| **Body fixed point.** Stripping the comment body's output changes nothing. +public export +bodyIsFixedPoint : (cs : List Char) -> + stripLineComments (stripLineCommentBody cs) = stripLineCommentBody cs +bodyIsFixedPoint cs = stripIsIdOnClean _ (bodyIsClean cs) + +-- ═══════════════════════════════════════════════════════════════════════ +-- Sanity tests (closed terms, checked by evaluation) -- ═══════════════════════════════════════════════════════════════════════ -||| Empty input: both sides reduce to []. private sanityEmpty : stripLineComments (stripLineComments []) = stripLineComments [] sanityEmpty = Refl -||| Single non-comment char: preserved through both passes. private sanityNonCommentSingleChar : - stripLineComments (stripLineComments ['x']) - = stripLineComments ['x'] + stripLineComments (stripLineComments ['x']) = stripLineComments ['x'] sanityNonCommentSingleChar = Refl -||| Bare `//`: produces `[sp, sp]` then `[sp, sp]` again. private sanityBareCommentMarker : - stripLineComments (stripLineComments ['/', '/']) - = stripLineComments ['/', '/'] + stripLineComments (stripLineComments ['/', '/']) = stripLineComments ['/', '/'] sanityBareCommentMarker = Refl -||| `x//`: char preserved, then sp+sp. private sanityCharPlusCommentMarker : stripLineComments (stripLineComments ['x', '/', '/']) = stripLineComments ['x', '/', '/'] sanityCharPlusCommentMarker = Refl -||| `//x`: comment body strips `x` to `sp`, total `[sp, sp, sp]`. Then -||| second pass is a no-op (no further `//` can form from spaces). +||| `//x` strips to three spaces. private -sanityCommentWithBody : - stripLineComments (stripLineComments ['/', '/', 'x']) - = stripLineComments ['/', '/', 'x'] +sanityCommentWithBody : stripLineComments ['/', '/', 'x'] = [' ', ' ', ' '] sanityCommentWithBody = Refl -||| `//x\\ny`: first pass produces `[sp, sp, sp, nl, y]`. Second pass -||| is the identity. The post-newline `y` is preserved because -||| stripLineCommentBody calls back into stripLineComments which leaves -||| non-comment chars alone. +||| `//x\ny`: the newline and the code after it survive. private sanityCommentThenCode : - stripLineComments (stripLineComments ['/', '/', 'x', '\n', 'y']) - = stripLineComments ['/', '/', 'x', '\n', 'y'] + stripLineComments ['/', '/', 'x', '\n', 'y'] = [' ', ' ', ' ', '\n', 'y'] sanityCommentThenCode = Refl -||| TWO comments separated by a newline. PR #111's broken single-comment -||| model would have left the second `//` unstripped; this corrected -||| mutual-recursion model strips both. +||| Two comments on different lines are both stripped (the case PR #111's +||| single-comment model got wrong). private sanityTwoComments : - stripLineComments (stripLineComments ['/', '/', 'a', '\n', '/', '/', 'b']) - = stripLineComments ['/', '/', 'a', '\n', '/', '/', 'b'] + stripLineComments ['/', '/', 'a', '\n', '/', '/', 'b'] + = [' ', ' ', ' ', '\n', ' ', ' ', ' '] sanityTwoComments = Refl --- ═══════════════════════════════════════════════════════════════════════ --- What still remains (Layer 1.0 future slices) --- ═══════════════════════════════════════════════════════════════════════ +||| A lone `/` is code, not a comment, and is kept. +private +sanityLoneSlash : stripLineComments ['a', '/', 'b'] = ['a', '/', 'b'] +sanityLoneSlash = Refl -||| 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. +||| `///` is a comment whose body starts with `/`. +private +sanityTripleSlash : stripLineComments ['/', '/', '/'] = [' ', ' ', ' '] +sanityTripleSlash = Refl + +-- Future Layer-1.0 slices (PROOF-NEEDS, issue #114): block comments +-- (`/* … */`), string literals with escapes, the composition of the three +-- strippers, and position preservation (the stripped view has the same +-- length and newline positions as the source). diff --git a/src/abi/Types.idr b/src/abi/Types.idr index ee997b1..1afe5c0 100644 --- a/src/abi/Types.idr +++ b/src/abi/Types.idr @@ -18,6 +18,15 @@ import Data.Fin public export data Severity = Info | Warning | Error | Critical +||| Equality on severity, required by `Ord`. +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 +52,7 @@ data ScanOp ||| Language identifier (47 supported, bounded) public export -data LangId = MkLangId (n : Fin 47) +data LangId = MkLangId (Fin 47) -- ═══════════════════════════════════════════════════════════════════════ -- C ABI Exports