Commit Graph

1981 Commits

Author SHA1 Message Date
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
KtorZ
aadf3cfb48 Allow test definition to carry one parameter
The parameter is special as it takes no annotation but a 'via' keyword followed by an expression that should unify to a Fuzzer<a>, where Fuzzer<a> = fn(Seed) -> (Seed, a). The current commit only allow name identifiers for now. Ultimately, this may allow full expressions.
2024-03-03 19:33:24 +01:00
KtorZ
84c4ccaf4c Forbid opaque types in the application binary interface.
We cannot enforce internal invariants on opaque types from only structural checks on Data. Thus, it is forbidden to find an opaque type in an outward-facing interface. Instead, users should rely on intermediate representations and lift them into opaque types using constructors and methods provided by the type (e.g. Dict.from_list, Rational.from_int, Rational.new, ...)
2024-03-03 13:55:10 +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
ff5491caa0 fix(check): only disallow ml_result in data 2024-02-29 11:19:26 -05:00
rvcas
d18caaeecb feat(cli): support mainnet address output
closes #832
2024-02-27 21:55:18 -05:00
rvcas
2018a18d15 fix: error message for bls elements in a type def
closes #840
2024-02-27 21:21: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
rvcas
0ccfe60072 feat: support nested void matching 2024-02-13 21:29:24 -05:00
rvcas
ac0c73a56a chore: clippy fixes 2024-02-13 20:26:12 -05:00
rvcas
3582c5569d fix: no single when clause warning sometimes
While looking at some code, I noticed that this
warning would show up even if an error for a
non-exhaustive when/is shows up for the same when/is
expression. This isn't a useful situation to show this
warning because things are not exhaustive yet so we should
let the user finish and only provide the errors. If things
are exhaustive then the code proceeds and if a warning was set
when there's only one clause pattern then this warning message
can be pushed because that's when it's actually useful.
2024-02-13 20:12:40 -05:00
rvcas
4c5a449d83 chore: improve a comment/doc 2024-02-13 19:46:34 -05:00
microproofs
6e2f9b9eb9 fix tests 2024-02-07 12:48:07 -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
51f1da2505 Removed AirStatements and AirExpressions
Still a WIP
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
713b16e25d we now build forwards when it comes to piplines and expressions
so this test got reordered
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
8702c736d0 fix warning 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
KtorZ
3c8460e6af Allow annotating Data for blueprint
This commit allows Data to be optionally annotated with a
  phantom-type. This doesn't change anything in codegen but we can now
  leverage this information to generate better blueprint schemas.
2024-02-07 11:48:52 -05:00
KtorZ
20ce19dfb1 Fix error hint when expecting 0 generic parameters. 2024-02-07 11:48:52 -05:00
microproofs
0e2995e16e fix test 2024-02-07 11:48:52 -05:00
microproofs
3b4c6cb2aa fix: missing message error term in one place for type is void 2024-02-07 11:48:52 -05:00
microproofs
e25be7643e discards will now check for type too. 2024-02-07 11:48:52 -05:00
microproofs
982eff449e chore: Release 2024-01-31 13:48:20 -05:00
microproofs
551941392e fix: assert had one minor edge case due to final clauses with lists 2024-01-31 00:05:09 -05:00
microproofs
444bccf19c fix: change list_access_to_uplc to properly handle list discards 2024-01-30 23:53:33 -05:00
microproofs
a83220c8d9 fix: module_name was being overrided by the moduleselect field 2024-01-30 23:52:50 -05:00
Kuly14
81e93b4309 Introduce cli aliases for check and build subcommands 2024-01-30 12:32:17 -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
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