diff --git a/src/mir/loop_canonicalizer/skeleton_types.rs b/src/mir/loop_canonicalizer/skeleton_types.rs index 484adc7a..8cd32f77 100644 --- a/src/mir/loop_canonicalizer/skeleton_types.rs +++ b/src/mir/loop_canonicalizer/skeleton_types.rs @@ -65,7 +65,46 @@ pub enum UpdateKind { /// Constant step (`i = i + const`) ConstStep { delta: i64 }, - /// Conditional step with numeric deltas (`if escape { i = i + 2 } else { i = i + 1 }`) + /// Conditional step with numeric deltas + /// + /// # Pattern + /// + /// ```text + /// if escape_cond { carrier = carrier + then_delta } + /// else { carrier = carrier + else_delta } + /// ``` + /// + /// # Contract (SSOT - Phase 92 P0) + /// + /// ## Invariants (MUST hold, Fail-Fast otherwise): + /// 1. **Single Update**: Updates the same carrier exactly once per iteration + /// 2. **Constant Deltas**: Both `then_delta` and `else_delta` are compile-time constants + /// 3. **Pure Condition**: The escape condition has no side effects + /// 4. **No Reassignment**: Carrier is not reassigned elsewhere in the loop body + /// 5. **Deterministic**: Update path is determined solely by escape condition + /// + /// ## Supported Use Cases: + /// - Escape sequence handling (e.g., `if ch == '\\' { i += 2 } else { i += 1 }`) + /// - Conditional skip patterns (e.g., `if skip { pos += len } else { pos += 1 }`) + /// + /// ## Fail-Fast Conditions: + /// - Multiple updates to the same carrier in one iteration → Error + /// - Non-constant deltas (e.g., `i += f()`) → Error + /// - Condition with side effects (e.g., `if mutate() { ... }`) → Error + /// - Carrier reassignment in body (e.g., `carrier = 0`) → Error + /// + /// # Phase 92 P0: Lowering Strategy + /// + /// Pattern2Break handles ConditionalStep by generating: + /// ```text + /// if escape_cond { + /// carrier_new = carrier + then_delta + /// } else { + /// carrier_new = carrier + else_delta + /// } + /// // PHI merge at loop header: carrier_phi = phi [init, carrier_new] + /// ``` + /// /// Phase 91 P5b: Used for escape sequence handling and similar conditional increments ConditionalStep { then_delta: i64, else_delta: i64 },