The disposes half of the propose->verify loop. Catches the plausible lie a grammar check never sees: fluent, confident, wrong. GROUNDING (anti-hallucination): fit a claim point against every real evidence neighborhood via engram_reason_point_fit; grounded iff best fit clears an absolute threshold. Off-model orthogonal residual is the hallucination signal. Distinct from abduction: asks 'is there any real support at all' and may say no. CONSISTENCY (contradiction): (a) polarity/negation inversion -- claim lands on the opposite side of a real polarity axis from the grounded truth (the reassurance->accusation catch: 'never fought'->'argued'); (b) geometric -- claim inside a forbidden region or beyond a max-distance constraint. Pure C11, read-only, composes existing primitives only. 29 constructed-case checks, 0 failures across PERF and ASan/UBSan; macOS leaks 0. el-exposure deferred (point/variadic-set inputs -- matches reasoning-agent precedent). Reach checks (formal/causal/predictive) not started; documented.
7.1 KiB
Verifier Layer — Grounding + Consistency (decisions + reversal)
Date: 2026-08-13
Branch: engram-tiered-storage (worktree /tmp/engram-tiered-wt), atop a3358df
Scope: additive, read-only, staged. No push, no tag, no merge. Live :8742 untouched.
What this adds
The VERIFIER layer — the "disposes" half of the propose→verify loop. The geometry PROPOSES (cheap, creative, sometimes wrong); the verifier DISPOSES, catching the class of failure no grammar check sees: a fluent, confident, WRONG output — the plausible lie.
Motivating failure (tonight's PT translation): a deleted negation turned "you never fought" into "you argued" — reassurance inverted into accusation, grammatical and invisible, catchable only by the geometry.
Two checks, both pure C11 (stdlib + libm), read-only over their inputs, touching no store / index / activation. Every geometry op is delegated to the already-shipped reasoning + §5 operator primitives; this layer only composes and thresholds.
Files added
lang/runtime/engram_verify.h— API + design contract.lang/runtime/engram_verify.c— implementation.engram/test/test_verify.c— closed-form constructed cases (29 checks).engram/test/run_verify_tests.sh— two-pass runner (PERF, then ASan/UBSan).
No existing file was modified.
C signatures + how each composes the existing primitives
GROUNDING (anti-hallucination)
int engram_verify_grounding(const float* claim, int dim,
const GeoDescriptor* const* evidence, int n_evidence,
double ext_floor, double ground_threshold,
GeoGrounding* out);
Fits the claim POINT against every real evidence neighborhood via
engram_reason_point_fit (in-distribution Mahalanobis + off-model orthogonal
residual) and keeps the BEST supporter. Grounded iff best fit score ≥
ground_threshold. Deliberately an ABSOLUTE-THRESHOLD gate, distinct from ABDUCTION
(which always ranks and picks a winner): grounding asks the prior question — "is there
any real support at all?" — and may answer no. The off-model best_ortho residual is
the sharpest hallucination signal: energy in a direction the manifold does not span.
CONSISTENCY (contradiction detection)
int engram_verify_consistency(const float* claim, int dim,
const GeoDescriptor* context,
const GeoDescriptor* pole_pos, const GeoDescriptor* pole_neg,
const GeoDescriptor* forbidden,
double ext_floor, double deadzone_frac,
double forbidden_thresh, double max_distance,
GeoConsistency* out);
Two independent sub-checks (either can fire; both flags reported):
- (a) POLARITY / negation inversion — the reassurance→accusation catch.
A polarity axis
p = (c_pos − c_neg)/‖·‖is defined by two REAL poles (affirm vs negate), midpointo = ½(c_pos + c_neg). Signed sides:claim_side = p·(claim − o),ref_side = p·(c_context − o). If they have OPPOSITE sign and both clear the neutral deadzone (deadzone_frac·½‖c_pos−c_neg‖), the claim asserts the polarity opposite to the grounded truth → inversion flagged. Pure dot products / projections over the same centroids the geometry already computes. - (b) GEOMETRIC contradiction — claim sits INSIDE a
forbiddenregion it must be far from (engram_reason_point_fitscore ≥forbidden_thresh), OR violates a max-distance constraint tocontext(L2 > max_distance).
Proof (constructed cases — demonstrate, not declare)
./engram/test/run_verify_tests.sh → 29 checks, 0 failures in BOTH passes
(PERF -O2, and ASan+UBSan -O1). macOS leaks --atExit: 0 leaks for 0 total leaked
bytes.
Key demonstrated numbers:
- Grounding IN (claim inside E0): score 0.885, grounded=1, ortho≈0.
- Grounding OUT (claim floating along unmodeled e2): score 0.0004, grounded=0, ortho=50.0 (the hallucination signal), nearest centroid L2=50.
- Negation inversion (the catch): truth "never fought" ref_side=−5.0, lie
"you argued" claim_side=+4.0 → opposite poles →
inverted=1, verdict=POLARITY, consistency=0. Faithful claim (−4.0, same pole) → inverted=0, verdict=OK, consistency=1. Neutral claim inside deadzone → not triggered. - Geometric: claim inside forbidden region → geo_violation=1 (forb_fit 0.99); claim beyond max_distance → geo_violation=1 (ctx_dist 8.0 > 3.0).
- Combined (the whole point): a claim that is GROUNDED in real vocabulary (grounded=1, score 1.0) yet polarity-inverted is PASSED by grounding and CAUGHT only by consistency (verdict=POLARITY). Grounding alone is insufficient; consistency is the catch.
el-exposure — DEFERRED (matches reasoning-agent precedent)
Not exposed as el builtins this pass. The reasoning agent exposed ONLY analogy
(three seed-identified neighborhoods → the clean fixed-arity seed-CSV→descriptor JSON
pattern) and deferred its point-input / variadic-set modes (abduction, induction,
causal, planning). The verifier's grounding (claim POINT + variadic evidence SET) and
consistency (claim POINT + context + two poles + forbidden + scalar thresholds) are
exactly those shapes: no clean fixed-arity seed-CSV JSON mapping exists, and adding one
would require new JSON list-of-lists + point-vector marshaling absent from the codebase,
risking an elc rebuild/fold (violates the capped-fold-only rail). A claim is also an
arbitrary proposed POINT, not necessarily an existing node — so the point-native C API
is the correct primitive. Deferred deliberately; the C layer is complete and proven.
When exposed later, follow the same additive pass-through pattern used for the geo
operators: native engram_verify_*_json(el_val_t ...) in el_runtime.c (heavy runtime)
- a
__engram_verify_*_jsonwrapper inel_seed.c, resolving seed CSVs → descriptors and marshaling the claim vector — no fold needed for callability (shipped elc passes unknown-ident builtin calls straight through to the heavy-runtime C symbols).
Reach checks (FORMAL / CAUSAL / PREDICTIVE) — NOT STARTED
Honestly not started this pass; the two tractable-now checks (grounding + consistency) were driven to done-with-proof first as specified.
- CAUSAL already exists as a REASONING operator (
engram_reason_causal, intervention/temporal-precedence over the typed causal graph); a verifier wrapper that checks "does the claimed cause actually precede/influence" would compose it — not built. - FORMAL (logical consistency of a claim SET) needs an external checker (SMT/proof kernel) — the non-geometric seam; not built.
- PREDICTIVE (commit a prediction, check vs outcome, restructure on error) is the CGI research frontier; not built.
Reversal
Fully additive. To reverse: delete the four added files
(lang/runtime/engram_verify.{h,c}, engram/test/test_verify.c,
engram/test/run_verify_tests.sh) or git revert this commit. Nothing else references
them; no build wiring, no el registration, no store schema, no runtime path was changed.
Live :8742 was never touched.