P-016 A1: loop support in the core (worklist fixpoint over back-edges)

README.md

@@ -276,8 +276,9 @@ fn process(size: int) {
 `borrow_mut` требует эксклюзива (живой shared → OWN006, живой mut → OWN011),
 `borrow` несовместим с живым mut (→ OWN012).
 
-Поскольку язык без циклов и borrow'ы блок-скоупные, множество активных loans
-**одинаково** на всех предшественниках любого merge. Это инвариант, который
+Поскольку borrow'ы блок-скоупные (loan, открытый в теле `while`, закрывается там
+же, в той же итерации), множество активных loans **одинаково** на всех
+предшественниках любого merge — включая back-edge цикла. Это инвариант, который
 `join()` **проверяет ассертом**, а не предполагает (см. ниже про OWN010-ревьюера).
 
 ---
@@ -341,7 +342,7 @@ fn process(size: int) {
 
 | Код | Что ловит |
 |-----|-----------|
-| OWN020 | неподдерживаемая конструкция (цикл/async) |
+| OWN020 | неподдерживаемая конструкция (`for`/`loop`-итерация, async; `while` поддержан) |
 | OWN030 | неизвестное имя |
 | OWN031 | переопределение в области видимости |
 | OWN032 | owned-ресурс скопирован без `move` |
@@ -387,7 +388,12 @@ if (flag) { release c; }     // then: c -> {RELEASED}
 - `OWNED ∈`, но рядом `MOVED` → **maybe** (OWN010);
 - на выходе `OWNED ∈` → OWN001.
 
-Обход — один топологический проход по DAG (циклов нет → fixpoint не нужен).
+Обход — worklist до fixpoint: `while` даёт back-edge, и блок переоценивается, пока
+его in-состояние не перестанет расти (решётка `{OWNED,MOVED,RELEASED,ESCAPED}`
+конечна, merge = объединение, transfer монотонен → сходится без widening). На CFG
+без циклов это вырождается в один проход на блок — как прежний топологический обход.
+Диагностики печатаются вторым проходом, по сошедшимся состояниям (один раз, не на
+каждой итерации fixpoint).
 
 ### Важный разворот про false positives
 
@@ -620,12 +626,14 @@ fallback = pool`) — тоже **OWN030**: конфликтующее обеща
 | OWN013 (missing-return) | OWN033 | |
 | — | OWN040 / OWN041 | новая граница вызовов |
 
-Про **OWN010-ревьюера «incompatible-state-at-join»**: в блок-скоупном языке без
-циклов несовместимых loans на merge быть не может (borrow всегда сбалансирован
-внутри ветки). Поэтому это не user-facing код, а **ассерт-инвариант** в `join()`.
+Про **OWN010-ревьюера «incompatible-state-at-join»**: в блок-скоупном языке
+несовместимых loans на merge быть не может (borrow всегда сбалансирован внутри
+ветки — и внутри тела `while`, так что back-edge цикла тоже несёт тот же набор
+loans). Поэтому это не user-facing код, а **ассерт-инвариант** в `join()`.
 Добавлять диагностику, которая структурно никогда не сработает, — это та самая
-декорация, против которой вся затея. Когда появятся циклы/ранний выход из borrow'а,
-ассерт превратится в реальный код. (Номер OWN010 в новой схеме занят «maybe-move».)
+декорация, против которой вся затея. Если появится ранний выход из borrow'а
+(`break` из тела с открытым loan), ассерт превратится в реальный код. (Номер
+OWN010 в новой схеме занят «maybe-move».)
 
 ---
 
@@ -644,8 +652,10 @@ fallback = pool`) — тоже **OWN030**: конфликтующее обеща
    Soundness не доказан — он аргументирован и протестирован. Трансляция в Dafny/F\*
    и доказательство — **следующий слой**, не этот.
 
-3. **Циклы и async отвергаются, а не анализируются** (OWN020). Нужен worklist с
-   fixpoint и loop-инварианты владения; CFG к этому готов (DAG-проход → worklist).
+3. **`while` анализируется** (worklist + fixpoint по back-edge: cross-iteration
+   leak/use-after-release/double-release, см. `tests/test_loops.py`). А вот
+   `for`/`loop`-итерация и async пока отвергаются (OWN020) — для них нужна
+   десугаризация в `while` либо отдельная модель; CFG и worklist к этому готовы.
 
 4. **В песочнице PoC нет .NET** — golden проверен *по построению* и чекером. Но
    **CI его реально компилирует и запускает** настоящим компилятором (job
@@ -691,7 +701,7 @@ fallback = pool`) — тоже **OWN030**: конфликтующее обеща
 ```
 ownlang/
   ownlang/
-    lexer.py        # токенизатор; цикл/async лексятся как REJECTED; строки для emit_*
+    lexer.py        # токенизатор; for/loop/async лексятся как REJECTED (while — нет); строки для emit_*
     ast_nodes.py    # dataclass-узлы AST (resource, extern, call, эффекты, buffer, policy)
     parser.py       # recursive descent; грамматика в docstring
     buffers.py      # storage policies: режимы, резолв policy+intent, валидация

docs/proposals/P-016-deep-fact-extraction.md

@@ -9,8 +9,13 @@
   FPs (Task/DataTable) now excluded by a CA2000-style exemption → 100% precision on
   the sample. The own-check wrappers (`own-check.ps1`/`.sh`) now **default to
   `--flow-locals`** (`-Legacy`/`--legacy` opts back to the flat detector); the raw
-  extractor flag stays default-off pending A1 + an `OWNIR_VERSION` bump. Next: A1
-  (loops), escape-via-projection hardening, then full graduation.
+  extractor flag stays default-off pending an `OWNIR_VERSION` bump. **A1 (core loop
+  support) landed:** `while` is analysed with a worklist+fixpoint over the back-edge
+  (cross-iteration leak / use-after-release / double-release), replacing the single
+  topological pass; `for`/`loop`/async stay `OWN020`. Pinned by `tests/test_loops.py`
+  + gallery `10_leak_in_loop.own`. Next: have the flow extractor lower `while` to
+  back-edge flow facts (it currently bails on loop bodies), escape-via-projection
+  hardening, then full graduation.
 - **Depends on:**
   - [P-014](P-014-semantic-resolution.md) Tier A — the `SemanticModel` (**DONE**).
     The hard prerequisite: typed ownership facts are impossible without binding.
@@ -68,11 +73,17 @@ a CFG-carrying bridge, and the existing core checks real code.
 
 ### Track A — core only (pure DSL, no frontend, `.own`-tested)
 
-- **A1 — Loops.** Replace the single topological pass over the DAG (`cfg.py`,
-  `analysis.py`) with a worklist + fixpoint over back-edges. The lattice is the
-  finite set-of-states (OwnCore §3, union at merges) → monotone → it converges
-  (confirm whether widening is even needed). Removes the `OWN020` "loops" clause.
-  Fully independent of the frontend; pinned by new `.own` loop cases + the gallery.
+- **A1 — Loops. ✅ DONE.** Replaced the single topological pass over the DAG
+  (`cfg.py`, `analysis.py`) with a worklist + fixpoint over back-edges. The lattice
+  is the finite set-of-states (OwnCore §3, union at merges) → monotone → it converges
+  (widening was **not** needed — the per-symbol lattice has height 4). `while` lowers
+  to a header block with a back-edge from the body exit; diagnostics are emitted in a
+  second pass on the converged in-states (never during fixpoint iteration). Removed
+  the `OWN020` "loops" clause for `while` (`for`/`loop`/async still `OWN020`). Fully
+  independent of the frontend; pinned by `tests/test_loops.py` (cross-iteration
+  OWN001/003/009) + gallery `10_leak_in_loop.own`. Remaining: the flow **extractor**
+  still bails on loop bodies — lowering `while` to back-edge flow facts is a Track-B
+  follow-on (so loopy C# methods stop being honestly skipped).
 
 ### Track B — frontend depth (needs the `SemanticModel`, now present)
 

examples/gallery/10_leak_in_loop.own

@@ -0,0 +1,13 @@
+// OWN001 — a resource acquired every iteration but never released: leaks each pass.
+// Real C#: `while (cond) { var conn = Open(...); Use(conn); }` with no Dispose() —
+// a fresh handle leaks on every loop turn, regardless of what ends the loop. The
+// condition is opaque to the checker (control flow is modelled, not values); what
+// matters is the back-edge, which the worklist fixpoint analyses rather than skips.
+module Gallery
+resource Conn { acquire open release close }
+fn drain(n: int) {
+  while (n) {
+    let c = acquire Conn(n);   // opened every iteration ...
+    use c;
+  }                            // ... never closed -> leak
+}

ownlang/analysis.py

@@ -26,13 +26,22 @@
   a move needs Own (suspended by *any* loan -> OWN007), a release needs Drop
   (-> OWN008), `use` needs Read (suspended by a mutable loan -> OWN013), and so on.
 
-The traversal is a single topological pass over the loop-free DAG. Because every
-borrow is block-scoped, the set of active loans is identical on all predecessors
-of a merge, so joining loans is trivial; this invariant is asserted, not assumed.
+The traversal is a forward worklist to a fixpoint, so it handles loops (`while`):
+a block is re-evaluated until its in-state stops growing. The per-symbol lattice
+is the finite set {OWNED,MOVED,RELEASED,ESCAPED} merged by union, and the transfer
+is monotone, so the iteration converges (no widening needed). On a loop-free CFG
+this reduces to one pass per block — identical to the previous topological walk.
+Because every borrow is block-scoped, the active loans are identical on all
+predecessors of a merge (back-edges included), so joining loans is trivial; this
+invariant is asserted, not assumed.
+
+Diagnostics are emitted in a second pass, once, on the converged in-states — never
+during the fixpoint iteration (a looped block is transferred many times).
 """
 
 from __future__ import annotations
 
+from collections import deque
 from dataclasses import dataclass, field
 from enum import Enum, auto
 from typing import assert_never
@@ -93,11 +102,13 @@ def join(a: State, b: State) -> State:
     out = State()
     for k in set(a.var) | set(b.var):
         out.var[k] = set(a.var.get(k, set())) | set(b.var.get(k, set()))
-    # Block-scoped borrows => identical active loans on both predecessors.
-    # Assert the invariant rather than silently papering over a builder bug.
+    # Block-scoped borrows => identical active loans on both predecessors. This
+    # holds across loop back-edges too: a borrow opened inside a loop body closes
+    # within the same iteration, so the loan set at the body exit equals the one on
+    # the entry edge. Assert the invariant rather than paper over a builder bug.
     assert set(a.loans) == set(b.loans), (
         "active loans differ at a control-flow merge; this should be impossible "
-        "for block-scoped borrows in a loop-free language"
+        "for block-scoped borrows (they close within the scope that opened them)"
     )
     out.loans = dict(a.loans)
     return out
@@ -108,6 +119,11 @@ def __init__(self, cfg: CFG):
         self.cfg = cfg
         self.diags: list[Diagnostic] = []
         self.blocks = {b.id: b for b in cfg.blocks}
+        # During the fixpoint pass (phase 1) the transfer runs repeatedly to
+        # converge the per-block in-states; diagnostics must NOT be emitted then
+        # (a block in a loop is visited many times). `silent` gates `err`; phase 2
+        # re-runs the transfer once per block, emitting on the converged state.
+        self.silent = False
 
     def initial_state(self) -> State:
         s = State()
@@ -119,6 +135,8 @@ def initial_state(self) -> State:
     def err(self, code: str, msg: str, line: int,
             subject: str | None = None,
             resource_kind: str | None = None) -> None:
+        if self.silent:
+            return
         self.diags.append(Diagnostic(code, msg, line, subject=subject,
                                      resource_kind=resource_kind))
 
@@ -171,55 +189,75 @@ def _state_problem(self, st: State, sym: Symbol, verb: str, line: int) -> bool:
             return True
         return False
 
-    # -- topological order over the DAG ------------------------------------
+    # -- reachability + dataflow fixpoint ----------------------------------
 
-    def topo_order(self) -> list[int]:
-        reachable: set[int] = set()
+    def reachable(self) -> set[int]:
+        seen: set[int] = set()
         stack = [self.cfg.entry]
         while stack:
             x = stack.pop()
-            if x in reachable:
+            if x in seen:
                 continue
-            reachable.add(x)
+            seen.add(x)
             stack.extend(self.blocks[x].succ)
-        local_indeg = dict.fromkeys(reachable, 0)
-        for b in reachable:
-            for s in self.blocks[b].succ:
-                if s in reachable:
-                    local_indeg[s] += 1
-        ready = [b for b in reachable if local_indeg[b] == 0]
-        order: list[int] = []
-        while ready:
-            b = ready.pop()
-            order.append(b)
-            for s in self.blocks[b].succ:
-                if s in reachable:
-                    local_indeg[s] -= 1
-                    if local_indeg[s] == 0:
-                        ready.append(s)
-        return order
+        return seen
+
+    def in_state_of(self, bid: int, preds: dict[int, list[int]],
+                    reachable: set[int], out_states: dict[int, State]) -> State:
+        """The in-state of a block = the join (union) of its already-computed
+        predecessors' out-states; the entry block starts from `initial_state`."""
+        if bid == self.cfg.entry:
+            return self.initial_state()
+        ps = [p for p in preds[bid] if p in reachable and p in out_states]
+        if not ps:
+            return State()
+        st = out_states[ps[0]].copy()
+        for p in ps[1:]:
+            st = join(st, out_states[p])
+        return st
+
+    def fixpoint(self, reachable: set[int]) -> dict[int, State]:
+        """Forward worklist to a fixpoint over a (possibly cyclic) CFG. The
+        per-symbol lattice is the finite set {OWNED,MOVED,RELEASED,ESCAPED}, merged
+        by union at joins; the transfer is monotone, so iterating until no out-state
+        changes converges (a block's out can only grow up the finite lattice). A
+        block is re-queued only when one of its predecessors' out-state changed.
+        Runs silently — phase 2 emits the diagnostics on the converged in-states."""
+        preds = self.cfg.preds()
+        in_states: dict[int, State] = {}
+        out_states: dict[int, State] = {}
+        work: deque[int] = deque(sorted(reachable))
+        queued: set[int] = set(reachable)
+        while work:
+            bid = work.popleft()
+            queued.discard(bid)
+            in_states[bid] = self.in_state_of(bid, preds, reachable, out_states)
+            new_out = self.transfer(self.blocks[bid], in_states[bid])
+            if bid not in out_states or new_out != out_states[bid]:
+                out_states[bid] = new_out
+                for s in self.blocks[bid].succ:
+                    if s in reachable and s not in queued:
+                        work.append(s)
+                        queued.add(s)
+        return in_states
 
     # -- main --------------------------------------------------------------
 
     def run(self) -> list[Diagnostic]:
-        order = self.topo_order()
-        preds = self.cfg.preds()
+        reachable = self.reachable()
+        # Phase 1: converge the in-states silently (no diagnostics — a looped block
+        # is transferred many times before it stabilises).
+        self.silent = True
+        in_states = self.fixpoint(reachable)
+        self.silent = False
+        # Phase 2: one emitting transfer per block, on its converged in-state, so
+        # every diagnostic is reported exactly once at the fixpoint. Block order is
+        # irrelevant — __main__ sorts the diagnostics by (line, code).
         out_states: dict[int, State] = {}
-        reachable = set(order)
-
-        for bid in order:
-            ps = [p for p in preds[bid] if p in reachable and p in out_states]
-            if bid == self.cfg.entry:
-                in_state = self.initial_state()
-            elif ps:
-                in_state = out_states[ps[0]].copy()
-                for p in ps[1:]:
-                    in_state = join(in_state, out_states[p])
-            else:
-                in_state = State()
-            out_states[bid] = self.transfer(self.blocks[bid], in_state)
+        for bid in sorted(reachable):
+            out_states[bid] = self.transfer(self.blocks[bid], in_states[bid])
 
-        for bid in order:
+        for bid in sorted(reachable):
             blk = self.blocks[bid]
             if blk.succ:
                 continue

ownlang/ast_nodes.py

@@ -138,6 +138,16 @@ class If:
     line: int
 
 
+@dataclass(frozen=True)
+class While:
+    # like If, the condition is opaque: we model the loop's control flow (a body
+    # that may run zero or more times, with a back-edge to the test), not the
+    # values. The analysis reaches a fixpoint over the back-edge (analysis.py).
+    cond_text: str
+    body: list[Stmt]
+    line: int
+
+
 @dataclass(frozen=True)
 class Return:
     var: str | None
@@ -154,7 +164,7 @@ class Subscribe:
     line: int
 
 
-Stmt = Let | Release | Use | Call | BorrowBlock | If | Return | Subscribe
+Stmt = Let | Release | Use | Call | BorrowBlock | If | While | Return | Subscribe
 
 
 # ---- top level ------------------------------------------------------------