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
microproofs
960a15c4ec
checkpoint - fixing tests and stuff
2023-08-07 12:02:44 -04:00
microproofs
6eeb282dee
Now code gen is finished and we just have testing
2023-08-07 12:02:44 -04:00
rvcas
be7a441205
fix(uplc): pair type formatting closes #680
2023-07-19 13:49:05 -04:00
rvcas
97acd6d7bd
chore: Release
2023-07-15 21:37:10 -04:00
rvcas
621017bd93
chore: Release
2023-07-14 10:55:13 -04:00
Pi Lanningham
723c347a1a
Clippy
...
Clippy has a build failure locally, for some reason, so I have to use CICD to find these
2023-07-09 23:16:01 -04:00
Pi Lanningham
189150612c
cargo fmt :|
2023-07-09 23:16:01 -04:00
Pi Lanningham
26a4c57805
Clippy cleanup
2023-07-09 23:16:01 -04:00
Pi Lanningham
c4690c6e00
Data parsing, tests
2023-07-09 23:16:01 -04:00
Pi Lanningham
6d9a95ef2d
Add all but data parsing
...
Updates the parsing to the standard, *except* for Data, since that'll be more involved
2023-07-09 23:16:01 -04:00
Pi Lanningham
a48c45b737
Formatting
2023-07-09 23:16:01 -04:00
Pi Lanningham
ecff82659d
Tweak pretty-printing
...
This pretty printing now (mostly) matches https://github.com/input-output-hk/plutus/issues/4751#issuecomment-1538377273 ; the only concern is whether the PlutusData stuff should be upstreamed to pallas, and whether pallas has a way to print BigInts easier
2023-07-09 23:16:01 -04:00
KtorZ
2a747305f7
Fixes evaluation of large positive bigint in the UPLC machine
...
Fixes #511 .
2023-07-05 18:52:14 +02:00
rvcas
8a7df7f66b
test: add empty list test
2023-07-04 17:19:29 -04:00
microproofs
42544af799
fix: safe encode bits to check for 2^num_bits <= byte we are encoding
...
fix: I thought namedDeBruijn takes advantage of Binder for encoding and decoding.
It does not...
fix: Debruijn was being converted to NamedDeBruijn incorrectly
2023-06-30 23:06:38 -04:00
rvcas
90ff211205
chore: Release
2023-06-23 19:41:14 -04:00
microproofs
93135cebbb
fix: redeemers in the script context are sorted by redeemer ptr not data hash
2023-06-16 12:24:44 -04:00
rvcas
85d82e5aec
chore: Release
2023-06-13 21:24:41 -04:00
microproofs
379c2fe2bf
chore: Release
2023-06-13 20:32:22 -04:00
microproofs
a5245fdc6b
chore: couple more identity tests in optimize step
2023-06-10 00:01:54 -04:00