docs+lint: clarify backtrack semantics — runtime is always-on for Choice

Three docs + the lint message itself were describing the `backtrack`
attribute as a runtime control. The actual behaviour (live in
src/frame.cpp:22) has been: every Choice frame is always backtracked
at runtime, regardless of the `Node.backtrack` flag. The flag exists
only for lint introspection.

External agent surfaced the discrepancy when authoring a constraint
grammar: setting `backtrack: true` made the lint go quiet, but the
parse behaved identically without it. Investigation showed the frame.cpp
comment is the source of truth — the flag is a lint annotation now,
not a parse-direction control. Docs and lint message had to be brought
in line.

**Fixed:**

* `docs/rawast-format.md` §4.7 — was "rawast does not backtrack at the
  structural level". Now: alternatives are tried in source order with
  mark/reject wrapping (always-on); `backtrack: true` is a grammar-
  author annotation the linter uses to suppress LL(k) warnings, not a
  runtime control.

* `docs/ARCHITECTURE.md` — the LL(1) lint section was claiming alts
  "become unreachable" without `backtrack: true`. They don't — the
  engine handles them correctly. Rewritten as: lint flags shared-prefix
  Choices as a heads-up so authors mark intentional fall-through with
  the flag; without the marker future readers can't tell whether the
  pattern is intentional or accidental.

* `docs/AGENTS.md` — the "Silencing the lint on intentional shared-
  prefix Choices" section had the same misframing. Reframed as
  "lint annotation, NOT runtime control" + the explicit note that you
  can skip the workaround entirely if you don't mind a few lint
  warnings (parse output is identical either way).

* `src/linter.cpp` — lint message itself updated. Was: "Without
  `backtrack: true` the predictive engine will commit to the first one
  and the others become unreachable" (incorrect — alts do get tried).
  Now: "The engine handles this correctly via alt-failure recovery...
  The lint flags it as a heads-up because the analysis can't prove
  disjointness statically. Set `backtrack: true` to mark this fall-
  through pattern as intentional (silences this warning; runtime
  behaviour is unchanged)."

**Issue #4** (DSL syntax for `backtrack`) remains valuable but reframed:
it's now "DSL needs a way to mark intentional fall-through patterns
inline rather than via Python loader hook", not "DSL needs a way to
control runtime backtracking".

Verification: 216/216 C++ doctest + 47/47 Python pytest passing. No
behaviour changes — only doc + lint message corrections.

Author: lanserge

docs/AGENTS.md

@@ -196,9 +196,11 @@ But this trade is rarely worth it — the linter (LL(k) lookahead) won't flag th
 
 ### Silencing the lint on intentional shared-prefix Choices
 
-The lint's LL(k) check is conservative — it flags shared-prefix Choices when one of the alternatives can begin with a generic Parse (identifier, number) that has no Key constraint at the lookahead depth. PEG handles these cases correctly via alt-failure recovery (alt A is tried, fails, alt B is tried), but the lint warns because the first-token analysis can't prove disjointness within bounded depth.
+The lint's LL(k) check flags Choices where two alternatives share a leading rule that can't be disambiguated by first-token analysis within bounded depth. The OR / OR_MULTI pattern above is a typical example — both branches start with `<AND>`, and the lint can't prove they diverge within its lookahead window because `<AND>` can begin with a generic Parse (identifier, number).
 
-The right marker is `backtrack: true` on the Choice — it tells both the engine and the lint "this alt-failure pattern is intentional." Today the DSL doesn't have syntax for this attribute (tracked as issue #4); the workaround is to set it on the dict at load time before passing to `Grammar.from_dict()`:
+**Important — this is a lint annotation, NOT a runtime control.** The rawast engine *always* backtracks Choice frames at runtime: every alternative attempt is wrapped in input-cursor `mark()` / `reject()`, so partial alt-failure cleanly restores position and tries the next alt. The shared-prefix pattern parses correctly without any `backtrack: true` setting. The lint just can't see that statically, so it flags as a heads-up.
+
+To silence the lint on a Choice that uses an intentional fall-through pattern, set `backtrack: true` on the Choice. Today the DSL doesn't have syntax for this attribute (tracked as issue #4); the workaround is to set it on the dict at load time before passing to `Grammar.from_dict()`:
 
 ```python
 import rawast
@@ -213,9 +215,9 @@ def _load(grammar_path: str, backtrack_rules: tuple[str, ...]) -> rawast.Grammar
 grammar = _load("constraint.rawast", backtrack_rules=("OR", "AND", "RELATION"))
 ```
 
-This is a **loader configuration**, not AST post-processing. The grammar still emits the host's IR shape directly via bindings; the dict gets one flag per Choice rule before construction. The lint goes clean; the parse behavior is unchanged. When the DSL syntax for `backtrack` lands (issue #4), this loader hook collapses to nothing — but `backtrack: true` in the dict is the canonical way to express the same intent today.
+This is a **loader-time lint annotation**, not AST post-processing. The grammar still emits the host's IR shape directly via bindings; the dict gets one flag per Choice rule before construction. The lint output goes clean; the parse behaviour is identical with or without it. When DSL syntax for `backtrack` lands (issue #4), this loader hook collapses to nothing.
 
-The honest framing: this is the one piece of "Python around a rawast grammar" that ISN'T an anti-pattern. It's saying "this Choice was designed to use alt-failure intentionally" — a structural assertion about the grammar, not a transformation of parsed output.
+The honest framing: this is the one piece of "Python around a rawast grammar" that isn't an anti-pattern. It's a *grammar annotation* saying "this fall-through pattern is intentional, don't warn me." Skip the loader hook entirely if you don't mind a few lint warnings — the grammar still produces correct output either way.
 
 ## How an agent uses the parsed AST
 

docs/ARCHITECTURE.md

@@ -103,7 +103,7 @@ See `src/save_stack.cpp` for the engine. The entry point is `Grammar::save` (def
 
 `Grammar::lint()` runs structural checks on the grammar tree at load time. Issues detected:
 
-- **LL(1) violations on non-backtracking Choices.** A Choice without `backtrack: true` whose alternatives share a first-token signature will silently always pick the first match. The lint flags this with the specific token + alt indices that collide.
+- **LL(k) ambiguity on Choices.** A Choice without `backtrack: true` whose alternatives share a first-token signature (and whose LL(k) lookahead can't prove disjointness within bounded depth) is flagged. The engine actually handles these cases correctly via always-on alt-failure recovery for Choice frames — the lint flags them as a heads-up so authors mark intentional fall-through patterns with `backtrack: true`. Without the marker, future readers of the grammar can't tell whether the shared-prefix Choice is intentional or accidental.
 - **Wildcard-rule-with-nested-Choice-type-emit anti-pattern.** A `sequence dict` rule with no top-level `:type=…` discriminator whose body contains a nested Choice with `type=` emits. Save dispatch can't introspect through the nested Choice, so the rule looks like a catch-all and may swallow values destined for sibling alternatives, then fail on the inner Choice with "no matching grammar alternative for value at save". Fix: lift each nested-Choice alt to a sibling rule of the outer Choice.
 - **Raw-consume (`*`) misuse.** A `*` node not followed by a literal-key sibling in the same sequence. The literal sibling tells the engine where to stop the raw consumption.
 

docs/rawast-format.md

@@ -746,10 +746,20 @@ permitted.
 choice_expr ::= 'choice' '{' items '}'
 ```
 
-Ordered alternation: the first alternative whose initial terminal
-accepts is selected (predictive PEG; rawast does not backtrack at the
-structural level). All alternatives must be terminal-prefix-
-distinguishable; the grammar linter (planned) flags violations.
+Ordered alternation: alternatives are tried in source order. Each
+alternative attempt is wrapped in input-cursor `mark()` / `reject()` —
+if an alternative partially matches and then fails, the input position
+is restored and the next alternative is tried from the same position.
+This is standard PEG ordered-choice semantics and applies to every
+Choice node by default; the `backtrack: true` attribute on a Choice
+(if explicitly set) is retained as a *grammar-author annotation* that
+the linter uses to suppress LL(k)-ambiguity warnings on intentional
+shared-prefix patterns. It does not gate runtime behaviour.
+
+Alternatives with overlapping first-token signatures still parse
+correctly via the alt-failure recovery above, but the linter flags
+them as a heads-up unless `backtrack: true` is set on the Choice.
+See the `Grammar::lint()` machinery and `docs/AGENTS.md`.
 
 ### 4.8 Repeat — `repeat expression [separator expression]`
 

src/linter.cpp

@@ -475,18 +475,22 @@ std::vector<LintIssue> lint_grammar(const Grammar& g) {
             issue.alternatives.assign(still_ambiguous.begin(),
                                       still_ambiguous.end());
             issue.description =
-                "Choice has an ambiguous first-token \"" + tok + "\" across " +
+                "Choice has shared first-token \"" + tok + "\" across " +
                 std::to_string(issue.alternatives.size()) +
                 " alternatives whose key-paths remain indistinguishable up to "
-                "depth " + std::to_string(kMaxDepth) + ". Without "
-                "`backtrack: true` the predictive engine will commit to the "
-                "first one and the others become unreachable. Either set "
-                "`backtrack: true` on the Choice or restructure the grammar "
-                "so the alternatives diverge at some Key position. "
-                "(Alternatives that share the first token but diverge at a "
-                "later Key — e.g. `\"+\", \"FIXED\"` vs `\"+\", \"ROUTED\"` — "
-                "are not flagged: PEG's ordered choice naturally falls back "
-                "between them on alt failure.)";
+                "LL(" + std::to_string(kMaxDepth) + ") lookahead. The engine "
+                "handles this correctly via alt-failure recovery (every Choice "
+                "frame is backtracked at runtime — partial alt matches restore "
+                "input cursor and the next alt is tried). The lint flags it as "
+                "a heads-up because the analysis can't prove disjointness "
+                "statically. Either set `backtrack: true` on the Choice to "
+                "mark this fall-through pattern as intentional (silences this "
+                "warning; runtime behaviour is unchanged), or restructure the "
+                "grammar so the alternatives diverge within LL(" +
+                std::to_string(kMaxDepth) + ") lookahead. "
+                "(Choices that share the first token but diverge at a later "
+                "Key — e.g. `\"+\", \"FIXED\"` vs `\"+\", \"ROUTED\"` — are not "
+                "flagged: the LL(k) check sees through to the diverging Key.)";
             issues.push_back(std::move(issue));
         }
     }