diff --git a/CURRENT_TASK.md b/CURRENT_TASK.md index 7e0bd898..7bbd19db 100644 --- a/CURRENT_TASK.md +++ b/CURRENT_TASK.md @@ -45,6 +45,9 @@ Pattern1/8 の候補抑制を planner 側に集約し、single_planner の Patte **2025-12-29: Phase 29al P0 COMPLETE (Skeleton/Feature model SSOT, docs-only)** CorePlan を骨格→特徴→合成で説明する SSOT を追加し、Freeze taxonomy に unstructured を追加。 +**2025-12-29: Phase 29al P1 COMPLETE (post-phi final form SSOT, docs-only)** +join 値（PHI相当）の最終表現（layout/mapping/pred分類/verify）を 1 枚 SSOT として固定。 + **2025-12-29: Phase 29aj P10 COMPLETE (single_planner unified shape)** single_planner を全パターンで planner-first → extractor フォールバックの共通形に統一（挙動不変）。 diff --git a/docs/development/current/main/10-Now.md b/docs/development/current/main/10-Now.md index 7c8cc882..3f106472 100644 --- a/docs/development/current/main/10-Now.md +++ b/docs/development/current/main/10-Now.md @@ -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` diff --git a/docs/development/current/main/30-Backlog.md b/docs/development/current/main/30-Backlog.md index b2162023..332baf8a 100644 --- a/docs/development/current/main/30-Backlog.md +++ b/docs/development/current/main/30-Backlog.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` diff --git a/docs/development/current/main/design/post-phi-final-form-ssot.md b/docs/development/current/main/design/post-phi-final-form-ssot.md new file mode 100644 index 00000000..acdbc2f2 --- /dev/null +++ b/docs/development/current/main/design/post-phi-final-form-ssot.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` + diff --git a/docs/development/current/main/phases/phase-29al/P1-POST-PHI-FINAL-FORM-SSOT-INSTRUCTIONS.md b/docs/development/current/main/phases/phase-29al/P1-POST-PHI-FINAL-FORM-SSOT-INSTRUCTIONS.md new file mode 100644 index 00000000..940c50ed --- /dev/null +++ b/docs/development/current/main/phases/phase-29al/P1-POST-PHI-FINAL-FORM-SSOT-INSTRUCTIONS.md @@ -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"` + diff --git a/docs/development/current/main/phases/phase-29al/README.md b/docs/development/current/main/phases/phase-29al/README.md index 4f86b8e0..c7ec83f1 100644 --- a/docs/development/current/main/phases/phase-29al/README.md +++ b/docs/development/current/main/phases/phase-29al/README.md @@ -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）を法典化する -