[FBumann]

Prompt: Write a fuzzer for mathspec and specsolve to find bugs in the parsing and program generation as well as the polars engine

Prompt: And we will need the fuzzer in our ci if possible…?

Note

The following content was generated by AI.

What this changes

A seeded fuzzer edits the example specs and checks the loader, the canonical form, the expansion and the typesetter. The CI job compares 1,000 mutants with a committed baseline, and a nightly runs fresh ones. The findings are #890 and #891.

The fuzzer

• tests/fuzz/mutate.py picks a spec from examples/ and applies one to three edits:
  • to the text of an expression or a predicate: delete, duplicate or swap a token; replace a name, an operator or a number; wrap the text in an operator; nest it past the depth limits; repeat a keyword;
  • to the mapping: splice in another spec's expression; delete a key; give a value another type; rename an entry; change a dims list; add an unknown key.
• tests/fuzz/check.py holds the oracles:
  • to_spec accepts the mapping, or raises MathSpecError;
  • an accepted spec round-trips through to_yaml, plain and canonical;
  • the canonical form is unchanged by shuffled keys and commuted terms;
  • the program and the expansion build, and an expansion expanded again is the same spec;
  • every format prints the spec, as written, without a legend, inlined, and expanded;
  • advice reads it.
• --hash-seeds runs every seed under two interpreter hash seeds and compares everything the spec printed.
• tests/test_fuzz.py holds the three reduced findings as strict xfails that name The canonical form keeps cases and relation columns in file order, so two files that state one spec differ in it #890 and A curve stated as lines over links with different dimensions loads, and then its expansion is refused #891. It also checks that every unedited example passes, apart from the six that The canonical form keeps cases and relation columns in file order, so two files that state one spec differ in it #890 names, and that enough mutants load.

CI

• pixi run fuzz checks mutants 0–999 under two hash seeds and compares each seed with tests/fuzz/baseline.json. A new finding fails, and so does a held finding that no longer occurs. The failure prints how to write the baseline again. 27 s on 4 cores, idle machine.
• It runs as a step of the CI job and as part of pixi run ci, because ci.yml adds gates as steps rather than as billed jobs. That makes it part of the required check.
• fuzz.yml runs pixi run fuzz-fresh each night over 50,000 mutants picked by the day of the year. It fails only on a kind of finding that tests/fuzz/kinds.json does not map to an issue.
• REUSE.toml covers the two JSON files, which cannot carry a header.

Why

20,000 mutants (2,183 accepted) found no loader crash and no output that depends on the hash seed. They did find two canonical-form orders (#890) and one expansion that the loader should have refused (#891). The baseline keeps the next such finding from going unseen, and the nightly looks past the baseline's seeds.

Gates run, departures, and what this does not do

• pixi run lint: every hook clean. pixi run test: 2,919 passed, 1 skipped, 3 xfailed. pixi run fuzz passes. I did not run docs-build or compile-tex, because nothing here touches them. fuzz.yml has not run.
• The reduced cases live in tests/test_fuzz.py rather than in construct-named files, as the fuzzer's regression corpus.
• tests/fuzz/run.py prints, so it has a T20 per-file ignore.
• No bug is fixed here.
• merge, override, symbol tables and the CLI are not fuzzed.

---

Generated by Claude Code

[FBumann]

Prompt: Comment on 893. Should be done after 894 merged.

Note

The following content was generated by AI.

A second fuzzer for this PR to take in once #894 has merged. It is a differential oracle for the divisor check under missing:. #894 and #942 add that check, so it has nothing to test on main.

This PR's oracles find a crash, a round trip that fails, or two canonical forms. A load check that loads a file it should refuse passes all of them. This fuzzer draws a random spec and a Python model of what the spec means. It runs the model on random data with missing rows and compares the result with what to_spec decided:

• soundness: the spec loads, and the missing rows alone make a divisor 0 in a row that is built;
• precision: the spec is refused for its divisor, and no draw divides by zero at all.

What it found on 12,000 seeds

Kind	Example	Where	State
soundness	a masked variable with missing: 1 spared a divisor: y: {where: "c > 0", missing: 1} with sum(y / c, over=g)	#942	fixed in #942 before it merged: 225 seeds before, none after
soundness	a missing: value other than 0 that cancels: missing: 1 with x / (1 - c)	#894	about 250 seeds; specsolve refuses it when the data is attached
soundness	constants that cancel around missing: 0: x / ((c + 1) - 1)	#894	specsolve refuses it when the data is attached
soundness	a literal zero in a case: when: d > 0, expression: 1 - 1	#894	specsolve refuses it when the data is attached
precision	a guard written NOT (c != 1), or a masked variable in another term of the same row	#942	conservative, and safe

The other precision seeds are rows that are never built, because their masks contradict each other.

How to take it in, after #894

• Put it beside mutate.py and check.py, as tests/fuzz/divisors.py, and give run.py a --oracle divisors that runs its seeds.
• Keep a baseline as pixi run fuzz does. The three feat(language)!: a missing row reads as the value the file names, and missing: neutral is gone #894 kinds above are known, so they go in kinds.json, or the check closes them first.
• It runs in one process. The 12,000-seed run used four shards of 3,000 seeds.
• Its ABSENT, row and summand rules restate absence.md. When that page changes, the model changes with it.

The fuzzer, as run (python divfuzz.py START STOP [FINDINGS.json])

"""A differential fuzzer for the load-time divisor check under `missing:`.

Each seed draws a small spec over one ordered dimension g = a, b, c, d, together with
a Python model of what the spec means: absence removes a row or a summand, a case reads
one region, a shift reads the row before. The model is evaluated on random data with
missing rows. A zero division counts only in a row or summand that is built, and it is
blamed on the missing rows only where it stays 0 whatever the present rows hold and stops
being 0 once every row is present.

    soundness   the file loads, and the missing rows make a divisor 0 in a built row
    precision   the file is refused for its divisor, and no draw divides by zero at all

Usage: python divfuzz.py START STOP [FINDINGS.json]
"""

from __future__ import annotations

import json
import math
import random
import sys
from dataclasses import dataclass, field

from mathspec import to_spec
from mathspec.errors import MathSpecError

LABELS = ['a', 'b', 'c', 'd']
N = len(LABELS)
ABSENT = object()
DIV_MSG = 'which no number divides by'

# --------------------------------------------------------------------------- model


@dataclass
class World:
    params: dict  # name -> {'missing': ..., 'dtype': ..., 'dims': [...]}
    data: dict  # name -> list of value or None (missing), or scalar
    variables: dict  # name -> {'where': Cond|None, 'missing': 'absent'|number}
    conds: dict  # named conditions
    exprs: dict  # named expressions
    events: list = field(default_factory=list)

    def param(self, name, i):
        p = self.params[name]
        v = self.data[name] if not p['dims'] else self.data[name][i]
        if v is not None:
            return v
        m = p['missing']
        return ABSENT if m == 'absent' else m


class Node:
    pass


@dataclass
class P(Node):
    name: str

    def text(self):
        return self.name

    def ev(self, w, i):
        return w.param(self.name, i)


@dataclass
class K(Node):
    v: float

    def text(self):
        return repr(self.v) if self.v >= 0 else f'({self.v!r})'

    def ev(self, w, i):
        return self.v


@dataclass
class V(Node):
    name: str

    def text(self):
        return self.name

    def ev(self, w, i):
        var = w.variables[self.name]
        if var['where'] is None or var['where'].ev(w, i):
            return 1.0
        return ABSENT if var['missing'] == 'absent' else float(var['missing'])


@dataclass
class Neg(Node):
    a: Node

    def text(self):
        return f'-({self.a.text()})'

    def ev(self, w, i):
        v = self.a.ev(w, i)
        return v if v is ABSENT else -v


@dataclass
class Bin(Node):
    op: str
    a: Node
    b: Node

    def text(self):
        return f'({self.a.text()} {self.op} {self.b.text()})'

    def ev(self, w, i):
        x, y = self.a.ev(w, i), self.b.ev(w, i)
        if x is ABSENT or y is ABSENT:
            return ABSENT
        if self.op == '+':
            return x + y
        if self.op == '-':
            return x - y
        if self.op == '*':
            return x * y
        if self.op == '**':
            return x**y
        if y == 0:
            w.events.append((f'{self.text()} at {LABELS[i]}', self.b, i))
            return math.nan
        return x / y


@dataclass
class Shift(Node):
    a: Node
    edge: object  # None, 'wrap', or a number

    def text(self):
        edge = '' if self.edge is None else f", edge='wrap'" if self.edge == 'wrap' else f', edge={self.edge!r}'
        return f'shift({self.a.text()}, along=g, offset=1{edge})'

    def ev(self, w, i):
        if i == 0 and self.edge != 'wrap':
            return ABSENT if self.edge is None else float(self.edge)
        return self.a.ev(w, (i - 1) % N)


@dataclass
class Sum(Node):
    a: Node

    def text(self):
        return f'sum({self.a.text()}, over=g)'

    def ev(self, w, i):
        total = 0.0
        for j in range(N):
            v = _guarded(w, lambda j=j: self.a.ev(w, j))
            if v is not ABSENT:
                total += v
        return total


@dataclass
class Ref(Node):
    name: str

    def text(self):
        return self.name

    def ev(self, w, i):
        return w.exprs[self.name].ev(w, i)


@dataclass
class Cased(Node):
    when: Cond
    then: Node
    otherwise: Node

    def ev(self, w, i):
        return (self.then if self.when.ev(w, i) else self.otherwise).ev(w, i)


def _guarded(w, thunk):
    """Evaluate a row or a summand: its divisions count only if it is built."""
    before = len(w.events)
    v = thunk()
    if v is ABSENT:
        del w.events[before:]
    return v


class Cond:
    pass


@dataclass
class Cmp(Cond):
    name: str
    op: str
    v: float

    def text(self):
        return f'{self.name} {self.op} {self.v!r}'

    def ev(self, w, i):
        x = w.param(self.name, i)
        if x is ABSENT:
            return False
        return {'<': x < self.v, '<=': x <= self.v, '>': x > self.v, '>=': x >= self.v,
                '==': x == self.v, '!=': x != self.v}[self.op]  # fmt: skip


@dataclass
class Bare(Cond):
    name: str

    def text(self):
        return self.name

    def ev(self, w, i):
        p = w.params.get(self.name)
        if p is None:  # a variable: does it exist here
            var = w.variables[self.name]
            return var['where'] is None or var['where'].ev(w, i)
        raw = w.data[self.name][i]
        if p['dtype'] == 'bool':
            if raw is not None:
                return raw
            return p['missing'] is True
        return raw is not None


@dataclass
class Not(Cond):
    a: Cond

    def text(self):
        return f'NOT ({self.a.text()})'

    def ev(self, w, i):
        return not self.a.ev(w, i)


@dataclass
class Conn(Cond):
    op: str
    a: Cond
    b: Cond

    def text(self):
        return f'({self.a.text()}) {self.op} ({self.b.text()})'

    def ev(self, w, i):
        x, y = self.a.ev(w, i), self.b.ev(w, i)
        return (x and y) if self.op == 'AND' else (x or y)


@dataclass
class CRef(Cond):
    name: str

    def text(self):
        return self.name

    def ev(self, w, i):
        return w.conds[self.name].ev(w, i)


# --------------------------------------------------------------------------- generator

FLOATS = ['c', 'd']
MISSING_FLOAT = [0, 0, 0, 1, -1, 2.5, 'absent', 'absent', 'refused']


class Gen:
    def __init__(self, seed):
        self.r = random.Random(seed)
        self.exprs = {}
        self.conds = {}
        self.yaml_exprs = {}

    def cond(self, depth=0):
        r = self.r
        k = r.random()
        if depth < 2 and k < 0.15:
            return Conn(r.choice(['AND', 'AND', 'OR']), self.cond(depth + 1), self.cond(depth + 1))
        if depth < 2 and k < 0.22:
            return Not(self.cond(depth + 1))
        if k < 0.30 and self.conds:
            return CRef(r.choice(list(self.conds)))
        if k < 0.42:
            return Bare(r.choice([*FLOATS, 'f']))
        return Cmp(r.choice(FLOATS), r.choice(['>', '>', '!=', '<', '>=', '<=', '==']), r.choice([0, 0, 1, -1, 0.5]))

    def data(self, depth=0):
        """A variable-free expression over g."""
        r = self.r
        k = r.random()
        if depth >= 3 or k < 0.35:
            return P(r.choice(FLOATS)) if r.random() < 0.85 else K(r.choice([1, 2, 0.5]))
        if k < 0.45:
            return Neg(self.data(depth + 1))
        if k < 0.60:
            return Bin(r.choice(['+', '-']), self.data(depth + 1), r.choice([self.data(depth + 1), K(1)]))
        if k < 0.70:
            return Bin('*', self.data(depth + 1), self.data(depth + 1))
        if k < 0.75:
            return Bin('**', self.data(depth + 1), K(2))
        if k < 0.85:
            operand = self.data(depth + 1)
            while not _has_param(operand):
                operand = self.data(depth + 1)
            return Shift(operand, r.choice(['wrap', 'wrap', 1, 2]))
        if k < 0.92:
            return self.named(depth)
        return Bin('/', self.data(depth + 1), self.data(depth + 1))

    def named(self, depth):
        r = self.r
        name = f'e{len(self.exprs)}'
        self.exprs[name] = None
        if r.random() < 0.5:
            body = self.data(depth + 1)
            self.exprs[name] = body
            self.yaml_exprs[name] = body.text()
        else:
            when, then, other = self.cond(), self.data(depth + 1), self.data(depth + 1)
            self.exprs[name] = Cased(when, then, other)
            self.yaml_exprs[name] = {
                'dims': ['g'],
                'cases': {'on': {'when': when.text(), 'expression': then.text()}},
                'otherwise': other.text(),
            }
        return Ref(name)

    def term(self, depth=0):
        """A term over g that carries exactly one variable, linearly."""
        r = self.r
        v = V(r.choice(['x', 'y', 'z']))
        k = r.random()
        if k < 0.35:
            return Bin('/', v, self.data(depth))
        if k < 0.55:
            return Bin('*', self.data(depth), v)
        if k < 0.70:
            return Bin('*', Bin('/', self.data(depth), self.data(depth)), v)
        if k < 0.80:
            return Shift(Bin('/', v, self.data(depth)), r.choice([None, 'wrap', 0]))
        if k < 0.90:
            return Bin('+', v, Bin('/', self.data(depth), self.data(depth)))
        return v


def _has_param(node):
    if isinstance(node, (P, Ref)):
        return True
    return any(_has_param(v) for v in vars(node).values() if isinstance(v, Node))


def draw(seed):
    g = Gen(seed)
    r = g.r
    params = {
        'c': {'dims': ['g'], 'dtype': 'float', 'missing': r.choice(MISSING_FLOAT)},
        'd': {'dims': ['g'], 'dtype': 'float', 'missing': r.choice(MISSING_FLOAT)},
        'f': {'dims': ['g'], 'dtype': 'bool', 'missing': r.choice([False, False, 'absent', 'refused'])},
        'k': {'dims': [], 'dtype': 'float', 'missing': 'refused'},
    }
    if r.random() < 0.3:
        g.conds['nc'] = g.cond()
    variables = {'x': {'where': None, 'missing': 'absent'}}
    for name in ('y', 'z'):
        variables[name] = {'where': g.cond(), 'missing': r.choice(['absent', 'absent', 0, 0, 1])}
    constraints = {}
    for n in range(r.choice([1, 1, 2])):
        shape = r.random()
        if shape < 0.6:
            terms = [g.term() for _ in range(r.choice([1, 1, 2]))]
            lhs = terms[0] if len(terms) == 1 else Bin('+', *terms)
            rhs = g.data() if r.random() < 0.5 else K(1)
            where = g.cond() if r.random() < 0.75 else None
            constraints[f'r{n}'] = ('g', where, lhs, rhs)
        else:
            lhs = Sum(g.term())
            constraints[f'r{n}'] = ('', None, lhs, K(1))
    reported = {}
    if r.random() < 0.3:
        reported['rep'] = Bin('/', V(r.choice(['x', 'y', 'z'])), g.data())
    raw = {
        'dimensions': {'g': {'dtype': 'str', 'ordered': True}},
        'parameters': {
            n: {k: v for k, v in p.items() if not (k == 'missing' and v == 'refused')} for n, p in params.items()
        },
        'variables': {},
        'constraints': {},
        'objective': {'sense': 'minimize', 'expression': 'sum(x, over=g)'},
    }
    for name, var in variables.items():
        entry = {'dims': ['g']}
        if var['where'] is not None:
            entry['where'] = var['where'].text()
            if var['missing'] != 'absent':
                entry['missing'] = var['missing']
        raw['variables'][name] = entry
    for name, (dims, where, lhs, rhs) in constraints.items():
        entry = {'dims': ['g'] if dims else [], 'expression': f'{lhs.text()} <= {rhs.text()}'}
        if where is not None:
            entry['where'] = where.text()
        raw['constraints'][name] = entry
    if g.conds:
        raw['conditions'] = {n: c.text() for n, c in g.conds.items()}
    exprs = dict(g.yaml_exprs)
    exprs.update({n: e.text() for n, e in reported.items()})
    if exprs:
        raw['expressions'] = exprs
    model = (params, variables, g.conds, {**g.exprs, **reported}, constraints, reported)
    return raw, model


PRESENT = [-2, -1, -0.5, 0.5, 1, 2, 2.5, 3, 0, 1.7, -1.3]


def _value(rng, p):
    if p['dtype'] == 'bool':
        return rng.random() < 0.5
    return rng.choice(PRESENT) if rng.random() < 0.6 else rng.uniform(0.5, 3) * rng.choice([1, -1])


def _fill(rng, p):
    return (rng.random() < 0.5) if p['dtype'] == 'bool' else rng.uniform(0.5, 3) * rng.choice([1, -1])


def divides_by_zero(model, rng, draws=80):
    """(any zero division in a built row, the first zero divisions the missing rows caused or None)."""
    params, variables, conds, exprs, constraints, _ = model
    any_zero = False
    for n in range(draws):
        p_present = [0.0, 0.3, 0.7, 1.0][n % 4]
        data = {}
        for name, p in params.items():
            if not p['dims']:
                data[name] = _value(rng, p)
            else:
                data[name] = [
                    _value(rng, p) if p['missing'] == 'refused' or rng.random() < p_present else None for _ in LABELS
                ]
        w = World(params, data, variables, conds, exprs)
        for dims, where, lhs, rhs in constraints.values():
            for i in range(N) if dims else [0]:
                if where is not None and not where.ev(w, i):
                    continue
                _guarded(w, lambda i=i: _row(w, lhs, rhs, i))
        for e in exprs.values():
            for i in range(N):
                _guarded(w, lambda i=i, e=e: e.ev(w, i))
        any_zero |= bool(w.events)
        caused = [text for text, divisor, i in w.events if _caused_by_missing(divisor, i, w, rng)]
        if caused:
            return any_zero, {'data': data, 'events': caused[:3]}
    return any_zero, None


def _caused_by_missing(divisor, i, w, rng):
    """Whether the missing rows alone make *divisor* 0 at *i*: a zero the file put in.

    It stays 0 whatever the present rows hold, and stops being 0 once every row is present.
    """

    def at(refill):
        data = {
            name: _fill(rng, p) if not p['dims'] else [refill(v, p) for v in w.data[name]]
            for name, p in w.params.items()
        }
        return divisor.ev(World(w.params, data, w.variables, w.conds, w.exprs), i)

    for _ in range(4):
        if at(lambda v, p: None if v is None else _fill(rng, p)) != 0:
            return False
    return any(v is not ABSENT and v != 0 for v in (at(lambda v, p: _fill(rng, p)) for _ in range(3)))


def _row(w, lhs, rhs, i):
    a, b = lhs.ev(w, i), rhs.ev(w, i)
    return ABSENT if a is ABSENT or b is ABSENT else 0.0


def verdict(raw):
    try:
        to_spec(raw)
        return 'loads', ''
    except MathSpecError as e:
        lines = [l for l in str(e).splitlines() if l.strip()]
        div = [l for l in lines if DIV_MSG in l]
        if div and len(div) == len(lines):
            return 'refused-divisor', div[0]
        return 'refused-other', lines[0] if lines else ''
    except Exception as e:  # noqa: BLE001 — a crash is a finding
        return 'crash', f'{type(e).__name__}: {e}'


def main():
    start, stop = int(sys.argv[1]), int(sys.argv[2])
    out = sys.argv[3] if len(sys.argv) > 3 else None
    counts = {}
    findings = []
    for seed in range(start, stop):
        raw, model = draw(seed)
        v, msg = verdict(raw)
        if v == 'refused-other':
            counts['refused-other'] = counts.get('refused-other', 0) + 1
            continue
        any_zero, hit = divides_by_zero(model, random.Random(seed * 7919 + 1), 80 if v == 'loads' else 400)
        if v == 'crash':
            kind = 'crash'
        elif v == 'loads':
            kind = 'soundness' if hit else 'ok-loads'
        else:
            kind = 'ok-refused' if any_zero else 'precision'
        counts[kind] = counts.get(kind, 0) + 1
        if kind in ('soundness', 'precision', 'crash'):
            findings.append({'seed': seed, 'kind': kind, 'message': msg, 'hit': hit, 'spec': raw})
    print(json.dumps(counts, sort_keys=True))
    if out:
        with open(out, 'w') as fh:
            json.dump(findings, fh, indent=1, default=str)


if __name__ == '__main__':
    main()

---

Generated by Claude Code