We'll piggyback on the tracing capabilities of the VM to provide labelling for prop tests. To ensure we do not interfere with normal traces, we only count traces that starts with a NUL byte as label. That convention is assumed to be known of the companion fuzz library that should then provide the labelling capabilities as a dedicated function.
I've been benchmarking that through the shrink of 'large' lists, and the cache brings about 1.5x speed increase. For small and simple cases, the cache as no visible effects (positive or negative).
Before this commit, we would always show the 'declared form' of type aliases, with their generic, non-instantiated parameters. This now tries to unify the annotation with the underlying inferred type to provide even better alias pretty printing.
Somehow, these have always been right-associative, when the natural thing to expect is left-associativity. It now matters when trying to crawl down binary tree to display them properly.
Using ByteArrays as vectors on-chain is a lot more efficient than relying on actul Data's list of values. From the Rust end, it doesn't change much as we were already manipulating vectors anyway.
Also, this commit makes `apply_term` automatically re-intern the
program since it isn't safe to apply any term onto a UPLC program. In
particular, terms that introduce new let-bindings (via lambdas) will
mess with the already generated DeBruijn indices.
The problem doesn't occur for pure constant terms like Data. So we
still have a safe and fast version 'apply_data' when needed.
This was a mess to say to the least. The mess started when we wanted
to make all definitions in codegen use immutable maps of references --
which was and still is a good idea. Yet, the population of the data
types and functions definitions was done somehow in a separate step,
in a rather ad-hoc manner.
This commit changes that to ensure the project's data_types and
functions are populated while type checking the AST such that we need
not to redo it after.
The code for registering the data type definitions and function
definitions was also duplicated in at least 3 places. It is now a
method of the TypedModule.
Note: this change isn't only just cosmetic, it's also necessary for
the commit that follows which aims at adding tests to the set of
available function definitions, thus allowing to make property tests
callable.
Those end-to-end tests are useful. Both for controlling the behavior of the shrinker, but also to double check the reification of Plutus Data back into untyped expressions.
I had to work-around a few things to get opaque type and private types play nice. Also found a weird bug due to how we apply parameters after unique debruijn indexes have been also applied. A work-around is to re-intern the program.
True corresponds to Constr=1 and False corresponds to Constr=0; their position in the vector shall reflect that. Note that while this would in principle impact codegen for any other type, it doesn't for bool since we likely never looked up this type definition since it is well-known. It does now as the 'reify' function relies on this. Whoopsie.
This is very very rough at the moment. But it does a couple of thing:
1. The 'ArgVia' now contains an Expr/TypedExpr which should unify to a Fuzzer. This is to avoid having to introduce custom logic to handle fuzzer referencing. So this now accepts function call, field access etc.. so long as they unify to the right thing.
2. I've done quite a lot of cleanup in aiken-project mostly around the tests and the naming surrounding them. What we used to call 'Script' is now called 'Test' and is an enum between UnitTest (ex-Script) and PropertyTest. I've moved some boilerplate and relevant function under those module Impl.
3. I've completed the end-to-end pipeline of:
- Compiling the property test
- Compiling the fuzzer
- Generating an initial seed
- Running property tests sequentially, threading the seed through each step.
An interesting finding is that, I had to wrap the prop test in a similar wrapper that we use for validator, to ensure we convert primitive types wrapped in Data back to UPLC terms. This is necessary because the fuzzer return a ProtoPair (and soon an Array) which holds 'Data'.
At the moment, we do nothing with the size, though the size should ideally grow after each iteration (up to a certain cap).
In addition, there are a couple of todo/fixme that I left in the code as reminders of what's left to do beyond the obvious (error and success reporting, testing, etc..)
The parameter is special as it takes no annotation but a 'via' keyword followed by an expression that should unify to a Fuzzer<a>, where Fuzzer<a> = fn(Seed) -> (Seed, a). The current commit only allow name identifiers for now. Ultimately, this may allow full expressions.
We cannot enforce internal invariants on opaque types from only structural checks on Data. Thus, it is forbidden to find an opaque type in an outward-facing interface. Instead, users should rely on intermediate representations and lift them into opaque types using constructors and methods provided by the type (e.g. Dict.from_list, Rational.from_int, Rational.new, ...)
We've been wrongly representing large ints as BigInt, causing them to
behave differently in the VM through builtins like 'serialise_data'.
Indeed, we expect anything that fits in 8 bytes to be encoded as Major
Type 0 or 1. But we were switching to encoding as Major type 6
(tagged, PosBigInt, NegBigInt) for much smaller values! Anything
outside of the range [-2^32, 2^32-1] would be treated as big int
(positive or negative).
Why? Because we checked whether a value i would fit in an i64, and if
it didn't we treated it as big int. But the reality is more subtle...
Fortunately, Rust has i128 and the minicbor library implements TryFrom
which enforces that the value fits in a range of [-2^64, 2^64 - 1], so
we're back on track easily.
While looking at some code, I noticed that this
warning would show up even if an error for a
non-exhaustive when/is shows up for the same when/is
expression. This isn't a useful situation to show this
warning because things are not exhaustive yet so we should
let the user finish and only provide the errors. If things
are exhaustive then the code proceeds and if a warning was set
when there's only one clause pattern then this warning message
can be pushed because that's when it's actually useful.
This commit allows Data to be optionally annotated with a
phantom-type. This doesn't change anything in codegen but we can now
leverage this information to generate better blueprint schemas.
KtorZ