Add Runtime Assertions chapter, fix npm test CI failure

- Add vitest + `npm test` script to package.json / vitest.config.js
- Add unit tests: worker-shim.test.js, lec-model.test.js
- New SVA chapter: Runtime Assertions
  - New lesson: Concurrent Assertions in Simulation (concurrent-sim)
  - Move vacuous-pass and $isunknown into Runtime Assertions
- Rename 'Your First Assertion' → 'Your First Formal Assertion'
  - immediate-assert stays bmc runner; gains simulation→formal bridge paragraph
- Move gear button next to split-view toggle in split editor header
- Update e2e/solutions.spec.js to match new chapter/lesson structure
- Add e2e test suite files (solutions, formal, lessons, waveform, etc.)
- Add playwright.config.js, scripts, and CI workflow

Co-Authored-By: Claude Sonnet 4.6 <noreply@anthropic.com>

Author: thomasahle

.env.example

@@ -6,6 +6,11 @@ VITE_CIRCT_SIM_JS_URL=/circt/circt-sim.js
 VITE_CIRCT_SIM_WASM_URL=/circt/circt-sim.wasm
 VITE_CIRCT_BMC_JS_URL=/circt/circt-bmc.js
 VITE_CIRCT_BMC_WASM_URL=/circt/circt-bmc.wasm
+# VPI-capable circt-sim (for cocotb lessons — built with Asyncify + VPI exports):
+VITE_CIRCT_SIM_VPI_JS_URL=/circt/circt-sim-vpi.js
+VITE_CIRCT_SIM_VPI_WASM_URL=/circt/circt-sim-vpi.wasm
+# Pyodide CDN URL (used by cocotb runner):
+# VITE_PYODIDE_URL=https://cdn.jsdelivr.net/pyodide/v0.27.0/full/pyodide.js
 #
 # Optional args for each stage (JSON array preferred):
 # VITE_CIRCT_VERILOG_ARGS=[\"--ir-llhd\",\"--timescale\",\"1ns/1ns\",\"--single-unit\"]

.gitignore

@@ -13,3 +13,5 @@ public/surfer/
 *.pdf
 .playwright-mcp/
 playwright-console.log
+playwright-report/
+test-results/

.nvmrc

@@ -0,0 +1 @@
+22

README.md

@@ -2,60 +2,110 @@
 
 Svelte-based interactive tutorial shell for SystemVerilog, SVA, and UVM.
 
-## CIRCT Fork
+## Reproducible Requirements
 
-This project is pinned to the CIRCT fork with wasm support:
+Pinned versions are centralized in `scripts/toolchain.lock.sh`:
 
-- `git@github.com:thomasnormal/circt.git`
+- Node major: `22`
+- Emscripten (emsdk): `4.0.21`
+- CIRCT repo: `https://github.com/thomasnormal/circt.git`
+- CIRCT ref: `8e8ca87dcda1c8abd47103ae7789c8ed261d5de3`
+- LLVM submodule ref: `972cd847efb20661ea7ee8982dd19730aa040c75`
+
+Host tools:
+
+- `git`
+- `node`/`npm` (Node 22.x)
+- `cmake` (>= 3.24)
+- `ninja` (>= 1.10)
+- `python3` (>= 3.10)
+- `rsync`
+- `unzip`
+
+Check prerequisites:
+
+- `npm run check:req` (frontend/tooling only)
+- `npm run check:req:wasm` (includes emsdk/emcc verification)
+
+## Reproducible Local Build
+
+1. Activate emsdk `4.0.21` (or ensure `emcc -v` reports `4.0.21`).
+2. Run the one-shot bootstrap:
+   - `npm run bootstrap:repro`
+
+Equivalent step-by-step:
+
+1. `npm ci`
+2. `scripts/setup-surfer.sh`
+3. `npm run setup:circt`
+4. `npm run build:circt`
+5. `npm run sync:circt`
+6. `npm run build`
+
+The CIRCT wasm build script enforces conservative resource limits by default:
+
+- Ninja parallelism: `CIRCT_WASM_JOBS=4`
+- Configure timeout: `CIRCT_WASM_CONFIGURE_TIMEOUT_MIN=30`
+- Build timeout: `CIRCT_WASM_BUILD_TIMEOUT_MIN=120`
+- Force clean build dir first: `CIRCT_WASM_CLEAN_BUILD=1`
+- Build targets override: `CIRCT_WASM_TARGETS="circt-verilog circt-sim circt-bmc"`
+- Optional virtual memory cap: `CIRCT_WASM_MEMORY_LIMIT_KB=<kb>`
+
+To also build `circt-sim-vpi` (required for cocotb lessons):
+
+```
+CIRCT_WASM_TARGETS="circt-verilog circt-sim circt-bmc circt-sim-vpi" npm run build:circt
+```
 
 ## Scripts
 
-- `npm install`
 - `npm run dev`
-- `npm run build`
 - `npm run preview`
-- `scripts/setup-circt.sh` (clone/update the CIRCT fork checkout)
-
-## CIRCT WASM Runtime Setup
-
-1. Clone/update the fork checkout:
-   - `scripts/setup-circt.sh`
-2. Build wasm artifacts from that checkout.
-3. Copy artifacts into this app:
-   - `cp vendor/circt/build-wasm/bin/circt-verilog.js public/circt/circt-verilog.js`
-   - `cp vendor/circt/build-wasm/bin/circt-verilog.wasm public/circt/circt-verilog.wasm`
-   - `cp vendor/circt/build-wasm/bin/circt-sim.js public/circt/circt-sim.js`
-   - `cp vendor/circt/build-wasm/bin/circt-sim.wasm public/circt/circt-sim.wasm`
-   - `cp vendor/circt/build-wasm/bin/circt-bmc.js public/circt/circt-bmc.js`
-   - `cp vendor/circt/build-wasm/bin/circt-bmc.wasm public/circt/circt-bmc.wasm`
-4. Runtime artifact lookup order:
-   - `public/circt/circt-verilog.js`
-   - `public/circt/circt-verilog.wasm`
-   - `public/circt/circt-sim.js`
-   - `public/circt/circt-sim.wasm`
-   - `public/circt/circt-bmc.js`
-   - `public/circt/circt-bmc.wasm`
-5. Optional mock shim (explicit opt-in only):
-   - `public/circt/circt.js`
-   - `public/circt/circt.wasm`
-   - not used by default runtime
-6. Optional URL overrides in `.env`:
-   - `VITE_CIRCT_VERILOG_JS_URL`
-   - `VITE_CIRCT_VERILOG_WASM_URL`
-   - `VITE_CIRCT_SIM_JS_URL`
-   - `VITE_CIRCT_SIM_WASM_URL`
-   - `VITE_CIRCT_BMC_JS_URL`
-   - `VITE_CIRCT_BMC_WASM_URL`
-   - `VITE_CIRCT_VERILOG_ARGS`
-   - `VITE_CIRCT_SIM_ARGS`
-   - `VITE_CIRCT_BMC_ARGS`
-
-## Notes
-
-- This repo currently includes a starter tutorial UI and lesson data model.
+- `npm run test:e2e`
+- `npm run setup:circt`
+- `npm run build:circt`
+- `npm run sync:circt`
+- `npm run bootstrap:repro`
+
+## Optional Runtime Overrides
+
+In `.env` (copy `.env.example`):
+
+- `VITE_CIRCT_VERILOG_JS_URL`
+- `VITE_CIRCT_VERILOG_WASM_URL`
+- `VITE_CIRCT_SIM_JS_URL`
+- `VITE_CIRCT_SIM_WASM_URL`
+- `VITE_CIRCT_BMC_JS_URL`
+- `VITE_CIRCT_BMC_WASM_URL`
+- `VITE_CIRCT_SIM_VPI_JS_URL` (cocotb lessons)
+- `VITE_CIRCT_SIM_VPI_WASM_URL` (cocotb lessons)
+- `VITE_PYODIDE_URL` (cocotb lessons, default: jsdelivr CDN)
+- `VITE_CIRCT_VERILOG_ARGS`
+- `VITE_CIRCT_SIM_ARGS`
+- `VITE_CIRCT_BMC_ARGS`
+
+## Runtime Notes
+
 - Runtime uses a real 2-stage wasm toolchain by default:
   - `circt-verilog` lowers SV/SVA/UVM source to MLIR
   - `circt-sim` executes lowered MLIR and emits VCD for the waveform pane
 - Tool invocations run in isolated Web Workers to avoid global Emscripten symbol collisions and re-entry issues.
-- The UI includes a `self-check` action in the Runtime panel to validate artifact compatibility.
-- Waveform pane is metadata-driven (`off`, `optional`, `required`) and prepared for Surfer integration.
+- UI includes a `self-check` action in the Runtime panel to validate artifact compatibility.
+- Waves tab appears automatically only when a valid VCD is generated.
+
+## CI
+
+- `.github/workflows/ci.yml` builds with pinned toolchain requirements:
+  1. install Node 22
+  2. install emsdk 4.0.21
+  3. run `scripts/setup-circt.sh` (pinned CIRCT ref)
+  4. run `scripts/build-circt-wasm.sh`
+  5. run `npm run sync:circt`
+  6. run `npm run build`
+
+## E2E
+
+- `npm run test:e2e -- e2e/waveform.spec.js`
+- Includes:
+  - non-mock pipeline check (`circt-verilog` + `circt-sim`, waveform generated)
+  - Surfer waveform render check when browser WebGL support is available in the test environment

docs/circt-uvm-browser-worker-repro.md

@@ -0,0 +1,44 @@
+# Browser-Worker UVM Repro (`Malformed attribute storage object`)
+
+This reproduces the CIRCT wasm UVM failure in the **browser worker** path
+without using lesson UI clicks.
+
+## Preconditions
+
+1. `vendor/circt` is checked out and wasm artifacts are built.
+2. Artifacts are synced into `public/circt`:
+
+```bash
+scripts/setup-circt.sh
+npm run sync:circt
+```
+
+## Repro command
+
+```bash
+node scripts/repro-uvm-browser-worker-assert.mjs
+```
+
+## What it does
+
+- starts Vite dev server on `http://127.0.0.1:4173` (`--strictPort`)
+- opens Chromium headless via Playwright
+- imports `createCirctWasmAdapter` from `/src/runtime/circt-adapter.js`
+- runs compile-only (`simulate: false`) on minimal UVM files:
+  - `/src/my_test.sv`
+  - `/src/tb_top.sv`
+- uses full UVM path (`--uvm-path /circt/uvm-core -I /circt/uvm-core/src`)
+
+## Expected failure signature
+
+- run result `ok=false`
+- logs include both:
+  - `Aborted(`
+  - `Malformed attribute storage object`
+- logs do **not** reach `$ circt-sim`
+
+If this signature appears, the script exits `0` and prints:
+
+`REPRODUCED: browser-worker UVM compile hit malformed-attribute abort`
+
+If not, it exits non-zero.

e2e/cocotb.spec.js

@@ -0,0 +1,43 @@
+/**
+ * E2E tests for the cocotb runner (circt-verilog → circt-sim + Pyodide).
+ */
+import { test, expect } from '@playwright/test';
+
+async function goToLesson(page, lessonName) {
+  await page.goto('/');
+  await page.getByRole('button', { name: 'cocotb Basics' }).click();
+  await page.getByRole('button', { name: new RegExp(lessonName) }).click();
+  await expect(page.getByRole('heading', { level: 2, name: lessonName })).toBeVisible();
+}
+
+test('cocotb: shows "test" button, not "run"', async ({ page }) => {
+  await goToLesson(page, 'Your First cocotb Test');
+  await expect(page.getByTestId('run-button')).toHaveText('test');
+});
+
+test('cocotb: Your First cocotb Test — solution passes all assertions', async ({ page }) => {
+  await goToLesson(page, 'Your First cocotb Test');
+
+  // The Python test file is the starter; apply the SV solution (correct adder).
+  await page.getByTestId('solve-button').click();
+  await page.getByTestId('run-button').click();
+
+  const logs = page.getByTestId('runtime-logs');
+  // Pyodide download can be slow on first run — generous timeout.
+  await expect(logs).toContainText('[cocotb] Simulation complete', { timeout: 180_000 });
+  await expect(logs).not.toContainText('[cocotb] Python error');
+  await expect(logs).not.toContainText('# cocotb error');
+  await expect(logs).not.toContainText('AssertionError');
+});
+
+test('cocotb: Clock and Timing — solution passes all assertions', async ({ page }) => {
+  await goToLesson(page, 'Clock and Timing');
+
+  await page.getByTestId('solve-button').click();
+  await page.getByTestId('run-button').click();
+
+  const logs = page.getByTestId('runtime-logs');
+  await expect(logs).toContainText('[cocotb] Simulation complete', { timeout: 180_000 });
+  await expect(logs).not.toContainText('[cocotb] Python error');
+  await expect(logs).not.toContainText('AssertionError');
+});

e2e/debug-cocotb.spec.js

@@ -0,0 +1,27 @@
+import { test, expect } from '@playwright/test';
+
+test('cocotb: debug - check wasmTable', async ({ page }) => {
+  const consoleLogs = [];
+  page.on('console', msg => {
+    const text = `[${msg.type()}] ${msg.text()}`;
+    consoleLogs.push(text);
+  });
+
+  await page.goto('/');
+  await page.getByRole('button', { name: 'cocotb Basics' }).click();
+  await page.getByRole('button', { name: /Your First cocotb Test/ }).click();
+  await page.getByTestId('solve-button').click();
+  await page.getByTestId('run-button').click();
+
+  await page.waitForTimeout(20000);
+
+  const logs = page.getByTestId('runtime-logs');
+  const text = await logs.textContent();
+
+  console.log('=== Runtime logs ===');
+  console.log(text);
+  console.log('=== Console logs (last 40) ===');
+  consoleLogs.slice(-40).forEach(l => console.log(l));
+
+  expect(text).not.toContain('# cocotb error');
+});

e2e/formal.spec.js

@@ -0,0 +1,90 @@
+import { test, expect } from '@playwright/test';
+
+// Helper: expand a chapter in the sidebar and click a lesson.
+async function goToLesson(page, chapterName, lessonName) {
+  await page.goto('/');
+  await page.getByRole('button', { name: chapterName }).click();
+  await page.getByRole('button', { name: lessonName }).click();
+  await expect(page.getByRole('heading', { level: 2, name: lessonName })).toBeVisible();
+}
+
+// ── BMC: Bounded Model Checking ───────────────────────────────────────────────
+
+test('BMC: starter code has no assertion → verify does not prove anything', async ({ page }) => {
+  await goToLesson(page, 'Implication & BMC', 'Bounded Model Checking');
+
+  await page.getByTestId('verify-button').click();
+
+  const logs = page.getByTestId('runtime-logs');
+  await expect(logs).toContainText('$ circt-verilog', { timeout: 120_000 });
+  await expect(logs).toContainText('$ circt-bmc', { timeout: 120_000 });
+  // No assertion in the module → bmc may exit with 0 but won't say "proved"
+  await expect(logs).not.toContainText('# circt-verilog exit code: 1');
+});
+
+test('BMC: solution proves all properties within the bound', async ({ page }) => {
+  await goToLesson(page, 'Implication & BMC', 'Bounded Model Checking');
+
+  await page.getByTestId('solve-button').click();
+  await page.getByTestId('verify-button').click();
+
+  const logs = page.getByTestId('runtime-logs');
+  await expect(logs).toContainText('$ circt-verilog', { timeout: 120_000 });
+  await expect(logs).toContainText('$ circt-bmc', { timeout: 120_000 });
+  await expect(logs).toContainText('[z3] unsat', { timeout: 120_000 });
+  await expect(logs).not.toContainText('# circt-verilog exit code: 1');
+  await expect(logs).not.toContainText('# circt-bmc exit code: 1');
+});
+
+test('BMC: shows only verify button, no run button', async ({ page }) => {
+  await goToLesson(page, 'Implication & BMC', 'Bounded Model Checking');
+
+  await expect(page.getByTestId('verify-button')).toBeVisible();
+  await expect(page.getByTestId('run-button')).toHaveCount(0);
+});
+
+// ── BMC: assume property ──────────────────────────────────────────────────────
+
+test('assume property: solution proves property with constraint', async ({ page }) => {
+  await goToLesson(page, 'Formal Verification', 'assume property');
+
+  await page.getByTestId('solve-button').click();
+  await page.getByTestId('verify-button').click();
+
+  const logs = page.getByTestId('runtime-logs');
+  await expect(logs).toContainText('[z3] unsat', { timeout: 120_000 });
+});
+
+// ── LEC: Logical Equivalence Checking ────────────────────────────────────────
+
+test('LEC: only shows verify (LEC) button, no run button', async ({ page }) => {
+  await goToLesson(page, 'Formal Verification', 'Logical Equivalence Checking');
+
+  await expect(page.getByTestId('verify-button')).toBeVisible();
+  await expect(page.getByTestId('verify-button')).toHaveText('verify (LEC)');
+  await expect(page.getByTestId('run-button')).toHaveCount(0);
+});
+
+test('LEC: buggy Impl is detected as NOT equivalent', async ({ page }) => {
+  await goToLesson(page, 'Formal Verification', 'Logical Equivalence Checking');
+
+  await page.getByTestId('verify-button').click();
+
+  const logs = page.getByTestId('runtime-logs');
+  await expect(logs).toContainText('$ circt-verilog', { timeout: 120_000 });
+  await expect(logs).toContainText('$ circt-lec', { timeout: 120_000 });
+  await expect(logs).toContainText('[z3] sat', { timeout: 120_000 });
+  await expect(logs).not.toContainText('# circt-verilog exit code: 1');
+});
+
+test('LEC: fixed Impl is proved equivalent to Spec', async ({ page }) => {
+  await goToLesson(page, 'Formal Verification', 'Logical Equivalence Checking');
+
+  await page.getByTestId('solve-button').click();
+  await page.getByTestId('verify-button').click();
+
+  const logs = page.getByTestId('runtime-logs');
+  await expect(logs).toContainText('[z3] unsat', { timeout: 120_000 });
+  await expect(logs).not.toContainText('# circt-verilog exit code: 1');
+  await expect(logs).not.toContainText('# circt-lec exit code: 1');
+});