Eutaxy

eutaxy ​

import { … } from "eutaxy"; 18 functions and values, 53 types; each links to the file that declares it.

Functions, classes and values ​

aggregate ​

function aggregate(module: string, verdicts: readonly SpecVerdict[], reports: readonly EngineReport[]): SpecVerdict[]

The simulator's verdicts for a module (CHECKED, TESTED, REFUTED, UNKNOWN, total included) combined with what the engines proved. Source

checkedRung ​

function checkedRung(input: CheckedInput): SpecVerdict

The CHECKED rung: evaluate the property on every distinct input the simulator passed the function. Source

checkInvariant ​

function checkInvariant(log: EffectLog, inv: Invariant): Violation | null

Check one invariant against a run's effect log; null when it holds. Source

checkInvariants ​

function checkInvariants(log: EffectLog, invariants: readonly Invariant[]): readonly Violation[]

Check every invariant against a run's effect log and return the violations, in the invariants' order. Source

describeSpecVerdict ​

function describeSpecVerdict(v: SpecVerdict): string

One line per spec verdict, for error messages; full rendering lives in report. Source

describeVerdict ​

function describeVerdict(v: ScenarioVerdict): string

One line per verdict, for error messages; full rendering lives in report. Source

emitRegressionTest ​

function emitRegressionTest(verdict: Violated, options: RegressionTestOptions): string

A Vitest test file that replays a violation's shrunk schedule: by default it fails while the bug is there and passes once it is fixed. Source

explore ​

function explore(scenario: ScenarioSpec, platform: Platform, options: ExploreOptions): Promise<ScenarioVerdict>

Explore a scenario on a platform: run it under schedules drawn from the seed (or every schedule within the bounds, when exhaustive), shrink the first violation found, and return the verdict. Source

observeCore ​

function observeCore(namespace: object, functions: readonly string[]): CoreObserver

Observe the named exports of a module's namespace while runs are installed; see the module comment. Source

renderJson ​

function renderJson(verdict: ScenarioVerdict, specs: readonly SpecVerdict[] = []): string

The JSON report: one object, canonical, with a schema version at the top. Source

renderSpecs ​

function renderSpecs(specs: readonly SpecVerdict[]): string

Spec verdicts as text: one line each, a counterexample under a refutation. Source

renderText ​

function renderText(verdict: ScenarioVerdict): string

A readable report: verdict, what it rests on, and for a violation the schedule and trace. Source

renderTrace ​

function renderTrace(log: EffectLog, evidence: readonly number[] = []): string

The trace as a fixed-width table; evidence rows are marked with *. Source

replay ​

function replay(spec: ScenarioSpec, platform: Platform, schedule: Schedule): Promise<EffectLog>

Re-run a recorded schedule exactly. Source

restrictSpec ​

function restrictSpec(platform: Platform, spec: ScenarioSpec, keepIds: readonly string[]): ScenarioSpec

The scenario restricted to the kept events, with per-message invariants re-derived. Source

specLadder ​

function specLadder(input: CheckedInput, options: LadderOptions = {}): SpecVerdict

One property through the ladder's rungs. Source

testedRung ​

function testedRung(input: TestedInput): SpecVerdict

The TESTED rung: evaluate the property on inputs generated from its binders' domains, drawn from the seed. Source

validateScenario ​

function validateScenario(spec: ScenarioSpec): readonly string[]

Every reason a spec is not usable; empty when it is. Source

Types ​

Arrow ​

interface Arrow

An arrow function from the spec file, as written. Source

AtLeastOnce ​

interface AtLeastOnce

Every expected key appears in at least one selected effect. Source

AtMostOncePerKey ​

interface AtMostOncePerKey

No two selected effects share the same key. Source

Binder ​

interface Binder

A quantified variable: a parameter, under the name the claim gives it. Source

Bounded ​

interface Bounded

No violation within the stated bounds; not a proof. Source

Bounds ​

interface Bounds

Exploration bounds. Source

BoundsReached ​

interface BoundsReached

How far exploration got: runs, effect points, faults injected and time taken, and coverage when exhaustive. Source

Checked ​

interface Checked

The property held on every distinct input the simulator passed the function during the scenario's runs. Source

Conflict ​

interface Conflict

Two engines disagree: one proves, one refutes. Source

CoreObserver ​

interface CoreObserver

The calls an observeCore has recorded, the functions it could not observe, and how to undo it. Source

Counterexample ​

interface Counterexample

One assignment that breaks the property, as JavaScript literals, and where it came from. Source

EffectLog ​

interface EffectLog

The ordered record of what a run did at its effect boundaries, which invariants are checked against. Source

EffectRecord ​

interface EffectRecord

One entry of the effect log: an effect's call, its result, an injected fault, or an end-of-run snapshot. Source

EffectSelector ​

interface EffectSelector

Picks effect records by target, op, kind and payload fields. Source

EngineId ​

interface EngineId

A proof engine's name and version, as verdicts record it. Source

EngineReport ​

interface EngineReport

What an engine said about one module, by its name. Source

EventRef ​

interface EventRef

One deliverable event, e.g. Source

EveryRow ​

interface EveryRow

Every row the query returns satisfies all of holds. Source

ExploreOptions ​

interface ExploreOptions

How explore searches: the seed, a cap on runs, the time budget, the share of runs with faults, and exhaustive mode. Source

FaultDecision ​

interface FaultDecision

One injected fault: which effect of which invocation it hit, and what kind of fault it was. Source

FaultKind ​

type FaultKind

cut_off is a crash that happens after a response or acknowledgement was already sent, so only background work (ctx.waitUntil) is lost; platforms offer it at the point where that work would start. Source

FunctionSpec ​

interface FunctionSpec

The specs on one exported function. Source

Hint ​

interface Hint

What the precondition says about one binder on its own, read from its conjuncts: Number.isInteger(n), 0 <= n, n < 5, /^a+$/.test(s). Source

Implies ​

interface Implies

For every selected effect, a row exists whose column equals the effect's key. Source

Invariant ​

type Invariant

Anything a scenario says must hold after every run, over the effect log or the end-of-run state. Source

LadderOptions ​

interface LadderOptions

How far specLadder climbs: the TESTED rung's options (or none), and whether a scenario ran for CHECKED. Source

ModuleProofs ​

interface ModuleProofs

An engine's answer for one module: an outcome per property, the specs that did not read, and the open goals. Source

ModuleSpecs ​

interface ModuleSpecs

Every spec of one module, and what did not read. Source

ObservedCall ​

interface ObservedCall

One call of an observed core function from outside its module: the function, its arguments, whether it threw. Source

Platform ​

interface Platform

What a platform package gives the engine to run a scenario: its events, how each is delivered to the Worker or function, how state is reset before a run and snapshotted after it, and the assumptions a verdict rests on. Source

ProofOutcome ​

type ProofOutcome

What an engine said about one property: proven, refuted (with a counterexample when it has one), or unknown and why. Source

Property ​

interface Property

One exported spec: forall(f, { when, ensures }), a universally quantified claim over f's parameters where the precondition holds, or total(f), that f terminates on every input. Source

PropertyProof ​

interface PropertyProof

An engine's outcome for one property of one function. Source

ProveInput ​

interface ProveInput

What an engine is given: the module's source and specs, the functions to prove, and where they live. Source

Proven ​

interface Proven

Proved for every input by a named engine; the lower rungs' evidence is kept beside it. Source

Prover ​

interface Prover

A proof engine: whether it can run here, and proving a module's properties. Source

Refines ​

interface Refines

The shell follows the core. Source

Refuted ​

interface Refuted

A counterexample breaks the property, found by the simulator's inputs, generated ones, or an engine. Source

RegressionTestOptions ​

interface RegressionTestOptions

What the emitted test imports, the expressions for its platform and scenario, and what it expects. Source

RowCondition ​

type RowCondition

A condition on one column of a row. Source

ScenarioSpec ​

interface ScenarioSpec

A scenario as plain data: the Worker, the drive, the setup, the externals, the invariants and the bounds, which defineScenario (or a platform's equivalent) builds and validates. Source

ScenarioVerdict ​

type ScenarioVerdict

A scenario's verdict: VIOLATED, BOUNDED or UNSUPPORTED. Source

Schedule ​

interface Schedule

What decided one run: the seed it drew from, the faults injected, and the turns picked when they were picked. Source

SpecType ​

type SpecType

A TypeScript type as far as the reader can read it; unknown carries what it could not. Source

SpecUnknown ​

interface SpecUnknown

Nothing is known about the property: the engine gave up, the construct is not supported, or no engine was available. Source

SpecVerdict ​

type SpecVerdict

What is known about one property of one pure function, from the highest rung that reached it. Source

StateQuery ​

interface StateQuery

Rows of a table in the last snapshot of a target, optionally filtered. Source

Tested ​

interface Tested

The property held on inputs generated from its binders' domains, and on the simulator's where it passed any. Source

TestedOptions ​

interface TestedOptions

The TESTED rung's seed, and how many distinct generated inputs a property must hold on (default 100). Source

Unique ​

interface Unique

No two rows the query returns share the value at path, a dot path into the row (a column name for flat rows). Source

Unsupported ​

interface Unsupported

The run did something the simulation cannot control or replay, so no claim is made: the cause and the reason. Source

Violated ​

interface Violated

An invariant broke: the violation, the shrunk schedule that reproduces it and its trace. Source

Violation ​

interface Violation

An invariant that did not hold: its name, what went wrong, the keys involved and the effects that show it. Source