diff --git a/doc/manual/souce/design/composition-and-materialization.md b/doc/manual/souce/design/composition-and-materialization.md
new file mode 100644
index 0000000..686c0f2
--- /dev/null
+++ b/doc/manual/souce/design/composition-and-materialization.md
@@ -0,0 +1,119 @@
+# Composition and Materialization
+
+`&`、`//`、`default`、materialize は、runtime value の variant に基づいて処理する。
+
+## `&`
+
+`&` は制約を保った合成である。
+
+```text
+compose_and(a: RuntimeValue, b: RuntimeValue) -> RuntimeValue | Diagnostic
+```
+
+基本規則:
+
+```text
+Abstract(a) & Abstract(b)
+  -> Abstract {
+       constraints: a.constraints + b.constraints,
+       default: merge_default(a.default, b.default)
+     }
+
+Abstract(a) & Concrete(v)
+  -> if satisfies(v, a.constraints) then Concrete(v)
+     else constraint diagnostic
+
+Concrete(v) & Abstract(a)
+  -> if satisfies(v, a.constraints) then Concrete(v)
+     else constraint diagnostic
+
+Concrete(Object(a)) & Concrete(Object(b))
+  -> Concrete(Object(fieldwise_and(a, b)))
+
+Concrete(a) & Concrete(b)
+  -> if a == b then Concrete(a)
+     else conflict diagnostic
+```
+
+`Abstract & Concrete` が成功した場合、default は消える。
+明示値があるなら fallback は不要だからである。
+
+## object の合成
+
+object は concrete structure だが、field の値は thunk 経由で concrete / abstract のどちらにもなりうる。
+object 同士の `&` は field ごとに再帰合成する。
+
+```dcdl
+MyConfig = {
+    host = String;
+    port = Int default 8080;
+};
+
+Config = MyConfig & {
+    host = "localhost";
+};
+```
+
+`host` は `Abstract(String) & Concrete("localhost")` として検証され、成功すれば `Concrete("localhost")` になる。
+`port` は右辺に明示値がないため、`Abstract(Int, default 8080)` のまま残る。
+
+## default の合成
+
+初期方針では、`&` による異なる default 同士の合成は conflict とする。
+同じ default は同一候補として扱ってよい。
+
+```text
+merge_default(None, None) -> None
+merge_default(Some(a), None) -> Some(a)
+merge_default(None, Some(b)) -> Some(b)
+merge_default(Some(a), Some(b)) -> if same(a, b) then Some(a) else conflict
+```
+
+`//` では右辺 default が左辺 default を置き換える。
+
+## `//`
+
+`//` は右辺優先の deep patch である。
+
+```text
+patch(a: RuntimeValue, b: RuntimeValue) -> RuntimeValue
+```
+
+基本規則:
+
+- object / object は field ごとに再帰 patch する。
+- object / object 以外は右辺で置き換える。
+- 左辺にしかない field は保持する。
+- 右辺にしかない field は追加する。
+- 配列、scalar、function は右辺置換とする。
+
+`//` は制約を保持するための演算子ではない。
+制約を満たす具体化には `&` を使う。
+
+## materialize
+
+materialize は runtime value を出力可能な `Data` に変換する。
+
+```text
+materialize(RuntimeValue) -> Data | Diagnostic
+```
+
+処理規則:
+
+```text
+Concrete(String/Int/Float/Bool) -> Data
+Concrete(Array(items))          -> each item を force して materialize
+Concrete(Object(fields))        -> each field を force して materialize
+Concrete(Function)              -> materialize 不能
+
+Abstract { constraints, default: Some(d) }
+  -> force(d)
+  -> result が constraints を満たすか検証
+  -> materialize(result)
+
+Abstract { constraints, default: None }
+  -> 未解決 abstract value として diagnostic
+```
+
+materialize は default を採用する唯一の段階である。
+通常評価中に明示値が得られた場合、default は採用されない。
diff --git a/doc/manual/souce/design/diagnostics-and-fallback.md b/doc/manual/souce/design/diagnostics-and-fallback.md
new file mode 100644
index 0000000..99a259a
--- /dev/null
+++ b/doc/manual/souce/design/diagnostics-and-fallback.md
@@ -0,0 +1,67 @@
+# Diagnostics and Fallback
+
+エラーは runtime value ではなく diagnostic として扱う。
+処理系はエラー内容に基づく汎用的な実行時分岐を提供しない。
+
+## Diagnostic
+
+```text
+Diagnostic {
+  kind: DiagnosticKind
+  span: Span
+  message: String
+  notes: Vec<Note>
+}
+```
+
+代表的な diagnostic kind:
+
+- syntax error
+- unresolved identifier
+- type mismatch
+- constraint violation
+- composition conflict
+- default conflict
+- cycle dependency
+- import failure
+- match failure
+- materialization failure
+
+## エラーは値ではない
+
+評価失敗は `RuntimeValue` ではなく `Diagnostic` を返す。
+そのため、通常の式はエラー内容に基づいて分岐できない。
+
+```text
+Result<RuntimeValue, Diagnostic>
+```
+
+これにより、制約違反、未定義識別子、循環依存、import 失敗などが通常値として流れることを避ける。
+
+## `try / catch` は core に入れない
+
+汎用 `try / catch` は core に入れない。
+エラーを制御フローとして扱うと、どの失敗を捕捉できるか、捕捉後の thunk state をどう扱うか、制約違反を握りつぶしてよいか、といった仕様が重くなる。
+
+fallback は有限で明示的な仕組みに限定する。
+
+- `default`: 未指定値の fallback。
+- `match`: 有限 pattern に基づく分岐。
+- optional import: ファイル不存在など、限定された失敗だけを fallback 可能にする候補。
+- optional field access: field 不在だけを fallback 可能にする候補。
+- union / tagged schema: 複数 schema の選択を明示的に表す将来候補。
+
+## optional fallback の扱い
+
+optional import や optional field access を導入する場合も、捕捉できる失敗は限定する。
+
+例として optional import は、ファイル不存在だけを fallback 可能にし、parse error や import 先の制約違反は diagnostic として報告する方がよい。
+
+```text
+optional import:
+  file not found -> fallback
+  parse error    -> diagnostic
+  eval error     -> diagnostic
+```
+
+この方針により、fallback は通常の値選択として扱い、エラー内容に依存した実行時分岐は避ける。
diff --git a/doc/manual/souce/design/execution-pipeline.md b/doc/manual/souce/design/execution-pipeline.md
new file mode 100644
index 0000000..016c2ab
--- /dev/null
+++ b/doc/manual/souce/design/execution-pipeline.md
@@ -0,0 +1,143 @@
+# Execution Pipeline
+
+処理系は、source を AST に変換し、必要な値だけを AST interpreter で評価する。
+
+```text
+source
+  ↓
+lexer / parser
+  ↓
+desugar
+  ↓
+register root module
+  ↓
+demand-driven evaluation
+  ├─ force thunk
+  ├─ load imported module on demand
+  ├─ evaluate expression
+  ├─ compose `&`
+  └─ patch `//`
+  ↓
+materialize
+  ↓
+data / diagnostics
+```
+
+## lexer / parser
+
+lexer / parser は source を AST に変換する。
+構文エラーはこの段階で diagnostic として報告する。
+
+AST は arena に格納し、式や pattern は `ExprId`、`PatternId` のような ID で参照する。
+
+## desugar
+
+desugar は、意味論を単純にするための表層構文変換を行う。
+
+例として、dot-path field は nested object に変換できる。
+
+```dcdl
+{
+    feature_hoge.enable = false;
+}
+```
+
+```dcdl
+{
+    feature_hoge = {
+        enable = false;
+    };
+}
+```
+
+この変換により、評価器は object field の再帰構造だけを扱えばよい。
+
+## module registry
+
+module registry は、読み込んだ module を canonical path で管理する。
+
+```text
+ModuleRegistry:
+  CanonicalPath -> ModuleId
+```
+
+処理系は、まず root module を parse / desugar して registry に登録する。
+import 先 module は、この段階で全て読み込む必要はない。
+
+import expression が評価されたとき、module registry は path を解決し、未登録なら対象 module を parse / desugar して登録する。
+登録された module は module root thunk を持つ。
+同じ module が複数回 import された場合は、同じ `ModuleId` を返す。
+
+つまり import は module を即時評価しない。
+module を読み込み、module root を thunk として登録するだけにする。
+
+## demand-driven evaluation
+
+評価器は、必要になった thunk だけを force する。
+未参照の field、let binding、import 先の field は評価しない。
+
+この方式により、module 間に循環 import があっても、実際に force された thunk の依存が循環しない限り評価できる。
+
+## composition
+
+composition は、module 全体に後からかける global pass ではない。
+`&` や `//` の式を評価するときに、demand-driven evaluation の中で呼ばれる演算である。
+
+```text
+eval(A & B):
+  a = eval(A)
+  b = eval(B)
+  compose_and(a, b)
+
+eval(A // B):
+  a = eval(A)
+  b = eval(B)
+  patch(a, b)
+```
+
+`&` は制約を保った合成を行い、`//` は右辺優先の deep patch を行う。
+詳細は [Composition and Materialization](./composition-and-materialization.md) に置く。
+
+## resolver / binder
+
+resolver / binder は初期実装では必須ではない。
+評価時に environment lookup を行えば、識別子参照は実装できる。
+
+ただし、将来的には optional phase として追加できる余地を残す。
+
+```text
+source
+  ↓
+lexer / parser
+  ↓
+desugar
+  ↓
+resolver / binder
+  ↓
+register root module
+  ↓
+demand-driven evaluation
+```
+
+resolver / binder を追加すると、以下を早期に診断しやすくなる。
+
+- 未定義識別子
+- shadowing の扱い
+- reserved word の扱い
+- symbol interning
+- import path の一部静的解決
+- span 付き diagnostic の精度向上
+
+ただし、Decodal の制約検証は独立した type checking pass ではなく、`&` の合成時や materialize 時に行う。
+
+## materialize
+
+通常の評価結果は runtime value であり、抽象値や default を含みうる。
+外部へ出力するときだけ materialize を行い、出力可能な data に変換する。
+
+materialize は以下を行う。
+
+- 必要な thunk を force する。
+- abstract value の default を必要に応じて force する。
+- concrete value が constraint を満たすか検証する。
+- 未解決の abstract value、function value などを diagnostic にする。
diff --git a/doc/manual/souce/design/index.md b/doc/manual/souce/design/index.md
new file mode 100644
index 0000000..01f4563
--- /dev/null
+++ b/doc/manual/souce/design/index.md
@@ -0,0 +1,17 @@
+# 処理系設計
+
+この章では、言語仕様を実装するための処理系モデルを定義する。
+言語仕様そのものは [Language Specification](../language/index.md) に置き、この章では AST interpreter、遅延評価、thunk、runtime value、materialize の実装方針を扱う。
+
+## 方針
+
+初期処理系は AST interpreter として実装する。
+bytecode VM や JIT ではなく、AST を demand-driven に評価することで、遅延評価、循環参照、`default`、`&`、`//` の意味論を小さく実装する。
+
+## 構成
+
+1. [Execution Pipeline](./execution-pipeline.md)
+2. [Runtime Model](./runtime-model.md)
+3. [Thunk and Lazy Evaluation](./thunk-and-lazy-evaluation.md)
+4. [Composition and Materialization](./composition-and-materialization.md)
+5. [Diagnostics and Fallback](./diagnostics-and-fallback.md)
diff --git a/doc/manual/souce/design/runtime-model.md b/doc/manual/souce/design/runtime-model.md
new file mode 100644
index 0000000..b8aa7f3
--- /dev/null
+++ b/doc/manual/souce/design/runtime-model.md
@@ -0,0 +1,135 @@
+# Runtime Model
+
+処理系の評価結果は、具体値と抽象値を区別した runtime value として扱う。
+`value`、`constraints`、`default` を横並びに持つ構造にはしない。
+
+## RuntimeValue
+
+```text
+RuntimeValue =
+  Concrete(ConcreteValue)
+  Abstract(AbstractValue)
+```
+
+`Concrete` は明示的な値である。
+`Abstract` は、まだ具体値に確定していない制約付きの値である。
+
+## ConcreteValue
+
+```text
+ConcreteValue =
+  String(String)
+  Int(i64)
+  Float(f64)
+  Bool(bool)
+  Array(Vec<ThunkId>)
+  Object(ObjectValue)
+  Function(FunctionValue)
+```
+
+object は concrete structure として扱う。
+ただし、各 field の中身は concrete value でも abstract value でもよい。
+
+```text
+ObjectValue:
+  fields: Map<Symbol, ThunkId>
+```
+
+例えば以下の schema object は、object 自体は concrete だが、field の値は abstract value になる。
+
+```dcdl
+MyConfig = {
+    host = String;
+    port = Int default 8080;
+};
+```
+
+概念的には以下である。
+
+```text
+Concrete(Object {
+  host -> Thunk(Abstract { constraints: [String], default: none })
+  port -> Thunk(Abstract { constraints: [Int], default: 8080 })
+})
+```
+
+## AbstractValue
+
+```text
+AbstractValue {
+  constraints: Vec<Constraint>
+  default: Option<ThunkId>
+}
+```
+
+`default` は `AbstractValue` にだけ存在する。
+明示的な concrete value がある場合、default は保持しない。
+
+```dcdl
+port = Int default 8080;
+```
+
+これは以下の runtime value になる。
+
+```text
+Abstract {
+  constraints: [Type(Int)]
+  default: Some(Thunk(8080))
+}
+```
+
+```dcdl
+port = 8000;
+```
+
+これは以下である。
+
+```text
+Concrete(Int(8000))
+```
+
+## Constraint
+
+constraint は concrete value とは別の型として扱う。
+
+```text
+Constraint =
+  Type(PrimitiveType)
+  Compare(Op, Literal)
+  Regex(Pattern)
+  BuiltinPredicate(Symbol)
+  ObjectConstraint(...)
+```
+
+初期実装では、object の形は主に `Concrete(Object)` の field に `Abstract` を置くことで表現する。
+object 全体にかかる constraint は必要になった時点で追加する。
+
+## Data
+
+materialize 後の出力可能な値は runtime value とは別型にする。
+
+```text
+Data =
+  String(String)
+  Int(i64)
+  Float(f64)
+  Bool(bool)
+  Array(Vec<Data>)
+  Object(Map<Symbol, Data>)
+```
+
+`Function`、未解決の `Abstract`、未評価の thunk は `Data` にはならない。
+
+## 命名
+
+実装内部では `RuntimeValue` を短く `Value` と呼んでもよい。
+ただし、materialize 後の出力値とは区別する。
+
+推奨する区別:
+
+```text
+RuntimeValue / Value  言語内部の評価結果。Abstract を含む。
+ConcreteValue         明示的な具体値。
+AbstractValue         constraint と default を持つ抽象値。
+Data                  外部へ出力可能な最終データ。
+```
diff --git a/doc/manual/souce/design/thunk-and-lazy-evaluation.md b/doc/manual/souce/design/thunk-and-lazy-evaluation.md
new file mode 100644
index 0000000..e8ba6a5
--- /dev/null
+++ b/doc/manual/souce/design/thunk-and-lazy-evaluation.md
@@ -0,0 +1,82 @@
+# Thunk and Lazy Evaluation
+
+thunk は、まだ評価していない式をあとで評価できるように包んだ遅延計算である。
+この処理系では、循環検出と memoize の単位として thunk を使う。
+
+## Thunk
+
+```text
+Thunk {
+  expr: ExprId
+  env: EnvId
+  state: ThunkState
+}
+
+ThunkState =
+  Unevaluated
+  Evaluating
+  Evaluated(RuntimeValue)
+  Error(Diagnostic)
+```
+
+`expr` は評価対象の AST node を指す。
+`env` は、その式を評価するときに使う lexical environment を指す。
+
+式だけではなく environment も保持するのは、遅延評価された式が定義時の名前解決文脈を必要とするためである。
+
+## force
+
+thunk を評価する操作を force と呼ぶ。
+
+```text
+force(thunk):
+  Unevaluated -> Evaluating -> Evaluated(value)
+  Evaluated(value) -> value
+  Evaluating -> cycle diagnostic
+  Error(diagnostic) -> diagnostic
+```
+
+一度 `Evaluated` になった thunk は memoize される。
+同じ thunk を複数回 force しても、式は一度だけ評価される。
+
+## 循環検出
+
+評価中の thunk を再度 force しようとした場合は循環依存である。
+
+```dcdl
+{
+    a = b;
+    b = a;
+}
+```
+
+`a` を force すると、`a -> b -> a` と戻る。
+このとき `a` は `Evaluating` なので cycle diagnostic を返す。
+
+## 遅延評価の単位
+
+thunk は主に以下に使う。
+
+- module root
+- object field
+- let binding
+- function argument
+- default expression
+
+object は field ごとに thunk を持つ。
+そのため、object の一部だけが必要な場合、他の field は評価されない。
+
+## module import
+
+import は module を登録するが、module 全体を即時評価しない。
+module root や field は thunk として保持され、参照されたときだけ force される。
+
+これにより、module 間に循環 import があっても、force された thunk の依存が循環しなければ評価できる。
+
+## function call
+
+関数引数は thunk として関数の environment に束縛する。
+関数本体で引数が参照されたときだけ force する。
+
+任意の関数呼び出し結果をグローバルに memoize する必要はない。
+field に束縛された関数呼び出し結果は、その field thunk の評価結果として memoize される。