Release 0.1.13: a lazy automaton answers match and bounds from host-owned storage

.github/workflows/ci.yml

@@ -24,6 +24,16 @@ jobs:
 
   input-differential:
     runs-on: ubuntu-latest
+    # Every harness below runs three times: with the evaluator alone, and with
+    # the lazy automaton answering every eligible case beside it, in a roomy
+    # cache and in the least storage each program accepts. Any disagreement is
+    # an outcome of its own. See docs/dfa.md.
+    strategy:
+      fail-fast: false
+      matrix:
+        dfa: ["", "1", "small"]
+    env:
+      PEREX_DFA: ${{ matrix.dfa }}
     steps:
       - uses: actions/checkout@11d5960a326750d5838078e36cf38b85af677262 # v4
       - uses: actions/setup-node@49933ea5288caeca8642d1e84afbd3f7d6820020 # v4
@@ -129,6 +139,11 @@ jobs:
         run: node tools/check-test262.mjs target/release/examples/engine_probe third_party/test262-checkout artifacts/test262 --work 64000000
       - name: Unicode and legacy case equivalence differential
         run: node tools/check-casefold.mjs target/release/examples/engine_probe
+      - name: Random automaton-eligible patterns against Node
+        if: matrix.dfa != ''
+        run: |
+          node tools/check-dfa-fuzz.mjs target/release/examples/engine_probe artifacts/dfa-fuzz-1 --seed 1 --cases 20000
+          node tools/check-dfa-fuzz.mjs target/release/examples/engine_probe artifacts/dfa-fuzz-2 --seed 2 --cases 20000
       - run: cargo +stable build --locked --release --example property_probe
       - name: Exhaustive properties and exact reviewed reference disagreements
         run: node tools/check-properties.mjs target/release/examples/property_probe target/release/examples/engine_probe --allow-reviewed-reference-disagreements

AGENTS.md

@@ -1,7 +1,7 @@
 # Perex development constraints
 
 - This repository is the authoritative reusable engine source; it must build independently of Perry.
-- Implement one production compiler/matcher. Other engines may be development references, never production fallbacks.
+- One semantics, two exact executors. One compiler emits one program format. The backtracking evaluator defines every answer and is the only source of captures. The lazy automaton (`src/dfa.rs`) may answer match/no-match and group zero's bounds for programs whose validated header bit says it decides them exactly; it answers exactly what the evaluator answers, which the differential and fuzz CI enforce in all three automaton modes (off, roomy cache, minimum cache), and it declines rather than approximates. Other engines may be development references, never production fallbacks.
 - Follow `docs/memory-contract.md`: explicit storage ownership, relocation-safe programs, scoped scratch, exact string semantics and offset-only results.
 - The compiler/matcher, input layer and resumable execution are implemented and are Perry's production regex engine. The `v` flag is implemented in full, properties of strings included. Do not claim matching, compatibility or performance that has not been measured.
 - Traverse the host's original subject without copying it or creating a UTF-16 conversion buffer. Integer spans remain the result contract.

CLAUDE.md

@@ -53,11 +53,11 @@ Cost drivers (diagnostics, not adoption evidence): `examples/input_cost.rs`, `en
 
 ## Architecture
 
-One compiler, one program format, one evaluator. There is no fallback engine and must never be one.
+One compiler, one program format, one semantics with two exact executors: the evaluator, which defines every answer and produces every capture, and the lazy automaton, which answers match/no-match and group zero's bounds for eligible programs exactly as the evaluator would, or declines. There is no approximating or fallback engine and must never be one.
 
 **Pattern text → program.** `compiler::compile` parses into a caller-owned arena of `Node`/`Range` scratch (indices only, no source pointers survive) and emits a validated immutable `u32` program. `compiler::prepare` splits the same pipeline so the host can drop its pattern borrow before allocating final output: `Prepared::required_words()` gives the exact size, `emit` consumes the plan. Emission walks the topologically ordered arena iteratively — no native-stack recursion on long concatenations, no per-count expansion of `a{n}`. Submodules under `src/compiler/` add optimizer analyses (`admission`, `candidate`, `classes`, `repetition`) and grammar corners (`escapes` for Annex B, `names`).
 
-**Program format** (`src/program.rs`). One relocatable buffer: header, three words per instruction, class-table pairs, eight-word repeat records, a filter section for properties of strings, optional packed name section. Everything is relative offsets/indices — never a host pointer. `Program::from_words` revalidates opcodes, operand ranges, property IDs, branch/table bounds and name/capture lists under a work budget, so a relocated or re-read buffer is always checked. `HEADER` and `VERSION` in `src/program.rs` are authoritative (currently 11 words / version 14); older versions are rejected outright, and a few docs still quote an earlier number. Word 9 (leading-literal run) is *re-derived* from the instructions during validation rather than trusted — hint words that can't be re-derived (words 7/8) are only allowed to be conservative, never to supply capture semantics.
+**Program format** (`src/program.rs`). One relocatable buffer: header, three words per instruction, class-table pairs, eight-word repeat records, a filter section for properties of strings, optional packed name section. Everything is relative offsets/indices — never a host pointer. `Program::from_words` revalidates opcodes, operand ranges, property IDs, branch/table bounds and name/capture lists under a work budget, so a relocated or re-read buffer is always checked. `HEADER` and `VERSION` in `src/program.rs` are authoritative (currently 11 words / version 15); older versions are rejected outright, and a few docs still quote an earlier number. Word 9 (leading-literal run) is *re-derived* from the instructions during validation rather than trusted — hint words that can't be re-derived (words 7/8) are only allowed to be conservative, never to supply capture semantics.
 
 **Subject access** (`src/input.rs`). `Input` borrows original storage — `&str`, generalized WTF-8 bytes (lone and separately-encoded surrogates accepted), or host `&[u16]`. **Never build a UTF-16 conversion buffer or copy the subject**; that is the core project constraint. All public positions count UTF-16 units, including positions between surrogate halves. ASCII byte storage gets a distinct internal representation with O(1) seeks; non-ASCII byte cursors pack a half-pair flag into the high bit of the byte offset.
 
@@ -79,6 +79,7 @@ A single `Budget` covers a whole compile or search — it is never reset per sta
 - Keep the three outcomes distinct: syntax error, `CompileError::Unsupported`, and no-match. Reporting an unimplemented feature as a syntax error or a no-match is a correctness bug, and unsupported cases must stay visible rather than being counted as handled.
 - Matching changes need complete-capture witnesses; memory changes need lifetime/relocation witnesses (relocate, poison and free the old storage, then continue). Each `docs/<feature>.md` ends with a Verification section naming its tests and harnesses — update the doc with the code.
 - Optimizations (admission, candidate starts, leading literals, atom repeats, sorted classes) must run the same VM for the answer. They may only reject impossible work; they never choose between matches or produce captures.
+- The lazy automaton (`src/dfa.rs`, `docs/dfa.md`) is the second exact executor of the same semantics (`AGENTS.md`): for programs whose validated word 7 bit says it decides them exactly, it answers match/no-match and group zero's bounds from the same instructions. It never produces captures, it declines rather than approximates, and the probe's `PEREX_DFA` mode (CI runs every differential harness off, with `1` and with `small`) and `tools/check-dfa-fuzz.mjs` compare it with the VM and Node. A change to either must keep them equal. Its idle skip reuses the evaluator's candidate scans and leading pairs (`src/executor/candidate.rs`); like them, it may pass over only positions where no match can begin.
 - Do not claim compatibility, conformance percentages or performance that has not been measured, and preserve failed measurements rather than deleting them. `docs/performance.md` defines the per-case CPU/RSS gates; aggregate wins do not satisfy them.
 - New dependencies, `unsafe`, implicit global caches, engine-owned result strings and host GC assumptions are all out of bounds. Perry-specific GC/adapter code belongs in Perry, not here.
 - Bumping the program format means rejecting older versions and updating both the validator and the docs that quote the layout.

Cargo.toml

@@ -1,6 +1,6 @@
 [package]
 name = "perex"
-version = "0.1.12"
+version = "0.1.13"
 edition = "2024"
 rust-version = "1.88"
 description = "An ECMAScript regex engine designed for explicit host memory ownership"

README.md

@@ -130,6 +130,9 @@ node tools/check-repetition.mjs target/release/examples/engine_probe
 node tools/check-atom-filter.mjs target/release/examples/engine_probe artifacts/atom-filter
 node tools/check-atom-filter.mjs target/release/examples/engine_probe artifacts/atom-filter-q1 --quantum 1 --relocate --grow
 node tools/check-atom-filter.mjs target/release/examples/engine_probe artifacts/atom-filter-q17 --quantum 17 --relocate --grow
+PEREX_DFA=1 node tools/check-engine.mjs target/release/examples/engine_probe --allow-listed-unsupported --allow-reviewed-reference-disagreements
+PEREX_DFA=small node tools/check-engine.mjs target/release/examples/engine_probe --allow-listed-unsupported --allow-reviewed-reference-disagreements
+node tools/check-dfa-fuzz.mjs target/release/examples/engine_probe artifacts/dfa-fuzz --seed 1 --cases 20000
 node tools/check-modifiers.mjs target/release/examples/engine_probe
 node tools/check-unicode-sets.mjs target/release/examples/engine_probe artifacts/unicode-sets
 node tools/check-sets.mjs target/release/examples/engine_probe artifacts/sets --allow-reviewed-reference-disagreements
@@ -177,6 +180,8 @@ Case equivalence uses generated Unicode 17.0.0 data under the [Unicode License V
 
 [Test262 pattern conformance](docs/conformance.md) compares every pattern harvested from the suite's regular-expression tests against Node, for syntax acceptance and complete match answers. There is no remaining gap: 48,718 cases compared, nothing unsupported and no difference, on the harvest recorded there.
 
+[The lazy automaton](docs/dfa.md) answers whether a program matches, and where its match begins and ends, in a few instructions per character from states it builds on demand in a cache the host owns, for programs without backreferences, lookaround or properties of strings. The evaluator remains the only source of captures, and every differential harness compares the two.
+
 [Branches](docs/branch.md) lay alternation out flat and skip an alternative, and its backtracking frame, when the next character cannot begin it, by a first-character set re-derived from the instructions during validation.
 
 [Leading literal starts](docs/leading.md) reject an impossible start with a byte comparison instead of an initialized trial. The claim is re-derived from the instructions during program validation, so it cannot disagree with them.

docs/candidate.md

@@ -36,7 +36,8 @@ no ASCII start is possible, or `2 | (lo << 8) | (hi << 16)` for an inclusive
 interval with `0 <= lo <= hi <= 127`. Reserved bits, malformed bounds and old
 format versions are rejected. The additional word costs four used program bytes.
 Since format 14 the descriptor occupies word 7's low 24 bits; bit 24 holds the
-validated start-anchored claim and the bits above it are reserved.
+validated start-anchored claim. Since format 15 bit 25 holds the validated
+[automaton eligibility](dfa.md) claim, and the bits above it are reserved.
 Bindings check the full eleven-word header when reacquiring a view. AOT and runtime
 programs must use this same format and its version checks.
 
@@ -65,7 +66,8 @@ positions; [leading](leading.md) describes it. Only logical positions
 through the first candidate are charged, so word-read speculation does not change
 matching work across quanta. Subject positions remain cursor offsets/checkpoints;
 no subject address survives the scoped borrow. The scan adds a phase but no frame,
-undo entry or match-scratch buffer.
+undo entry or match-scratch buffer. The lazy automaton's idle skip uses these same scans and
+leading pairs ([lazy DFA](dfa.md#the-idle-skip)).
 
 Mixed scanning uses the cursor's current byte suffix, never a UTF-16 re-seek from
 an end of the string. It checks the skipped prefix is ASCII and advances byte and