Commit Graph

183 Commits

Author SHA1 Message Date
rvcas 7af4ef53ab
feat: block expects on opaque types 2024-03-13 20:17:54 -04:00
KtorZ a578728a94
Resolve type aliases based on inferred types.
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.
2024-03-08 16:01:21 +01:00
KtorZ ed9f5c6ef7
Preserve TypeAlias in types for better context/feedback. 2024-03-08 15:59:33 +01:00
microproofs eb07365e73 fix tests 2024-03-08 00:12:44 -05:00
microproofs 275db2fd11 update tests 2024-03-08 00:12:44 -05:00
microproofs a3fbe6c155 fix tests 2024-03-06 23:27:10 -05: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 900b73b21a
cargo fmt --all 2024-03-03 21:05:43 +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 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 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 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
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
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 f79b37d551
Replace 'bool' with 'TraceLevel' in codegen
Co-authored-by: KtorZ <matthias.benkort@gmail.com>
2024-01-19 14:30:15 +01:00
KtorZ 0e2b8ae251
Bump pallas dependencies to include flat bigint patch
Fixes #796.
2024-01-18 18:26:21 +01: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 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
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 a86f08c6d1 update tests for new trace reduction 2023-10-07 19:42:24 -04:00
KtorZ 524d0dadf5
Add compiler's version to blueprint. 2023-10-06 14:17:55 +02:00
microproofs 8a1c824dd7 chore: add specific error for when the validator returns false 2023-10-04 11:08:22 -04:00
microproofs 83f0dd2cbe chore: fix blueprint validator tests 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
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 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
microproofs 90c7753201 update tests for new recursion optmization 2023-08-07 19:00:39 -04:00
microproofs 36c80f36c1 fix tests 2023-08-07 12:02:44 -04:00
rvcas 8a7df7f66b
test: add empty list test 2023-07-04 17:19:29 -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 cf6d04e95b
chore: some clippy warnings 2023-06-02 19:47:52 -04:00
rvcas 9c29f4f26b
fix: blueprints gen failing on List
closes #569

* added new methods to Definitions
  it doesn't use expect
* lookup was failing for the special map/pair case
  when resolving list generics

Co-authored-by: Pi <pi@sundaeswap.finance>
2023-06-02 17:53:10 -04:00
microproofs deee50b77e fix: just change `as_key`
Co-authored-by: Lucas Rosa <x@rvcas.dev>
2023-05-31 00:27:31 -04:00
microproofs a6807f0bfb fix: seems like definition lookups weren't working
Co-authored-by: Lucas Rosa <x@rvcas.dev>
2023-05-31 00:18:05 -04:00
microproofs b36cf1c029 chore: refactor default functions in uplc_code_gen.
feat: Add an identity optimization to remove functions that return the argument only.
2023-05-08 16:15:09 -04:00
microproofs 0d0c96deda commit validator changes and tests 2023-04-28 17:05:46 -04:00
microproofs b050018a37 test fix: blueprint change 2023-04-25 02:06:56 -04:00
microproofs 9bb1a88f23 fix: expect [] on a non-empty list now fails. 2023-04-21 17:39:21 -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
microproofs 23a7e7e680 chore: convert acceptance test 5
Also constructors with no fields are now converted to a constant data term.
2023-04-19 16:08:55 -04:00
microproofs 022d557906 chore: convert acceptance test 4 2023-04-19 16:08:55 -04:00
microproofs 7da3ac2c99 chore: convert acceptance test 3 2023-04-19 16:08:55 -04:00
microproofs 7dd13f8d73 feat: add end to end tests to replace acceptance tests with strict uplc comparison.
Add acceptance tests 1,2, 6 as end to end tests
2023-04-19 16:08:55 -04:00
Kasey White 02d57cc076 tests pass now after adding in final wrapper as air elements 2023-04-09 17:43:56 -04:00
Kasey White 9e95e24624 now tests are passing 2023-04-09 17:43:56 -04:00
Kasey White 4d97719e6d update blueprint tests with new hashes and script outputs 2023-04-09 17:43:56 -04:00
Kasey White abd97f0ade changed assert_on_list from being defined at uplc level to being defined at air level to enable proper hoisting 2023-04-09 17:43:56 -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 bf222a3ea2
Fix reference JSON deserialization. 2023-04-08 08:57:40 +02:00
KtorZ c18deecdc8
Show slightly better schema mismatch errors
Display terms as CBOR diagnostic when they are Plutus data.
2023-04-08 08:57:38 +02:00
KtorZ 176cb45524
Factor out error (schema mismatch) creation during blueprint validation. 2023-04-08 08:57:04 +02:00
KtorZ 7d6612b108
Rework parameter validation to work from 'Constant' instead of 'Term'
This simplifies the code and makes it more efficient as we no longer need to wrap and unwrap constant terms constantly.
2023-04-08 08:57:03 +02:00
KtorZ d58ef1a079
Implement blueprint schema & data validations. 2023-04-08 08:57:03 +02:00
KtorZ ee220881b6
Generalize schema definition to work from inline schema or reference. 2023-04-08 08:57:03 +02:00
KtorZ d620f6367c
Bootstrap schema validation for simple constants. 2023-04-08 08:57:03 +02:00
KtorZ f311e048b7
Improve error message on 'ParameterizedValidator'. 2023-04-08 08:57:01 +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
KtorZ f0d2d20a4c
Impl JSON deserialization for blueprint's 'Schema'. 2023-04-08 08:53:51 +02:00
KtorZ 565c0bea74
Write JSON deserializers for Reference, Constructors, Items and Data.
This is needed in order to deserialize a JSON blueprint and use it to perform validation.
  Still TODO:

  - [ ] Write JSON deserializer for 'Schema'

  Which should now be relatively straightforward.
2023-04-08 08:53:49 +02:00
rvcas 1444c9328d
fix some typos 2023-04-07 16:51:18 -04: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
KtorZ bc690c5410
Generated wrapped schemas for multi-validators' redeemers 2023-03-17 18:40:49 -04:00
Kasey White bb6fc76971
start on registering redeemer wrapper type in definitions 2023-03-17 18:40:49 -04:00
KtorZ 7e1403a3b2
Complete generation of blueprint multi-validators. 2023-03-17 18:40:49 -04:00
Kasey White fe92b27d50
start on refactoring validator to support multi-validators in blueprint 2023-03-17 18:40:49 -04:00
KtorZ 61113cd7b9
distinguish between multi vs single validator case in blueprint schema generation. 2023-03-17 18:40:48 -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
rvcas ed92869fb9
feat(validator): parsing and typechecking for double validators 2023-03-17 18:38:24 -04:00
KtorZ ae981403c6 Re-introduce field title & description in referenced schemas. 2023-03-12 12:44:49 -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
KtorZ f67e049dc2 Introduce indirection for fields. 2023-03-12 12:44:49 -04:00
KtorZ 3a7aac0a33 Make blueprint code slightly more resilient to changes.
Leverage traits instead of hard-coded type parameters.
2023-03-12 12:44:49 -04:00
KtorZ e44f18bae5 Add failing test scenario for recursive types. 2023-03-12 12:44:49 -04:00
KtorZ a66c9bd2c3
Remove redundant match on tuple blueprint generation. 2023-03-08 16:40:03 +01:00
rvcas e2dc4ec6c8 feat: implement convert command 2023-03-03 20:57:20 -05:00
KtorZ 6d098a4571 Fix blueprint generation for nested fields with Data
Having the data's schema be optional at the level of the 'Schema' did not allow to represent cases where there would be an opaque data at an arbitrary nesting. So I introduced a new variant 'Opaque' on 'Data' to fill that gap.
2023-03-02 15:25:17 -05:00
rvcas a40f88b918 fix: test never used Foo 2023-03-02 15:25:17 -05:00
KtorZ 65c336cb82
Update blueprint outputs to reflect latest specification.
Schemas of datums, redeemers and parameters are now nested under a field 'schema'. This allows to define a field 'purpose' at the same level.
2023-03-02 17:17:27 +01:00
KtorZ 70cdf3cb26
Add 'exported_data' test and revert 413a056 2023-03-02 16:09:08 +01:00
Kasey White 413a056c08 fix: Data was not allowed in an interface
Co-authored-by: rvcas <x@rvcas.dev>
2023-03-01 21:34:36 -05:00
KtorZ a46a9fca41
Only use colors & text decorations on ANSI-capable terminals.
Fixes #404.
2023-02-26 13:19:03 +01:00
KtorZ 0838d48f7c
Move module name validation outside of type-checking
And disable it for documentation generation. This way, we can generate documentation for aiken/builtins and aiken (prelude)
2023-02-22 11:51:32 +01:00
KtorZ c0230a811f
Add 'plutusVersion' to blueprints. 2023-02-21 15:37:35 +01:00
KtorZ 82a32a082b
Remove 'purpose' from blueprint's schema.
This has been removed from the CIP-0057 specification since validators
  are often re-used for multiple purposes (especially validators with
  arity 2). It's misleading to assign a validator a purpose since the
  purpose distinction actually happens _within_ the validator itself.
2023-02-21 15:30:41 +01:00
KtorZ db0dfbbec1
Fix blueprint schema for tuples. 2023-02-21 15:29:33 +01:00
rvcas 815d7d80c6 feat(lsp): hover and goto definition 2023-02-20 15:30:25 -05:00
KtorZ e9e3f4f50a Implement TraceIfFalse type-checking and AST transformation.
This caused me some trouble. In my first approach, I ended up having
  multiple traces because nested values would be evaluated twice; once
  as condition, and once as part of the continuation.

  To prevent this, we can simply evaluate the condition once, and return
  plain True / False boolean as outcome. So this effectively transforms any
  expression:

  ```
  expr
  ```

  as

  ```
  if expr { True } else { trace("...", False) }
  ```
2023-02-16 20:29:41 -05:00
KtorZ 3204322da6
Fix validator lookup by title.
We want the lookup to yield a result when there's only a single
  validator; and no title is provided. So that users can simply do
  'aiken address' in their project if it's unambiguous. The validator's
  name is only required to disambiguate between multiple validators.

  I also noticed that the order of arguments in with_validator was
  wrong. Somehow.
2023-02-16 10:28:27 +01:00
rvcas a311531508 fix(cli): aiken address 2023-02-16 00:05:55 -05:00
rvcas 2e78b7100c fix: blueprint tests 2023-02-16 00:05:55 -05:00
rvcas 673b57b81c feat: get bluprint stuff compiling again 2023-02-16 00:05:55 -05:00