Simplification of @trusted

[Ola Fosheim Grøstad]

On Thursday, 17 June 2021 at 19:25:51 UTC, ag0aep6g wrote:
> On 17.06.21 20:46, Ola Fosheim Grøstad wrote:
>> What about it isn't safe? It is provably safe? Meaning, I can 
>> do a formal verification of it as being safe!?
>
> `offset` is an input to `get` (via `this`). `offset` is an int, 
> so all possible values (int.min through int.max) are considered 
> "safe values". `get` exhibits undefined behavior when `offset` 
> is greater than 1. A function that can exhibit undefined 
> behavior when called with only safe values cannot be @trusted.

But this.offset can provably only hold the value 0 or 1. What is 
the point of manually auditing @trusted if one impose arbitrary 
requirements like these? So I am basically forced to use a bool 
to represent offset for it to be considered safe?

One should start by defining invariants that will keep the class 
safe.

Then one should audit all methods with respect to the invariants.

The invariant is that this.offset cannot hold a value different 
from 0 and 1. And it is easy to prove.

(I asssume here that all methods are marked as @trusted)