mod compile;
use compile::Compile;
use verified::*;
const TRUE: B1 = B1;
const FALSE: B0 = B0;
#[test]
fn can_verify_single_bool_identity_clause() {
#[verify]
fn f<B: Bit>(_: B)
where
_: Verify<{ B }>,
{
}
f(TRUE);
}
#[test]
fn can_verify_multiple_bool_identity_clauses() {
#[verify]
fn f<A: Bit, B: Bit>(_: A, _: B)
where
_: Verify<{ A }, { B }>,
{
}
f(TRUE, TRUE);
}
#[test]
fn can_verify_bool_equality_clause() {
#[verify]
fn f<A: Bit, B: Bit>(_: A, _: B)
where
_: Verify<{ A == B }>,
{
}
f(FALSE, FALSE);
}
#[test]
fn can_verify_bool_and_clause() {
#[verify]
fn f<A: Bit, B: Bit>(_: A, _: B)
where
_: Verify<{ A & B }>,
{
}
f(TRUE, TRUE);
}
#[test]
fn can_verify_bool_or_clause() {
#[verify]
fn f<A: Bit, B: Bit>(_: A, _: B)
where
_: Verify<{ A | B }>,
{
}
f(FALSE, TRUE);
f(TRUE, TRUE);
f(TRUE, TRUE);
}
#[test]
fn can_verify_bool_xor_clause() {
#[verify]
fn f<A: Bit, B: Bit>(_: A, _: B)
where
_: Verify<{ A ^ B }>,
{
}
f(FALSE, TRUE);
f(TRUE, FALSE);
}
#[test]
fn can_verify_bool_not_clause() {
#[verify]
fn f<B: Bit>(_: B)
where
_: Verify<{ !B }>,
{
}
f(FALSE);
}
#[test]
fn can_verify_parenthesised_clause() {
#[verify]
fn f<B: Bit>(_: B)
where
_: Verify<{ (B) }>,
{
}
f(TRUE);
}
#[test]
fn can_verify_nested_binary_clauses() {
#[verify]
fn f<A: Bit, B: Bit, C: Bit>(_: A, _: B, _: C)
where
_: Verify<{ (A & (B | C)) == C }>,
{
}
f(TRUE, FALSE, FALSE);
}
#[test]
fn can_verify_nested_unary_clause() {
#[verify]
fn f<A: Bit, B: Bit>(_: A, _: B)
where
_: Verify<{ !(A & B) }>,
{
}
f(TRUE, FALSE);
}
#[test]
fn can_verify_bool_less_than_clauses() {
#[verify]
fn f<A: Bit, B: Bit>(_: A, _: B)
where
_: Verify<{ A < B }>,
{
}
f(FALSE, TRUE);
}
#[test]
fn can_verify_bool_greater_than_clauses() {
#[verify]
fn f<A: Bit, B: Bit>(_: A, _: B)
where
_: Verify<{ A > B }>,
{
}
f(TRUE, FALSE);
}
#[test]
fn can_verify_bool_less_equal_clauses() {
#[verify]
fn f<A: Bit, B: Bit>(_: A, _: B)
where
_: Verify<{ A <= B }>,
{
}
f(FALSE, TRUE);
f(FALSE, FALSE);
f(TRUE, TRUE);
}
#[test]
fn can_verify_bool_greater_equal_clauses() {
#[verify]
fn f<A: Bit, B: Bit>(_: A, _: B)
where
_: Verify<{ A >= B }>,
{
}
f(TRUE, FALSE);
f(FALSE, FALSE);
f(TRUE, TRUE);
}
#[test]
fn can_verify_bool_not_equal_clauses() {
#[verify]
fn f<A: Bit, B: Bit>(_: A, _: B)
where
_: Verify<{ A != B }>,
{
}
f(TRUE, FALSE);
}
#[test]
fn can_verify_usize_bitand_clauses() {
#[verify]
fn f<A: Unsigned, B: Unsigned, C: Unsigned>(_: A, _: B, _: C)
where
_: Verify<{ (A & B) == C }>,
{
}
f(U2::default(), U1::default(), U0::default());
f(U2::default(), U2::default(), U2::default());
}
#[test]
fn can_verify_usize_bitor_clauses() {
#[verify]
fn f<A: Unsigned, B: Unsigned, C: Unsigned>(_: A, _: B, _: C)
where
_: Verify<{ (A | B) == C }>,
{
}
f(U2::default(), U1::default(), U3::default());
f(U2::default(), U2::default(), U2::default());
}
#[test]
fn can_verify_usize_bitxor_clauses() {
#[verify]
fn f<A: Unsigned, B: Unsigned, C: Unsigned>(_: A, _: B, _: C)
where
_: Verify<{ (A ^ B) == C }>,
{
}
f(U2::default(), U1::default(), U3::default());
f(U0::default(), U0::default(), U0::default());
f(U2::default(), U2::default(), U0::default());
}
#[test]
fn can_verify_bool_literals() {
#[verify]
fn f<B: Bit>(_: B)
where
_: Verify<{ B == false }, { B == !true }>,
{
}
f(FALSE);
}
#[test]
fn can_verify_usize_literals() {
#[verify]
fn f<Six: Unsigned, Zero: Unsigned>(_: Six, _: Zero)
where
_: Verify<{ Six == 6 }, { Zero == 0 }>,
{
}
f(U6::default(), U0::default());
}
#[test]
fn can_verify_usize_addition_clauses() {
#[verify]
fn f<A: Unsigned, B: Unsigned>(_: A, _: B)
where
_: Verify<{ (A + B) == 5 }>,
{
}
f(U2::default(), U3::default());
}
#[test]
fn can_verify_usize_subtraction_clauses() {
#[verify]
fn f<A: Unsigned, B: Unsigned>(_: A, _: B)
where
_: Verify<{ (A - B) == 3 }>,
{
}
f(U5::default(), U2::default());
}
#[test]
fn can_verify_usize_multiplication_clauses() {
#[verify]
fn f<A: Unsigned, B: Unsigned>(_: A, _: B)
where
_: Verify<{ (A * B) == 8 }>,
{
}
f(U2::default(), U4::default());
}
#[test]
fn can_verify_usize_division_clauses() {
#[verify]
fn f<A: Unsigned, B: Unsigned>(_: A, _: B)
where
_: Verify<{ (A / B) == 4 }>,
{
}
f(U8::default(), U2::default());
}
#[test]
fn can_verify_usize_rem_clauses() {
#[verify]
fn f<A: Unsigned, B: Unsigned>(_: A, _: B)
where
_: Verify<{ (A % B) == 2 }>,
{
}
f(U8::default(), U3::default());
}
#[test]
fn can_verify_usize_shl_clauses() {
#[verify]
fn f<A: Unsigned>(_: A)
where
_: Verify<{ (A << 2) == 4 }>,
{
}
f(U1::default());
}
#[test]
fn can_verify_usize_shr_clauses() {
#[verify]
fn f<A: Unsigned>(_: A)
where
_: Verify<{ (A >> 2) == 1 }>,
{
}
f(U4::default());
}
#[test]
fn can_verify_usize_less_than_clauses() {
#[verify]
fn f<A: Unsigned, B: Unsigned>(_: A, _: B)
where
_: Verify<{ A < B }>,
{
}
f(U2::default(), U3::default());
}
#[test]
fn can_verify_usize_greater_than_clauses() {
#[verify]
fn f<A: Unsigned, B: Unsigned>(_: A, _: B)
where
_: Verify<{ A > B }>,
{
}
f(U3::default(), U2::default());
}
#[test]
fn can_verify_usize_less_equal_clauses() {
#[verify]
fn f<A: Unsigned, B: Unsigned>(_: A, _: B)
where
_: Verify<{ A <= B }>,
{
}
f(U2::default(), U3::default());
f(U3::default(), U3::default());
}
#[test]
fn can_verify_usize_greater_equal_clauses() {
#[verify]
fn f<A: Unsigned, B: Unsigned>(_: A, _: B)
where
_: Verify<{ A >= B }>,
{
}
f(U3::default(), U2::default());
f(U3::default(), U3::default());
}
#[test]
fn can_verify_usize_not_equal_clauses() {
#[verify]
fn f<A: Unsigned, B: Unsigned>(_: A, _: B)
where
_: Verify<{ A != B }>,
{
}
f(U3::default(), U2::default());
}
#[test]
fn can_verify_result_simple_addition_in_function_body_lhs() {
#[verify]
fn f<A: Unsigned, B: Unsigned, C: Unsigned>(a: A, b: B) -> C
where
_: Verify<{ A + B == C }>,
{
a + b
}
let _: U3 = f(U1::default(), U2::default());
}
#[test]
fn can_verify_result_simple_addition_in_function_body_rhs() {
#[verify]
fn f<A: Unsigned, B: Unsigned, C: Unsigned>(a: A, b: B) -> C
where
_: Verify<{ C == A + B }>,
{
a + b
}
let _: U3 = f(U1::default(), U2::default());
}
#[test]
fn can_verify_bools_without_braces() {
#[verify]
fn f<B: Bit>(_: B)
where
_: Verify<B>,
{
}
f(TRUE);
}
#[test]
fn can_verify_type_construction_in_fn_return_value() {
struct Pod<V: Unsigned>(V);
#[verify]
fn f<A: Unsigned>() -> Pod<{ A + 2 }>
where
A: Unsigned,
<A as Add<U2>>::Output: Unsigned,
{
Pod(Default::default())
}
let _: Pod<U5> = f::<U3>();
}
#[test]
#[ignore] // TODO: figure out how to make this test pass in automation.
#[allow(non_snake_case)]
fn compilation_tests() {
// TODO: Fix error handling.
Compile(
"Error_when_multiple_inferred_bounds_are_supplied.rs",
"
use verified::*;
#[verify]
fn _f<B: Bit>()
where
_: Verify<{ B }>,
_: Verify<{ B }>,
{}
",
)
.and_expect(
"
error: did not expect to find second `Verify` bound
--> $DIR/Error_when_multiple_inferred_bounds_are_supplied.rs:7:9
|
7 | _: Verify<{ B }>,
| ^^^^^^^^^^^^^^^^
",
);
Compile(
"Error_when_inferred_bound_is_not_Verify.rs",
"
use verified::*;
#[verify]
fn _f<B: Bit>()
where
_: SomethingElse<{ B }>,
{}
",
)
.and_expect(
"
error: expected `Verify<_>`
--> $DIR/Error_when_inferred_bound_is_not_Verify.rs:6:12
|
6 | _: SomethingElse<{ B }>,
| ^^^^^^^^^^^^^^^^^^^^
",
);
Compile(
"Error_on_unsupported_expression_in_clause.rs",
"
use verified::*;
#[verify]
fn _f<A: Bit, B: Bit>()
where
_: Verify<{ A *= B }>,
{}
",
)
.and_expect(
"
error: unsupported logical expression
--> $DIR/Error_on_unsupported_expression_in_clause.rs:6:21
|
6 | _: Verify<{ A *= B }>,
| ^^^^^^
",
);
Compile(
"Error_on_unsupported_literal_in_clause.rs",
"
use verified::*;
#[verify]
fn _f<N: Unsigned>()
where
_: Verify<{ N == \"abc\" }>,
{}
",
)
.and_expect(
"
error: only bool and int literals are supported here
--> $DIR/Error_on_unsupported_literal_in_clause.rs:6:26
|
6 | _: Verify<{ N == \"abc\" }>,
| ^^^^^
",
);
}