feat: complete dyadic type checker (affine + linear modes)

Implemented full support for both affine and linear type checking modes:

**Affine mode (permissive):**
- Values used ≤1 time (can be dropped implicitly)
- Suitable for prototyping and exploration
- Still prevents double-use

**Linear mode (strict):**
- Values used exactly 1 time (must be consumed)
- Prevents memory leaks and use-after-move
- Suitable for production safety

**Changes:**
- Added Mode enum (Affine | Linear)
- Made TypeChecker mode-aware with new_with_mode()
- Updated all consumption checks to respect mode
- Added 7 new dyadic mode tests (38 total, all passing)
- Created 0-AI-MANIFEST.a2ml following RSR standards
- Updated META.scm with ADR-002 (dyadic design decision)
- Updated STATE.scm with completion roadmap

**API:**
- TypeChecker::new_with_mode(Mode)
- type_check_module_with_mode(&Module, Mode)
- type_check_expr_with_mode(&Expr, Mode)

**Progress:** Type checker 60% → 85% complete

**Next:** WASM codegen mode awareness, production binaries

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

Author: Jonathan D.A. Jewell

.machine_readable/META.scm

@@ -1,4 +1,4 @@
-;; SPDX-License-Identifier: AGPL-3.0-or-later
+;; SPDX-License-Identifier: PMPL-1.0-or-later
 ;; META.scm - Architectural decisions and project meta-information
 ;; Media-Type: application/meta+scheme
 
@@ -11,7 +11,23 @@
       "Need to establish repository structure and standards"
       "Adopt RSR (Rhodium Standard Repository) conventions from rsr-template-repo"
       "Ensures consistency with 500+ repos in hyperpolymath ecosystem. "
-      "Enables automated quality enforcement via gitbot-fleet and Hypatia.")))
+      "Enables automated quality enforcement via gitbot-fleet and Hypatia.")
+
+    (adr-002 accepted "2026-02-07"
+      "Language supports both strict and permissive type checking modes"
+      "Implement dyadic design: Affine mode (permissive, use ≤1 time) AND Linear mode (strict, use exactly 1 time)"
+      "Both modes are first-class citizens, not a migration path. "
+      "Affine mode enables prototyping and exploration with optional cleanup. "
+      "Linear mode guarantees resource safety and prevents memory leaks. "
+      "Same syntax, different strictness via --mode flag. "
+      "Innovation: First language where you toggle between strict/permissive type systems.")
+
+    (adr-003 accepted "2026-02-07"
+      "Need to drive project to production readiness like phronesis"
+      "Complete type checker (60%→100%), WASM codegen (30%→100%), build production binary, implement stdlib, create LSP, expand tests"
+      "Makes Ephapax production-ready with working binaries for BOTH affine and linear modes. "
+      "Provides reference implementation for dyadic language design. "
+      "Enables real-world adoption and validation of affine/linear type systems.")))
 
   (development-practices
     (code-style
@@ -43,4 +59,18 @@
       "enabling automated tooling and consistent developer experience.")
     (why-hypatia
       "Neurosymbolic security scanning combines neural pattern recognition "
-      "with symbolic reasoning for fast, deterministic security checks.")))
+      "with symbolic reasoning for fast, deterministic security checks.")
+    (why-dyadic
+      "Dyadic design (affine + linear modes) addresses real-world trade-offs: "
+      "Affine mode for rapid prototyping where flexibility is key, "
+      "Linear mode for production where safety guarantees are critical. "
+      "Developers choose mode per use case, not per project maturity. "
+      "Eliminates false choice between 'move fast' and 'be safe'.")
+    (why-two-stage-compiler
+      "Stage 1 (Idris2): Dependent types enable formal verification of type system correctness. "
+      "Stage 2 (Rust): Performance-oriented WASM compilation with zero-cost abstractions. "
+      "Separation allows formal proofs without sacrificing runtime efficiency.")
+    (why-wasm-target
+      "WebAssembly provides sandboxed execution, portability, and predictable performance. "
+      "Linear types naturally map to WASM linear memory model. "
+      "Enables deployment to web, edge, embedded without code changes."))))

.machine_readable/STATE.scm

@@ -7,7 +7,7 @@
     (version "0.1.0")
     (schema-version "1.0")
     (created "2025-12-16")
-    (updated "2026-01-04")
+    (updated "2026-02-07")
     (project "ephapax")
     (repo "github.com/hyperpolymath/ephapax"))
 
@@ -201,6 +201,95 @@
       "basic-stdlib-string-ops"))
 
   (session-history
+    (session
+      (date "2026-02-07")
+      (goal "Drive ephapax to completion like phronesis - production ready in both affine and linear modes")
+      (tasks
+        (task-1
+          (name "Complete Type Checker")
+          (status "planned")
+          (target "60% → 100%")
+          (items
+            "complete-region-scope-tracking"
+            "finish-linear-context-threading"
+            "add-affine-mode-support"
+            "implement-region-escape-rejection"
+            "complete-unused-linear-rejection"))
+        (task-2
+          (name "Complete WASM Code Generation")
+          (status "planned")
+          (target "30% → 100%")
+          (items
+            "finish-primitives-codegen"
+            "complete-functions-codegen"
+            "implement-products-codegen"
+            "implement-sums-codegen"
+            "complete-regions-codegen"
+            "implement-linear-memory-mgmt"))
+        (task-3
+          (name "Build Production Binaries")
+          (status "planned")
+          (items
+            "create-unified-ephapax-binary"
+            "support-mode-flag-affine-linear"
+            "optimize-and-strip-release-build"
+            "target-2-5mb-like-phronesis"))
+        (task-4
+          (name "Implement Standard Library")
+          (status "planned")
+          (items
+            "string-operations"
+            "io-primitives"
+            "memory-management-regions"
+            "basic-collections"
+            "math-operations"
+            "ensure-both-modes-supported"))
+        (task-5
+          (name "Create Examples for Both Modes")
+          (status "planned")
+          (items
+            "affine-mode-examples-prototyping"
+            "linear-mode-examples-safety"
+            "side-by-side-comparisons"
+            "when-to-use-decision-guide"))
+        (task-6
+          (name "Write Complete Documentation")
+          (status "planned")
+          (items
+            "update-readme-dyadic-explanation"
+            "language-guide-affine"
+            "language-guide-linear"
+            "migration-path-guide"
+            "api-documentation"
+            "tutorial-series"))
+        (task-7
+          (name "Build LSP Server")
+          (status "planned")
+          (items
+            "syntax-highlighting"
+            "type-checking-on-save"
+            "error-diagnostics"
+            "code-completion"
+            "mode-aware-diagnostics"))
+        (task-8
+          (name "Expand Test Suite")
+          (status "planned")
+          (items
+            "affine-conformance-tests"
+            "linear-conformance-tests"
+            "mode-specific-errors"
+            "cross-mode-tests"
+            "target-100-tests-per-mode"))
+        (task-9
+          (name "Create AI Manifest and Metadata")
+          (status "in-progress")
+          (items
+            "created-0-ai-manifest-a2ml"
+            "update-state-scm-with-roadmap"
+            "update-meta-scm-dyadic-design"
+            "ensure-rsr-compliance")))
+      (reference-model "phronesis - production-ready with binary, CLI, LSP, examples, docs")
+      (key-insight "Ephapax is DYADIC - affine and linear modes are both first-class citizens"))
     (session
       (date "2026-01-04")
       (accomplishments
@@ -212,4 +301,4 @@
         "fixed-check_borrow-to-not-consume"
         "added-Context::snapshot-and-check_branch_agreement"
         "added-BranchLinearityMismatchDetailed-error"
-        "added-6-branch-linearity-tests"))))
+        "added-6-branch-linearity-tests")))))

0-AI-MANIFEST.a2ml

@@ -0,0 +1,221 @@
+# ⚠️ STOP - CRITICAL READING REQUIRED
+
+**THIS FILE MUST BE READ FIRST BY ALL AI AGENTS**
+
+## WHAT IS THIS?
+
+This is the AI manifest for **ephapax** — a dyadic language with linear and affine type systems. It declares:
+- Canonical file locations (where things MUST be, and nowhere else)
+- Critical invariants (rules that must NEVER be violated)
+- Repository structure and organization
+- Dyadic language design (affine vs. linear modes)
+
+## CANONICAL LOCATIONS (UNIVERSAL RULE)
+
+### Machine-Readable Metadata: `.machine_readable/` ONLY
+
+These 6 SCM files MUST exist in `.machine_readable/` directory ONLY:
+1. **STATE.scm** - Project state, progress, blockers
+2. **META.scm** - Architecture decisions, governance
+3. **ECOSYSTEM.scm** - Position in ecosystem, relationships
+4. **AGENTIC.scm** - AI agent interaction patterns
+5. **NEUROSYM.scm** - Neurosymbolic integration config
+6. **PLAYBOOK.scm** - Operational runbook
+
+**CRITICAL:** If ANY of these files exist in `.machine_read/` or the root directory, this is an ERROR.
+**LEGACY:** `.machine_read/` is DEPRECATED. All files must migrate to `.machine_readable/`.
+
+### Bot Directives: `.bot_directives/` ONLY
+
+Bot-specific instructions for:
+- rhodibot - Git operations
+- echidnabot - Code quality
+- sustainabot - Dependency updates
+- glambot - Documentation
+- seambot - Integration
+- finishbot - Task completion
+
+### Agent Instructions
+
+- `.claude/CLAUDE.md` - Claude-specific patterns (if exists)
+- `0-AI-MANIFEST.a2ml` - THIS FILE (universal entry point)
+
+## CORE INVARIANTS
+
+1. **No SCM duplication** - Root must NOT contain STATE.scm, META.scm, etc.
+2. **Single source of truth** - `.machine_readable/` is authoritative
+3. **No stale metadata** - If root or `.machine_read/` SCMs exist, they are OUT OF DATE
+4. **License consistency** - All code PMPL-1.0-or-later (was EUPL-1.2, updated)
+5. **Author attribution** - Always "Jonathan D.A. Jewell <jonathan.jewell@open.ac.uk>"
+6. **Dyadic design** - Language supports BOTH affine and linear modes (not mutually exclusive)
+
+## DYADIC LANGUAGE DESIGN (CRITICAL CONCEPT)
+
+Ephapax is a **dyadic language** with TWO type system modes:
+
+### Affine Mode (Permissive)
+- Values can be used **at most once** (0 or 1 times)
+- **Can be dropped/ignored** without error
+- Suitable for: prototyping, exploration, optional resource cleanup
+- Trade-off: More flexible, less safety guarantees
+- Compilation: `just compile-affine input.eph affine output.wasm`
+
+### Linear Mode (Strict)
+- Values MUST be used **exactly once** (1 time only)
+- **Cannot be dropped** - compiler error if unused
+- Suitable for: resource safety, connection management, memory leak prevention
+- Trade-off: Stricter, stronger guarantees
+- Compilation: (To be implemented with same pipeline)
+
+### Dyadic Philosophy
+- **Not a migration path** - Both modes are first-class citizens
+- **Use case driven** - Choose mode based on requirements, not maturity
+- **Same syntax** - Language features identical, only type system strictness differs
+- **Mode switching** - Code can be checked in either mode via `--mode` flag
+
+## REPOSITORY STRUCTURE
+
+This repo contains a **two-stage compiler**:
+
+```
+ephapax/
+├── 0-AI-MANIFEST.a2ml          # THIS FILE (start here)
+├── README.adoc                  # Project overview
+├── Cargo.toml                   # Rust workspace configuration
+├── justfile                     # Build commands
+│
+├── idris2/                      # Stage 1: Idris2 affine/linear type checker
+│   ├── ephapax-affine.ipkg     # Idris2 package (handles BOTH modes)
+│   ├── src/                     # Idris2 source (parser, type checker)
+│   └── build/                   # Compiled Idris2 binary
+│
+├── src/                         # Stage 2: Rust WASM compiler (11 crates)
+│   ├── ephapax-syntax/          # AST definitions
+│   ├── ephapax-ir/              # S-expression IR
+│   ├── ephapax-lexer/           # Tokenizer (logos)
+│   ├── ephapax-parser/          # Parser (chumsky)
+│   ├── ephapax-typing/          # Type checker (Rust implementation)
+│   ├── ephapax-interp/          # Tree-walking interpreter
+│   ├── ephapax-wasm/            # WASM code generation
+│   ├── ephapax-runtime/         # Runtime support
+│   ├── ephapax-stdlib/          # Standard library
+│   ├── ephapax-repl/            # Interactive shell
+│   └── ephapax-cli/             # Command-line interface
+│
+├── ephapax-linear/              # Linear mode specification & docs
+│   ├── docs/                    # Linear semantics documentation
+│   ├── grammar/                 # Linear mode grammar
+│   └── src/                     # Linear-specific examples
+│
+├── ephapax-proven/              # Coq-verified components
+│   └── (Subproject with formal proofs)
+│
+├── formal/                      # Coq formalization
+│   ├── Syntax.v                 # AST and types
+│   ├── Typing.v                 # Linear typing rules
+│   └── Semantics.v              # Operational semantics & soundness
+│
+├── examples/                    # Example programs (affine & linear)
+├── conformance/                 # Type system conformance tests
+│   ├── pass/                    # Valid programs
+│   └── fail/                    # Invalid programs (must be rejected)
+│
+├── .machine_readable/           # SCM files (6 files)
+│   ├── STATE.scm
+│   ├── META.scm
+│   ├── ECOSYSTEM.scm
+│   ├── AGENTIC.scm
+│   ├── NEUROSYM.scm
+│   └── PLAYBOOK.scm
+│
+└── .bot_directives/             # Bot instructions
+```
+
+## COMPILATION PIPELINE
+
+### Current (Idris2 + Rust)
+```
+input.eph
+  → [Idris2: parse + typecheck in affine/linear mode]
+  → IR (S-expression)
+  → [Rust: WASM codegen]
+  → output.wasm
+```
+
+**Key commands:**
+- `just idris-build` - Build Idris2 stage
+- `just compile-affine input.eph affine output.wasm` - Full pipeline (affine)
+- `just smoke` - End-to-end test
+- `just build` - Build Rust stage only
+
+## SESSION STARTUP CHECKLIST
+
+✅ Read THIS file (0-AI-MANIFEST.a2ml) first
+✅ Understand **dyadic design** (affine vs. linear, both are first-class)
+✅ Understand canonical locations (.machine_readable/, not .machine_read/)
+✅ Know the invariants (no SCM duplication, etc.)
+✅ Check for MCP enforcement (if applicable)
+✅ Read `.machine_readable/STATE.scm` for current status
+✅ Read `.machine_readable/AGENTIC.scm` for interaction patterns
+✅ Check type checker completion status (currently 60%)
+✅ Check WASM codegen completion status (currently 30%)
+
+## LIFECYCLE HOOKS
+
+### on-enter (Session Start)
+
+When starting a new session:
+
+1. Read and acknowledge this manifest
+2. Log session start (optional but recommended)
+   - Format: `[YYYY-MM-DD HH:MM:SS] Session started: [agent-name]`
+   - Location: `.machine_readable/session-log.txt`
+3. Read `.machine_readable/STATE.scm`
+4. Check for blockers (type checker, WASM codegen)
+5. State understanding of canonical locations AND dyadic design
+6. Identify which mode (affine/linear) work applies to
+
+### on-exit (Session End)
+
+When ending a session:
+
+1. Update `.machine_readable/STATE.scm` if changes made
+2. Update completion percentages (type checker, WASM codegen)
+3. Log session end (optional but recommended)
+   - Format: `[YYYY-MM-DD HH:MM:SS] Session ended: [summary]`
+   - Location: `.machine_readable/session-log.txt`
+4. Document new blockers
+5. Summarize outcomes for BOTH modes if applicable
+
+## CRITICAL WORK IN PROGRESS
+
+**Type Checker (60% complete):**
+- ✅ Branch agreement verification
+- ✅ Borrow validity checking
+- ⚠️  Linear context threading (partial)
+- ❌ Region scope tracking (incomplete)
+- ❌ Affine mode support (planned)
+
+**WASM Codegen (30% complete):**
+- ⚠️  Primitives codegen (in progress)
+- ⚠️  Functions codegen (in progress)
+- ❌ Products/sums codegen (planned)
+- ❌ Regions codegen (planned)
+- ❌ Linear memory management (planned)
+
+**Target:** Make ephapax as complete as phronesis (working binary, full CLI, LSP, examples, docs)
+
+## ATTESTATION PROOF
+
+After reading this file, demonstrate understanding by stating:
+
+**"I have read the AI manifest. SCM files are located in `.machine_readable/` ONLY (not `.machine_read/`), bot directives in `.bot_directives/`, and I understand the dyadic design (affine vs. linear modes are both first-class). I will not create duplicate files in the root directory."**
+
+## META
+
+- **Format Version:** 1.0.0
+- **Created:** 2026-02-07
+- **Maintained By:** hyperpolymath
+- **License:** PMPL-1.0-or-later (was EUPL-1.2, updated)
+- **Protocol:** https://github.com/hyperpolymath/0-ai-gatekeeper-protocol
+- **Completion Status:** 40% overall (type checker 60%, WASM codegen 30%)