Conversation
buger
added a commit
to buger/graphql-go-tools
that referenced
this pull request
May 1, 2026
Uses reqproof's proof verify-lemma command (Z3 deeper roadmap, Phase E) to prove invariants of the resolve package's algorithms. Lemma 1 (slice_append_length_invariant) PROVES cleanly via Z3's seq theory — sanity check that the verifier works. Lemmas 2-4 produce COUNTEREXAMPLES that map to the existing known bugs (wundergraph#6 FieldInfo.Merge slice parity, wundergraph#7 Field.Copy ParentOnTypeNames, wundergraph#9 Resolvable.Reset state clearing). These are spec-level evidence complementing the failing-test reproducers in cve_reproducers_test.go. Lemma 5 (type_names_pop_safety) PROVES with explicit precondition, demonstrating the value of // reqproof:requires for documenting safety invariants the production skipFieldOnTypeNames currently lacks. The _proof.go file is build-tag-gated (//go:build reqproof_proof) so production builds exclude the proof code. Lemmas 2-4 use simplified models because the gosmt translator (Phase B/C of the SMT roadmap) accepts only a restricted Go subset: pure free functions, no methods, no for/range loops, no inter-function calls. The production Field.Copy / FieldInfo.Merge / Resolvable.Reset all use unsupported constructs, so each lemma inlines a faithful model of the relevant fragment in its body. The mapping is documented at the top of resolve_proof.go and per-lemma in docs/cve-candidates.md. See docs/cve-candidates.md 'Z3-verified lemma evidence (Phase F)' for per-lemma counterexamples, source-line mapping, and an honest assessment of what works end-to-end vs. what needed simplification.
buger
added a commit
to buger/graphql-go-tools
that referenced
this pull request
May 1, 2026
Expands the Z3-verified lemma corpus from 5 (Phase F) to 25 covering
every major obligation class in v2/pkg/engine/resolve — resolvable.go,
node_object.go, loader.go, subscription_filter.go, tainted_objects.go.
Verdict summary:
- PROVED: 20 (9 via library citations from Phases J/L)
- COUNTEREXAMPLE: 3 (each reconfirms a known bug at spec level:
Bug wundergraph#6 FieldInfo.Merge slice-parity desync,
Bug wundergraph#7 Field.Copy omits ParentOnTypeNames,
Bug wundergraph#9 Resolvable.Reset stale currentFieldInfo / marshalBuf)
- UNKNOWN: 2 (recursive-datatype goals; Z3 reports
"datatype is not well-founded" — cvc5 with --quant-ind is the
upstream resolution; dispatcher has cvc5 wired in but the
auto-route heuristic missed both queries)
- TRANSLATION_ERROR: 0 (after two iterations to fit gosmt subset)
Total wall time: ~114 ms across 25 lemmas (~4.6 ms mean per lemma).
Library citations don't materially shorten Z3 wall time at this scale;
their value is proof auditability — `by(SliceAppendLength)` makes the
load-bearing axiom explicit.
Phase K demonstrates the full Z3 deeper roadmap (reqproof Phases A
through L plus H) cooperating end-to-end on a real commercial Go
codebase. Every Phase contributed: A/B/C (gosmt translator) emit the
SMT, D/E (annotation scanner + orchestrator) dispatch each lemma,
F seed corpus expanded, G cvc5 wired (cited as resolution for
UNKNOWNs), H `by induction(t)` expands the recursive walker lemma,
I auto-synthesises 2 obligations from declarative `// reqproof:invariant`
annotations, J library lemmas cited 9 times via `by(...)`, L
composes the by/induction syntax through the parser.
The remaining gap surfaced by Phase K — and the load-bearing item for
the next round of investment — is recursive-ADT routing: any query
containing `(declare-datatypes ((T 0)) ...)` with a self-referential
field should auto-route to cvc5 by default.
No new bugs surfaced; the corpus reconfirms known structural bugs at
the specification level (rather than in observed runtime test runs)
which is the honest outcome of an incremental verification round.
Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
1 participant
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
This PR will just remove some obsolete code/comments.