Skip to content

test(fuzz): add deterministic state models - #21

Draft
dangduc wants to merge 3 commits into
jojojames:mainfrom
dangduc:codex/fzfa-fuzz-state-models
Draft

test(fuzz): add deterministic state models#21
dangduc wants to merge 3 commits into
jojojames:mainfrom
dangduc:codex/fzfa-fuzz-state-models

Conversation

@dangduc

@dangduc dangduc commented Sep 3, 2026

Copy link
Copy Markdown
Collaborator

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:

  1. completion frontends may change the candidate list they receive;
  2. producer callbacks and refresh timers may run after restart or stop; and
  3. a poll result may become stale before its scheduled publication runs.

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 qualified only
when the generator reaches the important event sequence and a controlled
broken behavior makes the oracle fail.

make selftest now injects eight such defects. For example, it deliberately:

  • returns nil instead of the completion result;
  • removes candidate text properties;
  • makes a returned list share structure with fzfa's saved snapshot;
  • lets an old producer callback publish;
  • calls refresh before the new state is visible;
  • lets a callback publish after teardown; and
  • sends an inline message from the wrong buffer.

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:

(#("alpha" 0 5 (fzfa-source 0))
 #("alpha" 0 5 (fzfa-source 1))
 "beta")

The two alpha strings are duplicates, but their metadata says that they came
from 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:

  • the first returned value was correct;
  • fzfa's saved per-source snapshots still contain both alpha values and
    their properties; and
  • a second lookup returns the same complete logical result.

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:

fetch "a"
fetch "ab"
deliver the callback for "a"
deliver the callback for "ab"
run a queued refresh
stop
deliver every saved callback again
run every queued timer again

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 then
tries 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:

poll handle A at generation 1
schedule a frontend publication
replace A with handle B
run A's old publication closure

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:

  • with an owning minibuffer, log once, suppress echo-area output, and issue the
    inline cue from the owner buffer;
  • with no owner, log once and do not issue an inline cue; and
  • for the current worker-buffer product gap, accept only the exact documented
    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.md records fourteen historical contracts from the recent
producer, 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:

  • FZFA-C01, C02, and C09 have qualified generators and oracles;
  • C10's oracle is qualified, while its worker-buffer behavior remains a known
    product gap; and
  • C04 and C05 remain partial because the generated model does not cover every
    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.

make -C fuzz compile selftest replay state
FZFA_FUZZ_SEED=123 make -C fuzz state CASES=1

Failures include the seed and generated trace.

Verification performed

  • fuzz harness byte compilation with warnings treated as errors;
  • eight controlled state defects rejected by their intended oracles;
  • fixed replay cases;
  • 300 generated state cases x 40 steps, root seed 1; and
  • the full aggregate repository suite: 261 expected, 0 unexpected.

Stack

@dangduc

dangduc commented Sep 3, 2026

Copy link
Copy Markdown
Collaborator Author

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 merge

1. Make the lifecycle model independent of the code under test

In fzfa-fuzz-state--producer-case (fuzz/fzfa-fuzz-state.el:149-270), the production callback receives candidates before the model stores the same object as model-snapshot. The model also observes refresh only as a count, and it does not model filtered or last-result.

Two controlled broken implementations stayed green:

  • Destructively corrupting a just-published snapshot was accepted 242 times in an 80-case × 30-step run because expected and actual state shared the same list.
  • Calling the refresh callback before publishing restart state passed 300 cases × 40 steps; a direct observer saw nil during refresh and ("fresh") only afterward.

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 nil also made every destructive mutation a no-op, although focused rank ERT catches that broader semantic break. Focus this fix on the empty-query ownership contract: construct an independent expected value before calling the table, require the destructive operation to change the returned list spine, and compare both lookups—including properties and multiplicity—to that expectation.

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

fzfa-fuzz-state--message-events records the buffer for each log/inline call, but fzfa-fuzz-state--message-violation ignores it and stops after the first violation. A controlled partial repair inhibited the echo and called minibuffer-message from the worker buffer. The harness printed RESOLVED message-owner/process and passed, even though both recorded calls occurred in the worker buffer.

Please make the three finite contexts (owner, process, and none) deterministic, check all relevant invariants, and require inline delivery from the minibuffer owner buffer. If the current process-buffer defect remains documented for now, accept only its exact known event shape—not either one of several first-found violations.

Nonblocking follow-ups

  • The ownership case reaches the default completion path but not the parallel Ivy copy site. Both production sites are currently correct; parameterizing this later would close that scope gap without making this PR depend on a frontend refactor.
  • After the first generated stop, 68% of the 300 × 40 operations and 86.5% of the weekly 5000 × 100 operations are stale deliveries/task runs already subsumed by the final exhaustive teardown sweep. Ending random generation at stop reduced a local weekly run from 18.60s to 7.12s without removing assertions.

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.

@dangduc

dangduc commented Sep 3, 2026

Copy link
Copy Markdown
Collaborator Author

Phase-two oracle work is now on this branch at 7a3cb35.

The two requested findings are addressed:

  • The completion oracle builds expected strings and list spines before it calls
    production code. It compares the first result, saved snapshots, and a second
    lookup, including duplicates and text properties. Its controlled failures
    cover a nil result, stripped properties, and result/snapshot aliasing.
  • The producer model copies callback input before delivery and tracks snapshot,
    total, filtered count, last result, and callback-time refresh views. Generated
    traces end at the first stop, followed by an exhaustive late-callback/task
    sweep. A 2,000-seed reachability check requires the important event shapes.
  • Message checks now run deterministic owner/process/none contexts, inspect all
    invariants and event buffers, and accept the current worker-buffer gap only
    when it has the exact known shape. A wrong-buffer inline canary is rejected.

make selftest rejects eight controlled defects. Compile, replay, state fuzz at
300 cases x 40 steps, and the aggregate 261-test ERT suite pass. The PR body now
explains the examples and qualification boundary in plain English.

Intentionally still open in the catalog: the wider C04/C05 epoch and reentrant
publication space, the C10 worker-buffer product gap, and a shared cross-lane
resource-leak oracle.

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

None yet

Projects

None yet

Development

Successfully merging this pull request may close these issues.

1 participant