Missing preconditions in Boogie code generation for anonymous functions

[jtristan]

Dafny version

4.1.0

Code to produce this issue

datatype Pack<T> = Pack(ghost c: T)

method m()
  ensures false
{
  var r := new (array<Pack<() ~> bool>>)[1];
  r[0] := new (Pack<() ~> bool>)[1];
  r[0][0] := Pack(() => false);
  var tf := Pack(() requires r[0].Length != 0 reads r, r[0], r[0][0].c.reads  => (
                     if r[0][0].c.requires() then !r[0][0].c() else false
                   ));
  r[0][0] := tf;
}

Command to run and resulting output

vscode

What happened?

Despite the precondition, the reads clause cannot be prove to be within bounds. Indeed, the Boogie code for the well-formedness check is wrong:

CheckWellformedness[[ reads_clause ]];
CheckWellformedness[[ precondition ]];
if (precondition) {
  CheckWellformedness[[ body ]];
}

It should instead be:

CheckWellformedness[[ precondition ]];
if (precondition) {
  CheckWellformedness[[ reads_clause ]];
  CheckWellformedness[[ body ]];
}

In a little more detail, the well-formedness of the precondition and reads clause perform reads checks. Each time a reads check is done, a boolean variable (with a name like b$reqreads#0) is set. Then, those booleans are asserted to be true. In the correct-way code I showed above, these variables should be assigned while checking the well-formedness of precondition and reads_clause, and then they should be asserted just after where I wrote CheckWellformedness[[ reads_clause ]];.

What type of operating system are you experiencing the problem on?

Mac

[keyboardDrummer]

The reproducing program is no longer accepted by Dafny 4.6:

/Users/rwillems/Documents/Sync/Temp/HasProjectFile2/newTypeSystem.dfy(8,10): Error: To prevent the creation of non-terminating functions, storing functions with read effects into memory is disallowed
  |
8 |   r[0][0] := Pack(() => false);
  |           ^^

/Users/rwillems/Documents/Sync/Temp/HasProjectFile2/newTypeSystem.dfy(12,10): Error: To prevent the creation of non-terminating functions, storing functions with read effects into memory is disallowed
   |
12 |   r[0][0] := tf;
   |           ^^

@jtristan could you confirm that this does not resolve the issue you reported here?