diff --git a/.github/scripts/bench_ab.py b/.github/scripts/bench_ab.py new file mode 100755 index 00000000..bf8f96a9 --- /dev/null +++ b/.github/scripts/bench_ab.py @@ -0,0 +1,254 @@ +#!/usr/bin/env python3 +"""A/B benchmark of two commits on the same machine. + +Builds the bench binaries for BASE and HEAD once each, both from the same +worktree path and target dir (checkout base, build, copy the executables +out; checkout head, build, copy out) so the two sides differ only in the +change under test: building the sides at different paths or into different +target dirs changes crate hashes and code layout, which alone moved cases by +5-25% in an A/A run. Then runs them for ROUNDS rounds. Benches run in parallel, each on its own +core from BENCH_CPUS (the base and head runs of a bench share that core, back +to back, alternating which side goes first each round). As soon as both +sides of a bench have run in a round, its compare table (per-round divan medians averaged over the rounds +finished so far, via benches/divan_fmt.py) is printed and saved as +$BENCH_OUT/cmp-.txt; $BENCH_OUT/compare.txt, the concatenation, is +rewritten after every completed round, as are $BENCH_OUT/summary.md (one row +per bench plus the cases that moved more than THRESH, which is what +pr_comment.py posts to the PR) and summary.json. Progress lines go to +$BENCH_OUT/progress.txt. + +usage: bench_ab.py + +env: BENCH_ROUNDS rounds per side (default 3) + BENCHES space separated bench targets (default: the set used in BENCH_BUGFIXES) + BENCH_CPUS cores to pin to, e.g. "0,2,4-8"; one bench pair runs per core at a time + (default: one SMT thread per physical core, every other core, at most 16) + BENCH_OUT output directory (default ./bench-out) + DIVAN_SAMPLE_COUNT sample count for benches that do not set their own (default 40) + CARGO_TARGET_DIR parent of the shared bench target dir (default ./target) +""" +import json, math, os, re, shutil, statistics, subprocess, sys, threading, time, tomllib +from concurrent.futures import ThreadPoolExecutor +from pathlib import Path +from queue import Queue + +DEFAULT_BENCHES = 'shakespeare cities sparse_keys binary_keys superdense_keys act_paths zipper_head_owned product_zipper' +THRESH = 0.05 # a case is listed in the summary when |change| exceeds this + + +def log(*a, **kw): + print(*a, flush=True, **kw) + + +def git(*args, cwd=None): + return subprocess.run(['git', *args], cwd=cwd, check=True, text=True, capture_output=True).stdout.strip() + + +def parse_cpus(spec): + cpus = [] + for part in spec.replace(' ', '').split(','): + a, _, b = part.partition('-') + cpus += list(range(int(a), int(b or a) + 1)) + return cpus + + +def default_cpus(limit=16): + """One SMT thread per physical core, every other core (spreads over the L3 complexes), at most `limit`.""" + cores = {} + for d in sorted(Path('/sys/devices/system/cpu').glob('cpu[0-9]*'), key=lambda d: int(d.name[3:])): + core = (d / 'topology' / 'core_id') + if core.is_file(): + cores.setdefault(int(core.read_text()), int(d.name[3:])) + first = [cpu for _, cpu in sorted(cores.items())] + return (first[::2] or [0])[:limit] + + +class Bench: + def __init__(self, base, head): + self.repo = Path.cwd() + self.base_sha, self.head_sha = base, head + self.rounds = int(os.environ.get('BENCH_ROUNDS', 3)) + self.benches = os.environ.get('BENCHES', DEFAULT_BENCHES).split() + self.cpus = parse_cpus(os.environ['BENCH_CPUS']) if os.environ.get('BENCH_CPUS') else default_cpus() + self.lock = threading.Lock() # serialises log/progress output from the workers + self.out = Path(os.environ.get('BENCH_OUT', self.repo / 'bench-out')).resolve() + self.target = Path(os.environ.get('CARGO_TARGET_DIR', self.repo / 'target')).resolve() + self.src = self.out / 'src' # one worktree for both sides + self.bins = {} + self.results = {} # bench -> {'group/case': {'base': ns, 'head': ns, 'pct': float}} + os.environ.setdefault('DIVAN_SAMPLE_COUNT', '40') + sys.path.insert(0, str(self.repo / 'benches')) + import divan_fmt + self.fmt = divan_fmt + + def progress(self, msg): + with self.lock, open(self.out / 'progress.txt', 'a') as f: + f.write(f'{time.strftime("%H:%M:%S", time.gmtime())} {msg}\n') + + def short(self, sha): + return git('rev-parse', '--short', sha, cwd=self.repo) + + def cleanup(self): + subprocess.run(['git', 'worktree', 'remove', '--force', str(self.src)], cwd=self.repo, + capture_output=True) + + def required_features(self, src): + """Features the requested benches declare via required-features, limited to those the tree has.""" + t = tomllib.loads((src / 'Cargo.toml').read_text()) + have = set(t.get('features', {})) + need = set() + for b in t.get('bench', []): + if b.get('name') in self.benches: + need |= set(b.get('required-features', [])) + return sorted(need & have) + + def build_side(self, side, sha): + """Check `sha` out in the shared worktree, build, and copy the bench executables to bins//.""" + src = self.src + git('checkout', '--detach', '-f', sha, cwd=src) + feats = self.required_features(src) + target = self.target / 'ab' + log(f'== building {side} ({self.short(sha)}) in {src} into {target}' + + (f' with features {",".join(feats)}' if feats else '')) + cmd = ['cargo', 'bench', '--no-run', '--message-format=json', '--target-dir', str(target)] + for b in self.benches: + cmd += ['--bench', b] + if feats: + cmd += ['--features', ','.join(feats)] + with open(self.out / f'build-{side}.log', 'w') as err: + p = subprocess.run(cmd, cwd=src, stdout=subprocess.PIPE, stderr=err, text=True) + if p.returncode: + sys.exit(f'build of {side} failed:\n' + tail(self.out / f'build-{side}.log')) + exes = {} + for line in p.stdout.splitlines(): + m = json.loads(line) + if m.get('reason') == 'compiler-artifact' and m.get('executable') and 'bench' in m['target']['kind']: + exes[m['target']['name']] = m['executable'] + missing = [b for b in self.benches if b not in exes] + if missing: + sys.exit(f'no executable for bench(es) {missing} on {side}') + bindir = self.out / 'bins' / side + bindir.mkdir(parents=True, exist_ok=True) + self.bins[side] = {} + for b in self.benches: + shutil.copy2(exes[b], bindir / b) + self.bins[side][b] = str(bindir / b) + (self.out / f'bins-{side}.txt').write_text(''.join(f'{b} {exes[b]}\n' for b in self.benches)) + + def run(self, side, bench, rnd, cpu): + t0 = time.time() + with open(self.out / f'{side}-{bench}-r{rnd}.txt', 'w') as out, open(self.out / f'run-{side}-{bench}.log', 'a') as err: + subprocess.run(['taskset', '-c', str(cpu), self.bins[side][bench], '--bench'], + cwd=self.repo, stdout=out, stderr=err, check=True) + self.progress(f'round {rnd}/{self.rounds} {bench} {side} {time.time() - t0:.0f}s cpu {cpu}') + + def run_pair(self, bench, rnd, free): + """Both sides of one bench, back to back on one core taken from the pool, then its compare table.""" + cpu = free.get() + try: + for side in (('base', 'head') if rnd % 2 else ('head', 'base')): + with self.lock: + log(f'== round {rnd}/{self.rounds} {bench} {side} (cpu {cpu})') + self.run(side, bench, rnd, cpu) + self.compare_bench(bench, rnd) + finally: + free.put(cpu) + + def compare_bench(self, bench, rounds_so_far): + """Average each side's rounds so far, compare medians, save and print the table.""" + avg = {} + for side in ('base', 'head'): + files = sorted(self.out.glob(f'{side}-{bench}-r*.txt')) + data = [self.fmt.parse_divan_output(f.read_text()) for f in files] + avg[side] = self.fmt.average_fields(data) + (self.out / f'{side}-{bench}-avg.txt').write_text(self.fmt.render_divan_table(avg[side]) + '\n') + cmp = self.fmt.compare_fields(avg['base'], avg['head'], 'median_ns') + self.results[bench] = {f'{g}/{c}': {'base': r['base'], 'head': r['other'], 'pct': r['pct']} for (g, c), r in cmp.items()} + table = re.sub(r'\x1b\[[0-9;]*m', '', self.fmt.render_divan_table(cmp)) + text = (f'{bench} (base {self.short(self.base_sha)} head {self.short(self.head_sha)}' + f' rounds {rounds_so_far} median ns)\n{table}\n\n') + (self.out / f'cmp-{bench}.txt').write_text(text) + with self.lock: + log(text, end='') + + def compare_rounds(self, rounds_so_far): + tmp = self.out / 'compare.tmp' + tmp.write_text(''.join((self.out / f'cmp-{b}.txt').read_text() for b in self.benches)) + tmp.rename(self.out / 'compare.txt') + (self.out / 'summary.json').write_text(json.dumps( + {'base': self.short(self.base_sha), 'head': self.short(self.head_sha), 'rounds': rounds_so_far, + 'benches': self.results})) + (self.out / 'summary.md').write_text(self.render_summary(rounds_so_far)) + + def render_summary(self, rounds_so_far): + """One row per bench, then the cases beyond THRESH, collapsed.""" + def pct(v): + return f'{v:+.1%}' + L = [f'base {self.short(self.base_sha)} → head {self.short(self.head_sha)}, {rounds_so_far} round(s), ' + f'median of each run averaged; negative is faster', '', + '| bench | cases | geomean | largest gain | largest loss | >5% faster | >5% slower |', + '|---|---:|---:|---|---|---:|---:|'] + movers = [] + for b in self.benches: + cases = self.results.get(b, {}) + if not cases: + L.append(f'| {b} | 0 | | | | | |') + continue + ratios = [r['head'] / r['base'] for r in cases.values() if r['base']] + geo = math.exp(statistics.fmean(map(math.log, ratios))) - 1 if ratios else 0.0 + lo = min(cases.items(), key=lambda kv: kv[1]['pct']) + hi = max(cases.items(), key=lambda kv: kv[1]['pct']) + faster = sum(r['pct'] < -THRESH for r in cases.values()) + slower = sum(r['pct'] > THRESH for r in cases.values()) + L.append(f'| {b} | {len(cases)} | {pct(geo)} | {pct(lo[1]["pct"])} `{lo[0]}` | {pct(hi[1]["pct"])} `{hi[0]}` ' + f'| {faster} | {slower} |') + movers += [(b, name, r) for name, r in cases.items() if abs(r['pct']) > THRESH] + movers.sort(key=lambda m: -abs(m[2]['pct'])) + if movers: + L += ['', f'
{len(movers)} case(s) moved more than {THRESH:.0%}', '', + '| bench | case | base | head | change |', '|---|---|---:|---:|---:|'] + L += [f'| {b} | `{name}` | {self.fmt.format_ns(r["base"])} | {self.fmt.format_ns(r["head"])} | {pct(r["pct"])} |' + for b, name, r in movers[:60]] + if len(movers) > 60: + L.append(f'| | … and {len(movers) - 60} more, see compare.txt in the bench-out artifact | | | |') + L += ['', '
'] + L += ['', 'Full tables per bench are in the job log and the bench-out artifact.'] + return '\n'.join(L) + '\n' + + def main(self): + self.out.mkdir(parents=True, exist_ok=True) + for f in self.out.iterdir(): + if f.suffix in ('.txt', '.log', '.json'): + f.unlink() + self.cleanup() + shutil.rmtree(self.out / 'bins', ignore_errors=True) + try: + git('worktree', 'add', '--detach', str(self.src), self.base_sha, cwd=self.repo) + self.progress(f'plan: {self.rounds} round(s) x base/head x [{" ".join(self.benches)}], ' + f'{min(len(self.cpus), len(self.benches))} at a time on cpus {",".join(map(str, self.cpus))}') + self.progress(f'building base {self.short(self.base_sha)}') + self.build_side('base', self.base_sha) + self.progress(f'building head {self.short(self.head_sha)}') + self.build_side('head', self.head_sha) + free = Queue() + for cpu in self.cpus: + free.put(cpu) + for rnd in range(1, self.rounds + 1): + with ThreadPoolExecutor(min(len(self.cpus), len(self.benches))) as pool: + for r in pool.map(lambda b: self.run_pair(b, rnd, free), self.benches): + pass # re-raises a worker's exception + self.compare_rounds(rnd) + self.progress(f'round {rnd}/{self.rounds} done, compare.txt refreshed') + log(f'== final compare over {self.rounds} round(s): {self.out / "compare.txt"}') + finally: + self.cleanup() + + +def tail(path, n=30): + return '\n'.join(Path(path).read_text().splitlines()[-n:]) + + +if __name__ == '__main__': + if len(sys.argv) != 3: + sys.exit('usage: bench_ab.py ') + Bench(sys.argv[1], sys.argv[2]).main() diff --git a/.github/scripts/fuzz_ab.py b/.github/scripts/fuzz_ab.py new file mode 100755 index 00000000..25dedaa8 --- /dev/null +++ b/.github/scripts/fuzz_ab.py @@ -0,0 +1,288 @@ +#!/usr/bin/env python3 +"""Differential fuzz of two commits against the Lean model, as a regression gate. + +The crate at HEAD has known divergences from the model, so "zero divergences" +cannot be the bar. Instead both commits are run on identical inputs, and an +input that diverges on HEAD but not on BASE is reported as a GitHub warning +annotation (the job stays green) or, with FUZZ_STRICT=1, fails the job. A +run that does not finish always fails the job. For the first REPROS newly +diverging inputs with distinct first-differing operations, the input is +shrunk with lean/shrink.py and a standalone Rust reproducer is emitted with +`pathmap_trace --repro` into the summary and $FUZZ_OUT/repro/. The harness +(differential/) and the model (lean/) are taken from HEAD for both sides, so +the only thing that differs is the crate under test in src/. If BASE cannot +be built with HEAD's harness, BASE's own harness is tried; if that fails too +there is no baseline, which is reported loudly and does not fail the job. + +usage: fuzz_ab.py + +env: FUZZ_INPUTS random programs, model vs crate (default 20000) + FUZZ_ACT_INPUTS random programs with the ACT read side (default 5000; 0 skips) + FUZZ_SEED (default 7) + FUZZ_JOBS worker processes (default 16) + FUZZ_STRICT 1 = new divergences fail the job instead of warning (default 0) + FUZZ_REPROS newly diverging inputs to shrink and turn into Rust (default 3) + FUZZ_OUT output dir (default ./fuzz-out) + CARGO_TARGET_DIR parent of the per-side target dirs (default ./target) + LAKE_CACHE optional dir to keep lean's .lake build dirs across runs +""" +import os, re, shutil, subprocess, sys, time +from pathlib import Path + +FAIL_RE = re.compile(r'^FAIL (\S+) \[saved ([^\]]*)\]: (.*)$') +SUMMARY_RE = re.compile(r'^(\d+)/(\d+) inputs agree \((\d+) hit known bugs, (\d+) new divergences\)') +KNOWN_RE = re.compile(r'^ known x(\d+): (.*)$') + + +def log(*a, **kw): + print(*a, flush=True, **kw) + + +def git(*args, cwd=None, check=True): + return subprocess.run(['git', *args], cwd=cwd, check=check, text=True, capture_output=True).stdout.strip() + + +def tail(path, n=30): + return '\n'.join(Path(path).read_text().splitlines()[-n:]) + + +class Fuzz: + def __init__(self, base, head): + self.repo = Path.cwd() + self.base_sha, self.head_sha = base, head + self.inputs = int(os.environ.get('FUZZ_INPUTS', 20000)) + self.act_inputs = int(os.environ.get('FUZZ_ACT_INPUTS', 5000)) + self.seed = os.environ.get('FUZZ_SEED', '7') + self.jobs = os.environ.get('FUZZ_JOBS', '16') + self.out = Path(os.environ.get('FUZZ_OUT', self.repo / 'fuzz-out')).resolve() + self.target = Path(os.environ.get('CARGO_TARGET_DIR', self.repo / 'target')).resolve() + self.lake_cache = os.environ.get('LAKE_CACHE') + self.strict = os.environ.get('FUZZ_STRICT', '0') == '1' + self.repros = int(os.environ.get('FUZZ_REPROS', 3)) + self.base_src = self.out / 'src-base' + self.modes = [('crate', self.inputs, [])] + if self.act_inputs > 0: + self.modes.append(('act', self.act_inputs, ['--act'])) + + def short(self, sha): + return git('rev-parse', '--short', sha, cwd=self.repo) + + def cleanup(self): + subprocess.run(['git', 'worktree', 'remove', '--force', str(self.base_src)], cwd=self.repo, + capture_output=True) + + def build_side(self, side, src): + """lake build + cargo build into this side's target dir. Returns False on failure.""" + if self.lake_cache: + cache = Path(self.lake_cache) / side + cache.mkdir(parents=True, exist_ok=True) + lake = src / 'lean' / '.lake' + if lake.is_symlink() or lake.exists(): + lake.unlink() if lake.is_symlink() else shutil.rmtree(lake) + lake.symlink_to(cache) + for name, cmd, cwd in (('lake', ['lake', 'build'], src / 'lean'), + ('build', ['cargo', 'build', '--release', '-p', 'differential', + '--target-dir', str(self.target / f'fuzz-{side}')], src)): + logf = self.out / f'{name}-{side}.log' + t0 = time.time() + with open(logf, 'w') as f: + p = subprocess.run(cmd, cwd=cwd, stdout=f, stderr=subprocess.STDOUT) + if p.returncode: + log(f'{name} for {side} failed:\n{tail(logf)}') + return False + log(f' {" ".join(cmd[:2])} for {side}: ok in {time.time() - t0:.0f}s (log: {logf.name})') + return True + + def prepare_base(self): + """Build base with head's harness and model; fall back to base's own. Returns the baseline kind.""" + log(f"== building base ({self.short(self.base_sha)}) with head's differential/ and lean/") + for d in ('differential', 'lean'): + shutil.rmtree(self.base_src / d) + shutil.copytree(self.repo / d, self.base_src / d, symlinks=True, + ignore=shutil.ignore_patterns('.lake')) + if self.build_side('base', self.base_src): + return 'head-harness' + log("== head's harness does not build against base; trying base's own") + git('checkout', '--', 'differential', 'lean', cwd=self.base_src) + git('clean', '-fdq', '--', 'differential', 'lean', cwd=self.base_src) + return 'base-harness' if self.build_side('base', self.base_src) else 'none' + + def run_side(self, side, src, label, n, flags): + env = dict(os.environ, + TMPDIR=str(self.out / f'fails-{side}-{label}'), + PATHMAP_TRACE=str(self.target / f'fuzz-{side}' / 'release' / 'pathmap_trace'), + PATHMAP_ACT_TRACE=str(self.target / f'fuzz-{side}' / 'release' / 'act_trace')) + Path(env['TMPDIR']).mkdir(parents=True, exist_ok=True) + log(f'== fuzz {label} {side}: {n} inputs, seed {self.seed}') + outf = self.out / f'fuzz-{label}-{side}.txt' + with open(outf, 'w') as f: + subprocess.run([str(src / 'lean' / 'differential.py'), '--random', str(n), '--seed', self.seed, + '--maxlen', '300', '--max-fails', '0', '-j', self.jobs, *flags], + cwd=src, env=env, stdout=f, stderr=subprocess.STDOUT) + text = outf.read_text() + info = [l for l in text.splitlines() if SUMMARY_RE.match(l) or 'child restart' in l] + log('\n'.join(info) if info else tail(outf, 5)) + + def parse(self, label, side): + """fails: name -> {'path', 'msg', 'detail'}; summary: (agree, total, known, new); known: class -> count.""" + fails, summary, last, known = {}, None, None, {} + p = self.out / f'fuzz-{label}-{side}.txt' + if p.is_file(): + for line in p.read_text().splitlines(): + if m := FAIL_RE.match(line): + last = fails[m.group(1)] = {'path': m.group(2), 'msg': m.group(3), 'detail': []} + elif line.startswith(' ') and last is not None: + last['detail'].append(line.strip()) # the "lean: ..." / "crate: ..." trace lines + else: + last = None + if m := SUMMARY_RE.match(line): + summary = tuple(map(int, m.groups())) + if m := KNOWN_RE.match(line): + known[m.group(2)] = int(m.group(1)) + return fails, summary, known + + @staticmethod + def kind(f): + """What diverged: the first-differing op from the model's trace line, else the message shape.""" + for d in f['detail']: + if d.startswith('lean:'): + parts = d.split() + if len(parts) > 1 and parts[1].startswith(('MAP', 'ROOT')): + return f'{parts[1]} (final state)' + if len(parts) > 2: + return parts[2] + return re.sub(r'\d+', 'N', f['msg']) + + def repro(self, label, name, f, flags): + """Shrink one newly diverging input and emit a Rust reproducer. Returns markdown.""" + rdir = self.out / 'repro' + rdir.mkdir(exist_ok=True) + stem = rdir / f'{label}-{name.replace("#", "_")}' + env = dict(os.environ, + PATHMAP_ORACLE=os.environ.get('PATHMAP_ORACLE') or str(self.repo / 'lean' / '.lake' / 'build' / 'bin' / 'pathmap-oracle'), + PATHMAP_TRACE=str(self.target / 'fuzz-head' / 'release' / 'pathmap_trace'), + PATHMAP_ACT_TRACE=str(self.target / 'fuzz-head' / 'release' / 'act_trace')) + small = stem.with_suffix('.min.bin') + note = '' + try: + r = subprocess.run([str(self.repo / 'lean' / 'shrink.py'), f['path'], '-o', str(small), *flags], + cwd=self.repo, env=env, capture_output=True, text=True, timeout=600) + sizes = next((l for l in r.stdout.splitlines() if ' -> ' in l and 'bytes' in l), None) + if r.returncode or not small.is_file(): + raise RuntimeError((r.stdout + r.stderr).strip().splitlines()[-1:] or ['shrink failed']) + note = sizes.split(', written')[0] if sizes else 'shrunk' + except (subprocess.TimeoutExpired, RuntimeError) as e: + shutil.copy(f['path'], small) + note = f'not shrunk ({e}); reproducer is for the full input' + r = subprocess.run([env['PATHMAP_TRACE'], '--repro', str(small)], capture_output=True, text=True) + code = r.stdout if r.returncode == 0 else f'// pathmap_trace --repro failed:\n// {r.stderr.strip()}' + stem.with_suffix('.rs').write_text(code) + act_note = ' (act mode: the harness reads map1 through an ArenaCompactTree; the reproducer uses a PathMap read zipper)' if flags else '' + log(f'== repro {label} {name}: {self.kind(f)}, {note}\n{code}') + return '\n'.join([f'
{name}: first differs at {self.kind(f)}, {note}{act_note}', '', + f"{f['msg']}", *[f' {d}' for d in f['detail']], '', '```rust', code.rstrip(), '```', '', '
', '']) + + def summarize(self, baseline): + """Write summary.md (with reproducers for the first few new divergences); return (new divergences, unfinished runs).""" + L = [f'# Differential fuzz: head {self.short(self.head_sha)} vs base {self.short(self.base_sha)}', '', '', ''] + if baseline == 'none': + L += ['**No baseline**: base could not be built with either harness, so only head was run and nothing is gated.', ''] + elif baseline == 'base-harness': + L += ["Base was built with its own harness and model (head's did not build against it), " + 'so harness changes may show up as differences.', ''] + new_total, unfinished = 0, 0 + for label, n, _ in self.modes: + hf, hs, hk = self.parse(label, 'head') + bf, bs, bk = self.parse(label, 'base') + L += [f'## {label}: {n} inputs, seed {self.seed}', '', + 'agree = model and crate match; known = the divergence matches a classified bug in ' + 'differential.py; new = it matches none. Only the new set is compared input by input below.', '', + '| side | agree | known | new divergences |', '|---|---:|---:|---:|'] + for side, s in (('head', hs), ('base', bs)): + if s and s[1] < n: + # differential.py reports against the inputs it actually ran, so a denominator + # below the requested count means the run stopped early (--max-fails). The two + # sides then covered different inputs and the comparison below is not a gate. + L.append(f'| {side} | {s[0]}/{s[1]} — **stopped early, {n - s[1]} input(s) not run** | {s[2]} | {s[3]} |') + unfinished += 1 + elif s: + L.append(f'| {side} | {s[0]}/{s[1]} | {s[2]} | {s[3]} |') + elif side == 'head' or baseline != 'none': + L.append(f'| {side} | run did not finish, see fuzz-{label}-{side}.txt | | |') + unfinished += 1 + if baseline != 'none' and hs and bs: + new = sorted(set(hf) - set(bf)) # names are random#NNNNN, so this is input order + fixed = sorted(set(bf) - set(hf)) + L += ['', f'{len(new)} input(s) diverge on head but not on base; {len(fixed)} diverge on base but not on head.'] + changed = sorted(((bk.get(k, 0), hk.get(k, 0), k) for k in set(bk) | set(hk) if bk.get(k, 0) != hk.get(k, 0)), + key=lambda t: -abs(t[0] - t[1])) + if changed: + L += ['', '### Known-class hits that changed', '', '| known class | base | head |', '|---|---:|---:|'] + L += [f'| {k[:100]} | {b} | {h} |' for b, h, k in changed[:10]] + if len(changed) > 10: + L.append(f'| … {len(changed) - 10} more | | |') + if new: + new_total += len(new) + log(f'::{"error" if self.strict else "warning"} title=Differential fuzz ({label})::{len(new)} input(s) diverge from the model on head ' + f'but not on base, e.g. {new[0]}: {hf[new[0]]["msg"][:150]}') + kinds = {} # first-differing op -> [input names], input order + for name in new: + kinds.setdefault(self.kind(hf[name]), []).append(name) + L += ['', f'### Newly diverging inputs (head only): {len(new)} input(s), {len(kinds)} kind(s)', '', + '| first differs at | inputs | first example |', '|---|---:|---|'] + for k, names in list(kinds.items())[:10]: + L.append(f'| `{k}` | {len(names)} | `{names[0]}`: {hf[names[0]]["msg"][:80]} |') + if len(kinds) > 10: + L.append(f'| … {len(kinds) - 10} more kind(s) | | see fuzz-{label}-head.txt |') + picked = [names[0] for names in kinds.values()][:self.repros] + if picked: + flags = next(fl for lb, _, fl in self.modes if lb == label) + L += ['', f'### Reproducers: first {len(picked)} distinct kind(s), shrunk', ''] + L += [self.repro(label, name, hf[name], flags) for name in picked] + if fixed: + L += ['', f'
{len(fixed)} input(s) fixed on head', ''] + L += [f'- `{name}`' for name in fixed[:50]] + L += ['', '
'] + L.append('') + if unfinished: + L[2] = '**FAIL: a fuzz run did not cover every input**' + elif new_total: + L[2] = f'**{"FAIL" if self.strict else "WARNING"}: {new_total} new divergence(s) relative to base**' + else: + L[2] = '**OK: no new divergences relative to base**' + text = '\n'.join(L) + '\n' + (self.out / 'summary.md').write_text(text) + findings = self.out / 'findings' # exists only when there is something to report + findings.unlink(missing_ok=True) + if new_total or unfinished: + findings.write_text(f'{new_total} new divergences, {unfinished} unfinished runs\n') + log(text, end='') + return new_total, unfinished + + def main(self): + self.out.mkdir(parents=True, exist_ok=True) + for f in self.out.iterdir(): + if f.suffix in ('.txt', '.log', '.md'): + f.unlink() + shutil.rmtree(self.out / 'repro', ignore_errors=True) + self.cleanup() + try: + git('worktree', 'add', '--detach', str(self.base_src), self.base_sha, cwd=self.repo) + log(f'== building head ({self.short(self.head_sha)})') + if not self.build_side('head', self.repo): + sys.exit(1) + baseline = self.prepare_base() + for label, n, flags in self.modes: + self.run_side('head', self.repo, label, n, flags) + if baseline != 'none': + self.run_side('base', self.base_src, label, n, flags) + new_total, unfinished = self.summarize(baseline) + return 1 if unfinished or (self.strict and new_total) else 0 + finally: + self.cleanup() + + +if __name__ == '__main__': + if len(sys.argv) != 3: + sys.exit('usage: fuzz_ab.py ') + sys.exit(Fuzz(sys.argv[1], sys.argv[2]).main()) diff --git a/.github/scripts/pr_comment.py b/.github/scripts/pr_comment.py new file mode 100755 index 00000000..5b685dbb --- /dev/null +++ b/.github/scripts/pr_comment.py @@ -0,0 +1,102 @@ +#!/usr/bin/env python3 +"""Create or update one job's comment on a pull request. + +One comment per pull request and job id, edited in place: a title with a +status, a link to the job that produced it, and the job's summary.md once it +exists. The first call of a run finds the PR's existing comment by the hidden +marker on its first line (so a re-run or a new push reuses it) or creates it, +and records the id in /comment_id; later calls in the same run go straight +to that id. Standard library only. + +usage: pr_comment.py [--id ID] [--title TITLE] [--dir DIR] + --id comment identity, one per job (default bench-ab) + --title heading before the status (default "Bench A/B vs base") + --dir dir holding summary.md, comment_id (default $BENCH_OUT) + --create-only-if FILE create the comment only when FILE exists; an existing comment is + always updated (so a clean run clears earlier findings) +env: GITHUB_TOKEN GITHUB_REPOSITORY GITHUB_RUN_ID RUNNER_NAME (provided by Actions) + GITHUB_SERVER_URL optional +""" +import argparse, json, os, sys, time, urllib.request +from pathlib import Path + +LIMIT = 65536 # GitHub's comment body cap + +ap = argparse.ArgumentParser() +ap.add_argument('--id', default='bench-ab') +ap.add_argument('--title', default='Bench A/B vs base') +ap.add_argument('--dir', default=os.environ.get('BENCH_OUT')) +ap.add_argument('--create-only-if') +ap.add_argument('pr') +ap.add_argument('status', nargs='?', default='') +args = ap.parse_args() +pr, status = args.pr, args.status +MARKER = f'' +out = Path(args.dir) +repo = os.environ['GITHUB_REPOSITORY'] +api = f'https://api.github.com/repos/{repo}' +headers = {'Authorization': f"Bearer {os.environ['GITHUB_TOKEN']}", + 'Accept': 'application/vnd.github+json', 'Content-Type': 'application/json'} +run_id = os.environ.get('GITHUB_RUN_ID', '') +run_url = f"{os.environ.get('GITHUB_SERVER_URL', 'https://github.com')}/{repo}/actions/runs/{run_id}" + + +def call(method, url, data=None): + req = urllib.request.Request(url, method=method, headers=headers, + data=json.dumps(data).encode() if data is not None else None) + with urllib.request.urlopen(req, timeout=30) as r: + return json.load(r) + + +def read(name): + p = out / name + return p.read_text() if p.is_file() else '' + + +def job_url(): + """Link to this job's log: the job in progress on this runner within the run. Cached per run.""" + cache = out / 'job_url' + if cache.is_file(): + return cache.read_text().strip() + url = run_url + try: + jobs = call('GET', f'{api}/actions/runs/{run_id}/jobs?per_page=100')['jobs'] + mine = [j for j in jobs if j.get('runner_name') == os.environ.get('RUNNER_NAME') and j.get('status') == 'in_progress'] + if mine: + url = mine[0]['html_url'] + cache.write_text(url) + except Exception as e: # the run link is a fine fallback + print(f'job lookup failed, using run link: {e}', file=sys.stderr) + return url + + +parts = [MARKER, f'### {args.title}: {status}', '', + f"[job log]({job_url()}) · {time.strftime('%Y-%m-%d %H:%M:%S', time.gmtime())} UTC"] +summary = read('summary.md') +if summary.startswith('# '): # the comment has its own heading + summary = summary.split('\n', 1)[1].lstrip('\n') if '\n' in summary else '' +if summary: + head = '\n'.join(parts) + room = LIMIT - len(head) - 200 + if len(summary) > room: + summary = summary[:room] + '\n\n… truncated; see the bench-out artifact\n' + parts += ['', summary.rstrip()] +body = '\n'.join(parts) + +id_file = out / 'comment_id' +if id_file.is_file(): + cid = id_file.read_text().strip() + how = 'updated' +else: + found = [c['id'] for c in call('GET', f'{api}/issues/{pr}/comments?per_page=100') if c['body'].startswith(MARKER)] + cid = found[0] if found else None + how = 'reused' if found else 'created' +if cid is None and args.create_only_if and not Path(args.create_only_if).exists(): + print(f'no comment yet and {args.create_only_if} is absent: nothing to report') + sys.exit(0) +if cid is None: + cid = call('POST', f'{api}/issues/{pr}/comments', {'body': body})['id'] +else: + call('PATCH', f'{api}/issues/comments/{cid}', {'body': body}) +id_file.write_text(str(cid)) +print(f'comment {cid} {how}: {len(body)} chars') diff --git a/.github/workflows/ci.yml b/.github/workflows/ci.yml new file mode 100644 index 00000000..90baa18e --- /dev/null +++ b/.github/workflows/ci.yml @@ -0,0 +1,253 @@ +name: CI + +on: + pull_request: + push: + branches: [master] + workflow_dispatch: + inputs: + base: + description: base ref to benchmark against + default: master + rounds: + description: bench rounds per side + default: "3" + fuzz_inputs: + description: random programs for the differential fuzzer + default: "20000" + benches: + description: space separated bench targets (empty = default set) + default: "" + +permissions: + contents: read + +# One workflow run per PR / branch; a new push cancels the one in progress. +concurrency: + group: ci-${{ github.event.pull_request.number || github.ref }} + cancel-in-progress: true + +env: + CARGO_TERM_COLOR: never + # CARGO_TARGET_DIR and LAKE_CACHE are deliberately not set here: they live under the runner + # user's $HOME, and values in this block are not shell expanded. Each job exports them from + # its toolchain step via $GITHUB_ENV, so a runner under any user works. + +jobs: + test: + name: tests + runs-on: [self-hosted, linux, x64] + timeout-minutes: 120 + steps: + - uses: actions/checkout@v5 + - name: toolchain + # rustup is installed per runner user on first use + run: | + [ -x "$HOME/.cargo/bin/rustup" ] || curl --proto '=https' --tlsv1.2 -sSf https://sh.rustup.rs | sh -s -- -y --profile minimal --default-toolchain none --no-modify-path + echo "$HOME/.cargo/bin" >> "$GITHUB_PATH" + echo "CARGO_TARGET_DIR=$HOME/cache/target" >> "$GITHUB_ENV" # persists outside _work, so builds stay incremental + export PATH="$HOME/.cargo/bin:$PATH" + rustup toolchain install stable --profile minimal + rustup default stable + rustc --version && cargo --version + - name: build + run: cargo build --release --all-targets + - name: unit + integration tests + run: cargo test --release + - name: tests with arena_compact + random + run: cargo test --release --features arena_compact,random + - name: doc tests + docs + run: cargo doc --no-deps + + bench: + name: bench A/B vs base + # Runs last, after the tests and the fuzz gate pass (skipped when either fails), on PRs + # and manual runs only; a push to master has nothing to compare against. + needs: [test, fuzz] + if: github.event_name == 'pull_request' || github.event_name == 'workflow_dispatch' + runs-on: [self-hosted, linux, x64] + timeout-minutes: 300 + permissions: + contents: read + pull-requests: write # for the progress comment; read-only on fork PRs, where commenting is skipped + steps: + - uses: actions/checkout@v5 + with: + fetch-depth: 0 + - name: toolchain + # rustup is installed per runner user on first use + run: | + [ -x "$HOME/.cargo/bin/rustup" ] || curl --proto '=https' --tlsv1.2 -sSf https://sh.rustup.rs | sh -s -- -y --profile minimal --default-toolchain none --no-modify-path + echo "$HOME/.cargo/bin" >> "$GITHUB_PATH" + echo "CARGO_TARGET_DIR=$HOME/cache/target" >> "$GITHUB_ENV" # persists outside _work, so builds stay incremental + export PATH="$HOME/.cargo/bin:$PATH" + rustup toolchain install stable --profile minimal + rustup default stable + - name: resolve base + id: base + run: | + if [ "${{ github.event_name }}" = pull_request ]; then + sha=${{ github.event.pull_request.base.sha }} + else + sha=$(git rev-parse "origin/${{ inputs.base }}" 2>/dev/null || git rev-parse "${{ inputs.base }}") + fi + echo "sha=$sha" >> "$GITHUB_OUTPUT" + - name: A/B bench + env: + BENCH_ROUNDS: ${{ inputs.rounds || '3' }} + BENCHES: ${{ inputs.benches }} + BENCH_OUT: ${{ runner.temp }}/bench-out + GITHUB_TOKEN: ${{ github.token }} + # Only same-repo PRs get a writable token; on fork PRs the comment calls fail and are ignored. + PR: ${{ github.event.pull_request.number }} + run: | + # an empty BENCHES must fall through to the script's default set + [ -n "$BENCHES" ] || unset BENCHES + mkdir -p "$BENCH_OUT" + comment() { [ -z "$PR" ] || python3 .github/scripts/pr_comment.py "$PR" "$1" || true; } + comment "running" + if .github/scripts/bench_ab.py "${{ steps.base.outputs.sha }}" "${{ github.sha }}"; then + comment "done" + else + comment "failed, see the job log"; exit 1 + fi + - name: summary + if: always() + run: | + f="${{ runner.temp }}/bench-out/summary.md" + [ -s "$f" ] && cat "$f" >> "$GITHUB_STEP_SUMMARY" || true + - uses: actions/upload-artifact@v7 + if: always() + with: + name: bench-out + path: | + ${{ runner.temp }}/bench-out/*.txt + ${{ runner.temp }}/bench-out/summary.* + if-no-files-found: ignore + + lean: + name: Lean model, proofs and checks + # `lake build` type-checks the theorems in lean/PathMapModel/Spec.lean and evaluates every + # `#guard` (the metamorphic laws over the fixture battery and the regression fixtures), so + # a broken law or fixture fails the build. Lean only warns on `sorry`, so that is checked + # for separately. + runs-on: [self-hosted, linux, x64] + timeout-minutes: 30 + steps: + - uses: actions/checkout@v5 + - name: toolchain + # elan is installed per runner user on first use and fetches the Lean pinned by lean/lean-toolchain + run: | + [ -x "$HOME/.elan/bin/elan" ] || curl https://elan.lean-lang.org/elan-init.sh -sSf | sh -s -- -y --default-toolchain none --no-modify-path + echo "$HOME/.elan/bin" >> "$GITHUB_PATH" + export PATH="$HOME/.elan/bin:$PATH" + (cd lean && lean --version && lake --version) + - name: build the model, check proofs and guards + run: | + # checkout wipes ignored files, so keep lake's build dir in the persistent cache + mkdir -p "$HOME"/cache/lean-lake/proofs + ln -sfn "$HOME"/cache/lean-lake/proofs lean/.lake + cd lean + lake build 2>&1 | tee ../lake.log + test "${PIPESTATUS[0]}" -eq 0 + - name: no sorry, no unexpected axioms + run: | + if grep -n 'declaration uses .sorry.' lake.log; then + echo "::error::a declaration uses sorry"; exit 1 + fi + if grep -rn "\bsorry\b\|^axiom " lean/PathMapModel lean/Main.lean; then + echo "::error::sorry or axiom in the model sources"; exit 1 + fi + - name: summary + if: always() + run: | + { + echo "### Lean model" + echo + echo "| file | theorems | guards |" + echo "|---|---:|---:|" + for f in lean/PathMapModel/*.lean; do + t=$(grep -c '^theorem\|^lemma' "$f" || true); g=$(grep -c '#guard' "$f" || true) + [ "$t$g" = "00" ] || echo "| $(basename "$f") | $t | $g |" + done + echo + echo "$(grep -c 'declaration uses' lake.log || true) declaration(s) use sorry; $(grep -c '^warning' lake.log || true) warning(s) from lake build." + } >> "$GITHUB_STEP_SUMMARY" + + fuzz: + name: differential fuzz vs Lean model + # Regression check: head and base run on identical inputs; an input on which head diverges + # from the model but base did not is reported as a warning annotation (master has known + # divergences). Set FUZZ_STRICT=1 below to make that fail the job instead. + # Ordered after the tests but not gated on them: findings are warnings, and a PR whose + # tests fail is exactly one whose divergences are worth seeing. + needs: test + if: ${{ !cancelled() && (github.event_name == 'pull_request' || github.event_name == 'workflow_dispatch') }} + runs-on: [self-hosted, linux, x64] + timeout-minutes: 90 + permissions: + contents: read + pull-requests: write # for the fuzz comment; read-only on fork PRs, where commenting is skipped + steps: + - uses: actions/checkout@v5 + with: + fetch-depth: 0 + - name: toolchains + # Everything is installed per runner user on first use: rustup and elan into $HOME, + # then the Rust toolchain and the Lean pinned by lean/lean-toolchain. + run: | + [ -x "$HOME/.cargo/bin/rustup" ] || curl --proto '=https' --tlsv1.2 -sSf https://sh.rustup.rs | sh -s -- -y --profile minimal --default-toolchain none --no-modify-path + [ -x "$HOME/.elan/bin/elan" ] || curl https://elan.lean-lang.org/elan-init.sh -sSf | sh -s -- -y --default-toolchain none --no-modify-path + export PATH="$HOME/.cargo/bin:$HOME/.elan/bin:$PATH" + echo "$HOME/.cargo/bin" >> "$GITHUB_PATH" + echo "$HOME/.elan/bin" >> "$GITHUB_PATH" + echo "CARGO_TARGET_DIR=$HOME/cache/target" >> "$GITHUB_ENV" # persists outside _work, so builds stay incremental + echo "LAKE_CACHE=$HOME/cache/lean-lake" >> "$GITHUB_ENV" # checkout wipes ignored files such as lean/.lake + rustup toolchain install stable --profile minimal + rustup default stable + rustc --version && cargo --version + elan --version + (cd lean && lean --version && lake --version) # fetches the pinned Lean when it is missing + - name: resolve base + id: base + run: | + if [ "${{ github.event_name }}" = pull_request ]; then + sha=${{ github.event.pull_request.base.sha }} + else + sha=$(git rev-parse "origin/${{ inputs.base }}" 2>/dev/null || git rev-parse "${{ inputs.base }}") + fi + echo "sha=$sha" >> "$GITHUB_OUTPUT" + - name: fuzz head and base + id: fuzz + env: + FUZZ_INPUTS: ${{ inputs.fuzz_inputs || '20000' }} + FUZZ_OUT: ${{ runner.temp }}/fuzz-out + run: | + .github/scripts/fuzz_ab.py "${{ steps.base.outputs.sha }}" "${{ github.sha }}" + - name: comment on the PR + # One comment per PR for this job (separate from the bench one): verdict, per-mode tables, + # newly diverging inputs and their shrunk Rust reproducers. Created only when there is + # something to report; an existing comment is updated by a clean run. Skipped when there + # is no PR; fails silently on fork PRs, whose token is read-only. + if: always() && github.event.pull_request.number + env: + GITHUB_TOKEN: ${{ github.token }} + run: | + python3 .github/scripts/pr_comment.py --id fuzz --title "Differential fuzz vs Lean model" \ + --dir "${{ runner.temp }}/fuzz-out" --create-only-if "${{ runner.temp }}/fuzz-out/findings" \ + "${{ github.event.pull_request.number }}" "${{ steps.fuzz.outcome }}" || true + - name: summary + if: always() + run: | + f="${{ runner.temp }}/fuzz-out/summary.md" + [ -s "$f" ] && cat "$f" >> "$GITHUB_STEP_SUMMARY" || true + - uses: actions/upload-artifact@v7 + if: always() + with: + name: fuzz-out + path: | + ${{ runner.temp }}/fuzz-out/*.txt + ${{ runner.temp }}/fuzz-out/*.md + ${{ runner.temp }}/fuzz-out/fails-* + ${{ runner.temp }}/fuzz-out/repro + if-no-files-found: ignore diff --git a/.gitignore b/.gitignore index b845d407..790fe2ad 100644 --- a/.gitignore +++ b/.gitignore @@ -10,3 +10,4 @@ whisper_benches/logs # Lean build output and shrink.py scratch file /lean/.lake /lean/.shrink.bin +__pycache__/ diff --git a/differential/src/harness.rs b/differential/src/harness.rs index e0e47ca6..0b0d72d9 100644 --- a/differential/src/harness.rs +++ b/differential/src/harness.rs @@ -82,10 +82,13 @@ pub fn show_val(v: Option<&u64>) -> String { } /// Render a status the read source may have declined to produce. +/// +/// Only the default `ReadSource` impls return `None`, and only the ACT zipper +/// uses them, so the reason is always ACT mode. See `SKIP_REASONS`. pub fn show_status_opt(s: Option) -> String { match s { Some(s) => show_status(s).to_string(), - None => "skip".to_string(), + None => SKIP_ACT.to_string(), } } @@ -134,6 +137,33 @@ pub fn fingerprint + ZipperAbso ) } +/// Why an operation was skipped. Every `skip` in the trace carries one of +/// these, so a skipped op says which rule declined it rather than just that +/// something declined it. `lean/PathMapModel/Fuzz.lean` emits the same +/// tokens; the two must agree exactly or every input with a skip diverges. +/// +/// * `skip:act` — the ACT read source cannot be a merge source +/// (`ZipperInfallibleSubtries` is not implemented for it) or does not +/// implement the trait the op needs. +/// * `skip:at-root` — `to_next`/`to_prev_sibling_byte` at the zipper root, +/// where the native read zipper escapes its own root. +/// * `skip:k0` — a degenerate `k = 0`. +/// * `skip:empty-focus` — the focus has nothing below it, where the op's +/// behaviour is a function of node materialisation rather than trie state. +/// * `skip:empty-path` — `insert_prefix("")`, which destroys the subtrie. +/// * `skip:off-root-prune` — a prune on a write zipper not rooted at the map +/// root, where the depth pruned is a function of internal node layout. +/// * `skip:quarantined` — the op is disabled outright (op 54). +/// +/// Each is recorded in lean/FINDINGS.md and commented at its site. +pub const SKIP_ACT: &str = "skip:act"; +pub const SKIP_AT_ROOT: &str = "skip:at-root"; +pub const SKIP_K0: &str = "skip:k0"; +pub const SKIP_EMPTY_FOCUS: &str = "skip:empty-focus"; +pub const SKIP_EMPTY_PATH: &str = "skip:empty-path"; +pub const SKIP_OFF_ROOT_PRUNE: &str = "skip:off-root-prune"; +pub const SKIP_QUARANTINED: &str = "skip:quarantined"; + /// Does the focus have no descendants at all? /// /// Several return values (`remove_branches`, `restricting`, `join_map_into`, @@ -175,7 +205,7 @@ pub fn dump>(z: &mut Z) -> Stri /// Keeping this behind a trait means there is still exactly one operation table, /// so the two front ends cannot drift apart. pub trait ReadSource: - Zipper + ZipperMoving + ZipperPath + ZipperValues + ZipperAbsolutePath + ZipperIteration + Zipper + ZipperMoving + ZipperPath + ZipperValues + ZipperValuesAt + ZipperAbsolutePath + ZipperIteration { /// Depth-first dump of everything below the focus (`fork_read_zipper` + walk). fn dump_fork(&self) -> String; @@ -523,7 +553,7 @@ pub fn run_ops( // Skipped at the zipper root: the native ReadZipper escapes // its own root there. See `Zip.toNextSiblingByte`. if tgt!(t, wz, *rz, z, z.at_root()) { - ("to_next_sibling_byte", "skip".to_string()) + ("to_next_sibling_byte", SKIP_AT_ROOT.to_string()) } else { let r = tgt!(t, wz, *rz, z, z.to_next_sibling_byte()); ("to_next_sibling_byte", show_byte_opt(r)) @@ -532,7 +562,7 @@ pub fn run_ops( 12 => { let t = get!(d.modn(2)); if tgt!(t, wz, *rz, z, z.at_root()) { - ("to_prev_sibling_byte", "skip".to_string()) + ("to_prev_sibling_byte", SKIP_AT_ROOT.to_string()) } else { let r = tgt!(t, wz, *rz, z, z.to_prev_sibling_byte()); ("to_prev_sibling_byte", show_byte_opt(r)) @@ -555,7 +585,7 @@ pub fn run_ops( let k = get!(d.modn(4)); // k == 0 is degenerate; see Fuzz.lean. if k == 0 { - ("descend_first_k_path", "skip".to_string()) + ("descend_first_k_path", SKIP_K0.to_string()) } else { let r = (*rz).descend_first_k_path(k); ("descend_first_k_path", show_bool(r).to_string()) @@ -570,7 +600,7 @@ pub fn run_ops( let mut v: Vec = Vec::new(); if k == 0 { let _ = writeln!(out, - "{step} k_path_walk ret=skip W={} R={}", + "{step} k_path_walk ret={SKIP_K0} W={} R={}", fingerprint(&wz, root0), fingerprint(rz, root1)); step += 1; continue; @@ -639,7 +669,7 @@ pub fn run_ops( }; match n { Some(n) => ("make_map_val_count", format!("{n}")), - None => ("make_map_val_count", "skip".to_string()), + None => ("make_map_val_count", SKIP_ACT.to_string()), } } 26 => { @@ -664,14 +694,14 @@ pub fn run_ops( if pruneable { ("prune_path", format!("{}", wz.prune_path())) } else { - ("prune_path", "skip".to_string()) + ("prune_path", SKIP_OFF_ROOT_PRUNE.to_string()) } } 31 => { if pruneable { ("prune_ascend", format!("{}", wz.prune_ascend())) } else { - ("prune_ascend", "skip".to_string()) + ("prune_ascend", SKIP_OFF_ROOT_PRUNE.to_string()) } } 32 => { @@ -693,7 +723,7 @@ pub fn run_ops( ("remove_unmasked_branches", hex_path(&canon)) } 34 => { - let s = if (*rz).do_graft(&mut wz) { "-" } else { "skip" }; + let s = if (*rz).do_graft(&mut wz) { "-" } else { SKIP_ACT }; ("graft", s.to_string()) } 35 => { @@ -701,7 +731,7 @@ pub fn run_ops( let s = if (*rz).do_graft_src_at(&mut wz, &p) { hex_path(&p) } else { - "skip".to_string() + SKIP_ACT.to_string() }; ("graft_src_at", s) } @@ -741,11 +771,11 @@ pub fn run_ops( // Skipped when either side has nothing below its focus; see // Fuzz.lean and lean/FINDINGS.md #8. if focus_node_empty(&wz) || focus_node_empty(rz) { - ("restricting", "skip".to_string()) + ("restricting", SKIP_EMPTY_FOCUS.to_string()) } else { match (*rz).do_restricting(&mut wz) { Some(b) => ("restricting", show_bool(b).to_string()), - None => ("restricting", "skip".to_string()), + None => ("restricting", SKIP_ACT.to_string()), } } } @@ -754,7 +784,7 @@ pub fn run_ops( let _pr = get!(d.boolean()); // decoded for stream alignment; see `no_prune` // `join_k_path_into(0)` destroys the subtrie in pathmap 0.3.1. if k == 0 { - ("join_k_path_into", "skip".to_string()) + ("join_k_path_into", SKIP_K0.to_string()) } else { // The bool leaks node materialisation; see FINDINGS.md #8. let r = wz.join_k_path_into(k, no_prune); @@ -770,7 +800,7 @@ pub fn run_ops( let p = get!(d.path(6)); // `insert_prefix("")` destroys the subtrie in pathmap 0.3.1. if p.is_empty() { - ("insert_prefix", "skip".to_string()) + ("insert_prefix", SKIP_EMPTY_PATH.to_string()) } else { ("insert_prefix", show_bool(wz.insert_prefix(&p)).to_string()) } @@ -797,8 +827,10 @@ pub fn run_ops( // `meet_k_path_into` spins forever when the focus has no // children, and escapes the focus subtree when k == 0. // See `Zip.meetKPathUnspecified`. - if k == 0 || wz.child_count() == 0 { - ("meet_k_path_into", "skip".to_string()) + if k == 0 { + ("meet_k_path_into", SKIP_K0.to_string()) + } else if wz.child_count() == 0 { + ("meet_k_path_into", SKIP_EMPTY_FOCUS.to_string()) } else { ( "meet_k_path_into", @@ -869,7 +901,7 @@ pub fn run_ops( show_bool(agree) ), ), - None => ("to_next_get_val", "skip".to_string()), + None => ("to_next_get_val", SKIP_ACT.to_string()), }, 53 => { let n = get!(d.modn(4)); @@ -882,7 +914,7 @@ pub fn run_ops( let s = if (*rz).do_graft_masked(&mut wz, mask, ru) { format!("{}:{}", hex_path(&canon), show_bool(ru)) } else { - "skip".to_string() + SKIP_ACT.to_string() }; ("graft_masked_branches", s) } @@ -899,7 +931,7 @@ pub fn run_ops( // leaves behind degrade the AlgebraicStatus that *later* // operations report, contaminating the rest of the run. let _ = (mask, ru, &canon); - ("graft_child_maps", "skip".to_string()) + ("graft_child_maps", SKIP_QUARANTINED.to_string()) } 55 => { let p = get!(d.path(6)); diff --git a/lean/PathMapModel/Fuzz.lean b/lean/PathMapModel/Fuzz.lean index b1fcc938..de6c88e7 100644 --- a/lean/PathMapModel/Fuzz.lean +++ b/lean/PathMapModel/Fuzz.lean @@ -50,6 +50,36 @@ abbrev V := UInt64 /-- The `Lattice`/`DistributiveLattice` instance `pathmap` provides for `u64`. -/ def ops : ValOps V := u64Ops +/-! ## Skip reasons + +Why an operation was skipped. Every `skip` in the trace carries one of these, +so a skipped op says which rule declined it rather than just that something +declined it. `differential/src/harness.rs` emits the same tokens; the two must +agree exactly or every input with a skip diverges. + +* `skip:act` — the ACT read source cannot be a merge source + (`ZipperInfallibleSubtries` is not implemented for it) or does not implement + the trait the op needs. +* `skip:at-root` — `to_next`/`to_prev_sibling_byte` at the zipper root, where + the native read zipper escapes its own root. +* `skip:k0` — a degenerate `k = 0`. +* `skip:empty-focus` — the focus has nothing below it, where the op's behaviour + is a function of node materialisation rather than trie state. +* `skip:empty-path` — `insert_prefix("")`, which destroys the subtrie. +* `skip:off-root-prune` — a prune on a write zipper not rooted at the map root, + where the depth pruned is a function of internal node layout. +* `skip:quarantined` — the op is disabled outright (op 54). + +Each is recorded in FINDINGS.md and commented at its site. -/ + +def skipAct : String := "skip:act" +def skipAtRoot : String := "skip:at-root" +def skipK0 : String := "skip:k0" +def skipEmptyFocus : String := "skip:empty-focus" +def skipEmptyPath : String := "skip:empty-path" +def skipOffRootPrune : String := "skip:off-root-prune" +def skipQuarantined : String := "skip:quarantined" + /-! ## Rendering -/ def hexDigit (n : Nat) : Char := @@ -262,12 +292,12 @@ def step (s : St) (d : Dec) : Option (St × Dec) := do | 11 => do let (t, d) ← d.mod 2 -- Skipped at the zipper root: `ReadZipper::to_next_sibling_byte` -- escapes its own root there (see the notes in `Zip.toNextSiblingByte`). - if (getTarget s t).atRoot then some (emit s "to_next_sibling_byte" "skip", d) + if (getTarget s t).atRoot then some (emit s "to_next_sibling_byte" skipAtRoot, d) else let (r, s) := onTarget s t (fun z => z.toNextSiblingByte) some (emit s "to_next_sibling_byte" (showByteOpt r), d) | 12 => do let (t, d) ← d.mod 2 - if (getTarget s t).atRoot then some (emit s "to_prev_sibling_byte" "skip", d) + if (getTarget s t).atRoot then some (emit s "to_prev_sibling_byte" skipAtRoot, d) else let (r, s) := onTarget s t (fun z => z.toPrevSiblingByte) some (emit s "to_prev_sibling_byte" (showByteOpt r), d) @@ -283,7 +313,7 @@ def step (s : St) (d : Dec) : Option (St × Dec) := do -- `k = 0` is degenerate: `k_path_internal` treats "already at depth -- base+0" as a hit and reports success without moving, then -- `to_next_k_path(0)` reports success forever. Skipped. - if k == 0 then some (emit s "descend_first_k_path" "skip", d) + if k == 0 then some (emit s "descend_first_k_path" skipK0, d) else let (r, z) := s.rz.descendFirstKPath k some (emit { s with rz := z } "descend_first_k_path" (showBool r), d) @@ -292,7 +322,7 @@ def step (s : St) (d : Dec) : Option (St × Dec) := do -- `descend_first_k_path` iteration -- `k_path_internal` carries -- iteration state, and calling it cold is flagged by pathmap's own -- debug assertions. So the op is the whole walk, not one step. - if k == 0 then some (emit s "k_path_walk" "skip", d) + if k == 0 then some (emit s "k_path_walk" skipK0, d) else let (ps, z) := kWalk s.rz k some (emit { s with rz := z } "k_path_walk" @@ -324,7 +354,7 @@ def step (s : St) (d : Dec) : Option (St × Dec) := do let z := getTarget s t some (emit s "val_at" (showVal (z.valAt p)), d) | 25 => do let (t, d) ← d.mod 2 - if s.act && t == 1 then some (emit s "make_map_val_count" "skip", d) + if s.act && t == 1 then some (emit s "make_map_val_count" skipAct, d) else let z := getTarget s t some (emit s "make_map_val_count" (toString (z.makeMap.valCount [])), d) @@ -342,11 +372,11 @@ def step (s : St) (d : Dec) : Option (St × Dec) := do | 30 => do if pruneable s then let (n, z) := s.wz.prunePath some (emit { s with wz := z } "prune_path" (toString n), d) - else some (emit s "prune_path" "skip", d) + else some (emit s "prune_path" skipOffRootPrune, d) | 31 => do if pruneable s then let (n, z) := s.wz.pruneAscend some (emit { s with wz := z } "prune_ascend" (toString n), d) - else some (emit s "prune_ascend" "skip", d) + else some (emit s "prune_ascend" skipOffRootPrune, d) | 32 => do let (_pr, d) ← d.bool let leaky := s.wz.focusNodeIsEmpty let (r, z) := s.wz.removeBranches noPrune @@ -355,56 +385,59 @@ def step (s : St) (d : Dec) : Option (St × Dec) := do | 33 => do let (n, d) ← d.mod 4; let (m, d) ← d.pathN n; let (_pr, d) ← d.bool let z := s.wz.removeUnmaskedBranches (ByteMask.ofList m) noPrune some (emit { s with wz := z } "remove_unmasked_branches" (hexPath (ByteMask.ofList m)), d) - | 34 => do if s.act then some (emit s "graft" "skip", d) else + | 34 => do if s.act then some (emit s "graft" skipAct, d) else do let z := s.wz.graft s.rz some (emit { s with wz := z } "graft" "-", d) | 35 => do let (p, d) ← d.path - if s.act then some (emit s "graft_src_at" "skip", d) + if s.act then some (emit s "graft_src_at" skipAct, d) else let z := s.wz.graftSrcAt s.rz p some (emit { s with wz := z } "graft_src_at" (hexPath p), d) - | 36 => do if s.act then some (emit s "join_into" "skip", d) else + | 36 => do if s.act then some (emit s "join_into" skipAct, d) else do let (st, z) := s.wz.joinInto ops s.rz some (emit { s with wz := z } "join_into" (toString st), d) - | 37 => do if s.act then some (emit s "join_map_into" "skip", d) else + | 37 => do if s.act then some (emit s "join_map_into" skipAct, d) else do let leaky := s.wz.focusNodeIsEmpty let (st, z) := s.wz.joinMapInto ops s.rz.makeMap some (emit { s with wz := z } "join_map_into" (if leaky then "?" else toString st), d) | 38 => do let (_pr, d) ← d.bool - if s.act then some (emit s "meet_into" "skip", d) + if s.act then some (emit s "meet_into" skipAct, d) else let (st, z) := s.wz.meetInto ops s.rz noPrune some (emit { s with wz := z } "meet_into" (toString st), d) | 39 => do let (_pr, d) ← d.bool - if s.act then some (emit s "subtract_into" "skip", d) + if s.act then some (emit s "subtract_into" skipAct, d) else let (st, z) := s.wz.subtractInto ops s.rz noPrune some (emit { s with wz := z } "subtract_into" (toString st), d) - | 40 => do if s.act then some (emit s "restrict" "skip", d) else + | 40 => do if s.act then some (emit s "restrict" skipAct, d) else do let leaky := s.wz.focusNodeIsEmpty let (st, z) := s.wz.restrict ops s.rz some (emit { s with wz := z } "restrict" (if leaky then "?" else toString st), d) - | 41 => do if s.act then some (emit s "restricting" "skip", d) else - do - -- Skipped, not merely masked, when either side has nothing below - -- its focus: there `restricting` branches on whether an empty node - -- happens to be materialised, and the two branches differ in - -- *effect*, not just in the reported bool. See FINDINGS.md #8. - if s.wz.focusNodeIsEmpty || s.rz.focusNodeIsEmpty then - some (emit s "restricting" "skip", d) - else - let (r, z) := s.wz.restricting s.rz - some (emit { s with wz := z } "restricting" (showBool r), d) + -- Skipped, not merely masked, when either side has nothing below + -- its focus: there `restricting` branches on whether an empty node + -- happens to be materialised, and the two branches differ in + -- *effect*, not just in the reported bool. See FINDINGS.md #8. + -- This guard is checked *before* the ACT one because the harness + -- reaches the ACT skip only by calling `do_restricting`, which it + -- does not do once this guard has fired; the two orders were + -- indistinguishable while both reasons rendered as a bare `skip`. + | 41 => do if s.wz.focusNodeIsEmpty || s.rz.focusNodeIsEmpty then + some (emit s "restricting" skipEmptyFocus, d) + else if s.act then some (emit s "restricting" skipAct, d) + else + let (r, z) := s.wz.restricting s.rz + some (emit { s with wz := z } "restricting" (showBool r), d) | 42 => do let (k, d) ← d.mod 4; let (_pr, d) ← d.bool -- `join_k_path_into(0)` should be the identity but destroys the -- subtrie in pathmap 0.3.1; see `Zip.joinKPathInto`. - if k == 0 then some (emit s "join_k_path_into" "skip", d) + if k == 0 then some (emit s "join_k_path_into" skipK0, d) else -- The bool is another `AbstractNodeRef` leak: an empty node still -- comes back as `Some(...)` from `into_option()` for some @@ -418,7 +451,7 @@ def step (s : St) (d : Dec) : Option (St × Dec) := do -- `insert_prefix("")` destroys the subtrie in pathmap 0.3.1; see -- `Zip.insertPrefix`. Skipped so the known bug does not mask others. if p.isEmpty then - some (emit s "insert_prefix" "skip", d) + some (emit s "insert_prefix" skipEmptyPath, d) else let (r, z) := s.wz.insertPrefix p some (emit { s with wz := z } "insert_prefix" (showBool r), d) @@ -437,9 +470,11 @@ def step (s : St) (d : Dec) : Option (St × Dec) := do | none => some (emit { s with wz := z } "take_map_restore" "0", d) | 46 => do let (k, d) ← d.mod 4; let (_pr, d) ← d.bool -- `meet_k_path_into` is not implementable for these arguments; see - -- `Zip.meetKPathUnspecified`. The Rust side applies the same guard. - if s.wz.meetKPathUnspecified k then - some (emit s "meet_k_path_into" "skip", d) + -- `Zip.meetKPathUnspecified`, whose two disjuncts are split out here + -- so the skip names which one fired. The Rust side matches. + if k == 0 then some (emit s "meet_k_path_into" skipK0, d) + else if s.wz.focusNodeIsEmpty then + some (emit s "meet_k_path_into" skipEmptyFocus, d) else let (r, z) := s.wz.meetKPathInto ops k noPrune some (emit { s with wz := z } "meet_k_path_into" (showBool r), d) @@ -477,14 +512,14 @@ def step (s : St) (d : Dec) : Option (St × Dec) := do | 52 => do -- `ZipperReadOnlyIteration::to_next_get_val` must advance exactly as -- `to_next_val` does and hand back the value at the new focus. -- ACT does not implement the trait, so the op is unavailable there. - if s.act then some (emit s "to_next_get_val" "skip", d) else + if s.act then some (emit s "to_next_get_val" skipAct, d) else do let (moved, z) := s.rz.toNextVal let v := if moved then z.val else none some (emit { s with rz := z } "to_next_get_val" (showBool moved ++ ":" ++ showVal v ++ ":1"), d) | 53 => do let (n, d) ← d.mod 4; let (m, d) ← d.pathN n; let (ru, d) ← d.bool - if s.act then some (emit s "graft_masked_branches" "skip", d) else + if s.act then some (emit s "graft_masked_branches" skipAct, d) else do let z := s.wz.graftMaskedBranches s.rz (ByteMask.ofList m) ru some (emit { s with wz := z } "graft_masked_branches" @@ -496,7 +531,7 @@ def step (s : St) (d : Dec) : Option (St × Dec) := do -- broken three ways (FINDINGS.md #15) and the node representations -- it leaves behind degrade the `AlgebraicStatus` that *later* -- operations report, which would contaminate the whole run. - if true then some (emit s "graft_child_maps" "skip", d) else + if true then some (emit s "graft_child_maps" skipQuarantined, d) else do let mask := ByteMask.ofList m let maps := mask.map (fun b => ([b], s.rz.trie.subtrie (s.rz.focus ++ [b]))) @@ -505,7 +540,7 @@ def step (s : St) (d : Dec) : Option (St × Dec) := do (hexPath mask ++ ":" ++ showBool ru), d) | 55 => do let (p, d) ← d.path -- `meet_2` takes two sources; the second is the first moved to `p`. - if s.act then some (emit s "meet_2" "skip", d) else + if s.act then some (emit s "meet_2" skipAct, d) else do let b := { s.rz with path := s.rz.path ++ p } let (st, z) := s.wz.meet2 ops s.rz b diff --git a/lean/README.md b/lean/README.md index 71906dc4..f3a0cb43 100644 --- a/lean/README.md +++ b/lean/README.md @@ -319,19 +319,29 @@ not, the maps it ends with match the trace's `MAP0`/`MAP1`. A handful of argument combinations are skipped by both sides, each because the crate's behaviour there is a confirmed bug that would otherwise mask everything downstream. Each is recorded in [FINDINGS.md](FINDINGS.md) and each skip is -commented at its site: - -* `meet_k_path_into` when the focus has no children, or `k = 0` — it does not - terminate. -* `insert_prefix("")` and `join_k_path_into(0)` — both should be the identity and - both destroy the subtrie. -* `descend_first_k_path(0)` / `to_next_k_path(0)` — degenerate; report success - without moving, forever. -* `to_next_sibling_byte` / `to_prev_sibling_byte` at the zipper root — the native - read zipper leaves its own root there. -* `prune_path` / `prune_ascend`, and the `prune` flag on every other operation, - for a write zipper not rooted at the map root — the depth pruned is a function - of internal node layout, so there is nothing to specify. +commented at its site. + +A skip is named in the trace — `ret=skip:`, never a bare `skip` — so a +skipped op says which rule declined it. The vocabulary is defined once on each +side (`SKIP_*` in `differential/src/harness.rs`, `skip*` in +`PathMapModel/Fuzz.lean`) and the two must agree exactly, or every input that +skips diverges: + +| token | what it means | +|---|---| +| `skip:k0` | `meet_k_path_into(0)`, `join_k_path_into(0)`, `descend_first_k_path(0)` / `to_next_k_path(0)` — degenerate; the first two should be the identity and destroy the subtrie, the last reports success without moving, forever. | +| `skip:empty-focus` | `meet_k_path_into` with no children (it does not terminate), and `restricting` when either side has nothing below its focus (the two branches differ in *effect*, not just in the reported bool). | +| `skip:empty-path` | `insert_prefix("")` — should be the identity, destroys the subtrie. | +| `skip:at-root` | `to_next_sibling_byte` / `to_prev_sibling_byte` at the zipper root — the native read zipper leaves its own root there. | +| `skip:off-root-prune` | `prune_path` / `prune_ascend`, and the `prune` flag on every other operation, for a write zipper not rooted at the map root — the depth pruned is a function of internal node layout, so there is nothing to specify. | +| `skip:quarantined` | `graft_child_maps` (op 54), disabled outright: it is broken three ways (FINDINGS.md #15) and the node representations it leaves behind degrade the `AlgebraicStatus` that *later* operations report. | +| `skip:act` | ACT mode only — the read source cannot be a merge source (`ZipperInfallibleSubtries` is not implemented for it) or does not implement the trait the op needs. | + +Naming these turned up an ordering bug the bare token had hidden: for +`restricting` the model tested ACT mode first and the harness tested the empty +focus first, so in ACT mode with an empty focus the two took different branches +and agreed only because both printed `skip`. The model now checks the guards in +the harness's order. `to_next_k_path` is also only exercised as the continuation of a `descend_first_k_path` iteration (the `k_path_walk` op), because @@ -481,25 +491,33 @@ documentation rather than from the code. ## Current agreement -500 random programs (`./lean/differential.py --random 500 --seed 99 --max-fails 0`), -model versus crate, comparing every return value plus both maps in full: +20000 random programs (`./lean/differential.py --random 20000 --seed 7 +--max-fails 0`), model versus crate, comparing every return value plus both maps +in full: ``` -404/500 inputs agree exactly - 87/500 hit one of the classified defects in FINDINGS.md - 9/500 diverge for reasons not yet classified +19735/20000 inputs agree exactly + 265/20000 hit one of the classified defects + 0/20000 diverge for reasons not yet classified ``` -The 87 break down as: `to_next_val` after `to_next_step` (19), `ascend_until` -corrupting a write zipper (17), zippers escaping their root (16), a `set_val` -unwrap on `None` (14), the `TrieRef` slice underflow (12), `make_unique` on an -empty sentinel (7), `join_into` dropping the source (2). - -Every defect listed in FINDINGS.md reproduces here exactly as it does on -`master`; the blind-zipper migration neither fixed nor introduced any of them. - -`differential.py` prints that breakdown itself, so new divergences stay visible -as the known ones are fixed. +The 265 break down as `graft_masked_branches` creating the focus (177), +`join_into` dropping the source (24), `AlgebraicStatus` imprecision (20 + 18), +value bias by node layout (11), a dangling child kept by an algebraic op (11), +`val_at` at a dangling path (3), `subtract_into` dropping a value (1). + +Five of those classes are keyed on the *shape* of the divergence rather than on +an operation name, because the same defect surfaces under whichever operation +happens to read the damaged location -- value bias, for instance, is reported by +`meet_into` where it is introduced but by `dump`, `val_at` or the final map dump +wherever it is later observed. `divergence_shape` in `differential.py` decides +those, and returning "no familiar shape" is its important case: it is what keeps +a genuinely new defect out of the known buckets. A shrunk reproducer for each +class is in `lean/corpus/`, and `./lean/differential.py lean/corpus/*.bin` +replays them all. + +`differential.py` prints the breakdown itself, so new divergences stay visible as +the known ones are fixed. ## ArenaCompactTree as the read source diff --git a/lean/differential.py b/lean/differential.py index 3f66934a..47b593dd 100755 --- a/lean/differential.py +++ b/lean/differential.py @@ -31,11 +31,13 @@ ROOT = os.path.dirname(os.path.dirname(os.path.abspath(__file__))) ORACLE = os.path.join(ROOT, "lean", ".lake", "build", "bin", "pathmap-oracle") -TRACE_CANDIDATES = [ +# PATHMAP_TRACE / PATHMAP_ACT_TRACE override the search, for builds that live +# in another target dir (CI builds two commits side by side). +TRACE_CANDIDATES = [os.environ.get("PATHMAP_TRACE", "")] + [ os.path.join(ROOT, "target", "release", "pathmap_trace"), os.path.join(ROOT, "target", "debug", "pathmap_trace"), ] -ACT_CANDIDATES = [ +ACT_CANDIDATES = [os.environ.get("PATHMAP_ACT_TRACE", "")] + [ os.path.join(ROOT, "target", "release", "act_trace"), os.path.join(ROOT, "target", "debug", "act_trace"), ] @@ -48,7 +50,7 @@ def find_trace_bin(act): for c in (ACT_CANDIDATES if act else TRACE_CANDIDATES): - if os.path.exists(c): + if c and os.path.exists(c): return c if act: sys.exit("build the ACT side first: " @@ -194,6 +196,11 @@ def run(self, blob): # and message. See lean/FINDINGS.md for the write-up of each, and # `cargo run -p differential --bin zipper_bug_repros -- ` for a reproducer. KNOWN = [ + # Tested first: this one is keyed on a shape, and an ACT val_count-only + # difference can land on a line whose op name matches an entry below. + (["ACT-VALCOUNT-ONLY"], + "ACTZipper::val_count() counts from the zipper root, not the focus " + "[act: val_count_ignores_focus]"), (["ESCAPED-ROOT"], "a zipper left its own root: root_prefix_path() changed [root_escape]"), (["to_next_val"], @@ -259,9 +266,6 @@ def run(self, blob): "copy-on-write cannot make a shared dangling path unique (finding 16) " "[shared_dangling_cow]"), # ArenaCompactTree read source (differential.py --act). - (["ACT-VALCOUNT-ONLY"], - "ACTZipper::val_count() counts from the zipper root, not the focus " - "[act: val_count_ignores_focus]"), (["k_path_walk"], "ACTZipper::descend_first_k_path() only walks the leftmost chain " "[act: first_k_path_no_backtrack]"), @@ -271,9 +275,122 @@ def run(self, blob): (["descend_last_path"], "ACTZipper::descend_last_path() runs one byte past the end of the trie " "[act: last_path_overshoots]"), + # Shape classes, from `divergence_shape`. Last on purpose: every entry + # above is more specific, and these are meant to catch only what none of + # them explain. Reproducers for each are in lean/corpus/. + (["STATUS-ONLY"], + "AlgebraicStatus::Identity is not returned reliably when nothing changed " + "(finding 8); meet_into/subtract_into, status only, effects agree " + "[status_imprecise]"), + (["DANGLING-KEPT"], + "an algebraic op keeps a dangling child the spec drops: an empty child " + "node meets/subtracts to itself rather than disappearing " + "[meet_keeps_dangling]"), + (["CONTENT-DROPPED"], + "subtract_into() drops a value under a path present in the source " + "[subtract_drops_value]"), + (["VALUE-ONLY"], + "which value survives a collision follows node layout rather than the " + "left-biased spec (join/meet and everything that later reads the " + "location) [value_bias_by_node_layout]"), + (["FOCUS-VALUE-FOR-DANGLING"], + "val_at()/get_val_at() return the focus value for a dangling child path " + "[val_at_dangling]"), ] +# Shapes that several operations share. These classes are defined by *which +# fields of the trace line moved*, not by which operation produced them: the +# same defect surfaces under whichever op happens to read the damaged location, +# so keying them on an op name would both miss cases and over-match. +STATUSES = ("Identity", "Element", "None") +# Ops whose `ret` is a value rather than a flag or a count. A bool return +# renders as `ret=1`/`ret=0`, which is indistinguishable from a value by shape, +# so the value-bias rule for `ret` is confined to these. +VALUE_RET_OPS = ("val_at", "set_val", "remove_val") + + +def _key(tok): + """The field name a trace token belongs to: `v126` -> v, `ret=X` -> ret.""" + if "=" in tok: + return tok.split("=", 1)[0] + m = re.match(r"[A-Za-z]+", tok) + return m.group(0) if m else tok + + +def _dump_shape(sa, sb): + """Shape of a difference between two trie dumps (`p:v,p:v,...`). + + Both the `MAP0`/`MAP1` final dumps and the `dump` op's return are this + shape, and the value-bias class shows up in either. + """ + ea, eb = sa.split(","), sb.split(",") + if len(ea) != len(eb): + return None + pa = [e.rsplit(":", 1) for e in ea] + pb = [e.rsplit(":", 1) for e in eb] + if any(len(x) != 2 for x in pa + pb): + return None + if [x[0] for x in pa] != [x[0] for x in pb]: + return None # the set of locations moved + moved = [(x[1], y[1]) for x, y in zip(pa, pb) if x[1] != y[1]] + if not moved or any("-" in m for m in moved): + return None # a value appeared or vanished + return "VALUE-ONLY" + + +def divergence_shape(a, b): + """Name the shape of a divergence, or None when it has no familiar one. + + Returning None is the important case: it is what keeps a genuinely new + defect out of the known buckets, so each shape below is deliberately narrow. + """ + ta, tb = a.split(), b.split() + if len(ta) != len(tb): + return None + diff = [(x, y) for x, y in zip(ta, tb) if x != y] + if not diff: + return None + if ta[0].startswith(("MAP", "ROOT")): + return _dump_shape(ta[1], tb[1]) if len(ta) == 2 else None + keys = {_key(x) for x, _ in diff} + vals = {t[1:] for t in ta if _key(t) == "v"} + if keys == {"ret"}: + ra, rb = diff[0][0].split("=", 1)[1], diff[0][1].split("=", 1)[1] + if ra in STATUSES and rb in STATUSES: + return "STATUS-ONLY" + # `-` on the model side against the focus value on the crate side, in + # a bare return (`val_at`) or a component of one (`get_val_agrees`). + ca, cb = ra.split(":"), rb.split(":") + if len(ca) == len(cb): + moved = [(x, y) for x, y in zip(ca, cb) if x != y] + if moved and all(x == "-" and y in vals for x, y in moved): + return "FOCUS-VALUE-FOR-DANGLING" + if "," in ra or ra.count(":") == 1: + return _dump_shape(ra, rb) # `dump` returns a whole subtrie + if ra.isdigit() and rb.isdigit() and len(ta) > 1 and ta[1] in VALUE_RET_OPS: + return "VALUE-ONLY" + return None + if keys == {"v"}: + # Both sides must hold a value: `v-` against `v42` is a value appearing + # or vanishing, which is a content difference, not a biased choice. + if all(x[1:].isdigit() and y[1:].isdigit() for x, y in diff): + return "VALUE-ONLY" + return None + if keys <= {"ret", "c", "n"} and ({"c", "n"} & keys): + # `c` (child_count) when it moved, else `n` (val_count): a dangling + # child adds a child without adding a value, a dropped value the + # reverse, so whichever field moved is the one that says which it was. + field = "c" if "c" in keys else "n" + xa = [int(x[1:]) for x, _ in diff if _key(x) == field] + xb = [int(y[1:]) for _, y in diff if _key(y) == field] + if all(y > x for x, y in zip(xa, xb)): + return "DANGLING-KEPT" + if all(y < x for x, y in zip(xa, xb)): + return "CONTENT-DROPPED" + return None + + def act_valcount_only(a, b): """Do these two trace lines differ *only* in the read zipper's val_count? @@ -312,7 +429,11 @@ def compare(blob, oracle, other, other_label, act=False): return "%s %s" % (other_label, real_err) for i, (a, b) in enumerate(zip(lean, real)): if a != b: - tag = "ACT-VALCOUNT-ONLY " if act and act_valcount_only(a, b) else "" + tags = ["ACT-VALCOUNT-ONLY"] if act and act_valcount_only(a, b) else [] + shape = divergence_shape(a, b) + if shape: + tags.append(shape) + tag = "".join(t + " " for t in tags) return "%sline %d\n lean: %s\n %-5s: %s" % (tag, i, a, other_label, b) if len(lean) != len(real): return "length %d (lean) vs %d (%s)" % (len(lean), len(real), other_label) @@ -503,12 +624,14 @@ def save(idx): fails = 0 known = {} + done = 0 # inputs actually classified; < n_inputs when --max-fails stops the run restarts = 0 reports = [] # (idx, name, msg) for failures, so -j output is ordered def record(idx, msg): """Classify one result. Returns True when the run should stop.""" - nonlocal fails + nonlocal fails, done + done += 1 name = source.name(idx) if not msg: if args.verbose: @@ -565,8 +688,13 @@ def record(idx, msg): if restarts: print("(%d child restart(s) after a timeout or crash)" % restarts) hit = sum(known.values()) + # Against `done`, not `n_inputs`: when --max-fails stops the run the remaining + # inputs were never executed, and counting them in the denominator would score + # every one of them as agreeing. print("%d/%d inputs agree (%d hit known bugs, %d new divergences)" - % (n_inputs - fails - hit, n_inputs, hit, fails)) + % (done - fails - hit, done, hit, fails)) + if done < n_inputs: + print("(%d of %d inputs were not run)" % (n_inputs - done, n_inputs)) for note, n in sorted(known.items()): print(" known x%d: %s" % (n, note)) return 1 if fails else 0 diff --git a/lean/shrink.py b/lean/shrink.py index 7afc4fa9..65f23f64 100755 --- a/lean/shrink.py +++ b/lean/shrink.py @@ -9,13 +9,15 @@ import argparse, os, re, subprocess, sys ROOT = os.path.dirname(os.path.dirname(os.path.abspath(__file__))) -ORACLE = os.path.join(ROOT, "lean", ".lake", "build", "bin", "pathmap-oracle") +# PATHMAP_ORACLE / PATHMAP_TRACE / PATHMAP_ACT_TRACE override the defaults, for +# builds that live in another target dir (CI builds two commits side by side). +ORACLE = os.environ.get("PATHMAP_ORACLE") or os.path.join(ROOT, "lean", ".lake", "build", "bin", "pathmap-oracle") # Release by default, matching differential.py: a debug build turns several # known bugs into panics, and the shrinker would then collapse every input onto # whichever panic it hits first. `--debug` shrinks toward a panic on purpose. -TRACE_RELEASE = os.path.join(ROOT, "target", "release", "pathmap_trace") +TRACE_RELEASE = os.environ.get("PATHMAP_TRACE") or os.path.join(ROOT, "target", "release", "pathmap_trace") TRACE_DEBUG = os.path.join(ROOT, "target", "debug", "pathmap_trace") -ACT_RELEASE = os.path.join(ROOT, "target", "release", "act_trace") +ACT_RELEASE = os.environ.get("PATHMAP_ACT_TRACE") or os.path.join(ROOT, "target", "release", "act_trace") ACT_DEBUG = os.path.join(ROOT, "target", "debug", "act_trace") TRACE = TRACE_RELEASE ORACLE_ARGS = []