Reomve ignore_type_invariant

voidc · voidc · commit 17b0aff87bb6 · 2023-06-14T13:32:10.000+02:00
diff --git a/creusot-contracts/src/invariant.rs b/creusot-contracts/src/invariant.rs
@@ -24,7 +24,6 @@ pub trait Invariant {
 impl<'a, T: Invariant + ?Sized> Invariant for &'a T {
     #[predicate]
     #[open]
-    #[creusot::ignore_type_invariant = "maybe"]
     fn invariant(self) -> bool {
         pearlite! { (*self).invariant() }
     }
@@ -33,7 +32,6 @@ impl<'a, T: Invariant + ?Sized> Invariant for &'a T {
 impl<'a, T: Invariant + ?Sized> Invariant for &'a mut T {
     #[predicate]
     #[open]
-    #[creusot::ignore_type_invariant = "maybe"]
     fn invariant(self) -> bool {
         pearlite! { (*self).invariant() }
     }
@@ -42,7 +40,6 @@ impl<'a, T: Invariant + ?Sized> Invariant for &'a mut T {
 impl<T: Invariant + ?Sized> Invariant for Box<T> {
     #[predicate]
     #[open]
-    #[creusot::ignore_type_invariant = "maybe"]
     fn invariant(self) -> bool {
         pearlite! { (*self).invariant() }
     }
@@ -51,7 +48,6 @@ impl<T: Invariant + ?Sized> Invariant for Box<T> {
 impl<T: Invariant, U: Invariant> Invariant for (T, U) {
     #[predicate]
     #[open]
-    #[creusot::ignore_type_invariant = "maybe"]
     fn invariant(self) -> bool {
         pearlite! { self.0.invariant() && self.1.invariant() }
     }
@@ -60,7 +56,6 @@ impl<T: Invariant, U: Invariant> Invariant for (T, U) {
 impl<T: Invariant> Invariant for Option<T> {
     #[predicate]
     #[open]
-    #[creusot::ignore_type_invariant = "maybe"]
     fn invariant(self) -> bool {
         pearlite! {
             match self {
diff --git a/creusot-contracts/src/std/iter/map_inv.rs b/creusot-contracts/src/std/iter/map_inv.rs
@@ -65,7 +65,6 @@ impl<I: Iterator, B, F: FnMut(I::Item, Ghost<Seq<I::Item>>) -> B> Invariant
     // Should not quantify over self or the `invariant` cannot be made into a type invariant
     #[open(self)]
     #[predicate]
-    #[creusot::ignore_type_invariant]
     fn invariant(self) -> bool {
         pearlite! {
             Self::reinitialize() &&
@@ -108,6 +107,7 @@ impl<I: Iterator, B, F: FnMut(I::Item, Ghost<Seq<I::Item>>) -> B> ::std::iter::I
 impl<I: Iterator, B, F: FnMut(I::Item, Ghost<Seq<I::Item>>) -> B> MapInv<I, I::Item, F> {
     #[open]
     #[predicate]
+    #[creusot::open_inv]
     pub fn next_precondition(self) -> bool {
         pearlite! {
             forall<e: I::Item, i: I>
@@ -131,6 +131,7 @@ impl<I: Iterator, B, F: FnMut(I::Item, Ghost<Seq<I::Item>>) -> B> MapInv<I, I::I
     #[open(self)]
     #[predicate]
     #[ensures(self.produced.inner() == Seq::EMPTY ==> result == Self::preservation(self.iter, self.func))]
+    #[creusot::open_inv]
     pub fn preservation_inv(self) -> bool {
         pearlite! {
             forall<s: Seq<I::Item>, e1: I::Item, e2: I::Item, f: &mut F, b: B, i: I>
diff --git a/creusot-contracts/src/std/slice.rs b/creusot-contracts/src/std/slice.rs
@@ -279,7 +279,6 @@ extern_spec! {
         fn iter(&self) -> Iter<'_, T>;
 
         #[ensures(result@ == self)]
-        #[ensures(result.invariant())]
         fn iter_mut(&mut self) -> IterMut<'_, T>;
 
         #[ensures(result == None ==> self@.len() == 0)]
@@ -400,6 +399,7 @@ impl<'a, T> ShallowModel for IterMut<'a, T> {
     #[open(self)]
     #[trusted]
     #[ensures((^result)@.len() == (*result)@.len())]
+    #[creusot::open_inv]
     fn shallow_model(self) -> Self::ShallowModelTy {
         absurd
     }
@@ -417,7 +417,6 @@ impl<'a, T> Resolve for IterMut<'a, T> {
 impl<'a, T> Invariant for IterMut<'a, T> {
     #[predicate]
     #[open]
-    #[creusot::ignore_type_invariant]
     fn invariant(self) -> bool {
         // Property that is always true but we must carry around..
         pearlite! { (^self@)@.len() == (*self@)@.len() }
diff --git a/creusot/src/ctx.rs b/creusot/src/ctx.rs
@@ -29,10 +29,7 @@ use rustc_infer::traits::{Obligation, ObligationCause};
 use rustc_middle::{
     mir::{Body, Promoted},
     thir,
-    ty::{
-        subst::{GenericArgKind, InternalSubsts},
-        GenericArg, ParamEnv, SubstsRef, Ty, TyCtxt, Visibility,
-    },
+    ty::{subst::InternalSubsts, GenericArg, ParamEnv, SubstsRef, Ty, TyCtxt, Visibility},
 };
 use rustc_span::{RealFileName, Span, Symbol, DUMMY_SP};
 use rustc_trait_selection::traits::SelectionContext;
@@ -225,41 +222,7 @@ impl<'tcx, 'sess> TranslationCtx<'tcx> {
             return None;
         }
 
-        match util::ignore_type_invariant(self.tcx, inv.0) {
-            util::TypeInvariantAttr::None => return Some(inv),
-            util::TypeInvariantAttr::AlwaysIgnore => return None,
-            util::TypeInvariantAttr::MaybeIgnore => {}
-        }
-
-        let mut walker = ty.walk();
-        walker.next(); // skip root type
-        while let Some(arg) = walker.next() {
-            if !matches!(arg.unpack(), GenericArgKind::Type(_)) {
-                walker.skip_current_subtree();
-                continue;
-            }
-
-            let substs = self.mk_substs(&[arg]);
-            let Some(arg_inv) = traits::resolve_opt(self.tcx, param_env, trait_did, substs) else {
-                walker.skip_current_subtree();
-                continue;
-            };
-
-            if arg_inv.0 == trait_did
-                && !traits::still_specializable(self.tcx, param_env, arg_inv.0, arg_inv.1)
-            {
-                walker.skip_current_subtree();
-                continue;
-            }
-
-            match util::ignore_type_invariant(self.tcx, arg_inv.0) {
-                util::TypeInvariantAttr::None => return Some(inv),
-                util::TypeInvariantAttr::AlwaysIgnore => walker.skip_current_subtree(),
-                util::TypeInvariantAttr::MaybeIgnore => {}
-            }
-        }
-
-        None
+        Some(inv)
     }
 
     pub(crate) fn crash_and_error(&self, span: Span, msg: &str) -> ! {
diff --git a/creusot/src/util.rs b/creusot/src/util.rs
@@ -118,24 +118,6 @@ pub(crate) fn opacity_witness_name(tcx: TyCtxt, def_id: DefId) -> Option<Symbol>
     })
 }
 
-pub(crate) enum TypeInvariantAttr {
-    None,
-    MaybeIgnore,
-    AlwaysIgnore,
-}
-
-pub(crate) fn ignore_type_invariant(tcx: TyCtxt, def_id: DefId) -> TypeInvariantAttr {
-    match get_attr(tcx.get_attrs_unchecked(def_id), &["creusot", "ignore_type_invariant"]) {
-        None => TypeInvariantAttr::None,
-        Some(AttrItem { args: AttrArgs::Eq(_, AttrArgsEq::Hir(v)), .. })
-            if v.symbol.as_str() == "maybe" =>
-        {
-            TypeInvariantAttr::MaybeIgnore
-        }
-        _ => TypeInvariantAttr::AlwaysIgnore,
-    }
-}
-
 pub(crate) fn why3_attrs(tcx: TyCtxt, def_id: DefId) -> Vec<why3::declaration::Attribute> {
     let matches = get_attrs(tcx.get_attrs_unchecked(def_id), &["why3", "attr"]);
     matches
@@ -494,8 +476,9 @@ fn elaborate_type_invariants<'tcx>(
                 let arg = Term { ty: *ty, span: *span, kind: TermKind::Var(*name) };
                 let arg =
                     Term { ty: inner, span: *span, kind: TermKind::Fin { term: Box::new(arg) } };
-                let term =
-                    pearlite::type_invariant_term_with_arg(ctx, def_id, arg, *span, inner).unwrap();
+                // FIXME: why can this be none?
+                let Some(term) =
+                    pearlite::type_invariant_term_with_arg(ctx, def_id, arg, *span, inner) else {continue; };
                 pre_sig.contract.ensures.push(term);
             }
 
diff --git a/creusot/tests/should_succeed/iterators/05_map.rs b/creusot/tests/should_succeed/iterators/05_map.rs
@@ -24,15 +24,11 @@ impl<I: Iterator, B, F: FnMut(I::Item) -> B> Iterator for Map<I, F> {
 
     #[law]
     #[open]
-    #[requires(a.invariant())]
     #[ensures(a.produces(Seq::EMPTY, a))]
     fn produces_refl(a: Self) {}
 
     #[law]
     #[open]
-    #[requires(a.invariant())]
-    #[requires(b.invariant())]
-    #[requires(c.invariant())]
     #[requires(a.produces(ab, b))]
     #[requires(b.produces(bc, c))]
     #[ensures(a.produces(ab.concat(bc), c))]
@@ -76,14 +72,14 @@ impl<I: Iterator, B, F: FnMut(I::Item) -> B> Iterator for Map<I, F> {
 
 impl<I: Iterator, B, F: FnMut(I::Item) -> B> Map<I, F> {
     #[predicate]
-    fn next_precondition(self) -> bool {
+    fn next_precondition(#[creusot::open_inv] self) -> bool {
         pearlite! {
-            forall<e: I::Item, i: I> i.invariant() ==>
-                self.iter.produces(Seq::singleton(e), i) ==> self.func.precondition((e,))
+            forall<e: I::Item, i: I> self.iter.produces(Seq::singleton(e), i) ==> self.func.precondition((e,))
         }
     }
 
     #[predicate]
+    #[creusot::open_inv]
     fn reinitialize() -> bool {
         pearlite! {
             forall<reset : &mut Map<I, F>> (^reset).iter.invariant() ==>
@@ -93,10 +89,9 @@ impl<I: Iterator, B, F: FnMut(I::Item) -> B> Map<I, F> {
 
     #[predicate]
     #[ensures(result == Self::preservation(self.iter, self.func))]
-    fn preservation_inv(self) -> bool {
+    fn preservation_inv(#[creusot::open_inv] self) -> bool {
         pearlite! {
             forall<s: Seq<I::Item>, e1: I::Item, e2: I::Item, f: &mut F, b: B, i: I>
-                i.invariant() ==>
                 self.func.unnest(*f) ==>
                 self.iter.produces(s.push(e1).push(e2), i) ==>
                 (*f).precondition((e1,)) ==>
@@ -109,7 +104,6 @@ impl<I: Iterator, B, F: FnMut(I::Item) -> B> Map<I, F> {
     fn preservation(iter: I, func: F) -> bool {
         pearlite! {
             forall<s: Seq<I::Item>, e1: I::Item, e2: I::Item, f: &mut F, b: B, i: I>
-                i.invariant() ==>
                 func.unnest(*f) ==>
                 iter.produces(s.push(e1).push(e2), i) ==>
                 (*f).precondition((e1,)) ==>
@@ -119,15 +113,18 @@ impl<I: Iterator, B, F: FnMut(I::Item) -> B> Map<I, F> {
     }
 
     #[logic]
-    #[requires(self.invariant())]
     #[requires(self.produces_one(e, other))]
     #[requires(other.iter.invariant())]
     #[ensures(other.invariant())]
-    fn produces_one_invariant(self, e: B, other: Self) {}
+    fn produces_one_invariant(self, e: B, #[creusot::open_inv] other: Self) {}
 
     #[predicate]
     #[ensures(result == self.produces(Seq::singleton(visited), succ))]
-    fn produces_one(self, visited: B, succ: Self) -> bool {
+    fn produces_one(
+        #[creusot::open_inv] self,
+        visited: B,
+        #[creusot::open_inv] succ: Self,
+    ) -> bool {
         pearlite! {
             exists<f: &mut F> *f == self.func && ^f == succ.func
             && { exists<e : I::Item> self.iter.produces(Seq::singleton(e), succ.iter)
@@ -140,7 +137,6 @@ impl<I: Iterator, B, F: FnMut(I::Item) -> B> Map<I, F> {
 impl<I: Iterator, B, F: FnMut(I::Item) -> B> Invariant for Map<I, F> {
     // Should not quantify over self or the `invariant` cannot be made into a type invariant
     #[predicate]
-    #[creusot::ignore_type_invariant]
     #[open(self)]
     fn invariant(self) -> bool {
         pearlite! {
@@ -152,11 +148,9 @@ impl<I: Iterator, B, F: FnMut(I::Item) -> B> Invariant for Map<I, F> {
     }
 }
 
-#[requires(forall<e : I::Item, i2 : I> i2.invariant() ==> iter.produces(Seq::singleton(e), i2) ==> func.precondition((e,)))]
+#[requires(forall<e : I::Item, i2 : I> iter.produces(Seq::singleton(e), i2) ==> func.precondition((e,)))]
 #[requires(Map::<I, F>::reinitialize())]
-#[requires(iter.invariant())]
 #[requires(Map::<I, F>::preservation(iter, func))]
-#[ensures(result.invariant())]
 #[ensures(result == Map { iter, func })]
 pub fn map<I: Iterator, B, F: FnMut(I::Item) -> B>(iter: I, func: F) -> Map<I, F> {
     Map { iter, func }
diff --git a/creusot/tests/should_succeed/iterators/06_map_precond.rs b/creusot/tests/should_succeed/iterators/06_map_precond.rs
diff --git a/creusot/tests/should_succeed/type_invariants/type_invariants.rs b/creusot/tests/should_succeed/type_invariants/type_invariants.rs
