Add @mettascript/fuzz: property testing written in MeTTa - #3
Closed
MesTTo wants to merge 49 commits into
Closed
Conversation
The fuzz effect table classified embedded ops when it was introduced, and log-enabled? arrived beside it on the reconciled base reading world.logLevel. The Pure fallthrough was behavior-neutral for the sandbox, which admits both Pure and World, but a world read must not be labeled referentially transparent, or a future consumer of the effect table could cache it across a pragma! log-level change.
A loop that only conses onto its state re-presents the same immutable subterms to isNormalForm and keyWellFormed on every step, and both re-walked the whole term each time: a 16k-step cons loop spent 28.6s in those walks. Atoms are immutable and instantiate shares unchanged subterms, so both verdicts are cacheable by node identity, the same lineage as exprVarsCache. isNormalForm entries carry the visible rule tables they were computed against: the env identity, its groundedEpoch (bumped on grounded registration), the world's selfRuleVersion, and the append-only static-removal log's identity. A node verified true covers its whole subtree; a false verdict lands on the deciding node and the queried root. keyWellFormed is purely structural, so its entries never expire. Core suite 1113 tests and the 23-file Hyperon oracle pass unchanged.
scopeVars instantiated every pending frame just to read variable names, so a frame embedding a large accumulator cost O(state) per metta-thread call. Walk the raw frame atoms instead and expand each name through the binding with the memoised fixpoint resolver; ground values contribute nothing, so the walk is O(live set). Same disease chainLiveVars was cured of in fd574b8.
isInertData bailed on any defined head, so quote-protected results and signature-only constructors (declared, type-checked, but never reducibly defined) re-entered interpret-tuple on every read, costing O(n^2) threading over machine states. Classify a head as reducible only when a visible static rule can actually rewrite it, admit standard quote immediately, and let constructor applications pass the same type check the interpreter would run. Verdicts are cached by node identity with the normalFormCache entry signature plus the space version, so a rule or space change invalidates them.
containsImpureHead and hasNanGround re-walked whole terms although machine states rebuild a fresh wrapper around the same large accumulator every step. Cache the impure-head verdict by node identity keyed per impure-op set, and memoise every expression a clean NaN walk visits instead of only the queried root, so each shared subtree is scanned once per process rather than once per wrapper.
The grammar slice interpreted every representation walk, so deep templates overflowed the evaluator and wide ones paid interpreter cost per node. Normalization, template plans, requirement set algebra, eligibility, productivity, and decision-leaf extraction are now single grounded kernel calls over raw template syntax, and generation itself runs on a kernel machine that replicates the MeTTa specification machine transition for transition. User Field callbacks and custom generators are served through a MeTTa trampoline as suspension effects, so fuzzing policy and callbacks stay ordinary MeTTa relations. The specification machine and the productivity fixed point remain callable under -reference names, and a differential test drives default and reference against identical Random, Edge, Replay, ShrinkReplay, and Exhaustive drivers; it caught a frozen _fuzz-two-children construction in the reference production arm, fixed here by let-binding. Regression tests pin deep and wide templates, reference chains, opaque marker payloads, Field freeze-once semantics, replay mutation rejection, many-seed identity, type schemas, and wall-clock scaling gates. A freshness test keeps the generated module in lockstep with the MeTTa sources on the test path, the dead _fuzz-grammar-requirement-plan op and stale declarations are removed, and the shared template walkers are factored (scanTemplateLeaves, rewriteTemplateLeaves, parseProductionsTargetArgs).
The prefix-product exhaustive driver was unsound for dependent generators: it forked every integer decision through superpose and sized the domain as a product of choice counts, so (gen-bind (gen-bool) dependent) claimed four decision trees where only three exist. The driver is now a deterministic depth-first cursor, (ExhaustiveCursor choices cursor frames): each integer decision reads its planned offset or defaults to zero and records an (ExhaustiveFrame offset count); after a terminal outcome the odometer increments the rightmost frame with another branch and truncates the suffix, so dependent suffixes are reconstructed run by run. The kernel grammar machine mirrors the same transition and loses its fork machinery; the machine-vs-reference differential now drives resumed cursors through both machines. fuzz-enumerate walks a generator's whole domain at one size and reports (FuzzEnumeration (DomainCount n) (Enumerated m) (GenerationDiscards g) (Samples ...)), truncating at its attempt limit. fuzz-check-exhaustive makes the stronger claim behind exit-code semantics: every accepted tree at MaxSize is replayed and checked, a counterexample goes through the standard failure pipeline with (Exhaustive (Choices ...)) replay coordinates, the MaxEnumerated cap and property discards give explicit FuzzGaveUp results, an empty accepted domain is FuzzInvalid, and coverage requirements are judged against the exact domain. Weights now bias only the Random ticket draw: gen-frequency records its decision in entry-index space like grammar production choice, so exhaustive enumeration visits each entry once and replayed trees are weight-independent.
Grounded operations received state handles pre-resolved to their cell contents, so a handle flowing through collapse, cons-atom, or a list operation silently became its value and get-state on the result failed. Hyperon passes handles through opaquely (verified live on 0.2.10: a handle survives collapse/superpose/cons round trips), so the grounded argument preparation now substitutes tokens only. The two comparator families are the exception: == and the assert result comparators judge states by VALUE in Hyperon ((== (new-state 1) (new-state 1)) is True), so stateValueCompareOps keeps resolving for exactly those heads while space reads and match patterns resolve as before (the live-state read feature). The grounded-exec head path drops resolution the same way.
A tail transfer in the reduce trampoline reused the caller's logical depth and consumed nothing, so a runaway tail cycle (mutual recursion, a phase flip, a compiled-operator spin) ran forever while every legitimate deep tail loop depended on the native stack as its accident of a bound. Each transfer now debits one unit of fuel, MOPS's per-transition cost, and exhaustion cuts with the standard (Error <call> StackOverflow) atom, effects kept, as Hyperon's error model keeps prior add-atoms. The lone-catch-all carve-out is gone with its reason: it existed only because the loop deliberately consumed no fuel. Transfers also continue through chain-internal steps that carry app-local variables (a let pattern flowing through its prelude unify body). The entry step must still be var-free, and finalPair instantiates every result, so a bound variable bakes its value into the transferred atom and only genuinely unbound ones stay free; without this every let-wrapped tail loop fell out of the trampoline at the queryVars guard and nested one evaluator frame per step. Deep interpreted let-recursion ((build 200000) with an add-atom binding) now completes flat instead of exhausting memory. Resource cuts now surface on the trace bus at the public entry (restrictPublicLimitBindings): cuts arrive from several layers - the trampoline's fuel cut, the plan machine's exhaustion, a compiled runtime cut - and the query-level event is what the native-overflow catch always reported.
Logical depth misses tail transfers (they reuse their level), so a long chain of wrapped tail steps nested one native generator quartet per step and a few thousand of them exhausted the host stack; the machine fuzz checks died at six runs on exactly that. EvaluationDepth now counts native frame descents separately, and mettaEvalG hands a branch to the heap continuation driver once the count crosses NATIVE_EVALUATION_NESTING_LIMIT, so deep nesting runs on the heap and the guarded multi-rule count-down completes in every mode. Open atoms (unbound variables left after instantiation) stay exempt: an open self-expansion mints fresh variables at every level at constant logical depth (compile-symbolic's (Greater $x $y) regress), so the heap driver would branch on it until memory dies, while native recursion cuts it fast and the top-level catch reports the observable (Error <query> StackOverflow) at counter zero, byte-identical to the prior behavior.
A tail call in a compiled imperative body invoked the callee's run directly, so a deep tail-recursive impure chain grew one JS frame per step and overflowed the host stack at a few tens of thousands of iterations, while the interpreter's flat tail semantics now complete the same chain: a genuine compiled-versus-interpreted divergence, in the slow direction. Hyperon completes this shape (verified live: build/add-atom recursion returns done plus every item) and PeTTa runs it flat through last-call optimization. A tail call now returns an ImpTail transfer sentinel instead of invoking, and impDrive at the holder entry loops on sentinels: one JS frame for the whole chain, matespace-class saturation walks included. Each hop debits one unit of fuel (threaded through CompiledImpureOps from the evaluator boundary), so a runaway impure cycle cuts with (Error <call> StackOverflow) instead of spinning; compiled (build 1000000) completes in under a second. Non-tail recursion keeps its native-overflow contract. The case-match node defers a tail sentinel only from the last solution with no earlier survivor, where the branch result is the case's result verbatim; every other position must know the branch's value for Empty-pruning and the single-survivor check, so it drives the sentinel in place. The deep compile-impure regression guard is inverted to pin completion in both modes - flat frames are what make completing it safe - plus a fuel-cut guard for the runaway cycle.
A misplaced closing paren can keep a fragment globally balanced while folding sibling switch arms into one arm; switch-internal then reduces the whole call to Empty silently, which cost a debugging session on a five-item machine draw-step arm. The generator now parses every fragment (string- and comment-aware) and rejects any switch or switch-minimal arm that is not exactly (pattern template) before emitting the module, in both generate and --check modes.
_fuzz-call-one handed collapse-bind to the validator as an evaluated argument, and a %Undefined%-typed argument branches first: with a two-rule relation both engines (Hyperon 0.2.10 verified) reduce the call nondeterministically before collapse-bind can collect, so the cardinality check saw parallel singleton results and a nondeterministic user relation slipped through as two passing runs instead of being rejected. The collapse-bind now sits inside a function/chain context with a metta interpretation, the prelude's own case idiom, so the call reaches it raw and every branch lands in one pair list. The multiple-results error also reports plain values again ((Results (1 2))) instead of leaking internal (value bindings) pairs.
_fuzz-drive-custom-results kept a superpose arm for the exhaustive mode, a leftover from the prefix-product driver that forked custom generators through nondeterminism. Every driver mode is deterministic now (the exhaustive cursor included), so the validator accepts exactly one DriveCustom result in every mode and the special case is gone.
A custom generator's own ShrinkChoices candidates were appended after the built-in child descent, so a structural candidate that removes a whole subtree (a machine command chunk) was only reached once every child pass had run and the search had already committed to smaller edits. Root candidates come first at both levels now: the custom relation's validated choices, then the generic child descent, which is the order the shrink search needs to reach the coarse edits while they still apply.
The shrink search accepted any candidate that reproduced the failure, so a candidate could re-inflate an accepted counterexample: the lenient shrink replay fills missing draws from each decision's origin, and a longer run that still fails is still a reproduction. A machine counterexample shrunk to three increments went back up to six that way. Two guards, both stated in terms of the published order (mettascript-shrink-v1 = shortlex over the flattened decision leaves, fewer leaves first, then lexicographically smaller origin distances). The runner accepts a reproducing candidate only when its canonical tree is strictly smaller under that order, which no candidate source (a built-in pass or a custom ShrinkChoices relation) can bypass. And the int candidate ladder offers a bound only when the bound sits strictly closer to the origin than the current value: the far-side bound was an anti-shrink, and a bound at the same distance is a lateral move the order could never accept anyway.
A machine is declared as ordinary MeTTa data, (FuzzMachine Name (InitialModel ..) (InitializeReal ..) (CommandGenerator ..) (Precondition ..) (Execute ..) (NextModel ..) (Postcondition ..) (Invariant ..) (Cleanup ..)), and reaches the runner through two ordinary pieces: (gen-machine Name) generates command sequences and fuzz-machine-run is an arity-one property that executes them. So machines inherit fuzz-check, fuzz-check-exhaustive, replay, and shrinking with no special cases in the runner. Generation walks the abstract model only. Each step asks the user generator for a command generator, draws from it, and retries up to sixteen times until the precondition holds, recording every attempt in a MachineCommand decision node so replay repeats the rejected draws; NextModel then threads the model forward. Since NextModel never sees the real system, the model cannot absorb the behavior it is meant to predict. Execution checks the invariant before the first command and after every model update, rechecks each precondition (a violation discards rather than fails, since the model may have drifted), judges the postcondition against the PRE-command model, and always runs cleanup - a cleanup error surfaces only when the run itself passed, so it can never mask a counterexample. Shrinking removes command chunks largest-first through a custom ShrinkChoices relation, then the generic child descent shrinks individual commands; every candidate replays from the initial model, so a chunk whose suffix no longer satisfies its preconditions is rejected.
fuzz-reachable explores a model transition relation as deterministic level-order breadth-first search, so the first witness it finds is shortest in transition count. The command enumerator returns (FiniteCommands ...) or (IncompleteCommands reason); a transition may return several next states and the whole ordered bag becomes outgoing edges, with each branch's index recorded so a witness names exactly one branch through a nondeterministic step. The outcomes are deliberately distinct. FuzzReachable carries a witness replayed from the initial model first: every step re-enumerates the commands, requires the recorded command at its recorded index, takes the recorded branch without deduplication, and the final state must satisfy the target. A mismatch means the model is not a function of its state, so the witness is not evidence and the result is a cutoff, never a reachable claim. FuzzUnreachableWithinDepth says only that no target occurred at or below the depth completed. FuzzReachabilityExhausted requires an empty frontier with every enumeration complete and no limit fired, so it means unreachable in the declared finite model and nothing about an external system. Every limit, incomplete enumeration, relation failure, or replay mismatch stays a FuzzReachabilityCutoff. Ordering is part of the contract: a transition branch is counted before any deduplication, the target is judged on a produced state before MaxStates can cut, and the initial state is checked before expansion. Identity is exact structural equality by default, through _fuzz-atom-key whose key is a length-prefixed serialization rather than a hash, so key equality IS state identity and distinct states cannot collide. (StateIdentity Alpha) merges alpha-variant states and is refused unless the user declares (FuzzReachEquivariant Name), since equivariance is a claim about the model. A state whose grounded payload has no serialization is an explicit UnkeyableState result, never a silently missed state. Every loop is a flat accumulator, which a 400-state chain test pins: the frontier, command, branch, and replay walks each iterate once per state. The same scaling gate caught two existing recurse-then-cons helpers, _fuzz-pair-values and the shrink order's _fuzz-leaf-distances, which failed between 200 and 600 elements and are now flat as well.
analyzeTableWorth admits a pure recursive component to automatic memo tabling when some rule body contains two or more calls into that component, the fib-style overlap case. The count was textual, so the prelude's own let* rule looked doubly recursive: its second mention of let* is (Error (let* $pairs $template) bad-let-star), a diagnostic payload rather than a call. let* was therefore tabled, and since it carries whole templates and accumulators its keys were the largest in the system while never hitting: a 200-iteration accumulator loop spent 3.5 million key tokens on let* alone, which made every MeTTa loop that threads an accumulator through let* quadratic in time with unbounded memory growth. functorCallCount now skips positions that can never become a redex, and the predicate covers only Error: its parameters are declared Atom, it has no equation, and no evaluator instruction hands an Error argument back for evaluation (verified directly - the payload of (Error (boom) r) stays unreduced through let, if-error, and return-on-error). Control constructs are deliberately NOT covered even where a parameter is declared unevaluated, because let rewrites to unify and unify returns the chosen branch for the caller to evaluate; a broader rule keyed on the declared type, or on the head simply lacking equations, wrongly excluded unify's branches and cost the read fixture its space-read table. Over-counting only risks tabling something, which is the prior behaviour, so the predicate stays narrow. Measured on a 400-step accumulator loop: 6.53s and 1479MB before, 2.53s and 227MB after, with the curve now linear and flat, matching the tabling-disabled baseline. Tabling still pays where it should (tabled fib remains fast) and the standing byte-identical differential over the adversarial corpus and 300 generated programs is unchanged, which is what guarantees admission cannot alter results.
gen-list expands its drawn length into that many copies of the element generator, and _fuzz-repeat-generator built the list by recursing then consing, so it cost an evaluator frame per element and a thousand-element list was impossible. The loop is now a flat accumulator; every element is the same generator, so accumulation order is not observable and no final reverse is needed. With this and the let* tabling admission fix, a thousand-element list generates in 1.19s using 205MB at the default depth and step budgets, where 300 elements previously failed while allocating 1.8GB. The new generator test pins that at defaults so neither cause can come back.
Every automatic-tabling decision rested on a static guess: analyzeTableWorth admits a functor whose body branches into its own strongly-connected component at least twice. The guess is cheap and usually right, but a wrong one is expensive, and the preceding commit is the proof - a single diagnostic mention of let* inside an Error payload was enough to memoize the busiest control construct in the language with keys that could never hit. Admission now also watches the outcome. TableSpace records inserts and reads per functor, and once a functor has stored 256 entries without a single read it stops being tabled for the rest of the run. A table is a pure memo, so refusing one can only cost time and never change a result, which is what makes measuring rather than proving safe here; the standing byte-identical differential against untabled evaluation is unchanged. The key carries its own functor because a chain of keys remembered together can span several. Statistics are shared across the key domains, so a functor that pays in one keeps its table in all of them - the conservative direction. The threshold sits far above any real warm-up and far below the waste it prevents. It is also aligned with the admission criterion it backs up: branching into your own component is exactly what produces repeated subcalls, so a memo that pays starts hitting within a few entries, while one that stores hundreds of distinct keys with no read is a functor whose branching was illusory or whose arguments are never repeated. Both admission paths are gated. Ground calls go through groundTableVersionIfAdmissible; non-ground moded calls are admitted by a separate block in the reduce trampoline, and gating only the first did nothing at all for let*, which is non-ground. Measured on a 400-step accumulator loop with the analysis fix reverted, so the mechanism is doing the work on its own: 6.53s and 1479MB before, 2.37s and 271MB after, about 95% of the win recovered without knowing the bug exists. On the corpus nothing regresses and the tabling-heavy cases improve (peano 0.86x, matespacefast 0.96x).
A run returns one result atom carrying everything a caller needs, and a host that wants to render, persist, or exit on it should not re-parse that atom by string matching. decodeFuzzOutcome turns each public outcome - passed, failed, gave-up, exhaustively verified, invalid, and the four reachability answers - into a discriminated value with the original atom kept alongside, so JSON output and artifacts still carry the full result. Strict means an unrecognized shape decodes as undecodable with a reason, never a partially filled success: tolerating a shape change would let a host report a pass for a result it did not understand, which is the one failure mode worth designing against. The tests feed the library's own output back through the decoder rather than hand-written imitations, so drift on the MeTTa side fails here. Exit codes are part of the contract: 0 for a definitive pass, 1 for a property failure, 2 for invalid input or data that could not be trusted, 3 for an incomplete run. Across a suite the most severe wins, and the precedence is deliberate - invalid outranks a failure because the run could not be trusted to execute, and a failure outranks incomplete because a found counterexample is the more actionable finding. Reachability answers are graded by completeness rather than by whether finding the target is good news, which the tool cannot know: a replayed witness and a finite exhaustion are definitive, while a depth answer and any cutoff are explicitly bounded and report incomplete.
A file now declares its tests as ordinary facts instead of through a
second host-side test DSL:
(FuzzTest reverse-involution (gen-list (gen-int -100 100) 0 40)
reverse-involution (fuzz-config (Runs 200)))
fuzz-run-suite finds every FuzzTest fact and runs it through the ordinary
fuzz-check, so a declaration is exactly what a hand-written query would
have been and inherits replay, shrinking, and exhaustive enumeration with
no special cases. The generator stays syntax in the declaration and is
evaluated once per run when fuzz-check receives it. fuzz-suite-tests lists
declarations without running them, and each result is paired with its test
id so a host reports per-test without re-deriving identity from the result
atom.
Command-line overrides merge by REPLACEMENT. A config carrying the same
option twice is an explicit DuplicateOption error, so appending would break
every run that overrides an option the test already set; the test's other
choices survive.
Two evaluation-order traps, both worth naming because they are silent. The
loop trio is deliberately left undeclared: an Atom parameter freezes its
argument, so declaring the loop would freeze the step call it is handed,
run exactly one iteration, and return that unevaluated call as the result.
And the merged config is inspected with unify rather than switch, because
switch evaluates its scrutinee: a config that normalizes into a validation
error would match an error arm that then reports the pre-evaluation syntax
instead of the error itself.
MaxDepth used to bound the levels the search expanded, so it generated and target-checked states one level deeper: a search asked for MaxDepth 2 could report a three-command witness, and a depth answer named a smaller depth than the one it had actually verified. MaxDepth now bounds the depth of every state considered, so a witness never exceeds it and FuzzUnreachableWithinDepth means exactly "every state at or below this depth was generated and judged". The boundary level is still enumerated, because a state with no command ends the model while a state with commands continues past the bound, and that is what separates exhaustion from a depth answer. A boundary state that does have commands leaves a marker in the next level instead of being stepped, so no transition is charged and no out-of-bound state is ever built.
…each A suite file declares its tests as data, so the CLI reads the file's declarations, drops its own directives, and evaluates its own query instead. Dropping them is the point: reading a suite must not execute whatever else the file would have run. `import!` and `register-module!` are kept, because a property defined in an imported file is undefined without them. Reachability searches are now discoverable the same way, through FuzzReachTest, and both suites take command-line settings as config overrides. The merge is one head-parameterized routine serving fuzz-config and reach-config, and it names an option by its head symbol rather than through the fuzz-config whitelist, which reported every reach option as InvalidOption and so kept the option it was supposed to replace. Exit codes: 0 pass or definitive answer, 1 property failure, 2 invalid input or data, 3 incomplete run. Precedence is worst-first across a run, with invalid outranking a failure because it means the run could not be trusted to execute. A witness longer than eight commands is elided with its true length, since the full command list is in the result atom and --json prints it.
The runner already had the replay phase: it matches (FuzzRegression <property> <value> <replay>) facts in the space and runs them before generating anything. A corpus is those facts written down, which `metta fuzz --corpus <dir>` now reads before a run and records into after one. Entries go through the same versioned codec MeTTa uses for replay rather than plain formatting, because a counterexample may have no source syntax: a float is stored as its two 32-bit words, so NaN, the infinities and negative zero survive exactly, and a value carrying a live host object is refused outright instead of being written back as something else. Each entry is one file named for the digest of its own text, so recording a counterexample that is already stored writes the name that is already there: deduplication is structural and a write never has to consider replacing another entry. New files land through a temporary name in the same directory followed by a rename. A corpus file that cannot be read stops the run with exit 2. Skipping it would drop a known failure while still reporting the run as complete. Every top-level atom in a file must be one well-formed entry, so nothing else in it can travel into the program alongside the entries. Results now go to stdout and diagnostics to stderr, so --json prints exactly one document however much the run has to say about the corpus.
@mettascript/fuzz had no @metta-ts/fuzz shim beside it and sat at 2.5.1 while every other package was at 2.7.0, which the release bump refuses to run across. Both are now fixed, and the parity test checks the pairing in the direction that would have caught it: walking compat/* alone cannot notice a canonical with no shim, so it now also asserts every publishable package has one and that all of them carry the same version. The README's MeTTa examples are executed by a test rather than trusted. Writing them turned up two things a reader would have hit: the state-machine fields were named from memory and wrong, and 200 runs report 213 passes because Runs counts the random cases with edge cases drawn on top. The counts printed in the README are now read out of the document and checked against a real run, and every gen-/expect-/fuzz-/reach- name it mentions must appear as a whole token in the library, which is the check that catches `fuzz-machine` for `fuzz-check-machine`.
… a run A tutorial and an API reference for @mettascript/fuzz, wired into the sidebar, the packages overview, and the CLI page. Both new pages are executed by a test: every MeTTa block runs in document order, every outcome kind the prose prints has to be one the run produced, and every count, shrunk value and witness printed is matched verbatim against the results. Writing them under that check turned up three things a reader would have hit. `gen-grammar` takes the name of a declared FuzzGrammar, not an inline grammar term, so the example errored with MissingGrammar. There is no `fuzz-label`; the annotations are fuzz-annotate, fuzz-classify, fuzz-collect and fuzz-cover, and cover takes its percentage first. And the shrinking example shrank nothing, because its failure came from an edge case that was already minimal: with a minimum length of one and edge cases off it now finds (4 -5) and reduces it to (-1) in five attempts, which is what the surrounding prose claims. The CLI's options are compared with the documentation page in both directions, since a documented flag that is silently ignored is worse than one that is missing.
…erty The typed view of a failure carried only the shrunk value, though the result carries the original too and the difference between them is the information a reader wants. Both are decoded now, and a decoded field is the value rather than the label around it: the details fields and the replay come out as their records, the way the smallest value already did. Node, browser, and hyperon each tested that the fuzz kernel's grounded operations were registered, which is not the same claim as the MeTTa module being usable. Each now runs a whole fuzz-check through its own entry point. The example this all exists for is in examples/property-testing.ts and its suite file, both run by the CLI test, so an example that stops working fails rather than sitting there. Writing the TypeScript one is what turned up the missing original value.
Running the example suite under --exhaustive took over three minutes before reporting EnumerationLimit. Measured as the marginal cost of one more case, a case here is milliseconds of interpreted MeTTa: about 7ms for a scalar generator, 12ms for a small list, 18ms for a list of forty under the exhaustive cursor. The default bound of 10000 multiplied straight into that, so a domain that could never fit was walked for minutes before the run could say so. A thousand keeps it under half a minute, and a larger domain is still coverable by asking. The measurement is worth stating precisely: the exhaustive cursor is only 1.2x the random driver on the same generator, and per-case cost does not depend on the size of an integer range, so this is the run loop's own cost rather than anything about enumeration. Six of the twelve defaults on the reference page were wrong, all of them plausible. The page's table is now read out of the document and compared with what the library reports, so a default written from memory fails.
They agree on the scalar kinds and differ on numbers, which is the point: a replay key has to separate values a rerun must reproduce exactly, so an integer keeps its kind and a float keys on its bits, while an identity key has to match core's numeric equality and keys both on the Number projection. Factoring the agreeing arms together would save four lines and hide the one distinction a reader has to check, so a duplication report on this pair is expected.
Every package moves together, which the release script refuses to do unless they start in lockstep. Release notes cover the fuzz library, the CLI subcommands, the collapse change that was sitting unreleased, and the interpreter work on deep tail recursion and tabling, with the tabling numbers quoted from the commit that measured them rather than from memory. The notes' current section is now executed by the documentation check, the same way the README and the website pages are. Earlier sections are left alone: their examples belong to the releases they describe.
The tutorial and the reference were reachable from the sidebar but nothing led to them: the landing page listed nine things the toolkit does without this one, and the only place a new reader is told where to go next did not mention it.
It pairs a fuel budget with a wall clock, because a mode that ignored fuel would run forever and a timeout is how that shows up. The first version paired 200,000 fuel with ten seconds, which passed here and timed out on a shared CI runner that was also running the differential suite: the slowest of the twelve combinations crossed the budget and the test read as a fuel bug when the machine was just busy. Burning fuel costs time in proportion to it, 3.9s for 200,000 and 1.1s for 50,000 in the slowest mode, with the same StackOverflow outcome at every level. The budget is now 50,000 fuel against a minute, so only a mode that never terminates reaches the clock.
Owner
Author
|
Landed on |
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
1 participant
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
Adds
@mettascript/fuzz, a property-testing library written in MeTTa, plus the CLI, engine, anddocumentation work that goes with it. Prepared as 2.8.0.
The library
Generation, shrinking, the run loop, the state machines, and the search are rewrite rules in
packages/fuzz/src/metta. TypeScript supplies only what a representation needs: a random source, astructural key over atoms, and a versioned atom codec.
shrunk, or enumerated. Scalars, text, structure, the combinators, and grammar and type-directed
generation for producing well-formed terms instead of random trees.
seed, and the result says whether it reached a local minimum or stopped early and why.
a domain that does not fit the bound is an incomplete run, never a verified one.
the real system from its model.
witness is replayed from the initial state before it is reported, and the four answers stay distinct:
a witness, exhaustion of a finite model, nothing at or below
MaxDepth, and a cutoff.The CLI
metta fuzzandmetta reachrun the declarations a file carries, not the file's own!queries, sodiscovery cannot become a way to execute whatever else a file would have done. Exit codes make the command
a test gate: 0 pass or definitive answer, 1 property failure, 2 invalid input or corrupt stored data, 3
incomplete run.
--corpus <dir>keeps found counterexamples as text so a later run replays them first, one file per casenamed for the digest of its contents. Values go through the versioned codec rather than being printed, so
NaNand-0.0survive exactly, and a corpus file that cannot be read stops the run instead of quietlydropping a known failure.
Engine
chain continues past bound variables. Native nesting is capped, with open atoms exempt. Deep flat
recursion that used to report
StackOverflownow completes.Errorpayloads no longer count as recursive calls for tabling, which had gotlet*memoized with keysthat could never hit: a 400-step accumulator loop went from 6.53s and 1479MB to 2.53s and 227MB, linear.
A table whose memo goes unread is also revoked now, per functor.
collapsereturns a plain expression of its ordered results, matching current Hyperon. This is thebehaviour change to know about: an empty collapse is
()rather than(,).Documentation is executed, not asserted
The README, the two website pages, and the current section of RELEASE_NOTES.md are run by tests. Every
MeTTa block executes in document order, every printed count and shrunk value is matched against the real
result, and every
gen-/expect-/fuzz-/reach-name mentioned must exist as a whole token in thelibrary. That check earned its place: it caught state-machine fields named from memory,
gen-grammargivenan inline grammar instead of a declared one, a
fuzz-labelthat does not exist, a shrinking example thatshrank nothing, and six of twelve wrong defaults in the reference table.
Verification
pnpm install --frozen-lockfile,pnpm build,pnpm lint,pnpm format:check,pnpm typecheckallclean, and all 169 test files pass, run in four batches because the whole suite at once exhausts memory on
the machine used. The packed tarballs were installed into a clean project and exercised under both scopes,
@mettascript/fuzzand@metta-ts/fuzz.Benchmarks were run but the machine was loaded at the time, so those numbers are noise-dominated and are
not offered as a clean comparison. The only change to
packages/core/srcafter the last quiet A/B is atest file.