Ensure Dafny internal datatypes are used correctly in external code

[robin-aws]

This is admittedly vague, but we should at least be worried about sharing potentially-mutable array state with immutable Dafny sequences.

Acceptance criteria: a mechanism for ensuring Dafny state is properly encapsulated, even if that means slower initial runtime performance.

See also dafny-lang/dafny#440. It might be best to change the Dafny runtime implementation(s) in general to make it harder to misuse them.

[acioc]

Enforced C# Immutability (removed option to not be immutable): dafny-lang/dafny#559

[acioc]

Replace arrays in Seq with ImmutableArrays (C#): dafny-lang/dafny#564

[acioc]

The reason we can refer to subclasses directly is because everything is part of the same assembly. Normally, we can (and do) use internal https://docs.microsoft.com/en-us/dotnet/csharp/language-reference/keywords/accessibility-levels

However, in this case, our Dafny code and the Dafny runtime are both in the same assembly, so we can refer to the internals directly. Only way to change this is to change how we handle the Dafny dependency.

[acioc]

As a follow up, we likely want to merge dafny-lang/dafny.msbuild#10 and revert #227