Keen. Why M1 and M2? Eyeballing it, they seem like they should instead be testing the sign of v? Also because I think it would be good to be testing/constraining the sign of v. As in what if / how to disallow X<=0 && v>0?
prval () = $UN.prop_assert{false}()