Fix: Support for double constant initialization in Dafny-to-Rust

[MikaelMayer]

This PR fixes #5642
I added the corresponding test.

By submitting this pull request, I confirm that my contribution is made under the terms of the MIT license.

[kbuaaaaaa]

Hi! This is Bua from the CI fuzzing project.

Not sure if this is related but the following code produces error only in rust backend.
The error showed up after you fixed the const initialisation.

original.dfy:

trait T0 {
	const f8 : bool
}
class C0 extends T0 {
	constructor (f8 : bool) {
		this.f8 := f8;
	}	
}

method Main() {
	var c0 := new C0(false);
	print c0.f8, "\n";
}

Command:

dafny build original.dfy -t rs

Output:

Dafny program verifier finished with 1 verified, 0 errors
error[E0046]: not all trait items implemented, missing: `f8`
  --> src/original.rs:48:3
   |
23 |       fn f8(&self) -> bool;
   |       --------------------- `f8` from trait
...
48 | /   impl T0
49 | |     for C0 {}
   | |__________^ missing `f8` in implementation

error[E0308]: mismatched types
  --> src/original.rs:35:7
   |
34 |     pub fn f8(&self) -> bool {
   |                         ---- expected `bool` because of return type
35 |       ::dafny_runtime::Object::<_>::from_ref(self)
   |       ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ expected `bool`, found `Object<C0>`
   |
   = note: expected type `bool`
            found struct `Object<C0>`

Some errors have detailed explanations: E0046, E0308.
For more information about an error, try `rustc --explain E0046`.
error: could not compile `original` (bin "original") due to 2 previous errors
Error while compiling Rust files. Process exited with exit code 101

[MikaelMayer]

Hi! This is Bua from the CI fuzzing project.

Not sure if this is related but the following code produces error only in rust backend. The error showed up after you fixed the const initialisation.

original.dfy:

trait T0 {
	const f8 : bool
}
class C0 extends T0 {
	constructor (f8 : bool) {
		this.f8 := f8;
	}	
}

method Main() {
	var c0 := new C0(false);
	print c0.f8, "\n";
}

Command:

dafny build original.dfy -t rs

Output:

Dafny program verifier finished with 1 verified, 0 errors
error[E0046]: not all trait items implemented, missing: `f8`
  --> src/original.rs:48:3
   |
23 |       fn f8(&self) -> bool;
   |       --------------------- `f8` from trait
...
48 | /   impl T0
49 | |     for C0 {}
   | |__________^ missing `f8` in implementation

error[E0308]: mismatched types
  --> src/original.rs:35:7
   |
34 |     pub fn f8(&self) -> bool {
   |                         ---- expected `bool` because of return type
35 |       ::dafny_runtime::Object::<_>::from_ref(self)
   |       ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ expected `bool`, found `Object<C0>`
   |
   = note: expected type `bool`
            found struct `Object<C0>`

Some errors have detailed explanations: E0046, E0308.
For more information about an error, try `rustc --explain E0046`.
error: could not compile `original` (bin "original") due to 2 previous errors
Error while compiling Rust files. Process exited with exit code 101

This is not related. Constant on traits are not yet supported on the Dafny to Rust code generator

[alex-chew]

LGTM