Fatal error: exception Cannot prove termination for ...

[ebruneton]

I get this error for the len function in the following example:

pub struct Node {
    next: Option<Box<Node>>,
}

#[logic]
fn len(n: Node) -> Int {
    match n.next {
        Some(node) => len(*node) + 1,
        None => 0,
    }
}

impl Node {
    #[ensures(len(result) == 0)]
    pub fn nil() -> Self {
        Self { next: None }
    }
}

This variant works well:

pub enum Node {
    Nil,
    Cons(Box<Node>),
}

#[logic]
fn len(n: Node) -> Int {
    match n {
        Node::Cons(node) => len(*node) + 1,
        Node::Nil => 0,
    }
}

impl Node {
    #[ensures(len(result) == 0)]
    pub fn nil() -> Self {
        Self::Nil
    }
}

What is missing in the first case to make it work (in my use case I have other fields in Node which are valid whether next is None or not; with the second design I would need to duplicate them)? Maybe a #[variant]?

[jhjourdan]

Could you try:

#[logic]
fn len(n: Node) -> Int {
    match n {
        { next: Some(node) } => len(*node) + 1,
        { next: None } => 0,
    }
}

The point being, we use a very simple syntactic criterion to prove the well-formedness of structural recursion. Pattern matching is considered to generate smaller values, but not field access. The reason for this is that this is basically why Why3 does.

[ebruneton]

Yes, this works. Thanks for your help.

[ebruneton]

Now I want to replace the Boxwith an Rc

pub struct Node {
    next: Option<Rc<Node>>,
}

As I expected termination cannot be proved since it is possible to create circular structures with this. Can I add a precondition expressing that there should be no cycles? Maybe with a predicate "there exists n>=0 such that node has length n"?

Related question: is it possible to define a View for some values of a struct only, namely those that are "well-formed" (no cycles, etc)? Maybe with a precondition on the View.view() method?

[jhjourdan]

One solution is to add a Snapshot field depth, which is an upper bound on the depth of the structure.

Then, you can restrict to "well formed" structures where the depth only decreases, and define ViewTy as an Option<...>, define view by using the depth as a variant, and return None as soon as this decreasing property does not hold during the recursion.

[ebruneton]

Thanks! I was able to use this idea. For instance, this works:

pub struct Node {
    next: Option<Rc<Node>>,
    depth: Snapshot<Int>,
}

#[logic]
#[variant(n.depth.inner())]
fn len(n: Node) -> Option<Int> {
    if n.depth.inner() < 0 {
        None
    } else {
        match n {
            Node {
                next: Some(node),
                depth,
            } => {
                if node.view().depth.inner() >= depth.inner() {
                    None
                } else {
                    match len(node.view()) {
                        Some(l) => Some(l + 1),
                        None => None,
                    }
                }
            }
            Node { next: None, depth } => Some(0),
        }
    }
}

impl Node {
    #[ensures(len(result) == Some(0))]
    pub fn nil() -> Self {
        Self {
            next: None,
            depth: snapshot!(0),
        }
    }
}

but I wonder why I can't move the check depth >= 0 to an invariant. This does not work:

impl Invariant for Node {
    #[open(self)]
    #[predicate]
    fn invariant(self) -> bool {
        self.depth.inner() >= 0
    }
}

#[logic]
#[variant(n.depth.inner())]
fn len(n: Node) -> Option<Int> {
    match n {
        Node {
            next: Some(node),
            depth,
        } => {
            if node.view().depth.inner() >= depth.inner() {
                None
            } else {
                match len(node.view()) {
                    Some(l) => Some(l + 1),
                    None => None,
                }
            }
        }
        Node { next: None, depth } => Some(0),
    }
}

[ebruneton]

Another strange case. The following can't be proved (the proof of the invariant of the result of cons fails):

pub struct Node {
    depth: Snapshot<Int>,
    next: Option<Rc<Node>>,
}

impl Invariant for Node {
    #[open(self)]
    #[predicate]
    fn invariant(self) -> bool {
        self.depth.inner() >= 0
    }
}

impl Node {
    pub fn cons(next: Rc<Node>) -> Self {
        Self {
            depth: snapshot!(next.view().depth.inner() + 1),
            next: Some(next),
        }
    }
}

But if I change Rc to Box the proof works fine.