chore-rust-operators-followup

[MikaelMayer]

Description

This PR mostly brings small incremental changes to the compiler to make it possible to develop the Dafny-to-Rust code generator.

• Dafny files in DafnyCore now compatible with the new resolver
• Fixed typos
• The internal field prefix has been refactored and becomes "i" instead of "". Possibility to switch back for previous behavior for compilers other than Rust, just testing for now that this prefix change works. Since the Dafny to Rust compiler will encode extra fields with an internal prefix, user-defined names cannot just be prefixed with "" when needed to avoid name collision.
• Ability for the Code Generator to define a custom receiver (in prevision of calling constructor methods for the Dafny to Rust compiler). This is only a refactoring, the override will come in an upcoming PR.
• "NeedsCustomReceiver" now really encloses the logic for whether a custom receiver is needed, decision about traits is done inside (and outside in the rare cases). This will make it possible for Dafny-to-Rust to define custom receivers
• ArrayIndexToInt is now emitted instead of converted to string
• TrdDividedBlockStmt has its own conversion pipeline (before it's going to be overriden in the Dafny to Rust compiler)
• Rust code generator now takes options as argument, supports two kinds of string
• The dfy-to-cs script won't proceed to class extraction if the translation fails.

How has this been tested?

Existing tests should pass for most refactorings.
I will not switch to the new type checker until a few PRs.

For the refactoring on NeedsCustomReceiver, I proved the equivalence for SinglePassCompiler, the Go compiler and the C# compiler with inheritance via the following proven Dafny program:

datatype Member = Member(
  Static: bool,
  InNewtype: bool,
  InTraitDecl: bool,
  IsConstantFunctionMethod: bool,
  InDatatype: bool,
  IsDatatypeMemberWithCustomReceiver: bool,
  IsDatatypeMemberWithCustomReceiverCSharp: bool
)

predicate NeedsCustomReceiverOld(
  m: Member,
  X: bool)
{
  if m.Static then false else
  if m.InNewtype then true else
  if m.InTraitDecl then m.IsConstantFunctionMethod else
  if m.InDatatype then m.IsDatatypeMemberWithCustomReceiver else
  X
}

predicate NeedsCustomReceiverNotTrait(
  m: Member,
  X: bool)
{
  if m.Static then false else
  if m.InNewtype then true else
  if m.InTraitDecl then false else
  if m.InDatatype then m.IsDatatypeMemberWithCustomReceiver else
  X
}

predicate NeedsCustomReceiverInTrait(
  m: Member,
  X: bool) {
  if m.Static then false else
  m.InTraitDecl && m.IsConstantFunctionMethod
}

predicate NeedsCustomReceiver(
  m: Member,
  X: bool)
{
  NeedsCustomReceiverNotTrait(m, X)
    || NeedsCustomReceiverInTrait(m, X)
}

lemma Equivalence(
  m: Member,
  X: bool) 
  ensures NeedsCustomReceiverOld(m, X)
      <==> NeedsCustomReceiver(m, X)
{
}

lemma Equivalence2(
  m: Member,
  X: bool) 
  requires (m.InNewtype && !m.InTraitDecl && !m.InDatatype) ||
            (!m.InNewtype && m.InTraitDecl && !m.InDatatype) ||
            (!m.InNewtype && !m.InTraitDecl && m.InDatatype) ||
            (!m.InNewtype && !m.InTraitDecl && !m.InDatatype)
  ensures !m.InTraitDecl && NeedsCustomReceiverOld(m, X) <==>
          NeedsCustomReceiverNotTrait(m, X)
{
}

// C# case and override

predicate NeedsCustomReceiverOldCSharp(
  m: Member,
  X: bool) {
  if !m.Static && m.InDatatype && m.IsDatatypeMemberWithCustomReceiverCSharp then
    true
  else
    NeedsCustomReceiverOld(m, X)
}

predicate NeedsCustomReceiverNotTraitCsharp(
  m: Member,
  X: bool)
{
  if m.Static then false else
  if m.InNewtype then true else
  if m.InTraitDecl then false else
  if m.InDatatype then
    m.IsDatatypeMemberWithCustomReceiverCSharp // Override might return true before base case
    || m.IsDatatypeMemberWithCustomReceiver else
  X
}

predicate NeedsCustomReceiverCSharp(
  m: Member,
  X: bool)
{
  NeedsCustomReceiverNotTraitCsharp(m, X)
    || NeedsCustomReceiverInTrait(m, X)
}

lemma Equivalence3(
  m: Member,
  X: bool) 
  requires (m.InNewtype && !m.InTraitDecl && !m.InDatatype) ||
            (!m.InNewtype && m.InTraitDecl && !m.InDatatype) ||
            (!m.InNewtype && !m.InTraitDecl && m.InDatatype) ||
            (!m.InNewtype && !m.InTraitDecl && !m.InDatatype)
  ensures !m.InTraitDecl && NeedsCustomReceiverOldCSharp(m, X)
     <==> NeedsCustomReceiverNotTraitCsharp(m, X)
{
}

lemma Equivalence4(
  m: Member,
  X: bool) 
  requires (m.InNewtype && !m.InTraitDecl && !m.InDatatype) ||
            (!m.InNewtype && m.InTraitDecl && !m.InDatatype) ||
            (!m.InNewtype && !m.InTraitDecl && m.InDatatype) ||
            (!m.InNewtype && !m.InTraitDecl && !m.InDatatype)
  ensures NeedsCustomReceiverOldCSharp(m, X)
     <==> NeedsCustomReceiverCSharp(m, X)
{
}

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

[keyboardDrummer]

I prefer using a pure function instead of an impure writer one, which would look like:

protected override ConcreteSyntaxTree ArrayIndexToInt(ConcreteSyntaxTree index) => 
    ConcreteSyntaxTree.Create($@"{HelperModulePrefix}IntOf(""{index}"")");

[MikaelMayer]

I did not know this syntax, but it looks great! I would happily use it. I found how I could take your snippet verbatim and it would work in this case, but looking forward at how this code snippet will be used for the Dafny-to-Dafny compiler, I found it's preferable to leave it as it for now. The Dafny-to-Dafny compiler requires the construction of the outer tree builder before the construction of the inner tree builder and uses fields to keep track of the current tree. I know it's cumbersome and at one point I'd like to revisit that entirely to use more of a pure syntax, but I am not prioritizing that right now.

[keyboardDrummer]

I don't fully understand. If Dafny user-defined names can not contain _, why do we need to do something special to distinguish them from compiler-generated names that contain _ ?

[MikaelMayer]

Dafny user-defined names can contain _, it's just that they are escaped like this __, so that ? becomes _q and ' becomes _k. It makes the encoding bijective. Moreover, Dafny identifiers cannot start with _, so anything starting with a _ in generated code is never in collision with user-defined Dafny names, this is what the original InternalFieldPrefix is about (its value was _). So far so good, no issue.

However, if one wants to add variables in the code that are not defined in Dafny (e.g. for instrumentation), one incur the risk of colliding with user-defined Dafny variables. For example, if the internal value of constant is a field prefixed with _`, a user writing this:

class A {
  const s
}

will get a C# class like this:

class A {
  private int _s;
  public int s => {
    // Compute _s if not computed.
    return _s;
  }
}

Now let's say I want to write a field, like "time" for instrumentation. If I prefix it with _, like _time, it might collide with a user-defined constant name time.
Moreover, if one wants to keep an encoding where a_b is translated to a_b (e.g. if an identifier is Rust-friendly in my case, we don't change it), then there is no possibility to avoid collisions with an internal prefix like _ for any field and variable name. For example, let's say I add a private field _a_b, then a user defining a constant a_b will collide with my private field.

To avoid that issue, it suffices to increase the length of the internal prefix, which I did here; Now I can add any private field that starts with _set_ for example (which I do for constructor variable initialization later) and I know it won't collide with any user-defined private field. In some sense, it serves as a namespace.
I could as well have put it with two underscores, __, I'm pretty sure it would work too, but I haven't tried; At least this prefix is easily recognizable and discoverable in case of bugs.

By the way, In this PR I'm putting the internal prefix for all compilers to _i_ but I could put it back to _ for all of them except the Rust compiler if we wanted to. The fact however that it captures all the places of where this prefix is used makes it more maintainable in the future, e.g. in case we want to generate more idiomatic output in the future for other compilers.