VerCors-2.0.0-alpha-8 scoping errors when let-expression-defined variables are used inside triggers.

[Jankoekenpan]

Repro file:

void qux() {
    assert (\forall int i; 0 <= i && i < 10; (\let set<int> C = set<int> {}; {: C <= set<int> { i } :} ));
}

Expected output: Pass

Actual output:

[INFO] Starting verification
A rewrite caused the AST to no longer typecheck:
======================================
 At examples\scc\VerCors bugs!\let_expression.pvl:4:81:
--------------------------------------
    2  //does not work
    3  void qux() {
                                                                                      [-
    4      assert (\forall int i; 0 <= i && i < 10; (\let set<int> C = set<int> {}; {: C <= set<int> { i } :} ));
                                                                                       -]
    5  }
    6  
--------------------------------------
[1/2] This usage is out of scope,
--------------------------------------
 At examples\scc\VerCors bugs!\let_expression.pvl:4:61:
--------------------------------------
    2  //does not work
    3  void qux() {
                                                                  [-
    4      assert (\forall int i; 0 <= i && i < 10; (\let set<int> C = set<int> {}; {: C <= set<int> { i } :} ));
                                                                   -]
    5  }
    6  
--------------------------------------
[2/2] since it is declared here.
======================================

[bobismijnnaam]

The viper equivalent is the following:

function f(i: Int): Bool

method m(xs: Seq[Int], ys: Seq[Int])
requires (forall i: Int :: {C} let C == (f(i)) in (C in xs) == (C in ys))
{

}

Syntactically it makes sense why this is not allowed in viper. But from vercors point of view it makes sense. I think we need to inline let bindings if we want to support this...

[Jankoekenpan]

I verified the following repro using my fork of VerCors-1.4.0 (with automatic quantifier trigger generation disabled):

class Test {

    static void qux() {
       assert (\forall int i; 0 <= i && i < 10; (\let set<int> C = set<int> {}; {: C <= set<int>{i} :} ));
   }

}

Silver encoding:

// Generated on 2022-06-22 at 12:53:44
domain TYPE {
  
  unique function class_Test(): TYPE
  
  unique function class_java_DOT_lang_DOT_Object(): TYPE
  
  unique function class_EncodedGlobalVariables(): TYPE
  
  function directSuperclass(t: TYPE): TYPE
  
  function type_of(val: Ref): TYPE
  
  axiom Test_directSuperclass {
    directSuperclass(class_Test()) == class_java_DOT_lang_DOT_Object()
  }
  
  axiom EncodedGlobalVariables_directSuperclass {
    directSuperclass(class_EncodedGlobalVariables()) == class_java_DOT_lang_DOT_Object()
  }
}

function instanceof_TYPE_TYPE(t: TYPE, u: TYPE): Bool
  ensures result == (t == u || directSuperclass(t) == u)


method Test_qux_EncodedGlobalVariables(globals: Ref)
{
  // assert
  assert (forall i__1: Int :: 0 <= i__1 && i__1 < 10 ==> (let C__2 == (Set[Int]()) in (C__2 subset Set(i__1))))
}

This silver file also verifies successfully with the Viper VSCode extension.

Looking at the generated silver code, I think this means that VerCors-1.4.0 ignores the trigger entirely? If that is the case I can just remove these triggers from my main pvl file when using VerCors 2.0.0.

[bobismijnnaam]

Nice that it's not a blocker for you! We'll keep this issue open for further discussion.

[pieter-bos]

I think there is nothing to support here, but I'm happy to consider explicitly inlining let expressions (I don't think it will have a big impact once on the smt level)

On the topic of the error message, I'm still thinking about how to generalize this kind of error. Declaration's are all stored in a Declarator, which allows us to split kinds of declarations into two universes by the predicate: a reference to a declaration may only occur below its declarator:

• true: GlobalDeclaration, Variable, ParBlockDecl, ParInvariantDecl
• false: {Class|Model|ADT}Declaration, SendDecl, LabelDecl, (CDeclaration, CParam, JavaLocalDeclaration)

For the true part of this, the check is thus simply to see if an extracted node contains a reference to a declaration in a declarator below the place where the node is to be placed. For the false part, I guess there is always a defined scope but it's detached from the Declarator? E.g. ClassDeclaration references should not cross Program, LabelDecl should not cross the nearest ContractApplicable.

[pieter-bos]

We just inline let bindings in patterns now. For now we are not dealing with the validity of declaration references generally. My plan for that is that I think Refs should probably be nodes, and Rewriters should be able to have automatic context for this kind of thing (so you don't need to manually type out all kinds of Declarator for example)