docs: update documentation to match current implementation

- SKILLS.md: Update roadmap phases with actual completion status
  - Phase 0-1 complete, Phase 2-5 partial, resolved design decisions
- OVERVIEW.md: Add HttpServer, Test effect, JIT to completed features
- ROADMAP.md: Add HttpServer, Process, Test effects to done list
- VISION.md: Update Phase 2-3 tables with current status
- guide/05-effects.md: Add Time, HttpServer, Test to effects table
- guide/09-stdlib.md: Add HttpServer, Time, Test effect docs
- reference/syntax.md: Fix interpolation syntax, remove unsupported literals
- testing.md: Add native Test effect documentation

Co-Authored-By: Claude Opus 4.5 <noreply@anthropic.com>

SKILLS.md

@@ -569,36 +569,36 @@ type HttpError = { NotFound | Timeout | ..rest }
 
 ## 5. Implementation Roadmap
 
-### Phase 0: Foundation
+### Phase 0: Foundation ✅ COMPLETE
 
 **Goal**: Minimal viable compiler
 
-- [ ] Lexer and parser for core syntax
-- [ ] AST representation
-- [ ] Basic type checker (no effects, no versions, no properties)
-- [ ] Interpreter for testing semantics
-- [ ] REPL
+- [x] Lexer and parser for core syntax
+- [x] AST representation
+- [x] Basic type checker (Hindley-Milner inference)
+- [x] Interpreter for testing semantics
+- [x] REPL with history, completions, syntax highlighting
 
-**Deliverable**: Can type-check and interpret pure functional programs
+**Deliverable**: Can type-check and interpret pure functional programs ✅
 
 ```lux
 fn fib(n: Int): Int =
   if n <= 1 then n else fib(n-1) + fib(n-2)
 ```
 
-### Phase 1: Effect System
+### Phase 1: Effect System ✅ COMPLETE
 
 **Goal**: First-class algebraic effects
 
-- [ ] Effect declarations
-- [ ] Effect signatures on functions
-- [ ] Handler definitions
-- [ ] `run ... with` syntax
-- [ ] Effect inference within function bodies
-- [ ] Effect polymorphism
-- [ ] Built-in effects (Fail, State, etc.)
+- [x] Effect declarations
+- [x] Effect signatures on functions
+- [x] Handler definitions
+- [x] `run ... with` syntax
+- [x] Effect inference within function bodies
+- [x] Effect polymorphism
+- [x] Built-in effects (Console, Fail, State, Random, File, Http, Time, Process, Test)
 
-**Deliverable**: Can define, handle, and compose effects
+**Deliverable**: Can define, handle, and compose effects ✅
 
 ```lux
 effect Console { fn print(s: String): Unit }
@@ -610,28 +610,33 @@ fn main() =
   run greet("World") with { Console = stdoutConsole }
 ```
 
-### Phase 2: Code Generation
+### Phase 2: Code Generation ⚠️ PARTIAL
 
 **Goal**: Compile to a real target
 
-- [ ] IR design (effect-aware)
-- [ ] Backend selection (LLVM, WASM, or JS)
-- [ ] Effect handler compilation (CPS or evidence-passing)
+- [x] JIT compiler (Cranelift) - works for numeric code (~160x speedup)
+- [x] C backend scaffolding
+- [ ] Full JIT (strings, lists, ADTs, effects)
+- [ ] JavaScript backend
+- [ ] WASM backend
 - [ ] Optimization passes
-- [ ] Runtime library
 
 **Deliverable**: Compiled programs that run natively or in browser
 
-### Phase 3: Schema Evolution
+**Current**: `lux compile <file>` JIT compiles numeric code. C backend in progress.
+
+### Phase 3: Schema Evolution ⚠️ PARTIAL
 
 **Goal**: Versioned types with migrations
 
-- [ ] Version annotations on types (`@v1`, `@v2`)
-- [ ] Compatibility checker
-- [ ] Migration syntax (`from @v1 = ...`)
-- [ ] Migration chaining
+- [x] Version annotations on types (`@v1`, `@v2`)
+- [x] Migration syntax (`from @v1 = ...`)
+- [x] Version constraints (`@v2+`, `@latest`)
+- [x] Runtime versioned values
+- [x] Schema registry & compatibility checking
+- [ ] Type system integration (versions partially ignored in typechecker)
+- [ ] Auto-migration generation
 - [ ] Codec generation
-- [ ] Version constraints (`@v2+`, `@latest`)
 
 **Deliverable**: Types with automatic serialization and migration
 
@@ -642,16 +647,19 @@ type Config @v2 { host: String, port: Int, from @v1 = { port: 8080, ..v1 } }
 let cfg: Config @v2 = Codec.decode(legacyBytes)
 ```
 
-### Phase 4: Behavioral Types
+### Phase 4: Behavioral Types ⚠️ PARTIAL
 
 **Goal**: Property specifications and verification
 
-- [ ] Property syntax (`is pure`, `where result > 0`)
-- [ ] Built-in properties (pure, total, idempotent, etc.)
-- [ ] Refinement type checking
+- [x] Property syntax (`is pure`, `is total`, `is idempotent`, etc.)
+- [x] Built-in properties parsing
+- [x] Pure function checking (no effects)
+- [ ] Total function verification
+- [ ] Idempotent verification
+- [ ] Deterministic verification
+- [ ] Where clause enforcement
 - [ ] SMT solver integration (Z3)
 - [ ] Property-based test generation
-- [ ] Property inference for simple cases
 - [ ] `assume` escape hatch
 
 **Deliverable**: Compile-time verification of behavioral properties
@@ -664,49 +672,56 @@ fn abs(x: Int): Int
 = if x < 0 then -x else x
 ```
 
-### Phase 5: Ecosystem
+### Phase 5: Ecosystem ✅ MOSTLY COMPLETE
 
 **Goal**: Usable for real projects
 
-- [ ] Package manager
-- [ ] Standard library
-- [ ] LSP server (IDE support)
+- [x] Standard library (List, String, Option, Result, Math, Json modules)
+- [x] LSP server (diagnostics, hover, completions)
+- [x] REPL with history, tab completion, syntax highlighting
+- [x] Formatter
+- [x] Watch mode / hot reload
+- [x] Basic debugger
+- [x] Module system (imports, exports, aliases)
+- [ ] Package manager (manifest parsing exists, not fully functional)
 - [ ] Documentation generator
-- [ ] REPL improvements
-- [ ] Debugger
 - [ ] Profiler
 
 ### Phase 6: Advanced Features
 
 **Goal**: Full language vision
 
-- [ ] Database effect with schema-aware queries
-- [ ] HTTP effect with API versioning
-- [ ] Incremental computation (bonus feature)
+- [x] HTTP client effect
+- [x] HTTP server effect
+- [x] File system effect
+- [x] Process/shell effect
+- [x] Test effect (native testing framework)
+- [ ] Database/SQL effect
+- [ ] Incremental computation
 - [ ] Distributed effects (location-aware)
-- [ ] Proof assistant mode (optional full verification)
+- [ ] Proof assistant mode
 
 ---
 
-## Open Design Questions
+## Resolved Design Decisions
 
-### Syntax
+### Syntax (Decided)
 
-- [ ] Significant whitespace vs braces?
-- [ ] Effect syntax: `with {E1, E2}` vs `!E1 + E2` vs `<E1, E2>`?
-- [ ] Version syntax: `@v1` vs `v1` vs `#1`?
+- [x] Braces for blocks, not significant whitespace
+- [x] Effect syntax: `with {E1, E2}`
+- [x] Version syntax: `@v1`, `@v2+`, `@latest`
 
-### Semantics
+### Semantics (Decided)
 
-- [ ] Effect handler semantics: deep vs shallow handlers?
-- [ ] Version compatibility: structural or nominal?
-- [ ] Property verification: sound or best-effort?
+- [x] Deep handlers (algebraic effect style with resume)
+- [x] Structural compatibility for records
+- [x] Best-effort property verification (gradual)
 
-### Pragmatics
+### Pragmatics (In Progress)
 
-- [ ] Primary compile target: native, WASM, JS?
-- [ ] Interop story: FFI design?
-- [ ] Gradual adoption: can you use Lux from other languages?
+- Primary target: Tree-walking interpreter (default), JIT for performance
+- FFI: Shell commands via Process effect
+- [ ] JavaScript backend for browser use
 
 ---