Enumerated 2026-07-21 by running the estate checker (standards/scripts/check-trusted-base.sh)
against this repository: 19 soundness-relevant escape hatches detected, of which
16 are real Lean axiom declarations and 3 are detector false positives (§(e)).
lake build is green and Lean reports no incomplete proofs — no sorry is reached in
any proof position. That is true, and it is not the same as "the proofs are done".
Lean’s sorry warning does not fire on axiom. This repository declares 16 axioms, and
none of them is a necessary axiom in the policy’s §(c) sense (function extensionality,
classical choice, an extraction boundary). Every one is a stub — a declaration written
to make the file compile while the implementation or proof was deferred. Two consequences
that must not be understated:
-
Five axioms occupy executable positions.
parseToIR,deserializeIR,many,many1andsepByare declared asaxiom, so they have no implementation at all. Code that calls them typechecks and cannot run. "34/35 targets build" is therefore a statement about typechecking, not about a working parser. -
executePreservesTypesproves nothing. Its statement reduces to… → True, with the body commented-- Placeholder. It reads like a type-safety soundness theorem and discharges no obligation whatsoever. It is the most misleading item in this list.
Similarly, the worked examples in TypeSafeQueries.lean — the ones whose comments claim
✓ Type-safe INSERT with valid score and demonstrate that an out-of-range score
-- Type error: failed to prove 150 ≤ 100 — are themselves axioms. They assert the
existence of the well-typed value rather than constructing it, so they demonstrate the
opposite of what the surrounding comments claim.
None of this is a regression introduced here; it is the inherited state of the imported GQLdt sources, recorded honestly for the first time.
-
(none yet — entries are removed from §(d) and not listed here once a proof lands)
-
(none yet — but the prerequisite is now met.)
Updated 2026-07-28. This section previously read "this repo has no executable test
coverage: lake test reports no test driver configured … adding a @[test_driver] is a
prerequisite for moving any item into this section." That prerequisite has been satisfied:
lake test now runs three suites and 163 checks, and the gate is canary-tested in both
directions (a seeded false check turns it red; removing it returns green).
So items can now be moved here — but none has been yet, and none should be moved without
a stated refutation budget. Coverage existing is not the same as a given axiom being
covered. The policy’s requirement is a citable budget ("property-tested at N inputs by
<command>, last green on `<date>`"), because without one "covered by tests" is
unfalsifiable — which is the whole reason this section exists.
The nearest candidate is D4 (inferredInsertTypesMatch); see its entry.
Owner: @hyperpolymath · Deadline: INDEFINITE — sequenced behind the GNPL narration
layer (see docs/THEORY.adoc), except D1 which is called out as urgent below.
-
src/GqlDt/TypeSafe.lean:194—axiom executePreservesTypes-
Kind: asserted soundness theorem whose statement is vacuous (
… → True). -
Why urgent: it is the only item here that actively misinforms. A reader encountering
executePreservesTypesreasonably concludes execution is proved type-preserving. Nothing of the sort has been established. -
Plan: either state and prove the real property (execution preserves the schema typing of
stmt.values), or delete the axiom and record the obligation as an open goal. Deleting is strictly better than keeping a vacuous placeholder. -
Blocked on: the
satisfiesConstraintssignature issue noted in the source comment.
-
Declared axiom, therefore unimplemented, not merely unproven:
| Location | Axiom | Note |
|---|---|---|
|
|
commented-out |
|
|
as above |
|
|
as above |
|
|
|
|
|
|
|
|
|
|
|
pipeline entry point; DELETE→IR conversion commented out as not implemented |
|
|
|
-
Plan: implement as
partial def(or with an explicit termination measure / fuel parameter, which is the standard Lean 4 remedy for the combinator non-termination the source comment describes).many/many1/sepByare the root — the fourparse*axioms above them exist because these three do. -
Consequence while open: the M6 "parser substantially complete" status in
README.adocoverstates what is executable. Corrected inREADME.adoc.
| Location | Axiom |
|---|---|
|
|
|
|
|
|
|
|
|
|
|
|
-
Plan: construct each concretely, discharging the
BoundedNat 0 100/NonEmptyString/Confidenceobligations withby decideorby norm_num. These are the demonstrations of the repo’s central claim ("invalid insert won’t compile"), so leaving them asserted defeats their purpose. Lowest difficulty, highest credibility-per-unit-effort of the three groups — do these first after D1.
-
src/GqlDt/Pipeline.lean:147—axiom inferredInsertTypesMatch-
Kind: the one item with a reasoned justification in-source — the dynamic schema lookup in
inferInsertalready performs the check, and reconstructing that proof structurally would require reflecting the schema into the type system. -
Assessment: plausible, and closest of the 16 to a genuine §(b)/§(c) entry. Not §(c), because it is derivable in principle. Not yet §(b) either — but the reason has changed as of 2026-07-28: a test suite now exists (163 checks), so the blocker is no longer "no coverage at all", it is that this specific path is not property-tested and has no citable refutation budget.
-
Plan: property-test
inferInsertover generated schema/value pairs, then promote to §(b) quoting the command and the input count; or discharge via schema reflection (the source’s own "future work"). The first is now genuinely reachable.
-
The estate checker matches \bsorry\b textually in .lean files. Three hits are not
escape hatches, and are listed here so the count reconciles (19 = 16 + 3):
| Location | What it actually is |
|---|---|
|
|
|
|
|
|
A fourth textual hit, src/GqlDt/TypeSafeQueries.lean:90
(-- overall_correct := by sorry }), is inside a comment and is already excluded by
the checker’s own comment filter.
scripts/check-lean-proofs.sh in this repo excludes all four by design. See its header.
The two checks answer different questions and both are needed:
| Check | Question | Current answer |
|---|---|---|
|
Does Lean report any incomplete proof ( |
No ✅ |
|
How large is the unproven trusted base ( |
16 axioms, all stubs ❌ |
A green proof gate here means "nothing is admitted mid-proof". It does not mean "nothing is assumed". This document is the record of what is assumed.