[New Project] MuGraph Verifier without Lax Constraints

[wmdi]

Currently, Mirage requires the input subprogram to satisfy the Lax Constraint (see our paper for the detailed description). The main issue of this constraint is that Mirage does not support many widely-used nonlinear operators like ReLU. The Lax constraint is only required by the probabilistic verifier to ensure the precise of the random tests. We want a verification method that does not constrain the input subprogram so that Mirage can support all kinds of operators.