Soundness violation: query-mode snapshots emit phantom tuples after retraction and duplicate tuples after input changes (IDB-clear gate keyed on total_iterations)

[SeoyunL]

Affects: 0.52.99 (upstream main @ ae5c307), columnar backend, wirelog_easy_* query mode (snapshot without step()). Reproduction tests are provided as a companion PR (linked below).

Summary

In query mode (host drives the session with insert/remove + wirelog_easy_snapshot() only, no delta callback, no step()), the columnar backend violates perfect-model semantics:

• B-1 (phantom, unsound): after retracting all support for a derived tuple, the tuple is still emitted by subsequent snapshots (stale IDB row survives).
• B-2 (duplicate emission): re-evaluation appends re-derived rows onto uncleared IDB storage, so a tuple is emitted twice after an input change on either side — a retraction of redundant support (S2) or an incremental insert (S4).

Both defects share one root cause: the snapshot path gates IDB clearing and delta seeding on total_iterations > 0, but total_iterations counts effective fixpoint iterations of the last evaluation, which is 0 whenever evaluation converges without iterating. Exposure is therefore:

• Non-recursive programs: always exposed. Every evaluation converges with 0 effective iterations, the counter never leaves 0, and the gate never opens. Adding an unrelated recursive stratum makes the defects disappear (control S5R).
• Recursive programs: exposed after any re-evaluation that converges with 0 effective iterations. The evaluator assigns the counter (eval.c:1099), so a no-op re-evaluation — e.g. a duplicate EDB insert followed by a snapshot — resets a previously-positive counter back to 0 and reopens the phantom (experiment S6, confirmed on both a cycle-entry and a cycle-tail duplicate edge). The recursion-based protection observed in S5R is an artifact of counter state, not a semantic boundary.

The phantom is not cosmetic: it leaks into stratified negation and suppresses correct positive conclusions (see "Corruption propagation" below). Step-mode (delta-callback) evaluation is unaffected.

EDB ledger integrity was explicitly checked and is not compromised; no separate EDB-corruption issue is warranted (see "EDB integrity verdict").

Minimal reproduction (= test_snapshot_phantom.c in the companion PR)

Program:

.decl A(x: int32)
.decl B(x: int32)
.decl Q(x: int32)
Q(x) :- A(x).
Q(x) :- B(x).

Driver (easy API, query mode):

wirelog_easy_open(SRC, &s);
wirelog_easy_insert(s, "A", r7, 1);      /* A(7) */
wirelog_easy_insert(s, "B", r7, 1);      /* B(7) */
wirelog_easy_snapshot(s, "Q", count_cb, &n1);   /* n1 == 1, correct */
wirelog_easy_remove(s, "A", r7, 1);
wirelog_easy_remove(s, "B", r7, 1);      /* Q(7) now has ZERO support */
wirelog_easy_snapshot(s, "Q", count_cb, &n2);   /* expected 0, observed 1 */

Observed:

S5: snap1 Q=1 (want 1); after removing ALL support, snap2 Q=1 -> PHANTOM TUPLES (stale IDB)

Scenario matrix

All scenarios: fresh session, query mode, program above (plus noted variants). Each row is pinned by a driver in the companion PR (test_snapshot_matrix.c, test_snapshot_phantom.c, test_snapshot_retract.c, test_snapshot_recursive_ctl.c, test_phantom_negation.c).

#	Sequence	Expected Q	Observed Q	Verdict
S1	insert A,B → snap ×3	1, 1, 1	1, 1, 1	OK (idempotent re-snapshot)
S2	insert A,B → snap → rm A → snap ×3	1; 1, 1, 1	1; 2, 2, 2	B-2 dup after retract
S3	insert A,B → rm A → snap	1	1	OK (first snapshot evaluates from scratch)
S4	insert B → snap → insert A → snap	1; 1	1; 2	B-2 dup after incremental insert
S5	insert A,B → snap → rm A → rm B → snap	1; 0	1; 1	B-1 phantom (zero support)
S5R	S5 + unrelated recursive stratum T(x,y) :- E(x,y). T(x,y) :- T(x,z), E(z,y). seeded with 3 E rows	1; 0	1; 0	OK — control confirming root cause
S6	S5R program; insert A,B,3×E → snap → insert duplicate E(1,2) → snap → rm A, rm B → snap	…; 0	…; 1	B-1 in a recursive program — no-op re-eval resets the counter
S6b	S6 without the duplicate insert	…; 0	…; 0	OK (control; same binary as S6)
N1	Alarm(x) :- P(x), !Q(x).; insert A,B,P → snap → rm A, rm B → snap Alarm	Alarm=1	Alarm=0	B-1 leaks through negation
N1R	N1 + recursive stratum	Alarm=1	Alarm=1	OK (control)

S6 detail (drives the scope statement in the Summary; also reproduced with duplicate E(3,4)):

1. insert A(7),B(7), E(1,2),E(2,3),E(3,4); snap Q=1 T=6   [recursive stratum iterated: counter > 0]
2. insert E(1,2) again (multiplicity +2, no new T tuple); snap T=6
   -> re-evaluation converges with 0 effective iterations; eval.c:1099 assigns counter = 0
3. rm A(7); rm B(7); snap Q -> observed 1 (want 0): phantom is back despite recursion

Notes:

• S3 shows the defect requires a prior snapshot: the stale state is the previous snapshot's materialized IDB.
• S1 shows repeated snapshots without input changes are clean (the snapshot_stable_valid fast path at columnar/session.c:2286 is not the problem).
• Step-mode control: tests/test_hypo_driver.c runs insert/retract round trips through wirelog_easy_step() with delta callbacks — retract streams mirror insert streams and post-retraction snapshots are empty. Query mode only is affected.

Root cause

col_session_snapshot (wirelog/columnar/session.c:2274) must discard stale IDB rows before re-evaluating when inputs changed. The clear is gated:

/* columnar/session.c:2296 */
if (sess->total_iterations > 0
    && (sess->pending_full_input_eval
    || (sess->pending_input_change
    && sess->last_inserted_relation == NULL))) {
    col_session_clear_idb_rows(plan, sess);
}

total_iterations is written by the evaluator as the number of effective fixpoint iterations of recursive strata (eval.c:1099: sess->total_iterations = final_eff_iter;). A non-recursive program converges with final_eff_iter == 0, so after every evaluation the counter is still 0 and the gate never opens. The retraction path then re-evaluates all strata and appends re-derived rows onto the uncleared IDB relations:

• S2/S5: the stale Q(7) row from the previous snapshot survives (phantom), and re-derivation appends a second copy while support remains (dup).
• S4: the incremental-insert delta path (columnar/session.c:2308) also requires total_iterations > 0; at 0 it falls back to full re-evaluation of all strata — again without clearing — so the re-derived Q(7) is appended next to the old row.

The counter is being used as a proxy for "has this session completed at least one evaluation pass?", which it does not measure. Two experiments pin this down from both sides:

• S5R: adding any stratum that needs ≥1 fixpoint iteration flips the counter to nonzero and both defects vanish.
• S6: in that same recursive program, one no-op re-evaluation (duplicate EDB insert → snapshot) converges with 0 effective iterations, the assignment at eval.c:1099 resets the counter, and the very next retraction snapshot emits the phantom again.

The codebase already contains evidence that this proxy is fragile — S6 is the demonstration of exactly the hazard Issue #416 described:

• Issue Validate DOOP W=4/W=8 stability (prerequisite for Phase 1) #416 changed the TDD-recursive path to accumulate (eval.c:7333: coord->total_iterations += final_eff_iter;) specifically because assigning 0 "would incorrectly reset the first-snapshot guard".
• The non-TDD path still assigns (eval.c:1099); S6 shows that reset happening in practice and reopening B-1.
• The TDD adaptive-workers fallback works around the assign/accumulate mismatch by saving the counter and re-adding it after the sequential re-run (eval.c:6735-6738) — doubling the value, which is harmless only because every consumer treats it as a boolean.

Note that switching eval.c:1099 to accumulate would close S6 but not the non-recursive exposure (the counter would still never leave 0 there); only an explicit "has evaluated" signal fixes both.

Fix directions

1. Audit every use of total_iterations as an "evaluation happened" proxy (do this first). Complete inventory as of ae5c307:

   Site	Role	Risk at total_iterations == 0 after a real evaluation
   columnar/session.c:2296	IDB-clear gate on retraction / full-input change	B-1/B-2: clear skipped, stale rows survive
   columnar/session.c:2308	enables incremental affected-strata + delta pre-seed on insert	falls back to full re-eval without clear → B-2 (S4)
   columnar/session.c:2430-2436	TDD enable for initial snapshot (Measure serial fraction as function of W (Amdahl's Law validation) #413)	treats every non-recursive snapshot as "initial"; audit for redundant TDD setup
   eval.c:6640-6644	per-stratum IDB clear before TDD when new EDB inserted (feat(#368): Asymmetric partition-replicate join for IDB-IDB self-joins #372)	clear skipped for non-recursive strata → same stale-row family inside TDD path
   eval.c:1099 (write, assign) vs eval.c:7328-7333 (write, accumulate, Validate DOOP W=4/W=8 stability (prerequisite for Phase 1) #416)	producer inconsistency	a later 0-iteration eval silently resets the guard on the non-TDD path
   eval.c:6735-6738 (write, save/re-add)	fallback workaround for the above	counter value becomes meaningless as a count; only >0 is safe
   columnar/session.c:414 (col_session_get_iteration_count)	observability API	none, but documents the intended meaning ("iterations in last eval"), which the guards contradict

2. Replace the proxy with an explicit flag. Add bool has_evaluated (or an evaluation epoch counter) to wl_col_session_t, set unconditionally at the end of every completed evaluation pass regardless of final_eff_iter, and use it in the four guard sites above. Keep total_iterations purely as the observability metric its doc comment describes.

3. Make the retraction path clear unconditionally. pending_input_change && last_inserted_relation == NULL (a retraction happened) can only be answered correctly by re-deriving from scratch or by differential retraction; either way the stale materialization must not survive. S3 (retract before first snapshot) already takes the correct full-eval-from-empty path.

4. Defense in depth (optional): consolidate on emit. col_session_emit_snapshot (columnar/session.c:2216) emits raw row storage. Deduplicating by z-set weight at emission would mask append bugs like S4 at the reporting boundary — worth considering, but it must not substitute for fixing the gate (the phantom's weight would still be wrong).

Direction 2 + 3 together are the minimal semantic fix; 1 is the safety net that catches sites this issue has not exercised (e.g. the TDD-internal clear at eval.c:6640).

Corruption propagation: phantoms suppress negation-derived facts

tests/test_phantom_negation.c, program:

Q(x) :- A(x).   Q(x) :- B(x).
Alarm(x) :- P(x), !Q(x).

Sequence: insert A(7), B(7), P(7) → snapshot → remove A(7), remove B(7) → snapshot.

The perfect model after the retracts contains Alarm(7) (P(7) holds, Q(7) does not). Observed:

plain    : before rm: Q=1 Alarm=0 | after rm all support: Q=1 Alarm=0 -> WRONG
recursive: before rm: Q=1 Alarm=0 | after rm all support: Q=0 Alarm=1 -> CORRECT

The phantom Q(7) feeds the negation stratum, so the engine is not merely emitting an extra tuple — it omits a true positive conclusion. Any downstream consumer using negation for absence detection (alarms, integrity checks) silently loses alerts. This upgrades the defect from "stale cache artifact" to a soundness and completeness violation of stratified-negation semantics.

EDB integrity verdict (no separate issue)

The fix-direction-1 audit and targeted probes checked whether the EDB ledger itself is corrupted. It is not:

• Snapshot emission contract (by design): col_session_emit_snapshot iterates only relations listed in plan strata, and stratum relation lists are built exclusively from rule-head names (exec_plan_gen.c:2672-2684). Pure host-fed EDB relations (never a rule head) are therefore never emitted by snapshots — before or after any retract. An earlier read of A=0, B=0 in the retract repro as "EDB rows lost" was a misdiagnosis; B reads 0 at every point in the sequence, including before the retract. Inline facts do not change this: with B(9). in the program, snap B = 0 while snap Q = 1 proves the fact was seeded but the relation is still not emitted.
• Ledger survives retraction of a sibling: in S3, rm A followed by a first snapshot yields Q=1 derived from B's ledger row, with no prior snapshot state involved. The EDB store is intact; only materialized IDB state goes stale.

Consequently no separate EDB-corruption issue is filed. One documentation follow-up belongs in the fix PR: docs/SEMANTICS.md's "+2 multiplicity … the row remains observable in snapshots" wording is only true through derived IDB rows; pure-EDB relations are never directly emitted, and the sentence should say so.

Regression test status

The six reproductions are provided as a companion PR (link: to be added once opened) rather than in-tree references — this issue comes from an external-contributor workflow. The PR registers them in the semantics suite (tests/meson.build), all easy-API drivers asserting the verdict via exit code:

Test	Asserts	Current	Registration
snapshot_phantom	S5: zero-support tuple not emitted	fails (B-1)	should_fail: true
snapshot_retract	S2 core: Q survives exactly once after rm A; A/B emit 0 per EDB contract	fails (B-2 dup)	should_fail: true
snapshot_matrix	S1–S4 all report Q=1	fails (S2, S4)	should_fail: true
phantom_negation	plain + recursive both yield Alarm(7) after full retract	fails (plain leg)	should_fail: true
snapshot_recursive_ctl	S5R control: recursive stratum → no phantom (q1=1, T=6, q2=0)	passes	normal
hypo_driver	step-mode control: retract mirrors insert, no residue	passes	normal

S6 (counter reset in a recursive program) is currently covered only by a standalone probe; the fix PR should promote the 3-step sequence above into a seventh regression test (should_fail while red, flag dropped with the fix, same contract as the other four).

should_fail contract: the four red tests keep the default suite green while enforcing the reproduction. The moment the engine is fixed they exit 0, meson reports them as unexpected pass, and the suite fails — so the fix PR must remove the should_fail: true marks in the same commit (the contract is documented in the meson block comment in the companion PR). One caveat for the fix PR: snapshot_matrix S4 asserts set-observation (Q=1) for a doubly-supported tuple; docs/SEMANTICS.md explicitly leaves IDB multiplicity exposure unpromised, so if the intended post-fix semantics is multiplicity exposure (Q=2 by design), adjust that single assertion and document the decision.

[justinjoy]

Closed after merging PR #930 (fixes query snapshot frontier reset regression).