CBMC: Eliminate proof performance workaround in signing

[mkannwischer]

#1015 introduced the following workarounds in signing due to proof performance issues:

mldsa-native/mldsa/src/sign.c

Lines 673 to 681 in 086846b

	/* TODO: Remove this workaround for CBMC performance issues */
	*t = w0->vec[k];
	mld_poly_sub(t, z);
	mld_poly_reduce(t);
	/* Check that subtracting cs2 does not change high bits of w and low bits
	* do not reveal secret information */
	w0_invalid = mld_poly_chknorm(t, MLDSA_GAMMA2 - MLDSA_BETA);
	w0->vec[k] = *t;

mldsa-native/mldsa/src/sign.c

Lines 705 to 708 in 086846b

	/* TODO: Remove this workaround for CBMC performance issues */
	*t = w0->vec[k];
	mld_poly_add(t, z);
	w0->vec[k] = *t;

We should eliminate those workarounds.