I didn't say it is. Please carefully re-read what I wrote. The information density is very high. I'll write this down in a blog post eventually which explains this in 10x as many words, but I don't have the time currently to write that all up so right now I can only offer the highly condensed version, sorry.
The state transition I am describing transitions the AM state. If there's state that the AM cannot see nor observe, not even indirectly, the asm block can do with it whatever it wants. Ofc in reality the AM will eventually be able to observe the state change, but typically one has to insert a sort of fence to ensure that the act of doing the state change is ordered-before anything that may depend on it; in AM terms, that fence then performs some sort of reorganization on the abstract state (e.g. making some memory available), and that has to be expressible in Rust terms.
Reading or writing /proc/self/mem
can easily cause UB. This is a well-known soundness hole, and going down that rabbit hole is not helpful for this discussion.
No.
No, we cannot. The compiler can do reasoning based on what other code can or cannot observe. If you use inline asm to extend the observational power of other code, you are potentially breaking compiler assumptions.
So in general it really has to be any kind of interaction with or dependency on the AM state that is so carefully guarded. As I already said, freeze
is a somewhat special case in that I am not aware of optimizations that it actually breaks, but I would be extremely hesitant to permit any kind of deviation from the recipe laid out above.
The main reason it cannot have angelic non-determinism is that there is no operation you can write in pure Rust that is guaranteed to be angelically non-deterministic. Angelic non-determinism has global ramifications, e.g. you cannot move a malloc
down across an unknown function call if that call may make an angelic choice. This kind of issue is exactly the reason why the inline asm block's action on the AM state must be expressible in Rust code.
I invite anyone who disagrees with the inline asm and FFI rules I laid down to come up with their own rules and then convincingly argue that any inline asm block or FFI call following those rules is compatible with every current and future optimization and analysis the compiler may make. I am fairly convinced that it is not possible, in general, to relax the requirements I described. I also think the vast majority of inline asm usages are actually compatible with these rules, much more so than people realize, but it requires a very particular kind of thinking to fit the actions of an inline asm block into this framework.
I also apologize for being so terse, but I am extremely short on time currently so I just don't have the time to spell this out in more detail.