Add PlutusV3 conformance tests and also control budgets

There were some odd discrepancy for `integerToByteString` on the mem
  side. Either 1 or about 1000 mem units off; which I couldn't quite
  figure out. Yet, it proves useful to validate builtin at large and
  ensure we have a valid cost model for v3.
This commit is contained in:
KtorZ
2024-08-14 02:42:04 +02:00
parent f879f6d183
commit 2cb87f4f8f
2893 changed files with 6385 additions and 13 deletions

View File

@@ -0,0 +1,4 @@
-- Missing the 0x prefix.
(program 0.0.0
(con bls12_381_G1_element c00000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000)
)

View File

@@ -0,0 +1,4 @@
-- This has # instead of 0x.
(program 0.0.0
(con bls12_381_G1_element #c00000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000)
)

View File

@@ -0,0 +1,4 @@
-- A bad encoding: this has the negative bit set, but nothing else.
(program 0.0.0
(con bls12_381_G1_element 0x400000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000)
)

View File

@@ -0,0 +1,4 @@
-- Almost a correct representation of the zero point, but with the negation bit set.
(program 0.0.0
(con bls12_381_G1_element 0xe00000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000)
)

View File

@@ -0,0 +1,4 @@
-- The zero point, but with a random bit set in the body (should all be 0)
(program 0.0.0
(con bls12_381_G1_element 0xc00000000000000000000000000000000000000000000010000000000000000000000000000000000000000000000000)
)

View File

@@ -0,0 +1,4 @@
-- This encodes a field element which isn't the x-coordinate of any point on the curve (no square root).
(program 0.0.0
(con bls12_381_G1_element 0xa00000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000003)
)

View File

@@ -0,0 +1,4 @@
-- This is a valid encoding with the sign bit clear.
(program 0.0.0
(con bls12_381_G1_element 0x81e9a0c68985059bd25a5ef05b351ca22f7d7c19e37928583ae12a1f4939440ff754cfd85b23df4a54f66c7089db6deb)
)

View File

@@ -0,0 +1,7 @@
(program
0.0.0
(con
bls12_381_G1_element
0x81e9a0c68985059bd25a5ef05b351ca22f7d7c19e37928583ae12a1f4939440ff754cfd85b23df4a54f66c7089db6deb
)
)

View File

@@ -0,0 +1,4 @@
-- This is a valid encoding with the sign bit set (obtained by hashing 0x0102030405 to G1)
(program 0.0.0
(con bls12_381_G1_element 0xa1e9a0c68985059bd25a5ef05b351ca22f7d7c19e37928583ae12a1f4939440ff754cfd85b23df4a54f66c7089db6deb)
)

View File

@@ -0,0 +1,7 @@
(program
0.0.0
(con
bls12_381_G1_element
0xa1e9a0c68985059bd25a5ef05b351ca22f7d7c19e37928583ae12a1f4939440ff754cfd85b23df4a54f66c7089db6deb
)
)

View File

@@ -0,0 +1,5 @@
-- This is a valid serialisation of a point on G1 (obtained by hashing 0x0102030405),
-- but we only accept compressed points.
(program 0.0.0
(con bls12_381_G1_element 0x01e9a0c68985059bd25a5ef05b351ca22f7d7c19e37928583ae12a1f4939440ff754cfd85b23df4a54f66c7089db6deb12ae8470d881eb628dfcf4bb083fb8a6968d907a0c265f6d06e04b05a19418d395d3e0c115430f88e7156822904ef5bf)
)

View File

@@ -0,0 +1,4 @@
-- This is a valid point on the E1 curve, but it's not in the G1 subgroup.
(program 0.0.0
(con bls12_381_G1_element 0xa00000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000005)
)

View File

@@ -0,0 +1,4 @@
-- The compressed encoding of the zero element of G1, but with an extra zero byte at the end.
(program 0.0.0
(con bls12_381_G1_element 0xc000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000)
)

View File

@@ -0,0 +1,4 @@
-- The zero element of G1, but one byte short
(program 0.0.0
(con bls12_381_G1_element 0xc000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000)
)

View File

@@ -0,0 +1,4 @@
-- A correct compressed encoding of the zero element of G1.
(program 0.0.0
(con bls12_381_G1_element 0xc00000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000)
)

View File

@@ -0,0 +1,2 @@
({cpu: 23100
| mem: 200})

View File

@@ -0,0 +1,7 @@
(program
0.0.0
(con
bls12_381_G1_element
0xc00000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000
)
)

View File

@@ -0,0 +1,4 @@
-- Missing the 0x prefix.
(program 0.0.0
(con bls12_381_G2_element c00000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000)
)

View File

@@ -0,0 +1,4 @@
-- This has # instead of 0x.
(program 0.0.0
(con bls12_381_G2_element #c00000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000)
)

View File

@@ -0,0 +1,4 @@
-- A bad encoding: this has the negative bit set, but nothing else.
(program 0.0.0
(con bls12_381_G2_element 0x400000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000)
)

View File

@@ -0,0 +1,4 @@
-- Almost a correct represntation of the zero point, but with the negation bit set.
(program 0.0.0
(con bls12_381_G2_element 0xe00000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000)
)

View File

@@ -0,0 +1,4 @@
-- The zero point, but with a random bit set in the body (should all be 0)
(program 0.0.0
(con bls12_381_G2_element 0xc0000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000010000000000000000000000000000000000000000000000000)
)

View File

@@ -0,0 +1,4 @@
-- This encodes a field element which isn't the x-coordinate of any point on the curve (no square root).
(program 0.0.0
(con bls12_381_G2_element 0xa00000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000003)
)

View File

@@ -0,0 +1,4 @@
-- This is a valid encoding with the sign bit clear.
(program 0.0.0
(con bls12_381_G2_element 0x88138ebea766d4d1aa64dd3b5826244c32ea3fe9351f9c8d584203716dae151d14bb5d06e245c24877955c79287682ba082d077bbb2afdb1ad1d48d18e2f0c56b001bce207801adfa9fd451fc59d56f0433b02f921ba5a272c58c06536291d07)
)

View File

@@ -0,0 +1,7 @@
(program
0.0.0
(con
bls12_381_G2_element
0x88138ebea766d4d1aa64dd3b5826244c32ea3fe9351f9c8d584203716dae151d14bb5d06e245c24877955c79287682ba082d077bbb2afdb1ad1d48d18e2f0c56b001bce207801adfa9fd451fc59d56f0433b02f921ba5a272c58c06536291d07
)
)

View File

@@ -0,0 +1,4 @@
-- This is a valid encoding with the sign bit set (obtained by hashing 0x0102030405 to G2)
(program 0.0.0
(con bls12_381_G2_element 0xa8138ebea766d4d1aa64dd3b5826244c32ea3fe9351f9c8d584203716dae151d14bb5d06e245c24877955c79287682ba082d077bbb2afdb1ad1d48d18e2f0c56b001bce207801adfa9fd451fc59d56f0433b02f921ba5a272c58c06536291d07)
)

View File

@@ -0,0 +1,7 @@
(program
0.0.0
(con
bls12_381_G2_element
0xa8138ebea766d4d1aa64dd3b5826244c32ea3fe9351f9c8d584203716dae151d14bb5d06e245c24877955c79287682ba082d077bbb2afdb1ad1d48d18e2f0c56b001bce207801adfa9fd451fc59d56f0433b02f921ba5a272c58c06536291d07
)
)

View File

@@ -0,0 +1,5 @@
-- This is a valid serialisation of a point on G2 (obtained by hashing 0x0102030405),
-- but we only accept compressed points.
(program 0.0.0
(con bls12_381_G2_element 0x08138ebea766d4d1aa64dd3b5826244c32ea3fe9351f9c8d584203716dae151d14bb5d06e245c24877955c79287682ba082d077bbb2afdb1ad1d48d18e2f0c56b001bce207801adfa9fd451fc59d56f0433b02f921ba5a272c58c06536291d071676b275e27060b26dd91aac0a1feb56d1c1de7c323f486e48d54eae0c3c8f4caa45faad589c5d180ac0830dcdb3ecd8126c9c5db86cdf7129cf18582013d267a7c2827a901ef61ab58e7ef150219441abc57671eb39009f6bb166bcbade700d)
)

View File

@@ -0,0 +1,4 @@
-- This is a valid point on the E2 curve, but it's not in the G2 subgroup.
(program 0.0.0
(con bls12_381_G2_element 0xa00000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000005)
)

View File

@@ -0,0 +1,4 @@
-- The compressed encoding of the zero element of G2, but with an extra zero byte at the end.
(program 0.0.0
(con bls12_381_G2_element 0xc0000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000)
)

View File

@@ -0,0 +1,4 @@
-- The zero element of G2, but one byte short
(program 0.0.0
(con bls12_381_G2_element 0xc000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000)
)

View File

@@ -0,0 +1,4 @@
-- A correct compressed encoding of the zero element of G2
(program 0.0.0
(con bls12_381_G2_element 0xc00000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000)
)

View File

@@ -0,0 +1,2 @@
({cpu: 23100
| mem: 200})

View File

@@ -0,0 +1,7 @@
(program
0.0.0
(con
bls12_381_G2_element
0xc00000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000
)
)

View File

@@ -0,0 +1 @@
(program 0.0.0 (con bool False))

View File

@@ -0,0 +1,2 @@
({cpu: 23100
| mem: 200})

View File

@@ -0,0 +1 @@
(program 0.0.0 (con bool False))

View File

@@ -0,0 +1 @@
(program 0.0.0 (con bool True))

View File

@@ -0,0 +1,2 @@
({cpu: 23100
| mem: 200})

View File

@@ -0,0 +1 @@
(program 0.0.0 (con bool True))

View File

@@ -0,0 +1 @@
(program 0.0.0 (con bytestring #00ff))

View File

@@ -0,0 +1 @@
(program 0.0.0 (con bytestring #00ff))

View File

@@ -0,0 +1,3 @@
(program 1.0.0
(con bytestring #54686543616B654973414C6965)
)

View File

@@ -0,0 +1 @@
(program 1.0.0 (con bytestring #54686543616B654973414C6965))

View File

@@ -0,0 +1,3 @@
(program 1.0.0
(con bytestring #)
)

View File

@@ -0,0 +1 @@
(program 1.0.0 (con bytestring #))

View File

@@ -0,0 +1,3 @@
(program 1.0.0
(con bytestring #12345)
)

View File

@@ -0,0 +1 @@
(program 0.0.0 (con data (B #0123456789ABCDEF)))

View File

@@ -0,0 +1 @@
(program 0.0.0 (con data (B #0123456789abcdef)))

View File

@@ -0,0 +1 @@
(program 0.0.0 (con data (Constr 1 [I 1])))

Some files were not shown because too many files have changed in this diff Show More