einsiedlerkrebs

A diff-scoped, fail-closed property/invariant testing PR gate, sibling to marmorkrebs and built on the same discipline: a result only counts with evidence, and every degenerate state (no target exercised, an engine that can't prove it's live, a vacuous run) is an explicit non-passing verdict — never a silent green.

einsiedlerkrebs runs property tests across languages through pluggable lanes, all behind one fail-closed verdict + exit-code contract (like marmorkrebs normalizes many mutation tools). The JS/TS lane uses fast-check (*.eks.mjs modules exporting properties(fc) → { name, coversSymbol, property } — see examples/sample/clamp.eks.mjs); the Python lane uses Hypothesis (*.eks.py). See "Lanes (languages)" below.

Two ways to get invariants. The base tool is targeted: it tests the invariants someone wrote as *.eks.mjs modules — no authored properties, no coverage. Use it deliberately on the functions where an invariant is worth stating (parsers, math/clamping helpers, serialization round-trips). Read "Authoring good invariants" below before writing your first one by hand.

The --author mode (see "AI-authoring mode" below) is what makes einsiedler point-and-go: an LLM proposes the invariants for your changed files, and every proposal is base-validated so a hallucinated invariant (one that's simply wrong about your existing code) is discarded before it can produce a false signal. You still don't get magic — you get a validated first cut you can review and keep.

Usage

# Prove the fast-check lane is actually live before trusting any result from it
einsiedlerkrebs --validate

# Run named property modules (dir or comma-list of *.eks.mjs files)
einsiedlerkrebs --repo /path/to/repo --modules examples/sample

# Tune the property search
einsiedlerkrebs --repo /path/to/repo --modules src/props \
  --seed 42 --num-runs 500 --min-runs 100

# Diff-scoped, persisted, and tolerant of an empty target set
einsiedlerkrebs --repo /path/to/repo --modules src/props \
  --base main --report-file report.json --allow-empty

Flag	Meaning
--validate	Run the canary lane; must catch a deliberately-false property or the wiring is broken
--repo <path>	Repo to run against (used for --base diffing and seed derivation)
--modules <dir-or-comma-list>	Directory of *.eks.mjs files, or a comma-separated list
--base <ref>	Print the changed-file surface vs this git ref (diff scoping evidence)
--seed <n>	fast-check seed (defaults to a value derived from repo HEAD, or 42)
--num-runs <n>	Number of fast-check runs per property (default 500)
--min-runs <n>	Minimum runs before a filtered/vacuous property is flagged (default 100)
--allow-empty	Treat zero exercised targets as an explicit pass (PASS_EMPTY) instead of NO_PROPERTY
--report-file <path>	Persist the full JSON report (written before exit, survives a failing gate)

Lanes (languages)

Each lane is a per-language adapter behind the shared core/report.mjs verdict + exit codes. The lane is auto-detected from the module extension, or forced with --lane <id>:

Language	--lane	Modules	Library	Runtime
JS/TS	fast-check	*.eks.mjs	fast-check (bundled)	Node, in-process
Python	hypothesis	*.eks.py	Hypothesis (pip install hypothesis)	python3 subprocess
C# (scaffold)	csharp-fscheck	*.cs, *.csproj	Roslyn + FsCheck (planned)	Scaffold-only

einsiedlerkrebs --validate --lane hypothesis            # prove the Python lane is live
einsiedlerkrebs --validate --lane csharp-fscheck        # phase-1 C# wiring proof
einsiedlerkrebs --modules src/props --lane hypothesis   # (or auto-detected from *.eks.py)
einsiedlerkrebs --modules src/props --lane csharp-fscheck

A Python module exposes properties() returning dicts with given (a Hypothesis strategy or a list of them) and property (returns a bool, fast-check style, or asserts):

from hypothesis import strategies as st

def properties():
    return [{
        "name": "result within [lo,hi]",
        "coversSymbol": "clamp",
        "given": [st.integers(), st.integers(), st.integers()],
        "property": lambda x, a, b: min(a, b) <= clamp(x, a, b) <= max(a, b),
    }]

Fail-closed per lane. --validate proves the selected lane catches its own planted canary before that lane is trusted; a lane whose runtime/library is absent is QUARANTINED (exit 5) and reported SKIP by validate:provider — never a silent pass. Point python3 at a venv with EINSIEDLERKREBS_PYTHON=/path/to/venv/bin/python.

Adding a language. Non-JS lanes run out of process: a thin runner (in that language) discovers its *.eks.<lang> modules, drives its property library, and prints a normalized PropertyResult[] as JSON on stdout — the generic SubprocessLane (einsiedler/lanes/subprocess.mjs) just spawns it and parses. Adding C# (Roslyn+FsCheck), Swift (SwiftCheck), Go (gopter/testing/quick), Rust (proptest), or C++ (RapidCheck) is "write a runner + register a lane", no framework changes. The protocol generalizes the cross-library quirks: seed is a string reproduction token (int seed, Hypothesis @reproduce_failure blob, proptest byte-array, …), shrinkSteps is nullable (Hypothesis and Go testing/quick don't expose it), counterexample is a pre-formatted string, and the runner separates a graceful FALSIFIED from an unhandled ERROR.

AI-authoring mode (--author)

Instead of hand-writing *.eks.mjs modules, let an LLM propose invariants for the files you changed — and trust them only after they've been validated against your existing code.

einsiedlerkrebs --author --repo /path/to/repo --base main
einsiedlerkrebs --author --repo . --base main --engine "my-llm-cmd"   # custom engine

Pipeline:

1. Derive — the changed source files vs --base (reuses core/diff.mjs), keeping JS/TS files with plausibly-pure exported functions.
2. AI-author — for each file, an LLM is asked to propose fast-check invariants as a .eks.mjs module. The prompt demands type-aware generators (never untyped garbage against a typed param — the false-positive lesson below) and prefers low-risk never-crash / round-trip / idempotence / range invariants over risky semantic guesses. The default engine is the local, free ask-opencode (Qwen), falling back to ask-codex; --engine <cmd> overrides both (the prompt is passed as the trailing argument). Authored modules are persisted to authored/<safe-name>.eks.mjs.
3. Base-validate (the anti-hallucination filter) — each authored property is run against the base version of the code in a clean git worktree. Any property that falsifies on base is wrong about existing behavior — a hallucination — and is discarded. Only base-holders survive. Fail-closed: a property that errored or ran vacuously on base doesn't count either.
4. Head-run — the surviving, base-validated properties run against HEAD via the normal fast-check lane. A falsification here is a real behavior change / bug worth review — exactly the signal the gate exists to produce.
5. Report — files scanned, invariants authored, discarded-on-base (hallucinations filtered), survivors, and HEAD falsifications, plus the standard fail-closed verdict.

Worked run (a clean clamp at base, an off-by-one introduced at HEAD; invariants written by Qwen via ask-opencode):

✓ HELD       [clamp] [authored] never-crash: clamp(x, lo, hi) does not throw for all valid inputs
✗ FALSIFIED  [clamp] [authored] bounds: result is within [min(lo,hi), max(lo,hi)] inclusive
             counterexample=[0,0,0]
=> VERDICT FALSIFIED (exit 2)
  --- AI-authoring pipeline ---
  files scanned=1  authored=1  invariants authored=2
  discarded on base: 0 hallucination(s) (falsified base) + 0 unvalidatable
  base-validated survivors=2  HEAD falsifications=1

--author flag	Meaning
--author	Enable AI-authoring mode (requires --repo and --base)
--engine <cmd>	Override the authoring engine; the prompt is appended as the last arg
--out-dir <path>	Where authored .eks.mjs modules are written (default authored/)
--no-keep-authored	Don't persist authored modules to disk

Limitations of this first cut. Parsing free-form LLM output is the fragile part: the engine's response is scanned for a fenced code block containing a properties(fc) export, its import is normalized to the source, and it's syntax-checked — anything unparseable is skipped (never trusted). New files have no base version, so their invariants can't be validated and are discarded. Sources are imported directly, so plain ESM is the solid path; TypeScript needing a real compile step degrades to a skip. A v2 would add the marmorkrebs mutation-filter (keep only invariants a mutant can actually kill, to weed out trivially-true tautologies).

Fail-closed contract

• validate-provider canary. fixtures/canary/canary.eks.mjs is a deliberately false property that fast-check must report FALSIFIED. Run --validate before trusting any other result from this lane — if the canary isn't caught, the engine wiring is broken silently, which is exactly the failure mode a gate exists to prevent.

• Distinct exit code per failure class, mirroring marmorkrebs:

  Code	Verdict	Meaning
  0	PASS / PASS_EMPTY / ENGINE_OK	clean, or explicitly empty with --allow-empty
  2	FALSIFIED	a property failed
  3	NO_PROPERTY	no targets ran and --allow-empty wasn't set
  4	VACUOUS	property held only because filtering exhausted it
  5	QUARANTINED	the engine itself failed to validate
  6	ERROR	crash, import failure, or timeout

• Diff scoping. --base <ref> runs core/diff.mjs's changedFiles against the given repo and prints the changed-file surface the gate ran against, so a report shows what it actually covered rather than implying whole-repo coverage.

• Evidence survives a failing exit. --report-file <path> writes the full JSON report (report + verdict) to disk before the process exits, so a red gate still leaves behind its evidence.

Authoring good invariants

einsiedlerkrebs is only as good as the properties you feed it, and the single biggest failure mode is a generator that doesn't match the parameter's declared type.

If a function's parameter is typed string and you generate inputs with something broader than that — e.g. fc.anything() instead of fc.string() — fast-check will happily hand it numbers, objects, undefined, symbols, and the "crash" it reports is just TypeScript/JS enforcing a type constraint the code never claimed to relax. That is not a bug in the code under test; it's a bug in the property. This is the exact lesson from the first dogfood run against real authored properties: over-broad generators produced false "crashes" the type system had already ruled out, wasting review time on non-issues and eroding trust in the gate's signal.

Rules of thumb:

• Match the generator to the declared type, not to "whatever might get passed at runtime." If you want to test what happens with malformed input, that's a separate, explicitly-named property (e.g. "rejects non-string input"), not the default case.
• Prefer the narrowest fc.* combinator that's still representative: fc.string()/fc.stringMatching(...) over fc.anything(), fc.integer({min,max}) over unbounded fc.integer() when the domain is bounded, fc.constantFrom(...) for enums.
• Name properties after the invariant, not the mechanism ("result within [lo,hi]", not "property 1") — see examples/sample/clamp.eks.mjs.
• If a property needs fc.pre(...) filtering to hold, watch for VACUOUS (exit 4): it means the filter threw away too many cases to trust the "pass."

Layout

core/            shared report shape + verdict logic (report.mjs), git diff helpers (diff.mjs)
einsiedler/      cli.mjs (lane-agnostic), fast-check-lane.mjs, author-mode.mjs (--author pipeline)
einsiedler/lanes/    lane registry + interface: index.mjs, lane.mjs, fast-check.mjs,
                     subprocess.mjs (generic out-of-process adapter), hypothesis.mjs
einsiedler/runners/  per-language runners that emit the JSON PropertyResult protocol
                     (hypothesis_runner.py)
fixtures/        validate-provider canaries per lane (canary.eks.mjs, canary.eks.py);
                 csharp/         scaffold canary for `csharp-fscheck`
                 author-demo/ — deterministic mock engine for the --author smoke test
examples/sample/ a worked example (clamp.mjs + clamp.eks.mjs)
scripts/         validate-provider.mjs — CI gate proving every installed lane's canary is live
test/            node:test suite

License

MIT — see LICENSE.