Fix translation of const to respect visibility

[Lysxia]

Close #2009

• add #[ensures] for consts
• add an opacity check for consts (my plan is that the body of a const is as visible as the const itself unless it has an #[ensures])
• add an attribute to force the evaluation of consts. Currently this is the default and this current PR adds an attribute to disable it as a stop-gap, but it's a bad default because it breaks opacity. We need to keep the ability to evaluate consts because MIN and MAX for machine integers are defined using bitwise operations (isize::MIN = !isize::MAX, isize::MAX = (usize::MAX >> 1) as isize, usize::MAX = !0), and we don't want to expose these definitions to users.
• Translate consts to verify their type invariants.
• In the translation of terms, when we encounter a non-visible constructor (due to an evaluated const), replace it with an opaque constant and emit a warning.