Skip to content

AGENTS.md

Latest commit

 

History

History
73 lines (54 loc) · 3.08 KB

AGENTS.md

File metadata and controls

73 lines (54 loc) · 3.08 KB

AGENTS.md — AI Agent Instructions for @stateproof/core

What This Is

A TypeScript-native formal specification testing framework. Define state machines in TypeScript → compile to TLA+ → run exhaustive model checking → generate Vitest tests.

Repository Structure

packages/
  core/          ← The main package (@stateproof/core)
    src/
      types.ts          All TypeScript types/interfaces
      machine.ts        Machine builder DSL (fluent API)
      concurrent.ts     Concurrent composition builder
      compiler.ts       JS function → TLA+ expression compiler
      tla-generator.ts  AST → TLA+ spec generation
      tlc.ts            TLC integration (verify function)
      test-generator.ts Trace-driven test generation
      runtime.ts        Runtime state machine + code generation
      mermaid.ts        Mermaid diagram generation
      diff.ts           Spec diffing
      vitest-plugin.ts  Vitest plugin
      cli.ts            CLI entry point
      index.ts          Public API (re-exports everything)
      index.test.ts     Comprehensive test suite (74 tests)
  client/        ← Template client (ignore)
  server/        ← Template server (ignore)

Key Commands

pnpm --filter @stateproof/core test    # Run tests
pnpm --filter @stateproof/core check   # TypeScript type check
pnpm --filter @stateproof/core build   # Build with rollup

Architecture

  1. DSL Layer (machine.ts, concurrent.ts): Fluent builders that collect state machine definitions into an AST (MachineAST / ConcurrentAST).

  2. Compiler Layer (compiler.ts): Parses constrained JavaScript function sources (guards, actions, invariants) into a simple expression AST, then translates to TLA+ expressions. Supports: comparisons, logic, arithmetic, array ops, Math.floor.

  3. Generator Layer (tla-generator.ts): Takes a MachineAST and produces a complete TLA+ module (.tla) and configuration (.cfg). Handles single machines and concurrent compositions.

  4. Verification Layer (tlc.ts): Writes TLA+ files to temp dir, shells out to TLC (Java), parses output into structured VerifyResult with violations and traces.

  5. Test Generation (test-generator.ts): BFS simulation to generate traces covering all transitions. Also extracts violation traces from TLC counterexamples.

  6. Runtime (runtime.ts): Creates executable state machines from specs. Also generates standalone TypeScript source code.

Constrained JS Subset (for guards/actions)

The compiler handles a strict subset of JavaScript:

  • Property access: ctx.x, ctx.arr.length
  • Comparisons: ===, !==, <, <=, >, >=
  • Logic: &&, ||, !
  • Arithmetic: +, -, *, %, Math.floor(x/y)
  • Array: .push(), .shift(), .length, .includes()
  • Assignments: ctx.x = expr, ctx.x += n
  • Literals, ternary, null

No closures, no async, no arbitrary function calls.

Adding New Features

  1. Add types to types.ts
  2. Implement in the appropriate module
  3. Export from index.ts
  4. Add tests to index.test.ts
  5. Run pnpm --filter @stateproof/core test && pnpm --filter @stateproof/core check