[tested] verify consistency in linked blocks

crates/semantics/src/types.rs

@@ -219,7 +219,7 @@ pub fn find_user_type_recursion(contract: &mut ContractDefinition) {
 fn collect_edges(edges: &mut HashSet<(usize, usize, usize)>, fields: &[Param], struct_no: usize) {
     for (no, field) in fields.iter().enumerate() {
         for dependency in field.ty.ty.custom_type_dependencies() {
-            if edges.insert((no, dependency, struct_no)) {
+            if edges.insert((struct_no, dependency, no)) {
                 collect_edges(edges, fields, struct_no)
             }
         }

crates/verifier/Cargo.toml

@@ -22,6 +22,7 @@ algonaut_core = { workspace = true }
 z3 = { workspace = true }
 hex = { workspace = true }
 indexmap = { workspace = true }
+petgraph = { workspace = true }
 
 [dev-dependencies]
 folidity-parser = { workspace = true }

crates/verifier/src/ast.rs

@@ -6,7 +6,6 @@ use folidity_semantics::{
         StateDeclaration,
     },
     DelayedDeclaration,
-    GlobalSymbol,
     Span,
 };
 use indexmap::IndexMap;
@@ -76,7 +75,7 @@ pub struct DeclarationBounds<'ctx> {
     /// `st` location block.
     pub loc: Span,
     /// Links of others declaration.
-    pub links: Vec<GlobalSymbol>,
+    pub links: Vec<usize>,
     /// Constraint block of the declaration.
     pub constraints: IndexMap<u32, Constraint<'ctx>>,
     /// Scope of the local constraints.

crates/verifier/src/executor.rs

@@ -1,3 +1,5 @@
+use std::collections::HashSet;
+
 use folidity_diagnostics::{
     Paint,
     Report,
@@ -7,6 +9,7 @@ use folidity_semantics::{
     ContractDefinition,
     DelayedDeclaration,
     GlobalSymbol,
+    Span,
     SymbolInfo,
 };
 use indexmap::IndexMap;
@@ -23,7 +26,11 @@ use crate::{
         Delays,
         Z3Scope,
     },
-    solver::verify_constraints,
+    links::build_constraint_blocks,
+    solver::{
+        verify_constraint_blocks,
+        verify_constraints,
+    },
     transformer::{
         type_to_sort,
         TransformParams,
@@ -195,7 +202,7 @@ impl<'ctx> SymbolicExecutor<'ctx> {
     pub fn resolve_links(&mut self, delays: Delays<'_>, contract: &ContractDefinition) {
         for s in &delays.state_delay {
             if let Some(StateBody::Model(model_sym)) = &s.decl.body {
-                let mut links: Vec<GlobalSymbol> = vec![];
+                let mut links: Vec<usize> = vec![];
                 let (m_sym, model_bound) = self
                     .declarations
                     .get_key_value(&GlobalSymbol::Model(model_sym.clone()))
@@ -207,38 +214,54 @@ impl<'ctx> SymbolicExecutor<'ctx> {
                     let Some(sym) = &m_sym else {
                         break;
                     };
-                    links.push(sym.clone());
+                    if let Some(id) = self.declarations.get_index_of(sym) {
+                        links.push(id);
+                    }
                     let model_decl = &contract.models[sym.symbol_info().i];
                     m_sym = model_decl
                         .parent
                         .as_ref()
                         .map(|info| GlobalSymbol::Model(info.clone()))
                         .clone();
                 }
+                if let Some(from) = &s.decl.from {
+                    if let Some(id) = self
+                        .declarations
+                        .get_index_of(&GlobalSymbol::State(from.0.clone()))
+                    {
+                        links.push(id);
+                    }
+                }
 
                 let s_bound = &mut self.declarations[s.i];
                 s_bound.scope.consts.extend(m_scope);
 
-                if let Some(from) = &s.decl.from {
-                    links.push(GlobalSymbol::State(from.0.clone()))
-                }
                 s_bound.links = links;
             }
         }
 
         for m in &delays.func_delay {
-            let f_bound = &mut self.declarations[m.i];
-            let mut links: Vec<GlobalSymbol> = vec![];
+            let mut links: Vec<usize> = vec![];
             if let Some(sb) = &m.decl.state_bound {
                 if let Some(from) = &sb.from {
-                    links.push(GlobalSymbol::State(from.ty.clone()));
+                    if let Some(id) = self
+                        .declarations
+                        .get_index_of(&GlobalSymbol::State(from.ty.clone()))
+                    {
+                        links.push(id);
+                    }
                 }
 
                 for t in &sb.to {
-                    links.push(GlobalSymbol::State(t.ty.clone()));
+                    if let Some(id) = self
+                        .declarations
+                        .get_index_of(&GlobalSymbol::State(t.ty.clone()))
+                    {
+                        links.push(id);
+                    }
                 }
             }
-            f_bound.links = links;
+            self.declarations[m.i].links = links;
         }
     }
 
@@ -423,6 +446,69 @@ impl<'ctx> SymbolicExecutor<'ctx> {
         !error
     }
 
+    /// Verify linked constraint blocks to ensure their constraints don't contradict each
+    /// other.
+    pub fn verify_linked_blocks(&mut self, contract: &ContractDefinition) -> bool {
+        let mut error = false;
+        let mut diagnostics: Diagnostics = vec![];
+
+        let blocks = build_constraint_blocks(self);
+        for b in &blocks {
+            if let Err(errs) = verify_constraint_blocks(b.as_slice(), self.context) {
+                error = true;
+                let mut notes: Diagnostics = vec![];
+
+                let syms: HashSet<GlobalSymbol> = errs.iter().map(|x| x.1.clone()).collect();
+                let mut syms: Vec<GlobalSymbol> = syms.into_iter().collect();
+                syms.sort_by(|x, y| x.loc().start.cmp(&y.loc().start));
+
+                let consts: Vec<u32> = errs.iter().map(|x| x.0).collect();
+                for (i, (cid, g)) in errs.iter().enumerate() {
+                    let decl = &self.declarations.get(g).expect("should exist");
+                    let c = decl.constraints.get(cid).expect("constraints exists");
+                    let other_consts = remove_element(&consts, i);
+
+                    notes.push(Report::ver_error(
+                        c.loc.clone(),
+                        format!(
+                            "This is a constraint {} in {}. It contradicts {:?}",
+                            cid.yellow().bold(),
+                            &symbol_name(g, contract).bold(),
+                            &other_consts.red(),
+                        ),
+                    ))
+                }
+
+                let sym_strs: String = syms
+                    .iter()
+                    .fold(String::new(), |init, x| {
+                        format!("{}, {}", init, symbol_name(x, contract).bold())
+                    })
+                    .trim_start_matches(", ")
+                    .to_string();
+                // just get the span from start till end.
+                let start = errs
+                    .iter()
+                    .map(|x| x.1.loc().start)
+                    .min_by(|x, y| x.cmp(y))
+                    .unwrap_or(0);
+                let end = errs
+                    .iter()
+                    .map(|x| x.1.loc().end)
+                    .max_by(|x, y| x.cmp(y))
+                    .unwrap_or(0);
+                let loc = Span { start, end };
+                diagnostics.push(Report::ver_error_with_extra(loc, format!("Detected conflicting constraints in linked blocks. These are the linked blocks: {}", sym_strs), notes, String::from("Consider rewriting logical bounds to be consistent with other entities.")));
+            }
+        }
+
+        if error {
+            self.diagnostics.extend(diagnostics);
+        }
+
+        !error
+    }
+
     /// Create a Z3 constant with the current symbol counter as a name while increasing
     /// the counter.
     pub fn create_constant(&mut self, sort: &Sort<'ctx>) -> (Dynamic<'ctx>, u32) {

crates/verifier/src/lib.rs

@@ -12,6 +12,7 @@ use z3::{
 
 mod ast;
 mod executor;
+mod links;
 mod solver;
 mod transformer;
 
@@ -46,6 +47,12 @@ impl<'ctx> Runner<ContractDefinition, ()> for SymbolicExecutor<'ctx> {
 
         err |= !executor.verify_individual_blocks(source);
 
+        // report errors in individual blocks earlier to avoid catching them in linked blocks.
+        if err {
+            return Err(CompilationError::Formal(executor.diagnostics));
+        }
+
+        err = !executor.verify_linked_blocks(source);
         if err {
             return Err(CompilationError::Formal(executor.diagnostics));
         }

crates/verifier/src/links.rs

@@ -0,0 +1,65 @@
+use folidity_semantics::GlobalSymbol;
+use petgraph::{
+    algo::tarjan_scc,
+    Graph,
+    Undirected,
+};
+use std::collections::HashSet;
+
+use crate::{
+    ast::Constraint,
+    SymbolicExecutor,
+};
+
+type LinkGraph = Graph<usize, usize, Undirected, usize>;
+
+// pub struct LinkBlock<'ctx> {
+
+// }
+
+fn find_link_components(executor: &SymbolicExecutor) -> Vec<Vec<usize>> {
+    let mut edges: HashSet<(usize, usize)> = HashSet::new();
+
+    for (sym, d) in &executor.declarations {
+        if d.links.is_empty() {
+            continue;
+        }
+        let origin = executor
+            .declarations
+            .get_index_of(sym)
+            .expect("should exist");
+
+        for l in &d.links {
+            edges.insert((origin, *l));
+        }
+    }
+
+    // collect into a graph.
+    let graph: LinkGraph = LinkGraph::from_edges(&edges);
+    // since the graph is undirected, tarjan algo will just return sets of connected nodes.
+    let components = tarjan_scc(&graph)
+        .iter()
+        .map(|vec| vec.iter().map(|x| x.index()).collect())
+        .collect();
+
+    components
+}
+
+pub fn build_constraint_blocks<'ctx>(
+    executor: &mut SymbolicExecutor<'ctx>,
+) -> Vec<Vec<(Constraint<'ctx>, GlobalSymbol)>> {
+    let components = find_link_components(executor);
+    let mut blocks = vec![];
+    for decls in &components {
+        let mut constraints: Vec<(Constraint, GlobalSymbol)> = vec![];
+        for i in decls {
+            let (sym, decl) = executor.declarations.get_index(*i).expect("should exist");
+
+            for (_, c) in decl.constraints.clone() {
+                constraints.push((c, sym.clone()));
+            }
+        }
+        blocks.push(constraints);
+    }
+    blocks
+}

crates/verifier/src/solver.rs

@@ -1,3 +1,4 @@
+use folidity_semantics::GlobalSymbol;
 use z3::{
     ast::Bool,
     Context,
@@ -40,6 +41,52 @@ pub fn verify_constraints<'ctx>(
     res
 }
 
+/// Verify the slice of constraints block for satisfiability.
+///
+/// # Errors
+/// - List of mapping from symbol of declaration to the vector of contradicting constant
+///   ids.
+pub fn verify_constraint_blocks<'ctx>(
+    constraints: &[(Constraint<'ctx>, GlobalSymbol)],
+    context: &'ctx Context,
+) -> Result<(), Vec<(u32, GlobalSymbol)>> {
+    let binding_consts: Vec<Bool<'ctx>> = constraints
+        .iter()
+        .map(|c| c.0.sym_to_const(context))
+        .collect();
+
+    let solver = Solver::new(context);
+    for c in constraints {
+        solver.assert(&c.0.expr);
+    }
+
+    let res = match solver.check_assumptions(&binding_consts) {
+        SatResult::Sat => Ok(()),
+        SatResult::Unsat | SatResult::Unknown => {
+            let consts: Vec<u32> = solver
+                .get_unsat_core()
+                .iter()
+                .filter_map(|b| bool_const_to_id(b))
+                .collect();
+
+            let mut consts_syms: Vec<(u32, GlobalSymbol)> = constraints
+                .iter()
+                .filter_map(|(c, g)| {
+                    if consts.contains(&c.binding_sym) {
+                        Some((c.binding_sym, g.clone()))
+                    } else {
+                        None
+                    }
+                })
+                .collect();
+            consts_syms.sort_by_key(|x| x.0);
+            Err(consts_syms)
+        }
+    };
+    solver.reset();
+    res
+}
+
 /// Z3 converts integer names to `k!_` format, we need to parse it back to integers.
 fn bool_const_to_id(c: &Bool) -> Option<u32> {
     c.to_string().replace("k!", "").parse().ok()