test(fuzz): add deterministic state models - #21
Conversation
|
I ran a two-round adversarial review of the new fuzz oracles using six independent, persona-inspired review lenses. Each item below was reproduced with a temporary local mutation and then challenged by another reviewer. These are harness false positives, not claims that the current production code is broken. Requested before merge1. Make the lifecycle model independent of the code under testIn Two controlled broken implementations stayed green:
The completion ownership case has the same independence problem: it derives its snapshot expectation only after the target runs and checks the returned value only for being a proper list. Stripping all generated text properties passed after 4,465 candidates. Forcing every returned result to This lets the reference model agree with corrupt state or miss state that observers actually saw. Please build independent expected values before invoking production callbacks, record immutable source state inside the refresh callback, and assert the callback-owned state relevant to each operation and teardown. 2. Do not let the message oracle certify a wrong repair
Please make the three finite contexts ( Nonblocking follow-ups
Baseline remained green before mutations: 261/261 ERT tests, compile/replay, and state 300 × 40. The worktree was restored and verified clean after every probe. |
|
Phase-two oracle work is now on this branch at The two requested findings are addressed:
Intentionally still open in the catalog: the wider C04/C05 epoch and reentrant |
What this adds
This is stack PR 1 of 3. It adds deterministic fuzz tests for fzfa's Elisp
state boundaries and a catalog of the contracts that the stack is meant to
test.
It does not change
fzfa.el, any extension, or any existing test.The lane focuses on three places where order and ownership matter:
It also checks message delivery from the owning minibuffer, a producer worker
buffer, and a normal buffer with no active fzfa minibuffer.
What “qualified” means here
Reaching a line of code is not enough. An oracle is marked
qualifiedonlywhen the generator reaches the important event sequence and a controlled
broken behavior makes the oracle fail.
make selftestnow injects eight such defects. For example, it deliberately:nilinstead of the completion result;The self-test must reject all eight before generated state cases run. This
qualifies the oracles; it is not a claim that fuzzing proves the program free
of bugs.
Simple examples
A frontend changes its copy of a candidate list
Suppose fzfa has this saved snapshot:
The two
alphastrings are duplicates, but their metadata says that they camefrom different sources. Emacs completion code is allowed to sort, reverse,
truncate, deduplicate, or attach a dotted tail to the list it receives.
The fuzzer builds the expected values before it calls fzfa. It then requires
the chosen mutation to change the returned list and checks three things:
alphavalues andtheir properties; and
This catches a test bug where expected and actual values accidentally share
the same list structure.
An old producer answers late
A generated trace can say:
The model owns copies of callback input. It tracks snapshot, total, filtered
count, last result, producer token, and what state was visible inside each
refresh callback. Only the newest callback may publish. After stop, every old
callback and timer must be inert.
The generated part ends at its first
stop; an exhaustive teardown sweep thentries all saved callbacks and tasks. A static reachability check over 2,000
seeds requires current delivery, stale delivery, restart, stop, and a refresh
that was queued when stop happened.
A scheduled poll result becomes stale
The fixed replay does this:
A's old generation must not be committed to B. The contract catalog keeps the
larger request-epoch and reentrant-publication space marked partial; this replay
tests one specific replacement ordering.
A worker reports a message
The oracle checks all events, not only the first error it finds:
inline cue from the owner buffer;
event shape.
A controlled “repair” that suppresses echo but still runs the inline cue from
the worker buffer is rejected. The worker-buffer behavior itself remains
listed as a known product gap; this PR does not change it.
Contract catalog
fuzz/CONTRACTS.mdrecords fourteen historical contracts from the recentproducer, native-session, frontend, and live-minibuffer fixes. Each entry gives
a small failure witness, expected observable behavior, oracle, nearby inputs,
source evidence, and current status.
In this PR:
product gap; and
request-epoch and reentrant-publication ordering.
CI and local use
Pull requests run 300 cases with 40 lifecycle steps on Emacs 29.1, 30.1, and
snapshot. The weekly job runs 5,000 cases with 100 steps.
Failures include the seed and generated trace.
Verification performed
Stack