Fix translation of const to respect visibility

creusot/src/backend.rs

@@ -80,7 +80,7 @@ impl<'tcx> Why3Generator<'tcx> {
                 let proof_modl = logic::translate_logic(self, def_id);
                 TranslatedItem::Logic { proof_modl }
             }
-            ItemType::Program => {
+            ItemType::Program | ItemType::Constant => {
                 let modl = program::translate_function(self, def_id);
                 TranslatedItem::Program { modl }
             }
@@ -93,8 +93,7 @@ impl<'tcx> Why3Generator<'tcx> {
             | ItemType::Trait
             | ItemType::Type
             | ItemType::AssocTy
-            | ItemType::Impl
-            | ItemType::Constant => return,
+            | ItemType::Impl => return,
         };
         self.functions.push(translated_item);
     }

creusot/src/backend/clone_map.rs

@@ -132,6 +132,10 @@ pub(crate) trait Namer<'tcx> {
         self.dependency(Dependency::PrivateResolve(struct_id, subst)).ident()
     }
 
+    fn opaque_const(&self, name: &str, ty: Ty<'tcx>) -> Ident {
+        self.dependency(Dependency::OpaqueConst(rustc_span::Symbol::intern(name), ty)).ident()
+    }
+
     /// Ideally we'd like to avoid caring about normalization in the backend,
     /// but we still need this for normalizing field types after instantiation.
     /// Also for normalizing RPITs but that seems easier to get rid of if we ever care to.
@@ -625,6 +629,9 @@ fn display_cycle_<'tcx>(
             &PrivateTyInv(def_id, _args) => {
                 write!(f, "private ty inv {}", tcx.def_path_str(def_id))
             }
+            &OpaqueConst(name, ty) => {
+                write!(f, "opaque const {name} {ty}")
+            }
         }?;
         f.write_str(";")?;
         if i < scc.len() - 1 {
@@ -669,20 +676,18 @@ impl Setters {
             Decl::Goal(Goal { name, goal })
         } else {
             let ret = Ident::fresh_local("ret");
-            let prototype = Prototype {
-                name,
-                attrs: vec![],
-                params: [Param::Cont(name::return_(), [].into(), [].into())].into(),
-            };
+            let params = args
+                .into_iter()
+                .map(|(arg, ty)| Param::Term(arg, ty))
+                .chain(std::iter::once(Param::Cont(name::return_(), [].into(), [].into())))
+                .collect::<Box<[_]>>();
+            let prototype = Prototype { name, attrs: vec![], params };
             let body = self.call_setters(Expr::var(ret)).black_box();
             let body = requires
                 .into_iter()
                 .rfold(body, |body, pre| Expr::Assert(pre.boxed(), body.boxed()));
             let ret_defn = Defn {
-                prototype: Prototype::new(
-                    ret,
-                    args.into_iter().map(|(arg, ty)| Param::Term(arg, ty)).collect::<Box<[_]>>(),
-                ),
+                prototype: Prototype::new(ret, []),
                 body: Expr::Assert(ensures.boxed(), Expr::var(name::return_()).black_box().boxed()),
             };
             let body = Expr::Defn(body.boxed(), false, [ret_defn].into());

creusot/src/backend/clone_map/elaborator.rs

@@ -640,6 +640,14 @@ impl<'a, 'ctx, 'tcx> Expander<'a, 'ctx, 'tcx> {
                 };
                 vec![Decl::predicate(sig, None)]
             }
+            Dependency::OpaqueConst(_, ty) => {
+                let name = self.namer.dependency(dep).ident();
+                let ty = translate_ty(ctx, self.namer, self.root_span, ty);
+                vec![Decl::LogicDecl(LogicDecl {
+                    kind: Some(DeclKind::Constant),
+                    sig: Signature::constant(name, ty),
+                })]
+            }
         };
 
         self.dep_bodies.insert(dep, decls);

creusot/src/backend/dependency.rs

@@ -29,6 +29,8 @@ pub(crate) enum Dependency<'tcx> {
     PrivateFields(DefId, GenericArgsRef<'tcx>),
     PrivateResolve(DefId, GenericArgsRef<'tcx>),
     PrivateTyInv(DefId, GenericArgsRef<'tcx>),
+    /// An opaque constant from trying to use a non-visible constructor.
+    OpaqueConst(Symbol, Ty<'tcx>),
 }
 
 impl<'tcx> Dependency<'tcx> {
@@ -120,6 +122,7 @@ impl<'tcx> Dependency<'tcx> {
             Dependency::PreMod(_) => None,
             Dependency::PrivateResolve(..) => Some(Symbol::intern("resolve__private")),
             Dependency::PrivateTyInv(..) => Some(Symbol::intern("inv__private")),
+            Dependency::OpaqueConst(name, _) => Some(name),
         }
     }
 }

creusot/src/backend/program.rs

@@ -62,11 +62,27 @@ pub(crate) fn translate_function<'tcx>(
     ctx: &Why3Generator<'tcx>,
     def_id: DefId,
 ) -> Option<FileModule> {
+    if !def_id.is_local() || !ctx.has_body(def_id) || is_trusted_item(ctx.tcx, def_id) {
+        return None;
+    }
+
     let names = Dependencies::new(ctx, def_id);
     let namespace_ty = names.namespace_ty();
 
-    if !def_id.is_local() || !ctx.has_body(def_id) || is_trusted_item(ctx.tcx, def_id) {
-        return None;
+    use DefKind::*;
+    match ctx.tcx().def_kind(def_id) {
+        AssocConst { .. } | Const { .. } => {
+            // Translate const only if there is a non-trivial invariant or postcondition
+            let sig = ctx.sig(def_id);
+            let span = ctx.tcx().def_span(def_id);
+            if is_tyinv_trivial(&ctx.ctx, def_id, names.typing_env(), sig.output, span)
+                && !sig.contract.has_user_contract
+            {
+                return None;
+            }
+        }
+        InlineConst { .. } => return None,
+        _ => {}
     }
 
     let name = names.source_ident();

creusot/src/backend/term.rs

@@ -4,8 +4,8 @@ use crate::{
         program::{PtrCastKind, ptr_cast_kind},
         projections::{borrow_generated_id, projections_term},
         ty::{
-            constructor, floatty_to_prelude, ity_to_prelude, translate_ty, ty_to_prelude,
-            uty_to_prelude,
+            classify_adt, constructor, floatty_to_prelude, ity_to_prelude, translate_ty,
+            ty_to_prelude, uty_to_prelude,
         },
     },
     contracts_items::{is_builtin_ascription, is_new_namespace},
@@ -297,6 +297,27 @@ impl<'tcx, N: Namer<'tcx>> Lower<'_, 'tcx, N> {
             }
             TermKind::Constructor { variant, fields, .. } => {
                 let TyKind::Adt(adt, subst) = term.ty.kind() else { unreachable!() };
+                use crate::backend::ty::AdtKind::*;
+                if let Opaque { .. } | Struct { partially_opaque: true } =
+                    classify_adt(self.ctx, self.names.source_id(), *adt, subst)
+                {
+                    self.ctx
+                        .struct_warn(
+                            term.span,
+                            format!(
+                                "encountered non-visible constructor {}",
+                                self.tcx().def_path_str(adt.did())
+                            ),
+                        )
+                        .with_span_note(
+                            self.tcx().def_span(self.names.source_id()),
+                            "during the translation of this function",
+                        )
+                        .emit();
+                    let name = format!("opaque_{}", self.tcx().item_name(adt.did()));
+                    let ident = self.names.opaque_const(&name, term.ty);
+                    return Exp::var(ident);
+                }
                 let fields = fields.into_iter().map(|f| self.lower_term(f)).collect();
                 constructor(self.names, fields, adt.variant(*variant).def_id, subst)
             }

creusot/src/contracts_items/attributes.rs

@@ -74,6 +74,7 @@ attribute_functions! {
     [creusot::clause::check_ghost::trusted]     => is_check_ghost_trusted
     [creusot::bitwise]                          => is_bitwise
     [creusot::builtin_ascription]               => is_builtin_ascription
+    [creusot::no_simp]                          => is_no_simp
 }
 
 pub(crate) fn get_invariant_expl(tcx: TyCtxt, def_id: DefId) -> Option<String> {

creusot/src/ctx.rs

@@ -147,6 +147,10 @@ pub trait HasTyCtxt<'tcx> {
         self.tcx().dcx().span_warn(span, msg)
     }
 
+    fn struct_warn(&self, span: Span, msg: impl Into<DiagMessage>) -> Diag<'tcx, ()> {
+        self.tcx().dcx().struct_span_warn(span, msg)
+    }
+
     fn span_bug(&self, span: Span, msg: impl Into<String>) -> ! {
         self.tcx().dcx().span_bug(span, msg.into())
     }
@@ -424,7 +428,7 @@ impl<'tcx> TranslationCtx<'tcx> {
     /// set as their *visibility*.
     fn mk_opacity(&self, item: DefId) -> Opacity {
         match self.item_type(item) {
-            ItemType::Constant => Opacity::Transparent(Visibility::Public),
+            ItemType::Constant => Opacity::Transparent(self.visibility(item)),
             ItemType::Logic { .. } if is_opaque(self.tcx, item) => Opacity::Opaque,
             ItemType::Logic { .. } => {
                 let vis = opacity_witness_name(self.tcx, item).map_or_else(

creusot/src/translation/constant.rs

@@ -1,4 +1,5 @@
 use crate::{
+    contracts_items::is_no_simp,
     ctx::{HasTyCtxt as _, TranslationCtx},
     translation::{fmir::Operand, pearlite::Literal, traits::TraitResolved},
 };
@@ -130,6 +131,16 @@ fn try_scalar_to_literal<'tcx>(
 /// Translate constant with a simple body: it can be reduced to a value expressible in
 /// the logical fragment of Why3, or its body is just a variable.
 /// `None` if it does not match these cases.
+///
+/// We try to normalize consts by default because there are really silly
+/// definitions out there that are best hidden from users:
+///
+/// ```
+/// const MAX: usize = !0;
+///
+/// const MIN: isize = !isize::MAX
+/// const MAX: isize = (usize::MAX >> 1) as isize;
+/// ```
 pub fn try_const_to_term<'tcx>(
     def_id: DefId,
     subst: ty::GenericArgsRef<'tcx>,
@@ -139,14 +150,16 @@ pub fn try_const_to_term<'tcx>(
     if ctx.def_kind(def_id) == DefKind::ConstParam {
         return None;
     }
-    let ty = ctx.type_of(def_id).instantiate(ctx.tcx, subst);
-    let ty = ctx.tcx.normalize_erasing_regions(typing_env, ty);
-    let span = ctx.def_span(def_id);
-    let uneval = ty::UnevaluatedConst::new(def_id, subst);
-    match ctx.const_eval_resolve_for_typeck(typing_env, uneval, span) {
-        Ok(Ok(val)) => valtree_to_term(val, ctx, ty, typing_env, span),
-        _ => try_const_synonym(def_id, subst, ctx, typing_env),
+    if !is_no_simp(ctx.tcx, def_id) {
+        let ty = ctx.type_of(def_id).instantiate(ctx.tcx, subst);
+        let ty = ctx.tcx.normalize_erasing_regions(typing_env, ty);
+        let span = ctx.def_span(def_id);
+        let uneval = ty::UnevaluatedConst::new(def_id, subst);
+        if let Ok(Ok(val)) = ctx.const_eval_resolve_for_typeck(typing_env, uneval, span) {
+            return valtree_to_term(val, ctx, ty, typing_env, span);
+        }
     }
+    try_const_synonym(def_id, subst, ctx, typing_env)
 }
 
 pub(crate) fn valtree_to_term<'tcx>(

creusot/src/validate/opacity.rs

@@ -23,6 +23,12 @@ struct OpacityVisitor<'a, 'tcx> {
 }
 
 impl OpacityVisitor<'_, '_> {
+    fn assert_visible_enough(&self, id: DefId, span: Span) {
+        if !self.is_visible_enough(id) {
+            self.error(id, span)
+        }
+    }
+
     fn is_visible_enough(&self, id: DefId) -> bool {
         let Opacity::Transparent(op) = self.opacity else { return true };
         self.ctx.visibility(id).is_at_least(op, self.ctx.tcx)
@@ -49,33 +55,23 @@ impl<'tcx> TermVisitor<'tcx> for OpacityVisitor<'_, 'tcx> {
                 if matches!(self.ctx.def_kind(id), DefKind::ConstParam) {
                     return;
                 }
-                if !self.is_visible_enough(id) {
-                    self.error(id, term.span)
-                }
+                self.assert_visible_enough(id, term.span);
             }
             &TermKind::Call { id, .. } => {
-                if !self.is_visible_enough(id) {
-                    self.error(id, term.span)
-                }
+                self.assert_visible_enough(id, term.span);
             }
             &TermKind::Constructor { variant, .. } => {
                 if let Some(adt) = term.ty.ty_adt_def() {
-                    if !self.is_visible_enough(adt.did()) {
-                        self.error(adt.did(), term.span);
-                    }
+                    self.assert_visible_enough(adt.did(), term.span);
                     for fld in &adt.variant(variant).fields {
-                        if !self.is_visible_enough(fld.did) {
-                            self.error(fld.did, term.span);
-                        }
+                        self.assert_visible_enough(fld.did, term.span);
                     }
                 }
             }
             &TermKind::Projection { idx, ref lhs } => {
                 if let Some(adt) = lhs.ty.ty_adt_def() {
                     let fdid = adt.non_enum_variant().fields[idx].did;
-                    if !self.is_visible_enough(fdid) {
-                        self.error(fdid, term.span);
-                    }
+                    self.assert_visible_enough(fdid, term.span);
                 }
             }
             &TermKind::Reborrow { ref projections, ref inner } => {
@@ -89,9 +85,7 @@ impl<'tcx> TermVisitor<'tcx> for OpacityVisitor<'_, 'tcx> {
                                 && adt.is_struct()
                             {
                                 let fdid = adt.non_enum_variant().fields[*field_idx].did;
-                                if !self.is_visible_enough(fdid) {
-                                    self.error(fdid, term.span);
-                                }
+                                self.assert_visible_enough(fdid, term.span);
                             }
                         }
                         ProjectionElem::Deref | ProjectionElem::Index(_) => (),
@@ -111,9 +105,7 @@ impl<'tcx> TermVisitor<'tcx> for OpacityVisitor<'_, 'tcx> {
                 let fields_def = &pat.ty.ty_adt_def().unwrap().variants()[*variant_idx].fields;
                 for (fld, _) in patterns {
                     let fdid = fields_def[*fld].did;
-                    if !self.is_visible_enough(fdid) {
-                        self.error(fdid, pat.span);
-                    }
+                    self.assert_visible_enough(fdid, pat.span);
                 }
             }
             _ => (),
@@ -122,8 +114,10 @@ impl<'tcx> TermVisitor<'tcx> for OpacityVisitor<'_, 'tcx> {
     }
 }
 
-/// Forbid use of opaque type constructors and fields
-struct NoOpaqueTypeAccess<'a, 'tcx> {
+/// Opacity check in THIR. Check two things:
+/// 1. Forbid use of opaque type constructors and fields (in logic and non-trusted program definitions)
+/// 2. In consts, forbid use of less visible functions, constructors, and fields.
+struct ThirOpacityVisitor<'a, 'tcx> {
     ctx: &'a TranslationCtx<'tcx>,
     thir: &'a Thir<'tcx>,
 }
@@ -147,7 +141,7 @@ impl TranslationCtx<'_> {
     }
 }
 
-impl<'thir, 'tcx> Visitor<'thir, 'tcx> for NoOpaqueTypeAccess<'thir, 'tcx> {
+impl<'thir, 'tcx> Visitor<'thir, 'tcx> for ThirOpacityVisitor<'thir, 'tcx> {
     fn thir(&self) -> &'thir Thir<'tcx> {
         self.thir
     }
@@ -186,7 +180,7 @@ pub(crate) fn validate_opacity<'tcx>(ctx: &TranslationCtx<'tcx>, item: DefId) {
     if is_logic || !is_trusted(ctx.tcx, item) {
         let (thir, expr) = ctx.thir_body(item.expect_local());
         let thir = &thir.borrow();
-        NoOpaqueTypeAccess { ctx, thir }.visit_expr(&thir[expr]);
+        ThirOpacityVisitor { ctx, thir }.visit_expr(&thir[expr]);
     }
     if is_logic && !is_opaque(ctx.tcx, item) {
         let Some(Scoped(_, term)) = ctx.term(item) else { return };