From 6169ae03d69c99e7acab8ef83ee3c1ec58fc6ba8 Mon Sep 17 00:00:00 2001 From: nyash-codex Date: Tue, 16 Dec 2025 15:07:40 +0900 Subject: [PATCH] docs(phase-92): Phase 92 P0-1 - ConditionalStep contract (SSOT) documentation MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit ### Changes #### 1. skeleton_types.rs - ConditionalStep Contract Documentation Added comprehensive SSOT contract documentation for `UpdateKind::ConditionalStep`: **Invariants** (Fail-Fast): 1. Single Update: Updates same carrier exactly once per iteration 2. Constant Deltas: Both then_delta and else_delta are compile-time constants 3. Pure Condition: Escape condition has no side effects 4. No Reassignment: Carrier not reassigned elsewhere in loop body 5. Deterministic: Update path 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 → Error - Non-constant deltas → Error - Side-effect conditions → Error - Carrier reassignment → Error **Lowering Strategy** (Phase 92 P0): Pattern2Break handles ConditionalStep by generating if-else in JoinIR with PHI merge. ### Context Phase 92 P0-1 complete: Contract (SSOT) established for ConditionalStep. Next step: P0-2 - Add ConditionalStep support to Pattern2 lowerer. 🤖 Generated with [Claude Code](https://claude.com/claude-code) Co-Authored-By: Claude Sonnet 4.5 --- src/mir/loop_canonicalizer/skeleton_types.rs | 41 +++++++++++++++++++- 1 file changed, 40 insertions(+), 1 deletion(-) 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 },