Skip to content

Add causal runtime verification laws - #88

Merged
SandroMaglione merged 1 commit into
mainfrom
codex/runtime-invariant-verification
Aug 10, 2026
Merged

Add causal runtime verification laws#88
SandroMaglione merged 1 commit into
mainfrom
codex/runtime-invariant-verification

Conversation

@SandroMaglione

Copy link
Copy Markdown
Member

Summary

  • add reusable snapshot, command, and transcript runtime invariants with filtering, observation requirements, aggregate reports, and exact violation locations
  • add verifyCausalCommands for law-oriented causal tests without a dummy reference model, plus explicit planner/runtime agreement assertions
  • retain stable public microstep snapshots for acknowledged probe sends while keeping cloning out of ordinary production sends
  • document the new testing workflow and add runtime, property-based, regression, and type-inference coverage

Changeset

  • Added or updated for a library or package-metadata change
  • Not required because this PR does not change src/ or package.json

Validation

  • pnpm check
  • Relevant example checks, when examples changed (no examples changed)
  • Reviewed the automated type-performance report, when the public TypeScript API or inference changed
  • Reviewed the automated runtime-performance report, when runtime behavior changed

Local validation also included pnpm perf:types and two successful pnpm perf:runtime runs. The automated base-versus-PR performance reports will be reviewed before merge.

@SandroMaglione
SandroMaglione marked this pull request as ready for review August 10, 2026 17:24
@github-actions

Copy link
Copy Markdown
Contributor

Type performance

Measured with TypeScript 6.0.3 and skipLibCheck=true.

Scenario Base PR Difference
Effect only 55 55 0 (0.0%)
Import effect-machine 55 55 0 (0.0%)
Machine.defineStates (3 states) 2,965 2,965 0 (0.0%)
Machine.make (3 states, 2 events) 8,715 8,715 0 (0.0%)
machine.handle (3 states, 2 transitions) 23,492 23,492 0 (0.0%)
machine.handle (depth 8) 117,075 117,075 0 (0.0%)
machine.handle (depth 12) 129,713 129,713 0 (0.0%)
machine.handle (depth 16) 145,055 145,055 0 (0.0%)
machine.handle (depth 24) 183,851 183,851 0 (0.0%)
machine.handle (wide depth 16) 214,189 214,189 0 (0.0%)
machine.handle (parallel/history/choice) 132,667 132,667 0 (0.0%)
machine.handle (4 successive calls) 128,674 128,674 0 (0.0%)
machine exact input/output/error/services 110,584 110,584 0 (0.0%)
execution adapter readiness 127,854 127,854 0 (0.0%)

Marginal instantiations are measured against the matching setup without that API call:

Scenario Base PR Difference
Import effect-machine 0 0 0
Machine.defineStates (3 states) 2,910 2,910 0 (0.0%)
Machine.make (3 states, 2 events) 5,742 5,742 0 (0.0%)
machine.handle (3 states, 2 transitions) 14,777 14,777 0 (0.0%)
machine.handle (depth 8) 109,601 109,601 0 (0.0%)
machine.handle (depth 12) 121,039 121,039 0 (0.0%)
machine.handle (depth 16) 135,181 135,181 0 (0.0%)
machine.handle (depth 24) 171,577 171,577 0 (0.0%)
machine.handle (wide depth 16) 202,224 202,224 0 (0.0%)
machine.handle (parallel/history/choice) 114,331 114,331 0 (0.0%)
machine.handle (4 successive calls) 113,703 113,703 0 (0.0%)
machine exact input/output/error/services 100,670 100,670 0 (0.0%)
execution adapter readiness 102,092 102,092 0 (0.0%)
Check times (informational)
Scenario Base PR
Effect only 0.02s 0.02s
Import effect-machine 0.02s 0.02s
Machine.defineStates (3 states) 0.07s 0.07s
Machine.make (3 states, 2 events) 0.10s 0.11s
machine.handle (3 states, 2 transitions) 0.18s 0.15s
machine.handle (depth 8) 0.38s 0.33s
machine.handle (depth 12) 0.37s 0.37s
machine.handle (depth 16) 0.39s 0.38s
machine.handle (depth 24) 0.43s 0.43s
machine.handle (wide depth 16) 0.49s 0.49s
machine.handle (parallel/history/choice) 0.40s 0.41s
machine.handle (4 successive calls) 0.38s 0.38s
machine exact input/output/error/services 0.34s 0.36s
execution adapter readiness 0.38s 0.40s

Type instantiations are the comparison metric. Check time varies with runner load and is informational only.

@github-actions

Copy link
Copy Markdown
Contributor

Runtime performance

Median of 5 independent benchmark processes on AMD EPYC 7763 64-Core Processor with Node v24.18.0.

Pull request baseline

Scenario Effect Machine XState 5 XState 6 alpha
Plan counter transitions 123,093 transitions/s 135,046 transitions/s 13,210 transitions/s
Drain burst with terminal fence 484,429 increments/s 388,908 increments/s 192,950 increments/s
Drain burst with a change observer 455,881 increments/s 385,859 increments/s 193,269 increments/s
Lookup and send to one child 390,296 increments/s 383,089 increments/s 185,462 increments/s
Start and stop a machine 168,606 machines/s 187,266 machines/s 144,446 machines/s
Start and stop a parent with one child 35,635 families/s 69,027 families/s 40,558 families/s
Plan transitions through a compound state 118,276 transitions/s
Plan transitions through parallel regions 91,237 transitions/s
Drain burst through a compound state 494,808 events/s 343,542 events/s 188,141 events/s
Drain burst through two parallel regions 461,266 events/s 260,927 events/s 143,118 events/s
Drain a compound-state burst with a change observer 452,524 events/s

Effect runtime reference points

Scenario Effect Machine Effect runtime primitives
Start and stop a raw generic process 16,512 processes/s
Start and stop a raw compiled process 66,234 processes/s
Start and interrupt a suspended fiber 163,908 fibers/s
Start and stop a queue worker 116,198 workers/s
Start and stop an actor shell 106,417 actors/s
Start and stop two actor shells 62,937 families/s
Update an owner-only mutable snapshot 316,856,781 updates/s
Update a synchronized snapshot 1,523,415 updates/s
Create, resolve, and await a terminal latch 1,412,635 latches/s
Memory profile Effect Machine XState 5 XState 6 alpha Effect runtime primitives
Idle machine 1.5 KiB 3.8 KiB 2.2 KiB
Raw generic managed process 12.7 KiB
Raw compiled process 2.8 KiB
Two independent idle machines 3.0 KiB 7.3 KiB 3.9 KiB
Idle parent with one child 4.8 KiB 5.5 KiB 4.0 KiB
Parent with observed child registry 9.0 KiB
Parent with observed invoked child snapshots 5.0 KiB
Suspended Effect fiber 0.6 KiB
Effect queue with waiting fiber 2.8 KiB
Effect mailbox actor shell 3.2 KiB
Two Effect actor shells 6.8 KiB

Effect Machine change from base

Metric Base Base variability PR PR variability Difference
Plan counter transitions 124,150 transitions/s 2.1% MAD 123,093 transitions/s 0.6% MAD -0.9%
Drain burst with terminal fence 495,957 increments/s 2.4% MAD 484,429 increments/s 2.9% MAD -2.3%
Drain burst with a change observer 455,748 increments/s 2.2% MAD 455,881 increments/s 3.5% MAD +0.0%
Lookup and send to one child 388,579 increments/s 1.6% MAD 390,296 increments/s 3.4% MAD +0.4%
Start and stop a machine 168,322 machines/s 2.0% MAD 168,606 machines/s 1.3% MAD +0.2%
Start and stop a parent with one child 33,563 families/s 2.0% MAD 35,635 families/s 6.6% MAD +6.2%
Plan transitions through a compound state 118,772 transitions/s 2.3% MAD 118,276 transitions/s 0.7% MAD -0.4%
Plan transitions through parallel regions 90,027 transitions/s 2.4% MAD 91,237 transitions/s 0.8% MAD +1.3%
Drain burst through a compound state 503,480 events/s 1.9% MAD 494,808 events/s 1.3% MAD -1.7%
Drain burst through two parallel regions 462,934 events/s 0.3% MAD 461,266 events/s 1.0% MAD -0.4%
Drain a compound-state burst with a change observer 462,848 events/s 1.6% MAD 452,524 events/s 1.8% MAD -2.2%
Idle machine heap per unit 1.5 KiB 0.2% MAD 1.5 KiB 0.1% MAD +0.3%
Raw generic managed process heap per unit 12.7 KiB 0.0% MAD 12.7 KiB 0.0% MAD -0.0%
Raw compiled process heap per unit 2.8 KiB 0.5% MAD 2.8 KiB 0.1% MAD -0.1%
Two independent idle machines heap per unit 3.0 KiB 0.0% MAD 3.0 KiB 0.0% MAD +0.1%
Idle parent with one child heap per unit 4.8 KiB 0.0% MAD 4.8 KiB 0.0% MAD +0.0%
Parent with observed child registry heap per unit 9.0 KiB 0.0% MAD 9.0 KiB 0.0% MAD -0.2%
Parent with observed invoked child snapshots heap per unit 5.0 KiB 0.1% MAD 5.0 KiB 0.1% MAD +0.0%

Effect runtime reference change from base

Metric Base Base variability PR PR variability Difference
Start and stop a raw generic process 16,275 processes/s 2.7% MAD 16,512 processes/s 0.6% MAD +1.5%
Start and stop a raw compiled process 66,765 processes/s 1.2% MAD 66,234 processes/s 0.5% MAD -0.8%
Start and interrupt a suspended fiber 165,810 fibers/s 1.2% MAD 163,908 fibers/s 1.2% MAD -1.1%
Start and stop a queue worker 115,929 workers/s 1.9% MAD 116,198 workers/s 0.2% MAD +0.2%
Start and stop an actor shell 107,910 actors/s 1.2% MAD 106,417 actors/s 0.3% MAD -1.4%
Start and stop two actor shells 66,278 families/s 2.3% MAD 62,937 families/s 3.9% MAD -5.0%
Update an owner-only mutable snapshot 316,856,781 updates/s 0.0% MAD 316,856,781 updates/s 0.0% MAD 0.0%
Update a synchronized snapshot 1,542,222 updates/s 1.4% MAD 1,523,415 updates/s 1.3% MAD -1.2%
Create, resolve, and await a terminal latch 1,426,218 latches/s 4.8% MAD 1,412,635 latches/s 3.3% MAD -1.0%
Versions and interpretation
  • Effect Machine: 0.4.0
  • XState 5: 5.32.5
  • XState 6 alpha: 6.0.0-alpha.31
  • Effect runtime primitives: 4.0.0-beta.107

Higher throughput is better; lower heap is better. Variability is the median absolute deviation across independent processes, relative to their median. Runtime measurements on shared GitHub-hosted hardware remain informational, so small differences should be confirmed across multiple workflow runs.

@SandroMaglione
SandroMaglione merged commit f3e1e78 into main Aug 10, 2026
9 checks passed
@SandroMaglione
SandroMaglione deleted the codex/runtime-invariant-verification branch August 10, 2026 17:35
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

None yet

Projects

None yet

Development

Successfully merging this pull request may close these issues.

1 participant