This PR is the result of many discussions with @romac @gsps @vkuncak. There was also great support by @jad-hamza on the Stainless side of things, thanks!
The PR brings the mutability support of rust-stainless closer to Rust's semantics by dropping the var annotation on fields.
Closes #157. Closes #99 because now, all fields can be mutated with mut at binding.
This is a big step for #92 and brings us closer to #140.
Theory
The safety of what we do in this PR, mainly on this single line change is guaranteed by the following theoretical argument:
Rust has either 1 mutable reference or many shared, immutable, aliasable borrows
Stainless allows 1 reference to a mutable object but we can create aliases with freshCopy at our own risk
Thanks to Rust, we know that when we borrow something immutably (BorrowKind::Shared), it’s aliasable and we can therefore safely freshCopy it.
There are 3 other places, where freshCopy is/was introduced:
For function parameters that are taken by-value. It's safe to freshCopy them because the by-value/move semantics guarantee that they are owned i.e. there are no other references to them.
Return values are freshCopy'd to avoid aliasing. This is safe (currently) because we only support returning by-value or by shared, immutable reference.
stainless::Map is a special case. In order to get support for mutable value types, we needed to refactor the map extraction. Behind the immutable Rust interface that resides in libstainless the map is now extracted as MutableMap. To combat aliasing, the insert and remove method now consume self. This allows on the extraction side, to extract for example let b = a.insert(0, 1); as the following in Scala:
val b: MutableMap[UInt32, Option[UInt32]] = freshCopy({
val map: MutableMap[UInt32, Option[UInt32]] = freshCopy(a)
map(0) = Some[UInt32](1)
map
})
This PR is the result of many discussions with @romac @gsps @vkuncak. There was also great support by @jad-hamza on the Stainless side of things, thanks!
The PR brings the mutability support of
rust-stainless
closer to Rust's semantics by dropping thevar
annotation on fields.Closes #157. Closes #99 because now, all fields can be mutated with
mut
at binding. This is a big step for #92 and brings us closer to #140.Theory The safety of what we do in this PR, mainly on this single line change is guaranteed by the following theoretical argument:
freshCopy
at our own riskBorrowKind::Shared
), it’s aliasable and we can therefore safelyfreshCopy
it.There are 3 other places, where
freshCopy
is/was introduced:For function parameters that are taken by-value. It's safe to
freshCopy
them because the by-value/move semantics guarantee that they are owned i.e. there are no other references to them.Return values are
freshCopy
'd to avoid aliasing. This is safe (currently) because we only support returning by-value or by shared, immutable reference.stainless::Map
is a special case. In order to get support for mutable value types, we needed to refactor the map extraction. Behind the immutable Rust interface that resides inlibstainless
the map is now extracted asMutableMap
. To combat aliasing, theinsert
andremove
method now consumeself
. This allows on the extraction side, to extract for examplelet b = a.insert(0, 1);
as the following in Scala: