docs(phase29al): post-phi final form ssot
This commit is contained in:
@ -2,10 +2,14 @@
|
||||
|
||||
## Current Focus: Phase 29al(CorePlan composition hardening / docs-first)
|
||||
|
||||
Next: Phase 29al P1(post-phi final form SSOT)
|
||||
Next: Phase 29al P2(effect classification SSOT)
|
||||
運用ルール: integration filter で phase143_* は回さない(JoinIR 回帰は phase29ae pack のみ)
|
||||
運用ルール: phase286_pattern9_* は legacy pack (SKIP) を使う
|
||||
|
||||
**2025-12-29: Phase 29al P1 完了** ✅
|
||||
- 目的: join 値(PHI相当)の最終表現と局所 verify を SSOT 化(仕様不変)
|
||||
- SSOT: `docs/development/current/main/design/post-phi-final-form-ssot.md`
|
||||
|
||||
**2025-12-29: Phase 29al P0 完了** ✅
|
||||
- 目的: Skeleton/Feature model を SSOT 化し、「通らない/危険」形を Freeze taxonomy に落とす(仕様不変)
|
||||
- SSOT: `docs/development/current/main/design/coreplan-skeleton-feature-model.md`
|
||||
|
||||
@ -31,8 +31,8 @@ Related:
|
||||
|
||||
- **Phase 29al(candidate): CorePlan composition hardening (docs-first)**
|
||||
- 入口: `docs/development/current/main/phases/phase-29al/README.md`
|
||||
- 状況: P0 ✅ 完了(docs-only)
|
||||
- Next: P1(post-phi final form SSOT)/ P2(effect classification SSOT)
|
||||
- 状況: P0/P1 ✅ 完了(docs-only)
|
||||
- Next: P2(effect classification SSOT)
|
||||
|
||||
- **Phase 29ai(candidate): Plan/Frag single-planner(Facts SSOT)**
|
||||
- 入口: `docs/development/current/main/phases/phase-29ai/README.md`
|
||||
|
||||
@ -0,0 +1,87 @@
|
||||
---
|
||||
Status: SSOT
|
||||
Scope: JoinIR/PlanFrag の join 値(PHI 相当)の“最終表現”と局所検証(post-phi)
|
||||
Related:
|
||||
- docs/development/current/main/design/coreplan-skeleton-feature-model.md
|
||||
- docs/development/current/main/design/joinir-plan-frag-ssot.md
|
||||
- docs/development/current/main/design/edgecfg-fragments.md
|
||||
- docs/development/current/main/phases/phase-29ae/README.md
|
||||
---
|
||||
|
||||
# Post-PHI Final Form (SSOT)
|
||||
|
||||
目的: JoinIR/PlanFrag 導線における「pred 由来で値が変わる join」を、**局所的に検証できる最終表現**として固定し、emit/merge が再解析で穴埋めする余地を消す。
|
||||
|
||||
この文書で言う “post-phi” は、語として「PHI ノードを完全に排除した後」という意味ではない。
|
||||
ここでは **“PHI 相当の join 値” が最終的にどう表現され、どこで verify されるか**を SSOT 化する。
|
||||
|
||||
## 1. 用語
|
||||
|
||||
- join 値: predecessor によって値が変わる値(if/loop の merge 点で必要になる)
|
||||
- join 入力: pred → join 値の対応(どの pred がどの値を渡すか)
|
||||
- layout: join 入力の順序と名前(carrier 名)を固定する SSOT
|
||||
|
||||
## 2. SSOT: join 値は “対応表” と “順序” を必ず持つ
|
||||
|
||||
### 2.1 順序の SSOT
|
||||
|
||||
JoinIR merge では、carrier の順序は `BoundaryCarrierLayout` を SSOT とする。
|
||||
|
||||
- SSOT 実装: `src/mir/builder/control_flow/joinir/merge/boundary_carrier_layout.rs`
|
||||
- 入口の検証(strict/dev): boundary hygiene / header PHI layout checks
|
||||
|
||||
### 2.2 対応表の SSOT
|
||||
|
||||
JoinInlineBoundary は join の入力を明示で持つ(“暗黙の推論”は禁止)。
|
||||
|
||||
- SSOT データ: `JoinInlineBoundary::join_inputs`(名前/順序は layout と一致する)
|
||||
- 禁止: emit/merge が CFG/AST を覗いて join 入力を再推論すること
|
||||
|
||||
## 3. Invariants(局所 verify できる不変条件)
|
||||
|
||||
不変条件は「どこで落とすか」も含めて SSOT とする。
|
||||
|
||||
### 3.1 Layout 整合(入口で Fail-Fast)
|
||||
|
||||
- L1: `BoundaryCarrierLayout` の carrier 順序は一意で、同名が存在しない
|
||||
- L2: `boundary.join_inputs` の長さ/順序/名前が layout と一致する
|
||||
- L3: header PHI の順序が layout と一致する(LoopHeaderPhiInfo との整合)
|
||||
|
||||
検証:
|
||||
- `src/mir/builder/control_flow/joinir/merge/contract_checks/boundary_hygiene.rs`(strict/dev)
|
||||
- `src/mir/builder/control_flow/joinir/merge/contract_checks/header_phi_layout.rs`(strict/dev)
|
||||
|
||||
### 3.2 Pred 分類(entry vs latch)と値の流し先
|
||||
|
||||
Loop の join は “entry 値” と “latch 値” を混ぜない。
|
||||
|
||||
- P1: entry preds と latch preds を分類し、latch 側が初期値で上書きされない
|
||||
- P2: multi-pred join では、許可された条件(例: state の intersection 等)以外で initial を採用しない(曖昧さは Freeze/Fail-Fast)
|
||||
|
||||
検証:
|
||||
- merge の contract checks(strict/dev)
|
||||
- debug assertions(debug ビルド)
|
||||
|
||||
### 3.3 Header PHI の安全条件(debug_assertions)
|
||||
|
||||
Header PHI の dst は “他の命令 dst として再利用しない”。
|
||||
|
||||
検証:
|
||||
- `src/mir/builder/control_flow/joinir/merge/debug_assertions.rs`(debug_assertions)
|
||||
|
||||
## 4. “危険な失敗モード” と再発防止
|
||||
|
||||
### 4.1 一般 pattern が JoinIR 専用 pattern を飲み込む
|
||||
|
||||
例: nested loop(phase1883)が plan 側の一般 pattern に誤マッチし、JoinIR の dedicated lowerer が選ばれない。
|
||||
|
||||
SSOT ルール:
|
||||
- より一般な extractor は、上位形(nested loop 等)を構造条件で `Ok(None)` に倒す
|
||||
- 入口で by-name 特例を足さない(設計的に禁止)
|
||||
|
||||
## 5. Verification(SSOT)
|
||||
|
||||
JoinIR regression gate(VM):
|
||||
|
||||
- `./tools/smokes/v2/profiles/integration/joinir/phase29ae_regression_pack_vm.sh`
|
||||
|
||||
@ -0,0 +1,70 @@
|
||||
---
|
||||
Status: Active
|
||||
Scope: docs-first(仕様不変)
|
||||
Related:
|
||||
- docs/development/current/main/phases/phase-29al/README.md
|
||||
- docs/development/current/main/design/post-phi-final-form-ssot.md
|
||||
- docs/development/current/main/design/joinir-plan-frag-ssot.md
|
||||
- docs/development/current/main/phases/phase-29ae/README.md
|
||||
---
|
||||
|
||||
# Phase 29al P1: Post-PHI final form SSOT(docs-first)
|
||||
|
||||
Date: 2025-12-29
|
||||
Status: Ready for execution
|
||||
Scope: join 値(PHI 相当)の最終表現と局所 verify を SSOT 化する(仕様不変)
|
||||
|
||||
## Objective
|
||||
|
||||
- “pred によって値が変わる join” を、**暗黙推論なし**で表現できることを SSOT 化する
|
||||
- layout / mapping / pred 分類 / verify の責務境界を 1 枚に固定し、再解析や if 地獄の余地を消す
|
||||
|
||||
## Non-goals
|
||||
|
||||
- PHI の完全排除(これは別フェーズ)
|
||||
- 既存の error 文字列の変更
|
||||
- 新 env var 追加
|
||||
- 既定挙動の変更(release は不変)
|
||||
|
||||
## Steps
|
||||
|
||||
### Step 1: SSOT を 1 枚に固定
|
||||
|
||||
Add:
|
||||
- `docs/development/current/main/design/post-phi-final-form-ssot.md`
|
||||
|
||||
Must include:
|
||||
- “post-phi” の定義(ここでは PHI 排除ではなく、join 値の最終表現/verify の SSOT)
|
||||
- `BoundaryCarrierLayout` と `JoinInlineBoundary::join_inputs` の関係
|
||||
- 検証点(contract_checks / debug_assertions)の一覧
|
||||
- 危険な失敗モード(一般 pattern が専用 pattern を飲む)と SSOT ルール
|
||||
|
||||
### Step 2: 参照導線を追加
|
||||
|
||||
Update:
|
||||
- `docs/development/current/main/design/planfrag-ssot-registry.md`(SSOT 参照の追加)
|
||||
- 必要なら `docs/development/current/main/design/joinir-plan-frag-ssot.md` の “関連ドキュメント” に追加
|
||||
|
||||
### Step 3: Phase 入口を更新
|
||||
|
||||
Update:
|
||||
- `docs/development/current/main/phases/phase-29al/README.md` に P1 を追加(P0→P1 の流れを明確化)
|
||||
|
||||
### Step 4: Now/Backlog/CURRENT_TASK を更新
|
||||
|
||||
Update:
|
||||
- `docs/development/current/main/10-Now.md`(Current Focus と Next を更新)
|
||||
- `docs/development/current/main/30-Backlog.md`
|
||||
- `CURRENT_TASK.md`
|
||||
|
||||
## Verification
|
||||
|
||||
- docs-only のため `cargo build` は必須ではない
|
||||
- ただし Gate の SSOT を維持するため、次は任意で実行:
|
||||
- `./tools/smokes/v2/run.sh --profile quick`
|
||||
- `./tools/smokes/v2/profiles/integration/joinir/phase29ae_regression_pack_vm.sh`
|
||||
|
||||
## Commit
|
||||
|
||||
- `git add -A && git commit -m "docs(phase29al): post-phi final form ssot"`
|
||||
|
||||
@ -23,8 +23,9 @@ Goal: “pattern が重なる/増殖する” を設計で根治し、JoinIR/Pla
|
||||
### P1: post-phi(join 入力の最終表現)SSOT
|
||||
|
||||
- ねらい: join 値の “最終表現” と “局所 verify” の不変条件を SSOT 化する(emit/merge の再解析禁止を強化)
|
||||
- 指示書: `docs/development/current/main/phases/phase-29al/P1-POST-PHI-FINAL-FORM-SSOT-INSTRUCTIONS.md`
|
||||
- SSOT: `docs/development/current/main/design/post-phi-final-form-ssot.md`
|
||||
|
||||
### P2: effect classification SSOT
|
||||
|
||||
- ねらい: pure/control/rc/observability などの効果分類と、許される変形(最適化/RC挿入/DCE)を法典化する
|
||||
|
||||
|
||||
Reference in New Issue
Block a user