feat(lanes): multi-language property lanes; add a Python/Hypothesis lane

[anagnorisis2peripeteia]

What

Multi-language property lanes. The engine is now a pluggable per-language lane registry
behind the existing fail-closed core/report.mjs verdict + exit codes (marmorkrebs' multi-tool
discipline, applied to property testing). Adds a real Python / Hypothesis lane as the
proof of concept. core/report.mjs + decideVerdict are unchanged — they were already
language-agnostic.

Lanes

• fast-check (JS/TS, *.eks.mjs, in-process) — moved into a lane implementing the
  interface; no behaviour change (its canary + the 33 existing tests are unchanged).
• hypothesis (Python, *.eks.py, python3 subprocess) — a thin runner
  (einsiedler/runners/hypothesis_runner.py) discovers the modules, drives Hypothesis, and
  prints a normalized PropertyResult[] as JSON that a generic SubprocessLane parses.
  Canary-validated; HELD / FALSIFIED / VACUOUS / ERROR mapped correctly; shrunk counterexamples
  (the canary shrinks to canary(1)). A bool-returning property is wrapped so Hypothesis' "bare
  False is a pass" quirk can't hide a failure — and any falsey return (0, "", numpy.False_)
  fails, not just literal False; a None (assertion-style void) is the pass; an async def/generator property (whose body never runs) is an ERROR, never a HELD. Modules are
  registered in sys.modules before execution, so @dataclass and similar decorators work.

The lane is auto-detected from the module extension or forced with --lane <id>.

Fail-closed hardening (found by dogfooding ClawSweeper on this PR)

Reviewing this PR with the local ClawSweeper caught several false-green paths — the exact defect
class this tool exists to prevent — and all are closed here:

• validate-provider validates explicitly-selected lanes; never exits 0 on a selected-but-absent
  runtime. By default it checks only bundled lanes (fast-check), so a JS-only consumer is never
  forced to install Python — no upgrade break; --all-lanes / --lane <id> opt a non-bundled lane
  in. Any selected lane whose runtime is absent is QUARANTINED (exit 5), a distinct non-zero
  verdict — no waiver launders it green. (This repo's CI runs --all-lanes to prove every lane.)
  Argument parsing is strict (both the CLI and validate-provider): an unknown lane id, an
  unrecognized option (--all-lane), or a dangling --lane with no value all fail loudly (exit 64)
  — a typo can never silently narrow the run and exit 0 having skipped what you asked for. --validate --modules <dir> auto-detects the lane from the modules (so a Python dir validates the hypothesis canary, not fast-check).
  --author (fast-check-only) rejects a non-fast-check --lane (exit 64) rather than authoring for
  the wrong engine.
• validate-provider's lane list is derived from the single registry (einsiedler/lanes/ index.mjs), not duplicated — so a newly registered lane can't drift out of validation while
  the aggregate still reports PASS. "required" is the lane's own bundled flag.
• The Hypothesis runner reports the ACTUAL executed count and enforces a --min-runs VACUOUS
  floor. It used to report the requested max as numRuns and ignore --min-runs, so a
  heavily-filtered run that executed only a handful of real examples was trusted as HELD. Now a
  filtering-driven shortfall ⇒ VACUOUS (see the finite-domain refinement below).
• A present-but-empty property module is an explicit ERROR, not silently dropped (both
  lanes). A .eks.{mjs,py} that defines no properties tests nothing; without this, another
  module's HELD would mask the coverage gap.
• The subprocess trust boundary requires execution evidence for a pass. A runner reporting a
  bare HELD with no run count is downgraded to ERROR — a pass must carry a finite numRuns ≥ 1,
  so a buggy/dishonest runner can't forge an evidence-free green (the canary gate proves the runner
  is honest; this proves it actually ran).
  Each subprocess runs one module and must yield ≥ 1 result — an empty per-module result is an
  ERROR, so a broken module can't vanish and let a sibling's HELD carry the run to green.
• Runner robustness: the Python runner reserves stdout for the JSON protocol (a user module's
  print() goes to stderr, never corrupting the payload), and module paths are passed after --
  so a dash-leading filename can't be mis-parsed as a flag.
  The runner runs Python with -B and the syntax check compiles in memory, so importing property/
  target modules never writes __pycache__ into the target checkout — the gate leaves a clean tree.
• Bounded execution + output (liveness/memory): a hung runner or probe can't stall the gate
  forever — the subprocess is SIGKILLed after a timeout (120s default, EINSIEDLERKREBS_LANE_TIMEOUT_MS);
  and a runner that floods stdout/stderr is killed once its output passes a 16 MiB cap, so a noisy
  or runaway runner can't exhaust the parent's memory — bounded both per module (16 MiB) and across the whole invocation (64 MiB total). All fail closed to an ERROR.
• Contract & usability: an unexpected harness/generation exception (one raised outside a
  property invocation, with no recorded args) is an ERROR, never a mislabeled FALSIFIED; and
  a property module can import its sibling target source (from clamp import clamp) — the
  module's directory is placed on sys.path.
• Min-runs floor is sound about finite domains. A run short of --min-runs stays HELD only
  when Hypothesis' own statistics PROVE it exhausted the whole reachable input space
  (stopped-because = "nothing left to do") — every value the strategy can produce was tested, the
  strongest evidence there is. Any other shortfall (a heavy .filter()/assume() the engine gives
  up on, or simply hitting the example budget) is VACUOUS. This closes a false-green where a
  .filter()-limited run — whose rejections Hypothesis retries invisibly during generation, so a
  rejection count can't see them — looked like a complete finite sweep. The floor lives in the
  runner (which holds the authoritative stats); the subprocess adapter enforces only "a pass
  executed ≥ 1 example".
• Each property module runs in its OWN fresh interpreter. The adapter spawns one subprocess
  per .eks.py, so nothing an earlier module does can leak into a later one — not a same-named
  target, not a rogue sibling random.py, not an in-place monkeypatch of random/builtins or
  mutated Hypothesis state. In-process reset can only restore object identity (not undo mutations),
  so a fresh process per module is the only fail-closed isolation. A sibling that shadows a
  stdlib/runtime name fails closed, never silently validating the wrong target.
• The seed stays an opaque token, end to end. The CLI no longer parseInts --seed, and each
  lane derives its engine seed from the WHOLE token: the hypothesis runner hashes it, and the
  fast-check lane maps a pure integer to that exact seed but hashes any other token (so 12suffix
  ≠ 12 and distinct non-numeric tokens map to distinct streams with overwhelming probability — via a portable inline hash — no new Node version requirement — bounded, like fast-check itself, by its 2³² seed space). Deterministic, so a
  run replays. Author mode applies the same conversion before driving fast-check.
• The --report-file schema is versioned (schemaVersion: 2): the per-result seed became a
  string replay token (was a fast-check integer) and a lane field was added, so a consumer can
  switch on the version instead of breaking on the changed seed type. v2 is an intentional breaking change from the implicit v1 (numeric seed) — pre-1.0, with no released consumers to migrate; the version field is the signal. buildReport normalizes
  every seed to a string centrally, so even the --author path (which feeds fast-check results
  straight through) can't advertise v2 with a numeric seed.
• The check/lint script is portable — the optional Python py_compile step runs through a
  small Node helper (honoring EINSIEDLERKREBS_PYTHON), not a POSIX shell group, so npm run check
  works on Windows (cmd.exe) too, not just POSIX shells.
• CI is reproducible + proves the Python lane (.github/workflows/ci.yml): actions are pinned
  by commit SHA (not mutable @vN tags), the Python runtime installs from a hash-locked
  requirements-ci.txt (--require-hashes, hypothesis + every transitive dep), and it runs
  validate:provider --all-lanes — so identical commits execute byte-identical third-party code and
  this repo dogfoods every lane (fail closed if any is absent), while JS-only consumers keep the
  bundled-only default.

Future-proofed for the next lanes

The subprocess protocol is generalized up front so Swift (SwiftCheck), Go (gopter /
testing/quick), Rust (proptest) and C++ (RapidCheck) drop in as "write a runner + register a
lane", no framework change: seed is a string deterministic-replay token each lane feeds back
to its own engine (a fast-check int seed, a hashed Hypothesis run seed, a proptest byte-array, …)
so the same token reproduces the same run, shrinkSteps is nullable (Hypothesis and Go
testing/quick don't expose it), counterexample is a string, and the runner separates a graceful
FALSIFIED from an unhandled ERROR.

Evidence

• npm run check: JS node --check over the new lane files + Python py_compile — exit 0.
• npm test: 74 pass (33 original + lane/registry + fail-closed regression tests; the
  hypothesis-lane tests run when the runtime is present, else self-skip). New regressions cover
  the min-runs VACUOUS floor (num=5/min=100 ⇒ VACUOUS with the real executed count), the
  validate-provider fail-closed aggregate (any SKIP ⇒ exit 5; FAIL ⇒ 1) and its registry-drift
  guard, and a present-but-empty property module ⇒ explicit ERROR.
• npm run validate:provider (default) validates bundled lanes only → PASS even with no
  Python (no upgrade break); -- --all-lanes with the runtime present → both lanes PASS, and
  with it absent → QUARANTINED exit 5 (proven end-to-end), never a silent green.
• Runtime: kanarienkrebs strict layer — PASS, no new diagnostics.

Proof (real runs, hypothesis 6.156.6)

Before / after (same command, base cab3d96 vs HEAD). On base the Python lane does not exist:
--lane is ignored, the run falls back to lane=fast-check, resolves 0 modules, and fails
NO_PROPERTY (exit 3). On HEAD the same command selects lane=hypothesis and drives a real
Hypothesis run — both clamp properties HELD at 500 examples each, PASS (exit 0):

# BEFORE — base cab3d96 (deps installed; the FEATURE is what's absent)
$ einsiedlerkrebs --modules examples/sample-python --lane hypothesis
einsiedlerkrebs · lane=fast-check · repo=(cwd)
  base=(explicit-modules) sha=- engineValidated=null exercised=0
  => VERDICT NO_PROPERTY (exit 3)

# AFTER — HEAD
$ einsiedlerkrebs --modules examples/sample-python --lane hypothesis
einsiedlerkrebs · lane=hypothesis · repo=(cwd)
  ✓ HELD  [clamp] result within [lo,hi]      runs=500 seed=42
  ✓ HELD  [clamp] idempotent                 runs=500 seed=42
  => VERDICT PASS (exit 0)

Both lanes' canaries are live — validate:provider --all-lanes drives each lane's planted-false
canary and confirms it is CAUGHT (ENGINE_OK):

$ npm run validate:provider -- --all-lanes
validate-provider: einsiedlerkrebs lane canary gate
  validating: fast-check, hypothesis
====================================================
- fast-check: PASS (exit=0)
      ✗ FALSIFIED  [canary] CANARY: every positive integer is negative (must be falsified)
            runs=1 seed=1 shrinks=1  counterexample=[1]
      => VERDICT ENGINE_OK (exit 0)
- hypothesis: PASS (exit=0)
      ✗ FALSIFIED  [canary] CANARY: every positive integer is negative (must be falsified)
            runs=- seed=1  counterexample=canary(1)
      => VERDICT ENGINE_OK (exit 0)  (lane=hypothesis python + hypothesis 6.156.6)
====================================================
validate-provider: PASS (every selected lane's canary is live)

A real Python property HOLDS (the worked clamp example — 500 examples each), and the planted-false
canary is FALSIFIED with a shrunk counterexample and the fail-closed exit code 2:

$ einsiedlerkrebs --modules examples/sample-python --lane hypothesis
  ✓ HELD  [clamp] result within [lo,hi]      runs=500 seed=42
  ✓ HELD  [clamp] idempotent                 runs=500 seed=42
  => VERDICT PASS (exit 0)

$ einsiedlerkrebs --modules fixtures/canary --lane hypothesis
  ✗ FALSIFIED  [canary] CANARY: every positive integer is negative (must be falsified)
        runs=- seed=42  counterexample=canary(1)
  => VERDICT FALSIFIED (exit 2)

Review history

Review history (23 local ClawSweeper rounds): https://gist.github.com/f353c43ef23b0c6adf49e9c2e199a86f