Verified Completions Phase 1: run the consistency rule pack on the real engine

Why

The Verified Completions rule pack (docs/internals/verified-completions/rules/consistency-core.iql) and its test fixture were written in a design session that had no Rust toolchain. They are syntax-checked and linted, but have never run on the real engine. The expected query results in the fixture were derived by hand. Before we build any gateway code on top of this, we need to prove the rules actually work.

What to do

Build the engine (cargo build --release), start the server, open the CLI
Run docs/internals/verified-completions/quickstart/hello-consistency.iql. Expected: one conflict reported in both orders (a,b) and (b,a), plus a .why proof tree
.load docs/internals/verified-completions/rules/consistency-core.iql, then run docs/internals/verified-completions/tests/consistency-core-fixture.iql
Compare actual query results against the expected rows written in the fixture comments. Fix the pack or fix the expectations, whichever is wrong
Check the two rules most likely to fail at load time:
- areach (recursion where the attribute is a variable). If the engine rejects it, generate one specialized rule per attribute at load time instead
- member_tally (an aggregation result used by another rule). Same fallback: restructure if the engine objects
Generate a real .iql.out snapshot using the existing harness (tests/example_verification.rs conventions)
Re-run docs/internals/verified-completions/tools/lint_iql.py after every edit to the pack

Done when

The fixture runs green against the real engine and a .iql.out snapshot is checked in. The retraction check at the end of the fixture must also pass: after deleting the m4 fact, the three "cycle" findings disappear and every other finding survives.

Notes for whoever picks this up

Two engine facts were already verified by reading the source, do not rediscover them the hard way:

Var != Var works on any type, including strings
Var < Var only works on ints and floats. On strings it silently evaluates to false, no error. That is why every ordered comparison in the pack runs on integer mirror columns (claim_num, constraint_num), with dates encoded as YYYYMMDD integers

Full context: docs/internals/verified-completions/HANDOFF.md and docs/internals/verified-completions/docs/REVIEW-GUIDE.md.

Validation complete. The fixture runs green on the real engine (built at d955fc0, Rust 1.96). Summary of what happened:

The original pack silently returned zero conflicts. The 15-clause conflict rule triggered an engine bug where multi-clause rules can evaluate empty with no error (filed as #91 with minimal repros). violation and tension worked from the start.

Fix: restructured the pack. Every detection rule now has its own single-clause relation (conflict_functional, conflict_cycle_before, ...); the reporting views (conflict, violation, tension, finding) union them with one clause per kind, each reading a distinct relation - a pattern verified safe against #91. The external query interface is unchanged, so nothing downstream (gateway design, RFC response assembly) moves.

Second fix: .why timed out on the functional conflict. The eq helper's recursive symmetric rule (eq(X,Y) <- eq(Y,X)) sent the backward-chaining prover in circles. Rewrote it to symmetrize at the base (eq0) and keep the recursion directed - same derived relation, and all three .why queries in the fixture now return.

Results vs the hand-derived expectations:

All 14 expected conflict rows present, all 4 violations, the soft tension, and the provenance view with both quoted spans
The two load-time worries from the handoff were unfounded: areach (recursion parameterized by attribute) and member_tally (aggregation feeding another rule) both work as written
Two correct rows the hand derivation missed: mutual parent_of (m9) fires both asymmetry AND the hierarchy cycle rule, since a 2-cycle violates acyclicity. Fixture expectations updated
Retraction check passes: deleting m4 removes exactly the three before-claim cycle findings; the two parent_of cycle findings and everything else survive

Also confirmed: .why proof trees already come over the WS API as structured JSON (proof_trees field, src/protocol/handler.rs) - the CLI just does not render them. The RFC open question about needing an engine PR for that is resolved: none needed.

Snapshot saved at docs/internals/verified-completions/tests/consistency-core-fixture.iql.out. Updated pack, fixture, and PLAN.md are on the verified-completions-plan branch (PR #90).

Two operational notes for the gateway milestones: the default WS rate limit (100 msgs/sec) is too low for loading the pack over one connection, so the gateway should either batch statements or the deploy config needs a higher limit; and the repo's config.toml template is stale (http.auth.enabled is no longer a valid field, and the server only reads config via --config, not env vars).

feat: Verified Completions design package, engine-validated rule pack…

feat: Verified Completions - proven core loop, executable benchmark, …

feat: Verified Completions - proven core loop, verified benchmark cor…

Navigation Menu

Repository navigation

Verified Completions Phase 1: run the consistency rule pack on the real engine #81

Why

What to do

Done when

Notes for whoever picks this up

Metadata

Assignees

Labels

Type

Projects

Milestone

Relationships

Development

Verified Completions Phase 1: run the consistency rule pack on the real engine #81

Description

Why

What to do

Done when

Notes for whoever picks this up

Activity

jsam commented on Jul 26, 2026

Metadata

Metadata

Assignees

Labels

Type

Projects

Milestone

Relationships

Development

Issue actions