#rust-lang

alercah: If bar fails to uphold its invariants, there are two cases

If bar is trusted, this is a failure of bar

If bar is not trusted, this is a failure of foo

right

Either way, the UB is in foo, not in bar

so an unsafe operation is one that warns "there are some invariants which must be maintained or else I may cause UB", as opposed a safe one which promises no UB

Trusted isn't about "I don't cause UB" - it's about "You can gate your own UB on my invariants"

right

code using an unsafe operation must prove that it does not cause UB; for this purpose it is permitted to rely on invariants of trusted functions

currently, the compiler requires that safe fns must explicitly state that they have discharged the obligation with unsafe {}

unsafe fns are not required to do so

this seems to me like if we don't allow any inference, it's merely an opinionated decision

there is no inherent reason that safe fns require unsafe {}, or that unsafe fns do not

if unsafe is *specifically* about UB, then there is no reason to write an fn function that doesn't in turn rely on unsafe behaviour

unsafe *could* be reused by safe Rust code for maintaining internal invariants, rather than just UB invariants

in that case, unsafe fns that did not rely on any further unsafe behaviour would make sense

requiring unsafe {} inside unsafe fns would explicitly demarcating where the code is maintaining proof obligations

*would be

I don't think this would be worthless, because it narrows the scope of where those proof obligations lie

but it's not any more necessary than unsafe{} on safe fns

*in

the other possibility that comes to mind is the idea of a function which promises certain invariants *provided* other invariants hold

is trusted sufficient for this? in isolation, yes, because a trusted function can make its invariants conditional

and unsafe code calling it must ensure it calls it correctly in order to be able to rely on those invariants

in its proof

i don't think there's any principled/philosophical reason for `unsafe fn` to be automatically able to perform operations that need `unsafe {}` otherwise. it's just common for unsafe fns to do _some_ unsafe operations inside, that is all. and this "convenience" has downsides. it doesn't take a whole philosophy of unsafe code and trusted code to argue that IMO

well I want to think about propagation first before I say that I agree

trusted I think propagates fine; conditionally-trusted generic code says "If the provided callees promise to uphold their invariants, then I promise to uphold mine."

the proof obligation lies on the trusted fn here

what about unsafe propagation?

is it meaningful to have conditionally-unsafe code?

for me the reason to want the unsafe block in `unsafe fn() { unsafe { foo() } }` to be required is *much* simpler: some unsafe fns need to be unsafe to call (e.g., target features) but don't necessarily need to do unsafe stuff themselves, so it should be possible to write those without accidentially doing unsafe things in the body. end of story.

actually hm, does it make sense for trusted code to prpagate

a conditionally-trusted fn is one that is trusted only if all its conditioned-on callees are trusted

in other words, it only promises its guarantees if all relevant callees do too

so the dual of that would be a conditionally-unsafe fn is one that is unsafe if any of its conditioned-on callees are unsafe

i still don't know what exactly you mean by "trusted" (tbh that might be because i've only half-followed the discussion earlier) and for the reasons i described it's not really relevant to my position on the relation of `unsafe fn` and unsafe blocks

rkruppe: https://internals.rust-lang.org/t/what-does-uns...

oh. i've been ignoring that thread

no offense but everything in that thread i've read is philosophizing that hurts my head and doesn't illuminate anything to me

rkruppe: ah ok

basically the problem that gives rise to trusted is that unsafe code can't actually verify that, say, Eq is actually an equivalence relation

and so it can't rely on it

isn't that what `unsafe trait` is for?

yeah

'trusted' is trying to generalize that notion

so a conditionally-unsafe fn says "if any of my callees require invariants to maintain, then I will only promise to maintain them if these other invariants are maintained"

huh?

an unsafe fn requires invariants to be upheld to be called, it doesn't promise to _uphold_ invariants

(unless you call "not UB" an invariant, which is an abuse of terminology in multiple ways IMO)

so a "conditionally-unsafe" fn would be some that... sometimes requires invariants to be uphold by the caller? but that's just a more complex invariant period.

by conditional here, I mean generically

rkruppe: conditionally-unsafe code is promising that if all of its generic callees are themselves safe, it will be safe. Otherwise, it will be unsafe; that is, it will have some invariant whose violation will lead to UB.

OK that i can make sense of

it still has a proof obligation to discharge, therefore, when calling a potentially-unsafe callee

it has a moral obligation to document the invariants it requires when it is unsafe

and a proof obligation that, if called with those invariants satisfied, it will not violate any invariants of its callers

i still don't see how that can actually be very useful, though. the invariants that need to be upheld not only depends on the callees but also on everything else the function does that might be relevant to the callees. therefore it's very difficult and anti-modular to state what a concrete invocation requires (and thus, what the caller needs to ensure)

yeah, I'm not sure it's super useful

I can make contrived examples but I'm not sure they're useful in general

since mostly they become roughly equivalent to imposing additional invariants on the callee

and it's easy to express "this passed-in closure must obey these restrictions" in documentation

expressing it in-language, and not doing so by using trusted, seems very edge casey

so then the last thing is masking

unsafe { } is the masking of unsafety, which discharges proof obligations

trusted { } would be masking untrustedness, which *creates* proof obligations

in other words, it is saying that some part of the function has proof obligations which the callees---preceding code in the function---must uphold

but that's worthless; the function has access to its own code

without some way of actually checking invariants, you could do the same with a comment like "at this point, the list must be sorted, so retrieving the first element retrieves the least element in the list"

trusted { } would just be syntactic bloviation there, I think

this is again true even in conditionally-trusted functions

so while trusted and unsafe are dual concepts, I don't think either really lines up with effects

I think there is advantage to always require unsafe { } to discharge proof obligations, even in unsafe code

and no advantage to allowing trusted { } to crate them

*create

you can model them as effects, but I simply think it doesn't quite line up in either case

eternaleye: ^

finished my rubberducking

alercah: Sure it does make sense to have conditionally unsafe code. `map` with an unsafe fn as its transformation is a classic example.

unsafe fn foo(x: *const u32) -> u32 { *x }; fn bar(l: &[*const u32]) -> u32 { unsafe { l.map(foo) }.fold(<u32 as Add>::add) }

well, l.into_iter().map

alercah: But std::iterator::Map::next() needs to be "unsafe-polymorphic" for that to work

eternaleye: right, fair point, ok

that makes sense

I don't think that changes the logic about proof obligations

but on the bus I had another realization

which is that this whole thing is about proof obligations, right?

we're focused a lot on UB, since that's the main purpose of unsafe, but it is used for other things and there may be other proof obligations

alercah: I disagree there?

oh?

alercah: If it was _only_ about proof oblications, then the only thing it would make sense for it to cover is the `assume` intrinsic.

well

here's my thinking

alercah: Unsafe code _has actual effects_ that transitively-safe code cannot have

It can mutate statics

It can access through raw pointers

yes, but I just see those as unsafe primitives

The fact that those operations themselves carry proof obligations is not the same thing as this being "all about proof oblications"

*obligations

fair

what I meant is

if we think in terms of invariants

safe Rust promises "I do not cause UB"

alercah: And that's why it's an effect.

unsafe { } is effectively assert(I do not cause UB)

The constructors of an effects carrier are exactly the effect's "primitives"

eternaleye: btw... given 'unsafe const fn' does that mess up referential transparency (by mutating statics (is that possible))?

hm

No, it's an assume, not an assert

centril: see the discussion I had with eddyb earlier

An assume, if violated, results in UB. An assert, if violated, results in a panic.

eternaleye: yes, sorry, that was bad terminology on my part

(earlier today)

alercah: ah ah; TL;DR?

centril: the current design for const fns does not provide strong referential transparency

centril: There's overlap

mutating statics in const fns is disallowed by the MIR evaluator

alercah: Anyway, if it was a non-effect, its only primitive _would be_ assume

but a static can be referenced in a const fn and then later mutated at runtime

alercah: ah I see; seems like a reasonable trade-off

centril: well it leads to weird stuff like const x = f(); x != f();

alercah: For example, assume(forall x, x != y || &x = &y) (where x and y are raw pointers) would enforce the absence of aliases to y

despite f() being weakly referentially transparent

On penalty of UB

ok I have to go for a little bit, gonna chew on this a tad

alercah: that is weird indeed.

centril: or worse, if it's allwoed in matches, match f() { f() => ...} not matching

(and that's planned afaict)

alercah: I'll update the i.rl.o thread referencing the discussion here re. unsafe :)

eternaleye: hm I think I found a hangup around masking

I haven't run into that concept before so perhaps that's part of the issue; do you have a good reference paper I can take a look at?

because I think my concept of masking and yours are subtley different

oh I found your link

alercah: The short of it is that masking is what stops infection

usually by evaluating the effect then-and-there

runST is an example of that, for Haskell's ST monad (a carrier for statefulness)

albel727: interesting comment on i.rl.o :)

alercah: However, stTtoIO is _also_ an example, which "merely" transforms it to another effect

Or rather, to another carrier

Since haskell lacks the "effect system" bits