Don't require that @inbounds depends only on local information

[LilithHafner]

Delete "from the information locally available" from "Only use @inbounds when it is certain that all accesses are in bounds."

This reflects the fact that the compiler models the possibility of undefined behavior and therefore does not constant propagate functions with @inbounds (unless it can prove they are safe).

If one semantically executes and out of bounds @inbounds, that's UB. If it's not semantically executed, it's not UB.

Related: #54099. cc @Keno
Documents that @stevengj is right here

[vtjnash]

The question seems to be whether the compiler is permitted to speculatively construct and object (ignoring constructor invariants with abstract interpretation) and then use that object to speculate other queries (such as that getindex). I don't think anything currently disallows that, though @oscardssmith was previously examining that question in the context of SubString constructor/methods also.

[Keno]

Yes, there's different requirements that apply to @assume_effects :ub vs @inbounds. @inbounds only asserts that the inbounds access does not happen, so the user is allowed to place their own contracts on things (in this case, if you construct a Triangular while bypassing the inner constructor, or mutate something afterwards in a way that invalidates the assertions and then call this method that's UB). @assume_effects is stronger and is required for all arguments, no matter how constructed.

As @vtjnash mentioned, there are some plans to annotate types to allow inner constructor constraints to be valid for @assume_effects purposes, but this issue is a bit separate.

[vtjnash]

if you construct a Triangular while bypassing the inner constructor, ... and then call this method that's UB

Isn't that what inference does? Or are you saying that is why inference poisons the UB flag on the method containing the inbounds so that it shouldn't attempt that second call?

[Keno]

Or are you saying that is why inference poisons the UB flag on the method containing the inbounds so that it shouldn't attempt that second call?

Yes

[Keno]

I think the most coherent thing we can say is that:

1. @inbounds needs to be valid for all code paths reachable from "public api" (where the latter is somewhat deliberately vague)
2. @assume_effects needs to be valid for all code path reachable from any call to the annotated function (for any element of the argument types).

So this PR should reflect 1) appropriately for inbounds.

[stevengj]

Suggested change

	Only use `@inbounds` when it is certain that all accesses are in bounds. In
	Only use `@inbounds` when you are certain that all accesses are in bounds (as undefined behavior, e.g. crashes, might occur if this assertion is violated). In

Maybe just change it to "when you are certain". Basically, it's up to the code writer to decide what level of certainty they are comfortable with (e.g. "I'm certain as long as users don't break my API abstractions", or even "I'm certain because this is throwaway code and I'm only passing 1-based arrays today"). I think that subsumes @Keno's comment without opening a can of worms with phrasing about "public API".

[LilithHafner]

It seems form the comments above that this PR gets the semantics right, so I'm going to go ahead and merge it unless folks object.

[andrewjradcliffe]

you are

The original "it is" achieves better clarity. Use of "you" could be interpreted as "am I certain? yes, then let's try my luck" -- but one can be wrong.

Instead "it is" implies that a truth exists outside of oneself, and, furthermore, that due to fallibility, one should provide a proof. Whether one actually provides a proof for each @inbounds is unlikely, but if one gets in the habit of thinking that way, the probability of flippant and unsound @inbounds should greatly decrease.

[LilithHafner]

I agree with @stevengj's #54270 (comment). The crux is that there is no external truth outside of oneself. It's perfectly valid to try your luck. If you're wrong, you might get hard to trace problems, which this docstring indicates clearly.

I, for one, do use @inbounds "flippantly" and unsoundly at many points during early development, and sometimes provide proofs for usage in registered packages (e.g. https://github.com/LilithHafner/AliasTables.jl/blob/ca6eacd2c222e7e797ec446b5cf6343a733f756e/src/AliasTables.jl#L354). That whole range is allowed by the language semantic. It is the place of a style guide or code quality standard to require or encourage correctness proofs, not the place of this language.

[andrewjradcliffe]

Eh, it's true: the nature of @inbounds implies acceptance of potential UB. I'm reading too much into "it is" / "you are", anyway.

It is the place of a style guide or code quality standard to require or encourage correctness proofs, not the place of this language.

Requirement, ok. However, I fail to see the harm caused by active discouragement of bad practices in any programming language manual.

The crux is that there is no external truth outside of oneself.

In the metaphysical sense? Perhaps. However, in a machine, the truth value of inbounds? can be determined, albeit, sometimes with a trawling of a great number of states, other people's code, etc.

---

To complement the tangent: discrete sampling based on tables necessitates @inbounds for performance. This comes from direct experience; incidentally, you may be interested in reading Marsaglia's article "Fast generation of discrete random variables."

[LilithHafner]

However, in a machine, the truth value of inbounds? can be determined, albeit, sometimes with a trawling of a great number of states, other people's code, etc.

Julia has an open world (i.e. you can always add more methods later) so it is impossible to make a universal truth determination without also trawling the future or having some alternative formalization of the language that prohibits piracy.

[Seelengrab]

Without getting bogged down in metaphysical discussions, I think having a note/comment explaining why the @inbounds is safe next to the use is a good idea, because it provides a future reader with the same context the original author had when determining that the use was safe. As such, I also think the it is formulation is better, because it prompts a user of @inbounds to think about why their use is safe and to state that clearly to a future reader.

Rust has a similar culture around its uses of unsafe, where people put comments next to uses of unsafe to justify & document it for the future.