Refining a module method with linear parameters causes linearity errors

[rtjohnso]

If a module A implements a method with linear or linear inout parameters, and a module B refines A and overrides the method implementation, then dafny generates linearity errors. shared parameters seem to be ok.

module A {
  // Error: linear variable <<old_data>> is unavailable here
  // Error: variable must be unavailable before assignment
  method Foo(linear inout data: seq<int>)
  {
  }
  method Bar(linear data: seq<int>) returns (linear result: seq<int>)
  {
    // Error: linear variable <<data>> is unavailable here
    // Error: variable must be unavailable before assignment
    result := data;
  }
  method Baz(shared data: seq<int>)
  {
  }
}

module B refines A {
  method Foo(linear inout data: seq<int>)
  {
  }
  method Bar(linear data: seq<int>) returns (linear result: seq<int>)
  {
    result := data;
  }
  method Baz(shared data: seq<int>)
  {
  }
}

[parno]

@rtjohnso mentioned that this works in 3748f6c but breaks in 183116c. Is that right?

If so, that's quite odd, since the changes in 183116c (a) skip compiling Functors (which aren't present here), and (b) change how ApplyFunctor works, which also isn't relevant here.

[rtjohnso]

I can't reproduce that result. My bad. In fact, picking a few random commits, even all the way back to inout-merge (last updated May 19), suggests that this never worked.

…

On Tue, Aug 17, 2021 at 11:15 AM Bryan Parno ***@***.***> wrote: @rtjohnso <https://github.com/rtjohnso> mentioned that this works in 3748f6c <3748f6c> but breaks in 183116c <183116c>. Is that right? If so, that's quite odd, since the changes in 183116c <183116c> (a) skip compiling Functors (which aren't present here), and (b) change how ApplyFunctor works, which also isn't relevant here. — You are receiving this because you were mentioned. Reply to this email directly, view it on GitHub <#39 (comment)>, or unsubscribe <https://github.com/notifications/unsubscribe-auth/AA45FRISIWJQHHSR4NNXDO3T5KRMZANCNFSM5CKKS4TA> . Triage notifications on the go with GitHub Mobile for iOS <https://apps.apple.com/app/apple-store/id1477376905?ct=notification-email&mt=8&pt=524675> or Android <https://play.google.com/store/apps/details?id=com.github.android&utm_campaign=notification-email> .

[parno]

@Chris-Hawblitzel points out that Dafny objects to this more generally:

module A {
  method Bar(data: int) returns (result: int)
  {
    result := data;
  }
}

module B refines A {
  method Bar(data: int) returns (result: int)
  {
    result := data;
  }
}

results in

Error: refinement method cannot assign to variable defined in parent module ('result')

I'm not sure that Dafny actually lets you provide a method body in a refining module (B) if it already had a body in the parent module (A), or at least not as a general feature. Do you need this ability for the parser?

[rtjohnso]

That seems to be a quirk about assigning to variables. The following equivalent code passes: ``` module A { method Foo() returns (result: char) { print "Running A\n"; result := 'A'; } } module B refines A { method Foo() returns (result: char) { print "Running B\n"; return 'B'; } } method Main() { var a := A.Foo(); print a; print "\n"; var b := B.Foo(); print b; print "\n"; } ``` It compiles, runs, and outputs: ``` Running A A Running B B ``` So maybe overriding methods is not completely supported, but it sorta is? Also, I could probably work around it if we didn't have it.

…

On Tue, Aug 17, 2021 at 7:42 PM Bryan Parno ***@***.***> wrote: @Chris-Hawblitzel <https://github.com/Chris-Hawblitzel> points out that Dafny objects to this more generally: module A { method Bar(data: int) returns (result: int) { result := data; } } module B refines A { method Bar(data: int) returns (result: int) { result := data; } } results in Error: refinement method cannot assign to variable defined in parent module ('result') I'm not sure that Dafny actually lets you provide a method body in a refining module (B) if it already had a body in the parent module (A), or at least as a general feature. Do you need this ability for the parser? — You are receiving this because you were mentioned. Reply to this email directly, view it on GitHub <#39 (comment)>, or unsubscribe <https://github.com/notifications/unsubscribe-auth/AA45FRMLSUD4CVI2LLTUPETT5MMZXANCNFSM5CKKS4TA> . Triage notifications on the go with GitHub Mobile for iOS <https://apps.apple.com/app/apple-store/id1477376905?ct=notification-email&mt=8&pt=524675> or Android <https://play.google.com/store/apps/details?id=com.github.android&utm_campaign=notification-email> .

[parno]

Weird! What's the use case you want to use it for? Judging from commit density, the Amazon folks have been using Dafny's classes and traits a fair bit, so if that would better fit your use case, they might be usable by this point. Of course, we'd need to update the C++ backend to accommodate them, so it won't compile right away.