Skip to content

Commit cab3d96

Browse files
feat: AI-authoring mode (--author) with base-validation anti-hallucination filter (#1)
Adds 'einsiedler --author --repo <r> --base <ref> [--engine <cmd>]': an LLM proposes fast-check invariants for changed files, and every proposal is validated against the BASE version of the code so a hallucinated invariant (wrong about existing behavior) is discarded before it can produce a false signal. Surviving, base-validated invariants run against HEAD; falsifications there are real behavior changes worth review. Pipeline (einsiedler/author-mode.mjs): derive changed source files (core/diff), AI-author via ask-opencode (Qwen, free/local) with ask-codex fallback and a --engine override, parse+normalize+syntax-check the returned module, base- validate in a clean git worktree, head-run survivors via the fast-check lane, report fail-closed stats. Type-aware generator prompt guards the README false- positive lesson. v2 note: marmorkrebs mutation-filter left out of this first cut. - einsiedler/author-mode.mjs: full pipeline + pure helpers (export detection, LLM-output extraction, import normalization, syntax check). - einsiedler/cli.mjs: --author/--engine/--out-dir/--no-keep-authored wiring; existing --modules/--validate unchanged. - fixtures/author-demo/mock-engine.mjs: deterministic engine for a hermetic smoke test (canned 3-invariant module: 1 survivor, 1 head-falsifier, 1 base-hallucination). - test/einsiedler-author.test.mjs: pure-helper unit tests + end-to-end pipeline smoke test (real git worktree, mock engine, asserts hallucination filtered and HEAD behavior change surfaced, exit 2). - README: AI-authoring section, flags, worked run, honest limitations. - package.json lint: check author-mode.mjs + mock-engine.mjs.
1 parent 7349b6d commit cab3d96

6 files changed

Lines changed: 812 additions & 10 deletions

File tree

README.md

Lines changed: 76 additions & 9 deletions
Original file line numberDiff line numberDiff line change
@@ -11,13 +11,17 @@ in `*.eks.mjs` modules against symbols you name. Each module exports a `properti
1111
function returning `{ name, coversSymbol, property }` entries — see
1212
`examples/sample/clamp.eks.mjs` for the shape.
1313

14-
**Be honest about what this is:** einsiedlerkrebs is a **targeted** tool, not a
15-
point-and-go one. It can only test the invariants someone — a human or an AI — actually
16-
wrote down as `*.eks.mjs` modules. No authored properties, no coverage. Use it
17-
deliberately on the functions where an invariant is worth stating (parsers,
18-
math/clamping helpers, serialization round-trips), not as a blanket CI requirement that
19-
somehow "just works" the moment it's wired in. Read "Authoring good invariants" below
20-
before writing your first one.
14+
**Two ways to get invariants.** The base tool is **targeted**: it tests the invariants
15+
someone wrote as `*.eks.mjs` modules — no authored properties, no coverage. Use it
16+
deliberately on the functions where an invariant is worth stating (parsers, math/clamping
17+
helpers, serialization round-trips). Read "Authoring good invariants" below before writing
18+
your first one by hand.
19+
20+
The **`--author` mode** (see "AI-authoring mode" below) is what makes einsiedler
21+
point-and-go: an LLM proposes the invariants for your changed files, and every proposal is
22+
**base-validated** so a hallucinated invariant (one that's simply wrong about your existing
23+
code) is discarded before it can produce a false signal. You still don't get magic — you
24+
get a validated first cut you can review and keep.
2125

2226
## Usage
2327

@@ -49,6 +53,68 @@ einsiedlerkrebs --repo /path/to/repo --modules src/props \
4953
| `--allow-empty` | Treat zero exercised targets as an explicit pass (`PASS_EMPTY`) instead of `NO_PROPERTY` |
5054
| `--report-file <path>` | Persist the full JSON report (written before exit, survives a failing gate) |
5155

56+
## AI-authoring mode (`--author`)
57+
58+
Instead of hand-writing `*.eks.mjs` modules, let an LLM propose invariants for the files
59+
you changed — and trust them only after they've been validated against your existing code.
60+
61+
```bash
62+
einsiedlerkrebs --author --repo /path/to/repo --base main
63+
einsiedlerkrebs --author --repo . --base main --engine "my-llm-cmd" # custom engine
64+
```
65+
66+
Pipeline:
67+
68+
1. **Derive** — the changed source files vs `--base` (reuses `core/diff.mjs`), keeping
69+
JS/TS files with plausibly-pure exported functions.
70+
2. **AI-author** — for each file, an LLM is asked to propose fast-check invariants as a
71+
`.eks.mjs` module. The prompt demands **type-aware generators** (never untyped garbage
72+
against a typed param — the false-positive lesson below) and prefers low-risk
73+
never-crash / round-trip / idempotence / range invariants over risky semantic guesses.
74+
The default engine is the local, free `ask-opencode` (Qwen), falling back to `ask-codex`;
75+
`--engine <cmd>` overrides both (the prompt is passed as the trailing argument).
76+
Authored modules are persisted to `authored/<safe-name>.eks.mjs`.
77+
3. **Base-validate (the anti-hallucination filter)** — each authored property is run
78+
against the **base** version of the code in a clean `git worktree`. Any property that
79+
**falsifies on base** is *wrong about existing behavior* — a hallucination — and is
80+
**discarded**. Only base-holders survive. Fail-closed: a property that errored or ran
81+
vacuously on base doesn't count either.
82+
4. **Head-run** — the surviving, base-validated properties run against **HEAD** via the
83+
normal fast-check lane. A **falsification here is a real behavior change / bug** worth
84+
review — exactly the signal the gate exists to produce.
85+
5. **Report** — files scanned, invariants authored, discarded-on-base (hallucinations
86+
filtered), survivors, and HEAD falsifications, plus the standard fail-closed verdict.
87+
88+
Worked run (a clean `clamp` at base, an off-by-one introduced at HEAD; invariants written
89+
by Qwen via `ask-opencode`):
90+
91+
```
92+
✓ HELD [clamp] [authored] never-crash: clamp(x, lo, hi) does not throw for all valid inputs
93+
✗ FALSIFIED [clamp] [authored] bounds: result is within [min(lo,hi), max(lo,hi)] inclusive
94+
counterexample=[0,0,0]
95+
=> VERDICT FALSIFIED (exit 2)
96+
--- AI-authoring pipeline ---
97+
files scanned=1 authored=1 invariants authored=2
98+
discarded on base: 0 hallucination(s) (falsified base) + 0 unvalidatable
99+
base-validated survivors=2 HEAD falsifications=1
100+
```
101+
102+
| `--author` flag | Meaning |
103+
|---|---|
104+
| `--author` | Enable AI-authoring mode (requires `--repo` and `--base`) |
105+
| `--engine <cmd>` | Override the authoring engine; the prompt is appended as the last arg |
106+
| `--out-dir <path>` | Where authored `.eks.mjs` modules are written (default `authored/`) |
107+
| `--no-keep-authored` | Don't persist authored modules to disk |
108+
109+
> **Limitations of this first cut.** Parsing free-form LLM output is the fragile part: the
110+
> engine's response is scanned for a fenced code block containing a `properties(fc)` export,
111+
> its import is normalized to the source, and it's syntax-checked — anything unparseable is
112+
> skipped (never trusted). New files have no base version, so their invariants can't be
113+
> validated and are discarded. Sources are imported directly, so plain ESM is the solid
114+
> path; TypeScript needing a real compile step degrades to a skip. A **v2** would add the
115+
> marmorkrebs mutation-filter (keep only invariants a mutant can actually kill, to weed out
116+
> trivially-true tautologies).
117+
52118
## Fail-closed contract
53119

54120
- **validate-provider canary.** `fixtures/canary/canary.eks.mjs` is a deliberately false
@@ -105,8 +171,9 @@ Rules of thumb:
105171

106172
```
107173
core/ shared report shape + verdict logic (report.mjs), git diff helpers (diff.mjs)
108-
einsiedler/ cli.mjs, fast-check-lane.mjs
109-
fixtures/ validate-provider canary (fixtures/canary/canary.eks.mjs)
174+
einsiedler/ cli.mjs, fast-check-lane.mjs, author-mode.mjs (the --author pipeline)
175+
fixtures/ validate-provider canary (fixtures/canary/canary.eks.mjs);
176+
author-demo/ — deterministic mock engine for the --author smoke test
110177
examples/sample/ a worked example (clamp.mjs + clamp.eks.mjs)
111178
scripts/ validate-provider.mjs — CI gate proving the canary is live
112179
test/ node:test suite

0 commit comments

Comments
 (0)