OffchainLabs / arb-os

ArbOS operating system, to run at Layer 2 on Arbitrum chains. Also a compiler for Mini, the language in which ArbOS is written.
93 stars 20 forks source link

Add safe casting #477

Open RGates94 opened 3 years ago

RGates94 commented 3 years ago

Currently the only option we have for changing one data type to another is unsafecast, and this allows conversion between arbitrary types, creating the potential for errors and crashes.

I believe we should have 3 new casting types:

  1. A cast that ensures all possible values from the origin type can be interpreted as a valid in the destination type. For example we would allow a cast from a bool to a uint but not from a uint to a bool. This would always result in valid code so it would be preferable.
  2. A downcast that allows casting to subtypes, for example from impure func() to func() or any to bool, but does not allow casts between two types that do not have a subtyping relation, so downcasting from func() to uint would be forbidden.
  3. A assignablecast that only allows casts if the origin type is assignable to the destination type. This behavior is currently implicit in the = operator, and by adding this cast option we can remove this behavior, allowing for stronger type guarantees.

The primary benefits of adding these casting types are that we can maintain greater type safety in ArbOs, and making the code simpler to audit.

RGates94 commented 3 years ago

I think it might be better to allow downcast any time there are values in the origin type that can be cast to the destination type. For example, something like (bool, uint) to (uint, bool). As long as the uint in the second tuple field is 0 or 1, it would produce a valid cast. The cast from (bool, uint) to (bool, bool) would have identical requirements for safety, and would be allowed by the subtyping relation, but (bool, uint) -> (uint, bool) would not. Therefore, I think this is more flexible while also maintaining the same or a higher level of safety guarantees.