diff --git a/CURRENT_TASK.md b/CURRENT_TASK.md index f7eebf12..94ca3ee4 100644 --- a/CURRENT_TASK.md +++ b/CURRENT_TASK.md @@ -24,6 +24,9 @@ Scope: Repo root の旧リンク互換。現行の入口は `docs/development/cu **2025-12-29: Phase 29am P0 COMPLETE (CorePlan If/Exit lowerer/verifier)** CorePlan の If/Exit を lowerer/verifier で扱えるようにして、CorePlan 移行の土台を作った。 +**2025-12-29: Phase 29am P1 COMPLETE (CoreLoopPlan.body Seq flatten)** +CoreLoopPlan.body の `Seq([Effect...])` を再帰で flatten して emit できるようにした（Effect-only制約は維持）。 + **PlanRuleOrder SSOT** single_planner の順序/名前 SSOT は `src/mir/builder/control_flow/plan/single_planner/rule_order.rs` に固定。PlannerContext で Pattern1 facts の抑制を開始し、残りの guard/filter は段階移行。 diff --git a/docs/development/current/main/10-Now.md b/docs/development/current/main/10-Now.md index d87c750c..a7371a47 100644 --- a/docs/development/current/main/10-Now.md +++ b/docs/development/current/main/10-Now.md @@ -2,11 +2,16 @@ ## Current Focus: Phase 29am（CorePlan Step-A implementation） -Next: Phase 29am P1（Loop body Seq flatten） +Next: Phase 29am P2（Verifier: Loop.body Effect-only） 運用ルール: integration filter で phase143_* は回さない（JoinIR 回帰は phase29ae pack のみ） 運用ルール: phase286_pattern9_* は legacy pack (SKIP) を使う 移行道筋 SSOT: `docs/development/current/main/design/coreplan-migration-roadmap-ssot.md` +**2025-12-29: Phase 29am P1 完了** ✅ +- 目的: CoreLoopPlan.body で `Seq([Effect...])` を flatten して emit（Effect-only制約は維持） +- 変更: `src/mir/builder/control_flow/plan/lowerer.rs` +- 検証: `cargo build --release` / `./tools/smokes/v2/run.sh --profile quick` / `./tools/smokes/v2/profiles/integration/joinir/phase29ae_regression_pack_vm.sh` + **2025-12-29: Phase 29am P0 完了** ✅ - 目的: CorePlan の If/Exit を lowerer/verifier で扱えるようにして、CorePlan 移行の土台を作る（仕様不変） - 変更: `src/mir/builder/control_flow/plan/lowerer.rs` / `src/mir/builder/control_flow/plan/verifier.rs` diff --git a/docs/development/current/main/30-Backlog.md b/docs/development/current/main/30-Backlog.md index 8ac03d4a..97155a1d 100644 --- a/docs/development/current/main/30-Backlog.md +++ b/docs/development/current/main/30-Backlog.md @@ -38,7 +38,8 @@ Related: - **Phase 29am（candidate）: CorePlan Step-A implementation (lowerer/verifier)** - 入口: `docs/development/current/main/phases/phase-29am/README.md` - 状況: P0 ✅ 完了 - - Next: P1（Loop body Seq flatten） + - 状況: P0/P1 ✅ 完了 + - Next: P2（Verifier: Loop.body Effect-only） - Gate: `./tools/smokes/v2/profiles/integration/joinir/phase29ae_regression_pack_vm.sh` - **Phase 29ai（candidate）: Plan/Frag single-planner（Facts SSOT）** diff --git a/docs/development/current/main/phases/phase-29am/P2-VERIFY-CORELOOP-BODY-EFFECTONLY-INSTRUCTIONS.md b/docs/development/current/main/phases/phase-29am/P2-VERIFY-CORELOOP-BODY-EFFECTONLY-INSTRUCTIONS.md new file mode 100644 index 00000000..e6051566 --- /dev/null +++ b/docs/development/current/main/phases/phase-29am/P2-VERIFY-CORELOOP-BODY-EFFECTONLY-INSTRUCTIONS.md @@ -0,0 +1,60 @@ +--- +Status: Active +Scope: code（fail-fastの前倒し、仕様不変） +Related: +- docs/development/current/main/phases/phase-29am/README.md +- docs/development/current/main/design/effect-classification-ssot.md +- docs/development/current/main/design/exitkind-cleanup-effect-contract-ssot.md +--- + +# Phase 29am P2: Verify CoreLoopPlan.body is Effect-only (Seq flatten allowed) + +Date: 2025-12-29 +Status: Ready for execution +Scope: `CoreLoopPlan.body` の許可語彙を verifier で fail-fast（仕様不変） + +## Objective + +- `CoreLoopPlan.body` は “body_bb に emit できるものだけ” を許可する +- 許可語彙は最小（Effect-only）。ただし P1 により `Seq([Effect...])` は flatten して扱えるため許可 +- `If/Exit/Loop` が body に混入した場合、lowerer の実行時エラーではなく **PlanVerifier の局所エラー**で落とす + +## Non-goals + +- 既存のルーティング/観測の変更 +- `If/Exit` を body で扱う実装追加（branch/exit は Frag/ExitMap がSSOT） +- 新 env var / 恒常ログ追加 + +## Implementation + +### Step 1: PlanVerifier で Loop.body の語彙制約を追加 + +Target: +- `src/mir/builder/control_flow/plan/verifier.rs` + +Rule: +- Loop.body の各 item は + - `CorePlan::Effect(_)` または + - `CorePlan::Seq([Effect...])`（入れ子 Seq は再帰で検査） + のみ許可 +- それ以外が出たら Err（新しい invariant tag を追加してよい） + +### Step 2: unit tests + +Target: +- `src/mir/builder/control_flow/plan/verifier.rs` の tests + +Add (minimum): +- body に `Seq([Effect, Seq([Effect])])` が入っても verify OK +- body に `If` または `Exit` が入ったら verify Err + +## Verification + +- `cargo build --release` +- `./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 "phase29am(p2): verify core loop body effect-only"` + diff --git a/docs/development/current/main/phases/phase-29am/README.md b/docs/development/current/main/phases/phase-29am/README.md index 1b5896ca..ed038a8a 100644 --- a/docs/development/current/main/phases/phase-29am/README.md +++ b/docs/development/current/main/phases/phase-29am/README.md @@ -25,3 +25,8 @@ SSOT 道筋: `docs/development/current/main/design/coreplan-migration-roadmap-ss - 指示書: `docs/development/current/main/phases/phase-29am/P1-CORELOOP-BODY-SEQ-FLATTEN-INSTRUCTIONS.md` - ねらい: ループ body_bb では “Effect だけ” を前提にしつつ、`Seq([Effect...])` を安全に flatten して emit できるようにする - 非目的: `If/Exit` を body_bb に入れる（これは Frag/ExitMap 側の語彙で表現する） + +## P2: Verifier enforces Loop.body Effect-only (Seq flatten allowed) + +- 指示書: `docs/development/current/main/phases/phase-29am/P2-VERIFY-CORELOOP-BODY-EFFECTONLY-INSTRUCTIONS.md` +- ねらい: lowerer の “Non-Effect plan in Loop body” エラーを、PlanVerifier の fail-fast で先に検出して局所化する（仕様不変）