linear type-checking doesn't handle simultaneity right

[tjhance]

Right now, Dafny lets this pass:

linear datatype Foo = Foo 

method f(linear x: Foo)
returns (linear x': Foo)
{
  x' := x;
  linear var y: Foo;

  y, x' := x', y;
}

but not this:

method g(linear x: Foo, linear y: Foo)
returns (linear x': Foo, linear y': Foo)
{
  x' := x;
  y' := y;

  x', y' := y', x'; 
}

It should be the other way around.

[Chris-Hawblitzel]

Due to the way Dafny resolves multi-assignment, I just disabled multiple-right-hand-side assignment to linear variables for soundness's sake. Multiple assignment from method calls still works, so you can do:

method Assign2<A, B>(linear a: A, linear b: B) returns(linear a': A, linear b': B)
  ensures a' == a;
  ensures b' == b;
{
  a' := a;
  b' := b;
}

method f(linear x: int, linear y: int) returns (linear x': int, linear y': int)
{
  x' := x;
  y' := y;

  x', y' := Assign2(y', x'); 
}

[tjhance]

ok cool. I'll leave this issue up as a note that it would still be great to support the latter example at some point