Prototype for property-based testing

[translatenix]

Some time ago, I implemented a fairly complete prototype for property-based testing in Pkl. Here is a small (and artificial) example:

mytest.pkl

amends "pkl:test"

properties {
  ["reverse string"] { string: String(length == 99) ->
    string.length == 99
    string.reverse().reverse() == string
  }
  ["set"] { set: Set<String(isAscii)> ->
    set.isEmpty
  }
  ["person"] { p: Person(firstName.isWithinCharRange("a", "f")) ->
    p.fullName.startsWith(p.firstName)
    p.fullName.endsWith(p.lastName)
    p.firstName.isWithinCharRange("a", "f")
  }
}

settings {
  properties {
    tries = 1000
  }
}

local class Person {
  firstName: String
  lastName: String
  fixed fullName: String = "\(firstName) \(lastName)"
}

Running pkl test mytest.pkl produces the following output:

module mytest (file:///home/translatenix/pkl/mytest.pkl, line 1)
  reverse string ✅
  set ❌
    set.isEmpty ❌ (file:///home/translatenix/pkl/mytest.pkl, line 8)
    Falsified for set = Set("")
  person ✅

Generation of property inputs is entirely driven by test parameter types
such as String(length == 99) and Person(firstName.isWithinCharRange("a", "f")). (String.isWithinCharRange is one of several predicates I added to the stdlib.) Values of almost all Pkl types can be generated, including almost all stdlib types.

Many constraints, including those used in the above example, are understood and used to inform input generation. Constraints that aren't understood are used to discard generated inputs. If more than settings.properties.maxDiscardRatio inputs are discarded, the test fails.

When a property is falsified, inputs are shrunk to find a small counterexample. In the above example, shrinking produced the smallest possible counterexample Set(""). Shrinking is essential for a good user experience.

Why I stopped working towards a PR

Input generation and shrinking is delegated to jqwik, a Java library for property-based testing. Unfortunately, jqwik is heavily tied to JUnit. While jqwik can also be used as a plain Java library, its public API is quite limited (no shrinking), and JUnit is still required at runtime.

To overcome these limitations, I had to make substantial changes to jqwik's source code. Eventually I concluded that modifying jqwik's source code is a showstopper, even just to get my PR through a code review.

As far as I know, jqwik is the only actively maintained property-based testing library for Java. jqwik 2.0 plans to offer a standalone library that supports shrinking and doesn't depend on JUnit. However, due to a lack of funding, its development has stalled.

kotest-property looks promising but is implemented in Kotlin, which seems to rule out its use in a Pkl stdlib module.

[jlink]

jqwik 2 will have an API independent from JUnit. You may want to participate in the discussion about a good API on https://github.com/jqwik-team/jqwik2-api-discussion

[translatenix]

Thanks for chiming in! I love jqwik, and the plan for jqwik 2 looks great. I’m just not sure when it’s going to happen. I totally understand that your time is limited. Perhaps Apple would like to sponsor jqwik? :-)

[jlink]

I'm open to any offers :-)

[bioball]

We'd love property-based testing in Pkl! CC @holzensp, who's bought it up many times in our convos.

Looking at your example: how does it work? For example, how does the test runner know to supply values of String(length == 99)?

Do you have a commit with this pushed up anywhere? Would love to take a look.

Also, maybe silly question (my knowledge is limited here): have you considered hand-rolling PBT? Do we need to depend on a library for this?

[translatenix]

For example, how does the test runner know to supply values of String(length == 99)?

It analyzes the Truffle AST for String(length == 99) and builds the corresponding jqwik generator StringArbitrary.ofLength(99).
It knows how to resolve type and variable names (unfortunately they are unresolved in the Truffle AST) and knows certain stdlib methods (String.length, Int.isOdd, Number.isBetween, and many more), comparison operators, etc.
It can handle things like Person(name.isAscii, address.street.length <= 10). :-)

Do you have a commit with this pushed up anywhere? Would love to take a look.

It's quite a large change set, and I might have to clean it up first. :-)

have you considered hand-rolling PBT

I did for a moment, but implementing high-quality generators and shrinkers isn't easy.
What I did instead was to move a subset of jqwik's source code into Pkl's codebase.
However, to get rid of the JUnit dependency and unneeded code, I had to make a lot of changes,
and the resulting jqwik codebase was still much larger than I had hoped (well over 100 Java files).

[bioball]

It analyzes the Truffle AST for String(length == 99) and builds the corresponding jqwik generator StringArbitrary.ofLength(99).
It knows how to resolve type and variable names (unfortunately they are unresolved in the Truffle AST) and knows certain stdlib methods (String.length, Int.isOdd, Number.isBetween, and many more), comparison operators, etc.
It can handle things like Person(name.isAscii, address.street.length <= 10). :-)

Ah, I see! So it would break if the constraint can't be statically analyzed. For example, this would be pretty hard because we have no idea what the result of read("prop:name") is.

properties {
  local name = read("prop:name")
  ["startsWith\(name)"] { str: String(this.startsWith(name)) ->
    str.length >= name.length
  }
}

This API design could work, actually... where the type node describes the property. But, to do this correctly, I think we'd have to add some instrumentation when we initialize that type node. Then after initializing the type node, we should have enough metadata to build the PBT generator.

[translatenix]

In your example, maybe the local property could be evaluated during analysis. But my prototype doesn't go quite as far.

If a constraint can’t be analyzed or isn’t supported, it is ignored during generation. Instead, the constraint is used to discard generated values that violate the constraint. The worst that can happen is that settings.maxDiscardRatio is exceeded, causing the test to fail. This is standard practice in PBT:
https://jqwik.net/docs/current/user-guide.html#filtering
https://jqwik.net/docs/current/user-guide.html#assumptions

[holzensp]

I had just come across jqwik yesterday, as it happens, and put it on my TODO list to explore. The JUnit dependency is, indeed, somewhat hefty. That need not be a problem, if we manage to modularise Pkl more (such that pkl something can either be implemented in Pkl itself, or delegated to some external binary, a la protoc's proto-gen-foo approach).

Wholly agreed with a lot (if not all) of @translatenix's remarks here (hand rolling PBT should not be undertaken lightly, JUnit dependencies are heavy, analyse-time-unknown things translate to discards).

[translatenix]

That need not be a problem, if we manage to modularise Pkl more

A PBT implementation that, like my prototype, analyzes Pkl types/constraints and manipulates the Truffle AST of Pkl tests, needs access to pkl-core internals. Hence it seems problematic for such an implementation to live outside pkl-core.

Regarding PBT generators and shrinkers, the following options feel most promising to me:

1. Wait for jqwik 2 (unknown timeline, could be accelerated by sponsoring the project through GitHub)
2. Investigate the suitability of kotest-property and either port it to Java or call the existing Kotlin library from Java (optional dependency of pkl-core?)

Modifying the jqwik 1 codebase has proven to be impractical.

[holzensp]

A PBT implementation that, like my prototype, analyzes Pkl types/constraints and manipulates the Truffle AST of Pkl tests, needs access to pkl-core internals. Hence it seems problematic for such an implementation to live outside pkl-core.

We're thinking about libraries for better access to syntax (basically expose the AST as Pkl structures, which would allow access to constraints syntactically; name resolution may still be problematic, but thinking about facilitating that as well). It may turn the Truffle AST rewrite into a two-stage (via syntax) rewrite, which would be less than ideal, but sounds feasible to me.

I think I agree with your two options to go forward. (1) seems my preferred option; for (2) the Kotlin dependency has kept me from considering it and I think maintaining a fork of a PBT lib is too much out-of-focus-area effort. The thing that gives me pause is that for how mature the Java ecosystem is, no PBT really survived in it (functional-java / junit-quickcheck / quicktheories all seem to have been abandoned).

[jlink]

(1) seems my preferred option

I'll start work on jqwik 2 as early as this year. If you can specify which parts of jqwik's arbitraries/generators and extensions are most useful for your intended purposes, this would give me a reason to prioritize them.

The thing that gives me pause is that for how mature the Java ecosystem is, no PBT really survived in it (functional-java / junit-quickcheck / quicktheories all seem to have been abandoned).

That's definitely a problem. And the uptake of jqwik is not really huge. 1.5 mio downloads per month is ok, but the growth is linear at best.