Commit Graph

95 Commits

Author SHA1 Message Date
KtorZ 8e558d893f
Only reify unit tests assertions on failure. 2024-03-07 19:07:55 +01:00
KtorZ bff822ea7f
Rework unit test report to leverage new reification
And also provide slightly better errors when traces, or trace-if-false operators are present.
2024-03-07 01:20:40 +01:00
rvcas c9ab1aec98
chore: consume errs instead of cloning 2024-03-06 18:20:14 -05:00
rvcas f8377af0c8 feat(parse): run in parallel 2024-03-06 18:16:07 -05:00
rvcas 9c5556aa1e feat(deps): remove tests from ast and ignore warnings 2024-03-06 18:16:07 -05:00
KtorZ df3baa082e
Remove 'seed' arg from 'with_project' to FinishedTests event
Also polish a bit the output of tests, move test result to stdout to allow filtering out warnings by redirecting stderr to /dev/null.
2024-03-04 18:43:51 +01:00
KtorZ dd1c7d675f
Allow Aiken files to have more than one dot-separated suffix. 2024-03-04 00:15:05 +01:00
KtorZ 7a2537432a
Accept an optional --seed parameter for check, otherwise default to random.
Also, show the seed on failure.
2024-03-03 20:36:01 +01:00
KtorZ 30841fe000
Rework generate_raw to avoid need to intern in prop tests
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.
2024-03-03 19:33:27 +01:00
KtorZ 1134b8d7d0
Register tests as callable definitions.
Also move the registering of validators into the same place as they
  other and define a little cute function to avoid code-duplication.
2024-03-03 19:33:27 +01:00
KtorZ c2dc47fa0b
Refactor creation of CodeGenerator and management of known data_types and functions.
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.
2024-03-03 19:33:26 +01:00
KtorZ 26e563a9be
Hardened property-based testing framework. More tests, less bugs.
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.
2024-03-03 19:33:26 +01:00
KtorZ 70ea3c9598
Write boilerplate code for being able to easily test properties.
Loads of plumbing, but we now have at least some nice ways to test property execution and shrinking.
2024-03-03 19:33:26 +01:00
KtorZ 2db15d59be
Rename 'aiken-project::script' into 'aiken-project::test_framework' 2024-03-03 19:33:26 +01:00
KtorZ 5b4fedd084
Add PRNG to the Prelude. 2024-03-03 19:33:25 +01:00
KtorZ bfcfc5c41b
Implement reification from Maps. 2024-03-03 19:33:25 +01:00
KtorZ 14f1025f0b
Display counterexamples as Aiken values instead of raw UPLC. 2024-03-03 19:33:24 +01:00
KtorZ c766f44601
Allow Fuzzer with type parameter
Also fix shrinker first reduction, as well as passing of List/Tuples to fuzzer.
2024-03-03 19:33:24 +01:00
KtorZ a703db4d14
Borrow integrated shrinking approach from MiniThesis. 2024-03-03 19:33:24 +01:00
KtorZ 3762473a60
Add preliminary plumbing to run property test through the CLI.
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..)
2024-03-03 19:33:24 +01:00
rvcas d18caaeecb
feat(cli): support mainnet address output
closes #832
2024-02-27 21:55:18 -05:00
rvcas 589bb9a4b3
chore: change how we depend on pallas 2024-01-24 21:26:48 -05:00
KtorZ 8a90e9eda0
Improve behavior and reporting of tests expected to fail
Fixes #786.
2024-01-19 18:20:58 +01:00
microproofs f79b37d551
Replace 'bool' with 'TraceLevel' in codegen
Co-authored-by: KtorZ <matthias.benkort@gmail.com>
2024-01-19 14:30:15 +01:00
KtorZ d27ea98a8f
Rework tracing arguments to --keep-traces & --trace-level
This allows for a more fine-grained control over how the traces are showed. Now users can instrument the compiler to preserve only their user-defined traces, or the only the compiler, or all, or none. We also want to add another trace level on top of that: 'compact' to only show line numbers; which will work for both user-defined and/or compiler-generated traces.
2024-01-19 14:30:15 +01:00
microproofs 86146ae7f4
adding codegen traces 2024-01-19 14:30:14 +01:00
microproofs 71cfb6f6af feat: Add specific messages for using expect with booleans
TODO: fill out the rest of the expects with messages
2024-01-04 16:03:51 -05:00
KtorZ 1ca81ec133
Turn evaluation hints into strings earlier, to make project's Error thread-safe. 2023-11-24 09:44:05 +01:00
Pi Lanningham 5068da3a17
Refactor into cargo-project
Rather than have this logic in the aiken binary, this provides a generic
mechanism to do "something" on file change events.  KtorZ is going to
handle wiring it up to the CLI in the best way for the project.

I tried to write some tests for this, but it's hard to isolate the
watcher logic without wrestling with the borrow checker, or overly
neutering this utility.
2023-11-24 08:37:54 +01:00
rvcas e5801f9c19
feat: support doc comments for functions args and validator params
- Add support to the formatter for these doc comments
- Add a new field to `Arg` `doc: Option<String>`
- Don't attach docs immediately after typechecking a module
  - instead we should do it on demand in docs, build, and lsp
  - the check command doesn't need to have any docs attached
  - doing it more lazily defers the computation until later making
    typechecking feedback a bit faster
- Add support for function arg and validator param docs in
  `attach_module_docs` methods
- Update some snapshots
- Add put_doc to Arg

closes #685
2023-10-16 13:38:23 -04:00
KtorZ 15efeb3069 Remove unused code & data-type 'UseManifest'
If it's unused, it shall be gone. It obfuscate what functions are
  doing and require managing extra complexity for no reason.
2023-09-13 17:17:32 -04:00
rvcas 437a95bfe8
fix: behave like rust with hyphens closes #722 closes #690 2023-08-31 18:00:21 -04:00
KtorZ 961e323c36 Enable iterating over validator's parameters with a callback
This is how we'll construct parameters interactively. We need to lookup the definition, and provide a data representation for it.
2023-08-19 13:39:39 -04:00
Ariady Putra 8cf92ce8ed `aiken new`: Try to get the latest tag of stdlib 2023-08-16 22:30:15 -04:00
rvcas e7c1b28b52
feat: add ability to reference validators in tests closes #632 2023-07-12 18:29:03 -04:00
Pi Lanningham c10f0e53df cargo fmt 2023-07-01 16:17:10 -04:00
Pi Lanningham 4a8cb72708 Add a blueprint policy command
Computes the policy ID of a minting policy; added guards for blueprint address to check that it's not a minting policy; Wasn't 100% sure where the errors should live, so I'm happy to move them if there's objections
2023-07-01 16:17:10 -04:00
microproofs db369da96e feat: Make traces produced by expect dependent on
the value of the tracing flag.
2023-06-23 14:03:23 -04:00
rvcas 8d107b1293
fix(build): --uplc must use Program<Name> to pretty print 2023-06-07 16:25:59 -04:00
rvcas a124a16a61
feat(tests): implement a way to express that tests can fail 2023-05-25 16:54:53 -04:00
microproofs c2ee631d07 feat: new setup for the gen_uplc testing
* new test only module aiken_project::tests
* move TestProject to tests/mod.rs
* new tests go in gen_uplc.rs
2023-04-19 16:08:55 -04:00
rvcas 70f12d3fc5 chore: new branch with some things from the bumpalo branch 2023-04-13 01:28:27 -04:00
KtorZ 4799af3242
Rework 'blueprint apply' command and wrap up wiring up validation.
The apply command now works only from a serialized CBOR data (instead of a UPLC syntax). So it is no longer possible to specify arbitrary cbor terms through the CLI. I believe it to be an acceptable limitation for now; especially given that Aiken will never generate blueprints with non-data terms at the interface boundary.
2023-04-08 08:57:40 +02:00
KtorZ cdc7ebf9a0
Remove now-unnecessary blueprint generics.
These were needed before as a way to _partially deserialize_
  blueprints. Indeed, some commands required accessing information of
  the blueprint, but not necessarily the schema. So out of laziness (or
  cleverness?), we only deserialized validators as serde::Value and
  achieved that through the use of generics.

  Now that validators and schemas have proper deserialisers, we can
  simply deserialize a blueprint.

  TODO: Our serialisation/deserialisation is safe with regards to
  itself; i.e. it roundtrips. However, we only supports a subset of the
  specified blueprint format. For example, we would fail to deserialize
  blueprints that have inline data-schemas (we only use references).
2023-04-08 08:53:51 +02:00
rvcas 3e6f688e2d feat: refactor some methods and modules
* move uplc::ast::builder to uplc::builder
* rename aiken_lang::uplc to aiken_lang::gen_uplc
* move aiken_lang::air and aiken_lang::builder to aiken_lang::gen_uplc
  as submodules

Co-authored-by: Kasey White <kwhitemsg@gmail.com>
2023-03-27 20:00:32 -04:00
rvcas 2dbc50f098
feat: generate_test doesn't need arguments 2023-03-17 18:41:22 -04:00
rvcas c3870e340e
feat(codegen): support multi-validators
* rename force_wrap to force
* add a bunch of builder methods to Term<Name>
* refactor one tiny location to show off builder methods
* split generate into `generate` and `generate_test`
* create wrap_as_multi_validator function

Co-authored-by: Kasey White <kwhitemsg@gmail.com>
2023-03-17 18:40:44 -04:00
KtorZ 451737237e Fix blueprint generation for recursive types.
This was a bit tricky and I ended up breaking things down a lot and
  trying different path. This commit is the result of the most
  satisfying one.

  It introduces a new 'concept' and types: Definitions and Reference.
  These elements are meant to reflect JSON pointers and JSON-schema
  definitions which we now use for pretty much all user-defined
  data-types.

  In fact, Schemas are no longer inlined, but are always referencing
  some schema under "definitions".

  This indirection is necessary in order to cope with recursive types.
  And while it's only truly necessary for recursive types, using it
  consistently makes it both easier to produce and easier to consume.

  ---

  The blueprint generation for recursive types here also works thanks to
  the 'Definitions' data-structure wrapper around a BTreeMap. This uses
  a strategy where:

  (1) schemas are only generated if they haven't been seen before
  (2) schemas are marked as seen BEFORE actually being generated (to
  effectively stop a recursive generation).

  This relies on one important aspect: the key must be uniquely
  identifying a given schema. Which means that we have to monomorphize
  data-types with generic parameters also here, and use keys that are
  specialized in one data-type.

  ---

  In this large overhaul we've also lost one thing which I didn't bother
  re-introducing yet to keep the work manageable: title for record
  fields. Before, we use to pull those from record constructor when
  available, yet now, every record constructor has been replaced by a
  `$ref`. We could theoritically attach a title to the reference. I'll
  try to quickly add that in a later commit.
2023-03-12 12:44:49 -04:00
rvcas 6cde0628a7 fix(check): filter tests before code gen
Co-authored-by: Kasey White <kwhitemsg@gmail.com>
2023-03-08 20:58:27 -05:00
KtorZ ab32302117
Only generate documentation of current package with 'docs'
This was generating documentation for ALL packages including dependencies.
2023-03-08 12:00:59 +01:00