From 3995742b20fff67e4c36ca2dd9d30f837b6f2d52 Mon Sep 17 00:00:00 2001
From: Zack Maril <zmaril@users.noreply.github.com>
Date: Tue, 25 Aug 2026 15:21:06 +0000
Subject: [PATCH 1/3] Give repetition and exchange forms of their own
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

Three of seven hand-written sort spellings were opaque at the top, because a
`while` was raw syntax and described no work at all: a library function that
loops that way yielded no behavior. `Repeat` holds the construct, and a `loop`
is the same construct with its condition written inside as a `break` — so
`loop { if done { break } .. }` reduces to `while !done { .. }` and the two
spellings stop sharing nothing. A loop with a second way out keeps its shape,
because hoisting only the first test would claim it runs longer than it does.

`Swap` is the operation every naive sort is built from. `v.swap(i, j)` and the
three statements through a temporary are the same exchange and shared no
subterm; the corpus writes the second 131 times. The law is narrow — what is
saved must be what the first assignment overwrites, what that is overwritten
with must be what the second overwrites, and the temporary must be spent — so a
shift through three positions and a temporary read afterwards both decline.

With those, and with a group of one step reducing to that step, the two
spellings of a bubble sort reduce to ONE form. That is not sort detection and
should not be mistaken for it: what it means is that the shape space stopped
growing with the spelling.

Nothing already found changed: 11 and 30 on CodeNet, still zero on production
Rust. The normalizer moved under both and the findings did not.

Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_017ghYbUJFcVfkKYacbTVJsR
---
 crates/infact-normalize/src/lib.rs            |  55 +++++-
 crates/infact-normalize/src/matching.rs       |  30 ++++
 crates/infact-normalize/src/renaming.rs       |  13 ++
 crates/infact-normalize/src/simplify.rs       | 165 ++++++++++++++++++
 .../infact-rust-normalize/examples/census.rs  |   2 +
 .../infact-rust-normalize/examples/lower.rs   |  12 ++
 crates/infact-rust-normalize/src/lib.rs       |  38 ++++
 .../infact-rust-normalize/tests/normalize.rs  | 114 ++++++++++++
 8 files changed, 428 insertions(+), 1 deletion(-)

diff --git a/crates/infact-normalize/src/lib.rs b/crates/infact-normalize/src/lib.rs
index 079dc3e..de51cfa 100644
--- a/crates/infact-normalize/src/lib.rs
+++ b/crates/infact-normalize/src/lib.rs
@@ -233,6 +233,32 @@ pub enum Form {
         /// lets a reader of the form tell which they have.
         coverage: Coverage,
     },
+    /// Repeating a body for as long as a condition holds.
+    ///
+    /// A `while` and a `loop` are one construct: the second is the first with
+    /// the condition written inside as a `break`. Held as syntax they were two,
+    /// and neither described work, so a library function that loops this way
+    /// yielded no behavior at all.
+    ///
+    /// Distinct from [`Form::Traverse`], which walks something. A repetition
+    /// has no sequence — what it visits, if anything, is whatever its body
+    /// advances. Where that is a counted index, simplification turns the whole
+    /// thing into the traversal it is written to be.
+    Repeat {
+        condition: Box<Form>,
+        body: Box<Form>,
+    },
+    /// Exchanging two of a sequence's elements.
+    ///
+    /// `v.swap(i, j)` and the three-line dance through a temporary are the same
+    /// operation, and held apart they share no subterm. This is the operation
+    /// every naive sort is built from, so a form that cannot say it cannot say
+    /// anything about one.
+    Swap {
+        sequence: Box<Form>,
+        left: Box<Form>,
+        right: Box<Form>,
+    },
     /// Producing a new sequence by transforming each element.
     Transform {
         sequence: Box<Form>,
@@ -480,6 +506,12 @@ impl Form {
             } => vec![sequence.as_ref(), initial.as_ref(), body.as_ref()],
             Self::Collect { sequence, .. } => vec![sequence.as_ref()],
             Self::Assign { target, value, .. } => vec![target.as_ref(), value.as_ref()],
+            Self::Repeat { condition, body } => vec![condition.as_ref(), body.as_ref()],
+            Self::Swap {
+                sequence,
+                left,
+                right,
+            } => vec![sequence.as_ref(), left.as_ref(), right.as_ref()],
             Self::Binary { left, right, .. } => vec![left.as_ref(), right.as_ref()],
             Self::Unary { value, .. } => vec![value.as_ref()],
             Self::Index { sequence, position } => vec![sequence.as_ref(), position.as_ref()],
@@ -667,6 +699,19 @@ impl Form {
                 left: apply(left),
                 right: apply(right),
             },
+            Self::Repeat { condition, body } => Self::Repeat {
+                condition: apply(condition),
+                body: apply(body),
+            },
+            Self::Swap {
+                sequence,
+                left,
+                right,
+            } => Self::Swap {
+                sequence: apply(sequence),
+                left: apply(left),
+                right: apply(right),
+            },
             Self::Unary { operator, value } => Self::Unary {
                 operator: operator.clone(),
                 value: apply(value),
@@ -740,7 +785,7 @@ impl Form {
             // Indexing names an operation the way a method call does. A span
             // names only a shape, so like a traversal it anchors nothing of its
             // own and is counted through its endpoints.
-            Self::Index { .. } => 1,
+            Self::Index { .. } | Self::Swap { .. } => 1,
             Self::Collect { container, .. } => u32::from(container.is_some()),
             // what the arms name is the whole content of a decision
             Self::Select { arms, .. } => arms.iter().map(|arm| arm.pattern.anchors()).sum(),
@@ -1032,6 +1077,8 @@ impl Form {
             | Self::Retain { .. }
             | Self::Accumulate { .. }
             | Self::Pairwise { .. }
+            | Self::Repeat { .. }
+            | Self::Swap { .. }
             | Self::Collect { .. } => true,
             _ => self.children().into_iter().any(Self::describes_work),
         }
@@ -1402,6 +1449,12 @@ impl Display for Form {
                 right,
             } => write!(formatter, "(binary {operator} {left} {right})"),
             Self::Unary { operator, value } => write!(formatter, "(unary {operator} {value})"),
+            Self::Repeat { condition, body } => write!(formatter, "(repeat {condition} {body})"),
+            Self::Swap {
+                sequence,
+                left,
+                right,
+            } => write!(formatter, "(swap {sequence} {left} {right})"),
             Self::Index { sequence, position } => {
                 write!(formatter, "(index {sequence} {position})")
             }
diff --git a/crates/infact-normalize/src/matching.rs b/crates/infact-normalize/src/matching.rs
index 1a20db5..305230d 100644
--- a/crates/infact-normalize/src/matching.rs
+++ b/crates/infact-normalize/src/matching.rs
@@ -655,6 +655,36 @@ impl Bindings {
             }
             (Form::Return(subject), Form::Return(pattern)) => self.form(subject, pattern),
             (Form::Sequence(subject), Form::Sequence(pattern)) => self.all(subject, pattern),
+            (
+                Form::Repeat {
+                    condition: subject_condition,
+                    body: subject_body,
+                },
+                Form::Repeat {
+                    condition: pattern_condition,
+                    body: pattern_body,
+                },
+            ) => {
+                self.form(subject_condition, pattern_condition)
+                    && (self.form(subject_body, pattern_body)
+                        || self.fused_body(subject_body, pattern_body))
+            }
+            (
+                Form::Swap {
+                    sequence: subject_sequence,
+                    left: subject_left,
+                    right: subject_right,
+                },
+                Form::Swap {
+                    sequence: pattern_sequence,
+                    left: pattern_left,
+                    right: pattern_right,
+                },
+            ) => {
+                self.form(subject_sequence, pattern_sequence)
+                    && self.form(subject_left, pattern_left)
+                    && self.form(subject_right, pattern_right)
+            }
             (
                 Form::Unary {
                     operator: subject_operator,
diff --git a/crates/infact-normalize/src/renaming.rs b/crates/infact-normalize/src/renaming.rs
index e8bf5a6..4b8fa33 100644
--- a/crates/infact-normalize/src/renaming.rs
+++ b/crates/infact-normalize/src/renaming.rs
@@ -196,6 +196,19 @@ impl Renaming {
                 left: self.boxed(left),
                 right: self.boxed(right),
             },
+            Form::Repeat { condition, body } => Form::Repeat {
+                condition: self.boxed(condition),
+                body: self.boxed(body),
+            },
+            Form::Swap {
+                sequence,
+                left,
+                right,
+            } => Form::Swap {
+                sequence: self.boxed(sequence),
+                left: self.boxed(left),
+                right: self.boxed(right),
+            },
             Form::Unary { operator, value } => Form::Unary {
                 operator: operator.clone(),
                 value: self.boxed(value),
diff --git a/crates/infact-normalize/src/simplify.rs b/crates/infact-normalize/src/simplify.rs
index 3322c06..1ac8f44 100644
--- a/crates/infact-normalize/src/simplify.rs
+++ b/crates/infact-normalize/src/simplify.rs
@@ -176,6 +176,9 @@ impl Form {
             .or_else(|| rebuilt.as_element_traversal())
             .or_else(|| rebuilt.as_pairwise())
             .or_else(|| rebuilt.as_adjacent_pairwise())
+            .or_else(|| rebuilt.as_swap())
+            .or_else(|| rebuilt.as_single_step())
+            .or_else(|| rebuilt.as_guarded_repeat())
             .or_else(|| rebuilt.as_recovered_escape())
             .or_else(|| rebuilt.as_unfolded(fuel))
             .unwrap_or(rebuilt)
@@ -480,6 +483,143 @@ impl Form {
             .or_else(|| Self::as_enumerated_pairwise(outer, first, inner, second, inner_body))
     }
 
+    /// A group of one step is that step.
+    ///
+    /// Braces are punctuation. A body that held one statement stayed a sequence
+    /// of one, so `{ v.swap(i, j) }` and `v.swap(i, j)` were different forms —
+    /// which is exactly the difference the two spellings of a bubble sort came
+    /// down to once the exchange itself was recognized.
+    fn as_single_step(&self) -> Option<Self> {
+        match self {
+            Self::Sequence(steps) => match steps.as_slice() {
+                [only] if !matches!(only, Self::Let { .. }) => Some(only.clone()),
+                _ => None,
+            },
+            _ => None,
+        }
+    }
+
+    /// Three statements through a temporary are an exchange.
+    ///
+    /// `let t = v[i]; v[i] = v[j]; v[j] = t;` is `v.swap(i, j)`, and it is how
+    /// the exchange is written wherever `swap` is not reached for — 131 files
+    /// in the corpus measured. The temporary must be read back exactly where
+    /// the second assignment puts it, and nothing else may use it, or the three
+    /// statements are moving values around rather than exchanging two.
+    fn as_swap(&self) -> Option<Self> {
+        let Self::Sequence(steps) = self else {
+            return None;
+        };
+        for (index, window) in steps.windows(3).enumerate() {
+            let [
+                Self::Let {
+                    pattern,
+                    value: saved,
+                },
+                Self::Assign {
+                    operator: first_operator,
+                    target: first_target,
+                    value: first_value,
+                },
+                Self::Assign {
+                    operator: second_operator,
+                    target: second_target,
+                    value: second_value,
+                },
+            ] = window
+            else {
+                continue;
+            };
+            let Pattern::Binding(temporary) = pattern.as_ref() else {
+                continue;
+            };
+            if first_operator != "=" || second_operator != "=" {
+                continue;
+            }
+            // What was saved is what the first assignment overwrites, what it
+            // is overwritten with is what the second assignment overwrites, and
+            // the second is given back the saved value. Anything else is not a
+            // two-element exchange.
+            if saved.as_ref() != first_target.as_ref()
+                || first_value.as_ref() != second_target.as_ref()
+                || **second_value != Self::Local(*temporary)
+            {
+                continue;
+            }
+            let (Some((sequence, left)), Some((other, right))) = (
+                indexed_position(first_target),
+                indexed_position(second_target),
+            ) else {
+                continue;
+            };
+            if sequence != other {
+                continue;
+            }
+            // A temporary that outlives the exchange is holding a value for
+            // something else too, and dropping it would drop that.
+            let mut rest = steps.to_vec();
+            let exchange = Self::Swap {
+                sequence: Box::new(sequence.clone()),
+                left: Box::new(left.clone()),
+                right: Box::new(right.clone()),
+            };
+            rest.splice(index..index + 3, [exchange]);
+            if rest.iter().any(|step| step.references_local(*temporary)) {
+                continue;
+            }
+            return Some(Self::Sequence(rest));
+        }
+        None
+    }
+
+    /// A repetition that tests for its own end is a repetition with a guard.
+    ///
+    /// `loop { if done { break } .. }` and `while !done { .. }` are the same
+    /// loop, and the first is how it gets written when the test is awkward to
+    /// put at the top. Reducing one to the other is what stops the two
+    /// spellings of a hand-rolled sort from sharing nothing.
+    fn as_guarded_repeat(&self) -> Option<Self> {
+        let Self::Repeat { condition, body } = self else {
+            return None;
+        };
+        // Only a repetition that has no guard yet, or the rewrite would be
+        // discarding one.
+        if **condition != Self::Constant("true".to_owned()) {
+            return None;
+        }
+        let Self::Sequence(steps) = body.as_ref() else {
+            return None;
+        };
+        let (guard, rest) = steps.split_first()?;
+        let Self::Branch {
+            condition: test,
+            consequence,
+            alternative: None,
+        } = guard
+        else {
+            return None;
+        };
+        if !matches!(consequence.as_ref(), Self::Opaque { kind, .. } if kind == "break_expression")
+        {
+            return None;
+        }
+        // A `break` further in would leave for another reason, and hoisting
+        // only the first test would say the loop runs longer than it does.
+        if rest.iter().any(leaves_a_loop) {
+            return None;
+        }
+        Some(Self::Repeat {
+            condition: Box::new(Self::Unary {
+                operator: "!".to_owned(),
+                value: test.clone(),
+            }),
+            body: Box::new(match rest {
+                [only] => only.clone(),
+                _ => Self::Sequence(rest.to_vec()),
+            }),
+        })
+    }
+
     /// A single loop reading each element and the one after it.
     ///
     /// `for i in 0..v.len() - 1 { .. v[i] .. v[i + 1] .. }` is the `windows(2)`
@@ -1084,6 +1224,31 @@ fn one_more_than(form: &Form) -> Option<Form> {
     }
 }
 
+/// The sequence and position an indexing reads.
+fn indexed_position(form: &Form) -> Option<(&Form, &Form)> {
+    match form {
+        Form::Index { sequence, position } => Some((sequence.as_ref(), position.as_ref())),
+        _ => None,
+    }
+}
+
+/// Whether a step can leave the loop around it.
+///
+/// A `break` nested inside another loop belongs to that one, so only the steps
+/// this loop runs directly are asked.
+fn leaves_a_loop(form: &Form) -> bool {
+    match form {
+        Form::Opaque { kind, .. } if kind == "break_expression" => true,
+        Form::Repeat { .. }
+        | Form::Traverse { .. }
+        | Form::Pairwise { .. }
+        | Form::Transform { .. }
+        | Form::Retain { .. }
+        | Form::Sift { .. } => false,
+        _ => form.children().into_iter().any(leaves_a_loop),
+    }
+}
+
 /// Whether a form is one less than another.
 fn is_predecessor_of(form: &Form, of: &Form) -> bool {
     matches!(form, Form::Binary { operator, left, right }
diff --git a/crates/infact-rust-normalize/examples/census.rs b/crates/infact-rust-normalize/examples/census.rs
index b6c8d40..0a92562 100644
--- a/crates/infact-rust-normalize/examples/census.rs
+++ b/crates/infact-rust-normalize/examples/census.rs
@@ -65,6 +65,8 @@ fn variant(form: &Form) -> &'static str {
         Form::Assign { .. } => "Assign",
         Form::Binary { .. } => "Binary",
         Form::Unary { .. } => "Unary",
+        Form::Repeat { .. } => "Repeat",
+        Form::Swap { .. } => "Swap",
         Form::Pairwise { .. } => "Pairwise",
         Form::Index { .. } => "Index",
         Form::Span { .. } => "Span",
diff --git a/crates/infact-rust-normalize/examples/lower.rs b/crates/infact-rust-normalize/examples/lower.rs
index 34ee269..054173d 100644
--- a/crates/infact-rust-normalize/examples/lower.rs
+++ b/crates/infact-rust-normalize/examples/lower.rs
@@ -258,6 +258,18 @@ fn lower(form: &Form, level: usize, guesses: &Guesses, names: &Names) -> String
             right,
         } => format!("({} {operator} {})", sub(left), sub(right)),
         Form::Unary { operator, value } => format!("{operator}{}", sub(value)),
+        Form::Repeat { condition, body } => format!(
+            "while {} {{\n{}{}\n{}}}",
+            sub(condition),
+            indent(level + 1),
+            lower(body, level + 1, guesses, names),
+            indent(level)
+        ),
+        Form::Swap {
+            sequence,
+            left,
+            right,
+        } => format!("{}.swap({}, {})", sub(sequence), sub(left), sub(right)),
         Form::Index { sequence, position } => format!("{}[{}]", sub(sequence), sub(position)),
         Form::Span {
             start,
diff --git a/crates/infact-rust-normalize/src/lib.rs b/crates/infact-rust-normalize/src/lib.rs
index b96f43d..8c19686 100644
--- a/crates/infact-rust-normalize/src/lib.rs
+++ b/crates/infact-rust-normalize/src/lib.rs
@@ -586,6 +586,31 @@ impl<'a> Normalizer<'a> {
                     right: Box::new(right),
                 }
             }
+            // `while c { b }` and `loop { b }` are one construct: a loop is a
+            // repetition whose condition is always met, and whatever ends it is
+            // written inside. Spelling that out here is what lets one law reach
+            // both.
+            "while_expression" => {
+                let condition = node
+                    .child_by_field_name("condition")
+                    .map_or(Form::Literal, |child| self.expression(child));
+                let body = node
+                    .child_by_field_name("body")
+                    .map_or(Form::Literal, |child| self.expression(child));
+                Form::Repeat {
+                    condition: Box::new(condition),
+                    body: Box::new(body),
+                }
+            }
+            "loop_expression" => {
+                let body = node
+                    .child_by_field_name("body")
+                    .map_or(Form::Literal, |child| self.expression(child));
+                Form::Repeat {
+                    condition: Box::new(Form::Constant("true".to_owned())),
+                    body: Box::new(body),
+                }
+            }
             // A dereference has already been peeled by `unwrap_noise`, so
             // whatever reaches here applies an operator that changes the value.
             "unary_expression" => {
@@ -900,6 +925,19 @@ impl<'a> Normalizer<'a> {
             let name = call.name.to_owned();
             let receiver = self.expression(peel_adapters(call.receiver, self.source));
             let arguments = self.arguments(node);
+            // Exchanging two elements is an operation, not a call that happens
+            // to be named `swap`. Written out through a temporary it is three
+            // statements, and a form that held one spelling as a method and the
+            // other as assignments could never see they were the same.
+            if name == "swap"
+                && let [left, right] = arguments.as_slice()
+            {
+                return Form::Swap {
+                    sequence: Box::new(receiver),
+                    left: Box::new(left.clone()),
+                    right: Box::new(right.clone()),
+                };
+            }
             return Form::Method {
                 name,
                 receiver: Box::new(receiver),
diff --git a/crates/infact-rust-normalize/tests/normalize.rs b/crates/infact-rust-normalize/tests/normalize.rs
index f744efb..5887707 100644
--- a/crates/infact-rust-normalize/tests/normalize.rs
+++ b/crates/infact-rust-normalize/tests/normalize.rs
@@ -822,3 +822,117 @@ fn adjacent_pairs_differ_from_every_pair() {
     );
     assert_ne!(adjacent, every);
 }
+
+/// An exchange written through a temporary is the exchange.
+///
+/// This is the difference the two spellings of a bubble sort came down to, and
+/// with it they reduce to one form.
+#[test]
+fn a_temporary_swap_agrees_with_the_method() {
+    let method = behavior_of(
+        "fn f(values: &mut [i32]) {
+             for i in 0..values.len() {
+                 for j in 0..values.len() - 1 - i {
+                     if values[j] > values[j + 1] { values.swap(j, j + 1); }
+                 }
+             }
+         }",
+        "f",
+    );
+    let temporary = behavior_of(
+        "fn f(values: &mut [i32]) {
+             for i in 0..values.len() {
+                 for j in 0..values.len() - 1 - i {
+                     if values[j] > values[j + 1] {
+                         let t = values[j];
+                         values[j] = values[j + 1];
+                         values[j + 1] = t;
+                     }
+                 }
+             }
+         }",
+        "f",
+    );
+    assert!(method.contains("(swap"), "{method}");
+    assert_eq!(method, temporary);
+}
+
+/// Moving values around is not exchanging two of them.
+#[test]
+fn a_shift_through_a_temporary_is_not_a_swap() {
+    let form = behavior_of(
+        "fn f(values: &mut [i32], i: usize, j: usize, k: usize) {
+             let t = values[i];
+             values[i] = values[j];
+             values[k] = t;
+         }",
+        "f",
+    );
+    assert!(!form.contains("(swap"), "{form}");
+}
+
+/// A temporary that is used again is not spent on the exchange.
+#[test]
+fn a_temporary_read_afterwards_is_not_a_swap() {
+    let form = behavior_of(
+        "fn f(values: &mut [i32], i: usize, j: usize) -> i32 {
+             let t = values[i];
+             values[i] = values[j];
+             values[j] = t;
+             t
+         }",
+        "f",
+    );
+    assert!(!form.contains("(swap"), "{form}");
+}
+
+/// A `loop` that tests for its own end is a `while`.
+#[test]
+fn a_loop_that_breaks_agrees_with_a_while() {
+    let broken = behavior_of(
+        "fn f(n: usize) -> usize {
+             let mut i = 0;
+             loop { if i >= n { break; } i += 1; }
+             i
+         }",
+        "f",
+    );
+    let guarded = behavior_of(
+        "fn f(n: usize) -> usize {
+             let mut i = 0;
+             while !(i >= n) { i += 1; }
+             i
+         }",
+        "f",
+    );
+    assert!(broken.contains("(repeat"), "{broken}");
+    assert_eq!(broken, guarded);
+}
+
+/// A loop with another way out is not just its first test.
+#[test]
+fn a_loop_with_a_second_break_keeps_its_shape() {
+    let form = behavior_of(
+        "fn f(n: usize, m: usize) -> usize {
+             let mut i = 0;
+             loop { if i >= n { break; } if i == m { break; } i += 1; }
+             i
+         }",
+        "f",
+    );
+    assert!(form.contains("(const true)"), "{form}");
+}
+
+/// A repetition describes work, so a library that loops has a behavior.
+#[test]
+fn a_repetition_is_comparable() {
+    let form = behavior_of(
+        "fn f(values: &mut Vec<i32>) -> i32 {
+             let mut total = 0;
+             while let Some(value) = values.pop() { total += value; }
+             total
+         }",
+        "f",
+    );
+    assert!(form.contains("(repeat"), "{form}");
+}

From 1f78c10be359a983dd59b056b511703cbe0ef3f4 Mon Sep 17 00:00:00 2001
From: Zack Maril <zmaril@users.noreply.github.com>
Date: Tue, 25 Aug 2026 17:01:55 +0000
Subject: [PATCH 2/3] Read a counter loop as the traversal it is written to be
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

`let mut i = 0; while i < n { .. ; i += 1 }` is `for i in 0..n`, and the two
shared nothing. This law only has to reach a walk over a span — the element
traversal law already takes it from there — so the `while` spelling now lands on
the identical form the `for` spelling does, and a `loop` with a leading `break`
reaches it through four laws in a row.

Unlike every other law here it is not local to a node: the span's START is in
the binding before the loop, not in the loop, so the two have to be seen
together and that means matching on the sequence they are steps of.

Where the step sits is part of what the loop visits, and writing that down found
a bug in the first version. Counting up, the increment goes last and the walk is
`a..n`. Counting down, the decrement goes FIRST — that is what keeps the index
inside the sequence, and it is how the loop is actually written — and the walk
is the same span the other way about. The other two placements visit different
spans and are refused rather than quietly given their sibling's. `rev` on a
sequence now flips a walk's direction too, which nothing produced before, so a
descending counter and a reversed range agree.

The side conditions all earn their place, each with a test: a step inside a
branch may not happen, a stride is not a span, a counter read afterwards is a
value the rewrite would delete, and a body that can move the limit is not
walking a fixed one. That last one has no effects to consult, so it asks what it
can — a name the limit depends on may be read and not assigned to, called on, or
swapped through — with one exemption that nested loops need: working the limit
out again is reading it, not changing it.

MEASURED, AND THE NUMBER IS ZERO. Across 727 CodeNet files the law absorbs no
repetitions at all: 590 forms hold one with the law and 590 without. The reason
is plain in what those loops are — 434 are `loop` with the exit deeper in, and
most of the rest are binary searches and two-pointer walks whose index jumps
rather than steps. In 575 functions of production Rust only 15 repetitions
survive and 13 of those are `while let`. Rust programmers write `for` when they
mean a counted loop, and reach for `while` precisely when `for` will not do.

The law is kept because it is correct, costs nothing, and a `while`-spelled
distinctness or sortedness check is now recognized where it was not — both
verified end to end. But it is not the unlock, and `while let` is where the
loops actually are.

Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_017ghYbUJFcVfkKYacbTVJsR
---
 crates/infact-normalize/src/simplify.rs       | 318 ++++++++++++++++++
 .../infact-rust-normalize/tests/normalize.rs  | 200 +++++++++++
 2 files changed, 518 insertions(+)

diff --git a/crates/infact-normalize/src/simplify.rs b/crates/infact-normalize/src/simplify.rs
index 1ac8f44..2f36cd5 100644
--- a/crates/infact-normalize/src/simplify.rs
+++ b/crates/infact-normalize/src/simplify.rs
@@ -177,6 +177,8 @@ impl Form {
             .or_else(|| rebuilt.as_pairwise())
             .or_else(|| rebuilt.as_adjacent_pairwise())
             .or_else(|| rebuilt.as_swap())
+            .or_else(|| rebuilt.as_counted_traversal())
+            .or_else(|| rebuilt.as_reversed_traversal())
             .or_else(|| rebuilt.as_single_step())
             .or_else(|| rebuilt.as_guarded_repeat())
             .or_else(|| rebuilt.as_recovered_escape())
@@ -483,6 +485,116 @@ impl Form {
             .or_else(|| Self::as_enumerated_pairwise(outer, first, inner, second, inner_body))
     }
 
+    /// A counter loop is the traversal of a span it is written to be.
+    ///
+    /// `let mut i = 0; while i < n { .. i .. ; i += 1 }` is `for i in 0..n`,
+    /// and until this ran they shared nothing: one walked a span, the other
+    /// repeated while a name compared small. This only has to reach
+    /// `Traverse` over a `Span` — [`Form::as_element_traversal`] already takes
+    /// a span walk that only ever indexes the rest of the way, so the `while`
+    /// spelling lands on the same form the `for` spelling does.
+    ///
+    /// Unlike every other law here this one is not local to a node. The span's
+    /// START is not in the loop; it is in the binding before it, so the two
+    /// have to be seen together and that means matching on the sequence they
+    /// are steps of.
+    fn as_counted_traversal(&self) -> Option<Self> {
+        let Self::Sequence(steps) = self else {
+            return None;
+        };
+        for (bound, step) in steps.iter().enumerate() {
+            let Self::Let {
+                pattern,
+                value: start,
+            } = step
+            else {
+                continue;
+            };
+            let Pattern::Binding(counter) = pattern.as_ref() else {
+                continue;
+            };
+            for (repeated, candidate) in steps.iter().enumerate().skip(bound + 1) {
+                // The counter must still hold what it was bound to when the
+                // loop starts, and must not outlive it: a `for` leaves no
+                // counter behind, so anything reading it afterwards would lose
+                // a value it depends on.
+                if steps[bound + 1..repeated]
+                    .iter()
+                    .chain(&steps[repeated + 1..])
+                    .any(|other| other.references_local(*counter))
+                {
+                    break;
+                }
+                let Some((limit, body, direction)) = counted_loop(candidate, *counter) else {
+                    continue;
+                };
+                if limit.references_local(*counter) || moves_the_limit(limit, &body) {
+                    continue;
+                }
+                let (from, to) = match direction {
+                    // Counting down from the binding to the limit walks the
+                    // same positions the other way about.
+                    Direction::Backward => (limit.clone(), start.as_ref().clone()),
+                    Direction::Forward => (start.as_ref().clone(), limit.clone()),
+                };
+                let walk = Self::Traverse {
+                    sequence: Box::new(Self::Span {
+                        start: Box::new(from),
+                        end: Box::new(to),
+                        inclusive: false,
+                    }),
+                    item: pattern.clone(),
+                    body: Box::new(body),
+                    direction,
+                };
+                let mut rewritten = steps.to_vec();
+                rewritten[repeated] = walk;
+                rewritten.remove(bound);
+                return Some(Self::Sequence(rewritten));
+            }
+        }
+        None
+    }
+
+    /// Walking a reversed sequence is walking it backwards.
+    ///
+    /// `for x in v.iter().rev()` and a loop counting down reach the elements in
+    /// the same order, and `Direction` exists to say so — but nothing produced
+    /// it, so a reversal stayed a method call on the sequence and the two
+    /// spellings shared nothing. Reversing twice is not reversing, so the flip
+    /// is a flip rather than an assignment.
+    fn as_reversed_traversal(&self) -> Option<Self> {
+        let Self::Traverse {
+            sequence,
+            item,
+            body,
+            direction,
+        } = self
+        else {
+            return None;
+        };
+        let Self::Method {
+            name,
+            receiver,
+            arguments,
+        } = sequence.as_ref()
+        else {
+            return None;
+        };
+        if name != "rev" || !arguments.is_empty() {
+            return None;
+        }
+        Some(Self::Traverse {
+            sequence: receiver.clone(),
+            item: item.clone(),
+            body: body.clone(),
+            direction: match direction {
+                Direction::Forward => Direction::Backward,
+                Direction::Backward => Direction::Forward,
+            },
+        })
+    }
+
     /// A group of one step is that step.
     ///
     /// Braces are punctuation. A body that held one statement stayed a sequence
@@ -1224,6 +1336,212 @@ fn one_more_than(form: &Form) -> Option<Form> {
     }
 }
 
+/// A repetition read as counting, with the limit and the body it leaves behind.
+///
+/// The test may be written either way round and either way up: `i < n`, `n > i`,
+/// and the `!(i >= n)` that a `loop` with a leading `break` reduces to are one
+/// test. Pushing negation through a comparison is NOT sound in general — under
+/// a partial order `!(a >= b)` and `a < b` differ, which is the whole content
+/// of `IncomparableElements` — but a counter that is stepped by one and used as
+/// a span bound is an integer, and integers are totally ordered. The licence
+/// comes from the context, so it is taken here and not in the arithmetic law.
+///
+/// WHERE the step sits is part of what the loop visits, and the two directions
+/// want it in opposite places. Counting up, `while i < n { .. ; i += 1 }` from
+/// `i = a` visits `a` through `n - 1`. Counting down, the decrement goes FIRST
+/// — `while i > a { i -= 1; .. }` from `i = b` visits `b - 1` through `a` —
+/// because that is what keeps the index inside the sequence, and it is how the
+/// loop is actually written. Both are then the span `a..b`, walked opposite
+/// ways.
+///
+/// The other two placements visit `a + 1..=n` and `a + 1..=b`, which are real
+/// loops and different spans, and are refused rather than quietly given the
+/// span their sibling has.
+///
+/// A step inside a branch may not happen at all, so the loop would visit
+/// something other than a span and might not finish.
+fn counted_loop(form: &Form, counter: u32) -> Option<(&Form, Form, Direction)> {
+    let Form::Repeat { condition, body } = form else {
+        return None;
+    };
+    let Form::Sequence(steps) = body.as_ref() else {
+        return None;
+    };
+    // Take the step from each end and let the operator say which one counts.
+    let (first, after) = steps.split_first()?;
+    let (last, before) = steps.split_last()?;
+    let (direction, rest) = match counter_step(first, counter) {
+        Some(Direction::Backward) => (Direction::Backward, after),
+        _ => match counter_step(last, counter) {
+            Some(Direction::Forward) => (Direction::Forward, before),
+            _ => return None,
+        },
+    };
+    // The direction decides which side of the test the counter belongs on: a
+    // loop counting up stops when it reaches the limit from below, one counting
+    // down when it reaches it from above. Reading the test without knowing
+    // which way the loop runs cannot tell `i < n` from `i > 0`.
+    let limit = counting_test(condition, counter, direction)?;
+    // Anything else that moves the counter changes how many times the loop
+    // runs, and the span would be claiming a trip count the code does not have.
+    let remaining = match rest {
+        [only] => only.clone(),
+        _ => Form::Sequence(rest.to_vec()),
+    };
+    if assigns_to(&remaining, counter) {
+        return None;
+    }
+    Some((limit, remaining, direction))
+}
+
+/// Which way a statement steps a counter, when that is all it does.
+///
+/// A stride is not a span: `Span` has no room to say "every second one", and
+/// walking it as though it did would claim a trip count the code has not got.
+fn counter_step(step: &Form, counter: u32) -> Option<Direction> {
+    let Form::Assign {
+        operator,
+        target,
+        value,
+    } = step
+    else {
+        return None;
+    };
+    if **target != Form::Local(counter) || **value != Form::Number("1".to_owned()) {
+        return None;
+    }
+    match operator.as_str() {
+        "+=" => Some(Direction::Forward),
+        "-=" => Some(Direction::Backward),
+        _ => None,
+    }
+}
+
+/// The limit a test compares a counter against, when it is one.
+///
+/// Four spellings per direction, and they are one test: the counter on either
+/// side, and the whole thing negated as a `loop` with a leading `break` reduces
+/// to. Pushing negation through a comparison is NOT sound in general — under a
+/// partial order `!(a >= b)` and `a < b` differ, which is the whole content of
+/// `IncomparableElements` — but a counter stepped by one and used as a span
+/// bound is an integer, and integers are totally ordered. The licence comes
+/// from the context, which is why it is taken here and not in the arithmetic
+/// law where it would reach every comparison.
+fn counting_test(condition: &Form, counter: u32, direction: Direction) -> Option<&Form> {
+    if let Form::Unary { operator, value } = condition
+        && operator == "!"
+    {
+        return match direction {
+            Direction::Forward => compared_against(value, counter, ">=", "<="),
+            Direction::Backward => compared_against(value, counter, "<=", ">="),
+        };
+    }
+    match direction {
+        Direction::Forward => compared_against(condition, counter, "<", ">"),
+        Direction::Backward => compared_against(condition, counter, ">", "<"),
+    }
+}
+
+/// What a counter is compared with, when the comparison is one of two shapes.
+///
+/// `left` is the operator wanted with the counter written first, `right` the
+/// one wanted with it written second. `i < n` and `n > i` are the same test.
+fn compared_against<'a>(
+    condition: &'a Form,
+    counter: u32,
+    left_operator: &str,
+    right_operator: &str,
+) -> Option<&'a Form> {
+    let Form::Binary {
+        operator,
+        left,
+        right,
+    } = condition
+    else {
+        return None;
+    };
+    let name = Form::Local(counter);
+    if operator == left_operator && **left == name {
+        return Some(right.as_ref());
+    }
+    if operator == right_operator && **right == name {
+        return Some(left.as_ref());
+    }
+    None
+}
+
+/// Whether anything here assigns to a name.
+fn assigns_to(form: &Form, local: u32) -> bool {
+    if let Form::Assign { target, .. } = form
+        && **target == Form::Local(local)
+    {
+        return true;
+    }
+    form.children()
+        .into_iter()
+        .any(|child| assigns_to(child, local))
+}
+
+/// Whether the body might change what the limit is measuring.
+///
+/// A `for` evaluates its range once; a `while` re-reads its test every time
+/// around. The two agree only when nothing in the loop can move the limit, and
+/// `while i < v.len() { v.push(x); i += 1 }` is exactly the case where they do
+/// not.
+///
+/// The form carries no effects, so this asks the question it can. A name the
+/// limit depends on may be READ — `total += n` is fine — and may not be
+/// assigned to, have a method called on it, or be swapped through, because any
+/// of those might be the one that moves it. That refuses some loops whose limit
+/// is in fact fixed, which is the side to be wrong on.
+fn moves_the_limit(limit: &Form, body: &Form) -> bool {
+    let mut names = Vec::new();
+    collect_names(limit, &mut names);
+    names.iter().any(|name| disturbs(body, name, limit))
+}
+
+fn collect_names(form: &Form, found: &mut Vec<Form>) {
+    if matches!(form, Form::Local(_) | Form::Free(_)) && !found.contains(form) {
+        found.push(form.clone());
+    }
+    for child in form.children() {
+        collect_names(child, found);
+    }
+}
+
+/// Whether a body does anything to a name beyond reading it.
+///
+/// Working out the limit again is reading it, not changing it. That exemption
+/// is what keeps a nested counter loop readable: the inner loop's own bound is
+/// `v.len()` too, and without it the outer loop would be told that measuring
+/// the sequence had moved it.
+fn disturbs(form: &Form, name: &Form, limit: &Form) -> bool {
+    if form == limit {
+        return false;
+    }
+    let touched = match form {
+        Form::Assign { target, .. } => mentions(target, name),
+        // A method might be `push`. Which ones move a sequence and which only
+        // read it is an effect question, and the form does not carry effects.
+        Form::Method { receiver, .. } => receiver.as_ref() == name,
+        Form::Swap { sequence, .. } => sequence.as_ref() == name,
+        _ => false,
+    };
+    touched
+        || form
+            .children()
+            .into_iter()
+            .any(|child| disturbs(child, name, limit))
+}
+
+fn mentions(form: &Form, name: &Form) -> bool {
+    form == name
+        || form
+            .children()
+            .into_iter()
+            .any(|child| mentions(child, name))
+}
+
 /// The sequence and position an indexing reads.
 fn indexed_position(form: &Form) -> Option<(&Form, &Form)> {
     match form {
diff --git a/crates/infact-rust-normalize/tests/normalize.rs b/crates/infact-rust-normalize/tests/normalize.rs
index 5887707..fed147c 100644
--- a/crates/infact-rust-normalize/tests/normalize.rs
+++ b/crates/infact-rust-normalize/tests/normalize.rs
@@ -936,3 +936,203 @@ fn a_repetition_is_comparable() {
     );
     assert!(form.contains("(repeat"), "{form}");
 }
+
+/// A counter loop is the traversal it is written to be.
+///
+/// Two laws compose to get here: the counter loop becomes a walk over a span,
+/// and a span walk that only ever indexes becomes a walk over the elements.
+#[test]
+fn a_counter_loop_agrees_with_a_for_loop() {
+    let counted = behavior_of(
+        "fn f(values: &[i32]) -> i32 {
+             let mut total = 0;
+             let mut i = 0;
+             while i < values.len() { total += values[i]; i += 1; }
+             total
+         }",
+        "f",
+    );
+    let direct = behavior_of(
+        "fn f(values: &[i32]) -> i32 {
+             let mut total = 0;
+             for i in 0..values.len() { total += values[i]; }
+             total
+         }",
+        "f",
+    );
+    assert_eq!(counted, direct);
+    assert!(!counted.contains("(repeat"), "{counted}");
+}
+
+/// A `loop` with a leading `break` reaches the same place.
+///
+/// Four laws in a row: the break becomes a guard, the guard's negation is read
+/// as the counting test, the counter loop becomes a span walk, and the span
+/// walk becomes an element walk.
+#[test]
+fn a_loop_with_a_break_agrees_with_a_for_loop() {
+    let broken = behavior_of(
+        "fn f(values: &[i32]) -> i32 {
+             let mut total = 0;
+             let mut i = 0;
+             loop { if i >= values.len() { break; } total += values[i]; i += 1; }
+             total
+         }",
+        "f",
+    );
+    let direct = behavior_of(
+        "fn f(values: &[i32]) -> i32 {
+             let mut total = 0;
+             for i in 0..values.len() { total += values[i]; }
+             total
+         }",
+        "f",
+    );
+    assert_eq!(broken, direct);
+}
+
+/// Counting down agrees with walking a reversed range.
+#[test]
+fn a_descending_counter_agrees_with_a_reversed_range() {
+    let counted = behavior_of(
+        "fn f(values: &[i32]) -> i32 {
+             let mut total = 0;
+             let mut i = values.len();
+             while i > 0 { i -= 1; total += values[i]; }
+             total
+         }",
+        "f",
+    );
+    let reversed = behavior_of(
+        "fn f(values: &[i32]) -> i32 {
+             let mut total = 0;
+             for i in (0..values.len()).rev() { total += values[i]; }
+             total
+         }",
+        "f",
+    );
+    assert_eq!(counted, reversed);
+    assert!(counted.contains("traverse-back"), "{counted}");
+}
+
+/// Walking backwards is not the same as walking forwards.
+#[test]
+fn a_reversed_walk_differs_from_a_forward_one() {
+    let forward = behavior_of("fn f(v: &[i32]) { for x in v.iter() { g(x); } }", "f");
+    let backward = behavior_of("fn f(v: &[i32]) { for x in v.iter().rev() { g(x); } }", "f");
+    assert_ne!(forward, backward);
+}
+
+/// Where the step sits decides which positions the loop visits.
+///
+/// Counting down with the decrement LAST visits `n` through `1`, not `n - 1`
+/// through `0`, so it is a different span and is refused rather than given the
+/// span its sibling has.
+#[test]
+fn a_descending_loop_that_steps_last_is_refused() {
+    let form = behavior_of(
+        "fn f(values: &[i32]) -> i32 {
+             let mut total = 0;
+             let mut i = values.len();
+             while i > 0 { total += values[i - 1]; i -= 1; }
+             total
+         }",
+        "f",
+    );
+    assert!(form.contains("(repeat"), "{form}");
+}
+
+/// A loop whose body can move the limit is not a walk over a fixed span.
+#[test]
+fn a_loop_that_changes_its_limit_is_refused() {
+    let form = behavior_of(
+        "fn f(values: &mut Vec<i32>) -> usize {
+             let mut i = 0;
+             while i < values.len() { values.push(1); i += 1; }
+             i
+         }",
+        "f",
+    );
+    assert!(form.contains("(repeat"), "{form}");
+}
+
+/// A counter something reads afterwards is not one a traversal may consume.
+#[test]
+fn a_counter_read_after_the_loop_is_refused() {
+    let form = behavior_of(
+        "fn f(values: &[i32]) -> usize {
+             let mut total = 0;
+             let mut i = 0;
+             while i < values.len() { total += values[i]; i += 1; }
+             i
+         }",
+        "f",
+    );
+    assert!(form.contains("(repeat"), "{form}");
+}
+
+/// A step that might not happen is not a span.
+#[test]
+fn a_conditional_step_is_refused() {
+    let form = behavior_of(
+        "fn f(values: &[i32]) -> i32 {
+             let mut total = 0;
+             let mut i = 0;
+             while i < values.len() { if values[i] > 0 { i += 1; } total += 1; }
+             total
+         }",
+        "f",
+    );
+    assert!(form.contains("(repeat"), "{form}");
+}
+
+/// A stride is not a span.
+#[test]
+fn a_stride_is_refused() {
+    let form = behavior_of(
+        "fn f(n: usize) -> usize {
+             let mut i = 0;
+             let mut total = 0;
+             while i < n { total += i; i += 2; }
+             total
+         }",
+        "f",
+    );
+    assert!(form.contains("(repeat"), "{form}");
+}
+
+/// Nested counter loops reach the same walk over pairs as nested `for` loops.
+///
+/// The inner loop's own bound is `values.len()` as well, so this only holds
+/// because working the limit out again counts as reading it.
+#[test]
+fn nested_counter_loops_agree_with_nested_for_loops() {
+    let counted = behavior_of(
+        "fn f(values: &[i32]) -> bool {
+             let mut i = 0;
+             while i < values.len() {
+                 let mut j = i + 1;
+                 while j < values.len() {
+                     if values[i] == values[j] { return false; }
+                     j += 1;
+                 }
+                 i += 1;
+             }
+             true
+         }",
+        "f",
+    );
+    let direct = behavior_of(
+        "fn f(values: &[i32]) -> bool {
+             for i in 0..values.len() {
+                 for j in i + 1..values.len() {
+                     if values[i] == values[j] { return false; }
+                 }
+             }
+             true
+         }",
+        "f",
+    );
+    assert_eq!(counted, direct);
+    assert!(counted.contains("(pairwise"), "{counted}");
+}

From f863dd1e8abd27a0b661dc6ab1e0f10ce88270a9 Mon Sep 17 00:00:00 2001
From: Zack Maril <zmaril@users.noreply.github.com>
Date: Tue, 25 Aug 2026 17:46:30 +0000
Subject: [PATCH 3/3] Read a drain as the walk it is, and give while-let its
 binding
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

`while let P = e { b }` is `loop { match e { P => b, _ => break } }` — not an
analogy, the desugaring the language performs — and writing it out that way
needs no new vocabulary. It also fixes something worse than a missing law: the
condition was normalized as an EXPRESSION, so the name the pattern binds came
out a free variable. A hole matching anything, where the body reads a binding.

On top of that, `as_drain`: taking from a container until it is empty reaches
every element exactly once, which is what walking it does. So
`while let Some(x) = queue.pop_front()` and `for x in queue` now reduce to one
form, and so does a hand-written `while let Some(x) = it.next()`.

Two refusals carry the law. A body that puts something back is not draining —
it is a worklist, and its elements are not the ones the container started with;
measured, that is the commoner shape by two to one, 1,353 against 583. And a
bare `pop` is not taken at all, because the name settles no order: it is the
last element of a `Vec` and the GREATEST of a `BinaryHeap`. That is not a corner
case here — of the 931 files draining with `pop`, 434 also use a `BinaryHeap` —
and calling a heap's drain a backward walk would report the opposite order,
which is the one thing `Direction` exists to prevent.

Measured on the population it is for: across 900 files that drain with
`pop_front`, `pop_back` or `next`, repetitions fall from 1,291 to 1,131. A
hundred and sixty loops that were opaque repetitions are now traversals, and
comparable to every `for` loop in the corpus. The counted-loop law absorbed
exactly none; this is where the loops were.

Findings unchanged either way: 11 and 30 on CodeNet, zero on production Rust.

Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_017ghYbUJFcVfkKYacbTVJsR
---
 crates/infact-normalize/src/simplify.rs       | 108 +++++++++++++++
 crates/infact-rust-normalize/src/lib.rs       |  47 +++++++
 .../infact-rust-normalize/tests/normalize.rs  | 123 ++++++++++++++++++
 3 files changed, 278 insertions(+)

diff --git a/crates/infact-normalize/src/simplify.rs b/crates/infact-normalize/src/simplify.rs
index 2f36cd5..0d9ad6d 100644
--- a/crates/infact-normalize/src/simplify.rs
+++ b/crates/infact-normalize/src/simplify.rs
@@ -180,6 +180,7 @@ impl Form {
             .or_else(|| rebuilt.as_counted_traversal())
             .or_else(|| rebuilt.as_reversed_traversal())
             .or_else(|| rebuilt.as_single_step())
+            .or_else(|| rebuilt.as_drain())
             .or_else(|| rebuilt.as_guarded_repeat())
             .or_else(|| rebuilt.as_recovered_escape())
             .or_else(|| rebuilt.as_unfolded(fuel))
@@ -684,6 +685,67 @@ impl Form {
         None
     }
 
+    /// Taking from a container until it is empty is walking it.
+    ///
+    /// `while let Some(x) = queue.pop_front() { .. }` reaches every element
+    /// exactly once and leaves the container empty, which is what `for x in
+    /// queue` does. The two shared nothing.
+    ///
+    /// Only methods whose order the name settles are taken. `pop_front` and
+    /// `pop_back` say which end on any container that has them; a bare `pop`
+    /// does not — it is the last element of a `Vec` and the GREATEST element of
+    /// a `BinaryHeap`, and the form carries no types to tell them apart. In the
+    /// corpus that is not a corner: of 931 files with a `while let Some(..) =
+    /// x.pop()`, 434 also use `BinaryHeap`. Calling a heap's drain a backward
+    /// walk would be reporting the opposite order, which is the one thing
+    /// `Direction` exists to prevent.
+    ///
+    /// A body that puts something back is not draining. That is the commoner
+    /// shape by two to one — a worklist, breadth-first search, a queue that
+    /// feeds itself — and the elements it visits are not the ones the container
+    /// started with.
+    fn as_drain(&self) -> Option<Self> {
+        let Self::Repeat { condition, body } = self else {
+            return None;
+        };
+        if **condition != Self::Constant("true".to_owned()) {
+            return None;
+        }
+        let Self::Select { scrutinee, arms } = body.as_ref() else {
+            return None;
+        };
+        let [taken, exhausted] = arms.as_slice() else {
+            return None;
+        };
+        // The other arm must do nothing but leave. Anything else happens when
+        // the container runs out, and a walk over the elements has nowhere to
+        // put it.
+        if !matches!(exhausted.pattern, Pattern::Ignored)
+            || !matches!(&exhausted.body, Self::Opaque { kind, .. } if kind == "break_expression")
+        {
+            return None;
+        }
+        let Pattern::Variant { name, parts } = &taken.pattern else {
+            return None;
+        };
+        let [item] = parts.as_slice() else {
+            return None;
+        };
+        if name != "Some" {
+            return None;
+        }
+        let (direction, container) = taking_method(scrutinee)?;
+        if disturbs_container(&taken.body, container) {
+            return None;
+        }
+        Some(Self::Traverse {
+            sequence: Box::new(container.clone()),
+            item: Box::new(item.clone()),
+            body: Box::new(taken.body.clone()),
+            direction,
+        })
+    }
+
     /// A repetition that tests for its own end is a repetition with a guard.
     ///
     /// `loop { if done { break } .. }` and `while !done { .. }` are the same
@@ -1509,6 +1571,52 @@ fn collect_names(form: &Form, found: &mut Vec<Form>) {
     }
 }
 
+/// The container a call takes an element from, and which end it takes from.
+///
+/// `next` is here because an iterator's is the whole of its contract and yields
+/// in order; `pop` is not, because the name settles no order.
+fn taking_method(scrutinee: &Form) -> Option<(Direction, &Form)> {
+    let Form::Method {
+        name,
+        receiver,
+        arguments,
+    } = scrutinee
+    else {
+        return None;
+    };
+    if !arguments.is_empty() {
+        return None;
+    }
+    let direction = match name.as_str() {
+        "pop_front" | "next" => Direction::Forward,
+        "pop_back" | "next_back" => Direction::Backward,
+        _ => return None,
+    };
+    Some((direction, receiver.as_ref()))
+}
+
+/// Whether a body reaches the container it is being handed elements from.
+///
+/// Putting something back makes the walk cover elements the container did not
+/// start with; measuring it mid-drain observes a state a walk over the elements
+/// never has. Both are asked as one question, because the form carries no
+/// effects and a method on the container could be either.
+fn disturbs_container(body: &Form, container: &Form) -> bool {
+    let touched = match body {
+        Form::Assign { target, .. } => mentions(target, container),
+        Form::Method { receiver, .. } => receiver.as_ref() == container,
+        Form::Swap { sequence, .. } | Form::Index { sequence, .. } => {
+            sequence.as_ref() == container
+        }
+        _ => false,
+    };
+    touched
+        || body
+            .children()
+            .into_iter()
+            .any(|child| disturbs_container(child, container))
+}
+
 /// Whether a body does anything to a name beyond reading it.
 ///
 /// Working out the limit again is reading it, not changing it. That exemption
diff --git a/crates/infact-rust-normalize/src/lib.rs b/crates/infact-rust-normalize/src/lib.rs
index 8c19686..0d7c10c 100644
--- a/crates/infact-rust-normalize/src/lib.rs
+++ b/crates/infact-rust-normalize/src/lib.rs
@@ -591,6 +591,19 @@ impl<'a> Normalizer<'a> {
             // written inside. Spelling that out here is what lets one law reach
             // both.
             "while_expression" => {
+                // `while let P = e { b }` is `loop { match e { P => b, _ =>
+                // break } }`, which is not an analogy but the desugaring the
+                // language performs. Written out it needs no vocabulary of its
+                // own, and — the point — the name the pattern binds becomes a
+                // binding. Left as a condition it was normalized as an
+                // EXPRESSION, so `x` came out a free variable: a hole matching
+                // anything rather than a name the body uses.
+                if let Some(condition) = node.child_by_field_name("condition")
+                    && condition.kind() == "let_condition"
+                    && let Some(repeated) = self.repeat_from_let(node, condition)
+                {
+                    return repeated;
+                }
                 let condition = node
                     .child_by_field_name("condition")
                     .map_or(Form::Literal, |child| self.expression(child));
@@ -793,6 +806,40 @@ impl<'a> Normalizer<'a> {
         ))
     }
 
+    /// `while let` as the loop around a decision that it is.
+    ///
+    /// Returns `None` when the pattern names no alternative — `while let (a, b)
+    /// = p` destructures rather than deciding, and it would never end.
+    fn repeat_from_let(&mut self, node: Node<'a>, condition: Node<'a>) -> Option<Form> {
+        let scrutinee = self.expression(condition.child_by_field_name("value")?);
+        let bound = self.bind_pattern(condition.child_by_field_name("pattern")?);
+        if !matches!(bound, Pattern::Variant { .. }) {
+            return None;
+        }
+        let taken = node
+            .child_by_field_name("body")
+            .map_or(Form::Literal, |child| self.expression(child));
+        Some(Form::Repeat {
+            condition: Box::new(Form::Constant("true".to_owned())),
+            body: Box::new(Form::select(
+                scrutinee,
+                vec![
+                    Arm {
+                        pattern: bound,
+                        body: taken,
+                    },
+                    Arm {
+                        pattern: Pattern::Ignored,
+                        body: Form::Opaque {
+                            kind: "break_expression".to_owned(),
+                            parts: Vec::new(),
+                        },
+                    },
+                ],
+            )),
+        })
+    }
+
     /// A `match`, as a decision among named alternatives.
     ///
     /// An arm with a guard is left as written: a guard makes the order of the
diff --git a/crates/infact-rust-normalize/tests/normalize.rs b/crates/infact-rust-normalize/tests/normalize.rs
index fed147c..a4bd567 100644
--- a/crates/infact-rust-normalize/tests/normalize.rs
+++ b/crates/infact-rust-normalize/tests/normalize.rs
@@ -1136,3 +1136,126 @@ fn nested_counter_loops_agree_with_nested_for_loops() {
     assert_eq!(counted, direct);
     assert!(counted.contains("(pairwise"), "{counted}");
 }
+
+/// Draining a container agrees with walking it.
+#[test]
+fn a_drain_agrees_with_a_for_loop() {
+    let drained = behavior_of(
+        "fn f(queue: &mut VecDeque<i32>) -> i32 {
+             let mut total = 0;
+             while let Some(x) = queue.pop_front() { total += x; }
+             total
+         }",
+        "f",
+    );
+    let direct = behavior_of(
+        "fn f(queue: VecDeque<i32>) -> i32 {
+             let mut total = 0;
+             for x in queue { total += x; }
+             total
+         }",
+        "f",
+    );
+    assert_eq!(drained, direct);
+}
+
+/// Pulling from an iterator by hand agrees with walking it.
+#[test]
+fn a_hand_written_next_loop_agrees_with_a_for_loop() {
+    let pulled = behavior_of(
+        "fn f(items: &mut Iter<i32>) -> i32 {
+             let mut total = 0;
+             while let Some(x) = items.next() { total += x; }
+             total
+         }",
+        "f",
+    );
+    let direct = behavior_of(
+        "fn f(items: Iter<i32>) -> i32 {
+             let mut total = 0;
+             for x in items { total += x; }
+             total
+         }",
+        "f",
+    );
+    assert_eq!(pulled, direct);
+}
+
+/// Taking from the back is not taking from the front.
+#[test]
+fn draining_from_each_end_gives_different_walks() {
+    let front = behavior_of(
+        "fn f(q: &mut VecDeque<i32>) -> i32 {
+             let mut t = 0; while let Some(x) = q.pop_front() { t += x; } t
+         }",
+        "f",
+    );
+    let back = behavior_of(
+        "fn f(q: &mut VecDeque<i32>) -> i32 {
+             let mut t = 0; while let Some(x) = q.pop_back() { t += x; } t
+         }",
+        "f",
+    );
+    assert_ne!(front, back);
+    assert!(back.contains("traverse-back"), "{back}");
+}
+
+/// A worklist is not a drain.
+///
+/// Putting something back makes the loop visit elements the container did not
+/// start with, and it is the commoner shape by two to one.
+#[test]
+fn a_worklist_is_not_a_drain() {
+    let form = behavior_of(
+        "fn f(q: &mut VecDeque<i32>) -> i32 {
+             let mut t = 0;
+             while let Some(x) = q.pop_front() { t += x; if x > 0 { q.push_back(x - 1); } }
+             t
+         }",
+        "f",
+    );
+    assert!(form.contains("(repeat"), "{form}");
+}
+
+/// A bare `pop` settles no order, so it is not read as a walk.
+///
+/// It is the last element of a `Vec` and the greatest of a `BinaryHeap`, and
+/// nothing in the form says which. Measured across the corpus, 434 of the 931
+/// files that drain with `pop` also use a `BinaryHeap`.
+#[test]
+fn a_bare_pop_is_not_a_drain() {
+    let form = behavior_of(
+        "fn f(v: &mut Vec<i32>) -> i32 {
+             let mut t = 0; while let Some(x) = v.pop() { t += x; } t
+         }",
+        "f",
+    );
+    assert!(form.contains("(repeat"), "{form}");
+}
+
+/// Measuring the container mid-drain observes a state a walk never has.
+#[test]
+fn a_body_that_measures_the_container_is_not_a_drain() {
+    let form = behavior_of(
+        "fn f(q: &mut VecDeque<i32>) -> usize {
+             let mut t = 0; while let Some(_x) = q.pop_front() { t += q.len(); } t
+         }",
+        "f",
+    );
+    assert!(form.contains("(repeat"), "{form}");
+}
+
+/// A `while let` binds a name, and the body uses that name.
+///
+/// Held as a condition it was normalized as an expression, so the name came out
+/// a hole that matched anything rather than the binding the body reads.
+#[test]
+fn a_while_let_binds_rather_than_leaving_a_hole() {
+    let form = behavior_of(
+        "fn f(v: &mut Vec<i32>) -> i32 {
+             let mut t = 0; while let Some(x) = v.pop() { t += x; } t
+         }",
+        "f",
+    );
+    assert!(form.contains("(Some v"), "{form}");
+}