test: add all plutus conformance tests

This commit is contained in:
rvcas 2023-11-15 00:07:00 -05:00 committed by Lucas
parent b80db2f7f8
commit b6f6064aaf
880 changed files with 5384 additions and 2 deletions

1
Cargo.lock generated vendored
View File

@ -3037,6 +3037,7 @@ dependencies = [
"strum",
"strum_macros",
"thiserror",
"walkdir",
]
[[package]]

View File

@ -10,6 +10,7 @@ shared-version = true
tag-name = "v{{version}}"
[workspace.dependencies]
walkdir = "2.3.2"
insta = { version = "1.30.0", features = ["yaml", "json"] }
[profile.dev.package.insta]

View File

@ -40,7 +40,7 @@ strip-ansi-escapes = "0.1.1"
thiserror = "1.0.39"
tokio = { version = "1.26.0", features = ["full"] }
toml = "0.7.2"
walkdir = "2.3.2"
walkdir.workspace = true
zip = "0.6.4"
aiken-lang = { path = "../aiken-lang", version = "1.0.20-alpha" }

View File

@ -45,3 +45,4 @@ k256 = { version = "0.13.0" }
[dev-dependencies]
hex = "0.4.3"
indoc = "2.0.1"
walkdir.workspace = true

View File

@ -403,7 +403,7 @@ impl From<&Constant> for Type {
mod tests {
use num_bigint::BigInt;
use super::cost_model::ExBudget;
use super::{cost_model::ExBudget, runtime::Compressable};
use crate::{
ast::{Constant, NamedDeBruijn, Program, Term},
builtins::DefaultFunction,
@ -543,4 +543,116 @@ mod tests {
);
}
}
#[test]
fn bls_g1_add_associative() {
let a = blst::blst_p1::uncompress(&[
0xab, 0xd6, 0x18, 0x64, 0xf5, 0x19, 0x74, 0x80, 0x32, 0x55, 0x1e, 0x42, 0xe0, 0xac,
0x41, 0x7f, 0xd8, 0x28, 0xf0, 0x79, 0x45, 0x4e, 0x3e, 0x3c, 0x98, 0x91, 0xc5, 0xc2,
0x9e, 0xd7, 0xf1, 0x0b, 0xde, 0xcc, 0x04, 0x68, 0x54, 0xe3, 0x93, 0x1c, 0xb7, 0x00,
0x27, 0x79, 0xbd, 0x76, 0xd7, 0x1f,
])
.unwrap();
let b = blst::blst_p1::uncompress(&[
0x95, 0x0d, 0xfd, 0x33, 0xda, 0x26, 0x82, 0x26, 0x0c, 0x76, 0x03, 0x8d, 0xfb, 0x8b,
0xad, 0x6e, 0x84, 0xae, 0x9d, 0x59, 0x9a, 0x3c, 0x15, 0x18, 0x15, 0x94, 0x5a, 0xc1,
0xe6, 0xef, 0x6b, 0x10, 0x27, 0xcd, 0x91, 0x7f, 0x39, 0x07, 0x47, 0x9d, 0x20, 0xd6,
0x36, 0xce, 0x43, 0x7a, 0x41, 0xf5,
])
.unwrap();
let c = blst::blst_p1::uncompress(&[
0xb9, 0x62, 0xfd, 0x0c, 0xc8, 0x10, 0x48, 0xe0, 0xcf, 0x75, 0x57, 0xbf, 0x3e, 0x4b,
0x6e, 0xdc, 0x5a, 0xb4, 0xbf, 0xb3, 0xdc, 0x87, 0xf8, 0x3a, 0xf4, 0x28, 0xb6, 0x30,
0x07, 0x27, 0xb1, 0x39, 0xc4, 0x04, 0xab, 0x15, 0x9b, 0xdf, 0x2e, 0xae, 0xa3, 0xf6,
0x49, 0x90, 0x34, 0x21, 0x53, 0x7f,
])
.unwrap();
let term: Term<NamedDeBruijn> = Term::bls12_381_g1_equal()
.apply(
Term::bls12_381_g1_add().apply(Term::bls12_381_g1(a)).apply(
Term::bls12_381_g1_add()
.apply(Term::bls12_381_g1(b))
.apply(Term::bls12_381_g1(c)),
),
)
.apply(
Term::bls12_381_g1_add()
.apply(
Term::bls12_381_g1_add()
.apply(Term::bls12_381_g1(a))
.apply(Term::bls12_381_g1(b)),
)
.apply(Term::bls12_381_g1(c)),
);
let program = Program {
version: (1, 0, 0),
term,
};
let eval_result = program.eval(Default::default());
let final_term = eval_result.result().unwrap();
assert_eq!(final_term, Term::bool(true))
}
#[test]
fn bls_g2_add_associative() {
let a = blst::blst_p1::uncompress(&[
0xab, 0xd6, 0x18, 0x64, 0xf5, 0x19, 0x74, 0x80, 0x32, 0x55, 0x1e, 0x42, 0xe0, 0xac,
0x41, 0x7f, 0xd8, 0x28, 0xf0, 0x79, 0x45, 0x4e, 0x3e, 0x3c, 0x98, 0x91, 0xc5, 0xc2,
0x9e, 0xd7, 0xf1, 0x0b, 0xde, 0xcc, 0x04, 0x68, 0x54, 0xe3, 0x93, 0x1c, 0xb7, 0x00,
0x27, 0x79, 0xbd, 0x76, 0xd7, 0x1f,
])
.unwrap();
let b = blst::blst_p1::uncompress(&[
0x95, 0x0d, 0xfd, 0x33, 0xda, 0x26, 0x82, 0x26, 0x0c, 0x76, 0x03, 0x8d, 0xfb, 0x8b,
0xad, 0x6e, 0x84, 0xae, 0x9d, 0x59, 0x9a, 0x3c, 0x15, 0x18, 0x15, 0x94, 0x5a, 0xc1,
0xe6, 0xef, 0x6b, 0x10, 0x27, 0xcd, 0x91, 0x7f, 0x39, 0x07, 0x47, 0x9d, 0x20, 0xd6,
0x36, 0xce, 0x43, 0x7a, 0x41, 0xf5,
])
.unwrap();
let c = blst::blst_p1::uncompress(&[
0xb9, 0x62, 0xfd, 0x0c, 0xc8, 0x10, 0x48, 0xe0, 0xcf, 0x75, 0x57, 0xbf, 0x3e, 0x4b,
0x6e, 0xdc, 0x5a, 0xb4, 0xbf, 0xb3, 0xdc, 0x87, 0xf8, 0x3a, 0xf4, 0x28, 0xb6, 0x30,
0x07, 0x27, 0xb1, 0x39, 0xc4, 0x04, 0xab, 0x15, 0x9b, 0xdf, 0x2e, 0xae, 0xa3, 0xf6,
0x49, 0x90, 0x34, 0x21, 0x53, 0x7f,
])
.unwrap();
let term: Term<NamedDeBruijn> = Term::bls12_381_g1_equal()
.apply(
Term::bls12_381_g1_add().apply(Term::bls12_381_g1(a)).apply(
Term::bls12_381_g1_add()
.apply(Term::bls12_381_g1(b))
.apply(Term::bls12_381_g1(c)),
),
)
.apply(
Term::bls12_381_g1_add()
.apply(
Term::bls12_381_g1_add()
.apply(Term::bls12_381_g1(a))
.apply(Term::bls12_381_g1(b)),
)
.apply(Term::bls12_381_g1(c)),
);
let program = Program {
version: (1, 0, 0),
term,
};
let eval_result = program.eval(Default::default());
let final_term = eval_result.result().unwrap();
assert_eq!(final_term, Term::bool(true))
}
}

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,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,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 @@
(program 0.0.0 (con bool False))

View File

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

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])))

View File

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

View File

@ -0,0 +1 @@
(program 0.0.0 (con data (I 12354898)))

View File

@ -0,0 +1 @@
(program 0.0.0 (con data (I 12354898)))

View File

@ -0,0 +1 @@
(program 0.0.0 (con data (List [Constr 1 [], I 1234, B #ABCDEF])))

View File

@ -0,0 +1 @@
(program 0.0.0 (con data (List [Constr 1 [], I 1234, B #abcdef])))

View File

@ -0,0 +1,5 @@
(program 0.0.0 (con data (
Map [ (B #0123, I 12345),
(B #456789, I 789453),
(B #0ABCDE, I 12364689486)]
)))

View File

@ -0,0 +1,8 @@
(program
0.0.0
(con
data
(Map
[(B #0123, I 12345), (B #456789, I 789453), (B #0abcde, I 12364689486)])
)
)

View File

@ -0,0 +1 @@
(program 0.0.0 (con data (B 42)))

View File

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

View File

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

View File

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

View File

@ -0,0 +1,5 @@
(program 0.0.0 (con data (
List [ (B #0123, I 12345),
(B #456789, I 789453),
(B #0ABCDE, I 12364689486)]
)))

View File

@ -0,0 +1 @@
(program 0.0.0 (con integer 0))

View File

@ -0,0 +1 @@
(program 0.0.0 (con integer 0))

View File

@ -0,0 +1 @@
(program 0.0.0 (con integer #12))

View File

@ -0,0 +1 @@
(program 0.0.0 (con integer 1))

View File

@ -0,0 +1 @@
(program 0.0.0 (con integer 1))

View File

@ -0,0 +1 @@
(program 0.0.0 (con integer -1))

View File

@ -0,0 +1 @@
(program 0.0.0 (con integer -1))

View File

@ -0,0 +1 @@
(program 0.0.0 (con integer 000000000000000000000000000000000000012345))

View File

@ -0,0 +1 @@
(program 0.0.0 (con integer 12345))

View File

@ -0,0 +1 @@
(program 0.0.0 (con integer -000000000000000000000000000000000000012345))

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