Currently the semantic of coefficientModulus is unclear and a lowering of it faces uncertainty, for example, https://github.com/google/heir/pull/995#issuecomment-2387394895 Also, it lacks a verifier which should conform to the definition in the document. This PR tries to further define the semantic of coefficientModulus and adds a verifier for it. Cc @j2kun for review and suggestions.