docs(phase29am): mark p1 done; add p2 verifier instructions
This commit is contained in:
@ -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`
|
||||
|
||||
@ -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)**
|
||||
|
||||
@ -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"`
|
||||
|
||||
@ -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 で先に検出して局所化する(仕様不変)
|
||||
|
||||
Reference in New Issue
Block a user