docs: add demos and update documentation for new features

Documentation:
- Update IMPLEMENTATION_PLAN.md with current status (222 tests)
- Update feature comparison table (Schema Evolution, Behavioral Types: ✅)
- Add HttpServer to built-in effects list
- Update OVERVIEW.md with working behavioral types examples

Demo Programs:
- examples/schema_evolution.lux - Version annotations, constraints, runtime ops
- examples/behavioral_types.lux - pure, deterministic, commutative, idempotent, total

Sample Project:
- projects/rest-api/ - Full REST API demo with:
  - Task CRUD endpoints
  - Pattern matching router
  - JSON serialization
  - Effect-tracked request handling

Tests:
- Add behavioral type tests (pure, deterministic, commutative, idempotent, total)
- 227 tests passing

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

docs/IMPLEMENTATION_PLAN.md

@@ -2,7 +2,7 @@
 
 ## Current Status Summary
 
-### What's Working (150+ tests passing)
+### What's Working (222 tests passing)
 
 **Core Language:**
 - Lexer and parser for core syntax
@@ -31,7 +31,8 @@
 **Built-in Effects:**
 - `Console` - print, readLine, readInt
 - `File` - read, write, exists, delete, listDir, createDir
-- `Http` - get, post
+- `Http` - get, post, put, delete (HTTP client)
+- `HttpServer` - listen, accept, respond, respondWithHeaders, stop (HTTP server)
 - `Random` - int, float, range, bool, element
 - `Time` - now, sleep
 
@@ -41,9 +42,13 @@
 - Basic trait method dispatch
 
 **Behavioral Properties:**
-- Property declarations (`is pure`, `is idempotent`, etc.)
+- Property declarations (`is pure`, `is idempotent`, `is total`, `is deterministic`, `is commutative`)
 - Property parsing and storage in AST
 - Pure function verification (no effects allowed)
+- Deterministic verification (no Random/Time effects)
+- Commutative verification (operator-based analysis)
+- Idempotent verification (pattern-based analysis)
+- Total verification (structural recursion, termination checking)
 
 **Module System:**
 - Import/export with `pub` visibility
@@ -87,9 +92,10 @@
 12. `json.lux` - JSON parsing and serialization
 13. `jit_test.lux` - JIT compilation demo
 14. `guessing_game.lux` - Console input/output
-15. `examples/modules/main.lux` - Module imports
-16. `examples/modules/main_selective.lux` - Selective imports
-17. `examples/modules/main_wildcard.lux` - Wildcard imports
+15. `http_server.lux` - HTTP server with routing
+16. `examples/modules/main.lux` - Module imports
+17. `examples/modules/main_selective.lux` - Selective imports
+18. `examples/modules/main_wildcard.lux` - Wildcard imports
 
 ---
 
@@ -156,25 +162,21 @@ fn withRetry<E>(action: fn(): T with E, attempts: Int): T with E = ...
 3. Support effect quantification in type schemes
 
 #### 2.2 Built-in Effects
-**Status:** ⚠️ Partial - Several working, some missing
+**Status:** ✅ Core effects complete
 
 **Working Effects:**
 - `Console` - print, readLine, readInt
 - `File` - read, write, exists, delete, listDir, createDir
-- `Http` - get, post
+- `Http` - get, post, put, delete (HTTP client)
+- `HttpServer` - listen, accept, respond, respondWithHeaders, stop
 - `Random` - int, float, range, bool, element
 - `Time` - now, sleep
+- `State` - get, put (built-in)
+- `Reader` - ask (built-in)
 
-**Missing Effects:**
-- `State<S>` - get/put state (generic over state type)
-- `Reader<R>` - read-only environment
-- `Fail` - early returns/exceptions
-- `Async` - async/await
-
-**Implementation Steps:**
-1. Add generic effect support (`State<S>`)
-2. Implement `Fail` for error handling
-3. Add async/await pattern
+**Missing Effects (nice-to-have):**
+- `Async` - async/await pattern
+- Generic effect parameters (`State<S>`)
 
 #### 2.3 Resumable Handlers
 **Status:** Handlers exist but may not support continuation resumption.
@@ -187,19 +189,18 @@ fn withRetry<E>(action: fn(): T with E, attempts: Int): T with E = ...
 ### Priority 3: Schema Evolution
 
 #### 3.1 Versioned Types
-**Status:** Parser supports `@v1` syntax but runtime doesn't use it.
+**Status:** ✅ Type system integration complete
 
-**What's Missing:**
-- Version tracking in type system
-- Migration function generation
-- Compatibility checking
-- Codec generation
+**What's Working:**
+- Version annotations preserved in type system (`Int @v1`, `User @v2`)
+- Version mismatch detection at compile time
+- Version constraints: `@v1` (exact), `@v2+` (at least), `@latest` (any)
+- Versioned type declarations tracked
+- Migration bodies stored for future execution
 
-**Implementation Steps:**
-1. Track version in type representation
-2. Implement migration chain resolution
-3. Add compatibility rules to type checker
-4. Generate serialization code
+**Still Missing (nice-to-have):**
+- Auto-migration generation
+- Version-aware serialization/codecs
 
 ### Priority 4: Module System
 
@@ -297,14 +298,17 @@ The module system is fully functional with:
 11. **Full compilation** - Extend JIT or add WASM/JS backend
 
 ### Phase 4: Behavioral Types (Verification)
-12. **Total function verification** - Termination checking
-13. **Idempotent verification** - Pattern-based analysis
-14. **Where clause enforcement** - Constraint checking
+12. ~~**Total function verification**~~ ✅ Done - Termination checking
+13. ~~**Idempotent verification**~~ ✅ Done - Pattern-based analysis
+14. ~~**Deterministic verification**~~ ✅ Done - Effect-based analysis
+15. ~~**Commutative verification**~~ ✅ Done - Operator analysis
+16. **Where clause enforcement** - Constraint checking (basic parsing done)
 
 ### Phase 5: Schema Evolution (Data)
-15. **Type system version tracking**
-16. **Auto-migration generation**
-17. **Version-aware serialization**
+17. ~~**Type system version tracking**~~ ✅ Done
+18. ~~**Version mismatch detection**~~ ✅ Done
+19. **Auto-migration generation** - Generate migration code
+20. **Version-aware serialization** - Codecs
 
 ### Phase 6: Advanced Features
 18. **Refinement types** - SMT solver integration
@@ -343,8 +347,9 @@ The module system is fully functional with:
 | Type Classes | Basic | ✅ | ✅ | ✅ | ❌ |
 | String Interpolation | ✅ | ✅ | ❌ | ❌ | ✅ |
 | Effect Polymorphism | ❌ | ✅ | Via mtl | N/A | N/A |
-| Schema Evolution | ⚠️ Parsing | ❌ | ❌ | ❌ | ❌ |
-| Behavioral Types | ⚠️ Parsing | ❌ | ❌ | ❌ | ❌ |
+| Schema Evolution | ✅ | ❌ | ❌ | ❌ | ❌ |
+| Behavioral Types | ✅ | ❌ | ❌ | ❌ | ❌ |
+| HTTP Server | ✅ | ❌ | Via libs | Via libs | Via libs |
 | Refinement Types | Planned | ❌ | Via LH | ❌ | ❌ |
 | Tail Call Opt | ✅ | ✅ | ✅ | Limited | ❌ |
 | JIT Compilation | ⚠️ Numeric | ✅ | ✅ | N/A | N/A |
@@ -358,12 +363,14 @@ The module system is fully functional with:
 Lux differentiates itself through:
 
 1. **First-class algebraic effects** - Making side effects explicit, testable, and composable
-2. **Schema evolution** (planned) - Type-safe data migrations built into the language
-3. **Behavioral types** (planned) - Compile-time verification of properties like purity and totality
-4. **Developer experience** - Elm-style errors, REPL, LSP support
+2. **Schema evolution** - Type-safe version tracking with compile-time mismatch detection
+3. **Behavioral types** - Compile-time verification of purity, totality, determinism, idempotency
+4. **Built-in HTTP server** - Effect-tracked web servers without external frameworks
+5. **Developer experience** - Elm-style errors, REPL, LSP support
 
 The combination of these features makes Lux particularly suited for:
-- Building reliable backend services
+- Building reliable backend services with explicit effect tracking
 - Applications with complex state management
 - Systems requiring careful versioning and migration
 - Projects where testing and verification are critical
+- Educational use for learning algebraic effects

docs/OVERVIEW.md

@@ -157,11 +157,32 @@ import math.{sqrt, abs}
 import prelude.*
 ```
 
+### Also Working
+
+```lux
+// Behavioral types with compile-time verification
+fn factorial(n: Int): Int is pure is deterministic is total =
+    if n <= 1 then 1 else n * factorial(n - 1)
+
+fn add(a: Int, b: Int): Int is commutative = a + b
+
+fn absolute(x: Int): Int is idempotent =
+    if x < 0 then 0 - x else x
+
+// Schema evolution with version tracking
+fn processV2(data: Int @v2): Int = data * 2
+let value: Int @v2 = 42
+let result = processV2(value)
+
+// Version constraints
+fn processModern(x: Int @v2+): Int = x  // v2 or later
+fn processAny(x: Int @latest): Int = x  // any version
+```
+
 ### Planned (Not Yet Fully Implemented)
 
-- **Schema Evolution**: Parsing works (`@v1`, `from @v1`), type system integration missing
-- **Behavioral Types**: Parsing works (`is pure`, `is total`), verification beyond `pure` missing
 - **Full Compilation**: JIT works for numeric code, strings/lists/ADTs missing
+- **Auto-migration Generation**: Migration bodies stored, execution pending
 
 ---