Skip to content

Commit c375b7b

Browse files
hyperpolymathhyperpolymath
authored
proof(SafeXML): annotate 9 bodyless decls as OWED (Refs standards#158) (#55)
## Summary Annotates 9 bodyless signatures in `src/Proven/SafeXML/Proofs.idr` as **OWED-with-justification** per the estate convention set 2026-05-20 (SafeChecksum/Buffer/CryptoAccel/HKDF/Bloom/FPGA; siblings #37-54). Each declaration retains its prose docstring + claim, gains an explicit per-decl justification naming the **specific Idris2 0.8.0 blocker** that prevents discharge and the structural refactor or reflective tactic that would unblock it. Multiplicity changed to `0` (erased); no `postulate` keyword; no `believe_me`; no `idris_crash`. Refs hyperpolymath/standards#158. ## Per-decl OWED reasons ### String FFI opacity (8 / 9) The dominant blocker: `prim__eq_String`, `unpack`, and `isInfixOf` over opaque FFI-bound `String` do not reduce by `Refl` in Idris2 0.8.0 (same trust-posture as `Boj.SafetyLemmas.charEqSym`). | # | Decl | OWED claim | Specific blocker | |---|------|-----------|------------------| | 1 | `builderNoXXE` | builder never emits `<!ENTITY ... SYSTEM/PUBLIC ...>` | `NoExternalEntities` predicate's `auto`-found Bool-equality on `isInfixOf` over opaque `renderNode` output | | 2 | `builderNoDTD` | builder never emits `<!DOCTYPE ...>` | `isInfixOf "<!DOCTYPE" (renderNode ...)` over opaque FFI String | | 3 | `builderNoEntities` | rendered output contains no raw entity refs beyond the five predefined | conjunctive `isInfixOf` Bool chain bottoms out in `prim__eq_String` | | 4 | `textEscapingSound` | `xmlText` escapes all `<` to `&lt;` | per-char escape pass through `unpack`/`pack`/`prim__strCons` | | 5 | `attrEscapingSound` | `xmlAttrValue` escapes all `"` to `&quot;` | same `unpack` opacity as 4 | | 6 | `elementNameValidation` | `isOk (xmlName n)` implies `isValidXMLName n` | extensional equality between two opaque `unpack`-based pipelines | | 7 | `qnameComponentsValid` | `isOk (xmlQName p l)` implies both components valid | conjunction across two opaque `isValidXMLName` calls | | 8 | `attrValueNoQuotes` | escaped attribute contains no unescaped `"` | `all` predicate over `unpack` of opaque escaped `String` | ### DOM-traversal `Refl` gap (1 / 9) | # | Decl | OWED claim | Specific blocker | |---|------|-----------|------------------| | 9 | `nestedElementsSafe` | `ProperlyEscaped child` propagates through `build . withChild` | `Element` constructor pattern-match does not propagate child invariant without explicit structural induction on children list | ## Discharge paths Two general routes apply to most items: 1. **Reflective tactics on `unpack` / `isInfixOf`** (estate-wide improvement; would also unblock siblings in SafeChecksum / SafeHtml / SafeString). 2. **Structural refactors** — return types like `EscapedString` / `EscapedAttrValue` indexed by a `List Char` whose constructor character-class excludes the forbidden raw character by construction (item 9 specifically needs a structural induction lemma on `XMLNode` children). ## Compliance with convention - [x] `0 ` erased multiplicity (no runtime presence) - [x] Triple-pipe `||| OWED:` opening line per decl - [x] Specific Idris2 0.8.0 blocker named (not a generic claim) - [x] Discharge precondition named per decl - [x] No `postulate` keyword - [x] No `believe_me` / `idris_crash` - [x] Visibility preserved (`export`, not `public export` — matches the file's pre-existing pattern) - [x] No file outside `src/Proven/SafeXML/Proofs.idr` touched ## Test plan - [ ] Sibling PRs land (estate CI jammed; this is DRAFT) - [ ] Local `idris2 --build proven.ipkg` once the local toolchain is re-wired (this worktree's `idris2 --prefix` resolves to an asdf shim missing its Prelude; not blocking) - [ ] CI green once estate-wide concurrency-pool exhaustion clears 🤖 Generated with [Claude Code](https://claude.com/claude-code)
1 parent df6b0a1 commit c375b7b

1 file changed

Lines changed: 113 additions & 57 deletions

File tree

‎src/Proven/SafeXML/Proofs.idr‎

Lines changed: 113 additions & 57 deletions
Original file line numberDiff line numberDiff line change
@@ -86,18 +86,30 @@ export
8686
secureDefaultsZeroExpansions : Types.secureDefaults.maxEntityExpansions = 0
8787
secureDefaultsZeroExpansions = Refl
8888

89-
||| The builder API never emits <!ENTITY ... SYSTEM/PUBLIC ...> in rendered output.
90-
||| Depends on renderNode implementation which constructs XML from safe primitives
91-
||| and never injects entity declarations.
89+
||| OWED: The builder API never emits `<!ENTITY ... SYSTEM/PUBLIC ...>` in
90+
||| rendered output, because `renderNode` constructs XML from safe primitives
91+
||| (element/text/attribute markup) and never injects entity declarations.
92+
||| Held back by Idris2 0.8.0 not type-level reducing the recursive
93+
||| `renderNode` / `isInfixOf` composition over an opaque `String` —
94+
||| `NoExternalEntities` lives behind `auto`-found Bool-equality proofs on
95+
||| `isInfixOf`, and the FFI-bound `String` primitives do not reduce by
96+
||| `Refl`. Discharge once an `isInfixOf` reflective tactic (or a structural
97+
||| `Data.String` representation supplanting the FFI-opaque one) is
98+
||| available.
9299
export
93-
builderNoXXE : (builder : ElementBuilder) ->
94-
NoExternalEntities (renderNode (build builder))
95-
96-
||| The builder API never emits <!DOCTYPE ...> in rendered output.
97-
||| Depends on renderNode only producing element/text/attribute markup.
100+
0 builderNoXXE : (builder : ElementBuilder) ->
101+
NoExternalEntities (renderNode (build builder))
102+
103+
||| OWED: The builder API never emits `<!DOCTYPE ...>` in rendered output,
104+
||| because `renderNode` only produces element/text/attribute markup and
105+
||| never an `<!DOCTYPE` token. Held back by Idris2 0.8.0 not type-level
106+
||| reducing `isInfixOf "<!DOCTYPE" (renderNode …)` over an opaque
107+
||| FFI-bound `String`. Same blocker family as `builderNoXXE`. Discharge
108+
||| once `isInfixOf` is reflective, or once `renderNode` is refactored to
109+
||| return a structural type that excludes `!DOCTYPE` by construction.
98110
export
99-
builderNoDTD : (builder : ElementBuilder) ->
100-
NoDTD (renderNode (build builder))
111+
0 builderNoDTD : (builder : ElementBuilder) ->
112+
NoDTD (renderNode (build builder))
101113

102114
--------------------------------------------------------------------------------
103115
-- Entity Expansion Proofs
@@ -111,37 +123,54 @@ entityExpansionBounded : (opts : XMLSecurityOptions) -> (count : Nat) ->
111123
()
112124
entityExpansionBounded opts count tooMany = ()
113125

114-
||| The builder escapes & to &amp;, so rendered output contains no raw entity
115-
||| references beyond the five XML predefined entities (&amp; &lt; &gt; &quot; &#39;).
116-
||| Depends on the escaping behaviour of renderNode.
126+
||| OWED: The builder escapes `&` to `&amp;`, so rendered output contains
127+
||| no raw entity references beyond the five XML predefined entities
128+
||| (`&amp;` `&lt;` `&gt;` `&quot;` `&#39;`). Held back by Idris2 0.8.0
129+
||| not type-level reducing `isInfixOf` over `renderNode`'s opaque
130+
||| FFI-bound `String` output — the proof obligation is a Bool equality
131+
||| that bottoms out in `prim__eq_String`, which is class-(J) opaque
132+
||| (same trust posture as `Boj.SafetyLemmas.charEqSym`). Discharge once
133+
||| an `isInfixOf` reflective tactic is available, or once `xmlText` /
134+
||| `xmlAttrValue` return a structural escaped-string type that
135+
||| character-class excludes raw `&` by construction.
117136
export
118-
builderNoEntities : (builder : ElementBuilder) ->
119-
-- Builder escapes & to &amp;, preventing entity references
120-
not (isInfixOf "&" (renderNode (build builder)) &&
121-
not (isInfixOf "&amp;" (renderNode (build builder)) ||
122-
isInfixOf "&lt;" (renderNode (build builder)) ||
123-
isInfixOf "&gt;" (renderNode (build builder)) ||
124-
isInfixOf "&quot;" (renderNode (build builder)))) = True
137+
0 builderNoEntities : (builder : ElementBuilder) ->
138+
-- Builder escapes & to &amp;, preventing entity references
139+
not (isInfixOf "&" (renderNode (build builder)) &&
140+
not (isInfixOf "&amp;" (renderNode (build builder)) ||
141+
isInfixOf "&lt;" (renderNode (build builder)) ||
142+
isInfixOf "&gt;" (renderNode (build builder)) ||
143+
isInfixOf "&quot;" (renderNode (build builder)))) = True
125144

126145
--------------------------------------------------------------------------------
127146
-- Escaping Correctness Proofs
128147
--------------------------------------------------------------------------------
129148

130-
||| xmlText escapes all occurrences of '<' to '&lt;', so the escaped output
131-
||| never contains a raw '<' that could be interpreted as tag injection.
132-
||| Depends on the character-level escaping in xmlText.
149+
||| OWED: `xmlText` escapes all occurrences of `'<'` to `'&lt;'`, so the
150+
||| escaped output never contains a raw `<` that could be interpreted as
151+
||| tag injection. Held back by Idris2 0.8.0 not type-level reducing the
152+
||| per-character escape pass over an opaque FFI-bound `String` —
153+
||| `unpack`/`pack`/`prim__strCons` do not reduce by `Refl`, and
154+
||| `isInfixOf` inherits that opacity. Discharge once a `Data.String`
155+
||| reflective tactic over `unpack` is available, or once `xmlText`
156+
||| returns a structural `EscapedString` whose constructor character-class
157+
||| excludes raw `<`.
133158
export
134-
textEscapingSound : (s : String) ->
135-
let escaped = (xmlText s).escaped
136-
in not (isInfixOf "<" escaped && not (isInfixOf "&lt;" escaped)) = True
137-
138-
||| xmlAttrValue escapes all occurrences of '"' to '&quot;', so the escaped output
139-
||| never contains a raw quote that could break out of attribute context.
140-
||| Depends on the character-level escaping in xmlAttrValue.
159+
0 textEscapingSound : (s : String) ->
160+
let escaped = (xmlText s).escaped
161+
in not (isInfixOf "<" escaped && not (isInfixOf "&lt;" escaped)) = True
162+
163+
||| OWED: `xmlAttrValue` escapes all occurrences of `'"'` to `'&quot;'`,
164+
||| so the escaped output never contains a raw quote that could break out
165+
||| of attribute context. Held back by Idris2 0.8.0 not type-level
166+
||| reducing the per-character escape pass over an opaque FFI-bound
167+
||| `String` (same blocker family as `textEscapingSound`). Discharge once
168+
||| `unpack` is reflective, or once `xmlAttrValue` returns a structural
169+
||| `EscapedAttrValue` whose constructor character-class excludes raw `"`.
141170
export
142-
attrEscapingSound : (s : String) ->
143-
let escaped = (xmlAttrValue s).escaped
144-
in not (isInfixOf "\"" escaped && not (isInfixOf "&quot;" escaped)) = True
171+
0 attrEscapingSound : (s : String) ->
172+
let escaped = (xmlAttrValue s).escaped
173+
in not (isInfixOf "\"" escaped && not (isInfixOf "&quot;" escaped)) = True
145174

146175
||| Theorem: Escaping preserves content semantics
147176
export
@@ -170,20 +199,32 @@ builderElementWellFormed : (builder : ElementBuilder) ->
170199
WellFormed (MkXMLDocument Nothing Nothing (build builder))
171200
builderElementWellFormed builder = MkWellFormed (MkXMLDocument Nothing Nothing (build builder))
172201

173-
||| When xmlName returns Ok, isValidXMLName holds. Depends on xmlName
174-
||| performing the same character checks as isValidXMLName but returning
175-
||| a validated wrapper type (opaque string validation).
202+
||| OWED: When `xmlName` returns `Ok`, `isValidXMLName` holds, because
203+
||| `xmlName` performs the same character checks as `isValidXMLName`
204+
||| before producing the validated wrapper. Held back by Idris2 0.8.0
205+
||| not type-level reducing the two character-check passes to a single
206+
||| `Refl` — both traverse `unpack`, which is FFI-opaque, and the proof
207+
||| requires showing extensional equality between two opaque pipelines.
208+
||| Discharge once `unpack` is reflective, or once `xmlName` is rewritten
209+
||| to call `isValidXMLName` directly (so the two paths share a single
210+
||| reduction).
176211
export
177-
elementNameValidation : (name : String) ->
178-
isOk (xmlName name) = True ->
179-
isValidXMLName name = True
180-
181-
||| When xmlQName returns Ok, both prefix and local components satisfy
182-
||| isValidXMLName. Depends on xmlQName validating each component.
212+
0 elementNameValidation : (name : String) ->
213+
isOk (xmlName name) = True ->
214+
isValidXMLName name = True
215+
216+
||| OWED: When `xmlQName` returns `Ok`, both `pfx` and `local`
217+
||| individually satisfy `isValidXMLName`, because `xmlQName` validates
218+
||| each component before composing them. Held back by Idris2 0.8.0 not
219+
||| type-level reducing the conjunction across two opaque
220+
||| `isValidXMLName` calls (same `unpack` opacity blocker as
221+
||| `elementNameValidation`). Discharge once `unpack` is reflective, or
222+
||| once `xmlQName` is rewritten to compose `xmlName pfx` and
223+
||| `xmlName local` so the two arms expose their underlying checks.
183224
export
184-
qnameComponentsValid : (pfx : String) -> (local : String) ->
185-
isOk (xmlQName pfx local) = True ->
186-
(isValidXMLName pfx = True, isValidXMLName local = True)
225+
0 qnameComponentsValid : (pfx : String) -> (local : String) ->
226+
isOk (xmlQName pfx local) = True ->
227+
(isValidXMLName pfx = True, isValidXMLName local = True)
187228

188229
--------------------------------------------------------------------------------
189230
-- Depth Limiting Proofs
@@ -208,13 +249,19 @@ builderDepthConstant builder = ()
208249
-- Attribute Safety Proofs
209250
--------------------------------------------------------------------------------
210251

211-
||| xmlAttrValue replaces all '"' characters with '&quot;', so the escaped
212-
||| attribute value contains no unescaped double-quote characters.
213-
||| Depends on the character-level escaping in xmlAttrValue.
252+
||| OWED: `xmlAttrValue` replaces all `'"'` characters with `'&quot;'`,
253+
||| so the escaped attribute value contains no unescaped double-quote
254+
||| characters. Held back by Idris2 0.8.0 not type-level reducing
255+
||| `all (\c => c /= '"' || False)` over `unpack` of an opaque FFI-bound
256+
||| `String` — the `unpack` produces a `List Char` whose elements are
257+
||| FFI-opaque, and the predicate's `Bool` reduction inherits that
258+
||| opacity. Discharge once `unpack` is reflective, or once
259+
||| `xmlAttrValue` returns a structural `EscapedAttrValue` indexed by a
260+
||| `List Char` whose constructor excludes `'"'` by construction.
214261
export
215-
attrValueNoQuotes : (value : String) ->
216-
let attrVal = xmlAttrValue value
217-
in all (\c => c /= '"' || False) (unpack attrVal.escaped) = True
262+
0 attrValueNoQuotes : (value : String) ->
263+
let attrVal = xmlAttrValue value
264+
in all (\c => c /= '"' || False) (unpack attrVal.escaped) = True
218265

219266
||| Theorem: Attribute count is bounded
220267
export
@@ -253,13 +300,22 @@ piNotXmlDecl target isXml = ()
253300
-- Composition Proofs
254301
--------------------------------------------------------------------------------
255302

256-
||| Adding a properly-escaped child to a builder preserves the ProperlyEscaped
257-
||| property on the built output. Depends on withChild not altering the
258-
||| child's escaped content and build composing children safely.
303+
||| OWED: Adding a properly-escaped child to a builder preserves the
304+
||| `ProperlyEscaped` property on the built output, because `withChild`
305+
||| does not alter the child's escaped content and `build` composes
306+
||| children without re-escaping. Held back by Idris2 0.8.0 not
307+
||| type-level reducing `build . withChild child` to the child-level
308+
||| `ProperlyEscaped` witness through the `XMLNode` tree-traversal
309+
||| (DOM-traversal `Refl` gap — the `Element` constructor pattern-match
310+
||| does not propagate the child invariant without an explicit induction
311+
||| on the children list). Discharge once a structural induction lemma
312+
||| on `XMLNode` children is written, or once `ProperlyEscaped` is
313+
||| refactored to a structurally-recursive proof over the `XMLNode`
314+
||| constructors.
259315
export
260-
nestedElementsSafe : (parent : ElementBuilder) -> (child : XMLNode) ->
261-
ProperlyEscaped child ->
262-
ProperlyEscaped (build (withChild child parent))
316+
0 nestedElementsSafe : (parent : ElementBuilder) -> (child : XMLNode) ->
317+
ProperlyEscaped child ->
318+
ProperlyEscaped (build (withChild child parent))
263319

264320
||| Theorem: Multiple children preserve well-formedness
265321
export

0 commit comments

Comments
 (0)