Commit Graph

435 Commits

Author SHA1 Message Date
rvcas fe6710935d feat: impl serde on errythang 2024-03-08 19:19:07 -05:00
microproofs 94f383762c step up the optimizations a bit more by inlining a small function 2024-03-08 00:12:44 -05:00
microproofs 1edd1a1fa3 change currying to happen with 3 or more occurrences 2024-03-08 00:12:44 -05:00
microproofs e9122de061 more identity reduce testing 2024-03-08 00:12:44 -05:00
microproofs dabaae8ca6 more identity and inline tests 2024-03-08 00:12:44 -05:00
microproofs 97b0cf6813 reorganize shrinker tests 2024-03-08 00:12:44 -05:00
microproofs eb709d6fc3 reorder tests to match order of functions 2024-03-08 00:12:44 -05: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
microproofs 2bc433f61e fix: need to use temp_term for counting var occurrences in identity reducer
chore: Adding more shrinker tests and fixed some of the existing ones
2024-03-05 12:08:18 -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 af6c107187 remove unneeded assert 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
microproofs 2aaa46e54c remove print 2024-03-04 10:52:56 -05:00
microproofs c6ef37cc5c checkpoint 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
microproofs 62963f7fc2 feat: finish curry optmization, improve inline optimization further, and add a subtract integer to add integer conversion 2024-03-04 10:52:56 -05:00
microproofs 7d8fdc0f22 prevent curried function hoisting if occurrences is 0 2024-03-04 10:52:56 -05:00
microproofs 258b5abf23 now currying works 2024-03-04 10:52:56 -05:00
microproofs 3b55a32583 finish up curry optimization on builtins 2024-03-04 10:52:56 -05:00
microproofs 58d586c5cf large refactor to reduce complexity 2024-03-04 10:52:56 -05:00
microproofs 8f84eb382f commit some changes so far 2024-03-04 10:52:56 -05:00
microproofs 9a52258e14 chugging along with a small refactor and some more work toward currying 2024-03-04 10:52:56 -05:00
microproofs 2f72510102 chore: Add back curry code removed in a previous commit 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 14f1025f0b
Display counterexamples as Aiken values instead of raw UPLC. 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 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
KtorZ 46c357df7b Fix Int/BigInt pivot
We've been wrongly representing large ints as BigInt, causing them to
  behave differently in the VM through builtins like 'serialise_data'.

  Indeed, we expect anything that fits in 8 bytes to be encoded as Major
  Type 0 or 1. But we were switching to encoding as Major type 6
  (tagged, PosBigInt, NegBigInt) for much smaller values! Anything
  outside of the range [-2^32, 2^32-1] would be treated as big int
  (positive or negative).

  Why? Because we checked whether a value i would fit in an i64, and if
  it didn't we treated it as big int. But the reality is more subtle...
  Fortunately, Rust has i128 and the minicbor library implements TryFrom
  which enforces that the value fits in a range of [-2^64, 2^64 - 1], so
  we're back on track easily.
2024-02-25 14:09:56 -05:00
rvcas a15fead982 chore: remove unused import 2024-02-20 13:05:28 -05:00
rvcas 20917bbd5b feat(machine): fix Value::Constr fields order
cc @MicroProofs
2024-02-20 13:05:28 -05:00
rvcas 028528899c feat(runtime): implement byteStringToInteger and add conformance tests 2024-02-20 13:05:28 -05:00
rvcas da6e5ec6d1 feat: implement integerToByteString
Co-authored-by: Kasey White <kwhitemsg@gmail.com>
2024-02-20 13:05:28 -05:00
rvcas c7dd4d0e48 feat(aiken-lang): expose integerToByteString and byteStringToInteger 2024-02-20 13:05:28 -05:00
rvcas fc3bc4d9ff feat(cost_model): add costing for integerToByteString and byteStringToInteger 2024-02-20 13:05:28 -05:00
rvcas 70d4d7fdeb feat(runtime): add force count and arity for integerToByteString and byteStringToInteger 2024-02-20 13:05:28 -05:00
rvcas b0eade209b feat(DefaultFunction): add IntegerToByteString and ByteString 2024-02-20 13:05:28 -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
KtorZ 0e2b8ae251
Bump pallas dependencies to include flat bigint patch
Fixes #796.
2024-01-18 18:26:21 +01:00
Niels Mündler f934e87b1d Reuse "convert_tag_to_constr" 2024-01-13 13:23:58 -05:00
Niels Mündler cda1716d47 Unify construction of PlutusData objects from int + fields 2024-01-13 13:23:58 -05:00
Niels Mündler 4bd8ab890a Add reverse mapping for PlutusData constr 2024-01-13 13:23:58 -05:00
Niels Mündler 0ae631a1fe Fix parsing Constr PlutusData 2024-01-13 13:23:58 -05:00
microproofs 4a8fecb70a fix: satisfy clippy's demands 2024-01-11 14:53:02 -05:00
Mitchell Turner 7992a50bec
Make foreign `Language` type publicly available (#793)
* Make foreign type public available

* Fix formatting
2024-01-08 13:31:21 -08: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