Skip to content

Commit e4759a5

Browse files
hyperpolymathhyperpolymath
authored
ci+proof: fix proof-check gate + repair 5 never-compiled proofs (#148)
Corrects the #147 proof-check gate (run from src/ with module-relative paths; scope to the *.Proofs modules listed in proven.ipkg, not all 93 on-disk) and repairs the 5 "DISCHARGED" theorems it surfaced that never type-checked on a clean idris2-0.8.0 + contrib toolchain: - SafeUrl: appendAssociative -> sym (Data.List.appendAssociative ...); addParamIncreasesCount -> lengthSnoc arg order. Both genuinely hold. - SafeSQL: builderQueriesSafe, cannotEscapeStringLiteral, combinePreservesSafety, addParamPreservesSafety reverted DISCHARGED -> OWED (they consumed erased OWED premises -- "not accessible in context"). - SafeEmail: validResultIsValid reverted DISCHARGED -> OWED (Idris2 0.8.0 won't reduce a top-level constant's record projection cross-module). All 29 ipkg proof modules now compile (proof-check green). No believe_me / postulate / idris_crash introduced. STATE.a2ml discharged-decls 36 -> 31. The remaining governance / Language / package anti-pattern policy failure is pre-existing (hyperpolymath/standards) and out of scope.
1 parent 9c33f00 commit e4759a5

5 files changed

Lines changed: 101 additions & 66 deletions

File tree

‎.github/workflows/idris2-ci.yml‎

Lines changed: 21 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -144,24 +144,41 @@ jobs:
144144
- name: Add Idris 2 to PATH
145145
run: echo "$HOME/.idris2/bin" >> $GITHUB_PATH
146146

147-
- name: Type check every Proofs.idr
147+
- name: Type check the proof modules in proven.ipkg
148+
# Scope: every `*.Proofs` module LISTED IN proven.ipkg — i.e. the proof
149+
# modules the package actually builds. (64 of the 93 Proofs.idr files on
150+
# disk are intentionally absent from the package: env-blocked on retired
151+
# stdlib like Data.Nat.Division, or work-in-progress. Gating on those
152+
# would be stricter than `build` itself.)
153+
#
154+
# Run from the package source root (proven.ipkg `sourcedir = src`) with
155+
# module-relative paths. Idris2 matches a module's dotted namespace
156+
# against trailing path segments, so `Proven/Foo/Proofs.idr` resolves
157+
# `module Proven.Foo.Proofs` whereas `src/Proven/Foo/Proofs.idr` raises a
158+
# spurious "module name does not match file name". The clean `build/`
159+
# removal guarantees a stale TTC cannot mask a real break.
148160
run: |
149161
set -uo pipefail
162+
grep -oE 'Proven\.[A-Za-z0-9]+(\.[A-Za-z0-9]+)*\.Proofs' proven.ipkg \
163+
| sort -u | sed 's#\.#/#g; s#$#.idr#' > /tmp/proof_modules.txt
164+
echo "Proof modules from proven.ipkg:"; cat /tmp/proof_modules.txt
165+
cd src
150166
rm -rf build
151167
fail=0
152168
checked=0
153169
while IFS= read -r f; do
170+
[ -f "$f" ] || { echo "::error file=proven.ipkg::listed proof module missing on disk: src/$f"; fail=1; continue; }
154171
checked=$((checked + 1))
155172
echo "::group::idris2 --check $f"
156173
if idris2 -p contrib -p network --check "$f"; then
157174
echo "PASS $f"
158175
else
159-
echo "::error file=$f::idris2 --check failed"
176+
echo "::error file=src/$f::idris2 --check failed"
160177
fail=1
161178
fi
162179
echo "::endgroup::"
163-
done < <(find src -name 'Proofs.idr' | sort)
164-
echo "Checked $checked Proofs.idr module(s); fail=$fail"
180+
done < /tmp/proof_modules.txt
181+
echo "Checked $checked proof module(s); fail=$fail"
165182
exit "$fail"
166183
167184
docs:

‎.machine_readable/6a2/STATE.a2ml‎

Lines changed: 12 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -30,11 +30,18 @@ bodyless-decls-total = 256
3030
# SafeChecksum convention. See PROOF-NEEDS.md "OWED-with-justification
3131
# convention" and META.a2ml ADR-001.
3232

33-
discharged-decls = 36
33+
discharged-decls = 31
3434
# DISCHARGED entries (OWED → proven Refl or contrib-lemma) landed
35-
# across Phase 3 PRs #97-124 (2026-05-30 session) + #144 (2026-05-31:
36-
# SafeJson anyMatchesTAny, singleKeyPath). Each PR converts one OWED to
37-
# a machine-checked theorem.
35+
# across Phase 3 PRs #97-124 (2026-05-30) + #144 (SafeJson anyMatchesTAny,
36+
# singleKeyPath). 2026-05-31 honesty correction (#147 proof-check gate):
37+
# the new gate type-checked all 29 ipkg proof modules on a clean toolchain
38+
# and found 5 that never actually compiled — "DISCHARGED" theorems merged
39+
# without a verifying build. Repaired: SafeUrl appendAssociative (wrong
40+
# contrib name) + addParamIncreasesCount (lengthSnoc arg order) now
41+
# genuinely hold; SafeSQL builderQueriesSafe / cannotEscapeStringLiteral /
42+
# combinePreservesSafety / addParamPreservesSafety reverted to OWED (they
43+
# consumed erased OWED premises); SafeEmail validResultIsValid reverted to
44+
# OWED (top-level-constant projection opacity). Net: 36 → 31 honest.
3845

3946
[trust-posture]
4047
believe-me-uses = 0
@@ -66,6 +73,7 @@ scorecard-fuzzing-source-fixed = "PR #121 (real ClusterFuzzLite + cargo-fuzz)"
6673

6774
[session-history]
6875
# Most recent first.
76+
"2026-05-31b" = "CI proof-gate (#147 → #148): added a fast `proof-check` job type-checking every *.Proofs module listed in proven.ipkg (29) from src/ with module-relative paths; fixed two self-inflicted gate bugs (repo-root path → spurious 'module name does not match file name'; over-broad glob over all 93 on-disk vs the 29 ipkg-built). The gate found 5 ipkg proof modules that never compiled (DISCHARGED-but-unbuilt, same disease as #127): SafeUrl appendAssociative (referenced nonexistent Data.List.Equalities.appendAssociative; fixed to sym (Data.List.appendAssociative)) + addParamIncreasesCount (lengthSnoc arg order) now genuinely hold; SafeSQL ×4 and SafeEmail ×1 reverted DISCHARGED→OWED (depended on erased OWED premises / top-level-constant opacity). All 29 now green on a clean idris2-0.8.0+contrib build. ADR-004."
6977
"2026-05-31" = "SafeJson Phase 3: #144 DISCHARGES anyMatchesTAny (6-arm split) + singleKeyPath (with-pattern), completing #138. Root-caused a pre-existing breakage: appendLengthInc (from #127) used `lengthSnoc arr v` but contrib Data.List.Equalities.lengthSnoc is element-first — it failed to type-check and blocked the ENTIRE SafeJson.Proofs module (so main did not compile). Fixed to `lengthSnoc v arr`. Verified on a clean idris2-0.8.0+contrib install (full SafeJson cone, 0 errors). Filed #145: the Idris build is not a required status check, so #127's broken merge went green (created→merged in ~2.5min with build jobs still queued); recommends branch-protection gating + faster cone-check job."
7078
"2026-05-30" = "Phase 3 discharge: PRs #97-124 land (~28 OWED→DISCHARGED conversions). Security tab cleanup: source-fixes for #2 / #296 / #299 + branch-protection safe-subset + 100 Hypatia FP alerts dismissed at API. Estate-wide CSA self-echo bulk-dismiss sweep (~9050 alerts) running in background."
7179
"2026-05-20" = "Fork A campaign complete: 250 bodyless decls across 28 of 41 modules annotated via OWED-with-justification convention (PRs #37-64, Refs standards#158); cross-prover audit confirms 0 Lean sorry / 0 Coq Admitted in first-party code (only echidnabot dogfood fixtures)"

‎src/Proven/SafeEmail/Proofs.idr‎

Lines changed: 14 additions & 7 deletions
Original file line numberDiff line numberDiff line change
@@ -64,14 +64,21 @@ parseDeterministic s = Refl
6464
-- Validation Properties
6565
--------------------------------------------------------------------------------
6666

67-
||| DISCHARGED: `validResult.isValid = True`. By definition
68-
||| `validResult = MkValidationResult True []` (Validation.idr L62)
69-
||| and `validResult` is `public export`, so the elaborator unfolds
70-
||| `validResult.isValid` to `(MkValidationResult True []).isValid =
71-
||| True` by direct record-projection reduction.
67+
||| OWED: `validResult.isValid = True`. Operationally immediate —
68+
||| `validResult = MkValidationResult True []` (Validation.idr L62) — but
69+
||| Idris2 0.8.0 does not reduce the projection of a top-level constant
70+
||| (`validResult.isValid`) by `Refl`, even with `ValidationResult` and
71+
||| `validResult` both `public export`. Verified: the same
72+
||| `Can't solve constraint between: True and validResult.isValid` arises
73+
||| in a minimal cross-module repro. Same top-level-constant-opacity
74+
||| blocker as `SafePassword.chainedBuildersCompose` and
75+
||| `SafeCSV.defaultDelimiterIsComma`. Discharge once Idris2 reduces
76+
||| top-level constant projections, or `validResult` is inlined at the use
77+
||| site so the constructor is exposed. (The prior "DISCHARGED … by direct
78+
||| record-projection reduction" comment was incorrect — it did not
79+
||| type-check under Idris2 0.8.0.)
7280
public export
73-
validResultIsValid : validResult.isValid = True
74-
validResultIsValid = Refl
81+
0 validResultIsValid : validResult.isValid = True
7582

7683
||| OWED: adding an Error-severity issue makes the result invalid.
7784
||| `addIssue` (Validation.idr L71-74) computes the new validity as

‎src/Proven/SafeSQL/Proofs.idr‎

Lines changed: 39 additions & 43 deletions
Original file line numberDiff line numberDiff line change
@@ -200,27 +200,30 @@ data InjectionSafe : ParameterizedQuery -> Type where
200200
||| 1. Validated identifiers (table/column names)
201201
||| 2. Parameterized values (never interpolated)
202202
||| 3. Literal SQL fragments (from trusted code, not user input)
203+
||| OWED: queries built with the builder are injection-safe.
204+
||| The witness would be `SafeByParameterization q (parameterizedQueriesSafe q)
205+
||| (\v, _ => allValuesSafe q.dialect v)`, but `parameterizedQueriesSafe` is
206+
||| itself OWED (erased, `0`-multiplicity) — an erased proof cannot be supplied
207+
||| as the relevant `IsParameterized` field of `SafeByParameterization`, so this
208+
||| theorem cannot be discharged until `parameterizedQueriesSafe` is (i.e. once
209+
||| `Data.List.all` reflection lands, or `ParameterizedQuery` carries the
210+
||| invariant intrinsically). Held back by the same blocker as its premise.
203211
export
204-
builderQueriesSafe : (q : ParameterizedQuery) ->
205-
(builtWithBuilder : ()) ->
206-
InjectionSafe q
207-
builderQueriesSafe q _ =
208-
SafeByParameterization q
209-
(parameterizedQueriesSafe q)
210-
(\v, _ => allValuesSafe q.dialect v)
211-
212-
||| Theorem: User input cannot escape string literals after escaping
213-
|||
214-
||| Proof sketch:
215-
||| 1. escapeString doubles all single quotes in the input
216-
||| 2. The result is wrapped in single quotes: 'escaped_input'
217-
||| 3. Any quote in the original input becomes '' which is an escaped quote in SQL
218-
||| 4. Therefore the string literal cannot be terminated early
212+
0 builderQueriesSafe : (q : ParameterizedQuery) ->
213+
(builtWithBuilder : ()) ->
214+
InjectionSafe q
215+
216+
||| OWED: user input cannot escape string literals after escaping.
217+
||| Proof sketch: escapeString doubles all single quotes and wraps the result
218+
||| in single quotes, so any quote in the input becomes the escaped `''` and the
219+
||| literal cannot be terminated early. The witness is exactly
220+
||| `escapeStringQuotesSafe d userInput`, but that is OWED (erased,
221+
||| `0`-multiplicity, opaque-String-FFI blocker), so this theorem inherits the
222+
||| same debt and cannot be relevantly discharged until it is.
219223
export
220-
cannotEscapeStringLiteral : (d : SQLDialect) -> (userInput : String) ->
221-
let escaped = escapeString d userInput
222-
in NoUnescapedQuotes escaped
223-
cannotEscapeStringLiteral d userInput = escapeStringQuotesSafe d userInput
224+
0 cannotEscapeStringLiteral : (d : SQLDialect) -> (userInput : String) ->
225+
let escaped = escapeString d userInput
226+
in NoUnescapedQuotes escaped
224227

225228
||| Theorem: Numeric values cannot contain SQL injection
226229
|||
@@ -237,32 +240,25 @@ numericValuesCannotInject d i = IntSafe
237240
-- Composition Safety
238241
--------------------------------------------------------------------------------
239242

240-
||| Theorem: Combining safe queries produces a safe query
243+
||| OWED: combining safe queries produces a safe query.
244+
||| The witness would reuse `parameterizedQueriesSafe (combineQueries q1 q2)`,
245+
||| which is OWED (erased) — so, like `builderQueriesSafe`, this cannot be
246+
||| relevantly discharged until `parameterizedQueriesSafe` is.
241247
export
242-
combinePreservesSafety : (q1 : ParameterizedQuery) -> (q2 : ParameterizedQuery) ->
243-
InjectionSafe q1 -> InjectionSafe q2 ->
244-
InjectionSafe (combineQueries q1 q2)
245-
combinePreservesSafety q1 q2 safe1 safe2 =
246-
SafeByParameterization (combineQueries q1 q2)
247-
(parameterizedQueriesSafe (combineQueries q1 q2))
248-
(\v, _ => allValuesSafe q1.dialect v)
249-
250-
||| Theorem: Adding parameters preserves safety
251-
|||
252-
||| addParam only appends to q.params and preserves fragments/dialect.
253-
||| Since allValuesSafe covers all constructors and fragments are unchanged,
254-
||| the parameterized query remains injection-safe.
255-
||| addParam uses record update `{ params := q.params ++ [val] } q`, which
256-
||| preserves fragments and dialect. The proof follows the same pattern as
257-
||| combinePreservesSafety.
248+
0 combinePreservesSafety : (q1 : ParameterizedQuery) -> (q2 : ParameterizedQuery) ->
249+
InjectionSafe q1 -> InjectionSafe q2 ->
250+
InjectionSafe (combineQueries q1 q2)
251+
252+
||| OWED: adding parameters preserves safety.
253+
||| addParam only appends to q.params and preserves fragments/dialect, so the
254+
||| query stays injection-safe — but the witness reuses
255+
||| `parameterizedQueriesSafe (addParam v q)`, which is OWED (erased). Same debt
256+
||| as `combinePreservesSafety`; discharge together once
257+
||| `parameterizedQueriesSafe` is.
258258
export
259-
addParamPreservesSafety : (q : ParameterizedQuery) -> (v : SQLValue) ->
260-
InjectionSafe q ->
261-
InjectionSafe (addParam v q)
262-
addParamPreservesSafety q v safe =
263-
SafeByParameterization (addParam v q)
264-
(parameterizedQueriesSafe (addParam v q))
265-
(\v', _ => allValuesSafe (addParam v q).dialect v')
259+
0 addParamPreservesSafety : (q : ParameterizedQuery) -> (v : SQLValue) ->
260+
InjectionSafe q ->
261+
InjectionSafe (addParam v q)
266262

267263
--------------------------------------------------------------------------------
268264
-- Defensive Checks (Runtime Validation)

‎src/Proven/SafeUrl/Proofs.idr‎

Lines changed: 15 additions & 8 deletions
Original file line numberDiff line numberDiff line change
@@ -134,12 +134,15 @@ export
134134
||| [(key, val)])`, so `(addParam key val qb).params` reduces to
135135
||| `qb.params ++ [(key, val)]` and the claim becomes
136136
||| `length (qb.params ++ [(key, val)]) = S (length qb.params)`.
137-
||| Discharged via `Data.List.Equalities.lengthSnoc` from `contrib`.
137+
||| Discharged via `Data.List.Equalities.lengthSnoc` from `contrib`,
138+
||| which is element-first (`lengthSnoc x xs : length (xs ++ [x]) =
139+
||| S (length xs)`), so the element `(key, val)` precedes the list
140+
||| `qb.params`.
138141
public export
139142
addParamIncreasesCount : (key, val : String) -> (qb : QueryBuilder) ->
140143
paramCount (addParam key val qb).params =
141144
S (paramCount qb.params)
142-
addParamIncreasesCount key val qb = lengthSnoc qb.params (key, val)
145+
addParamIncreasesCount key val qb = lengthSnoc (key, val) qb.params
143146

144147
||| OWED: Getting a parameter just set by key returns that value.
145148
||| Operationally true by case analysis on `hasParam key qs`: in the
@@ -257,16 +260,20 @@ export
257260
||| `Data.List` not exposing `appendAssociative` as a `%reducible`
258261
||| rewrite (the proof exists in Prelude but requires induction on
259262
||| `qs1`, and `Refl` cannot close it for abstract `qs1`). Discharge
260-
||| DISCHARGED via `Data.List.Equalities.appendAssociative` from
261-
||| contrib. `appendQueryStrings = (++)` (Query.idr L205-206), so the
262-
||| goal reduces to `(qs1 ++ qs2) ++ qs3 = qs1 ++ (qs2 ++ qs3)` —
263-
||| exactly the stdlib lemma. The OWED was a stdlib-plumbing residual,
264-
||| not a fundamental gap, as the comment noted.
263+
||| DISCHARGED via the Prelude/`Data.List` lemma `appendAssociative`.
264+
||| `appendQueryStrings = (++)` (Query.idr L205-206), so the goal reduces
265+
||| to `(qs1 ++ qs2) ++ qs3 = qs1 ++ (qs2 ++ qs3)`. `Data.List`'s lemma is
266+
||| stated in the opposite direction (`xs ++ (ys ++ zs) = (xs ++ ys) ++
267+
||| zs`), so we flip it with `sym`, and qualify it as
268+
||| `Data.List.appendAssociative` to disambiguate from this same-named
269+
||| local function. (The earlier `Data.List.Equalities.appendAssociative`
270+
||| reference did not resolve under Idris2 0.8.0 — the lemma lives in
271+
||| `Data.List`, not `Data.List.Equalities`.)
265272
public export
266273
appendAssociative : (qs1, qs2, qs3 : QueryString) ->
267274
appendQueryStrings (appendQueryStrings qs1 qs2) qs3 =
268275
appendQueryStrings qs1 (appendQueryStrings qs2 qs3)
269-
appendAssociative qs1 qs2 qs3 = Data.List.Equalities.appendAssociative qs1 qs2 qs3
276+
appendAssociative qs1 qs2 qs3 = sym (Data.List.appendAssociative qs1 qs2 qs3)
270277

271278
--------------------------------------------------------------------------------
272279
-- URL Security Properties

0 commit comments

Comments
 (0)