Commit Graph

79 Commits

Author SHA1 Message Date
microproofs c382e6fba8 Add a debug flag for uplc eval 2025-02-09 08:39:38 -05:00
Riley-Kilgore df05ae7e5d Uh, formatting again.. 2025-01-22 15:23:17 -08:00
Riley-Kilgore 84a0abeb0f Old Fuzzer, new Sampler 2025-01-22 15:23:17 -08:00
Riley-Kilgore c0fabcd26a Added benchmark keyword and unified Samplers and Fuzzers as Generator 2025-01-22 15:23:17 -08:00
Riley-Kilgore d353e07ea1 Formatting 2025-01-22 15:23:17 -08:00
Riley-Kilgore 699628df62 Added ScaledFuzzer capabilities 2025-01-22 15:23:17 -08:00
microproofs f7f68fbafc
Add writeBits back in and use the optimizer to utilize the list conversion 2025-01-11 19:08:42 +07:00
KtorZ 67bf64967b
rename 'constr_{fields,index}' to 'unconstr_{field,index}'
Better match the conventions so far used across the existing builtins.
2024-12-13 15:18:20 +01:00
microproofs 463b88413e
feat: new builtins constr_index and constr_fields for alternative fast ways to take apart Data 2024-12-13 14:15:19 +07:00
microproofs ebc7d89d5d
Comment out ExpModInteger since it's not live on testnets yet 2024-12-08 14:29:58 +07:00
KtorZ 1105dbf3c6
enable new builtins (*with gotcha)
We still need to adjust the writeBits one to work around its list<int> argument.
2024-12-07 15:43:38 +01:00
KtorZ d3344528b3
add type signatures for new builtins. 2024-12-07 15:43:38 +01:00
KtorZ 1f1e68712c
add type signatures for new builtins. 2024-12-07 14:25:12 +01:00
microproofs 5cf3275793
Detect difference in cost model length to maintain compatability with mainnet and testnet 2024-12-05 11:03:41 +07:00
microproofs befbb6ec18
Start adding implementation for new builtins 2024-12-05 11:03:41 +07:00
KtorZ 4b95db4f88
Fix data-type reification from Void 2024-10-19 10:50:44 +02:00
KtorZ 4fb13af49f
Fix type reification of PRNG. 2024-09-13 18:34:53 +02:00
KtorZ d74e36d0bc
Introduce 'Never' type as a safe alternative to always None options
Unfortunately, as documented in:

  https://github.com/IntersectMBO/cardano-ledger/issues/4571

  Some Option fields in the script context certificates are going to
  remain set to None, at least until the next Hard fork. There's a risk
  that people permanently lock their funds if they expect deposits on
  registration credentials to ever be `Some`.

  So, we introduce a special type that emulate an `Option` that can only
  ever be `None`. We call it `Never` and it is the first type of this
  kind (i.e. with constructors indexes not starting at 0).
2024-08-27 14:40:39 +02:00
KtorZ 7ec3f2e8df
DRY builtins types creation to ensure proper consistency. 2024-08-25 16:20:06 +02:00
rvcas 5b61a75088
feat: handler withdraw purpose 2024-08-25 16:20:06 +02:00
microproofs 953ee6b5d1
Fix ordering for ScriptInfo type 2024-08-25 16:20:05 +02:00
KtorZ 972e9bd763
Define ScriptPurpose & ScriptContext types in prelude, fix codegen new v3 wrapper. 2024-08-25 16:20:04 +02:00
KtorZ beb5ac4643
Add 'diagnostic' to the prelude, as well as companion functions.
This is not fully satisfactory as it pollutes a bit the prelude. Ideally, those functions should only be visible
  and usable by the underlying trace code. But for now, we'll just go with it.
2024-07-19 12:28:07 +02:00
KtorZ b6da42baf2
Bump 'is_validator_param' up from 'ArgName' to '...Arg'
There's no reasons for this to be a property of only ArgName::Named to begin with. And now, with the extra indirection introduced for arg_name, it may leads to subtle issues when patterns args are used in validators.
2024-06-07 11:32:05 +02:00
KtorZ 4d42c6cb19
Introduce 'ArgBy' to allow defining function arg not only by name. 2024-06-07 11:17:16 +02:00
KtorZ 5694d9f9cb
Introduce 'fail once' and alter behavior of 'fail' keyword for properties. 2024-05-30 17:18:50 +02:00
KtorZ 5ce30b2632
Rename AList -> Pairs due to popular demand. 2024-05-23 16:45:40 +02:00
KtorZ ef70c6b8a8 Re-use generic id across builtin type-definitions.
This was somehow wrong and corrected by codegen later on, but we should be re-using the same generic id across an entire definition if the variable refers to the same element.
2024-05-06 15:17:01 -04:00
microproofs a44ed4c1a8 Change prelude Map to AList 2024-05-04 14:04:12 -04:00
KtorZ 1091eba3c3 Review & fix acceptance tests
Temporarily using the 'specialize-dict-key' branch from the stdlib
  which makes use of Pair where relevant. Once this is merged back into
  'main' we should update the acceptance test toml files to keep getting
  them automatically upgraded.

  This commit also fixes an oversight in the reification of data-types
  now properly distinguishing between pairs and 2-tuples.

  Co-authored-by: Microproofs <kasey.white@cardanofoundation.org>
2024-05-04 14:04:12 -04:00
KtorZ 2cb2c7fa1f Add dedicated 'Pair' typed and untyped expression
Before this commit, we would parse 'Pair' as a user-defined
  data-types, and thus piggybacking on that whole record system. While
  perhaps handy for some things, it's also semantically wrong and
  induces a lot more complexity in codegen which now needs to
  systematically distinguish every data-type access between pairs, and
  others.

  So it's better to have it as a separate expression, and handle it
  similar to tuples (since it's fundamentally a 2-tuple with a special
  serialization).
2024-05-04 14:04:12 -04:00
KtorZ 3dd94983bd Revert "fixing more pair issues"
This reverts commit b76cc7436294cd73e7bbaf656c76a8f8b0ad56a9.
2024-05-04 14:04:12 -04:00
microproofs 46c7cb797a fixing more pair issues 2024-05-04 14:04:12 -04:00
KtorZ cbf3ef2854 Add new Prelude alias: 'Map' 2024-05-04 14:04:12 -04:00
microproofs 7b5ad961e2 fix: found issue with record access on Pairs 2024-05-04 14:04:12 -04:00
microproofs fd226be51f add Pair type to prelude 2024-05-04 14:04:12 -04:00
microproofs 61a021f9e3 update pair to handle alias 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
rvcas e71470747f
feat: fix some tests and add a failing one 2024-03-13 20:18:56 -04:00
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
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
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 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 93347d8e7b
Add Fuzzer to the prelude. 2024-03-03 19:33:25 +01:00
KtorZ 5b4fedd084
Add PRNG to the Prelude. 2024-03-03 19:33:25 +01:00
KtorZ 5272f5ecee
Adjust order in which Bool's constructors are declared in the prelude
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.
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
rvcas ff5491caa0
fix(check): only disallow ml_result in data 2024-02-29 11:19:26 -05:00