Compile and Run: Const initialisations problems

[franck44]

What the problem is:

Here is a simple program:

module Foo {
    class A {

        const a : int 
        const b : int

        constructor(k : int, j : int) 
        {
            // a := k;
            // b := j;
            a, b := k, j;
        }
    }
    method Main() 
    {
        var o := new A(1, 2);
    }
}

With Dafny 3 (latest release), the compile and run commands produces an error:

> dafny /version
Dafny 3.0.0.30203
> dafny /compile:4 /trace examples/test-const-init.dfy 
Parsing examples/test-const-init.dfy
Coalescing blocks...
Inlining...

Running abstract interpretation...
  [0.066908 s]
[TRACE] Using prover: /Users/franck/local/dafny3.0.0/z3/bin/z3

Verifying Impl$$Foo.__default._default_Main ...
  [0.497 s, 1 proof obligation]  verified

Dafny program verifier finished with 1 verified, 0 errors
Errors compiling program:
(1780,7): error CS0200: Property or indexer 'A.a' cannot be assigned to -- it is read only

(1781,7): error CS0200: Property or indexer 'A.b' cannot be assigned to -- it is read only

However, if I understand the Dafny semantics correctly (and as the initial investigations below seen to support), this code should compile and it should be OK to assign a and b once in the constructor.

Preliminary investigations

I am running Dafny on a MacBook Pro, Big Sur, with latest version of dotnet.
Some initial simple tests produced the following results:

1. this compilation problem does not happen with dafny2.3.0 (Dafny 2.3.0.10506);
2. it also happens with dafny 3 pre-release3 (Dafny 3.0.0.30125)

Temporary fix
If the variables are not assigned concurrently in the constructor, there is no issue.
As a result replacing the code of the constructor by

 constructor(k : int, j : int) 
        {
            a := k;
            b := j;
            // a, b := k, j;
        }

solves the problem.

How the problem was discovered
The problem was discovered during the verification of the deposit smart contract.

[RustanLeino]

This is a bug. The simultaneous assignment should be allowed. Evidently, this is broken in all compiler back ends, which suggests the problem lies in Compiler.cs.