spec: update grammar header to 12-level framework

Header comment now lists all 12 levels including Level 11 (tropical
cost-tracking) and Level 12 (epistemic safety). Grammar body productions
for L11-12 surface syntax are the next step.

Co-Authored-By: Claude Opus 4.6 (1M context) <noreply@anthropic.com>

Author: hyperpolymath

spec/grammar.ebnf

@@ -6,9 +6,10 @@
  * Version: 0.1.0
  * Date: 2026-03-21
  *
- * Applies TypeLL's 10 levels of type safety to WebAssembly linear memory,
- * treating memory regions as typed schemas and memory operations as typed
- * projections — analogous to how TypedQL treats database tables and queries.
+ * Applies TypeLL's 12-level progressive type safety framework to WebAssembly
+ * linear memory, treating memory regions as typed schemas and memory operations
+ * as typed projections — analogous to how TypedQL treats database tables and
+ * queries.
  *
  * The key insight: WASM linear memory is an untyped byte store that programs
  * "query" with load/store instructions at byte offsets. This grammar makes
@@ -17,8 +18,10 @@
  *   - Typing all memory access through schema projections
  *   - Proving safety properties at compile time via dependent types
  *   - Enabling multi-module shared memory with cross-module type agreement
+ *   - Bounding access pattern costs via tropical semiring annotations
+ *   - Preventing stale reads via epistemic freshness tracking
  *
- * The 10 levels adapted for WASM memory:
+ * The 12 levels adapted for WASM memory:
  *   Level  1: Instruction validity (well-formed access expressions)
  *   Level  2: Region-binding (every access resolves to a declared region.field)
  *   Level  3: Type-compatible access (load type matches field declaration)
@@ -29,6 +32,8 @@
  *   Level  8: Effect-tracking (Read / Write / Alloc / Free distinguished)
  *   Level  9: Lifetime safety (no use-after-free, no dangling pointers)
  *   Level 10: Linearity (resources used exactly once, memory freed exactly once)
+ *   Level 11: Tropical cost-tracking (access pattern costs bounded by semiring)
+ *   Level 12: Epistemic safety (reads require fresh knowledge of shared state)
  *)
 
 (* ============================================================================