Zlowcheck

A property-based model-testing library, coupled with a finite-entropy number generator.

A nice setup for automated bug detection with: test case serialization, shrinking of sequences to their smallest failing version, and replayable paths for model tests.

• Disclaimer
• Devlog entries
• Finite PRNG
• Property-based tests
• Why is it valuable?
• TODO
• Acknowledgements
• Warnings

Disclaimer

Pre-alpha software. There will be dragons. Consider this a proof of concept.

Devlog entries

• Devlog 1: How the PRNG works
• Devlog 2: How the model tester works

Finite PRNG:

A finite-entropy number generator: you input some bytes into it, you pass it to the property-based tests, and it churns out data until it runs out of bytes to consume. The length of the byte sequence determines for how long it can go - and incidentally describes how complex your program is. It will error upon running out with OutOfEntropy.

const FinitePrng = @import("finite_prng");
// Create a fixed byte array as the entropy source
const bytes = [_]u8{ 0x12, 0x34, 0x56, 0x78, 0x9A, 0xBC, 0xDE, 0xF0 };
// Initialize the PRNG with the byte array
var prng = FinitePrng.init(&bytes);
// Get a random generator from the PRNG
var random = prng.random();

// Generate random values of different types
const int_value = try random.int(i32);
const float_value = try random.float(f64);
const bool_value = try random.boolean();

// Generate values within ranges
const range_value = try random.intRangeLessThan(i32, -10, 10);

// Use probability ratios
const happens = try random.chance(.{ .numerator = 1, .denominator = 4 }); // 25% chance

Property-based tests:

Based on the wonderful fast-check library, this a minimal function composition api which allows you to do something akin to:

const zlowcheck = @import("zlowcheck");
const sortedProperty = zlowcheck.property( // Define a property
    []i32,
    zlowcheck.gen([]i32, .{ // create a generator
        .min_len = 0,
        .max_len = 100,
        .child_config = .{ .min = -1000, .max = 1000 },
    }),
    struct {
        fn test_(arr: []i32) bool {
            // Sort the array
            std.sort.insertion(i32, arr, {}, std.sort.asc(i32));

            // Check that it's sorted
            for (arr, 0..) |val, i| {
                if (i > 0 and val < arr[i - 1]) return false;
            }
            return true;
        }
    }.test_,
);

// Run the property test
const result = try zlowcheck.assert(sortedProperty, .{ .runs = 100, .verbose = true }, std.testing.allocator);

// If the property fails, result will contain the counterexample.
// Succeeding properties return null
try std.testing.expectEqual(null, result);

Why is it valuable?

Picture this pseudo-code:

const finite_prng = prng.bytes("hello, I am a byte sequence");
const result = try assert(property(generator(T, &finite_prng.random()), &predicate_fn), .{runs: 1000})
std.debug.print("{s}", .{ result.?.failing_bytes });
// prints: "Hello, I am a"
std.debug.print("{d}", .{ result.?.counterample.* });
// …prints the data which caused your test to fail…

What just happened? You ran a program with a byte sequence, it generated some data, the data triggered a failure, and the tests told you which of those bytes triggered it. To be more specific: the tests told you which of the bytes were used to generate the data which triggered the failure.

What can you do with this ?

• Well, for one: reproduce the failure! The number generator is deterministic, so the bytes will again trigger the failure when you re-run them. (digression: «pseudo-random number generators» is a misnomer. They should be called «deterministic and repetitive number generators», but that doesn't sound as scientific I guess).

• For seconds: store the bytes in a text file, and now you have a regression test - also reproducible, por supuesto.

• For thirds: Now that the bytes are in a text file, feed them to a fuzzer's base library, and plug the fuzzer into the number generator. The fuzzer can now search for bugs through the prng.

So at this point, the finite-prng acts as a de-serializer for test cases generated by your fuzzer. The sequence goes:

regressions lib => fuzzer => finite-prng => data generator => property check => on failure, shrink => gather failing bytes => report

Full disclaimer: I haven’t tried that - yet…

TODO

Some things I’d like to add:

• Documentation… 🧐

• Model-Based Testing

  • Similar to fast-check's ModelRunner
  • Allow testing against a simplified model of a system

• Stateful Testing

  • Commands that modify state
  • Ability to generate and shrink sequences of commands
  • State machine testing

• Fuzzing Integration

  • Integration with fuzzers for more thorough testing
  • Ability to use generated test cases as fuzzing inputs

Aknowledgements

• zigthesis thanks to which I discovered what PBT was.
• tigerbeetle’s prng module from which I lifted the best ideas in this lib.
• Matklad's properly testing concurrent data structures which spun this adventure
• fast-check, which gets a 5 star in my book

Warnings

• The tests could be more concise.
• The library code feels sluggishly verbose.
• The implementation of the generator's contexts for shrinking leaves to be desired.
• The shrink algos I used are based on my best effort at understanding fast-check's implementation and the recommendations of an AI gremlin.
• The library must allocate in order to shrink, because it needs to place failures' contexts on the heap for later retrieval.