From 2e0580c0a20f23dbe1d415a31aa9ce99e3d14a54 Mon Sep 17 00:00:00 2001 From: Ralf Jung Date: Tue, 12 Apr 2022 08:38:10 -0400 Subject: [PATCH] tweaks --- personal/_posts/2022-04-11-provenance-exposed.md | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/personal/_posts/2022-04-11-provenance-exposed.md b/personal/_posts/2022-04-11-provenance-exposed.md index b37344c..24b3402 100644 --- a/personal/_posts/2022-04-11-provenance-exposed.md +++ b/personal/_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. -- 2.30.2