Commit Graph

623 Commits

Author SHA1 Message Date
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 8d59ba1c77 chore: update the conformance tests 2024-02-20 13:05:28 -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
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 1ab6d050af
chore: bump pallas 2024-01-25 11:07:18 -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 742a728d53 Fix conformance test to make a point 2024-01-13 13:23:58 -05:00
Niels Mündler 316842876d Fix PlutusData Constr test case 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
Niels Mündler b6acdde552 Use to_i64 for clarity 2023-12-19 12:20:10 -05:00
Niels Mündler d06f2f6008 Formatting 2023-12-19 12:20:10 -05:00
Niels Mündler eefd26c6fa Add acceptance tests for this tricky case 2023-12-19 12:20:10 -05:00
Niels Mündler fb56700bde Fix and re-enable pretty print test for bigint 2023-12-19 12:20:10 -05:00
Niels Mündler 89e518f878 Deduplicate code 2023-12-19 12:20:10 -05:00
Niels Mündler ba76c1d2cf Adjust acceptance tests and fix IData and UData 2023-12-19 12:20:10 -05:00
Niels Mündler 022503e254 Fix to_pallas_bigint 2023-12-19 12:20:10 -05:00
Niels Mündler 1b1636ab0e Fix parsing of negative bigint 2023-12-19 12:20:10 -05:00
Niels Mündler 0cfcd78039 Use more clear functions 2023-12-15 21:59:57 -05:00
Niels Mündler 8c619954d3 Add conformance test for big ints 2023-12-15 21:59:57 -05:00
Niels Mündler ceb6d63e95 Add parsing for big builtins 2023-12-15 21:59:57 -05:00
microproofs 6a10be3e82 chore: remove redundant clone 2023-12-15 21:58:02 -05:00
microproofs a0ec92897b chore: clean up pr 2023-12-15 21:58:02 -05:00
microproofs 2cd1379aec for now comment out curry code so the rest of the changes
can be merged to main
2023-12-15 21:58:02 -05:00
microproofs c0c9f2f432 commit latest changes 2023-12-15 21:58:02 -05:00
microproofs 058a190294 feat: implement curried tree pruning 2023-12-15 21:58:02 -05:00
microproofs 51079b8590 fix: builtin_force_reducer wasn't handling double forces correctly 2023-12-15 21:58:02 -05:00
microproofs 4015550f55 start testing the first stage of currying builtins 2023-12-15 21:58:02 -05:00
microproofs 249581e1bc chore: continuing progress on implementing currying optimization for builtins
Introduced some new abstractions to make a different number of args easier to deal with
2023-12-15 21:58:02 -05:00
microproofs 8fdedb754e chore: continue more on curry optimizations 2023-12-15 21:58:02 -05:00
microproofs 88e21449c5 chore: comment fixes 2023-12-15 21:58:02 -05:00
microproofs 5c688b1404 Feat: refactor optimizations to use tree traversal algorithm
This makes each optimization a single function that acts on an existing tree traversal function
2023-12-15 21:58:02 -05:00
Niels Mündler b25e82ed36 Handle errors and format 2023-12-08 12:19:22 -05:00
Niels Mündler 772e73ae48 Fix parsing of hex encoded escaped bytes 2023-12-08 12:19:22 -05:00
Niels Mündler 3ac35f4e00 Make sure that new issue is covered by testcase 2023-12-08 12:19:22 -05:00
Niels Mündler d0bc782f75 Fix pretty prenting of strings in complex data structures 2023-12-08 12:19:22 -05:00
rvcas 2647e4aae6
chore: Release 2023-12-04 22:14:03 -05:00
rvcas 0a1e0d7bee
feat: remove flat-rs crate and use it through pallas_codec 2023-12-04 22:01:51 -05:00
rvcas b17b7f287c
chore: update to pallas v0.20.0 2023-12-04 21:44:19 -05:00
microproofs 1567e42875 chore: fill in machine todos and cost model for case and constr
This allows for several more tests to pass
**Had to remove case-7 since it was incorrectly passing before**
2023-11-17 19:52:03 -05:00
rvcas 0382e5ce12
chore: this comment doesn't make sense 2023-11-17 18:41:28 -05:00
rvcas df992cba67 chore: remove check_type 2023-11-17 13:58:13 -05:00
rvcas 9ab458dcc6 feat: delay typemismatch errors in the machine runtime
to pass 2 of the conformance tests, we need to make sure
that we aren't typechecking builtin arguments as arguments
are applied. This switches push to by removing the call to check_type
and then reworking all the associated unwrap methods on Value
so that they return the same errors that were being returned before.
2023-11-17 13:58:13 -05:00
rvcas ed909055b5 chore: temp remove conformance tests that are failing 2023-11-15 15:55:56 -05:00
rvcas 308fb47e40 fix: don't panic on invalid hex strings 2023-11-15 15:55:56 -05:00
rvcas dfa0378404 chore: explain a todo in the machine 2023-11-15 15:55:56 -05:00
rvcas 3f8f624a7b fix(uplc): more whitespace characters 2023-11-15 15:55:56 -05:00
rvcas 58d98b3325 fix(uplc): parser should accept single quote in var name and comments 2023-11-15 15:55:56 -05:00
rvcas b6f6064aaf test: add all plutus conformance tests 2023-11-15 15:55:56 -05:00
microproofs 8b89ba3b93 feat: implement bls primitives in code gen 2023-11-15 15:55:56 -05:00
microproofs d51374aac1 feat: add conversion to data and from data for new primitive types 2023-11-15 15:55:56 -05:00
rvcas 90aea6476a feat: uplc g1 and g2 literal parsing 2023-11-15 15:55:56 -05:00
rvcas 6ce85e1662 fix: add keccak to TryFrom<u8> 2023-11-15 15:55:56 -05:00
rvcas 49ae8152f8 feat(bls): add new aiken level builtins 2023-11-15 15:55:56 -05:00
rvcas cdcd8172e6 feat(bls): pretty print mlresult type 2023-11-15 15:55:56 -05:00
rvcas 318ae6aad4 feat(bls): finish cost model 2023-11-15 15:55:56 -05:00
rvcas 5243c36ed6 feat(bls): add default costs for the new functions 2023-11-15 15:55:56 -05:00
microproofs 18db1c394a feat: Implemented builtin semantic versioning
feat: impl flat serialization and deserialization for bls constants
feat: started on cost models for the new builtins

Co-authored-by: rvcas <x@rvcas.dev>
2023-11-15 15:55:56 -05:00
rvcas f101581813 feat(bls): pretty printing for g1 and g1 element
Co-authored-by: Kasey White <kwhitemsg@gmail.com>
2023-11-15 15:55:56 -05:00
microproofs 0d2ac952d0 feat: implemented the Bls381-12 builtins and types
also implemented Keccak256 and Blake2b_224

TODO: cost model, flat serialization, pretty

Co-authored-by: rvcas <x@rvcas.dev>
2023-11-15 15:55:56 -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 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
waalge 3e283a59ec Split off builtin function builders
- sort alphabetically
- add some of the missing builtins used for ints
- comment on what is "correct" for future additions
- comment on the current remaining missing builtins
- comment on the current incoherent method names
2023-10-22 17:08:48 -04:00
KtorZ 17832fc5af
Fix clippy warnings: remove redundant closures & guards. 2023-10-21 21:27:31 +02:00
microproofs 596ce49327 fix: mixed up operators for ConstAboveDiagonal and ConstBelowDiagonal
Closes #618
2023-10-13 11:40:07 -04:00
microproofs 8964675670 feat: Add tracing for common multivalidator issues 2023-10-07 19:42:24 -04:00
microproofs 9335522df4 Make change @ktorz suggested 2023-10-07 19:42:24 -04:00
microproofs 98cb01413b chore: prevent strings from being inlined and replicated 2023-10-07 19:42:24 -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 fb2ca0e3e0 inline is actually cheaper in a lot of cases 2023-09-29 17:47:39 -04:00
microproofs a2068ff062 fix: optmizer should never inline recursive functions
chore: some renames
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 5e2a78173b optimization: increase the cases that inline_basic_reduce can handle 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
KtorZ ee4001d2c8
chore: Release 2023-09-20 18:03:46 +02:00
KtorZ 9782c094b7
Fix clippy suggestions. 2023-09-08 16:21:07 +02:00
microproofs 819a0a20e6 add tests for case and constr
Fix a minor issue with decoding order
2023-09-03 11:52:49 -04:00
microproofs c9b01ab365 chore: fill in cost model
test: Add case and constr eval tests
2023-09-03 11:52:49 -04:00
microproofs 85901dc141 chore: update cost model with placeholders for new terms to pass tests 2023-09-03 11:52:49 -04:00
microproofs 40e1d39f8b Add placeholders for cost model 2023-09-03 11:52:49 -04:00
microproofs 33d6d3049e add compute for the new terms constr and case 2023-09-03 11:52:49 -04:00
microproofs e566c4e1de feat(uplc): add Case and Const terms
- parsering
- interning
- flat encoding and decoding
- pretty printing
- debruijn conversion

Co-authored-by: Lucas Rosa <x@rvcas.dev>
2023-09-03 11:52:49 -04:00
rvcas fb967d4c7b
fix: uplc formatter of Data closes #716 2023-08-31 17:20:48 -04:00
waalge cd3a02416f chore: rm unused pub function 2023-08-29 22:30:06 -04:00
waalge 756e16c14b fix: rename assert to expect 2023-08-29 22:30:06 -04:00
rvcas b075d85b40
chore: Release 2023-08-24 15:05:12 -06:00
rvcas a7062ccb88
chore: fix versions 2023-08-24 15:04:19 -06:00
rvcas 747e057d05
fix: tags 2023-08-24 15:00:09 -06:00
KtorZ 2f0211a7b1
Bump all version manually because cargo workspaces didn't work. 2023-08-22 13:27:10 +02:00
microproofs 89c55a23fa chore: Release 2023-08-19 20:17:00 -04:00
KtorZ 051e9a6851 Add some utility functions for displaying Term/PlutusData
This is useful with the blueprint stuff, where Term are often just plain PlutusData.
2023-08-19 13:39:39 -04:00
rvcas 690e41261e
chore: Release 2023-08-16 23:30:21 -04:00
rvcas 2600937447
chore: cargo fmt 2023-08-16 22:56:22 -04:00
logicalmechanism 649039c993 tx simulate still need fee work 2023-08-16 22:37:00 -04:00
logicalmechanism 050c41c8dc tx simulate returns a vector of exbudgets now 2023-08-16 22:37:00 -04:00
microproofs 4a1ae9f412 set eval to public 2023-08-12 16:42:23 -04:00
microproofs ca4a9fcd3d chore: make eval function and SlotConfig public 2023-08-11 20:33:08 -04:00
microproofs 8af253e1df chore: make slot_to_begin_posix_time a public function 2023-08-11 20:05:22 -04:00
Pi Lanningham f464eb3702 Cargo fmt + clippy, with latest rust 2023-08-07 19:00:39 -04:00
microproofs 36c80f36c1 fix tests 2023-08-07 12:02:44 -04:00
microproofs f5c7d222aa optmization fix 2023-08-07 12:02:44 -04:00