Commit Graph

263 Commits

Author SHA1 Message Date
microproofs 3c332ca42a Few more places in codegen where we need to be able to deal with Pair records 2024-05-04 14:04:12 -04:00
microproofs 26f68c2fb4 fix: found various unify and type issues while running tests 2024-05-04 14:04:12 -04:00
microproofs a8c8cf41cf Finishing up codegen changes for pair 2024-05-04 14:04:12 -04:00
microproofs 963d275bb8 continue progress on pair adding 2024-05-04 14:04:12 -04:00
microproofs f950ae7d3d WIP: add new opcodes to Air and AirTree and update parts of codegen to handle the new pair type 2024-05-04 14:04:12 -04:00
microproofs d05d8e7de6 Start working on separating pairs from 2 tuples in Aiken
co-authored-by: KtorZ <matthias.benkort@gmail.com>
2024-05-04 14:04:12 -04:00
KtorZ db8eb6a108
Provide more context for some panics
Actually ran into them both, will open issues about those in a bit.
2024-05-01 12:04:47 +02:00
Micah Kendall d25b8f91c7 feat: Emit keyword 2024-04-12 21:40:27 -04:00
KtorZ 435dd0d213
Refactor AssignmentKind to allow backpassing on both let and expect.
The 3rd kind of assignment kind (Bind) is gone and now reflected through a boolean parameter. Note that this parameter is completely erased by the type-checker so that the rest of the pipeline (i.e. code-generation) doesn't have to make any assumption. They simply can't see a backpassing let or expect.
2024-03-11 00:16:23 +01:00
microproofs b761d6a76d fix: function aliases were leading to free uniques 2024-03-09 12:46:12 -05:00
microproofs bffa678178 fix: mutually recursive zero arg functions needed to have their function bodies delayed 2024-03-09 10:04:30 -05:00
microproofs c51741cc35 fix: mutually recursive zero arg function calls were reaching an unreachable 2024-03-08 22:58:03 -05:00
microproofs 541d96f558 remove comment line 2024-03-08 00:12:44 -05:00
microproofs 275db2fd11 update tests 2024-03-08 00:12:44 -05:00
microproofs ae396c0224 Fix opaque type destructuring in code gen 2024-03-08 00:12:44 -05:00
KtorZ 23a22a65cb
Handle (recursive) generic types during reification.
Also moved a bunch of functions from code-gen back into _tipo_, as
  they're better suited and generic enough to be reused elsewhere.
2024-03-07 18:07:52 +01:00
microproofs e217423145 mixed up pair builtin 2024-03-06 23:27:10 -05:00
microproofs bdd84dc952 fixing the tests lead to me create a new function for converting from data 2024-03-06 23:27:10 -05:00
microproofs 27eb1a3e04 Change all uses of interning besides the uplc parser to use the new CodeGenInterner 2024-03-04 11:03:23 -05:00
microproofs d971d9818b update tests and ensure identity reducer handles no_inline lambda 2024-03-04 10:52:56 -05:00
microproofs 06ca22c26a update inliner to handle no_inline functions 2024-03-04 10:52:56 -05:00
microproofs 4e928f39db start adding no inline flag to functions 2024-03-04 10:52:56 -05: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 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 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 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 0ccfe60072
feat: support nested void matching 2024-02-13 21:29:24 -05:00
microproofs 056e3d76ea change check_validator_args to check type after each arg 2024-02-07 12:48:07 -05:00
microproofs 6c6be3f53d got past the errors and warnings 2024-02-07 12:37:37 -05:00
microproofs b807d58e89 fix first compiler pass of errors 2024-02-07 12:37:37 -05:00
microproofs dc195b22d4 missed another hoist over 2024-02-07 12:36:35 -05:00
microproofs d1c784ed49 few more hoist over fixes 2024-02-07 12:36:35 -05:00
microproofs 3938d74bb6 missed a hoist over 2024-02-07 12:36:35 -05:00
microproofs 6b97ab71fe fix up code gen tests 2024-02-07 12:36:35 -05:00
microproofs 4ab3b61200 In most cases the context isn't need so I made the code more explicit about that 2024-02-07 12:36:35 -05:00
microproofs 575dde9885 fix: issue with reordering statements caused clause props to not be updated 2024-02-07 12:36:35 -05:00
microproofs 806a74c192 fix all current errors 2024-02-07 12:36:35 -05:00
microproofs 9f96e4bc5a fix first compiler pass of errors 2024-02-07 12:36:35 -05:00
KtorZ a12c374258 Start turning AirTree statements into expressions (let)
Still many places to fix, WIP.
2024-02-07 12:36:35 -05:00
microproofs e25be7643e discards will now check for type too. 2024-02-07 11:48:52 -05:00
microproofs a83220c8d9 fix: module_name was being overrided by the moduleselect field 2024-01-30 23:52:50 -05:00
microproofs 78d2049d7b fix: Using the wrong match string for discards in FieldsExpose
Also need to return a lambda wrapped term from list_access_to_uplc under all conditions
2024-01-25 14:18:36 -05:00
microproofs 51f1f2b67f change redundant if branches 2024-01-24 16:29:40 -05:00
microproofs eda4e259d6 minor fix and some refactoring on the if statements 2024-01-24 16:29:40 -05:00
microproofs 82fc82ceee fix: used wrong index in tupleAcessor 2024-01-24 16:29:40 -05:00
microproofs 956c3d6cf0 feat: refactor code gen to avoid builtin errors when tracing is turned on 2024-01-24 16:29:40 -05:00
KtorZ 2b4137dc24
Revert "minor refactor"
This reverts commit 21f0b3a6220fdafb8f6aad6855de89d8cdde0e1b.

  Rationale:

  The absence of clause guard was here done *on purpose*. Indeed,
  introducing a clause guard here forces either duplication or the use
  of a wildcard which is not "future proof".

  Should we make a change to that one day (e.g. add a new variant to
  TraceLevel), we won't get any compiler warning and we'll very likely
  forget to update that particular section of the code.

  So as much as possible, enforce complete pattern-match on variants
  make for code that is easier to maintain in the long-run.
2024-01-19 14:31:09 +01:00
microproofs af90b38bf8
minor refactor 2024-01-19 14:31:04 +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
microproofs d26524048e fix: headlist builtin on assoc lists
implement chooseunit for 0 args
2024-01-13 19:29:34 -05:00
microproofs c7af27a6ba fix: generic edge case with tuples that allowed 2 tuples and 3 tuples to use the same monomorphized function.
Also massively reduced the space taken up by generics in scripts when using generics with list and tuples
2024-01-13 17:46:32 -05:00
microproofs 4a8fecb70a fix: satisfy clippy's demands 2024-01-11 14:53:02 -05:00
microproofs 2216f387c3 refactor: change codegen uplc to have more type safety
Also refactor list_access_to_uplc
2024-01-08 18:08:50 -05:00
KtorZ 30a6b77116 Get rid of 'VoidMsg' in favor of an 'Option'. 2024-01-04 16:03:51 -05:00
microproofs c50a9cb5bd refactor: convert msgs to use AirMsg type instead of AirTree 2024-01-04 16:03:51 -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 c7a1ff0959 refactor how tracing is popped off to be in one location in uplc_gen 2024-01-04 16:03:51 -05:00
microproofs 355e38d6e2 feat: expects now print the line of code that failed 2024-01-04 16:03:51 -05:00
microproofs 412945af3a update aiken code gen test 2024-01-04 16:03:51 -05:00
microproofs aa51ce3e3e feat: add code messages when using expects on constrs 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 825e65d7a3 fix: zero arg functions were being compiled without the trace messages
Now traces are added before evaluating
2023-12-06 10:31:48 -05:00
microproofs 45177cd08b fix: add missing type checks for the new bls primitives 2023-11-23 13:00:24 -05:00
microproofs 8b89ba3b93 feat: implement bls primitives in code gen 2023-11-15 15:55:56 -05:00
microproofs 4eebd4628b chore: fix comment 2023-11-06 15:37:04 -05:00
microproofs 7427bac4a0 chore: remove unused code 2023-11-06 15:37:04 -05:00
microproofs 598ec5eaef Use a better algorithm for inlining single occurrences 2023-11-06 15:37:04 -05:00
microproofs 4dd17dacf3 chore: rename uplc builder builtins 2023-10-22 17:08:48 -04:00
microproofs c764a6f99c fix: reset option should not reset special functions in only a multivalidator 2023-10-07 19:42:24 -04:00
microproofs 4649a5a9d2 fix: don't reset the used special functions 2023-10-07 19:42:24 -04:00
microproofs 8964675670 feat: Add tracing for common multivalidator issues 2023-10-07 19:42:24 -04:00
microproofs 7a6ddc45a0 feat: Rework codegen traces to prevent repeated messages from taking up uplc script space 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
microproofs 8a1c824dd7 chore: add specific error for when the validator returns false 2023-10-04 11:08:22 -04:00
microproofs add513790d hotfix: cyclic functions hoisted as a dependency used the wrong key to modify its own cyclic_calls 2023-09-29 22:01:43 -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 1ca3499128 chore: rename type 2023-09-25 21:16:19 -04:00
microproofs 1cab479b81 fix: dependency hoisting for cyclic functions
Add more tests
2023-09-25 21:16:19 -04:00
microproofs 2f80d07132 fix: minor stuff including fixing the var name used in modify_cyclic_calls
and carefully controling the functions we add to sorted dependencies
2023-09-25 21:16:19 -04:00
microproofs f4310bcf33 feat: finished up mutual recursion
Now we "handle" vars that call the cyclic function.
That includes vars in the cyclic function as well as in other functions
"handle" meaning we modify the var to be a call that takes in more arguments.
2023-09-25 21:16:19 -04:00
microproofs ae3053522e feat: Update cyclic functions to be aware of being in a cycle.
Finish the creation of cyclic functions
The last part is to update vars that call into a function in the cycle
2023-09-25 21:16:19 -04:00
microproofs 0b38855ce4 add new enum for hoistablefunctions 2023-09-25 21:16:19 -04:00
microproofs ced818c455 checkpoint commit 2023-09-25 21:16:19 -04:00
microproofs 0fb9837ddf chore: change UserFunction to HoistableFunction to prepare for mututal recursion 2023-09-25 21:16:19 -04:00
microproofs 74b8ab62b2 chore: add comments 2023-09-25 21:16:19 -04:00
microproofs a4aa51ed2d WIP: first part of mutual recursion is done.
This involves creating the function definition and detecting cycles.
The remaining part is to "fix" the call sites
of the mutually recursive functions
2023-09-25 21:16:19 -04:00
rvcas d808197507
chore: clippy fix 2023-09-13 18:17:59 -04:00
microproofs a45001376d fix: is_record was used incorrectly in code gen,
the real solution was to look up the datatype and check constructors length
2023-09-13 00:33:02 -04:00
microproofs d042d55d42 fix clippy warnings in code gen 2023-09-12 21:25:05 -04:00
rvcas 6b70292dfb
chore: cargo fmt 2023-09-06 21:10:50 -04:00
microproofs baa6917af5 Fix: Change type map length assert to check for greater than equals instead of equals to argument length 2023-08-29 21:59:15 -04:00
waalge d4b9f22ac3 rm unnecessary mut 2023-08-26 16:30:44 +00:00
microproofs 084b900b2a change: traverse_with_tree now has a boolean to determine when with is called
fix: Opaque types are now properly handled in code gen (i.e. code gen functions, in datums/redeemers, in from data casts)
chore: add specific nested opaque type tests to code gen
2023-08-19 20:07:37 -04:00