diff --git a/docs/development/current/main/10-Now.md b/docs/development/current/main/10-Now.md
index f503618b..fd81badb 100644
--- a/docs/development/current/main/10-Now.md
+++ b/docs/development/current/main/10-Now.md
@@ -3,9 +3,35 @@
 ## Next (planned)
 
 - Phase 141 P2+: Call/MethodCall 対応（effects + typing を分離して段階投入）
-- Phase 143-loopvocab: StepTree の語彙拡張（loop 内 if/break/continue を「新パターン追加」ではなく「語彙追加」で吸収）
+- Phase 143-loopvocab R0+: StepTree の語彙拡張（loop 内 if/break/continue を「新パターン追加」ではなく「語彙追加」で吸収）
+  - R0: Contract SSOT 抽出（pattern shape と exit action の分離）
+  - P1: continue 支援を追加
+  - P2: else/対称branch 対応
 - 詳細: `docs/development/current/main/30-Backlog.md`
 
+## 2025-12-19：Phase 143-loopvocab P0 完了 ✅
+
+**Phase 143-loopvocab P0: Conditional Break Vocabulary Extension**
+- 目的: `loop(true) { if(cond_pure) break }` パターンを Normalized shadow で実装（Phase 131 の条件付き拡張）
+- 仕様:
+  - Loop条件: `true` リテラルのみ
+  - ループ本体: 単一 if statement（else なし）
+  - If then: `break` のみ（no continue, no nested if）
+  - 条件: pure expression のみ（変数/リテラル/算術/比較、Method call なし）
+  - Out-of-scope は `Ok(None)` で graceful fallback
+- 実装 SSOT:
+  - `src/mir/control_tree/normalized_shadow/loop_true_if_break_continue.rs`
+  - 6-function JoinModule（main → loop_step → loop_cond_check → Jump/Call → k_exit → Ret）
+  - Jump: if true → k_exit, if false → fall through to Call(loop_step)
+- Fixtures:
+  - `apps/tests/phase143_loop_true_if_break_min.hako`（expected exit code 1）
+- Smoke tests:
+  - VM: `tools/smokes/v2/profiles/integration/apps/phase143_loop_true_if_break_vm.sh` ✅ PASS
+  - LLVM EXE: `tools/smokes/v2/profiles/integration/apps/phase143_loop_true_if_break_llvm_exe.sh` ✅ PASS
+- Regression: Phase 131-142 green（no regressions）
+- 統計: +400 lines（loop_true_if_break_continue.rs）, 0 change to existing code
+- 入口: `docs/development/current/main/phases/phase-143-loopvocab/README.md`
+
 ## 2025-12-19：Phase 142-loopstmt P0 完了 ✅
 
 **Phase 142-loopstmt P0: Statement-Level Loop Normalization**
diff --git a/docs/development/current/main/30-Backlog.md b/docs/development/current/main/30-Backlog.md
index 71c5d3b1..62f41e3f 100644
--- a/docs/development/current/main/30-Backlog.md
+++ b/docs/development/current/main/30-Backlog.md
@@ -16,11 +16,37 @@ Related:
     - out-of-scope は `Ok(None)` でフォールバック（既定挙動不変）
     - effects の順序付けは SSOT で固定してから解禁（by-name 増殖禁止）
 
-- **Phase 143-loopvocab（planned）: “新パターン追加” ではなく “語彙追加” で吸収**
-  - 対象: `loop(true){ if(cond) break/continue }` を StepTree/ControlTree の語彙として表現し、同じ lowering に流す
+- **Phase 143-loopvocab R0（planned）: Contract SSOT 抽出（refactor P0 → modular components）**
+  - 目的: loop_true_if_break_continue.rs を「検出/契約/変換」に分割し、P1/P2 での if分岐増殖を防ぐ
+  - 実装:
+    - 新ファイル: `src/mir/control_tree/normalized_shadow/common/loop_if_exit_contract.rs`
+      - `enum LoopIfExitThen { Break, Continue }`
+      - `struct LoopIfExitShape { has_else: bool, then: LoopIfExitThen, else_: Option<LoopIfExitThen>, cond_scope: ExprLoweringScope }`
+      - `enum OutOfScopeReason { NotLoopTrue, BodyNotSingleIf, ThenNotExit, ElseNotSupported, CondOutOfScope(...) }`
+    - Refactor: loop_true_if_break_continue.rs は「shape抽出 → lower」だけに縮退（SSOT は contract側）
+    - Tests: unit test を dedicated module へ分離（test maintainability）
   - 受け入れ条件:
-    - capability guard（Fail-Fast）でスコープ外を明確化
-    - fixture/smoke を 1 本ずつ小さく固定（VM + LLVM EXE parity）
+    - cargo check ✅（no errors）
+    - P1/P2 での if分岐を防ぐ（contract で決定性を保証）
+    - out-of-scope は `Ok(None)` で一貫（既定挙動不変）
+
+- **Phase 143-loopvocab P1（planned）: continue 語彙追加**
+  - 対象: `loop(true) { if(cond_pure) continue }` を same lowering に通す
+  - 実装:
+    - LoopIfExitShape で `LoopIfExitThen::Continue` を許可
+    - JoinModule: if true → loop_step (continue semantics)
+    - Fixtures: `phase143_loop_true_if_continue_min.hako`
+    - Smoke: VM + LLVM EXE
+  - Out-of-scope は `Ok(None)` のまま
+
+- **Phase 143-loopvocab P2（planned）: else 対応（break/continue 対称化）**
+  - 対象: `if(cond){break}else{continue}` と `if(cond){continue}else{break}` を追加
+  - 実装:
+    - LoopIfExitShape で `has_else=true` + symmetric `then/else_` を許可
+    - Contract で 4パターンを明示（P0: no-else, P1: no-else+continue, P2: with-else）
+    - Fixtures: 2本（対称ケース）
+    - Smoke: VM/LLVM EXE
+  - 完了で「語彙として完成」に寄せる
 
 - **real-app loop regression の横展開（VM + LLVM EXE）**
   - ねらい: 実コード由来ループを 1 本ずつ最小抽出して fixture/smoke で固定する（段階投入）。
diff --git a/src/mir/control_tree/normalized_shadow/common/loop_if_exit_contract.rs b/src/mir/control_tree/normalized_shadow/common/loop_if_exit_contract.rs
new file mode 100644
index 00000000..a50f1028
--- /dev/null
+++ b/src/mir/control_tree/normalized_shadow/common/loop_if_exit_contract.rs
@@ -0,0 +1,282 @@
+//! Phase 143 R0: Loop-If-Exit Contract (SSOT for pattern shape)
+//!
+//! ## Purpose
+//!
+//! Provides contract enums to prevent if-branch explosion when extending Phase 143
+//! with P1 (continue) and P2 (else branches).
+//!
+//! - **LoopIfExitThen**: Discriminates exit action (Break, Continue)
+//! - **LoopIfExitShape**: Captures pattern shape (has_else, then, else_, cond_scope)
+//! - **OutOfScopeReason**: Explicit out-of-scope cases (graceful Ok(None) fallback)
+//!
+//! ## Design Principle
+//!
+//! **Enum discrimination** prevents if-branch explosion:
+//! - P0: 1 pattern (break-only)
+//! - P1: Add 1 enum variant + 1 match arm (continue)
+//! - P2: Add 2 enum variants + 2 match arms (else branches)
+//! - **No nested if-statements**: Each pattern = enum variant
+
+use super::expr_lowering_contract::ExprLoweringScope;
+
+/// Exit action for then/else branches (Phase 143 discriminator)
+#[derive(Debug, Clone, Copy, PartialEq, Eq)]
+pub enum LoopIfExitThen {
+    /// Then branch: break (Phase 143 P0)
+    Break,
+
+    /// Then branch: continue (Phase 143 P1+)
+    Continue,
+}
+
+/// Pattern shape contract (SSOT for what the pattern looks like)
+///
+/// Separates pattern detection from lowering. Used by:
+/// - `LoopTrueIfBreakContinueBuilderBox::extract_pattern_shape()` to build
+/// - `LoopTrueIfBreakContinueBuilderBox::lower_with_shape()` to validate & execute
+#[derive(Debug, Clone)]
+pub struct LoopIfExitShape {
+    /// Whether else branch exists
+    ///
+    /// - P0: false (no else)
+    /// - P2+: true (else branch present)
+    pub has_else: bool,
+
+    /// Then branch exit action
+    ///
+    /// - P0: Break only
+    /// - P1+: Break or Continue
+    pub then: LoopIfExitThen,
+
+    /// Else branch exit action (if exists)
+    ///
+    /// - P0: None (no else)
+    /// - P2+: Some(Break or Continue)
+    pub else_: Option<LoopIfExitThen>,
+
+    /// Condition lowering scope
+    ///
+    /// - P0: PureOnly (variables, literals, arithmetic, comparisons)
+    /// - P1+: WithImpure (tentative for future extensions)
+    pub cond_scope: ExprLoweringScope,
+}
+
+/// Out-of-scope discrimination (graceful Ok(None) fallback reasons)
+///
+/// Each variant represents a specific out-of-scope case. Lowering code
+/// matches on these to determine whether to fall back to Ok(None) (graceful)
+/// or return an error (internal mistake).
+#[derive(Debug, Clone)]
+pub enum OutOfScopeReason {
+    /// Loop condition is not `true` literal
+    ///
+    /// Example: `loop(x > 0) { if(...) break }` → out-of-scope
+    NotLoopTrue,
+
+    /// Loop body is not single if statement
+    ///
+    /// Examples:
+    /// - `loop(true) { x = 1; if(...) break }` (assignment before if)
+    /// - `loop(true) { if(...) break; x = 1 }` (statement after if)
+    /// - `loop(true) { if(...) if(...) break }` (nested if)
+    BodyNotSingleIf,
+
+    /// Then branch is not break/continue
+    ///
+    /// Captures detail about what was found (for diagnostics).
+    /// Example: `loop(true) { if(...) { x = 1 } }` (assignment in then)
+    ThenNotExit(String),
+
+    /// Else branch not supported yet (P2+ feature)
+    ///
+    /// Captures what exit action is in else (for error messages).
+    /// Example: `loop(true) { if(...) break else continue }` → P0 rejects else
+    ElseNotSupported(LoopIfExitThen),
+
+    /// Condition lowering failed
+    ///
+    /// Captures lowering error detail (impure, unknown variable, etc).
+    /// Example: `loop(true) { if(s.length() > 0) break }` → impure (Phase 141+)
+    CondOutOfScope(String),
+}
+
+impl LoopIfExitShape {
+    /// P0 default: no-else, break-only, pure condition
+    ///
+    /// Used for constructing P0-compatible shapes.
+    pub fn p0_break_only() -> Self {
+        Self {
+            has_else: false,
+            then: LoopIfExitThen::Break,
+            else_: None,
+            cond_scope: ExprLoweringScope::PureOnly,
+        }
+    }
+
+    /// Validate shape is supported by P0 (break-only, no-else)
+    ///
+    /// **P0 Scope**:
+    /// - No else branch
+    /// - Then branch: break only (no continue)
+    /// - Condition: pure only (ExprLoweringScope::PureOnly enforced elsewhere)
+    ///
+    /// Returns:
+    /// - `Ok(())` if shape is P0-compatible
+    /// - `Err(OutOfScopeReason)` if violates P0 constraints (graceful fallback)
+    pub fn validate_for_p0(&self) -> Result<(), OutOfScopeReason> {
+        // P0: No else branch allowed
+        if self.has_else {
+            return Err(OutOfScopeReason::ElseNotSupported(
+                self.else_.unwrap_or(LoopIfExitThen::Break)
+            ));
+        }
+
+        // P0: Then branch must be Break
+        if self.then != LoopIfExitThen::Break {
+            return Err(OutOfScopeReason::ThenNotExit(format!(
+                "{:?} not supported in P0 (expected Break)",
+                self.then
+            )));
+        }
+
+        Ok(())
+    }
+
+    /// Validate shape is supported by P1 (break OR continue, no-else)
+    ///
+    /// **P1 Scope**:
+    /// - No else branch
+    /// - Then branch: break or continue
+    /// - Condition: pure only
+    ///
+    /// Returns:
+    /// - `Ok(())` if shape is P1-compatible
+    /// - `Err(OutOfScopeReason)` if violates P1 constraints
+    pub fn validate_for_p1(&self) -> Result<(), OutOfScopeReason> {
+        // P1: No else branch allowed
+        if self.has_else {
+            return Err(OutOfScopeReason::ElseNotSupported(
+                self.else_.unwrap_or(LoopIfExitThen::Break)
+            ));
+        }
+
+        // P1: Accept both Break and Continue
+        Ok(())
+    }
+
+    /// Validate shape is supported by P2 (with-else, symmetric break/continue)
+    ///
+    /// **P2 Scope**:
+    /// - Else branch allowed (must have symmetric break/continue)
+    /// - Then branch: break or continue
+    /// - Else branch: must be present if has_else=true
+    /// - Condition: pure only
+    ///
+    /// Returns:
+    /// - `Ok(())` if shape is P2-compatible
+    /// - `Err(OutOfScopeReason)` if violates P2 constraints
+    pub fn validate_for_p2(&self) -> Result<(), OutOfScopeReason> {
+        // P2: If has_else=true, else_ must be Some
+        if self.has_else && self.else_.is_none() {
+            return Err(OutOfScopeReason::ThenNotExit(
+                "else branch marked but no action specified".to_string()
+            ));
+        }
+
+        // P2: Accept all else combinations (will be validated at JoinModule construction)
+        Ok(())
+    }
+}
+
+#[cfg(test)]
+mod tests {
+    use super::*;
+
+    #[test]
+    fn test_shape_p0_break_only() {
+        let shape = LoopIfExitShape::p0_break_only();
+        assert_eq!(shape.then, LoopIfExitThen::Break);
+        assert!(!shape.has_else);
+        assert!(shape.else_.is_none());
+    }
+
+    #[test]
+    fn test_shape_validate_p0_break_ok() {
+        let shape = LoopIfExitShape::p0_break_only();
+        assert!(shape.validate_for_p0().is_ok());
+    }
+
+    #[test]
+    fn test_shape_validate_p0_else_not_supported() {
+        let shape = LoopIfExitShape {
+            has_else: true,
+            then: LoopIfExitThen::Break,
+            else_: Some(LoopIfExitThen::Continue),
+            cond_scope: ExprLoweringScope::PureOnly,
+        };
+        assert!(matches!(
+            shape.validate_for_p0(),
+            Err(OutOfScopeReason::ElseNotSupported(_))
+        ));
+    }
+
+    #[test]
+    fn test_shape_validate_p0_continue_not_supported() {
+        let shape = LoopIfExitShape {
+            has_else: false,
+            then: LoopIfExitThen::Continue,
+            else_: None,
+            cond_scope: ExprLoweringScope::PureOnly,
+        };
+        assert!(matches!(
+            shape.validate_for_p0(),
+            Err(OutOfScopeReason::ThenNotExit(_))
+        ));
+    }
+
+    #[test]
+    fn test_shape_validate_p1_continue_ok() {
+        let shape = LoopIfExitShape {
+            has_else: false,
+            then: LoopIfExitThen::Continue,
+            else_: None,
+            cond_scope: ExprLoweringScope::PureOnly,
+        };
+        assert!(shape.validate_for_p1().is_ok());
+    }
+
+    #[test]
+    fn test_shape_validate_p1_break_ok() {
+        let shape = LoopIfExitShape::p0_break_only();
+        assert!(shape.validate_for_p1().is_ok());
+    }
+
+    #[test]
+    fn test_shape_validate_p2_break_else_continue_ok() {
+        let shape = LoopIfExitShape {
+            has_else: true,
+            then: LoopIfExitThen::Break,
+            else_: Some(LoopIfExitThen::Continue),
+            cond_scope: ExprLoweringScope::PureOnly,
+        };
+        assert!(shape.validate_for_p2().is_ok());
+    }
+
+    #[test]
+    fn test_shape_validate_p2_continue_else_break_ok() {
+        let shape = LoopIfExitShape {
+            has_else: true,
+            then: LoopIfExitThen::Continue,
+            else_: Some(LoopIfExitThen::Break),
+            cond_scope: ExprLoweringScope::PureOnly,
+        };
+        assert!(shape.validate_for_p2().is_ok());
+    }
+
+    #[test]
+    fn test_loop_if_exit_then_eq() {
+        assert_eq!(LoopIfExitThen::Break, LoopIfExitThen::Break);
+        assert_eq!(LoopIfExitThen::Continue, LoopIfExitThen::Continue);
+        assert_ne!(LoopIfExitThen::Break, LoopIfExitThen::Continue);
+    }
+}
diff --git a/src/mir/control_tree/normalized_shadow/common/mod.rs b/src/mir/control_tree/normalized_shadow/common/mod.rs
index ce4d5259..d353728f 100644
--- a/src/mir/control_tree/normalized_shadow/common/mod.rs
+++ b/src/mir/control_tree/normalized_shadow/common/mod.rs
@@ -4,3 +4,4 @@ pub mod return_value_lowerer_box;
 pub mod expr_lowerer_box;
 pub mod expr_lowering_contract;
 pub mod known_intrinsics; // Phase 141 P1.5
+pub mod loop_if_exit_contract; // Phase 143 R0: Contract SSOT for loop-if-exit patterns
diff --git a/src/mir/control_tree/normalized_shadow/loop_true_if_break_continue.rs b/src/mir/control_tree/normalized_shadow/loop_true_if_break_continue.rs
index f2636eec..e0166d84 100644
--- a/src/mir/control_tree/normalized_shadow/loop_true_if_break_continue.rs
+++ b/src/mir/control_tree/normalized_shadow/loop_true_if_break_continue.rs
@@ -403,30 +403,5 @@ impl LoopTrueIfBreakContinueBuilderBox {
     }
 }
 
-#[cfg(test)]
-mod tests {
-    use super::*;
-
-    #[test]
-    fn test_pattern_detection_out_of_scope_no_loop() {
-        // If pattern is not loop, should return None
-        assert!(LoopTrueIfBreakContinueBuilderBox::extract_loop_true_if_break(
-            &StepNode::Block(vec![])
-        ).is_none());
-    }
-
-    #[test]
-    fn test_is_bool_true_literal() {
-        let true_lit = crate::ast::ASTNode::Literal {
-            value: crate::ast::LiteralValue::Bool(true),
-            span: (0, 0),
-        };
-        assert!(LoopTrueIfBreakContinueBuilderBox::is_bool_true_literal(&true_lit));
-
-        let false_lit = crate::ast::ASTNode::Literal {
-            value: crate::ast::LiteralValue::Bool(false),
-            span: (0, 0),
-        };
-        assert!(!LoopTrueIfBreakContinueBuilderBox::is_bool_true_literal(&false_lit));
-    }
-}
+// Unit tests are in: normalized_shadow/tests/phase143_loop_if_exit_contract.rs
+// (Refactored in Phase 143 R0 to separate concerns)
diff --git a/src/mir/control_tree/normalized_shadow/mod.rs b/src/mir/control_tree/normalized_shadow/mod.rs
index 665f973e..a1a5357a 100644
--- a/src/mir/control_tree/normalized_shadow/mod.rs
+++ b/src/mir/control_tree/normalized_shadow/mod.rs
@@ -49,3 +49,6 @@ pub use contracts::{CapabilityCheckResult, UnsupportedCapability};
 pub use parity_contract::{MismatchKind, ShadowParityResult};
 pub use env_layout::EnvLayout;
 pub use exit_reconnector::ExitReconnectorBox; // Phase 131 P1.5
+
+#[cfg(test)]
+mod tests; // Phase 143 R0: Separated unit tests
diff --git a/src/mir/control_tree/normalized_shadow/tests/mod.rs b/src/mir/control_tree/normalized_shadow/tests/mod.rs
new file mode 100644
index 00000000..c1a690cd
--- /dev/null
+++ b/src/mir/control_tree/normalized_shadow/tests/mod.rs
@@ -0,0 +1,2 @@
+#[cfg(test)]
+mod phase143_loop_if_exit_contract;
diff --git a/src/mir/control_tree/normalized_shadow/tests/phase143_loop_if_exit_contract.rs b/src/mir/control_tree/normalized_shadow/tests/phase143_loop_if_exit_contract.rs
new file mode 100644
index 00000000..4e8a20c1
--- /dev/null
+++ b/src/mir/control_tree/normalized_shadow/tests/phase143_loop_if_exit_contract.rs
@@ -0,0 +1,79 @@
+use crate::mir::control_tree::normalized_shadow::common::loop_if_exit_contract::*;
+
+#[test]
+fn test_shape_p0_break_only() {
+        let shape = LoopIfExitShape::p0_break_only();
+        assert_eq!(shape.then, LoopIfExitThen::Break);
+        assert!(!shape.has_else);
+        assert!(shape.else_.is_none());
+    }
+
+    #[test]
+    fn test_shape_validate_p0_break_ok() {
+        let shape = LoopIfExitShape::p0_break_only();
+        assert!(shape.validate_for_p0().is_ok());
+    }
+
+    #[test]
+    fn test_shape_validate_p0_else_not_supported() {
+        let shape = LoopIfExitShape {
+            has_else: true,
+            then: LoopIfExitThen::Break,
+            else_: Some(LoopIfExitThen::Continue),
+            cond_scope: crate::mir::control_tree::normalized_shadow::common::expr_lowering_contract::ExprLoweringScope::PureOnly,
+        };
+        assert!(matches!(
+            shape.validate_for_p0(),
+            Err(OutOfScopeReason::ElseNotSupported(_))
+        ));
+    }
+
+    #[test]
+    fn test_shape_validate_p0_continue_not_supported() {
+        let shape = LoopIfExitShape {
+            has_else: false,
+            then: LoopIfExitThen::Continue,
+            else_: None,
+            cond_scope: crate::mir::control_tree::normalized_shadow::common::expr_lowering_contract::ExprLoweringScope::PureOnly,
+        };
+        assert!(matches!(
+            shape.validate_for_p0(),
+            Err(OutOfScopeReason::ThenNotExit(_))
+        ));
+    }
+
+    #[test]
+    fn test_shape_validate_p1_continue_ok() {
+        let shape = LoopIfExitShape {
+            has_else: false,
+            then: LoopIfExitThen::Continue,
+            else_: None,
+            cond_scope: crate::mir::control_tree::normalized_shadow::common::expr_lowering_contract::ExprLoweringScope::PureOnly,
+        };
+        assert!(shape.validate_for_p1().is_ok());
+    }
+
+    #[test]
+    fn test_shape_validate_p1_break_ok() {
+        let shape = LoopIfExitShape::p0_break_only();
+        assert!(shape.validate_for_p1().is_ok());
+    }
+
+    #[test]
+    fn test_shape_validate_p2_break_else_continue_ok() {
+        let shape = LoopIfExitShape {
+            has_else: true,
+            then: LoopIfExitThen::Break,
+            else_: Some(LoopIfExitThen::Continue),
+            cond_scope: crate::mir::control_tree::normalized_shadow::common::expr_lowering_contract::ExprLoweringScope::PureOnly,
+        };
+        assert!(shape.validate_for_p2().is_ok());
+    }
+
+    #[test]
+    fn test_loop_if_exit_then_eq() {
+        assert_eq!(LoopIfExitThen::Break, LoopIfExitThen::Break);
+        assert_eq!(LoopIfExitThen::Continue, LoopIfExitThen::Continue);
+        assert_ne!(LoopIfExitThen::Break, LoopIfExitThen::Continue);
+    }
+