add an assert_valid method to Visit

Author: nikomatsakis

crates/formality-macros/src/visit.rs

@@ -11,6 +11,8 @@ pub(crate) fn derive_visit(mut s: synstructure::Structure) -> TokenStream {
 
     let size_body = s.each(|field| quote!(__sum += Visit::size(#field)));
 
+    let assert_valid_body = s.each(|field| quote!(Visit::assert_valid(#field)));
+
     // s.add_bounds(synstructure::AddBounds::None);
     s.gen_impl(quote! {
         use crate::derive_links::{Visit, Variable};
@@ -32,6 +34,12 @@ pub(crate) fn derive_visit(mut s: synstructure::Structure) -> TokenStream {
                 }
                 __sum
             }
+
+            fn assert_valid(&self) {
+                match self {
+                    #assert_valid_body
+                }
+            }
         }
     })
 }

crates/formality-prove/src/prove/constraints.rs

@@ -1,11 +1,9 @@
-use contracts::requires;
 use formality_types::{
     cast::Upcast,
     cast_impl,
-    collections::Set,
     derive_links::UpcastFrom,
     fold::Fold,
-    grammar::{AtomicRelation, Binder, InferenceVar, Parameter, Substitution, Variable},
+    grammar::{Binder, InferenceVar, Parameter, Substitution, Variable},
     visit::Visit,
 };
 
@@ -40,31 +38,10 @@ impl Default for Constraints {
 }
 
 impl Constraints {
-    /// Check type invariant:
-    ///
-    /// * Domain of substitution is disjoint from range: meaning we don't have
-    ///   a substitution like `[X := Vec<Y>, Y := u32]`, but instead
-    ///   `[X := Vec<u32>, Y := u32]`
-    pub fn is_valid(&self) -> bool {
-        let domain = self.substitution.domain();
-        let range = self.substitution.range();
-        range
-            .iter()
-            .all(|t| domain.iter().all(|&v| !occurs_in(v, t)))
-    }
-
     pub fn substitution(&self) -> &Substitution {
         &self.substitution
     }
 
-    #[requires(self.is_valid())]
-    pub fn as_relations(&self) -> Set<AtomicRelation> {
-        self.substitution
-            .iter()
-            .map(|(v, p)| AtomicRelation::eq(v, p))
-            .collect()
-    }
-
     pub fn ambiguous(self) -> Constraints {
         Self {
             known_true: false,
@@ -79,10 +56,10 @@ pub fn merge_constraints(
     c1: Binder<Constraints>,
 ) -> Binder<Constraints> {
     let c0: Constraints = c0.upcast();
-    assert!(c0.is_valid());
+    c0.assert_valid();
 
     let (c1_bound_vars, c1) = c1.open();
-    assert!(c1.is_valid());
+    c1.assert_valid();
 
     assert!(c0
         .substitution
@@ -125,10 +102,7 @@ impl Fold for Constraints {
         };
 
         // not all substitutions preserve the constraint set invariant
-        assert!(
-            c.is_valid(),
-            "folding `{self:?}` yielded invalid constraint set `{c:?}`"
-        );
+        c.assert_valid();
 
         c
     }
@@ -150,6 +124,14 @@ impl Visit for Constraints {
         } = self;
         substitution.size()
     }
+
+    fn assert_valid(&self) {
+        let domain = self.substitution.domain();
+        let range = self.substitution.range();
+        range
+            .iter()
+            .for_each(|t| assert!(domain.iter().all(|&v| !occurs_in(v, t))));
+    }
 }
 
 pub fn occurs_in(v: impl Upcast<Variable>, t: &impl Visit) -> bool {

crates/formality-prove/src/prove/prove_after.rs

@@ -5,7 +5,7 @@ use formality_types::{
 
 use crate::{
     program::Program,
-    prove::{constraints::merge_constraints, prove, prove_wc_list::prove_wc_list},
+    prove::{constraints::merge_constraints, prove},
 };
 
 use super::{constraints::Constraints, subst::existential_substitution};

crates/formality-prove/src/prove/prove_apr.rs

@@ -11,7 +11,6 @@ use crate::{
         prove_after::prove_after,
         prove_apr_via::prove_apr_via,
         prove_eq::{all_eq, prove_ty_eq},
-        prove_wc_list::prove_wc_list,
         subst::existential_substitution,
     },
 };

crates/formality-prove/src/prove/prove_eq.rs

@@ -17,7 +17,7 @@ use crate::{
     },
 };
 
-use super::{constraints::Constraints, prove_wc_list::prove_wc_list};
+use super::constraints::Constraints;
 
 /// Goal(s) to prove `a` and `b` are equal (they must have equal length)
 pub fn all_eq(a: impl Upcast<Vec<Parameter>>, b: impl Upcast<Vec<Parameter>>) -> Wcs {

crates/formality-rust/src/trait_binder.rs

@@ -52,6 +52,10 @@ where
     fn size(&self) -> usize {
         self.explicit_binder.size()
     }
+
+    fn assert_valid(&self) {
+        self.explicit_binder.assert_valid()
+    }
 }
 
 impl<T> Fold for TraitBinder<T>

crates/formality-types/src/grammar/binder.rs

@@ -177,6 +177,10 @@ impl<T: Visit> Visit for Binder<T> {
     fn size(&self) -> usize {
         self.term.size()
     }
+
+    fn assert_valid(&self) {
+        self.term.assert_valid();
+    }
 }
 
 impl<T: Fold> Fold for Binder<T> {

crates/formality-types/src/grammar/ids.rs

@@ -36,6 +36,8 @@ macro_rules! id {
                 fn size(&self) -> usize {
                     1
                 }
+
+                fn assert_valid(&self) {}
             }
 
             impl Fold for $n {

crates/formality-types/src/grammar/ty.rs

@@ -147,6 +147,8 @@ impl Visit for InferenceVar {
     fn size(&self) -> usize {
         1
     }
+
+    fn assert_valid(&self) {}
 }
 
 #[term((rigid $name $*parameters))]
@@ -421,6 +423,13 @@ impl Visit for LtData {
             LtData::Static => 1,
         }
     }
+
+    fn assert_valid(&self) {
+        match self {
+            LtData::Variable(v) => v.assert_valid(),
+            LtData::Static => (),
+        }
+    }
 }
 
 #[derive(Copy, Clone, PartialEq, Eq, PartialOrd, Ord, Hash)]
@@ -519,6 +528,8 @@ impl Visit for Variable {
     fn size(&self) -> usize {
         1
     }
+
+    fn assert_valid(&self) {}
 }
 
 impl UpcastFrom<Variable> for Parameter {
@@ -704,6 +715,10 @@ impl Visit for Substitution {
     fn size(&self) -> usize {
         self.range().iter().map(|r| r.size()).sum()
     }
+
+    fn assert_valid(&self) {
+        self.range().assert_valid()
+    }
 }
 
 /// A substitution that is only between variables.

crates/formality-types/src/visit.rs

@@ -21,6 +21,11 @@ pub trait Visit: Sized {
     /// Used to determine overflow.
     fn size(&self) -> usize;
 
+    /// Asserts various validity constraints and panics if they are not held.
+    /// These validition constraints should never fail unless there is a bug in our logic.
+    /// This is to aid with fuzzing and bug detection.
+    fn assert_valid(&self);
+
     /// True if this term references only placeholder variables.
     /// This means that it contains no inference variables.
     /// If this is a goal, then when we prove it true, we don't expect any substitution.
@@ -57,6 +62,10 @@ impl<T: Visit> Visit for Vec<T> {
     fn size(&self) -> usize {
         self.iter().map(|e| e.size()).sum()
     }
+
+    fn assert_valid(&self) {
+        self.iter().for_each(|e| e.assert_valid());
+    }
 }
 
 impl<T: Visit + Ord> Visit for Set<T> {
@@ -67,6 +76,10 @@ impl<T: Visit + Ord> Visit for Set<T> {
     fn size(&self) -> usize {
         self.iter().map(|e| e.size()).sum()
     }
+
+    fn assert_valid(&self) {
+        self.iter().for_each(|e| e.assert_valid());
+    }
 }
 
 impl<T: Visit> Visit for Option<T> {
@@ -77,6 +90,10 @@ impl<T: Visit> Visit for Option<T> {
     fn size(&self) -> usize {
         self.as_ref().map(|e| e.size()).unwrap_or(0)
     }
+
+    fn assert_valid(&self) {
+        self.iter().for_each(|e| e.assert_valid());
+    }
 }
 
 impl<T: Visit> Visit for Arc<T> {
@@ -87,6 +104,10 @@ impl<T: Visit> Visit for Arc<T> {
     fn size(&self) -> usize {
         T::size(self)
     }
+
+    fn assert_valid(&self) {
+        T::assert_valid(self)
+    }
 }
 
 impl Visit for Ty {
@@ -97,6 +118,10 @@ impl Visit for Ty {
     fn size(&self) -> usize {
         self.data().size()
     }
+
+    fn assert_valid(&self) {
+        self.data().assert_valid()
+    }
 }
 
 impl Visit for Lt {
@@ -107,6 +132,10 @@ impl Visit for Lt {
     fn size(&self) -> usize {
         self.data().size()
     }
+
+    fn assert_valid(&self) {
+        self.data().assert_valid()
+    }
 }
 
 impl Visit for usize {
@@ -117,6 +146,8 @@ impl Visit for usize {
     fn size(&self) -> usize {
         1
     }
+
+    fn assert_valid(&self) {}
 }
 
 impl Visit for u32 {
@@ -127,6 +158,8 @@ impl Visit for u32 {
     fn size(&self) -> usize {
         1
     }
+
+    fn assert_valid(&self) {}
 }
 
 impl<A: Visit, B: Visit> Visit for (A, B) {
@@ -142,6 +175,12 @@ impl<A: Visit, B: Visit> Visit for (A, B) {
         let (a, b) = self;
         a.size() + b.size()
     }
+
+    fn assert_valid(&self) {
+        let (a, b) = self;
+        a.assert_valid();
+        b.assert_valid();
+    }
 }
 
 impl<A: Visit, B: Visit, C: Visit> Visit for (A, B, C) {
@@ -158,6 +197,13 @@ impl<A: Visit, B: Visit, C: Visit> Visit for (A, B, C) {
         let (a, b, c) = self;
         a.size() + b.size() + c.size()
     }
+
+    fn assert_valid(&self) {
+        let (a, b, c) = self;
+        a.assert_valid();
+        b.assert_valid();
+        c.assert_valid();
+    }
 }
 
 impl<A: Visit> Visit for &A {
@@ -168,4 +214,8 @@ impl<A: Visit> Visit for &A {
     fn size(&self) -> usize {
         A::size(self)
     }
+
+    fn assert_valid(&self) {
+        A::assert_valid(self)
+    }
 }