fuzz: harvest custom inductive/structure types (Phase 3)#21
Merged
Conversation
Fragment-reuse now handles corpus functions whose params/return are custom
inductive or structure types (enums RPS/Player/Suit; structs Card/Nim/UnionFind),
not just the base value universe. Harvest 129 -> 145 (16 user-typed functions),
exercising the transpiler's inductive-emission + match-on-user-type paths under
differential testing for the first time.
Machinery:
- fuzz/TypeInfo.lean: Lean-side dump of each corpus type's constructors + field
types (robust vs. source regex / Lean version).
- corpus_frags: load type info; compute constructibility (all fields base or
constructible; recursive/Float types excluded); _rand_user_value builds
constructor values; _user_lean_lit emits Lean constructor applications; _json
emits {"c":ctor,"f":[...]}; _emit_user_serializers generates per-type Lean JSON
serializers (topologically ordered). Dotted def names (Card.value/RPS.beats)
now parse; short type names resolve via namespace prefixes.
- run_oracle.normalize reduces a transpiled @DataClass instance to the same
{"c":ctor,"f":[...]} shape; run_oracle.materialize + pycov.Harness._materialize
turn dict args back into dataclass instances for the Python call.
- ctor naming mirrors toPyTypeName: common ctor names (mk/node/…) are
parent-prefixed (Nim.mk -> dataclass Nim_mk) — separate Lean-match name (.mk)
from Python/JSON name (Nim_mk).
- --pycov-search skips user-typed fns (its mutators cover base types only); they
are validated by the main --corpus differential sweep.
Verified locally end-to-end (enums + Card + Nim + UnionFind: ALL AGREE vs
oracle); CI suites + round-trip 3807/3807 green. Scaled cloudnew sweep next.
VERIFICATION.md updated (Phase-3 note; F19+ to follow if the sweep finds bugs).
…ionFind) Phase-3 scaled sweep revealed two issues: 1. A hung oracle #eval can stall the whole pool with no recovery. lean_run now has a 60s timeout, treated as a Lean error (seed skipped) — a general robustness fix, not just Phase 3. 2. UnionFind has an internal invariant (acyclic parent array) that arbitrary field-filling violates, so find() loops forever. Types matching _UNSAFE_TO_CONSTRUCT are now non-constructible (the fuzzer can't safely build them). Harvest: 145 -> 139; 7 safe user-typed fns remain (Nim/Card/RPS). All 7 user-typed fns x 6 inputs AGREE with the oracle.
1500-seed cloudnew sweep over 139 harvestable functions (incl. 7 user-typed: Nim/Card/RPS) found no transpiler bug — inductive emission was already sound. Phase-3 findings were harness-side (UnionFind invariant nontermination -> excluded + lean_run timeout; common-ctor dataclass naming) and are fixed.
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.
Phase 3 of the bug-hunting roadmap — the largest unlock and hardest phase. Fragment-reuse now handles corpus functions whose parameters or return type are custom inductive/structure types (enums
RPS/Player/Suit; structsCard/Nim), exercising the transpiler's inductive-emission +match-on-user-type paths under differential testing for the first time.Harvest: 129 → 139 (7 safe user-typed functions:
Nim/Card/RPSmethods).Machinery
fuzz/TypeInfo.lean: Lean-side dump of each corpus type's constructors + field types (real environment — robust vs. source regex / Lean drift).corpus_frags: computes constructibility (fields all base-typed or themselves constructible; recursive types andFloatexcluded);_rand_user_valuebuilds constructor values;_jsonemits{"c":ctor,"f":[...]};_emit_user_serializersgenerates per-type Lean JSON serializers. Dotted def names (Card.value) parse; short type names resolve via namespace prefixes.run_oracle:normalizereduces a transpiled@dataclassto{"c":ctor,"f":[...]};materializeturns dict args back into dataclass instances. Constructor naming mirrorstoPyTypeName(common ctors likemk→Nim_mk).Result: transpiler is correct on this slice
A 1500-seed cloudnew sweep over 139 functions found 0 transpiler bugs — the inductive emission was already sound. The phase's findings were harness-side, both fixed:
UnionFind's parent array must be acyclic) makesfindloop forever → such types excluded (_UNSAFE_TO_CONSTRUCT), andlean_rungained a 60 s timeout so no hung#evalcan stall the pool (a general robustness win).mk/node) are parent-prefixed (Nim.mk→Nim_mk); the serializer andnormalizenow matchtoPyTypeName.Verification