Update expressions

[msaaltink]

I'd like to see some expression for the result of assigning to a field of a struct. Traditionally, this has been something like S[.f := new_value]. These would map directly onto functions that already exist in the generated BPL, so it is just a case of making that available in move.

I've had a few cases where some field of a struct is updated, then some other function is called, e.g.

fun fiddle(s: &mut S) {
  ...
  S.f = S.f + 1;
  let x = mangle(s);
  ...
}

and where mangle has a precondition.

#[spec]
fun mangle(s: &S): u64 {
  requires(P(s));
  ...
}

So now for the spec of fiddle we need P(s') where s' is that updated value. Currently there is no good way to write that in move. In some cases, like struct S {f: u8, g: u8}, we can write S{f: s.f+1, s.g}, but in the cases I am dealing with, S has fields that are not copyable. In that case it is possibe to write S{f: s.f+1, prover::prover::val(&s.g)}, but this is not always desirable: this expression typically must be written inside the module defining S, while the expression is needed in some other module, so in the module defining S one needs to add functions something like this:

#[test_only]
public fun update_f(s: &S, f: ...): S {
  S { f, g = val(&s.g), h = val(&s.h), .. }
}

#[test_only]
public fun update_g(s: &S, g: ...): S {
  S { f = val(&s.f), g, h = val(&s.h), .. }
}

and so on. While it has been deemed OK to add test_only accessors to source files under analysis, these new definitions use the spec_only function prover::prover::val and I'm not sure if they could be compiled successfully by the normal move compiler. It is also rather tedious to write these when the struct has many fields.

As a strawman proposal, given that supporting the traditional S[.f := v] would require changes to the move compiler, one very simple idea would be for a function

native fun update<T,U>(s: &T, fieldname: vector<u8>, x: &U): &T;

so that we could write update(s, b"f", new_value). Of course the type checking is very weak for that, and the sui-prover, rather than the move compiler, would need to check that type T is a struct with a field "f" of type "U" or "&U".

I'm sure some more elegant notation can be found.

I have not needed it yet, but something similar for updated vectors might also be useful. Again the traditional syntax is something like v[i := x].