[enhancement] quickcheck constraints

[mikex-oss]

What's hard to do? (limit 100 words)

quickcheck works well when the input is constrained naturally by a type. However, oftentimes, I've found a need to constrain the value beyond this type. Quickcheck does not appear to support adding constraints as part of the metadata.

Current best alternative workaround (limit 100 words)

You can 1) ignore the sample by explicitly returning true for that case, e.g.

https://github.com/google/xls/blob/8c8ad0284fa8475ab5fd5fbda2de03f3950b6002/xls/examples/quickcheck.x#L33

This reduces the number of actual useful samples in the quickcheck.

Or 2) compose the actual value with multiple inputs to satisfy the constraint. This may affect the statistical distribution compared to a properly constrained input.

Your view of the "best case XLS enhancement" (limit 100 words)

It'd be nice to be able to do:

#[quickcheck(constraint="x%2 == 0 && x != 42")]
fn foo(x: u32) -> bool {

or similar

[proppy]

2. compose the actual value with multiple inputs to satisfy the constraint. This may affect the statistical distribution compared to a properly constrained input.

can you give an example?

or similar

I'd love to be able to reuse existing stdlib (or used-defined) function too:

#[quickcheck(constraint="has_fractional_part(x)")]
fn some_test_for_fractional_float(x: float32::F32) -> bool {
}

As a reference some pointer to Rust implementation of the same feature:

• https://github.com/BurntSushi/quickcheck?tab=readme-ov-file#discarding-test-results-or-properties-are-polymorphic does this w/ traits (related: #618)
• https://proptest-rs.github.io/proptest/proptest/tutorial/filtering.html has some filter expression syntax embedded in the argument list.

[mikex-oss]

2. compose the actual value with multiple inputs to satisfy the constraint. This may affect the statistical distribution compared to a properly constrained input.

can you give an example?

Something like: needing a u3 value between 0-6, instead of filtering out the 7, take two u2 inputs and add them, which is obviously not the same as a uniform distribution over a constrained single input.

[cdleary]

One of the weirdnesses here is you'll end up with DSLX errors reported on your "constraint string".

I'd recommend defining a constraint function in the module scope and then just referring to it by name to avoid that kind of issue. Not much more typing and should simplify the mechanism.

fn has_fractional_part(x: float32::F32) -> bool { ...}

#[quickcheck(constraint=has_fractional_part)]
fn some_test_for_fractional_float(x: float32::F32) -> bool {
}

[mikex-oss]

Yeah, I was just spitballing, particularly with the idea to simplify associating input args to constraints by name.

What would be the mechanism to deal with constraints when there are multiple input args? Does every constraint function take all inputs?

[cdleary]

What would be the mechanism to deal with constraints when there are multiple input args? Does every constraint function take all inputs?

That would make sense, or you /could/ pass an array, it's just getting passed to the annotation so the way we interpret the annotation in the DSL run routines can be pretty much arbitrary -- though if we can get away with the simpler thing that seems like it'd be nice.

[proppy]

One of the weirdnesses here is you'll end up with DSLX errors reported on your "constraint string".

+1, it might be a bit annoying to have to define intermediate functions to be able to combine logically multiple predicate (or/and/all/any), or maybe we need a syntax for currying ? :)

[proppy]

Sharing a small helper that we've been using to simplify the expression of preconditions for checking quick check properties.

So that instead of writing long chain of || negated preconditions (as discussed https://github.com/google/xls/issues/1574#issue-2495593047):

#[quickcheck]
fn some_test_prop(some_arg: u32) -> bool {
   // 10 <= some_arg <= 20
   let some_result = f(some_arg);
   (some_arg < 10 || some_arg > 20) || (some_result & u32:1 == u32:0)
}

You can write something more structured like:

#[quickcheck]
fn some_test_prop(some_arg: u32) -> bool {
   // 10 <= some_arg <= 20
   verify_predicates(Predicates {
	preconditions: bool[2]:[u32:10 <= some_arg, some_arg <= u32:20],
        properties: bool[1]:[f(some_arg) & u32:1 == u32:0],
   })
}

By using:

pub struct Predicates<N: u32, M: u32> { preconditions: bool[N], properties: bool[M] }

// Verify a set of predicates; meant to be used with quickcheck tests:
// - all preconditions must be true for the properties to be evaluated.
// - returns `true` if any of the preconditions is false or if all of the properties are true.
pub fn verify_predicates<N: u32, M: u32>(predicates: Predicates<N, M>) -> bool {
    let anti_preconditions = for (i, b): (u32, bool) in u32:0..N {
        b | !predicates.preconditions[i]
    }(false);
    let properties = for (i, b): (u32, bool) in u32:0..M {
        b && predicates.properties[i]
    }(true);
    let predicates = anti_preconditions || properties;
    predicates
}

One limitation is that it doesn't really support highlighting which condition fails (which is challenging because of #1949 and #1929), it would be nice to have some support at the language level for this.

/cc @dassbrothers who has also been exploring relatic topics in #1344 and #1549