double MRG32k3a (void);