VerifiedJS Agent Dashboard

Sorries: 12 2026-03-19 22:56 UTC

(no runs yet)

(no runs yet)

## Run: 2026-03-19T21:30:01+00:00

2026-03-19T21:30:01+00:00 EXIT: code 126
2026-03-19T21:30:01+00:00 DONE

## Run: 2026-03-19T22:05:01+00:00

2026-03-19T22:05:02+00:00 EXIT: code 1
2026-03-19T22:05:02+00:00 DONE

# VerifiedJS — Progress Tracker

## Pipeline Status

| Pass | Syntax | Semantics | Interp | Print | Pass Impl | Proof |
|------|--------|-----------|--------|-------|-----------|-------|
| Source (AST) | ✅ full ES2020 | N/A | N/A | baseline | N/A | N/A |
| Lexer/Parser | ✅ | N/A | N/A | N/A | ✅ recursive descent (96.30% flagship coverage, 1976/2052 on 2026-03-08) | N/A |
| Core | ✅ | ✅ `step?` | ✅ small-step driver | ✅ full pretty-printer | Elaborate: ✅ (stubs for classes/for-in/destructuring) | stub |
| Flat | ✅ | ✅ `step?` (all constructors) | ✅ small-step driver | ✅ full pretty-printer | ClosureConvert: ✅ builds, handles free vars + env threading | stub |
| ANF | ✅ | ✅ `step?`, `Step`, `Steps`, `Behaves` | ✅ small-step driver | ✅ full pretty-printer | Convert: ✅, Optimize: ✅ (identity) | OptimizeCorrect: ✅ |
| Wasm.IR | ✅ | N/A | ✅ symbolic stack-machine (359 lines) | ✅ WAT-like pretty-printer | Lower: ✅ (with start wrapper + func bindings) | stub |
| Wasm.AST | ✅ | ✅ `step?`, `Step`, `Steps`, `Behaves` | stub | ✅ full WAT printer (all instructions) | Emit: ✅ (IR→AST with label resolution) | stub |
| Wasm.Binary | N/A | N/A | N/A | N/A | ✅ full encoder (LEB128 + all sections) | N/A |

## End-to-End Pipeline Status

**Working**: Parse → Elaborate → ClosureConvert → ANF Convert → Optimize → Lower → Emit → Binary

- Simple arithmetic programs compile to valid .wasm and run on wasmtime ✅
- Programs with top-level function definitions compile to .wasm ✅ (but wasmtime rejects due to runtime helper calls)
- All `--emit=` targets work: core, flat, anf, wasmIR, wat
- All `--run=` targets wired: core, flat, anf, wasmIR

### Known Wasm Runtime Issues

1. **Runtime helper functions missing**: Programs with function calls emit `call RuntimeIdx.*` (indices 0-15) but no runtime functions are defined in the module. Wasmtime rejects with "function index out of bounds".
2. **Value representation (partial)**: Lowering now carries JS values through `f64` with boxed placeholders and 

# VerifiedJS — Proof Blockers

Record goals agents are stuck on. Agents must read this before starting proof work.

Format:
```
### File:Line — lemma_name
**Goal**: (paste goal state)
**Attempts**:
1. approach tried — result
2. ...
**Status**: OPEN | ESCALATE (if attempted 3+ times)
```

---

(No blockers yet — project just initialized)

# VerifiedJS — Task List

## Priority 1 (blocking — end-to-end correctness)
- [ ] Parser milestone: parse ≥95% of JS files selected by `scripts/parse_flagship.sh --full` (current: 96.30% = 1976/2052 on 2026-03-08) — TODO(supervisor): symbolic checks failed
- [ ] Fix value representation in Wasm lowering: all JS values are currently lowered as i32 (ptr) but numeric operations need proper f64 handling. Need NaN-boxing or tagged pointer scheme. — TODO(supervisor): Implement end-to-end NaN-box decode/encode in lowering and runtime helpers so numeric/truthy ops operate on decoded JS values, not raw boxed `f64` payloads.; Replace placeholder f64/`bits:` handling with full NaN-box encode/decode across lo — TODO(supervisor): agent merged code but did not mark task as [x] for supervisor validation
- [ ] Fix float constant emission: `lowerTrivial` emits ptr constants for numbers but the Wasm emit maps ptr→i32, losing float precision. Numbers like `1.5` become `0`.
- [x] Handle global variable references in lowering (e.g., `console`, `Math`, `JSON`) — compile path now lowers unresolved identifiers via runtime global lookup stub; runtime semantics still TODO

## Priority 2 (important — completeness)
- [ ] Elaborate: implement class declarations (SPEC §14.6) — currently stubs
- [ ] Elaborate: implement for-in/for-of (SPEC §13.7) — currently stubs
- [ ] Elaborate: implement destructuring (SPEC §13.15.5) — currently stubs
- [ ] Elaborate: implement optional chaining (SPEC §13.3) — currently stubs
- [ ] Core.Interp: implement remaining constructs (currently returns "unimplemented" for many)
- [ ] Make test suite cover more of the parser
- [ ] Make test suite cover core elaboration
- [ ] Make test suite check ANF conversion
- [ ] Make test suite check Wasm lowering

## Priority 3 (proof work)
- [ ] Prove ElaborateCorrect.lean
- [ ] Prove ClosureConvertCorrect.lean
- [ ] Prove ANFConvertCorrect.lean
- [ ] Prove LowerCorrect.lean
- [ ] Prove EmitCorrect.lean
- [ ] Compose EndToEnd.lea