created by a gemini-powered agent
What's hard to do? (limit 100 words)
Currently, predicate functions in XLS DSLX must be annotated separately as either quickcheck or fuzz tests (they cannot be annotated as both simultaneously). Quickcheck (qc) runs via the DSLX interpreter and is faster for checking small domains, while fuzzing requires ahead-of-time (AOT) compilation and uses coverage guidance for broader domain exploration. Because annotations are separate, developers cannot easily switch between quickcheck and fuzz testing on the same predicate function.
Current best alternative workaround (limit 100 words)
Developers must maintain separate annotations or duplicate predicate wrappers to run both quickcheck and fuzz testing on the same domain properties, or choose one execution mode upfront and forgo the benefits of the other.
Your view of the "best case XLS enhancement" (limit 100 words)
Unify the annotation syntax for predicate functions so that a single annotation syntax is used for domain predicates, and allow selecting the execution mode/runner (qc vs fuzz) via test runner options.
Benefits:
- Simplifies DSLX predicate testing and avoids duplicate annotations.
- Allows running either quickcheck or fuzzing on the same predicates.
- Potentially allows collecting fuzz predicates for Z3 formal proofs (
prove_quickcheck_main).
What's hard to do? (limit 100 words)
Currently, predicate functions in XLS DSLX must be annotated separately as either quickcheck or fuzz tests (they cannot be annotated as both simultaneously). Quickcheck (
qc) runs via the DSLX interpreter and is faster for checking small domains, while fuzzing requires ahead-of-time (AOT) compilation and uses coverage guidance for broader domain exploration. Because annotations are separate, developers cannot easily switch between quickcheck and fuzz testing on the same predicate function.Current best alternative workaround (limit 100 words)
Developers must maintain separate annotations or duplicate predicate wrappers to run both quickcheck and fuzz testing on the same domain properties, or choose one execution mode upfront and forgo the benefits of the other.
Your view of the "best case XLS enhancement" (limit 100 words)
Unify the annotation syntax for predicate functions so that a single annotation syntax is used for domain predicates, and allow selecting the execution mode/runner (
qcvsfuzz) via test runner options.Benefits:
prove_quickcheck_main).