From 5157bbabee56d9f969f66135dd41b8530d0f7d68 Mon Sep 17 00:00:00 2001 From: hyperpolymath <6759885+hyperpolymath@users.noreply.github.com> Date: Thu, 21 May 2026 09:14:40 +0100 Subject: [PATCH 1/2] proof(xml-7-44): make Xml744.Escape.exfiltrate provably total MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit The `replaceAll` worker inside `exfiltrate` used three `assert_total` escapes (`strHead`, `head`, `tail`) on Idris2 0.7 stdlib, and the intermediate refactor that removed them broke the termination check (recursion through `pack $ drop ...` is not structurally smaller). Rewrite the worker as `replaceAllChars : Nat -> List Char -> ...` with a fuel parameter sized to `length (unpack str)`. Each recursive step consumes ≥ 1 char of the third argument so fuel is never the binding constraint — it simply makes termination structurally obvious to Idris2's checker, matching the Nat-fueled pattern used in the ephapax totality campaign. `idris2 --check Xml744/Escape.idr` reports all four exported names (`exfiltrate`, `infiltrate`, `infiltrateAttr`, `makeSafe`) as `total`, with no `assert_total` / `assert_smaller` / `believe_me` left in the file. Co-Authored-By: Claude Opus 4.7 (1M context) --- .../xml-toolkit/src/Xml744/Escape.idr | 26 ++++++++++++------- 1 file changed, 16 insertions(+), 10 deletions(-) diff --git a/idris2-ecosystem/xml-toolkit/src/Xml744/Escape.idr b/idris2-ecosystem/xml-toolkit/src/Xml744/Escape.idr index e01bd36b..92323c3b 100644 --- a/idris2-ecosystem/xml-toolkit/src/Xml744/Escape.idr +++ b/idris2-ecosystem/xml-toolkit/src/Xml744/Escape.idr @@ -48,6 +48,11 @@ infiltrateAttr : String -> String infiltrateAttr = concatMap escapeAttrChar . unpack ||| Exfiltrate: safely extract content from XML (unescape entities) +||| +||| The worker `replaceAllChars` recurses on a `Nat` fuel sized to the input. +||| Each step consumes at least one character of the third argument, so the +||| fuel bound is never reached in practice — it exists to make termination +||| structurally obvious to Idris2 without `assert_total` / `assert_smaller`. export exfiltrate : String -> String exfiltrate s = @@ -58,18 +63,19 @@ exfiltrate s = s5 = replaceAll "'" "'" s4 in s5 where + replaceAllChars : Nat -> List Char -> List Char -> List Char -> List Char + replaceAllChars _ _ _ [] = [] + replaceAllChars _ [] _ xs = xs + replaceAllChars Z _ _ xs = xs + replaceAllChars (S k) (f :: fs) to (x :: xs) = + if isPrefixOf (f :: fs) (x :: xs) + then to ++ replaceAllChars k (f :: fs) to (drop (length fs) xs) + else x :: replaceAllChars k (f :: fs) to xs + replaceAll : String -> String -> String -> String replaceAll from to str = - case unpack from of - [] => str -- empty search string, return unchanged - (fc :: _) => - case break (== fc) (unpack str) of - (before, []) => str - (before, (r :: rs)) => - if isPrefixOf (unpack from) (r :: rs) - then pack before ++ to ++ replaceAll from to (pack $ drop (length from) (r :: rs)) - else pack before ++ singleton r ++ - replaceAll from to (pack rs) + let chars = unpack str + in pack (replaceAllChars (length chars) (unpack from) (unpack to) chars) ||| Check if a string contains any unescaped dangerous characters export From 95455645935c22997028b0b262003b6ed3d27cd4 Mon Sep 17 00:00:00 2001 From: hyperpolymath <6759885+hyperpolymath@users.noreply.github.com> Date: Thu, 21 May 2026 10:08:25 +0100 Subject: [PATCH 2/2] proof(xml-7-44): discharge Xml744.Attribute proof debts MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Two PROOF_TODO sites in `Xml744.Attribute` blocked the toolkit build on Idris2 0.8.0: 1. `attrName s = case decEq (isValidName s) True of ...` — `decEq` for `Bool` is not in scope with the current imports. Replace with the `with proof` form, which binds `prf : isValidName s = True` directly in the matched branch and discharges `MkAttrName`'s auto-implicit. 2. `unsafeAttrName s = cast (MkAttrName s)` — never compiled (no matching `Cast` instance; `MkAttrName` requires the validity proof to construct). Change `unsafeAttrName` to take the proof as an auto-implicit, so it can only be called on strings whose validity Idris2 can verify at elaboration time. `Refl` discharges the proof for any literal (or compile-time-reducible string), matching the existing comment that this constructor "use only for known-good literals". `wAttr` previously routed through `unsafeAttrName` on a `("w:" ++ n)` runtime string. Bump its signature to `(n : String) -> {auto prf : isValidName ("w:" ++ n) = True} -> String -> XmlAttr` so the callers' literal `n` lets the elaborator reduce both the concatenation and `isValidName` to `True`. All four existing `wAttr` call sites pass literals (`"id"`, `"author"`, `"date"`, `"initials"`). Promote `isNameStartChar`, `isNameChar`, and `isValidName` from `export` to `public export` so cross-module callers see the definitions and the elaborator can reduce them. Without this the proofs only discharge inside `Xml744.Attribute` itself. Build outcome: 3/6 → Attribute compiles; all 9 exports check `is total`; no `assert_total` / `assert_smaller` / `believe_me` / `PROOF_TODO` / `idris_crash` remain in the file. Build still red downstream in `Xml744.Element` (parallel `decEq` / `cast` debts plus untreated mutual-recursion totality) — separate follow-up, not in scope for this branch. Co-Authored-By: Claude Opus 4.7 (1M context) --- .../xml-toolkit/src/Xml744/Attribute.idr | 48 +++++++++++++------ 1 file changed, 33 insertions(+), 15 deletions(-) diff --git a/idris2-ecosystem/xml-toolkit/src/Xml744/Attribute.idr b/idris2-ecosystem/xml-toolkit/src/Xml744/Attribute.idr index a2e8209b..a6bc5588 100644 --- a/idris2-ecosystem/xml-toolkit/src/Xml744/Attribute.idr +++ b/idris2-ecosystem/xml-toolkit/src/Xml744/Attribute.idr @@ -9,15 +9,22 @@ import Data.List %default total -||| Valid XML name characters (simplified - ASCII subset) +||| Valid XML name characters (simplified - ASCII subset). +||| +||| `public export` so cross-module callers of `unsafeAttrName` / `wAttr` on +||| string literals can have the auto-implicit `isValidName s = True` proof +||| discharged by elaboration-time reduction. With plain `export` only the +||| name is visible and reduction is blocked. +public export isNameStartChar : Char -> Bool isNameStartChar c = isAlpha c || c == '_' || c == ':' +public export isNameChar : Char -> Bool isNameChar c = isNameStartChar c || isDigit c || c == '-' || c == '.' -||| Check if a string is a valid XML name -export +||| Check if a string is a valid XML name. +public export isValidName : String -> Bool isValidName s = case unpack s of [] => False @@ -28,19 +35,26 @@ public export data AttrName : Type where MkAttrName : (n : String) -> {auto prf : isValidName n = True} -> AttrName -||| Try to create an attribute name (returns Nothing if invalid) +||| Try to create an attribute name (returns Nothing if invalid). +||| +||| The `with proof` form binds `prf : isValidName s = True` in the matched +||| branch, which discharges `MkAttrName`'s auto-implicit. Replaces the +||| previous `decEq (isValidName s) True` form — `decEq` for `Bool` is not in +||| scope on Idris2 0.8.0 with the current imports. export attrName : (s : String) -> Maybe AttrName -attrName s = case decEq (isValidName s) True of - Yes prf => Just (MkAttrName s) - No _ => Nothing - -||| Unsafe attribute name creation (use only for known-good literals) +attrName s with (isValidName s) proof prf + attrName s | True = Just (MkAttrName s) + attrName s | False = Nothing + +||| Attribute-name constructor for string literals whose validity Idris2 +||| can verify at elaboration time. The auto-implicit `isValidName s = True` +||| is discharged by `Refl` for any literal (or compile-time-known) string. +||| Replaces the previous `cast (MkAttrName s)` placeholder, which never +||| compiled (no matching `Cast` instance, and `MkAttrName` needs the proof). export -unsafeAttrName : String -> AttrName --- PROOF_TODO: Replace cast with actual proof --- PROOF_TODO: Replace cast with actual proof -unsafeAttrName s = cast (MkAttrName s) +unsafeAttrName : (s : String) -> {auto prf : isValidName s = True} -> AttrName +unsafeAttrName s = MkAttrName s ||| Common attribute names as constants export @@ -77,9 +91,13 @@ export getAttrValue : XmlAttr -> String getAttrValue (MkAttr _ v) = exfiltrate v -||| Convenience for common w: namespace attributes (OOXML) +||| Convenience for common w: namespace attributes (OOXML). +||| +||| The auto-implicit proof obligation `isValidName ("w:" ++ n) = True` is +||| discharged at the call site by `Refl` for any literal `n` (the elaborator +||| reduces both the string concatenation and `isValidName` on closed terms). export -wAttr : String -> String -> XmlAttr +wAttr : (n : String) -> {auto prf : isValidName ("w:" ++ n) = True} -> String -> XmlAttr wAttr n v = attr (unsafeAttrName ("w:" ++ n)) v ||| Example: attribute that would break with raw quotes