From: Ralf Jung Date: Tue, 12 Apr 2022 12:38:10 +0000 (-0400) Subject: tweaks X-Git-Url: https://git.ralfj.de/web.git/commitdiff_plain/4b32c2643ee1b60a8ef331949fc9f7cdd06b50c6?ds=inline;hp=1b47e7e5661b41b7708ce528a409ff7e412fa147 tweaks --- diff --git a/ralf/_posts/2022-04-11-provenance-exposed.md b/ralf/_posts/2022-04-11-provenance-exposed.md index b37344c..24b3402 100644 --- a/ralf/_posts/2022-04-11-provenance-exposed.md +++ b/ralf/_posts/2022-04-11-provenance-exposed.md @@ -345,8 +345,8 @@ Here, too, my vision for Rust aligns very well with the direction C is taking. (The set of valid guesses in C is just a lot more restricted since they do not have `wrapping_offset`, and the model does not cover `restrict`. That means they can actually feasibly give an algorithm for how to do the guessing. They don't have to invoke scary terms like "angelic non-determinism", but the end result is the same -- and to me, the fact that it is equivalent to angelic non-determinism is what justifies this as a reasonable semantics. -Presenting this as a concrete algorithm to pick a suitable provenance is then just a stylistic choice. -Kudos go to Michael Sammler for opening my eyes to this interpretation of "user disambiguation".) +Presenting this as a concrete algorithm to pick a suitable provenance is then just a stylistic choice.) +Kudos go to Michael Sammler for opening my eyes to this interpretation of "user disambiguation", and arguing that angelic non-determinism might not be such a crazy idea after all. What is left is the question of how to handle pointer-integer transmutation, and this is where the roads are forking. PNVI-ae-udi explicitly says loading from a union field at integer type exposes the provenance of the pointer being loaded, if any.