Skip to content

Commit

Permalink
Mul assign felt proptest (#717)
Browse files Browse the repository at this point in the history
* DO NOT PUSH this commit

* test for multiplication with assignment

* minor fix

Co-authored-by: Martina <martina@martina>
Co-authored-by: Juan-M-V <102986292+Juan-M-V@users.noreply.github.com>
  • Loading branch information
3 people authored Jan 17, 2023
1 parent 32ebe5f commit fe02a36
Showing 1 changed file with 12 additions and 1 deletion.
13 changes: 12 additions & 1 deletion felt/src/lib.rs
Original file line number Diff line number Diff line change
Expand Up @@ -213,10 +213,21 @@ mod test {
prop_assert!(as_uint < p, "{}", as_uint);
}

#[test]
// Property-based test that ensures, for 100 {x} and {y} values that are randomly generated each time tests are run, that a multiplication with assignment between two felts {x} and {y} and doesn't fall outside the range [0, p]. The values of {x} and {y} can be either [0] or a very large number.
fn mul_assign_in_range(ref x in "(0|[1-9][0-9]*)", ref y in "(0|[1-9][0-9]*)") {
let mut x = Felt::parse_bytes(x.as_bytes(), 10).unwrap();
let y = &Felt::parse_bytes(y.as_bytes(), 10).unwrap();
let p = &BigUint::parse_bytes(PRIME_STR[2..].as_bytes(), 16).unwrap();

x *= y;
let as_uint = &x.to_biguint();
prop_assert!(as_uint < p, "{}", as_uint);
}

#[test]
// Property-based test that ensures, for 100 {x} and {y} values that are randomly generated each time tests are run, that the result of the division of {x} by {y} is the inverse multiplicative of {x} --that is, multiplying the result by {y} returns the original number {x}. The values of {x} and {y} can be either [0] or a very large number.
fn div_is_mul_inv(ref x in "(0|[1-9][0-9]*)", ref y in "[1-9][0-9]*") {

let x = &Felt::parse_bytes(x.as_bytes(), 10).unwrap();
let y = &Felt::parse_bytes(y.as_bytes(), 10).unwrap();
prop_assume!(!y.is_zero());
Expand Down

0 comments on commit fe02a36

Please sign in to comment.