Commit Graph

396 Commits

Author SHA1 Message Date
KtorZ 4d432513e0
Fix interesting case identification for properties expected to fail. 2024-03-04 23:28:45 +01:00
KtorZ fbeb611e5f
Show counter examples in green when property is expected to fail. 2024-03-04 20:41:04 +01: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
microproofs d971d9818b update tests and ensure identity reducer handles no_inline lambda 2024-03-04 10:52:56 -05:00
microproofs 4e0aaf970f update tests and fix final unique issues 2024-03-04 10:52:56 -05:00
KtorZ 8e8e0de044
cargo fmt --all 2024-03-04 14:46:16 +01:00
KtorZ 362acd43a3
Rework and optimize PRNG
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.
2024-03-04 14:27:16 +01:00
KtorZ dd1c7d675f
Allow Aiken files to have more than one dot-separated suffix. 2024-03-04 00:15:05 +01:00
KtorZ 50faf81c0f
Use u64 for PRNG choices. 2024-03-04 00:14:34 +01:00
KtorZ 900b73b21a
cargo fmt --all 2024-03-03 21:05:43 +01:00
KtorZ fbda31d980
Fix and improve test outputs for prop tests. 2024-03-03 21:00:51 +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 a7b9d4bb22
Use u8 for fuzzer choices instead of u32
Value is bounded between 0 and 255.
2024-03-03 19:38:49 +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 3df5bcd96d
Fix shrinker impl and implement 3rd strategy of bin_search reduction. 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
KtorZ aadf3cfb48
Allow test definition to carry one parameter
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.
2024-03-03 19:33:24 +01:00
KtorZ 84c4ccaf4c
Forbid opaque types in the application binary interface.
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, ...)
2024-03-03 13:55:10 +01:00
rvcas d698f76e3c
fix(codegen): builtin calls for g1 and g2 where flipped
closes #840
2024-02-29 12:13:51 -05:00
rvcas d18caaeecb
feat(cli): support mainnet address output
closes #832
2024-02-27 21:55:18 -05:00
rvcas ac0c73a56a
chore: clippy fixes 2024-02-13 20:26:12 -05:00
microproofs 6e2f9b9eb9 fix tests 2024-02-07 12:48:07 -05:00
microproofs 713b16e25d we now build forwards when it comes to piplines and expressions
so this test got reordered
2024-02-07 12:36:35 -05:00
microproofs 6b97ab71fe fix up code gen tests 2024-02-07 12:36:35 -05:00
KtorZ 3c8460e6af Allow annotating Data for blueprint
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.
2024-02-07 11:48:52 -05:00
microproofs 0e2995e16e fix test 2024-02-07 11:48:52 -05:00
microproofs 982eff449e chore: Release 2024-01-31 13:48:20 -05:00
rvcas 3a7a0c1971
chore: remove unused deps 2024-01-30 12:28:18 -05:00
microproofs 8584adc1b7 chore: Release 2024-01-25 15:10:11 -05:00
rvcas defd36ad8c
chore: Release 2024-01-25 11:07:32 -05:00
rvcas 589bb9a4b3
chore: change how we depend on pallas 2024-01-24 21:26:48 -05:00
microproofs ae0b428658 update tests to account for new verbose tracing 2024-01-24 16:29:40 -05:00
microproofs 00e1942999 another test fix 2024-01-24 16:29:40 -05:00
microproofs dc61e11813 fix test 2024-01-24 16:29:40 -05:00
microproofs 3c81ebf137 updating more of the tests 2024-01-24 16:29:40 -05:00
microproofs e523ae63f3 fixed some of the tests 2024-01-24 16:29:40 -05:00
KtorZ 8a90e9eda0
Improve behavior and reporting of tests expected to fail
Fixes #786.
2024-01-19 18:20:58 +01:00
KtorZ 42fdecf41f
Fix coloring output of multi-line traces. 2024-01-19 14:30:44 +01:00
KtorZ 59c784778e
Convert span's start to line number + col
This requires to make line numbers a first-class citizen in the module
  hierarchy but it is fortunately not _too involved_.
2024-01-19 14:30:15 +01:00
KtorZ e67d5863a1
Introduce 'compact' trace level verbosity
For now, it only shows the span start. We'll change that in the next commit to show a line number and a column.
2024-01-19 14:30:15 +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
Matthias Benkort 81e29539c8
Merge pull request #803 from aiken-lang/780-possible-bug-with-test-github-action-version-generated-by-aiken-new
fix: aiken new github action version
2024-01-19 14:27:38 +01:00
KtorZ 0e2b8ae251
Bump pallas dependencies to include flat bigint patch
Fixes #796.
2024-01-18 18:26:21 +01:00
microproofs 1796147264 fix: aiken new github action version 2024-01-18 12:10:06 -05:00
microproofs 06672fce05 add new test 2024-01-13 19:29:34 -05:00
microproofs 4a8fecb70a fix: satisfy clippy's demands 2024-01-11 14:53:02 -05:00
microproofs 394cac86b8 feat: expect on a type now can take in a msg when in trace mode 2024-01-04 16:03:51 -05:00
microproofs 4fc65cc600 feat: change expect from data on constrs to take in a message term 2024-01-04 16:03:51 -05:00
microproofs 43e84d7af7 fixing gen_uplc tets 2024-01-04 16:03:51 -05:00
microproofs 412945af3a update aiken code gen test 2024-01-04 16:03:51 -05: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
rvcas 2647e4aae6
chore: Release 2023-12-04 22:14:03 -05:00
rvcas b17b7f287c
chore: update to pallas v0.20.0 2023-12-04 21:44:19 -05:00
KtorZ 7645a9460f
Display error codes better.
This is a *slight* hack / abuse of the code() method as we are now
  doing a bit of formatting within that function. Yet, we only do so at
  the very top-level (i.e. project's Error) because we can't actually
  fiddle with how miette presents errors.
2023-11-25 15:14:09 +01:00
KtorZ 6c039708c3
Rework 'watch_project' to reuse 'with_project'
Also removed the 'clear' flag to do it by default instead of clogging
  the terminal view.

  This now works pretty nicely, and the logic is back under
  `aiken_project`.
2023-11-25 14:48:22 +01: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 4bb424ba78
Fix a small bug with the filtering 2023-11-24 08:37:54 +01:00
Pi Lanningham 5945a9515b
Disable the doctest, since I don't have an impl of EventListener I can use 2023-11-24 08:37:54 +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 b6f6064aaf test: add all plutus conformance tests 2023-11-15 15:55:56 -05:00
microproofs 446ef11606 chore: finishing acceptance test 29
and updating acceptance test lock files
2023-11-08 14:31:44 -05:00
microproofs d50fb99b75 feat: add acceptance tests 28-30 2023-11-08 14:31:44 -05:00
microproofs 7d319077e6 chore: clean up validator comments and
commit script context test lockfile
2023-11-06 15:49:13 -05:00
microproofs 2f694b01cb chore: use insta snapshot for blueprint validator tests 2023-11-06 15:37:04 -05:00
microproofs 49bd4ba33d chore: Release 2023-10-25 19:00:03 -04:00
microproofs 4dd17dacf3 chore: rename uplc builder builtins 2023-10-22 17:08:48 -04:00
KtorZ c4221730bf
Define 'ExtraData' trait for errors
This should allow passing some extra information to LSP diagnostic in order to provide quickfix actions, such as auto-imports.
2023-10-20 18:00:12 +02: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
microproofs a86f08c6d1 update tests for new trace reduction 2023-10-07 19:42:24 -04:00
microproofs 44021cde19 Detect when fields_expose is unnecessary in clause_pattern 2023-10-07 19:42:24 -04:00
KtorZ c2bf6e5682
Add missing keywords to documentation generator. 2023-10-06 14:46:34 +02:00
KtorZ a524836c94
Add compiler version & system information to panic error message
So that we stop constantly asking people about it.
2023-10-06 14:46:11 +02:00
KtorZ 524d0dadf5
Add compiler's version to blueprint. 2023-10-06 14:17:55 +02:00
KtorZ d56d5180cf
Move compile-time build info to aiken-project
So that we can use it as part of the blueprints.
2023-10-06 14:08:47 +02:00
microproofs 8a1c824dd7 chore: add specific error for when the validator returns false 2023-10-04 11:08:22 -04:00
microproofs fb6cbbec8b chore: Release 2023-09-29 22:08:09 -04:00
microproofs 82ceb5b696 chore: Release 2023-09-29 19:39:28 -04:00
microproofs 83f0dd2cbe chore: fix blueprint validator tests 2023-09-29 17:47:39 -04:00
microproofs 335560b81f Add placeholders for new terms in optimize
Update tests to check optimization is applied properly
2023-09-29 17:47:39 -04:00
microproofs 47596f0324 feat: Remove tuple_index and record_access in favor of faster more direct functions for
accessing an item in a tuple or a field in a record
2023-09-28 01:05:05 -04:00
microproofs 1bcc9e8524 fix: expect on tuples from data now checks for no more items after the last 2023-09-26 12:49:50 -04:00
microproofs 5b018b7c07 test: add a test around a tuple of constructors when with many conditions 2023-09-20 16:20:42 -04:00
KtorZ ee4001d2c8
chore: Release 2023-09-20 18:03:46 +02:00
rvcas 7b915b7dcf
chore: allow clippy::arc_with_non_send_sync in tests 2023-09-13 19:07:45 -04:00
rvcas d808197507
chore: clippy fix 2023-09-13 18:17:59 -04:00
KtorZ c711a97e69 Throttle calls to package registry for version resolution
The 'HEAD' call that is done to resolve package revisions from
  unpinned versions is already quite cheap, but it would still be better
  to avoid overloading Github with such calls; especially for users of a
  language-server that would compile on-the-fly very often. Upstream
  packages don't change often so there's no need to constantly check the
  etag.

  So we now keep a local version of etags that we fetched, as well as a
  timestamp from the last time we fetched them so that we only re-fetch
  them if more than an hour has elapsed. This should be fairly resilient
  while still massively improving the UX for people showing up after a
  day and trying to use latest 'main' features.

  This means that we now effectively have two caching levels:

  - In the manifest, we store previously fetched etags.
  - In the filesystem, we have a cache of already downloaded zip archives.

  The first cache is basically invalidated every hour, while the second
  cache is only invalidated when a etag changes. For pinned versions,
  nothing is invalidated as they are considered immutable.
2023-09-13 17:17:32 -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
KtorZ 76ff09ba0e Ensure that version resolution works offline
And so, even for unpinned package. In this case, we can't do a HEAD request. So we fallback by looking at what's available in the cache and using the most recently downloaded version from the cache. This is only a best effort as the most recently downloaded one may not be the actual latest. But common, this is a case where (a) someone didn't pin any version, (b) is trying to build on in an offline setup. We could possibly make that edge-case better but, let's see if anyone ever complains about it first.
2023-09-13 17:17:32 -04:00