Merged
Conversation
…ByteSliceReferences
Byte slice references
jensneuse
pushed a commit
that referenced
this pull request
Apr 14, 2020
partly implementation of the contract
buger
added a commit
to buger/graphql-go-tools
that referenced
this pull request
Apr 30, 2026
Targeted the highest-leverage hotspots ranked by .proof/mcdc/go/latest.json
decision count × inverse coverage. Added 91 real exercising tests across
three rounds; 1 of them turned up a new defensive-coding bug (Resolvable.Reset
nil-xxh dereference) which is captured as a failing reproducer test.
MC/DC coverage delta:
statement: 73.32% -> 84.26% (+10.94pts)
decision: 36.31% -> 52.64% (+16.33pts)
condition: 38.68% -> 54.04% (+15.36pts)
fully-covered decisions: 289 -> 419 (+130)
New tests:
mcdc_aggressive_coverage_test.go (round 1, 43 tests — Equals/Copy/helpers)
mcdc_aggressive_round2_test.go (round 2, 17 tests — Resolver.New defaults,
trigger map !ok branches, FetchTreeNode helpers)
mcdc_aggressive_round3_test.go (round 3, 30 tests — errors.go, context.go,
variables_renderer.go, inputtemplate.go branches)
cve_reproducers_round2_test.go (1 failing reproducer — Bug wundergraph#9)
New bug (round 2):
Bug wundergraph#9 — Resolvable.Reset nil-xxh dereference at resolvable.go:109
Reproducer: TestCVE_BUG009_ResolvableResetNilXxhPanic (failing by design)
Severity: CVSS 5.3 Medium (limited reachability — internal pools only)
See: docs/cve-candidates.md
Stub witnesses remaining: ~155 (require federation simulator, subgraph HTTP
fixtures, or subscription event-loop wiring) — see mcdc_witnesses_pending_test.go.
Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
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>
buger
added a commit
to buger/graphql-go-tools
that referenced
this pull request
May 3, 2026
Replace v2/pkg/engine/resolve/resolve_proof.go (//go:build reqproof_proof shadow file) with resolve_lemmas.go, an ordinary production-code file hosting 25 // reqproof:lemma directives on lemma_* helper functions. The three former shadow types (ProofResolvable / ProofField / ProofTypeFieldSource) are gone. Their three lemmas now reference the production types (Resolvable / Field / TypeFieldSource) via // reqproof:model directives attached directly on those declarations in resolvable.go and node_object.go. The model projects the load-bearing fields: Resolvable: wroteData / wroteErrors / currentFieldInfo Field: OnTypeNames / ParentOnTypeNames as []int opaque tags TypeFieldSource: IDs / Names Verdicts preserved: 22 PROVED + 3 COUNTEREXAMPLE (Bugs wundergraph#6, wundergraph#7, wundergraph#9) + 0 UNKNOWN — same as the pre-migration baseline. Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
buger
added a commit
to buger/graphql-go-tools
that referenced
this pull request
May 3, 2026
…overage gaps - v2/pkg/engine/resolve/: was 22 PROVED + 3 CE, parent unchanged at 22 PROVED + 3 CE. - v2/pkg/engine/resolve/resolveloops/: new sub-package with 11 PROVED loop-invariant lemmas (8 Phase S.2c.1 range-over-slice + 3 Phase S.2c.4 break). Sub-package needed because the parent's recursive ADT (ProofWalkerNode) clashes with the loop-helper translator (snoc-ProofWalkerNode_Children_List undeclared). - Phase U adoption: 9 -> 15 by() references (+6) — SliceLengthNonNegative, MinLEMax, ClampWithinBounds, AddIdentityZero (x3) cited on existing proves- syntax lemmas. - Coverage: 89 branches recorded, 89 covered (100%). - Documented at docs/reqproof-coverage-gaps.md (G1-G6 phase blockers). - Pre-existing 3 CEs (BUG-wundergraph#6/wundergraph#7/wundergraph#9) preserved. Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
buger
added a commit
to buger/graphql-go-tools
that referenced
this pull request
May 3, 2026
Tautology pruning (operationreportprobes/, 4 deletions):
- RR-2 reset_clears_lengths: model returned 0 unconditionally; lemma
asserted post == 0. Z3 saw 0 == 0.
- RR-3 locations_from_position_length_match: model was identity
(return positionLen); lemma asserted out == positionLen. Tautology.
- RR-6 status_code_replacement_envelope: under preconditions the
model deterministically returned true. Tautology in disguise.
- RR-7 add_error_grows_length_by_one: model + lemma both
preLen + 1 == preLen + 1. Hard tautology.
None were traced to any SYS-REQ — pure speculative bug-hunt fixtures
with no real falsifiable property. Real Report.Reset / append /
envelope checking would need slice-mutation translation, a
translator-phase task.
resolveloops/ removal (Part B, 11 deletions):
All 11 lemmas asserted `count >= 0` over a counter initialized to 0
and only ever incremented or held — tautologies-in-disguise. The
package was carried as a translator-test workaround for a long-fixed
G1 collision. Nothing migrates inline because nothing earned its
place there.
Probe-package documentation (Part C):
README.md added to safetyprobes/, operationreportprobes/, and
astparserprobes/ explaining the synthetic-probe nature, the
method-receiver MCDC translator wall, and the Phase SS Path A
removal plan. File-level doc-comment headers strengthened to point
at the real production code being mirrored.
Audit at 0/0:
- documentation_coverage 100% (regenerated SRS picks up RR-block
requirements).
- suspect_clean 0 (proof trace review --all after annotation moves).
- authored_delta_expected 0 (proof review impact for traced files).
- lint_clean 0 (Implements: SYS-REQ-NNN annotations on all 25
inline lemma helpers in resolve.go; MarshalJSON tagged
SYS-REQ-015; lint excludes for autogenerated zz_reqproof_*.go and
probe packages).
Final corpus state under --no-cache: 75 lemmas total — 66 PROVED,
6 CE (expected), 2 TIMEOUT, 1 UNKNOWN. The 3 non-decisive verdicts
(resolvable_reset_clears_walker_state, fieldinfo_merge_preserves_slice_parity,
field_copy_preserves_parent_on_type_names) are pre-existing real
bug-shape probes (BUG wundergraph#6, wundergraph#7, wundergraph#9) blocked on translator-phase
struct-projection / len(append) / nil-pointer encoding gaps. They are
NOT tautologies — keeping them as honest TIMEOUT/UNKNOWN preserves
spec-level capture; cve_reproducers_test.go provides independent
runtime evidence.
Decision log: reqforge:docs/internal/phase-rr-honest-decision-log.md.
PR #1 reflects the cleanup. RBRACE bug (SYS-REQ-181) stays prominent
with formalization_status: violated and the live Z3 CE.
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 adds recent changes to the master. See the #8 for details.