Skip to content

Commit fd36055

Browse files
feat(lanes): multi-language property lanes; add a Python/Hypothesis lane
Refactor the engine into pluggable per-language lanes behind the existing fail-closed core/report.mjs verdict + exit codes (marmorkrebs' multi-tool discipline, for property testing). The lane is auto-detected from the module extension or forced with --lane; core/report.mjs is unchanged (already language-agnostic). - Lane interface + registry (einsiedler/lanes/): fast-check (JS, in-process) becomes a lane implementing the interface; a generic SubprocessLane spawns a per-language runner that emits a normalized PropertyResult[] as JSON on stdout. - Python/Hypothesis lane (*.eks.py + einsiedler/runners/hypothesis_runner.py): a real, canary-validated proof of concept with shrunk counterexamples; a bool-returning property is wrapped so Hypothesis' bare-False-is-pass quirk can't hide a failure, and Unsatisfiable maps to VACUOUS. - Protocol generalized up front for the future Swift/Go/Rust/C++ lanes: seed is a string reproduction token, shrinkSteps is nullable, counterexample is a string, and the runner separates a graceful FALSIFIED from an unhandled ERROR. - validate-provider proves every installed lane's canary is live (SKIP when a runtime is absent, never a silent pass); per-lane canaries; --lane flag; README "Lanes" section; a worked Python example; tests (39 pass).
1 parent cab3d96 commit fd36055

22 files changed

Lines changed: 2032 additions & 79 deletions

.github/workflows/ci.yml

Lines changed: 22 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -8,12 +8,28 @@ jobs:
88
gate:
99
runs-on: ubuntu-latest
1010
steps:
11-
- uses: actions/checkout@v4
11+
# Actions are pinned by commit SHA (not a mutable @vN tag) so an identical commit always runs
12+
# the same reviewed action code — the version tag is kept in a comment for readability.
13+
- uses: actions/checkout@34e114876b0b11c390a56381ad16ebd13914f8d5 # v4
1214

13-
- uses: actions/setup-node@v4
15+
- uses: actions/setup-node@49933ea5288caeca8642d1e84afbd3f7d6820020 # v4
1416
with:
1517
node-version: 24
1618

19+
# The Python / Hypothesis lane is a first-class gate, not an optional extra: install its
20+
# runtime so the tests actually EXERCISE it (instead of self-skipping) and validate:provider
21+
# can PROVE its canary. Without this, validate:provider is fail-closed and QUARANTINEs the
22+
# lane (exit 5) rather than reporting a false green — so provisioning is required, by design.
23+
- uses: actions/setup-python@a26af69be951a213d495a4c3e4e4022e16d87065 # v5
24+
with:
25+
python-version: "3.12"
26+
27+
- name: Install Python lane runtime (hash-locked)
28+
# --require-hashes over a fully pinned, hashed lockfile (hypothesis + every transitive dep):
29+
# identical commits install byte-identical third-party code, so the gate is reproducible and
30+
# nothing can change under us without a committed change to requirements-ci.txt.
31+
run: python -m pip install --require-hashes -r requirements-ci.txt
32+
1733
- name: Install dependencies
1834
run: npm ci || npm install
1935

@@ -23,5 +39,7 @@ jobs:
2339
- name: Test
2440
run: npm test
2541

26-
- name: Validate provider
27-
run: npm run validate:provider
42+
- name: Validate provider (all lanes — this repo dogfoods every lane)
43+
# --all-lanes: prove EVERY registered lane's canary here (fail closed if any is absent).
44+
# Downstream JS-only consumers run the bare command, which validates bundled lanes only.
45+
run: npm run validate:provider -- --all-lanes

.gitignore

Lines changed: 8 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -4,3 +4,11 @@ authored/
44
.DS_Store
55
/tmp
66
*.log
7+
8+
# Python lane runtime cruft
9+
__pycache__/
10+
*.pyc
11+
.eks-venv/
12+
13+
# pr-workflow gate ledger (local state)
14+
.pr-gates/

README.md

Lines changed: 59 additions & 7 deletions
Original file line numberDiff line numberDiff line change
@@ -6,10 +6,13 @@ discipline: a result only counts with evidence, and every degenerate state (no t
66
exercised, an engine that can't prove it's live, a vacuous run) is an explicit
77
non-passing verdict — never a silent green.
88

9-
einsiedlerkrebs runs [fast-check](https://github.com/dubzzz/fast-check) properties defined
10-
in `*.eks.mjs` modules against symbols you name. Each module exports a `properties(fc)`
11-
function returning `{ name, coversSymbol, property }` entries — see
12-
`examples/sample/clamp.eks.mjs` for the shape.
9+
einsiedlerkrebs runs property tests across languages through pluggable **lanes**, all behind
10+
one fail-closed verdict + exit-code contract (like [marmorkrebs](https://github.com/anagnorisis2peripeteia/marmorkrebs)
11+
normalizes many mutation tools). The JS/TS lane uses
12+
[fast-check](https://github.com/dubzzz/fast-check) (`*.eks.mjs` modules exporting
13+
`properties(fc)``{ name, coversSymbol, property }` — see `examples/sample/clamp.eks.mjs`);
14+
the Python lane uses [Hypothesis](https://hypothesis.readthedocs.io) (`*.eks.py`). See
15+
"Lanes (languages)" below.
1316

1417
**Two ways to get invariants.** The base tool is **targeted**: it tests the invariants
1518
someone wrote as `*.eks.mjs` modules — no authored properties, no coverage. Use it
@@ -53,6 +56,51 @@ einsiedlerkrebs --repo /path/to/repo --modules src/props \
5356
| `--allow-empty` | Treat zero exercised targets as an explicit pass (`PASS_EMPTY`) instead of `NO_PROPERTY` |
5457
| `--report-file <path>` | Persist the full JSON report (written before exit, survives a failing gate) |
5558

59+
## Lanes (languages)
60+
61+
Each lane is a per-language adapter behind the shared `core/report.mjs` verdict + exit codes.
62+
The lane is auto-detected from the module extension, or forced with `--lane <id>`:
63+
64+
| Language | `--lane` | Modules | Library | Runtime |
65+
|---|---|---|---|---|
66+
| JS/TS | `fast-check` | `*.eks.mjs` | fast-check (bundled) | Node, in-process |
67+
| Python | `hypothesis` | `*.eks.py` | Hypothesis (`pip install hypothesis`) | `python3` subprocess |
68+
69+
```bash
70+
einsiedlerkrebs --validate --lane hypothesis # prove the Python lane is live
71+
einsiedlerkrebs --modules src/props --lane hypothesis # (or auto-detected from *.eks.py)
72+
```
73+
74+
A Python module exposes `properties()` returning dicts with `given` (a Hypothesis strategy or
75+
a list of them) and `property` (returns a bool, fast-check style, **or** asserts):
76+
77+
```python
78+
from hypothesis import strategies as st
79+
80+
def properties():
81+
return [{
82+
"name": "result within [lo,hi]",
83+
"coversSymbol": "clamp",
84+
"given": [st.integers(), st.integers(), st.integers()],
85+
"property": lambda x, a, b: min(a, b) <= clamp(x, a, b) <= max(a, b),
86+
}]
87+
```
88+
89+
**Fail-closed per lane.** `--validate` proves the *selected* lane catches its own planted
90+
canary before that lane is trusted; a lane whose runtime/library is absent is `QUARANTINED`
91+
(exit 5) and reported `SKIP` by `validate:provider` — never a silent pass. Point `python3` at a
92+
venv with `EINSIEDLERKREBS_PYTHON=/path/to/venv/bin/python`.
93+
94+
**Adding a language.** Non-JS lanes run out of process: a thin runner (in that language)
95+
discovers its `*.eks.<lang>` modules, drives its property library, and prints a normalized
96+
`PropertyResult[]` as JSON on stdout — the generic `SubprocessLane` (`einsiedler/lanes/subprocess.mjs`)
97+
just spawns it and parses. Adding Swift (SwiftCheck), Go (gopter/`testing/quick`),
98+
Rust (proptest), or C++ (RapidCheck) is "write a runner + register a lane", no framework
99+
changes. The protocol generalizes the cross-library quirks: `seed` is a **string** reproduction
100+
token (int seed, Hypothesis `@reproduce_failure` blob, proptest byte-array, …), `shrinkSteps`
101+
is **nullable** (Hypothesis and Go `testing/quick` don't expose it), `counterexample` is a
102+
pre-formatted string, and the runner separates a graceful `FALSIFIED` from an unhandled `ERROR`.
103+
56104
## AI-authoring mode (`--author`)
57105

58106
Instead of hand-writing `*.eks.mjs` modules, let an LLM propose invariants for the files
@@ -171,11 +219,15 @@ Rules of thumb:
171219

172220
```
173221
core/ shared report shape + verdict logic (report.mjs), git diff helpers (diff.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);
222+
einsiedler/ cli.mjs (lane-agnostic), fast-check-lane.mjs, author-mode.mjs (--author pipeline)
223+
einsiedler/lanes/ lane registry + interface: index.mjs, lane.mjs, fast-check.mjs,
224+
subprocess.mjs (generic out-of-process adapter), hypothesis.mjs
225+
einsiedler/runners/ per-language runners that emit the JSON PropertyResult protocol
226+
(hypothesis_runner.py)
227+
fixtures/ validate-provider canaries per lane (canary.eks.mjs, canary.eks.py);
176228
author-demo/ — deterministic mock engine for the --author smoke test
177229
examples/sample/ a worked example (clamp.mjs + clamp.eks.mjs)
178-
scripts/ validate-provider.mjs — CI gate proving the canary is live
230+
scripts/ validate-provider.mjs — CI gate proving every installed lane's canary is live
179231
test/ node:test suite
180232
```
181233

core/report.mjs

Lines changed: 16 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -3,8 +3,22 @@
33
// degenerate state (no property, vacuous run, dead engine) is an explicit error,
44
// never a silent green.
55

6+
// Persisted report schema version. v2 is an INTENTIONAL BREAKING change from the implicit v1: the
7+
// per-result `seed` is now a STRING replay token (was a fast-check integer) and a `lane` field was
8+
// added. A `--report-file` consumer MUST branch on this — a v2 report's `seed` is a string, so an
9+
// old reader expecting a number has to be updated. (This is a pre-1.0 tool with no released v1
10+
// report consumers to migrate; the version field IS the migration signal — new readers detect v2
11+
// explicitly rather than silently mis-reading the changed type.)
12+
export const REPORT_SCHEMA_VERSION = 2;
13+
614
export function buildReport({ tool, engine, lane, repo, base, sha, results, engineValidated }) {
15+
// Enforce the schema-v2 contract centrally: every per-result `seed` is a STRING replay token (or
16+
// null). The lanes already stringify, but paths that feed results straight from the fast-check
17+
// engine (e.g. `--author` -> runFastCheckLane) still carry a numeric `details.seed`, so normalize
18+
// here — the report can never advertise v2 while leaking the old numeric type.
19+
const normalizedResults = (results ?? []).map((r) => ({ ...r, seed: r?.seed != null ? String(r.seed) : null }));
720
return {
21+
schemaVersion: REPORT_SCHEMA_VERSION,
822
tool,
923
engine,
1024
lane,
@@ -13,9 +27,9 @@ export function buildReport({ tool, engine, lane, repo, base, sha, results, engi
1327
sha: sha ?? null,
1428
evidence: {
1529
engineValidated: engineValidated ?? null, // did the validate-provider canary get caught?
16-
targetsExercised: results.length,
30+
targetsExercised: normalizedResults.length,
1731
},
18-
results,
32+
results: normalizedResults,
1933
};
2034
}
2135

einsiedler/cli.mjs

Lines changed: 81 additions & 20 deletions
Original file line numberDiff line numberDiff line change
@@ -10,7 +10,8 @@
1010
import { writeFileSync } from "node:fs";
1111
import { fileURLToPath } from "node:url";
1212
import { dirname, join } from "node:path";
13-
import { runFastCheckLane, resolveModules } from "./fast-check-lane.mjs";
13+
import { selectLane } from "./lanes/index.mjs";
14+
import { fastCheckSeed } from "./lanes/fast-check.mjs";
1415
import { buildReport, decideVerdict, summarize } from "../core/report.mjs";
1516
import { changedFiles, seedFromHead, repoHead } from "../core/diff.mjs";
1617
import { runAuthorMode, summarizeAuthor } from "./author-mode.mjs";
@@ -19,37 +20,79 @@ const HERE = dirname(fileURLToPath(import.meta.url));
1920

2021
function parseArgs(argv) {
2122
const a = { numRuns: 500, minRuns: 100 };
23+
const fail = (msg) => {
24+
console.error(`einsiedlerkrebs: ${msg}`);
25+
process.exit(64); // EX_USAGE
26+
};
2227
for (let i = 0; i < argv.length; i++) {
2328
const k = argv[i];
24-
const next = () => argv[++i];
25-
if (k === "--repo") a.repo = next();
26-
else if (k === "--modules") a.modules = next();
27-
else if (k === "--base") a.base = next();
28-
else if (k === "--seed") a.seed = parseInt(next(), 10);
29-
else if (k === "--num-runs") a.numRuns = parseInt(next(), 10);
30-
else if (k === "--min-runs") a.minRuns = parseInt(next(), 10);
29+
// Value getter for flags that take an argument. Fail closed on a MISSING value or one that
30+
// looks like the next flag (e.g. a dangling `--lane`, or `--lane --validate`): a swallowed
31+
// value must never silently fall back to a default and hand back a green that skipped it.
32+
// A leading-dash value that is a negative number (e.g. a seed "-5") is still allowed.
33+
const val = () => {
34+
const v = argv[i + 1];
35+
if (v == null || (v.length > 1 && v.startsWith("-") && !/^-\d/.test(v))) fail(`${k} requires a value`);
36+
i++;
37+
return v;
38+
};
39+
if (k === "--repo") a.repo = val();
40+
else if (k === "--modules") a.modules = val();
41+
else if (k === "--base") a.base = val();
42+
// Keep the seed as an OPAQUE string reproduction token — do NOT parseInt it here, which would
43+
// corrupt a non-numeric or numeric-prefixed token. Each lane interprets it (fast-check parses
44+
// an int, the hypothesis runner hashes the string), so it must reach them intact.
45+
else if (k === "--seed") a.seed = val();
46+
else if (k === "--num-runs") a.numRuns = parseInt(val(), 10);
47+
else if (k === "--min-runs") a.minRuns = parseInt(val(), 10);
3148
else if (k === "--allow-empty") a.allowEmpty = true;
32-
else if (k === "--report-file") a.reportFile = next();
49+
else if (k === "--report-file") a.reportFile = val();
3350
else if (k === "--validate") a.validate = true;
3451
else if (k === "--author") a.author = true;
35-
else if (k === "--engine") a.engine = next();
36-
else if (k === "--out-dir") a.outDir = next();
52+
else if (k === "--engine") a.engine = val();
53+
else if (k === "--out-dir") a.outDir = val();
54+
else if (k === "--lane") a.lane = val();
3755
else if (k === "--no-keep-authored") a.keepAuthored = false;
56+
// Strict: an unrecognized token (a typo like `--lan`) must fail loudly, never be ignored into
57+
// a default run that could exit 0 having skipped what the user asked for.
58+
else fail(`unrecognized argument '${k}'`);
3859
}
3960
return a;
4061
}
4162

4263
async function main() {
4364
const a = parseArgs(process.argv.slice(2));
4465

45-
// validate-provider: the lane MUST report the planted-false canary as FALSIFIED.
66+
// validate-provider: the selected lane MUST report its planted-false canary as FALSIFIED.
67+
// An absent runtime/lib is QUARANTINED (fail-closed) — never a silent pass.
4668
if (a.validate) {
47-
const canary = resolveModules(join(HERE, "..", "fixtures", "canary"));
48-
const results = await runFastCheckLane({ modules: canary, seed: 1, numRuns: 100, minRuns: 1 });
69+
let lane;
70+
try {
71+
// Honor auto-detection: `--validate --modules <python-dir>` should validate the lane those
72+
// modules belong to (e.g. hypothesis), not silently default to fast-check and certify the
73+
// wrong engine. Pass both the explicit --lane and --modules, like the normal run path.
74+
lane = selectLane({ lane: a.lane, modules: a.modules });
75+
} catch (e) {
76+
// An unknown --lane is a usage error here too (exit 64), same as the normal run path — not
77+
// the top-level fatal (70). Fail loudly rather than through a confusing generic crash.
78+
console.error(`einsiedlerkrebs: ${e.message}`);
79+
process.exit(64);
80+
}
81+
const probe = await lane.probe();
82+
if (!probe.available) {
83+
const report = buildReport({ tool: "einsiedlerkrebs", engine: lane.id, lane: lane.id, repo: "<canary>", results: [], engineValidated: false });
84+
const decision = { verdict: "QUARANTINED", code: 5 };
85+
console.log(summarize(report, decision));
86+
console.log(` (lane '${lane.id}' runtime unavailable: ${probe.detail ?? "?"})`);
87+
process.exit(decision.code);
88+
}
89+
const canary = lane.resolveModules(lane.canaryDir);
90+
const results = await lane.run({ modules: canary, seed: "1", numRuns: 100, minRuns: 1 });
4991
const caught = results.length > 0 && results.every((r) => r.status === "FALSIFIED");
50-
const report = buildReport({ tool: "einsiedlerkrebs", engine: "fast-check", lane: "fast-check", repo: "<canary>", results, engineValidated: caught });
92+
const report = buildReport({ tool: "einsiedlerkrebs", engine: lane.id, lane: lane.id, repo: "<canary>", results, engineValidated: caught });
5193
const decision = caught ? { verdict: "ENGINE_OK", code: 0 } : { verdict: "QUARANTINED", code: 5 };
5294
console.log(summarize(report, decision));
95+
console.log(` (lane=${lane.id} ${probe.detail ?? ""})`);
5396
process.exit(decision.code);
5497
}
5598

@@ -60,7 +103,17 @@ async function main() {
60103
console.error("einsiedlerkrebs --author: --repo <path> and --base <ref> are both required");
61104
process.exit(64);
62105
}
63-
const authorSeed = a.seed ?? seedFromHead(a.repo, 42);
106+
// Author mode generates fast-check `*.eks.mjs` invariants — it only supports the fast-check lane.
107+
// Reject `--author --lane <other>` loudly (EX_USAGE) rather than silently authoring for the wrong
108+
// engine and "succeeding" against a lane the user did not ask for.
109+
if (a.lane && a.lane !== "fast-check") {
110+
console.error(`einsiedlerkrebs --author: only the fast-check lane is supported (got --lane ${a.lane})`);
111+
process.exit(64);
112+
}
113+
// Author mode drives fast-check directly (runFastCheckLane), which wants an integer seed — so
114+
// convert the opaque token the same way the fast-check lane does, or a non-numeric --seed would
115+
// reach the engine unconverted and fail or replay differently.
116+
const authorSeed = fastCheckSeed(a.seed ?? seedFromHead(a.repo, 42));
64117
const authored = await runAuthorMode({
65118
repo: a.repo,
66119
base: a.base,
@@ -104,12 +157,20 @@ async function main() {
104157
let changed = null;
105158
if (a.repo && a.base) changed = changedFiles(a.repo, a.base);
106159

107-
const modules = resolveModules(a.modules);
108-
const results = await runFastCheckLane({ modules, seed, numRuns: a.numRuns, minRuns: a.minRuns });
160+
// Select the lane (explicit --lane, else auto-detect from the module extension).
161+
let lane;
162+
try {
163+
lane = selectLane({ lane: a.lane, modules: a.modules });
164+
} catch (e) {
165+
console.error(`einsiedlerkrebs: ${e.message}`);
166+
process.exit(64);
167+
}
168+
const modules = lane.resolveModules(a.modules);
169+
const results = await lane.run({ modules, seed: String(seed), numRuns: a.numRuns, minRuns: a.minRuns });
109170
const report = buildReport({
110171
tool: "einsiedlerkrebs",
111-
engine: "fast-check",
112-
lane: "fast-check",
172+
engine: lane.id,
173+
lane: lane.id,
113174
repo: a.repo ?? "(cwd)",
114175
base: a.base,
115176
sha,

einsiedler/fast-check-lane.mjs

Lines changed: 18 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -38,6 +38,24 @@ export async function runFastCheckLane({ modules, seed, numRuns, minRuns }) {
3838
continue;
3939
}
4040
const props = typeof mod.properties === "function" ? mod.properties(fc) : (mod.properties ?? []);
41+
if (!Array.isArray(props) || props.length === 0) {
42+
// A present .eks.mjs that exposes no usable properties tests NOTHING — a silent coverage gap
43+
// that another module's HELD would mask. Surface it as an explicit ERROR (fail closed), so a
44+
// property module that stops exercising anything cannot slip through green (lane parity with
45+
// the hypothesis runner).
46+
results.push({
47+
name: `<no properties in ${modPath}>`,
48+
targetSymbol: mod.target ?? modPath,
49+
engine: "fast-check",
50+
status: "ERROR",
51+
seed,
52+
numRuns: null,
53+
shrinkSteps: null,
54+
counterexample: null,
55+
error: "module defines no usable properties() (missing, empty, or not an array) — a present property module that exercises nothing is a coverage gap",
56+
});
57+
continue;
58+
}
4159
for (const p of props) {
4260
let details;
4361
try {

0 commit comments

Comments
 (0)