beam: add CHECK_DL gate with independent BFS oracle for true DL
The DL module's cells were module-level asserts: run_lane_tests.py --list reports unittest=0 bare=0 for test_damerau_levenshtein.py, so no named case moved when the module broke. CHECK_DL runs the shipped cells plus oracle_dl.py, which grades a deterministic 5300-pair corpus against a BFS over the edit graph (the definition of true DL) and proves in the same run that the corpus reds both classic impostors (OSA, plain Levenshtein). Measured: green on the tree (0/5228 mismatches, 42 OSA witnesses, 252 Lev witnesses); rc 1 with named witnesses on a transposition-deleted mutant and on an OSA module.
This commit is contained in:
ledger committed
1 parent
e1182ce4f8
commit
5ab4b187c7
2 files changed
+283
No files matched your search
Executable
+44
@@ -0,0 +1,44 @@
|
||||
#!/bin/bash
|
||||
# CHECK_DL: gate for wizard-work/beam/damerau_levenshtein.py (Q133-DL).
|
||||
#
|
||||
# Why this file exists (2026-10-31). The DL module and its cells landed in
|
||||
# 5bded80, but nothing pinned the *property* the module exists for: the cells
|
||||
# are module-level asserts that run only when the file is imported, and
|
||||
# `run_lane_tests.py --list` reports `test_damerau_levenshtein.py unittest=0
|
||||
# bare=0` -- zero named cases, so the gate's per-test count never moves when
|
||||
# they break. This gate names the work: the shipped cells run as a script, and
|
||||
# an independent BFS oracle (oracle_dl.py) grades a deterministic corpus against
|
||||
# the module and proves, in the same run, that the corpus can red the two
|
||||
# implementations people ship by mistake (OSA and plain Levenshtein).
|
||||
#
|
||||
# Exit codes follow the repo's tools/ contract:
|
||||
# 0 clean, 1 graded a fault, 2 could not grade.
|
||||
|
||||
set -u
|
||||
set -o pipefail
|
||||
cd "$(dirname "$(readlink -f "$0")")" || exit 2
|
||||
|
||||
if ! command -v python3 >/dev/null 2>&1; then
|
||||
echo "CHECK_DL: python3 not found -- cannot grade." >&2
|
||||
exit 2
|
||||
fi
|
||||
|
||||
echo "== shipped cells (test_damerau_levenshtein.py) =="
|
||||
python3 test_damerau_levenshtein.py
|
||||
rc=$?
|
||||
if [ "$rc" -ne 0 ]; then
|
||||
echo "CHECK_DL: shipped cells failed (rc=$rc)." >&2
|
||||
exit 1
|
||||
fi
|
||||
|
||||
echo "== independent BFS oracle (oracle_dl.py) =="
|
||||
python3 oracle_dl.py
|
||||
rc=$?
|
||||
case $rc in
|
||||
0) ;;
|
||||
1) echo "CHECK_DL: oracle graded a fault -- see MISMATCH/FAIL above." >&2; exit 1 ;;
|
||||
2) echo "CHECK_DL: oracle could not grade -- see message above." >&2; exit 2 ;;
|
||||
*) echo "CHECK_DL: oracle exited $rc -- internal error (a fault)." >&2; exit 1 ;;
|
||||
esac
|
||||
|
||||
echo "CHECK_DL: green"
|
||||
@@ -0,0 +1,239 @@
|
||||
#!/usr/bin/env python3
|
||||
"""oracle_dl.py -- independent exact oracle for damerau_levenshtein.py (Q133-DL).
|
||||
|
||||
WHY THIS EXISTS
|
||||
`wizard-work/beam/damerau_levenshtein.py` is graded only through
|
||||
`run_lane_tests.py`, which imports it and finds 0 unittest cases and 0 bare
|
||||
`test_*` functions (measured: `run_lane_tests.py --list` line
|
||||
"test_damerau_levenshtein.py unittest=0 bare=0"). The cells it does carry are
|
||||
module-level asserts that run at import, so a *crash* is a fault -- but the
|
||||
file's pass path prints "basic ok" / "monotonic ok" and nothing pins the
|
||||
property that separates true DL from the two cheaper implementations people
|
||||
ship by mistake:
|
||||
|
||||
OSA restricted optimal-string-alignment: a substring may be edited
|
||||
once. dl("ca","abc") is 2 for true DL and 3 for OSA.
|
||||
Lev plain Levenshtein: no transposition at all, so dl("ab","ba") is 1
|
||||
for DL and 2 for Lev.
|
||||
|
||||
Both wrong implementations pass every "dl <= lev" monotonicity assertion, and
|
||||
both pass "dl('ab','ba')==1"? No: OSA passes that one, Lev does not. What
|
||||
neither the shipped cells nor monotonicity pins is `dl("ca","abc")==2`, the
|
||||
single witness that OSA fails. This file makes that a measured corpus.
|
||||
|
||||
WHAT IT MEASURES
|
||||
A BFS over the edit graph itself -- states are strings, unit-cost edges are
|
||||
insert / delete / substitute / transpose-adjacent -- is the definition of true
|
||||
DL, so it is independent of the module's Lowrance-Wagner matrix. Depth is
|
||||
capped at the Levenshtein upper bound (dl <= lev, so no improving path can be
|
||||
longer), which keeps the search finite and exact.
|
||||
|
||||
`--teeth` feeds the SAME corpus an OSA implementation and a plain Levenshtein
|
||||
implementation and requires the corpus to catch both. A corpus that cannot
|
||||
red the classic wrong answers would report green on a broken module too.
|
||||
|
||||
EXIT CODES (repo tools/ contract)
|
||||
0 every corpus pair matched, and the corpus rejected both mutants
|
||||
1 a graded fault: a mismatch, or a mutant the corpus failed to catch
|
||||
2 could not grade: module missing, oracle could not run
|
||||
"""
|
||||
|
||||
from __future__ import annotations
|
||||
|
||||
import argparse
|
||||
import importlib.util
|
||||
import os
|
||||
import random
|
||||
import sys
|
||||
import time
|
||||
|
||||
HERE = os.path.dirname(os.path.abspath(__file__))
|
||||
MODULE = os.path.join(HERE, "damerau_levenshtein.py")
|
||||
|
||||
|
||||
def load_module(path):
|
||||
"""Import the module under test from beside this file (no host path)."""
|
||||
if not os.path.isfile(path):
|
||||
raise FileNotFoundError(path)
|
||||
spec = importlib.util.spec_from_file_location("_dl_under_test", path)
|
||||
if spec is None or spec.loader is None:
|
||||
raise ImportError("no import spec for %s" % path)
|
||||
module = importlib.util.module_from_spec(spec)
|
||||
spec.loader.exec_module(module)
|
||||
return module
|
||||
|
||||
|
||||
def levenshtein(a, b):
|
||||
"""Plain Levenshtein: the upper bound on DL and one of the two mutants."""
|
||||
if not a:
|
||||
return len(b)
|
||||
if not b:
|
||||
return len(a)
|
||||
prev = list(range(len(b) + 1))
|
||||
for i, ca in enumerate(a, 1):
|
||||
cur = [i]
|
||||
for j, cb in enumerate(b, 1):
|
||||
cur.append(min(prev[j] + 1, cur[-1] + 1, prev[j - 1] + (ca != cb)))
|
||||
prev = cur
|
||||
return prev[-1]
|
||||
|
||||
|
||||
def osa(a, b):
|
||||
"""Restricted edit distance (optimal string alignment) -- mutant one."""
|
||||
la, lb = len(a), len(b)
|
||||
d = [[0] * (lb + 1) for _ in range(la + 1)]
|
||||
for i in range(la + 1):
|
||||
d[i][0] = i
|
||||
for j in range(lb + 1):
|
||||
d[0][j] = j
|
||||
for i in range(1, la + 1):
|
||||
for j in range(1, lb + 1):
|
||||
cost = 0 if a[i - 1] == b[j - 1] else 1
|
||||
d[i][j] = min(d[i - 1][j] + 1, d[i][j - 1] + 1, d[i - 1][j - 1] + cost)
|
||||
if i > 1 and j > 1 and a[i - 1] == b[j - 2] and a[i - 2] == b[j - 1]:
|
||||
d[i][j] = min(d[i][j], d[i - 2][j - 2] + 1)
|
||||
return d[la][lb]
|
||||
|
||||
|
||||
def bfs_dl(a, b, cap):
|
||||
"""Exact DL by breadth-first search over the edit graph, bounded by `cap`."""
|
||||
if a == b:
|
||||
return 0
|
||||
alpha = sorted(set(a) | set(b))
|
||||
frontier = {a}
|
||||
seen = {a}
|
||||
for depth in range(1, cap + 1):
|
||||
nxt = set()
|
||||
for s in frontier:
|
||||
ls = len(s)
|
||||
for i in range(ls): # delete
|
||||
t = s[:i] + s[i + 1:]
|
||||
if t not in seen:
|
||||
if t == b:
|
||||
return depth
|
||||
seen.add(t)
|
||||
nxt.add(t)
|
||||
for i in range(ls + 1): # insert
|
||||
for c in alpha:
|
||||
t = s[:i] + c + s[i:]
|
||||
if t not in seen:
|
||||
if t == b:
|
||||
return depth
|
||||
seen.add(t)
|
||||
nxt.add(t)
|
||||
for i in range(ls): # substitute
|
||||
for c in alpha:
|
||||
if c != s[i]:
|
||||
t = s[:i] + c + s[i + 1:]
|
||||
if t not in seen:
|
||||
if t == b:
|
||||
return depth
|
||||
seen.add(t)
|
||||
nxt.add(t)
|
||||
for i in range(ls - 1): # transpose adjacent
|
||||
if s[i] != s[i + 1]:
|
||||
t = s[:i] + s[i + 1] + s[i] + s[i + 2:]
|
||||
if t not in seen:
|
||||
if t == b:
|
||||
return depth
|
||||
seen.add(t)
|
||||
nxt.add(t)
|
||||
frontier = nxt
|
||||
if not frontier:
|
||||
break
|
||||
return cap
|
||||
|
||||
|
||||
def corpus():
|
||||
"""Every string over {a,b} up to length 4, every string over {a,b,c} up to
|
||||
length 3, plus a seeded random sample of length 4-6 strings. Deterministic:
|
||||
the same pairs, in the same order, on every run."""
|
||||
import itertools
|
||||
|
||||
def explode(alpha, upto):
|
||||
return ["".join(t) for n in range(upto + 1) for t in itertools.product(alpha, repeat=n)]
|
||||
|
||||
pool = sorted(set(explode("ab", 4)) | set(explode("abc", 3)))
|
||||
rng = random.Random(1337)
|
||||
long_words = ["".join(rng.choice("abc") for _ in range(rng.randint(4, 6))) for _ in range(60)]
|
||||
pool = sorted(set(pool) | set(long_words))
|
||||
pairs = [(x, y) for x in pool for y in pool if len(x) <= 4 and len(y) <= 4]
|
||||
pairs += [(rng.choice(pool), rng.choice(pool)) for _ in range(400)]
|
||||
return pairs
|
||||
|
||||
|
||||
|
||||
def run(module, pairs, teeth):
|
||||
dl = module.damerau_levenshtein
|
||||
bad = []
|
||||
bfs_effort = 0
|
||||
t0 = time.time()
|
||||
for a, b in pairs:
|
||||
cap = levenshtein(a, b)
|
||||
if cap == 0:
|
||||
continue
|
||||
got = dl(a, b)
|
||||
want = bfs_dl(a, b, cap)
|
||||
bfs_effort += 1
|
||||
if got != want:
|
||||
bad.append((a, b, got, want))
|
||||
dy = time.time() - t0
|
||||
|
||||
print("corpus: %d pairs, %d graded by BFS, %.2fs" % (len(pairs), bfs_effort, dy))
|
||||
if bad:
|
||||
for a, b, got, want in bad[:10]:
|
||||
print("MISMATCH dl(%r,%r)=%d oracle=%d" % (a, b, got, want))
|
||||
print("FAIL: %d pair(s) disagree with the BFS oracle" % len(bad))
|
||||
return 1
|
||||
print("PASS: 0 mismatches against the BFS oracle")
|
||||
|
||||
# Known constants, stated separately so a failure names itself.
|
||||
for a, b, want in (("ca", "abc", 2), ("abc", "acb", 1), ("ab", "ba", 1), ("", "", 0)):
|
||||
got = dl(a, b)
|
||||
if got != want:
|
||||
print("FAIL constant dl(%r,%r)=%d want %d" % (a, b, got, want))
|
||||
return 1
|
||||
print("PASS: constants dl('ca','abc')=2 dl('abc','acb')=1 dl('ab','ba')=1 dl('','')=0")
|
||||
|
||||
if not teeth:
|
||||
return 0
|
||||
|
||||
# The corpus must be able to tell true DL from the two cheap impostors.
|
||||
caught = {}
|
||||
for name, impl in (("osa", osa), ("lev", levenshtein)):
|
||||
diff = [(a, b, impl(a, b), dl(a, b)) for a, b in pairs if impl(a, b) != dl(a, b)]
|
||||
caught[name] = len(diff)
|
||||
print("teeth: osa disagrees on %d pair(s), lev on %d pair(s)" % (caught["osa"], caught["lev"]))
|
||||
failed = False
|
||||
if caught["osa"] == 0:
|
||||
print("FAIL: corpus never separates true DL from OSA (gate has no teeth)")
|
||||
failed = True
|
||||
if caught["lev"] == 0:
|
||||
print("FAIL: corpus never separates true DL from plain Levenshtein")
|
||||
failed = True
|
||||
if not failed:
|
||||
witness = next((a, b, osa(a, b), dl(a, b)) for a, b in pairs if osa(a, b) != dl(a, b))
|
||||
print("PASS: OSA witness dl(%r,%r)=%d vs osa=%d" % (witness[0], witness[1], witness[3], witness[2]))
|
||||
return 1 if failed else 0
|
||||
|
||||
|
||||
def main(argv=None):
|
||||
ap = argparse.ArgumentParser(description=__doc__.splitlines()[0])
|
||||
ap.add_argument("--no-teeth", action="store_true", help="skip the mutant-corpus proof")
|
||||
ap.add_argument("--module", default=MODULE,
|
||||
help="path to the module under test (default: beside this file); "
|
||||
"used to prove the gate reds on a broken copy")
|
||||
args = ap.parse_args(argv)
|
||||
try:
|
||||
module = load_module(args.module)
|
||||
except Exception as exc: # noqa: BLE001 - cannot grade, name the reason
|
||||
print("could not grade: cannot import %s: %r" % (args.module, exc), file=sys.stderr)
|
||||
return 2
|
||||
if not hasattr(module, "damerau_levenshtein"):
|
||||
print("could not grade: module has no damerau_levenshtein()", file=sys.stderr)
|
||||
return 2
|
||||
return run(module, corpus(), not args.no_teeth)
|
||||
|
||||
|
||||
if __name__ == "__main__":
|
||||
sys.exit(main())
|
||||
Reference in new issue
Block a user