Skip to content

Commit f3ebd99

Browse files
hyperpolymathclaude
hyperpolymath
and
claude
authored
proof(SafeSQL): annotate 3 bodyless decls as OWED (Refs standards#158) (#47)
## Summary Converts the three bodyless declarations in `src/Proven/SafeSQL/Proofs.idr` from terse `Depends on …` comments to the estate's **OWED-with-justification** convention established 2026-05-20 across SafeChecksum / SafeAPIKey / SafeCORS / SafeCSV / SafeSemVer / SafeHtml: - Triple-pipe `|||` doc-comment stating the claim - `0 ` (erased multiplicity) so the postulate is not runtime-callable - Bare signature, no `postulate` keyword - Explicit Idris2 0.8.0 blocker + discharge condition Refs hyperpolymath/standards#158. ## The three OWED items ### 1. `escapeStringQuotesSafe` **Claim.** For every dialect `d` and input `s`, `escapeString d s` satisfies `NoUnescapedQuotes`. **Why OWED.** Operationally witnessed by `Proven.SafeSQL.Params.escapeString`, which wraps the input in single quotes and doubles every internal `'\''` (`'\'' :: cs |-> "''" ++ escape cs`) — by case-analysis every output position is either a non-quote source char, a dialect-specific escape sequence, or a doubled `''`, so no raw unescaped `'\''` remains. Held back by Idris2 0.8.0 not reducing `unpack` / `pack` / `++` / `singleton` over abstract `String` at the type level — these are FFI-bound String primitives, so `all (\c => c /= '\'') (unpack (escapeString d s))` does not normalise to `True` by Refl alone. Same blocker family as SafeChecksum's `luhnValidatesKnownGood` and SafeHtml's `escapePreservesNoLT`. **Discharge.** A `Data.String` reflective tactic, or per-character induction lemma over `unpack . concat . map`. ### 2. `identifierCharsSafe` **Claim.** If `isValidIdentifier s = True` then `IsSafeIdentifier s`. **Why OWED.** Operationally `isValidIdentifier` (in `Proven.SafeSQL.Types`) is the conjunction `(isAlpha c0 || c0 == '_') && all isIdentifierChar (unpack rest) && length s <= 128`, which directly mirrors the three fields of `MkSafeIdent` (validChars / notEmpty / notTooLong) — so the witness is structurally derivable from the Boolean proof. Held back by Idris2 0.8.0 not reducing `strM` / `unpack` / `length` over abstract `String` at the type level — the conjunction does not split into its three component `Refl`s by Refl alone, and the `notEmpty : length s > 0 = True` field cannot be projected from `isValidIdentifier s = True` without per-character induction. Same blocker family as SafeHtml's `sanitizeRemovesScripts`. **Discharge.** A `Data.String` reflective tactic for `strM` / `unpack` / `length`, or refactor `isValidIdentifier` to return a structural witness (e.g. `Dec (IsSafeIdentifier s)`) instead of a `Bool`. ### 3. `parameterizedQueriesSafe` **Claim.** Every `ParameterizedQuery q` satisfies `IsParameterized q`. **Why OWED.** `QueryFragment` has exactly four constructors (`Literal`, `Param`, `NamedParam`, `Identifier`) and `isParamOrLiteral` returns `True` on all four — so the predicate is total-by-exhaustion and the witness is constructible by induction over `q.fragments`. Held back by Idris2 0.8.0 not reducing `all` (`Data.List`) at the type level over an abstract `List QueryFragment` — the inductive case `all isParamOrLiteral (f :: fs) = isParamOrLiteral f && all isParamOrLiteral fs` cannot be discharged without a `Data.List.all`-reflection lemma. The current `ParameterizedQuery` record also does not carry the invariant in its constructor, so a manufactured `q` with a future non-paramic fragment would not be ruled out by typing. **Discharge.** Either (a) a `Data.List.all` reflective tactic + a per-fragment lemma, or (b) refactor `ParameterizedQuery` to carry an `IsParameterized` field at construction (intrinsic invariant). ## Safety posture - Zero `believe_me` - Zero `postulate` - Zero `idris_crash` - All `0 `-erased — postulates cannot leak into runtime - Discoverable as named declarations (vs silent / commented-out) ## Caveat / follow-up Unlike SafeHtml / SafeCSV / SafeAPIKey / SafeCORS / SafeSemVer (whose OWED decls are only referenced from outside the file), in this module the three OWED decls are *also* called by four downstream provers inside the same file: `builderQueriesSafe`, `cannotEscapeStringLiteral`, `combinePreservesSafety`, `addParamPreservesSafety`. Those provers' result types (`InjectionSafe q`, `NoUnescapedQuotes escaped`) are themselves propositions, so promoting them to `0`-erased too is the clean follow-up if Idris2 0.8.0's erasure check rejects the W-context call sites once CI thaws. Kept out of scope here per the standards#158 sibling-PR convention (one PR = OWED annotation only). ## Test plan - [ ] Idris2 0.8.0 `--check` on `src/Proven/SafeSQL/Proofs.idr` once estate base-package dependency resolution is unjammed (CI is currently jammed estate-wide — DRAFT until then) - [ ] If the four downstream provers' W-context calls fail erasure, open a follow-up PR promoting them to `0` too - [ ] Verify no downstream module shadows the names (grep was clean at edit time — only this file references them) - [ ] Owner review of OWED reasons against SafeChecksum / SafeHtml precedent Refs hyperpolymath/standards#158. Co-authored-by: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
1 parent eda8ebd commit f3ebd99

1 file changed

Lines changed: 62 additions & 17 deletions

File tree

‎src/Proven/SafeSQL/Proofs.idr‎

Lines changed: 62 additions & 17 deletions
Original file line numberDiff line numberDiff line change
@@ -97,28 +97,73 @@ data IsEscapedValue : SQLDialect -> SQLValue -> Type where
9797
-- Core Safety Theorems
9898
--------------------------------------------------------------------------------
9999

100-
||| Theorem: escapeString produces a string with no unescaped single quotes
100+
||| OWED: for every dialect `d` and input `s`, the result of
101+
||| `escapeString d s` satisfies `NoUnescapedQuotes`. Operationally
102+
||| witnessed by `Proven.SafeSQL.Params.escapeString`, which wraps the
103+
||| input in single quotes and doubles every internal `'\''`
104+
||| (`'\'' :: cs |-> "''" ++ escape cs`) — by case-analysis every
105+
||| position of the output is either a non-quote source char, a
106+
||| dialect-specific escape sequence, or a doubled `''`, so no raw
107+
||| unescaped `'\''` remains.
101108
|||
102-
||| The escaping function doubles all single quotes, making it impossible
103-
||| for user input to break out of a string literal.
104-
||| Depends on the correctness of escapeString in Proven.SafeSQL.Params.
109+
||| Held back by Idris2 0.8.0 not reducing `unpack` / `pack` / `++` /
110+
||| `singleton` over abstract `String` at the type level — these are
111+
||| FFI-bound String primitives, so `all (\c => c /= '\'')
112+
||| (unpack (escapeString d s))` does not normalise to `True` by Refl
113+
||| alone for an abstract `s`. Same blocker family as SafeChecksum's
114+
||| `luhnValidatesKnownGood` and SafeHtml's `escapePreservesNoLT`
115+
||| (opaque String FFI). Discharge once a `Data.String` reflective
116+
||| tactic or per-character induction lemma over
117+
||| `unpack . concat . map` is available.
105118
export
106-
escapeStringQuotesSafe : (d : SQLDialect) -> (s : String) ->
107-
NoUnescapedQuotes (escapeString d s)
108-
109-
||| Theorem: ValidIdentifier strings contain only safe characters
110-
||| Depends on isValidIdentifier checking character validity, length > 0, and length <= 128.
119+
0 escapeStringQuotesSafe : (d : SQLDialect) -> (s : String) ->
120+
NoUnescapedQuotes (escapeString d s)
121+
122+
||| OWED: if `isValidIdentifier s = True` then `IsSafeIdentifier s`.
123+
||| Operationally `isValidIdentifier` (in `Proven.SafeSQL.Types`) is
124+
||| the conjunction `(isAlpha c0 || c0 == '_') && all isIdentifierChar
125+
||| (unpack rest) && length s <= 128`, which directly mirrors the
126+
||| three fields of `MkSafeIdent` (validChars / notEmpty / notTooLong)
127+
||| — so the witness is structurally derivable from the Boolean proof.
128+
|||
129+
||| Held back by Idris2 0.8.0 not reducing `strM` / `unpack` /
130+
||| `length` over abstract `String` at the type level — these are
131+
||| FFI-bound String primitives, so the conjunction does not split
132+
||| into its three component `Refl`s by Refl alone, and the
133+
||| `notEmpty : length s > 0 = True` field cannot be projected from
134+
||| `isValidIdentifier s = True` without per-character induction.
135+
||| Same blocker family as SafeHtml's `sanitizeRemovesScripts`
136+
||| (opaque String FFI). Discharge once a `Data.String` reflective
137+
||| tactic for `strM` / `unpack` / `length` is available, or
138+
||| `isValidIdentifier` is refactored to return a structural witness
139+
||| (e.g. `Dec (IsSafeIdentifier s)`) instead of a `Bool`.
111140
export
112-
identifierCharsSafe : (s : String) -> (prf : isValidIdentifier s = True) ->
113-
IsSafeIdentifier s
114-
115-
||| Theorem: Parameterized queries separate data from code
141+
0 identifierCharsSafe : (s : String) -> (prf : isValidIdentifier s = True) ->
142+
IsSafeIdentifier s
143+
144+
||| OWED: every `ParameterizedQuery` value `q` satisfies
145+
||| `IsParameterized q`, i.e. every fragment in `q.fragments`
146+
||| satisfies `isParamOrLiteral`. Operationally true because
147+
||| `QueryFragment` has exactly four constructors (`Literal`, `Param`,
148+
||| `NamedParam`, `Identifier`) and `isParamOrLiteral` returns `True`
149+
||| on all four — so the predicate is total-by-exhaustion and the
150+
||| witness is constructible by induction over `q.fragments`.
116151
|||
117-
||| When using parameterized queries, user input is never parsed as SQL
118-
||| because parameters are bound separately from the query structure.
119-
||| Depends on the query builder only producing Literal, Param, NamedParam, and Identifier fragments.
152+
||| Held back by Idris2 0.8.0 not reducing `all` (`Data.List`) at the
153+
||| type level over an abstract `List QueryFragment` — `all f xs`
154+
||| does not normalise to `True` by Refl alone for an opaque `xs`,
155+
||| so the structural induction case `all isParamOrLiteral
156+
||| (f :: fs) = isParamOrLiteral f && all isParamOrLiteral fs`
157+
||| cannot be discharged without a `Data.List.all`-reflection lemma.
158+
||| The current `ParameterizedQuery` record also does not carry the
159+
||| invariant in its constructor, so a manufactured `q` with a future
160+
||| non-paramic fragment would not be ruled out by typing. Same
161+
||| blocker family as the String-FFI OWED set. Discharge once either
162+
||| (a) a `Data.List.all` reflective tactic + a per-fragment lemma is
163+
||| available, or (b) `ParameterizedQuery` is refactored to carry an
164+
||| `IsParameterized` field at construction (intrinsic invariant).
120165
export
121-
parameterizedQueriesSafe : (q : ParameterizedQuery) -> IsParameterized q
166+
0 parameterizedQueriesSafe : (q : ParameterizedQuery) -> IsParameterized q
122167

123168
||| Theorem: All SQLValue types are safely escapable
124169
export

0 commit comments

Comments
 (0)