/** * Property-harness (design/57 §9 / design/58) — the **oracle-free** half of the trusted-oracle problem. * * From a **trusted contract** (supplied by the spec / leader — NEVER the worker, so it dodges BUG8: a worker * can't write `assert(true)` here) this derives executable **invariants** that hold for ANY correct * implementation, with **no expected values** (no oracle — dodging the "expected is LLM-computed" trap of a * generated test) and **no LLM** (pure deterministic — design/56's "execute > analyze"). Run against an * implementation over many generated inputs, they catch the **structural-contract** bug class deterministically * at **0 false positives** (probe-13: structural 16/16 caught, FP 0/12). * * It is a thin **complement** to the mechanical exit gate ({@link runExecGate}), not a replacement: it provably * **cannot** catch value-semantic bugs — wrong output that is still structurally valid (`abs → square`, * titlecase `don't → Don'T`). Those still need a real test suite (MECH) or the L3 judge. The value is the * **sound invariant library + the contract→invariant derivation** centralized here (a profile re-deriving it * risks unsound invariants = false positives = the thing that makes a gate harmful). * * Honest limits (two independent probes converged — core probe-13 + search [52], both FP=0): * - **The only false-positive risk is an UNFAITHFUL contract.** Each invariant is sound by construction, so a * *correct* impl can't violate one — UNLESS the contract misdescribes the intended behavior (declaring a * property the correct impl doesn't have). The contract must faithfully describe intent (it is trusted input). * - **Order/positional blindness.** `permutation`/`subset`/multiset-based invariants are order-agnostic, so a * wrong-order-but-same-elements result (concat `b+a`, a mis-ordered flatten) passes. That is the value-semantic * class — catch it with a positional contract entry, a real test (MECH), or the judge. * - **No contract ⇒ no signal.** A function with no declared contract derives zero invariants (zero coverage); * the catch comes from the *contract* you declare, not from the type alone — this is not magic from signatures. * * Scope (design/58 §2): no type→input generation (caller supplies `genInput`), no multi-language rendering * (this is the JS/TS reference; other languages render their own from {@link FunctionContract}), no * non-termination detection (a sync infinite loop blocks {@link checkInvariants} — gate it with the * env/exec timeout via `runExecGate`; `totalNoThrow` only catches throws). */ /** Sound, oracle-free invariant kinds (design/58 §1.3). Each holds for ANY correct implementation. */ export type InvariantKind = "permutation" | "lengthPreserving" | "subset" | "distinctOutput" | "idempotent" | "involution" | "outputPredicate" | "rangeBound" | "nonNegative" | "nonEmptyPreserving" | "concatPreserving" | "chunkMaxLen" | "lengthEq" | "roundtrip" | "totalNoThrow"; /** * The TRUSTED contract a function is expected to satisfy — from the spec / leader, **never the worker** (BUG8). * The predicate/bound fields carry trusted JS supplied by the spec author (not worker output), so the * in-process model is safe for them. */ export interface FunctionContract { /** Output is a permutation (same multiset) of the input collection — sort / shuffle / reverse / rotate. */ permutation?: boolean; /** `|output| === |input collection|`. */ lengthPreserving?: boolean; /** Output is a sub-multiset of the input collection — filter / take. */ subset?: boolean; /** Output has no duplicate elements — dedupe / unique. */ distinctOutput?: boolean; /** `f(f(x))` deep-equals `f(x)` — normalize / sort / dedupe. (Output type must equal input type.) */ idempotent?: boolean; /** `f(f(x))` deep-equals `x` — reverse / negate. (Output type must equal input type.) */ involution?: boolean; /** Numeric output is `>= 0` — abs / length / count. */ nonNegative?: boolean; /** A non-empty input collection implies a non-empty output — titlecase / dedupe. */ nonEmptyPreserving?: boolean; /** Concatenating the output groups in order deep-equals the input collection — chunk / split. */ concatPreserving?: boolean; /** The function is an `{ encode, decode }` pair and `decode(encode(x))` deep-equals `x` — serde / base62. */ roundtrip?: boolean; /** The function must not throw on any valid-typed input. (Non-termination is NOT covered — see file header.) */ totalNoThrow?: boolean; /** Every output element satisfies this trusted predicate — filter-by-P. */ outputPredicate?: (el: any) => boolean; /** Numeric output lies within `[lo, hi]` computed from the input by this trusted fn — clamp. */ rangeBound?: (input: any) => readonly [number, number]; /** Every output group has length in `(0, n]` where `n` is this trusted fn of the input — chunk. */ chunkMaxLen?: (input: any) => number; /** `|output| === ` this trusted fn of the input — e.g. `countdown(n)` has length `n + 1`. */ lengthEq?: (input: any) => number; /** * Extract the input collection when the input WRAPS it — e.g. `(x) => x.a` for `{ a, k }`. Default: the input * IS the collection. 🔴 Required for the collection invariants when the input is a wrapper object, else they * compare the output against the wrapper instead of the collection (probe-13 soundness fix). */ inputCollection?: (input: any) => unknown[]; } /** One derived, runnable invariant. `check(fn, input)` returns `true` iff the invariant HOLDS. */ export interface Invariant { kind: InvariantKind; /** Human-readable description (surfaced in a violation). */ description: string; /** For `roundtrip`, `fn` is the `{ encode, decode }` pair; otherwise a unary function. A throw propagates to the runner. */ check: (fn: any, input: any) => boolean; } /** A concrete invariant violation found by {@link checkInvariants}. */ export interface InvariantViolation { kind: InvariantKind; description: string; /** The input that triggered it (the first one observed). */ input: unknown; /** A-5 fold: the violation was detected via the check THROWING on a structurally wrong return value * (e.g. `.length` of undefined) rather than returning false — the impl's output doesn't even have * the shape the contract implies. fn itself did NOT throw (that is `totalNoThrow`'s domain). */ evaluationThrew?: true; } /** The outcome of running invariants over generated inputs. */ export interface CheckResult { /** True iff no invariant was violated across all trials. */ ok: boolean; /** One entry per violated invariant (first triggering input). */ violations: InvariantViolation[]; /** How many inputs were tried. */ trials: number; } /** * Derive the sound, oracle-free invariants implied by a trusted {@link FunctionContract}. Pure and * deterministic. The collection invariants honor `contract.inputCollection` (default: the input is the * collection) so a wrapper-object input (`{ a, k }`) is handled correctly. */ export declare function deriveInvariants(contract: FunctionContract): Invariant[]; /** * Run derived `invariants` against `fn` over `opts.trials` generated inputs (default 200). Returns the * violated invariants (first triggering input each). * * 🔴 Runs `fn` **in the caller's process** (design/58 §1.2). Pass only a TRUSTED `fn`, or invoke this INSIDE * the worker's sandbox (a generated test the leader drops into the env and runs via `runExecGate`, gating on * exit code). **Non-termination is NOT caught here** — a sync infinite loop blocks the call; bound it with the * env/exec timeout. An impl throw is detected by the self-contained `totalNoThrow` invariant (recorded ONLY * when totality was contracted — soundness over recall); the runner's `catch` is just a safety net so one * pathological input can't crash the whole run. Note: `fn` is invoked once per invariant per trial (twice for * `idempotent`/`involution`) — pass a PURE function (the intended use); a side-effecting `fn` is amplified. */ export declare function checkInvariants(fn: unknown, genInput: (i: number) => unknown, invariants: Invariant[], opts?: { trials?: number; }): CheckResult; //# sourceMappingURL=property-harness.d.ts.map