From b6c75faf756365cb452d08cb860a23c4ed5eb365 Mon Sep 17 00:00:00 2001 From: Florian Sextl Date: Tue, 2 Feb 2021 19:34:44 +0100 Subject: [PATCH 1/4] add correct handling of false positives in coinductive cycles add new tests for coinduction handling --- chalk-recursive/src/recursive.rs | 30 ++++++-- chalk-recursive/src/search_graph.rs | 32 ++++++++ tests/test/coinduction.rs | 115 ++++++++++++++++++++++++---- 3 files changed, 156 insertions(+), 21 deletions(-) diff --git a/chalk-recursive/src/recursive.rs b/chalk-recursive/src/recursive.rs index 19b36e4e248..9dddf7f30f7 100644 --- a/chalk-recursive/src/recursive.rs +++ b/chalk-recursive/src/recursive.rs @@ -224,20 +224,33 @@ impl<'me, I: Interner> SolveDatabase for Solver<'me, I> { // Check if this table is still on the stack. if let Some(depth) = self.context.search_graph[dfn].stack_depth { // Is this a coinductive goal? If so, that is success, - // so we can return normally. Note that this return is - // not tabled. - // - // XXX how does caching with coinduction work? + // so we can return and set the minimum to its DFN. + // Note that this return is not tabled. And so are + // all other solutions in the cycle until the cycle + // start is finished. This avoids prematurely cached + // false positives. if self.context.stack.coinductive_cycle_from(depth) { let value = ConstrainedSubst { subst: goal.trivial_substitution(self.program.interner()), constraints: Constraints::empty(self.program.interner()), }; - debug!("applying coinductive semantics"); - return Ok(Solution::Unique(Canonical { + let trivial_solution = Ok(Solution::Unique(Canonical { value, binders: goal.canonical.binders, })); + + debug!("applying coinductive semantics"); + + // Set minimum to first occurrence of cyclic goal to prevent premature caching of possibly false solutions + minimums.update_from(self.context.search_graph[dfn].links); + + // Store trivial solution to start coinductive reasoning from this node + self.context.search_graph[dfn].solution = trivial_solution.clone(); + self.context.search_graph[dfn].solution_priority = + chalk_ir::ClausePriority::Low; + self.context.search_graph[dfn].coinductive_start = true; + + return trivial_solution; } self.context.stack[depth].flag_cycle(); @@ -275,6 +288,11 @@ impl<'me, I: Interner> SolveDatabase for Solver<'me, I> { // worst of the repeated work that we do during tabling. if subgoal_minimums.positive >= dfn { if self.context.caching_enabled { + // Remove possible false positives from coinductive cycle + if self.context.search_graph[dfn].coinductive_start && result.is_err() { + self.context.search_graph.remove_false_positives_after(dfn); + } + self.context .search_graph .move_to_cache(dfn, &mut self.context.cache); diff --git a/chalk-recursive/src/search_graph.rs b/chalk-recursive/src/search_graph.rs index 4d2af09c0a3..ee0489b3fd2 100644 --- a/chalk-recursive/src/search_graph.rs +++ b/chalk-recursive/src/search_graph.rs @@ -37,6 +37,11 @@ pub(super) struct Node { /// from the stack, it contains the DFN of the minimal ancestor /// that the table reached (or MAX if no cycle was encountered). pub(crate) links: Minimums, + + /// If this is true, the node is the start of coinductive cycle. + /// Thus, some cleanup has to be done before its result can be + /// cached to rule out false positives. + pub(crate) coinductive_start: bool, } impl SearchGraph { @@ -71,6 +76,7 @@ impl SearchGraph { solution_priority: ClausePriority::High, stack_depth: Some(stack_depth), links: Minimums { positive: dfn }, + coinductive_start: false, }; self.nodes.push(node); let previous_index = self.indices.insert(goal.clone(), dfn); @@ -101,6 +107,32 @@ impl SearchGraph { cache.insert(node.goal, node.solution); } } + + /// Removes all nodes that are part of a coinductive cycle and + /// have a solution as they might be false positives due to + /// coinductive reasoning. + #[instrument(level = "debug", skip(self))] + pub(crate) fn remove_false_positives_after(&mut self, dfn: DepthFirstNumber) { + let mut false_positive_indices = vec![]; + + // Find all possible false positives in the graph below the + // start of the coinductive cycle + for (index, node) in self.nodes[dfn.index + 1..].iter().enumerate() { + if node.solution.is_ok() { + false_positive_indices.push(index + dfn.index + 1); + } + } + + // Remove the potential false positives from the indices + self.indices + .retain(|_key, value| !false_positive_indices.contains(&value.index)); + + // Remove the potential false positives from the nodes + // in descending order to avoid unnecessary shifts + for false_positive_index in false_positive_indices.into_iter().rev() { + self.nodes.remove(false_positive_index); + } + } } impl Index for SearchGraph { diff --git a/tests/test/coinduction.rs b/tests/test/coinduction.rs index 957a41a2d39..52f8bc72556 100644 --- a/tests/test/coinduction.rs +++ b/tests/test/coinduction.rs @@ -213,23 +213,58 @@ fn coinductive_unsound1() { goal { forall { X: C1orC2 } - } yields[SolverChoice::slg(3, None)] { + } yields { "No possible solution" } + } +} + +/// The only difference between this test and `coinductive_unsound1` +/// is the order of the final `forall` clauses. +#[test] +fn coinductive_unsound2() { + test! { + program { + trait C1orC2 { } + + #[coinductive] + trait C1 { } + + #[coinductive] + trait C2 { } + + #[coinductive] + trait C3 { } + + forall { + T: C1 if T: C2, T: C3 + } + + forall { + T: C2 if T: C1 + } + + forall { + T: C1orC2 if T: C2 + } + + forall { + T: C1orC2 if T: C1 + } + } goal { forall { X: C1orC2 } - } yields[SolverChoice::recursive_default()] { - // FIXME(chalk#399) recursive solver doesn't handle coinduction correctly - "Unique; substitution [], lifetime constraints []" + } yields { + "No possible solution" } } } -/// The only difference between this test and `coinductive_unsound1` -/// is the order of the final `forall` clauses. +/// Same as the two before but needs to show T: C2 in both +// branches of T: C1. #[test] -fn coinductive_unsound2() { +fn coinductive_unsound3() { test! { program { trait C1orC2 { } @@ -243,6 +278,13 @@ fn coinductive_unsound2() { #[coinductive] trait C3 { } + #[coinductive] + trait C4 { } + + forall { + T: C3 if T: C2, T: C4 + } + forall { T: C1 if T: C2, T: C3 } @@ -251,13 +293,62 @@ fn coinductive_unsound2() { T: C2 if T: C1 } + forall { + T: C1orC2 if T: C1 + } + forall { T: C1orC2 if T: C2 } + } + + goal { + forall { X: C1orC2 } + } yields { + "No possible solution" + } + } +} + +/// Tests whether a nested coinductive cycle +/// that is also unsound is handled correctly. +#[test] +fn coinductive_unsound4() { + test! { + program { + trait C1orC2 { } + + #[coinductive] + trait C1 { } + + #[coinductive] + trait C2 { } + + #[coinductive] + trait C3 { } + + #[coinductive] + trait C4 { } + + forall { + T: C4 if T:C2, T: C3 + } + + forall { + T: C1 if T: C2, T: C3 + } + + forall { + T: C2 if T: C1, T: C4 + } forall { T: C1orC2 if T: C1 } + + forall { + T: C1orC2 if T: C2 + } } goal { @@ -450,14 +541,8 @@ fn coinductive_multicycle4() { goal { forall { X: Any } - } yields_all[SolverChoice::slg(3, None)] { - } - - goal { - forall { X: Any } - } yields[SolverChoice::recursive_default()] { - // FIXME(chalk#399) recursive solver doesn't handle coinduction correctly - "Unique; substitution [], lifetime constraints []" + } yields { + "No possible solution" } } } From 897d0df115aa17e1b50ec52b28500f4128d92789 Mon Sep 17 00:00:00 2001 From: Florian Sextl Date: Thu, 4 Feb 2021 14:25:19 +0100 Subject: [PATCH 2/4] add corresponding documentation in book add solution0 document solution0 and remove unecessary test cases simplify according to review --- book/src/recursive/coinduction.md | 72 +++++++++++++++- chalk-recursive/src/combine.rs | 28 +------ chalk-recursive/src/recursive.rs | 70 ++++------------ chalk-recursive/src/search_graph.rs | 55 +++++-------- chalk-recursive/src/stack.rs | 20 +++-- tests/test/coinduction.rs | 122 ++++++++++++++++++++++++---- 6 files changed, 231 insertions(+), 136 deletions(-) diff --git a/book/src/recursive/coinduction.md b/book/src/recursive/coinduction.md index dc9a4d87c26..d3184cfd7cf 100644 --- a/book/src/recursive/coinduction.md +++ b/book/src/recursive/coinduction.md @@ -1,3 +1,73 @@ # Coinduction -TBD \ No newline at end of file +This sub-chapter is meant to describe the current handling of coinductive goals in the recursive solver rather than providing an extensive overview over the theoretical backgrounds and ideas. +It follows the description in [this GitHub comment](https://github.com/rust-lang/chalk/issues/399#issuecomment-643420016) and the Zulip topic linked there. + +## General Idea +The general idea for the handling of coinductive cycles in the recursive solver is to start by assuming the goal is provable and then try to find evidence that it is not. +This search for a disproof is done by the standard recursive solving process described in the sub-chapters before. + +Albeit this approach would allow for the handling of mixed inductive/co-inductive cycles, these are actually handled as errors to prevent propagation of the assumed provability outside of the coinductive cycle. +This propagation of the assumed solution might also happen in pure coinductive cycles and can potentially lead to invalid results. + +## Prevention of Invalid Results +The problem of invalid results propagated outside of the coinductive cycle is also described in the [Coinduction chapter](../engine/logic/coinduction.md) for the SLG solver alongside the rather complex handling used with it. + +### The Problem +The problem arises if a solution that is purely based on the positive starting value for the coinductive cycle is cached and as such propagated to other goals that are possibly reliant on this. An example may look like this (cf. the test case `coinduction::coinductive_unsound`): + +```notrust +C :- C1. +C :- C2 +C1 :- C2, C3. +C2 :- C1. +``` + +Here `C` may be proved by either showing `C1` or `C2`. +Assuming the solver starts evaluating the branch with `C1` first, it then recursively tries to prove `C2` and `C3`. +For proving `C2` it needs to show `C1` again, the coinductive cycle becomes evident. +Therefore, `C1` is assumed to be provable and the solver proves `C2` with this information. +Assuming, the solve does not handle this case specifically, the solution for `C2` is cached. +Now it tries solving `C3` but fails due to the lack of information about it. +As such, `C1` can also not be proven for this program. +The recursive solver will now attempt to prove the initial goal `C` by solving `C2`. +Unfortunately, it finds the invalidly cached solution and returns it as proof for `C`. + +By visualizing this path of computation, it becomes evident, where the problem lies: +* Start proving `C` with `C1`: + * For `C1` prove `C2` and `C3`: + * For `C2` prove `C1`: + * This is a coinductive cycle. Assume that `C1` holds. + * Thus `C2` also holds. Store this result about `C2` in the cache. + * There is no way to prove `C3`. Lift this failure up. + * Due to the failure of `C3` there is also no solution for `C1`. +* Try proving `C` with `C2`: + * Find the cached result that `C2` has a solution and return it as the solution for `C`. +* Stop with the invalid result for `C`. + +### The Solution +The above example should make it evident that the caching of found solutions in coinductive cycles can lead to invalid results and should therefore be prevented. +This can be achieved by delaying the caching of all results inside the coinductive cycle until it is clear whether the start of the cycle (i.e. `C1` in the example above) is provable. +If the start of the cycle can be proven by the results of the cycle and related subgoals then the assumption about it was correct and thus all results for goals inside the cycle are also valid. +If, however, the start of the cycle can not be proved, i.e. the initial assumption was false, then a subset of the found solutions for the coinductive cycle may be invalid (i.e. the solution for `C2` in the example). + +To remove such invalid results, the cycle is restarted with a negative result for the cycle start. +With this approach, it is possible to remove all invalid result that would otherwise depend on the disproved cycle assumption. +To allow for the cycle to be restarted correctly, all nodes in the search graph after the cycle start are deleted. + +With this procedure, the example is handled as follows: +* Start proving `C` with `C1`: + * For `C1` prove `C2` and `C3`: + * For `C2` prove `C1`: + * This is a coinductive cycle. Assume that `C1` holds. + * Thus `C2` also holds. Delay the caching of the result about `C2`. + * There is no way to prove `C3`. Cache this result and lift the failure up. + * Due to the failure of `C3` there is also no solution for `C1`. Set `C1` to a negative result and restart the cycle. + * For `C2` prove `C1`: + * `C1` has now a negative result. + * Thus, `C2` also has a negative result which is not yet cached. + * The result for `C3` is already cached. + * Nothing changed regarding `C1` (this would indicate a negative cycle which is currently not allowed) and the negative result for `C1` and `C2` are cached. Lift negative result for `C1`. +* Start proving `C` with `C2`: + * Find negative cached result for `C2`. Lift the result back up. +* Neither `C1` nor `C2` have a positive result. Stop with the valid disproof of `C`. diff --git a/chalk-recursive/src/combine.rs b/chalk-recursive/src/combine.rs index d0a6441ba2e..df57bf666e7 100644 --- a/chalk-recursive/src/combine.rs +++ b/chalk-recursive/src/combine.rs @@ -2,33 +2,7 @@ use chalk_solve::Solution; use tracing::debug; use chalk_ir::interner::Interner; -use chalk_ir::{ClausePriority, DomainGoal, Fallible, GenericArg, Goal, GoalData}; - -pub(crate) fn with_priorities_for_goal( - interner: &I, - goal: &Goal, - a: Fallible>, - prio_a: ClausePriority, - b: Fallible>, - prio_b: ClausePriority, -) -> (Fallible>, ClausePriority) { - let domain_goal = match goal.data(interner) { - GoalData::DomainGoal(domain_goal) => domain_goal, - _ => { - // non-domain goals currently have no priorities, so we always take the new solution here - return (b, prio_b); - } - }; - match (a, b) { - (Ok(a), Ok(b)) => { - let (solution, prio) = with_priorities(interner, domain_goal, a, prio_a, b, prio_b); - (Ok(solution), prio) - } - (Ok(solution), Err(_)) => (Ok(solution), prio_a), - (Err(_), Ok(solution)) => (Ok(solution), prio_b), - (Err(_), Err(e)) => (Err(e), prio_b), - } -} +use chalk_ir::{ClausePriority, DomainGoal, GenericArg}; pub(super) fn with_priorities( interner: &I, diff --git a/chalk-recursive/src/recursive.rs b/chalk-recursive/src/recursive.rs index 9dddf7f30f7..53ccd94188f 100644 --- a/chalk-recursive/src/recursive.rs +++ b/chalk-recursive/src/recursive.rs @@ -2,10 +2,10 @@ use crate::search_graph::DepthFirstNumber; use crate::search_graph::SearchGraph; use crate::solve::{SolveDatabase, SolveIteration}; use crate::stack::{Stack, StackDepth}; -use crate::{combine, Minimums, UCanonicalGoal}; -use chalk_ir::interner::Interner; +use crate::{Minimums, UCanonicalGoal}; use chalk_ir::Fallible; -use chalk_ir::{Canonical, ConstrainedSubst, Constraints, Goal, InEnvironment, UCanonical}; +use chalk_ir::{interner::Interner, NoSolution}; +use chalk_ir::{Canonical, ConstrainedSubst, Goal, InEnvironment, UCanonical}; use chalk_solve::{coinductive_goal::IsCoinductive, RustIrDatabase, Solution}; use rustc_hash::FxHashMap; use std::fmt; @@ -163,18 +163,6 @@ impl<'me, I: Interner> Solver<'me, I> { return *minimums; } - let old_answer = &self.context.search_graph[dfn].solution; - let old_prio = self.context.search_graph[dfn].solution_priority; - - let (current_answer, current_prio) = combine::with_priorities_for_goal( - self.program.interner(), - &canonical_goal.canonical.value.goal, - old_answer.clone(), - old_prio, - current_answer, - current_prio, - ); - // Some of our subgoals depended on us. We need to re-run // with the current answer. if self.context.search_graph[dfn].solution == current_answer { @@ -223,37 +211,15 @@ impl<'me, I: Interner> SolveDatabase for Solver<'me, I> { if let Some(dfn) = self.context.search_graph.lookup(&goal) { // Check if this table is still on the stack. if let Some(depth) = self.context.search_graph[dfn].stack_depth { - // Is this a coinductive goal? If so, that is success, - // so we can return and set the minimum to its DFN. - // Note that this return is not tabled. And so are - // all other solutions in the cycle until the cycle - // start is finished. This avoids prematurely cached - // false positives. - if self.context.stack.coinductive_cycle_from(depth) { - let value = ConstrainedSubst { - subst: goal.trivial_substitution(self.program.interner()), - constraints: Constraints::empty(self.program.interner()), - }; - let trivial_solution = Ok(Solution::Unique(Canonical { - value, - binders: goal.canonical.binders, - })); - - debug!("applying coinductive semantics"); - - // Set minimum to first occurrence of cyclic goal to prevent premature caching of possibly false solutions - minimums.update_from(self.context.search_graph[dfn].links); - - // Store trivial solution to start coinductive reasoning from this node - self.context.search_graph[dfn].solution = trivial_solution.clone(); - self.context.search_graph[dfn].solution_priority = - chalk_ir::ClausePriority::Low; - self.context.search_graph[dfn].coinductive_start = true; - - return trivial_solution; - } - self.context.stack[depth].flag_cycle(); + // Mixed cycles are not allowed. + if self + .context + .stack + .mixed_inductive_coinductive_cycle_from(depth) + { + return Err(NoSolution); + } } minimums.update_from(self.context.search_graph[dfn].links); @@ -268,10 +234,15 @@ impl<'me, I: Interner> SolveDatabase for Solver<'me, I> { previous_solution } else { // Otherwise, push the goal onto the stack and create a table. - // The initial result for this table is error. + // The initial result for this table depends on whether the goal is coinductive. let coinductive_goal = goal.is_coinductive(self.program); let depth = self.context.stack.push(coinductive_goal); - let dfn = self.context.search_graph.insert(&goal, depth); + let dfn = self.context.search_graph.insert( + &goal, + depth, + coinductive_goal, + self.program.interner(), + ); let subgoal_minimums = self.solve_new_subgoal(goal, depth, dfn); self.context.search_graph[dfn].links = subgoal_minimums; self.context.search_graph[dfn].stack_depth = None; @@ -288,11 +259,6 @@ impl<'me, I: Interner> SolveDatabase for Solver<'me, I> { // worst of the repeated work that we do during tabling. if subgoal_minimums.positive >= dfn { if self.context.caching_enabled { - // Remove possible false positives from coinductive cycle - if self.context.search_graph[dfn].coinductive_start && result.is_err() { - self.context.search_graph.remove_false_positives_after(dfn); - } - self.context .search_graph .move_to_cache(dfn, &mut self.context.cache); diff --git a/chalk-recursive/src/search_graph.rs b/chalk-recursive/src/search_graph.rs index ee0489b3fd2..cd2c2ecbb8e 100644 --- a/chalk-recursive/src/search_graph.rs +++ b/chalk-recursive/src/search_graph.rs @@ -5,7 +5,10 @@ use std::usize; use super::stack::StackDepth; use crate::{Minimums, UCanonicalGoal}; -use chalk_ir::{interner::Interner, ClausePriority, Fallible, NoSolution}; +use chalk_ir::{ + interner::Interner, Canonical, ClausePriority, ConstrainedSubst, Constraints, Fallible, + NoSolution, +}; use chalk_solve::Solution; use rustc_hash::FxHashMap; use tracing::{debug, instrument}; @@ -37,11 +40,6 @@ pub(super) struct Node { /// from the stack, it contains the DFN of the minimal ancestor /// that the table reached (or MAX if no cycle was encountered). pub(crate) links: Minimums, - - /// If this is true, the node is the start of coinductive cycle. - /// Thus, some cleanup has to be done before its result can be - /// cached to rule out false positives. - pub(crate) coinductive_start: bool, } impl SearchGraph { @@ -61,22 +59,35 @@ impl SearchGraph { /// /// - stack depth as given /// - links set to its own DFN - /// - solution is initially `NoSolution` + /// - solution is initially an identity substitution for coinductive goals + /// or `NoSolution` for other goals pub(crate) fn insert( &mut self, goal: &UCanonicalGoal, stack_depth: StackDepth, + coinductive: bool, + interner: &I, ) -> DepthFirstNumber { let dfn = DepthFirstNumber { index: self.nodes.len(), }; + let solution = if coinductive { + Ok(Solution::Unique(Canonical { + value: ConstrainedSubst { + subst: goal.trivial_substitution(interner), + constraints: Constraints::empty(interner), + }, + binders: goal.canonical.binders.clone(), + })) + } else { + Err(NoSolution) + }; let node = Node { goal: goal.clone(), - solution: Err(NoSolution), + solution, solution_priority: ClausePriority::High, stack_depth: Some(stack_depth), links: Minimums { positive: dfn }, - coinductive_start: false, }; self.nodes.push(node); let previous_index = self.indices.insert(goal.clone(), dfn); @@ -107,32 +118,6 @@ impl SearchGraph { cache.insert(node.goal, node.solution); } } - - /// Removes all nodes that are part of a coinductive cycle and - /// have a solution as they might be false positives due to - /// coinductive reasoning. - #[instrument(level = "debug", skip(self))] - pub(crate) fn remove_false_positives_after(&mut self, dfn: DepthFirstNumber) { - let mut false_positive_indices = vec![]; - - // Find all possible false positives in the graph below the - // start of the coinductive cycle - for (index, node) in self.nodes[dfn.index + 1..].iter().enumerate() { - if node.solution.is_ok() { - false_positive_indices.push(index + dfn.index + 1); - } - } - - // Remove the potential false positives from the indices - self.indices - .retain(|_key, value| !false_positive_indices.contains(&value.index)); - - // Remove the potential false positives from the nodes - // in descending order to avoid unnecessary shifts - for false_positive_index in false_positive_indices.into_iter().rev() { - self.nodes.remove(false_positive_index); - } - } } impl Index for SearchGraph { diff --git a/chalk-recursive/src/stack.rs b/chalk-recursive/src/stack.rs index 917d39c7643..dd228cba471 100644 --- a/chalk-recursive/src/stack.rs +++ b/chalk-recursive/src/stack.rs @@ -67,12 +67,20 @@ impl Stack { self.entries.pop(); } - /// True if all the goals from the top of the stack down to (and - /// including) the given depth are coinductive. - pub(crate) fn coinductive_cycle_from(&self, depth: StackDepth) -> bool { - self.entries[depth.depth..] - .iter() - .all(|entry| entry.coinductive_goal) + /// True if either all the goals from the top of the stack down to (and + /// including) the given depth are coinductive or if all goals are inductive + /// (i.e. not coinductive). + pub(crate) fn mixed_inductive_coinductive_cycle_from(&self, depth: StackDepth) -> bool { + let (inductive, coinductive) = + self.entries[depth.depth..] + .iter() + .fold((false, false), |(ind, coind), entry| { + ( + ind || !entry.coinductive_goal, + coind || entry.coinductive_goal, + ) + }); + inductive && coinductive } } diff --git a/tests/test/coinduction.rs b/tests/test/coinduction.rs index 52f8bc72556..b469378766d 100644 --- a/tests/test/coinduction.rs +++ b/tests/test/coinduction.rs @@ -261,10 +261,10 @@ fn coinductive_unsound2() { } } -/// Same as the two before but needs to show T: C2 in both -// branches of T: C1. +/// Tests whether a nested coinductive cycle +/// that is also unsound is handled correctly. #[test] -fn coinductive_unsound3() { +fn coinductive_unsound_nested() { test! { program { trait C1orC2 { } @@ -282,7 +282,7 @@ fn coinductive_unsound3() { trait C4 { } forall { - T: C3 if T: C2, T: C4 + T: C4 if T:C2, T: C3 } forall { @@ -290,7 +290,7 @@ fn coinductive_unsound3() { } forall { - T: C2 if T: C1 + T: C2 if T: C1, T: C4 } forall { @@ -310,13 +310,14 @@ fn coinductive_unsound3() { } } -/// Tests whether a nested coinductive cycle -/// that is also unsound is handled correctly. +/// Test with two nested coinductive cycles where the inner fails +/// whereas the outer holds. No false positives should be kept from +/// the inner cycle. #[test] -fn coinductive_unsound4() { +fn coinductive_unsound_nested2() { test! { program { - trait C1orC2 { } + trait C1andC2 { } #[coinductive] trait C1 { } @@ -330,29 +331,120 @@ fn coinductive_unsound4() { #[coinductive] trait C4 { } + #[coinductive] + trait C5 { } + + #[coinductive] + trait C6 { } + + #[coinductive] + trait C7 { } + forall { - T: C4 if T:C2, T: C3 + T: C2 if T: C5 } forall { - T: C1 if T: C2, T: C3 + T: C6 if T: C2, T: C7 } forall { - T: C2 if T: C1, T: C4 + T: C5 if T:C6 } forall { - T: C1orC2 if T: C1 + T: C4 if T: C1 } forall { - T: C1orC2 if T: C2 + T: C3 if T: C5 + } + + forall { + T: C3 if T: C4 + } + + forall { + T: C1 if T: C3 + } + + forall { + T: C1andC2 if T: C1, T: C2 } } goal { - forall { X: C1orC2 } + forall { X: C1andC2 } + } yields { + "No possible solution" + } + } +} + +/// Another test with two nested coinductive cycles. +/// Here the inner cycle is also dependent on the outer one. +#[test] +fn coinductive_unsound_inter_cycle_dependency() { + test! { + program { + trait C1andC2 { } + + #[coinductive] + trait C1 { } + + #[coinductive] + trait C2 { } + + #[coinductive] + trait C3 { } + + #[coinductive] + trait C4 { } + + #[coinductive] + trait C5 { } + + #[coinductive] + trait C6 { } + + #[coinductive] + trait C7 { } + + forall { + T: C2 if T: C5, T: C1 + } + + forall { + T: C6 if T: C2, T: C7 + } + + forall { + T: C5 if T:C6 + } + + forall { + T: C4 if T: C1 + } + + forall { + T: C3 if T: C5 + } + + forall { + T: C3 if T: C4 + } + + forall { + T: C1 if T: C3 + } + + forall { + T: C1andC2 if T: C1, T: C2 + } + } + + goal { + forall { X: C1andC2 } } yields { "No possible solution" } From e98a14f30143b32e58c559e6e02362f34abd96a6 Mon Sep 17 00:00:00 2001 From: Florian Sextl Date: Mon, 5 Apr 2021 12:19:41 +0200 Subject: [PATCH 3/4] add documentation about mixed cycles --- book/src/glossary.md | 12 +++++ book/src/recursive/coinduction.md | 87 ++++++++++++++++++++----------- book/src/todo.md | 1 - chalk-recursive/src/recursive.rs | 4 +- chalk-recursive/src/stack.rs | 24 ++++----- 5 files changed, 82 insertions(+), 46 deletions(-) diff --git a/book/src/glossary.md b/book/src/glossary.md index e64090ae702..afa0aca6a02 100644 --- a/book/src/glossary.md +++ b/book/src/glossary.md @@ -229,3 +229,15 @@ valuation `A = true, B = false` makes the premise true and the conclusion false. ## Valuation A valuation is an assignment of values to all variables inside a logical formula. + +## Fixed-Points +A fixed-point of a function `f` is a value `x` for which `f(x)=x`. +Similarly a pre-fixed-point is defined as `x ≤ f(x)`, whereas for a post-fixed-point it holds that `f(x) ≤ x`. + +A least fixed-point (lfp) of `f` is the fixed-point `x` of `f` for which all other fixed-points `y` are greater or equal (i.e. if `f(y)=y` then `x ≤ y`). +Similarly, a greatest fixed-point (gfp) is greater or equal than all other fixed-points. +If `f` is a function on sets, the least fixed-point is defined as the intersection of all pre-fixed-points, which are then defined as sets `x` for which `x ⊆ f(x)`. +The greatest fixed-point is in this case the union of all post-fixed-points, respectively. + +This simple definition of lfp and gfp can also be lifted to general lattices. +The results for Chalk goals form such a lattice and, thus, every solver for such goals tries to find such fixed-points. \ No newline at end of file diff --git a/book/src/recursive/coinduction.md b/book/src/recursive/coinduction.md index d3184cfd7cf..1eb234c4e7b 100644 --- a/book/src/recursive/coinduction.md +++ b/book/src/recursive/coinduction.md @@ -2,52 +2,74 @@ This sub-chapter is meant to describe the current handling of coinductive goals in the recursive solver rather than providing an extensive overview over the theoretical backgrounds and ideas. It follows the description in [this GitHub comment](https://github.com/rust-lang/chalk/issues/399#issuecomment-643420016) and the Zulip topic linked there. +In general, coinductive cycles can arise for well-formedness checking and autotraits. +Therefore, correctly handling coinductive cycles is necessary to model the Rust trait system in its entirety. ## General Idea -The general idea for the handling of coinductive cycles in the recursive solver is to start by assuming the goal is provable and then try to find evidence that it is not. -This search for a disproof is done by the standard recursive solving process described in the sub-chapters before. +Coinductive cycles can be handled the same way as inductive cycles described [before](./inductive_cycles.md). +The only difference is the start value for coinductive goals. +Whereas inductive goals start with a negative result and are iterated until a least fixed-point is found, coinductive goals start with a positive result (i.e. a unique solution with identity substitution). +This negative result is then iterated until a greatest fixed-point is reached. -Albeit this approach would allow for the handling of mixed inductive/co-inductive cycles, these are actually handled as errors to prevent propagation of the assumed provability outside of the coinductive cycle. -This propagation of the assumed solution might also happen in pure coinductive cycles and can potentially lead to invalid results. +## Mixed co-inductive and inductive Cycles +As described above, the handling of inductive and coindutive cycles differs only in the start value from which the computation begins. +Thus, it might seem reasonable to have mixed inductive and coinductive cycles as all goals inside these cycles would be handled the same way anyway. +Unfortunately, this is not possible for the kind of logic that Chalk is based on (i.e. essentially an extension of co-LP for Hereditary Harrop clauses, cf. [this paper][co-LP]). + +There is fundamental difference between results for inductive cycles and results for coinductive cycles of goals. +An inductive goal is provable if and only if there exists a proof for it consisting of a finite chain of derivations from axioms that are members of the least-fixed point of the underlying logic program. +On the other hand, coinductive goals are provable if there exists an at most infinite derivation starting from the axioms that proves it (this includes in particular all finite derivations). +This infinite derivation is then part of the greatest fixed-point of the logic program. +As infinite derivations are not feasible to compute, it is enough to show that such a derivation contains no contradiction. + +A simple example `X :- X.` (with `X` a free variable) is thus not provable by inductive reasoning (the least solution/lfp for this is the empty solution, a failure) but it is provable by coinductive reasoning (the greatest solution/gfp is the universe, i.e. all values). + +This difference between inductive and coinductive results becomes a problem when combined in a single cycle. +Consider a coinductive goal `CG` and an inductive goal `IG`. Now consider the simplest possible mixed cycle: +```notrust +CG :- IG +IG :- CG +``` +It is apparent, that there can not exist a solution for `IG` as the cyclic dependency prevents a finite proof derivation. +In contrast to that, `CG` could potentially be provable as the derivation *`CG` if `IG` if `CG` if `IG` ...* is infinite and based only on the two axioms. +As a result, `CG` would hold whereas `IG` would not hold, creating a contradiction. + +The simplest solution to this problem, proposed by Simon et al. in [their paper about co-LP][co-LP], is to disallow mixed inductive and coinductive cycles. +This approach is also used by Chalk. ## Prevention of Invalid Results The problem of invalid results propagated outside of the coinductive cycle is also described in the [Coinduction chapter](../engine/logic/coinduction.md) for the SLG solver alongside the rather complex handling used with it. +Whereas the SLG solver introduces [special constructs](../engine/logic/coinduction.html#nikos-proposed-solution) to handle coinduction, it is sufficient for the recursive solver to use the same logic for inductive and coinductive cycles. +The following is a description of how this works in more detail. ### The Problem -The problem arises if a solution that is purely based on the positive starting value for the coinductive cycle is cached and as such propagated to other goals that are possibly reliant on this. An example may look like this (cf. the test case `coinduction::coinductive_unsound`): +The problem arises if a solution that is purely based on the positive starting value for the coinductive cycle is cached (or tabled in logic programming terms) and as such propagated to other goals that are possibly reliant on this. An example where all clause goals are assumedly coinductive may look like this (cf. the test case `coinduction::coinductive_unsound1`): ```notrust C :- C1. -C :- C2 +C :- C2. C1 :- C2, C3. C2 :- C1. ``` - -Here `C` may be proved by either showing `C1` or `C2`. -Assuming the solver starts evaluating the branch with `C1` first, it then recursively tries to prove `C2` and `C3`. -For proving `C2` it needs to show `C1` again, the coinductive cycle becomes evident. -Therefore, `C1` is assumed to be provable and the solver proves `C2` with this information. -Assuming, the solve does not handle this case specifically, the solution for `C2` is cached. -Now it tries solving `C3` but fails due to the lack of information about it. -As such, `C1` can also not be proven for this program. -The recursive solver will now attempt to prove the initial goal `C` by solving `C2`. -Unfortunately, it finds the invalidly cached solution and returns it as proof for `C`. - -By visualizing this path of computation, it becomes evident, where the problem lies: -* Start proving `C` with `C1`: - * For `C1` prove `C2` and `C3`: - * For `C2` prove `C1`: - * This is a coinductive cycle. Assume that `C1` holds. - * Thus `C2` also holds. Store this result about `C2` in the cache. - * There is no way to prove `C3`. Lift this failure up. - * Due to the failure of `C3` there is also no solution for `C1`. -* Try proving `C` with `C2`: - * Find the cached result that `C2` has a solution and return it as the solution for `C`. -* Stop with the invalid result for `C`. +The following is a computation to find out whether there exists a type that implements `C`. +Here the implementation of `C` may be proved by either showing that the type implements `C1` or `C2`. +* Start proving `C` by trying to prove `C1`: + * For `C1` try to prove `C2` and `C3`: + * Start with `C2`. For `C2` we need to prove `C1`: + * This is a (coinductive) cycle. Assume that `C1` holds, i.e. use the positive start value. + * Based on this `C2` also holds. If this case is not handled specifically, the solution for `C2` is cached without a reference to the solution for `C1` on which it depends. + * Now try to prove `C3`: + * Find that there is no way do so from the given axioms. + * Thus, there exists no solution for `C3` and the computation fails. This valid result is cached and lifted back up. + * Due to the failure of `C3` there is also no solution for `C1`. This failure is also cached correctly and lifted back up. The cached solution for `C2` has now become invalid as it depends on a positive result for `C1`. +* As a result of the failure for `C1`, `C` can not be proved from `C1`. Try proving `C` from `C2` instead: + * Find the cached result that `C2` has a solution and lift it back up. +* Due to the solution for `C2`, `C` is also proved with the same solution. +* Stop with this positive but invalid result for `C`. ### The Solution The above example should make it evident that the caching of found solutions in coinductive cycles can lead to invalid results and should therefore be prevented. -This can be achieved by delaying the caching of all results inside the coinductive cycle until it is clear whether the start of the cycle (i.e. `C1` in the example above) is provable. +This can be achieved by delaying the caching of all results inside the coinductive cycle until it is clear whether the start of the cycle (i.e. `C1` in the example above) is provable (cf. the handling of inductive cycles [before](./inductive_cycles.md)). If the start of the cycle can be proven by the results of the cycle and related subgoals then the assumption about it was correct and thus all results for goals inside the cycle are also valid. If, however, the start of the cycle can not be proved, i.e. the initial assumption was false, then a subset of the found solutions for the coinductive cycle may be invalid (i.e. the solution for `C2` in the example). @@ -66,8 +88,11 @@ With this procedure, the example is handled as follows: * For `C2` prove `C1`: * `C1` has now a negative result. * Thus, `C2` also has a negative result which is not yet cached. - * The result for `C3` is already cached. - * Nothing changed regarding `C1` (this would indicate a negative cycle which is currently not allowed) and the negative result for `C1` and `C2` are cached. Lift negative result for `C1`. + * Find the already cached negative result for `C3`. + * Nothing changed regarding `C1` (this would indicate a negative cycle which is currently not allowed) and the negative result for `C1` and `C2` are cached. Lift the negative result for `C1` back up. * Start proving `C` with `C2`: * Find negative cached result for `C2`. Lift the result back up. * Neither `C1` nor `C2` have a positive result. Stop with the valid disproof of `C`. + + +[co-LP]: https://link.springer.com/chapter/10.1007%2F978-3-540-73420-8_42 \ No newline at end of file diff --git a/book/src/todo.md b/book/src/todo.md index 978bc317169..845cc2a2f2d 100644 --- a/book/src/todo.md +++ b/book/src/todo.md @@ -4,4 +4,3 @@ Some topics yet to be written: - Elaborate on the proof procedure - SLG solving – introduce negative reasoning -- Recursive solver coinduction chapter diff --git a/chalk-recursive/src/recursive.rs b/chalk-recursive/src/recursive.rs index 53ccd94188f..7b7f15a2ba4 100644 --- a/chalk-recursive/src/recursive.rs +++ b/chalk-recursive/src/recursive.rs @@ -212,7 +212,9 @@ impl<'me, I: Interner> SolveDatabase for Solver<'me, I> { // Check if this table is still on the stack. if let Some(depth) = self.context.search_graph[dfn].stack_depth { self.context.stack[depth].flag_cycle(); - // Mixed cycles are not allowed. + // Mixed cycles are not allowed. For mor information about this + // see the corresponding section in the coinduction chapter: + // https://rust-lang.github.io/chalk/book/recursive/coinduction.html#mixed-co-inductive-and-inductive-cycles if self .context .stack diff --git a/chalk-recursive/src/stack.rs b/chalk-recursive/src/stack.rs index dd228cba471..c5669a67cd4 100644 --- a/chalk-recursive/src/stack.rs +++ b/chalk-recursive/src/stack.rs @@ -67,20 +67,18 @@ impl Stack { self.entries.pop(); } - /// True if either all the goals from the top of the stack down to (and - /// including) the given depth are coinductive or if all goals are inductive - /// (i.e. not coinductive). + /// True iff there exist at least one coinductive goal + /// and one inductive goal each from the top of the stack + /// down to (and including) the given depth. pub(crate) fn mixed_inductive_coinductive_cycle_from(&self, depth: StackDepth) -> bool { - let (inductive, coinductive) = - self.entries[depth.depth..] - .iter() - .fold((false, false), |(ind, coind), entry| { - ( - ind || !entry.coinductive_goal, - coind || entry.coinductive_goal, - ) - }); - inductive && coinductive + let coinductive_count = self.entries[depth.depth..] + .iter() + .filter(|entry| entry.coinductive_goal) + .count(); + let total_count = self.entries.len() - depth.depth; + let any_coinductive = coinductive_count != 0; + let any_inductive = coinductive_count != total_count; + any_coinductive && any_inductive } } From 9ce2cefc145931a6fca4c9253b9ba9a11ef5e13a Mon Sep 17 00:00:00 2001 From: Niko Matsakis Date: Sun, 11 Apr 2021 21:05:28 -0400 Subject: [PATCH 4/4] Update chalk-recursive/src/recursive.rs --- chalk-recursive/src/recursive.rs | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/chalk-recursive/src/recursive.rs b/chalk-recursive/src/recursive.rs index 7b7f15a2ba4..183b6b9213b 100644 --- a/chalk-recursive/src/recursive.rs +++ b/chalk-recursive/src/recursive.rs @@ -212,7 +212,7 @@ impl<'me, I: Interner> SolveDatabase for Solver<'me, I> { // Check if this table is still on the stack. if let Some(depth) = self.context.search_graph[dfn].stack_depth { self.context.stack[depth].flag_cycle(); - // Mixed cycles are not allowed. For mor information about this + // Mixed cycles are not allowed. For more information about this // see the corresponding section in the coinduction chapter: // https://rust-lang.github.io/chalk/book/recursive/coinduction.html#mixed-co-inductive-and-inductive-cycles if self