From ca1347174524b2d4619f575f4b405fd614f58f42 Mon Sep 17 00:00:00 2001 From: Will Anderson Date: Thu, 13 Aug 2026 01:43:36 -0500 Subject: [PATCH] =?UTF-8?q?Verifier=20layer:=20grounding=20+=20consistency?= =?UTF-8?q?=20over=20the=20=C2=A75=20geometry=20/=20reasoning=20ops?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit 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. --- ...13-verifier-layer-grounding-consistency.md | 128 +++++++++ engram/test/run_verify_tests.sh | 24 ++ engram/test/test_verify.c | 244 ++++++++++++++++++ lang/runtime/engram_verify.c | 157 +++++++++++ lang/runtime/engram_verify.h | 118 +++++++++ 5 files changed, 671 insertions(+) create mode 100644 docs/runbooks/2026-08-13-verifier-layer-grounding-consistency.md create mode 100755 engram/test/run_verify_tests.sh create mode 100644 engram/test/test_verify.c create mode 100644 lang/runtime/engram_verify.c create mode 100644 lang/runtime/engram_verify.h diff --git a/docs/runbooks/2026-08-13-verifier-layer-grounding-consistency.md b/docs/runbooks/2026-08-13-verifier-layer-grounding-consistency.md new file mode 100644 index 0000000..2dfcd55 --- /dev/null +++ b/docs/runbooks/2026-08-13-verifier-layer-grounding-consistency.md @@ -0,0 +1,128 @@ +# 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) +```c +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) +```c +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), midpoint `o = ½(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 `forbidden` region it must be + far from (`engram_reason_point_fit` score ≥ `forbidden_thresh`), OR violates a + max-distance constraint to `context` (`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_*_json` wrapper in `el_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. diff --git a/engram/test/run_verify_tests.sh b/engram/test/run_verify_tests.sh new file mode 100755 index 0000000..ce47c45 --- /dev/null +++ b/engram/test/run_verify_tests.sh @@ -0,0 +1,24 @@ +#!/bin/sh +# Build + RUN the VERIFIER-layer tests (engram_verify.c): closed-form constructed +# cases for GROUNDING (anti-hallucination) and CONSISTENCY (polarity/negation +# inversion + geometric contradiction), each composing the reasoning point-fit +# (engram_reason.c) and the §5 geometry OPERATORS (engram_geometry.c). Pure C11 +# (stdlib + libm). Standalone — NOT folded through elc. Two passes: +# 1. PERF — optimised (-O2, no sanitizer): the functional gate. +# 2. SAFETY — ASan + UBSan on the same suite (memory-safety is size-independent). +set -e +HERE=$(cd "$(dirname "$0")" && pwd) +RT="$HERE/../../lang/runtime" +CC=${CC:-cc} +SRC="$HERE/test_verify.c $RT/engram_verify.c $RT/engram_reason.c $RT/engram_geometry.c $RT/engram_store.c $RT/engram_vindex.c" +WARN="-std=c11 -Wall -Wextra" +TMP=$(mktemp -d) + +echo "### PASS 1: PERF (optimised, un-sanitised) — functional gate" +$CC $WARN -O2 -I"$RT" $SRC -lm -o "$TMP/perf" +"$TMP/perf" + +echo +echo "### PASS 2: SAFETY (ASan/UBSan)" +$CC $WARN -O1 -g -fsanitize=address,undefined -fno-omit-frame-pointer -I"$RT" $SRC -lm -o "$TMP/safe" +ASAN_OPTIONS=${ASAN_OPTIONS:-detect_leaks=0} UBSAN_OPTIONS=halt_on_error=1 "$TMP/safe" diff --git a/engram/test/test_verify.c b/engram/test/test_verify.c new file mode 100644 index 0000000..f79ead2 --- /dev/null +++ b/engram/test/test_verify.c @@ -0,0 +1,244 @@ +/* Closed-form unit tests for the VERIFIER layer (engram_verify.c). Every case is a + * hand-built synthetic descriptor / claim point whose verdict is known in closed + * form — the checks are PROVEN, not declared. ASan/UBSan target. + * + * The headline case is CONSISTENCY's polarity check: the reassurance→accusation + * inversion ("you never fought" → "you argued") that no grammar check catches. */ +#include "engram_verify.h" +#include +#include +#include +#include + +static int failures = 0, checks = 0; +static void ok(const char* what, int cond) { + checks++; + if (!cond) { failures++; printf(" FAIL: %s\n", what); } + else printf(" ok: %s\n", what); +} +static void approx(const char* what, double got, double exp, double tol) { + ok(what, fabs(got - exp) <= tol); + if (fabs(got - exp) > tol) printf(" got=%.9g exp=%.9g\n", got, exp); +} + +/* ── descriptor builder (mirrors test_reason.c) ─────────────────────────────── */ +static float* vec(const double* v, int dim) { + float* f = malloc((size_t)dim * sizeof(float)); + for (int i = 0; i < dim; i++) f[i] = (float)v[i]; + return f; +} +static GeoDescriptor* mk(int dim, const double* centroid, + int n_axes, const double* axis_flat, const double* extents, + int n_members, const char** ids, double total_var) { + GeoDescriptor* g = calloc(1, sizeof(GeoDescriptor)); + g->dim = dim; + g->centroid = centroid ? vec(centroid, dim) : NULL; + g->global_mean = NULL; + g->n_axes = n_axes; + g->axes = n_axes ? calloc((size_t)n_axes, sizeof(GeoAxis)) : NULL; + double tr = 0; + for (int k = 0; k < n_axes; k++) { + g->axes[k].axis = vec(&axis_flat[(size_t)k * dim], dim); + g->axes[k].extent = extents[k]; + tr += extents[k] * extents[k]; + } + g->total_variance = (total_var >= 0) ? total_var : tr; + g->radius = sqrt(g->total_variance > 0 ? g->total_variance : 0); + g->n_members = n_members; g->n_embedded = n_members; + g->members = n_members ? calloc((size_t)n_members, sizeof(GeoMember)) : NULL; + for (int i = 0; i < n_members; i++) { + g->members[i].id = strdup(ids[i]); + g->members[i].membership = 1.0; + g->members[i].centrality = (double)(n_members - i); + g->members[i].embedded = 1; + } + g->hub_id = n_members ? strdup(ids[0]) : strdup(""); + g->k_core = 1; g->co_registration = 0.0; g->n_edges = 0; g->edges = NULL; + return g; +} + +int main(void) { + printf("== VERIFIER layer unit tests ==\n"); + + /* ══════════════════ GROUNDING — supported vs floating (hallucination) ════ */ + /* Two real neighborhoods: E0 at origin, E1 far along e0. A claim planted inside + * E0 is grounded; a claim floating far off-manifold (along an unmodeled axis) is + * flagged UNGROUNDED; a claim near E1 grounds to E1, not E0. */ + { + int dim = 4; + double c0[4] = {0,0,0,0}, c1[4] = {10,0,0,0}; + double ax[8] = {1,0,0,0, 0,1,0,0}; double ex[2] = {1,1}; + const char* i0[1] = {"E0"}, *i1[1] = {"E1"}; + GeoDescriptor* E0 = mk(dim, c0, 2, ax, ex, 1, i0, -1); + GeoDescriptor* E1 = mk(dim, c1, 2, ax, ex, 1, i1, -1); + const GeoDescriptor* ev[2] = {E0, E1}; + + /* (1) grounded claim — sits inside E0. */ + float in[4] = {0.3f, -0.2f, 0, 0}; + GeoGrounding g1; + int rc = engram_verify_grounding(in, dim, ev, 2, 1.0, 0.5, &g1); + ok("grounding returns 0", rc == 0); + printf("[grounding] IN score=%.4f grounded=%d best=%d dist=%.3f ortho=%.3f nearL2=%.3f\n", + g1.grounding, g1.grounded, g1.best, g1.best_distance, g1.best_ortho, g1.nearest_centroid_l2); + ok("planted-inside claim is GROUNDED", g1.grounded == 1); + ok("grounds to the nearest structure E0", g1.best == 0); + ok("grounded score high (>0.7)", g1.grounding > 0.7); + approx("off-model residual ~0 for in-distribution claim", g1.best_ortho, 0.0, 1e-4); + engram_verify_grounding_free(&g1); + + /* (2) hallucinated claim — floats far along the unmodeled e2 axis. */ + float out[4] = {0, 0, 50.0f, 0}; + GeoGrounding g2; + engram_verify_grounding(out, dim, ev, 2, 1.0, 0.5, &g2); + printf("[grounding] OUT score=%.6f grounded=%d best=%d dist=%.3f ortho=%.3f nearL2=%.3f\n", + g2.grounding, g2.grounded, g2.best, g2.best_distance, g2.best_ortho, g2.nearest_centroid_l2); + ok("floating claim is FLAGGED (ungrounded)", g2.grounded == 0); + ok("floating claim scores near zero (<0.01)", g2.grounding < 0.01); + ok("off-model residual is large (the hallucination signal)", g2.best_ortho > 40.0); + ok("nearest real structure is far (L2>40)", g2.nearest_centroid_l2 > 40.0); + engram_verify_grounding_free(&g2); + + /* (3) selection — a claim near E1 grounds to E1. */ + float nearE1[4] = {9.8f, 0.1f, 0, 0}; + GeoGrounding g3; + engram_verify_grounding(nearE1, dim, ev, 2, 1.0, 0.5, &g3); + printf("[grounding] E1 score=%.4f grounded=%d best=%d\n", g3.grounding, g3.grounded, g3.best); + ok("claim near E1 grounds to E1 (best=1)", g3.best == 1 && g3.grounded == 1); + engram_verify_grounding_free(&g3); + + engram_geo_free(E0); engram_geo_free(E1); + } + + /* ══════════════════ CONSISTENCY (a) — THE NEGATION-INVERSION CATCH ═══════ */ + /* The motivating failure, geometrically. Polarity axis along e0: + * pole_pos = the AFFIRM region ("argued / fought") centroid (+5, …) + * pole_neg = the NEGATE region ("never fought / at peace") centroid (−5, …) + * The grounded TRUTH (context) is the reassurance "you never fought" → sits on + * the NEGATE side (−5). The bad translation CLAIM "you argued" lands on the + * AFFIRM side (+4). Opposite sides of the negation axis ⇒ INVERSION flagged — + * even though "you argued" is perfectly grammatical. This is the catch. */ + { + int dim = 4; + double c_pos[4] = { 5, 0, 0, 0}; /* "argued / fought" */ + double c_neg[4] = {-5, 0, 0, 0}; /* "never fought / at peace"*/ + double c_truth[4] = {-5, 0, 0, 0}; /* context: the reassurance */ + double ax[4] = {1,0,0,0}; double ex[1] = {1}; + const char* ip[1]={"pos"},*in[1]={"neg"},*it[1]={"truth"}; + GeoDescriptor* POS = mk(dim, c_pos, 1, ax, ex, 1, ip, -1); + GeoDescriptor* NEG = mk(dim, c_neg, 1, ax, ex, 1, in, -1); + GeoDescriptor* CTX = mk(dim, c_truth, 1, ax, ex, 1, it, -1); + + /* the plausible LIE: "you argued" — grammatical, fluent, and INVERTED. */ + float lie[4] = { 4, 0, 0, 0}; + GeoConsistency cl; + int rc = engram_verify_consistency(lie, dim, CTX, POS, NEG, NULL, + 1.0, 0.10, 0.5, 0.0, &cl); + ok("consistency returns 0", rc == 0); + printf("[consistency] LIE verdict=%d inverted=%d claim_side=%.3f ref_side=%.3f sep=%.3f consist=%.3f\n", + cl.verdict, cl.inverted, cl.polarity_claim, cl.polarity_reference, cl.polarity_separation, cl.consistency); + ok("NEGATION INVERSION caught (inverted=1)", cl.inverted == 1); + ok("verdict = POLARITY", cl.verdict == GEO_CONSIST_POLARITY); + ok("claim sits on the AFFIRM pole (+)", cl.polarity_claim > 0); + ok("truth sits on the NEGATE pole (−)", cl.polarity_reference < 0); + ok("consistency collapses to 0 on inversion", cl.consistency < 1e-9); + + /* the FAITHFUL translation: "you were at peace" — same pole as the truth. */ + float ok_claim[4] = {-4, 0, 0, 0}; + GeoConsistency cok; + engram_verify_consistency(ok_claim, dim, CTX, POS, NEG, NULL, + 1.0, 0.10, 0.5, 0.0, &cok); + printf("[consistency] TRUE verdict=%d inverted=%d claim_side=%.3f consist=%.3f\n", + cok.verdict, cok.inverted, cok.polarity_claim, cok.consistency); + ok("faithful claim NOT flagged (inverted=0)", cok.inverted == 0); + ok("faithful claim verdict OK", cok.verdict == GEO_CONSIST_OK); + ok("faithful claim consistency = 1", cok.consistency > 0.999); + + /* a NEUTRAL claim near the midpoint must NOT false-trigger. */ + float neutral[4] = {0.1f, 0, 0, 0}; /* |side|=0.1 < deadzone 0.5 */ + GeoConsistency cn; + engram_verify_consistency(neutral, dim, CTX, POS, NEG, NULL, + 1.0, 0.10, 0.5, 0.0, &cn); + printf("[consistency] NEUT verdict=%d inverted=%d claim_side=%.3f consist=%.3f\n", + cn.verdict, cn.inverted, cn.polarity_claim, cn.consistency); + ok("neutral claim inside deadzone does NOT trigger inversion", cn.inverted == 0); + + engram_geo_free(POS); engram_geo_free(NEG); engram_geo_free(CTX); + } + + /* ══════════════════ CONSISTENCY (b) — GEOMETRIC contradiction ════════════ */ + /* A claim that sits INSIDE a forbidden region it should be far from, and a claim + * that violates a max-distance constraint to its context, are both flagged. */ + { + int dim = 4; + double c_ctx[4] = {0,0,0,0}; + double c_forb[4] = {0,10,0,0}; /* forbidden region, offset along e1 */ + double ax[8] = {0,1,0,0, 1,0,0,0}; double ex[2] = {1,1}; + const char* ic[1]={"ctx"},*ifb[1]={"forb"}; + GeoDescriptor* CTX = mk(dim, c_ctx, 2, ax, ex, 1, ic, -1); + GeoDescriptor* FORB = mk(dim, c_forb, 2, ax, ex, 1, ifb, -1); + + /* claim sitting inside the forbidden region → geometric contradiction. */ + float inside[4] = {0, 10.1f, 0, 0}; + GeoConsistency cf; + engram_verify_consistency(inside, dim, CTX, NULL, NULL, FORB, + 1.0, 0.10, 0.5, 0.0, &cf); + printf("[consistency] FORB verdict=%d geo_viol=%d forb_fit=%.4f consist=%.3f\n", + cf.verdict, cf.geo_violation, cf.forbidden_fit, cf.consistency); + ok("claim inside forbidden region FLAGGED", cf.geo_violation == 1); + ok("verdict = GEOMETRIC", cf.verdict == GEO_CONSIST_GEOMETRIC); + ok("forbidden fit is high (claim really is inside)", cf.forbidden_fit > 0.5); + + /* claim well clear of the forbidden region → not flagged. */ + float clear[4] = {0.2f, 0.1f, 0, 0}; + GeoConsistency cc; + engram_verify_consistency(clear, dim, CTX, NULL, NULL, FORB, + 1.0, 0.10, 0.5, 0.0, &cc); + printf("[consistency] CLR verdict=%d geo_viol=%d forb_fit=%.4f\n", + cc.verdict, cc.geo_violation, cc.forbidden_fit); + ok("claim clear of forbidden NOT flagged", cc.geo_violation == 0 && cc.verdict == GEO_CONSIST_OK); + + /* max-distance constraint: claim too far from context (off-axis, no poles). */ + float far[4] = {0, 8.0f, 0, 0}; + GeoConsistency cd; + engram_verify_consistency(far, dim, CTX, NULL, NULL, NULL, + 1.0, 0.10, 0.5, /*max_distance*/3.0, &cd); + printf("[consistency] DIST verdict=%d geo_viol=%d ctx_dist=%.3f\n", + cd.verdict, cd.geo_violation, cd.context_distance); + ok("claim beyond max_distance FLAGGED", cd.geo_violation == 1 && cd.verdict == GEO_CONSIST_GEOMETRIC); + approx("context distance measured correctly", cd.context_distance, 8.0, 1e-4); + + engram_geo_free(CTX); engram_geo_free(FORB); + } + + /* ══════════════════ COMBINED — grounded but INVERTED (the full plausible lie) */ + /* The most dangerous output: fluent, GROUNDED in real vocabulary, yet polarity- + * inverted. Grounding alone passes it; only consistency catches the lie. This is + * exactly why the verifier needs BOTH checks. */ + { + int dim = 4; + double c_pos[4] = { 5, 0, 0, 0}, c_neg[4] = {-5, 0, 0, 0}; + double ax[4] = {1,0,0,0}; double ex[1] = {2}; + const char* ip[1]={"pos"},*in[1]={"neg"}; + GeoDescriptor* POS = mk(dim, c_pos, 1, ax, ex, 1, ip, -1); + GeoDescriptor* NEG = mk(dim, c_neg, 1, ax, ex, 1, in, -1); + const GeoDescriptor* ev[2] = {POS, NEG}; + + float lie[4] = {5, 0, 0, 0}; /* "argued" — sits dead-center in the affirm region */ + GeoGrounding g; + engram_verify_grounding(lie, dim, ev, 2, 1.0, 0.5, &g); + GeoConsistency c; + engram_verify_consistency(lie, dim, NEG /*truth=never fought*/, POS, NEG, NULL, + 1.0, 0.10, 0.5, 0.0, &c); + printf("[combined] grounded=%d (score=%.3f) inverted=%d verdict=%d\n", + g.grounded, g.grounding, c.inverted, c.verdict); + ok("plausible lie PASSES grounding (it is real vocabulary)", g.grounded == 1); + ok("plausible lie is CAUGHT by consistency (inverted)", c.inverted == 1); + ok("=> grounding alone is insufficient; consistency is the catch", + g.grounded == 1 && c.verdict == GEO_CONSIST_POLARITY); + engram_verify_grounding_free(&g); + engram_geo_free(POS); engram_geo_free(NEG); + } + + printf("\n== %d checks, %d failures ==\n", checks, failures); + return failures ? 1 : 0; +} diff --git a/lang/runtime/engram_verify.c b/lang/runtime/engram_verify.c new file mode 100644 index 0000000..819d62d --- /dev/null +++ b/lang/runtime/engram_verify.c @@ -0,0 +1,157 @@ +/* engram_verify.c — the VERIFIER layer. Pure compositions over engram_reason.h + + * engram_geometry.h. stdlib + libm only; READ-ONLY over its inputs; touches no + * store/index/activation. See engram_verify.h for the design and the frame contract. */ +#include "engram_verify.h" +#include +#include +#include + +/* ── small float-vector helpers (mirror engram_reason.c) ────────────────────── */ +static double vdot(const float* a, const float* b, int dim) { + double s = 0; for (int i = 0; i < dim; i++) s += (double)a[i] * (double)b[i]; return s; +} +static double l2(const float* a, const float* b, int dim) { + double s = 0; for (int i = 0; i < dim; i++) { double d = (double)a[i] - (double)b[i]; s += d * d; } + return sqrt(s); +} + +/* ═══════════════════════════════════════════════════════ GROUNDING ══════════ */ +int engram_verify_grounding(const float* claim, int dim, + const GeoDescriptor* const* evidence, int n_evidence, + double ext_floor, double ground_threshold, + GeoGrounding* out) { + if (!claim || dim <= 0 || !evidence || n_evidence < 1 || !out) return -1; + if (!(ext_floor > 0)) ext_floor = 1.0; + if (!(ground_threshold > 0 && ground_threshold < 1)) ground_threshold = 0.5; + memset(out, 0, sizeof *out); + out->n_evidence = n_evidence; + out->best = -1; + out->nearest_centroid_l2 = INFINITY; + out->scores = malloc((size_t)n_evidence * sizeof(double)); + if (!out->scores) return -1; + + double best = -1; + for (int i = 0; i < n_evidence; i++) { + const GeoDescriptor* e = evidence[i]; + GeoFit f; + if (!e || e->dim != dim || !e->centroid || + engram_reason_point_fit(e, claim, ext_floor, &f) != 0) { + out->scores[i] = 0.0; + continue; + } + out->scores[i] = f.score; + double cl2 = l2(claim, e->centroid, dim); + if (cl2 < out->nearest_centroid_l2) out->nearest_centroid_l2 = cl2; + if (out->best < 0 || f.score > best) { + best = f.score; + out->best = i; + out->grounding = f.score; + out->best_distance = f.distance; + out->best_ortho = f.ortho_residual; + } + } + if (out->best < 0) { out->grounding = 0.0; out->best_distance = INFINITY; } + out->grounded = (out->grounding >= ground_threshold) ? 1 : 0; + return 0; +} +void engram_verify_grounding_free(GeoGrounding* out) { + if (!out) return; + free(out->scores); out->scores = NULL; +} + +/* ═══════════════════════════════════════════════════════ CONSISTENCY ════════ */ +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) { + if (!claim || dim <= 0 || !out) return -1; + if (!(ext_floor > 0)) ext_floor = 1.0; + if (!(deadzone_frac >= 0 && deadzone_frac < 1)) deadzone_frac = 0.10; + if (!(forbidden_thresh > 0 && forbidden_thresh < 1)) forbidden_thresh = 0.5; + memset(out, 0, sizeof *out); + out->verdict = GEO_CONSIST_OK; + out->consistency = 1.0; + + int do_polarity = (pole_pos && pole_neg); + int do_distance = (max_distance > 0); + if ((do_polarity || do_distance) && + (!context || context->dim != dim || !context->centroid)) return -1; + if (do_polarity && (pole_pos->dim != dim || pole_neg->dim != dim || + !pole_pos->centroid || !pole_neg->centroid)) return -1; + if (forbidden && (forbidden->dim != dim || !forbidden->centroid)) return -1; + + double pol_score = 1.0, geo_score = 1.0; + + /* ── (a) POLARITY / negation inversion ─────────────────────────────────── */ + if (do_polarity) { + /* axis p = (c_pos − c_neg); midpoint o = ½(c_pos + c_neg). */ + float* p = malloc((size_t)dim * sizeof(float)); + float* o = malloc((size_t)dim * sizeof(float)); + if (!p || !o) { free(p); free(o); return -1; } + double pn2 = 0; + for (int i = 0; i < dim; i++) { + double dpos = (double)pole_pos->centroid[i], dneg = (double)pole_neg->centroid[i]; + p[i] = (float)(dpos - dneg); + o[i] = (float)(0.5 * (dpos + dneg)); + pn2 += (dpos - dneg) * (dpos - dneg); + } + double pn = sqrt(pn2); + out->polarity_separation = 0.5 * pn; + if (pn > 1e-12) { + /* signed positions along the axis (projection of (x − o) onto unit p). */ + float* cdo = malloc((size_t)dim * sizeof(float)); /* claim − o */ + float* rdo = malloc((size_t)dim * sizeof(float)); /* context − o */ + if (!cdo || !rdo) { free(p); free(o); free(cdo); free(rdo); return -1; } + for (int i = 0; i < dim; i++) { + cdo[i] = (float)((double)claim[i] - (double)o[i]); + rdo[i] = (float)((double)context->centroid[i] - (double)o[i]); + } + double claim_side = vdot(cdo, p, dim) / pn; /* units: emb-space length */ + double ref_side = vdot(rdo, p, dim) / pn; + out->polarity_claim = claim_side; + out->polarity_reference = ref_side; + double dz = deadzone_frac * out->polarity_separation; /* neutral band */ + if (fabs(claim_side) > dz && fabs(ref_side) > dz && + (claim_side > 0) != (ref_side > 0)) { + out->inverted = 1; + pol_score = 0.0; /* opposite poles ⇒ zero consistency */ + } else if (fabs(claim_side) <= dz || fabs(ref_side) <= dz) { + pol_score = 0.5; /* neutral / undecided */ + } else { + pol_score = 1.0; /* same pole ⇒ consistent */ + } + free(cdo); free(rdo); + } + free(p); free(o); + } + + /* ── (b) GEOMETRIC contradiction ───────────────────────────────────────── */ + if (forbidden) { + GeoFit f; + if (engram_reason_point_fit(forbidden, claim, ext_floor, &f) == 0) { + out->forbidden_fit = f.score; + if (f.score >= forbidden_thresh) { + out->geo_violation = 1; + double g = 1.0 - f.score; if (g < 0) g = 0; + if (g < geo_score) geo_score = g; + } + } + } + if (do_distance) { + out->context_distance = l2(claim, context->centroid, dim); + if (out->context_distance > max_distance) { + out->geo_violation = 1; + geo_score = 0.0; + } + } + + /* ── verdict + scalar (polarity is the headline; both flags stay visible) ─ */ + out->consistency = (pol_score < geo_score) ? pol_score : geo_score; + if (out->inverted) out->verdict = GEO_CONSIST_POLARITY; + else if (out->geo_violation) out->verdict = GEO_CONSIST_GEOMETRIC; + else out->verdict = GEO_CONSIST_OK; + return 0; +} diff --git a/lang/runtime/engram_verify.h b/lang/runtime/engram_verify.h new file mode 100644 index 0000000..156140b --- /dev/null +++ b/lang/runtime/engram_verify.h @@ -0,0 +1,118 @@ +/* engram_verify.h — the VERIFIER layer: GROUNDING + CONSISTENCY over the live + * geometry (engram_geometry.h) and reasoning (engram_reason.h) operators. + * + * The geometry PROPOSES (cheap, creative, sometimes wrong); the verifier DISPOSES. + * This layer catches the class of failure a grammar check never sees: a fluent, + * confident, WRONG output — the "plausible lie". The motivating case: a translation + * that DELETED a negation so "you never fought" became "you argued" — reassurance + * inverted into accusation, grammatical and invisible, catchable ONLY by the geometry. + * + * GROUNDING claim → is there ANY real structure that supports it, or is it + * floating free of the manifold? (anti-hallucination gate) + * CONSISTENCY claim → does it CONTRADICT the established structure? Two catches: + * (a) POLARITY: the claim lands on the OPPOSITE side of a negation + * axis from the grounded truth (the reassurance→accusation catch), + * (b) GEOMETRIC: the claim sits inside a region it must be far from, + * or violates a max-distance constraint to its context. + * + * PURE + READ-ONLY (stdlib + libm only): every function consumes a claim POINT + * (float* in R^dim) plus GeoDescriptor(s), and NEVER touches the store, index, or + * activation. All geometry is delegated to engram_reason_point_fit / engram_geo_*; + * this file only composes and applies thresholds. + * + * FRAME CONTRACT (inherited): the claim point and every descriptor passed together + * MUST share emb `dim` and the same `global_mean` frame — exactly the §5 operator + * contract. A function returns <0 on a dim/frame mismatch or bad argument. + */ +#ifndef ENGRAM_VERIFY_H +#define ENGRAM_VERIFY_H + +#include "engram_geometry.h" +#include "engram_reason.h" + +/* ═══════════════════════════════════════════════════════════════════════════ + * GROUNDING — anti-hallucination. Score how well a claimed POINT is supported by + * the ACTUAL structure: fit the claim against every real evidence neighborhood + * (engram_reason_point_fit → in-distribution Mahalanobis + off-model orthogonal + * residual) and take the BEST supporter. A claim that sits inside real structure + * scores high (grounded); a claim floating far from every neighborhood scores low + * on all of them → flagged UNGROUNDED (a hallucination). + * + * This is an ABSOLUTE-THRESHOLD gate, deliberately distinct from ABDUCTION (which + * always RANKS and picks a winner among competing hypotheses): grounding asks the + * prior question — "is there any real support at all?" — and is allowed to answer no. + * The off-model `ortho_residual` is the sharpest hallucination signal: energy in a + * direction the manifold does not even span. + * ═══════════════════════════════════════════════════════════════════════════ */ +typedef struct { + double grounding; /* ∈[0,1]: overall support = best fit score */ + int grounded; /* 1 iff grounding >= ground_threshold */ + int best; /* index of best-supporting evidence structure, or −1 */ + double best_distance; /* full point-to-manifold distance to the best */ + double best_ortho; /* off-model orthogonal residual of the best fit */ + double nearest_centroid_l2;/* raw L2 to the nearest evidence centroid (coarse) */ + int n_evidence; + double* scores; /* per-evidence fit score, higher = better (owned)*/ +} GeoGrounding; +/* ext_floor>0 guards zero-extent axes (default 1.0). ground_threshold∈(0,1): the + * minimum best-fit score to call the claim grounded (default 0.5). */ +int engram_verify_grounding(const float* claim, int dim, + const GeoDescriptor* const* evidence, int n_evidence, + double ext_floor, double ground_threshold, + GeoGrounding* out); +void engram_verify_grounding_free(GeoGrounding* out); + +/* ═══════════════════════════════════════════════════════════════════════════ + * CONSISTENCY — contradiction detection. Does the claim contradict the established + * structure? Two independent sub-checks (either can fire; both flags are reported): + * + * (a) POLARITY / negation inversion. A polarity axis p is defined by two REAL + * poles — pole_pos (asserts X) and pole_neg (asserts ¬X): + * p = (c_pos − c_neg)/‖·‖ , midpoint o = ½(c_pos + c_neg). + * The claim's side = p·(claim − o); the reference's side = p·(c_context − o). + * If the two sides have OPPOSITE sign AND both clear the neutral deadzone, the + * claim asserts the polarity opposite to the grounded truth → INVERSION flagged. + * This is the "you never fought"→"you argued" catch: the truth ("never fought") + * sits on the negate pole, the claim ("argued") on the affirm pole → opposite + * sides → flagged, though every word is grammatical. + * + * (b) GEOMETRIC contradiction. The claim sits INSIDE a `forbidden` region it must + * be far from (point_fit score to forbidden ≥ forbidden_thresh), OR it violates + * a max-distance constraint to its context centroid (L2 > max_distance). + * + * pole_pos/pole_neg may both be NULL to skip the polarity check; forbidden may be + * NULL and max_distance≤0 to skip the geometric check. `context` (the grounded truth + * region) is required whenever polarity or the distance constraint is used. + * ═══════════════════════════════════════════════════════════════════════════ */ +typedef enum { + GEO_CONSIST_OK = 0, /* consistent with context */ + GEO_CONSIST_POLARITY = 1, /* polarity/negation inversion (asserts ¬X where X) */ + GEO_CONSIST_GEOMETRIC = 2 /* geometric contradiction (in forbidden / too far) */ +} GeoConsistencyVerdict; +typedef struct { + GeoConsistencyVerdict verdict; /* headline (polarity takes precedence) */ + double consistency; /* ∈[0,1]: min over the checks (1 = fully consistent)*/ + /* polarity sub-check */ + int inverted; /* 1 iff a polarity inversion was detected */ + double polarity_claim; /* p·(claim − o) (signed position on the axis)*/ + double polarity_reference; /* p·(c_context − o) (the grounded truth's side) */ + double polarity_separation; /* ½‖c_pos − c_neg‖ (the axis half-length / scale)*/ + /* geometric sub-check */ + int geo_violation; /* 1 iff a geometric contradiction was detected */ + double forbidden_fit; /* claim's point_fit score to the forbidden region*/ + double context_distance; /* L2(claim, c_context) */ +} GeoConsistency; +/* ext_floor>0 (default 1.0). deadzone_frac∈[0,1): a polarity side within + * deadzone_frac·separation of the midpoint is "neutral" and never triggers inversion + * (default 0.10). forbidden_thresh∈(0,1): fit-to-forbidden at/above which the claim + * counts as inside the forbidden region (default 0.5). max_distance>0 enables the + * distance constraint; ≤0 disables it. */ +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); + +#endif /* ENGRAM_VERIFY_H */