AssertionError without counterexample

[RCoeurjoly]

When I execute nagini nagini.py --counterexample on the following piece of code:

from typing import Optional, List, Tuple
from nagini_contracts.contracts import *

class Node:
    def __init__(self, function_name: str, children:List['Node']) -> None:
        self.function_name = function_name # type: str
        self.children = children # type: List['Node']
        Ensures(Acc(self.function_name) and self.function_name is function_name and
                Acc(self.children) and self.children is children)

@Pure
def can_node_be_compressed(marked_execution_tree: 'Node') -> Tuple[bool, int]:
    """Searches for the longest compression possible. Returns:
    - bool: True if can be compressed. False otherwise
    - int: If it can be compressed, number of nodes to compress"""
    Requires(Acc(marked_execution_tree.children, 1/2))
    Requires(Acc(list_pred(marked_execution_tree.children)))
    Requires(Forall(int, lambda i: Implies(i >= 0 and i < len(marked_execution_tree.children), Acc(marked_execution_tree.children[i].function_name))))
    Requires(Acc(marked_execution_tree.function_name, 1/2))
    # Ensures(Implies(Result()[1] == 0, Result()[0] is False))
    # Ensures(Implies(Result()[1] > 0, Result()[0] is True))
    if len(marked_execution_tree.children) != 1:
        return False, 0
    if marked_execution_tree.children[0].function_name != marked_execution_tree.function_name:
        return False, 0
    _, downstream_length = can_node_be_compressed(marked_execution_tree.children[0])
    return True, downstream_length + 1

I get the following output:

Traceback (most recent call last): File "/home/drcoeurjoly/.cache/pypoetry/virtualenvs/declarative-debugger-for-cpp-3Q8a3Jio-py3.8/bin/nagini", line 8, in sys.exit(main()) File "/nix/store/06a4ly3dn289ksmgic7r9gal439bb01n-python3.8-nagini-0.9.0/lib/python3.8/site-packages/nagini_translation/main.py", line 352, in main translate_and_verify(args.python_file, jvm, args, arp=args.arp, base_dir=args.base_dir) File "/nix/store/06a4ly3dn289ksmgic7r9gal439bb01n-python3.8-nagini-0.9.0/lib/python3.8/site-packages/nagini_translation/main.py", line 359, in translate_and_verify modules, prog = translate(python_file, jvm, selected=selected, sif=args.sif, base_dir=base_dir, File "/nix/store/06a4ly3dn289ksmgic7r9gal439bb01n-python3.8-nagini-0.9.0/lib/python3.8/site-packages/nagini_translation/main.py", line 131, in translate prog = translator.translate_program(modules, sil_programs, selected, File "/nix/store/06a4ly3dn289ksmgic7r9gal439bb01n-python3.8-nagini-0.9.0/lib/python3.8/site-packages/nagini_translation/translator.py", line 100, in translate_program return self.prog_translator.translate_program(modules, sil_progs, ctx, File "/nix/store/06a4ly3dn289ksmgic7r9gal439bb01n-python3.8-nagini-0.9.0/lib/python3.8/site-packages/nagini_translation/translators/program.py", line 1306, in translate_program functions.append(self.translate_function(function, ctx)) File "/nix/store/06a4ly3dn289ksmgic7r9gal439bb01n-python3.8-nagini-0.9.0/lib/python3.8/site-packages/nagini_translation/translators/abstract.py", line 167, in translate_function return self.config.method_translator.translate_function(func, ctx) File "/nix/store/06a4ly3dn289ksmgic7r9gal439bb01n-python3.8-nagini-0.9.0/lib/python3.8/site-packages/nagini_translation/translators/method.py", line 294, in translate_function body = self.translate_exprs(actual_body, func, ctx) File "/nix/store/06a4ly3dn289ksmgic7r9gal439bb01n-python3.8-nagini-0.9.0/lib/python3.8/site-packages/nagini_translation/translators/abstract.py", line 110, in translate_exprs return self.config.pure_translator.translate_exprs(nodes, function, ctx) File "/nix/store/06a4ly3dn289ksmgic7r9gal439bb01n-python3.8-nagini-0.9.0/lib/python3.8/site-packages/nagini_translation/translators/pure.py", line 281, in translate_exprs wrappers = self._translate_to_wrappers(nodes, ctx) File "/nix/store/06a4ly3dn289ksmgic7r9gal439bb01n-python3.8-nagini-0.9.0/lib/python3.8/site-packages/nagini_translation/translators/pure.py", line 239, in _translate_to_wrappers return flatten([self.translate_pure([], node, ctx)for node in nodes]) File "/nix/store/06a4ly3dn289ksmgic7r9gal439bb01n-python3.8-nagini-0.9.0/lib/python3.8/site-packages/nagini_translation/translators/pure.py", line 239, in return flatten([self.translate_pure([], node, ctx)for node in nodes]) File "/nix/store/06a4ly3dn289ksmgic7r9gal439bb01n-python3.8-nagini-0.9.0/lib/python3.8/site-packages/nagini_translation/translators/pure.py", line 78, in translate_pure return visitor(conds, node, ctx) File "/nix/store/06a4ly3dn289ksmgic7r9gal439bb01n-python3.8-nagini-0.9.0/lib/python3.8/site-packages/nagini_translation/translators/pure.py", line 136, in translate_pure_Assign assert isinstance(node.targets[0], ast.Name) AssertionError

The assertion fails because elements of children are not Nodes? Because that is what I intend to express in the types of init.

[marcoeilers]

Pure functions can only contain a few very specific kinds of statements, in particular, only assignments with a single variable on the left hand side. Commit a2a19df7d833e67841e03c9885869c3dddef3327 adds a proper error message for this.

In your case, I think you could basically just drop the boolean return value from the function, or you could assign the result of the recursive call to a single variable x, and then explicitly return x[1] + 1 in the line below.