pub type TEE_BigIntFMM = u32;