Support adapting a C# MemoryStream as a Dafny.Sequence

[robin-aws]

This would be similar to the existing optimization in the Java runtime to allow adapting a java.lang.String as a DafnySequence using the StringDafnySequence adaptor class. In both cases the motivation is similar: avoiding having to copy values when they cross the FFI between native target language code and cross-compiled Dafny code.

This would selectively introduce a soundness risk, and to a greater degree than wrapping a string. MemoryStream exposes a CanWrite property, which if false means that it is not possible to mutate the underlying data through the MemoryStream API. However, you can create a new MemoryStream that wraps (a range of) an arbitrary byte[] value, which is intentionally not copied in the constructor. That means it will be possible to accidentally mutate a sequence's data, which obviously breaks the semantics of Dafny and leads to undefined behavior. Wrapping a java.lang.String is substantially safer, as that datatype DOES copy values on construction and does not mutate or expose its underlying byte[].

Also note that as per the name, MemoryStream is designed to be more of a "sequential stream backed by a byte array" rather than a "random-access sequence of bytes". It is possible to read a single byte at an arbitrary index in O(n) time, but the constant factor will be higher than ideal, and the code will not be thread-safe unless we apply additional synchronization, as it will look something like the snippet below. This could be avoided by requiring that the wrapped stream also supports GetBuffer(), which exposes the internal array, but that would be an even bigger soundness risk.

class MemoryStreamSequence : ISequence<byte> {
  private readonly MemoryStream memoryStream;
  
  // ...
  public T Select(int index) {
    memoryStream.Position = index;
    return (byte)memoryStream.ReadByte();
  }
}

It will be worth considering supporting more sequential access of sequences in Dafny itself, so that we can leverage the more efficient access patterns abstractions like MemoryStream (or its supertype Stream for that matter). dafny-lang/libraries#37 and dafny-lang/rfcs#9 both aim to progress towards supporting implementations of sequences that do not necessarily support efficient random access.