ZenLib 1.0.7

Introduction

Zen is a research library that aims to simplify the process of building verification tools. Zen lets users write a single implementation of a function and then execute, compile, and verify that function.

Getting Started

To import the library, add the following line to your file:

using ZenLib;
using static ZenLib.Language;

The main abstraction Zen provides is through the type Zen<T> which represents a value of type T that can be either concrete or symbolic. As a simple example, consider the following code:

Zen<int> MultiplyAndAdd(Zen<int> x, Zen<int> y)
{
    return 3 * x + y;
}

This is a function that takes two Zen parameters (x and y) that represents an integer values and returns a new Zen value of type integer by multiplying x by 3 and adding y to the result. Zen overloads common C# operators such as &,|,^,<=, <, >, >=, +, -, *, true, false to work over Zen values and supports implicit conversions between literals and Zen values.

The next step is to create a ZenFunction:

var function = Function<int, int, int>(MultiplyAndAdd);

Given a ZenFunction we can leverage the library to perform multiple tasks. The first is to simply evaluate the function on a collection of inputs:

var output = function.Evaluate(3, 2); // output = 11

To perform verification, we can ask Zen to find us the inputs that leads to something being true:

var input = function.Find((x, y, result) => And(x >= 0, x <= 10, result == 11)); // input.Value = (0, 11)

The type of the result in this case will be Option<(int, int)>, which will have a pair of integer inputs that make the expression true if such a pair exists.

Finally, Zen can compile the function to generate IL at runtime that executes without a performance penalty.

function.Compile();
output = function.Evaluate(3, 2); // output = 11

Comparing the performance between the two:

var watch = System.Diagnostics.Stopwatch.StartNew();

for (int i = 0; i < 1000000; i++) function.Evaluate(3, 2);

Console.WriteLine($"interpreted function time: {watch.ElapsedMilliseconds}ms");
watch.Restart();

function.Compile();
Console.WriteLine($"compilation time: {watch.ElapsedMilliseconds}ms");
watch.Restart();

for (int i = 0; i < 1000000; i++) function.Evaluate(3, 2);

Console.WriteLine($"compiled function time: {watch.ElapsedMilliseconds}ms");

interpreted function time: 4601ms
compilation time: 4ms
compiled function time: 2ms

Supported Types

Zen currently supports the following primitive types: bool, byte, short, ushort, int, uint, long, ulong, string. It also supports values of type Tuple<T1, T2>, (T1, T2), Option<T>, IList<T> and IDictionary<T> so long as the inner types are also supported. Zen has some limited support for class and struct types; it will attempt to model all public fields and properties. The class/struct must also have a default constructor.