CBMC: Revisit poly_chknorm/poly_chknorm_native contract

[willieyz]

• Related: CBMC: Add proofs for native backend functions #768
• During PR CBMC: Add proofs for native backend functions #768, we found that the cbmc proof for mld_poly_chknorm_native is rather ugly - we should consider simplifying that vastly, according to CBMC: Add proofs for native backend functions #768 (review)