From 2cd07acad0aa05a1fca299ba15f981b5d7c34f12 Mon Sep 17 00:00:00 2001 From: Balazs Komuves Date: Fri, 30 Jan 2026 06:41:16 +0100 Subject: [PATCH] implemented modular inversion (just for the kick of it) + lots of new tests (inversion certainly makes testing more serious!) --- README.md | 3 +- sanity/sanity.hs | 1 + src/bin/testmain.rs | 20 ++++ src/bn254/bigint.rs | 92 +++++++++++++++- src/bn254/constant.rs | 2 +- src/bn254/euclid.rs | 60 ++++++++++ src/bn254/field.rs | 37 ++++++- src/bn254/mod.rs | 1 + src/bn254/montgomery.rs | 2 + src/bn254/platform/unstable.rs | 28 ++++- src/bn254/test/bigint.rs | 16 +++ src/bn254/test/field.rs | 194 +++++++++++++++++++++++++++++++++ src/bn254/test/mod.rs | 2 +- src/bn254/test/properties.rs | 52 ++++++++- src/bn254/traits.rs | 8 +- 15 files changed, 505 insertions(+), 13 deletions(-) create mode 100644 src/bn254/euclid.rs create mode 100644 src/bn254/test/field.rs diff --git a/README.md b/README.md index caf39e9..e7626f3 100644 --- a/README.md +++ b/README.md @@ -91,8 +91,9 @@ On modern 64-bit CPU-s, the 64-bit version would be preferred (TODO: implement i - [x] clean up the code and make it more idiomatic - [x] implement `circomlib`-compatible Poseidon - [x] benchmark RISC-V cycles +- [x] add a proper test-suite; in particular, more complete testing of the field operations +- [ ] add more tests for the corner cases specifically - [ ] add more Poseidon2 state widths (not just `t=3`) -- [ ] add a proper test-suite; in particular, more complete testing of the field operations - [ ] add a 64 bit version - [ ] implement the sponge construction - [ ] optimize squaring to use less multiplications (?) diff --git a/sanity/sanity.hs b/sanity/sanity.hs index e831468..05d45f7 100644 --- a/sanity/sanity.hs +++ b/sanity/sanity.hs @@ -15,6 +15,7 @@ import "random" System.Random u32_mask = 0xFFFF_FFFF prime = 21888242871839275222246405745257275088548364400416034343698204186575808495617 +halfp1 = (div prime 2) + 1 r1 = 0x0e0a77c19a07df2f666ea36f7879462e36fc76959f60cd29ac96341c4ffffffb r2 = 0x0216d0b17f4e44a58c49833d53bb808553fe3ab1e35c59e31bb8e645ae216da7 diff --git a/src/bin/testmain.rs b/src/bin/testmain.rs index 1de87c6..d2c6744 100644 --- a/src/bin/testmain.rs +++ b/src/bin/testmain.rs @@ -240,5 +240,25 @@ fn main() { //---------------------------------------------------------------------------- println!("{}" , Mont::one() == Mont::convert_from_u32(1) ); + + //---------------------------------------------------------------------------- + + println!(""); + let a = BIG1 ; let (b , c ) = BigInt::shiftRightBy1(a ); + let a1 = a + BigInt::one() ; let (b1, c1) = BigInt::shiftRightBy1(a1); + println!(" a >> 1 = {} -> {} {}", a , b , c ); + println!("(a+1) >> 1 = {} -> {} {}", a1, b1, c1 ); + + println!(""); + let a = FELT1; + let b = FELT2; + let q = Felt::div(a,b); + let r = Felt::mul(q,b); + println!("a = {}" , a); + println!("b = {}" , b); + println!("a/b = {}" , q); + println!("(a/b)*b = {}" , r); + println!("ok = {}", r == a); + } diff --git a/src/bn254/bigint.rs b/src/bn254/bigint.rs index 76900a4..d1f87d8 100644 --- a/src/bn254/bigint.rs +++ b/src/bn254/bigint.rs @@ -19,7 +19,7 @@ use unroll::unroll_for_loops; use crate::bn254::traits::*; use crate::bn254::platform::*; -use crate::bn254::constant::{PRIME_ARRAY}; +use crate::bn254::constant::*; //------------------------------------------------------------------------------ @@ -270,6 +270,53 @@ impl BigInt { res } + //------------------------------------ + // shifts + + #[inline(always)] + pub fn is_even(big: BigInt) -> bool { + (big.0[0] & 1) == 0 + } + + #[inline(always)] + pub fn is_odd(big: BigInt) -> bool { + (big.0[0] & 1) != 0 + } + + #[unroll_for_loops] + pub fn rotLeftBy1(big: BigInt, cin: bool) -> (bool, BigInt) { + let limbs : [u32; N] = big.0; + let mut out : [u32; N] = [0; N]; + let mut carry : bool = cin; + for i in 0..N { + let (c,y) = rotLeft32By1(limbs[i], carry); + out[i] = y; + carry = c; + } + (carry, BigInt(out)) + } + + #[unroll_for_loops] + pub fn rotRightBy1(cin: bool, big: BigInt) -> (BigInt, bool) { + let limbs : [u32; N] = big.0; + let mut out : [u32; N] = [0; N]; + let mut carry : bool = cin; + for i in (0..N).rev() { + let (y,c) = rotRight32By1(carry, limbs[i]); + out[i] = y; + carry = c; + } + (BigInt(out), carry) + } + + pub fn shiftLeftBy1(big: BigInt) -> (bool, BigInt) { + BigInt::rotLeftBy1(big, false) + } + + pub fn shiftRightBy1(big: BigInt) -> (BigInt, bool) { + BigInt::rotRightBy1(false, big) + } + //------------------------------------ // addition and subtraction @@ -480,7 +527,7 @@ impl BigInt256 { #[inline(always)] #[unroll_for_loops] pub fn add_prime(big: BigInt256) -> (BigInt256, bool) { - let mut c : bool = false; + let mut c : bool = false; let mut zs : [u32; 8] = [0; 8]; for i in 0..8 { let (z,cout) = addCarry32( big.0[i] , PRIME_ARRAY[i] , c ); @@ -491,10 +538,24 @@ impl BigInt256 { (big, c) } + #[inline(always)] + #[unroll_for_loops] + pub fn add_half_prime_plus_1(big: BigInt256) -> BigInt256 { + let mut c : bool = false; + let mut zs : [u32; 8] = [0; 8]; + for i in 0..8 { + let (z,cout) = addCarry32( big.0[i] , HALFP_PLUS_1.0[i] , c ); + c = cout; + zs[i] = z; + } + // assert!( !c ); // it would ruin the quickcheck tests.. + BigInt(zs) + } + #[inline(always)] #[unroll_for_loops] pub fn subtract_prime(big: BigInt256) -> (BigInt256, bool) { - let mut c : bool = false; + let mut c : bool = false; let mut zs : [u32; 8] = [0; 8]; for i in 0..8 { let (z,cout) = subBorrow32( big.0[i] , PRIME_ARRAY[i] , c ); @@ -516,8 +577,31 @@ impl BigInt256 { } } + #[inline(always)] + pub fn div_by_2_mod_prime(big: BigInt256) -> BigInt256 { + let (half, carry): (BigInt256, bool) = BigInt::shiftRightBy1(big); + if carry { + BigInt256::add_half_prime_plus_1(half) + } + else { + half + } + } + + #[inline(always)] + pub fn sub_mod_prime(big1: BigInt256, big2: BigInt256) -> BigInt256 { + let (big, carry) = BigInt::subBorrow(big1, big2); + if carry { + let (corrected, _) = BigInt::add_prime(big); + corrected + } + else { + big + } + } + //------------------------------------ - // ramndom + // random fn sample_masked(source: &mut (impl RandomSource + ?Sized)) -> BigInt256 { let mut xs: [u32; 8] = [0; 8]; diff --git a/src/bn254/constant.rs b/src/bn254/constant.rs index 6969473..279f67f 100644 --- a/src/bn254/constant.rs +++ b/src/bn254/constant.rs @@ -10,7 +10,7 @@ pub const PRIME_ARRAY : [u32; 8] = [ 0xf0000001 , 0x43e1f593 , 0 pub const PRIME_EXT : BigInt<9> = BigInt::make( [ 0xf0000001 , 0x43e1f593 , 0x79b97091 , 0x2833e848 , 0x8181585d , 0xb85045b6 , 0xe131a029 , 0x30644e72 , 0x00000000 ] ); pub const FIELD_PRIME : Big = BigInt::make( [ 0xf0000001 , 0x43e1f593 , 0x79b97091 , 0x2833e848 , 0x8181585d , 0xb85045b6 , 0xe131a029 , 0x30644e72 ] ); pub const PRIME_PLUS_1 : Big = BigInt::make( [ 0xf0000002 , 0x43e1f593 , 0x79b97091 , 0x2833e848 , 0x8181585d , 0xb85045b6 , 0xe131a029 , 0x30644e72 ] ); -pub const HALFP_PLUS_1 : Big = BigInt::make( [ 0xf8000001 , 0xa1f0fac9 , 0x3cdcb848 , 0x9419f424 , 0x40c0ac2e , 0xdc2822db , 0x97098d01 , 0x01832273 ] ); +pub const HALFP_PLUS_1 : Big = BigInt::make( [ 0xf8000001 , 0xa1f0fac9 , 0x3cdcb848 , 0x9419f424 , 0x40c0ac2e , 0xdc2822db , 0x7098d014 , 0x18322739 ] ); //------------------------------------------------------------------------------ // montgomery constants diff --git a/src/bn254/euclid.rs b/src/bn254/euclid.rs new file mode 100644 index 0000000..c509fa5 --- /dev/null +++ b/src/bn254/euclid.rs @@ -0,0 +1,60 @@ + +// +// extended binary euclidean algorithm +// (used for modular inversion) +// + +#![allow(unused)] +#![allow(non_snake_case)] + +use std::ops::{Neg,Add,Sub,Mul}; + +use crate::bn254::bigint::*; + +//------------------------------------------------------------------------------ + +// NOTE: the prime is hard-wired into this +pub fn euclid + ( x0: BigInt256 + , y0: BigInt256 + , u0: BigInt256 + , v0: BigInt256 + ) -> BigInt256 { + + let mut x = x0; // x and y are modulo P + let mut y = y0; + let mut u = u0; // u and v are just integers + let mut v = v0; + + while( !BigInt::is_one(u) && !BigInt::is_one(v) ) { + + // shift right u and (x mod p) while u is even + while( BigInt::is_even(u) ) { + let (u1, _) = BigInt::shiftRightBy1(u); + u = u1; + x = BigInt::div_by_2_mod_prime(x); + } + + // shift right v and (y mod p) while v is even + while( BigInt::is_even(v) ) { + let (v1, _) = BigInt::shiftRightBy1(v); + v = v1; + y = BigInt::div_by_2_mod_prime(y); + } + + if u < v { + v = v - u; + y = BigInt::sub_mod_prime( y , x ); + } + else { + u = u - v; + x = BigInt::sub_mod_prime( x , y ); + } + + } + + if BigInt::is_one(u) { x } else { y } + +} + +//------------------------------------------------------------------------------ diff --git a/src/bn254/field.rs b/src/bn254/field.rs index 06aab21..9070bd3 100644 --- a/src/bn254/field.rs +++ b/src/bn254/field.rs @@ -10,7 +10,7 @@ #![allow(non_snake_case)] use std::fmt; -use std::ops::{Neg,Add,Sub,Mul,RangeFull}; +use std::ops::{Neg,Add,Sub,Mul,Div,RangeFull}; use std::random::{RandomSource,Distribution}; @@ -18,6 +18,7 @@ use crate::bn254::traits::*; use crate::bn254::bigint::*; use crate::bn254::constant::*; use crate::bn254::montgomery::*; +use crate::bn254::euclid::*; //------------------------------------------------------------------------------ @@ -64,6 +65,11 @@ impl Mul for Felt { fn mul(self, other: Self) -> Self { Felt::mul(self, other) } } +impl Div for Felt { + type Output = Self; + fn div(self, other: Self) -> Self { Felt::div(self, other) } +} + //-------------------------------------- // (non-standard ones, too...) @@ -77,6 +83,10 @@ impl One for Felt { fn is_one(x: Self) -> bool { Felt::is_one(x) } } +impl Inv for Felt { + fn inv(x: Self) -> Self { Felt::inv(x) } +} + //------------------------------------------------------------------------------ // conversion traits @@ -125,6 +135,11 @@ impl Felt { felt.0 } + #[inline(always)] + pub const fn unsafe_from_bigint(big: BigInt<8>) -> Felt { + Felt(big) + } + #[inline(always)] pub const fn unsafe_make( xs: [u32; 8] ) -> Felt { Felt(BigInt::from_limbs(xs)) @@ -259,6 +274,26 @@ impl Felt { Felt::from_mont(Mont::mul(mont1,mont2)) } + //------------------------------------ + + pub fn div_by_2(a: Felt) -> Felt { + Felt( BigInt::div_by_2_mod_prime(a.0) ) + } + + //------------------------------------ + + pub fn div(a: Felt, b: Felt) -> Felt { + let x: BigInt256 = a.0; + let y: BigInt256 = BigInt::zero(); + let u: BigInt256 = b.0; + let v: BigInt256 = FIELD_PRIME; + Felt( euclid(x, y, u, v) ) + } + + pub fn inv(b: Felt) -> Felt { + Felt::div( Felt::one() , b ) + } + } //------------------------------------------------------------------------------ diff --git a/src/bn254/mod.rs b/src/bn254/mod.rs index 4942ff8..6c6f70b 100644 --- a/src/bn254/mod.rs +++ b/src/bn254/mod.rs @@ -4,6 +4,7 @@ mod platform; pub mod traits; pub mod bigint; pub mod constant; +pub mod euclid; pub mod montgomery; pub mod field; diff --git a/src/bn254/montgomery.rs b/src/bn254/montgomery.rs index 5755f3d..d0bf296 100644 --- a/src/bn254/montgomery.rs +++ b/src/bn254/montgomery.rs @@ -261,6 +261,8 @@ impl Mont { } */ + //---------------- + // we can abuse the fact that we know the prime number `p`, // for which `p < 2^254` so we won't overflow in the 17th word diff --git a/src/bn254/platform/unstable.rs b/src/bn254/platform/unstable.rs index ea4aa5e..e9c4821 100644 --- a/src/bn254/platform/unstable.rs +++ b/src/bn254/platform/unstable.rs @@ -11,6 +11,11 @@ pub fn boolToU32(c: bool) -> u32 { if c { 1 } else { 0 } } +#[inline(always)] +pub fn boolToMSB32(c: bool) -> u32 { + if c { 0x_8000_0000 } else { 0 } +} + //------------------------------------------------------------------------------ #[inline(always)] @@ -24,7 +29,7 @@ pub fn subBorrow32_(x: u32, y: u32) -> (u32,bool) { } #[inline(always)] -pub fn addCarry32(x :u32, y: u32, cin: bool) -> (u32,bool) { +pub fn addCarry32(x: u32, y: u32, cin: bool) -> (u32,bool) { u32::carrying_add(x,y,cin) } @@ -70,3 +75,24 @@ pub fn u64AddAdd32(xy: (u32,u32), a: u32, b: u32) -> (u32,u32) { } //------------------------------------------------------------------------------ + +// rust, please just go home, you are drunk... +#[inline(always)] +pub fn rotRight32By1(cin: bool, x: u32) -> (u32, bool) { + unsafe { + let cout : bool = (x & 1) != 0; + let y : u32 = u32::unchecked_shr(x,1) | u32::unchecked_shl(boolToU32(cin),31); + (y, cout) + } +} + +#[inline(always)] +pub fn rotLeft32By1(x: u32, cin: bool) -> (bool, u32) { + unsafe { + let cout : bool = (x & 0x_8000_0000) != 0; + let y : u32 = u32::unchecked_shl(x,1) | boolToU32(cin); + (cout, y) + } +} + +//------------------------------------------------------------------------------ diff --git a/src/bn254/test/bigint.rs b/src/bn254/test/bigint.rs index c0c43d2..472c689 100644 --- a/src/bn254/test/bigint.rs +++ b/src/bn254/test/bigint.rs @@ -1,5 +1,7 @@ +// // tests for bigints +// #![allow(unused)] @@ -8,6 +10,7 @@ use quickcheck_macros::quickcheck; use crate::bn254::traits::*; use crate::bn254::bigint::*; +use crate::bn254::constant::*; use crate::bn254::test::properties::*; type Big = BigInt<8>; @@ -128,6 +131,9 @@ fn add_commutative(x: Big, y: Big) -> bool { prop_add_commutative(x,y) } #[quickcheck] fn sub_anticommutative(x: Big, y: Big) -> bool { prop_sub_anticommutative(x,y) } +#[quickcheck] +fn add_associative(x: Big, y: Big, z: Big) -> bool { prop_add_associative(x,y,z) } + #[quickcheck] fn neg_involutive(x: Big) -> bool { prop_neg_involutive(x) } @@ -145,3 +151,13 @@ fn sub_add_neg(x: Big, y: Big) -> bool { prop_sub_add_neg(x,y) } //------------------------------------------------------------------------------ +#[quickcheck] +fn add_halfp(x: Big) -> bool { + let a = BigInt::add_half_prime_plus_1(x); + let b = x + HALFP_PLUS_1; + a == b +} + +//------------------------------------------------------------------------------ + + diff --git a/src/bn254/test/field.rs b/src/bn254/test/field.rs new file mode 100644 index 0000000..38f92b5 --- /dev/null +++ b/src/bn254/test/field.rs @@ -0,0 +1,194 @@ + +// +// tests for fields (standard representation) +// + +#![allow(unused)] + +use quickcheck::{Arbitrary, Gen}; +use quickcheck_macros::quickcheck; + +use crate::bn254::traits::*; +use crate::bn254::constant::*; +use crate::bn254::bigint::*; +use crate::bn254::field::*; +use crate::bn254::test::properties::*; + +//------------------------------------------------------------------------------ +// some trivialities to get it started + +#[test] +fn zero_is_zero() { assert!( Felt::is_zero( Felt::zero() ) ) } + +#[test] +fn zero_is_not_one() { assert!( !Felt::is_one ( Felt::zero() ) ) } + +#[test] +fn one_is_not_zero() { assert!( !Felt::is_zero( Felt::one () ) ) } + +#[test] +fn one_is_one() { assert!( Felt::is_one ( Felt::one () ) ) } + +//------------------------------------------------------------------------------ +// quickcheck property-based testing + +impl Group for Felt {} +impl Ring for Felt {} +impl Field for Felt {} + +// aux helper for arbitrary +#[derive(Debug, Copy, Clone)] +struct Masked(BigInt256); + +impl Arbitrary for Masked { + fn arbitrary(g: &mut Gen) -> Masked { + let mut xs: [u32; 8] = [0; 8]; + for i in 0..8 { + xs[i] = u32::arbitrary(g); + } + xs[7] = xs[7] & 0x_3FFF_FFFF; + Masked(BigInt::make(xs)) + } +} + +// rejection sampling +impl Arbitrary for Felt { + fn arbitrary(g: &mut Gen) -> Felt { + let mut mx: Masked = Masked::arbitrary(g); + while( mx.0 >= FIELD_PRIME ) { + mx = Masked::arbitrary(g); + } + Felt::unsafe_from_bigint(mx.0) + } +} + +//-------------------------------------- + +#[quickcheck] +fn from_to_bytes_le(x: Felt) -> bool { + let bs: [u8; 32] = Felt::to_le_bytes(x); + Felt::unsafe_from_le_bytes(bs) == x +} + +#[quickcheck] +fn from_to_bytes_be(x: Felt) -> bool { + let bs: [u8; 32] = Felt::to_be_bytes(x); + Felt::unsafe_from_be_bytes(bs) == x +} +//-------------------------------------- + +#[quickcheck] +fn left_additive_unit(x: Felt) -> bool { prop_left_additive_unit(x) } + +#[quickcheck] +fn right_additive_unit(x: Felt) -> bool { prop_right_additive_unit(x) } + +#[quickcheck] +fn sub_zero(x: Felt) -> bool { prop_sub_zero(x) } + +#[quickcheck] +fn zero_sub(x: Felt) -> bool { prop_zero_sub(x) } + +#[quickcheck] +fn add_commutative(x: Felt, y: Felt) -> bool { prop_add_commutative(x,y) } + +#[quickcheck] +fn sub_anticommutative(x: Felt, y: Felt) -> bool { prop_sub_anticommutative(x,y) } + +#[quickcheck] +fn add_associative(x: Felt, y: Felt, z: Felt) -> bool { prop_add_associative(x,y,z) } + +#[quickcheck] +fn neg_involutive(x: Felt) -> bool { prop_neg_involutive(x) } + +#[quickcheck] +fn add_sub(x: Felt, y: Felt) -> bool { prop_add_sub(x,y) } + +#[quickcheck] +fn sub_add(x: Felt, y: Felt) -> bool { prop_sub_add(x,y) } + +#[quickcheck] +fn sub_neg_add(x: Felt, y: Felt) -> bool { prop_sub_neg_add(x,y) } + +#[quickcheck] +fn sub_add_neg(x: Felt, y: Felt) -> bool { prop_sub_add_neg(x,y) } + +//------------------------------------------------------------------------------ + +#[quickcheck] +fn halve_double(x: Felt) -> bool { + let y = Felt::div_by_2(x); + x == y + y +} + +#[quickcheck] +fn double_halve(x: Felt) -> bool { + let z = Felt::div_by_2(x + x); + x == z +} + +#[quickcheck] +fn halve_definition(x: Felt) -> bool { + let a = Felt::div_by_2(x); + let b = x / Felt::from_u32(2); + a == b +} + +//------------------------------------------------------------------------------ + +#[quickcheck] +fn twice(x: Felt) -> bool { prop_twice(x) } + +#[quickcheck] +fn thrice(x: Felt) -> bool { prop_thrice(x) } + +//-------------------------------------- + +#[quickcheck] +fn left_multiplicative_unit(x: Felt) -> bool { prop_left_multiplicative_unit(x) } + +#[quickcheck] +fn right_multiplicative_unit(x: Felt) -> bool { prop_right_multiplicative_unit(x) } + +#[quickcheck] +fn mul_commutative(x: Felt, y: Felt) -> bool { prop_mul_commutative(x,y) } + +#[quickcheck] +fn mul_associative(x: Felt, y: Felt, z: Felt) -> bool { prop_mul_associative(x,y,z) } + +#[quickcheck] +fn mul_neg(x: Felt, y: Felt) -> bool { prop_mul_neg(x,y) } + +#[quickcheck] +fn distributive_add(x: Felt, y: Felt, z: Felt) -> bool { prop_distributive_add(x,y,z) } + +#[quickcheck] +fn distributive_sub(x: Felt, y: Felt, z: Felt) -> bool { prop_distributive_sub(x,y,z) } + +//------------------------------------------------------------------------------ + +#[quickcheck] +fn div_by_1(x: Felt) -> bool { prop_div_by_1(x) } + +#[quickcheck] +fn inv_def(x: Felt) -> bool { prop_inv_def(x) } + +#[quickcheck] +fn mul_left_inverse(x: Felt) -> bool { prop_mul_left_inverse(x) } + +#[quickcheck] +fn mul_right_inverse(x: Felt) -> bool { prop_mul_right_inverse(x) } + +#[quickcheck] +fn mul_div(x: Felt, y: Felt) -> bool { prop_mul_div(x,y) } + +#[quickcheck] +fn div_mul(x: Felt, y: Felt) -> bool { prop_div_mul(x,y) } + +#[quickcheck] +fn distributive_div(x: Felt, y: Felt, z: Felt) -> bool { prop_distributive_div(x,y,z) } + +#[quickcheck] +fn div_div(x: Felt, y: Felt, z: Felt) -> bool { prop_div_div(x,y,z) } + +//------------------------------------------------------------------------------ diff --git a/src/bn254/test/mod.rs b/src/bn254/test/mod.rs index 2734ee1..721bf44 100644 --- a/src/bn254/test/mod.rs +++ b/src/bn254/test/mod.rs @@ -2,5 +2,5 @@ pub mod properties; pub mod bigint; -// pub mod field; +pub mod field; // pub mod mont; \ No newline at end of file diff --git a/src/bn254/test/properties.rs b/src/bn254/test/properties.rs index fe4dc76..ed16d86 100644 --- a/src/bn254/test/properties.rs +++ b/src/bn254/test/properties.rs @@ -1,21 +1,24 @@ // field properties +#![allow(unused)] #![allow(dead_code)] #![allow(non_snake_case)] use std::cmp::{Eq}; use std::ops::{Neg,Add,Sub,Mul,Div}; +use crate::bn254::traits::{Zero,One,Inv}; + //------------------------------------------------------------------------------ // pub trait Group = Copy + Clone + Default + From + Eq + Neg + Add + Sub; // pub trait Ring = Group + Mul; // pub trait Field = Ring + Div; -pub trait Group : Copy + Clone + Default + From + Eq + Neg + Add + Sub {} +pub trait Group : Copy + Clone + Default + From + Eq + Zero + One + Neg + Add + Sub {} pub trait Ring : Group + Mul {} -pub trait Field : Ring + Div {} +pub trait Field : Ring + Div + Inv {} //------------------------------------------------------------------------------ @@ -58,6 +61,10 @@ pub fn prop_sub_anticommutative(x: A, y: A) -> bool { x - y == xneg( y - x ) } +pub fn prop_add_associative(x: A, y: A, z: A) -> bool { + (x + y) + z == x + (y + z) +} + pub fn prop_neg_involutive(x: A) -> bool { xneg( xneg(x) ) == x } @@ -88,7 +95,7 @@ pub fn prop_thrice(x: A) -> bool { x + x + x == x * small::(3) } -//------------------------------------------------------------------------------ +//-------------------------------------- pub fn prop_left_multiplicative_unit(x: A) -> bool { small::(1) * x == x @@ -102,6 +109,10 @@ pub fn prop_mul_commutative(x: A, y: A) -> bool { x * y == y * x } +pub fn prop_mul_associative(x: A, y: A, z: A) -> bool { + (x * y) * z == x * (y * z) +} + pub fn prop_mul_neg(x: A, y: A) -> bool { xneg(x * y) == xneg(x) * y } @@ -115,3 +126,38 @@ pub fn prop_distributive_sub(x: A, y: A, z: A) -> bool { } //------------------------------------------------------------------------------ +// properties involving division + +pub fn prop_div_by_1(x: A) -> bool { + x / A::one() == x +} + +pub fn prop_inv_def(x: A) -> bool { + A::one() / x == A::inv(x) +} + +pub fn prop_mul_left_inverse(x: A) -> bool { + A::inv(x) * x == A::one() +} + +pub fn prop_mul_right_inverse(x: A) -> bool { + x * A::inv(x) == A::one() +} + +pub fn prop_mul_div(x: A, y: A) -> bool { + (x * y) / y == x +} + +pub fn prop_div_mul(x: A, y: A) -> bool { + (x / y) * y == x +} + +pub fn prop_distributive_div(x: A, y: A, z: A) -> bool { + (x + y) / z == (x/z) + (y/z) +} + +pub fn prop_div_div(x: A, y: A, z: A) -> bool { + (x / y) / z == x / (y * z) +} + +//------------------------------------------------------------------------------ diff --git a/src/bn254/traits.rs b/src/bn254/traits.rs index c969e96..ff37c07 100644 --- a/src/bn254/traits.rs +++ b/src/bn254/traits.rs @@ -10,4 +10,10 @@ pub trait Zero { pub trait One { fn one() -> Self; fn is_one(x: Self) -> bool; -} \ No newline at end of file +} + +// yeah, this one too... + +pub trait Inv { + fn inv(x: Self) -> Self; +}