Reworking unformed state

[chandlerc]

Introduce a more formal model for how unformed state is managed for types. This
includes:

• Specifying the interfaces used by types to opt into unformed state, and how
  they work.
• Providing a Core.MaybeUnformed(T) wrapper that models the API subset of
  T available both when fully formed and unformed.
• Initial concepts of unsafe adapt and unsafe as to model unsafe type
  conversions between compatible types.
• A flow-sensitive set of rules for how unformed types become fully formed.

[danakj]

I think this is saying that the following

var t: T;
F(t unsafe as ref T);

Would consider t to be initialized after.

The proposal doesn't say this AFAICT. It says t is initialized if passed to a fn that takes ref MaybeUnformed(T) (but not MaybeUnformed(T)*).

So two potential gaps here, I think:

• Does taking the address of the uninitialized var also make it considered as initialized? As most C++ out-params are going to be pointers.
• Does forming a reference expression to T also make it considered as initialized, or just a reference expression to MaybeUnformed(T)?

[josh11b]

FYI, It would be t unsafe as T not t unsafe as ref T. ref T is not a type, and this specific conversion will preserve the category so it is enough that t is a reference expression. On the other hand, it might be F(ref ...) if F takes a ref parameter, so this might end up being F(ref t unsafe as T).

[chandlerc]

I think the flow sensitive section does restrict this as it restricts the operation set.

Currently, I think even the above would be rejected. I think it has to be: F((ref t as Core.MaybeUnformed(T)) unsafe as T) ... which seems ... suboptimal.

We could build a wrapper to do the explicit escape:

unsafe fn Escape[T:! type](bound ref obj: Core.MaybeUnformed(T)) -> ref T {
  return obj unsafe as T;
}

And then use it:

var t: T;
F(unsafe Escape(ref t));

But it's not clear this is a great experience either.

Is it too ad-hoc to suggest unsafe ref instead of ref in this proposal to do this? Basically, unsafe ref would turn off the flow sensitive restrictions on unformed objects operation usage.

I suppose the down side is that we don't use ref for the object parameter, so this would only support non-methods. Personally, that works for me because methods I feel like are better situated to instead use Core.MaybeUnformed(T) themselves. Thoughts?

[zygoloid]

Perhaps we could allow the use of the name of a variable in an unformed state as the left operand of unsafe as in general? (In addition to allowing it to be implicitly converted to MaybeUnformed(T).)

[chandlerc]

Perhaps we could allow the use of the name of a variable in an unformed state as the left operand of unsafe as in general? (In addition to allowing it to be implicitly converted to MaybeUnformed(T).)

We could, it just feels like it'll be a bit surprising syntax wise:

var t: T;
F(ref (t unsafe as T));

It seems strange to cast t to T right after declaring it with that type.

Relatedly, is this how we want ref-form-preserving as-style expressions (or other such expressions) to interact with ref markings on arguments? Do we need parentheses there? But those are all questions for ref, not unformed...

[josh11b]

These two bullets don't seem to be describing the set of tradeoffs for not having unformed state, they seem to just be repeating "by necessity or choice."

[chandlerc]

Yeah, reworded.

[josh11b]

This talks a lot about what Carbon's Core.MaybeUnformed(T) is trying to do, but not how that is different from what Rust's MaybeUninit does -- is it only "user code dealing with complex initialization"? I thought it included delaying initialization of things like I/O buffers until data was read -- which seems pretty similar.

[chandlerc]

Tried to do a better job of spelling out what I meant here, PTAL.

[josh11b]

Feels like maybe this section should be merged with the alternative considered (or just deleted since the alternative might be enough by itself).

[chandlerc]

Yeah, deleted this and the previous section. Not adding anything.

[zygoloid]

Is it OK for the hardened build mode to use a different representation in the fields in UnformedInit.StructT than the representation that UnformedInit would use, or is the goal here only to allow additional fields to have values specified?

[chandlerc]

My goal was to let it have a different, but compatible representation. Although that may not have much utility. They're still fields of T, and each type has to be compatible with fields of T. And you can't access the fields (or the types used) from here. Reads always go through MaybeUnformed(T) and that in turn through the non-hardening struct.

[zygoloid]

I guess I'm worried about something like:

• A pointer type says its unformed value is 0
• We use that value for detecting whether it's unformed
• It then says that its hardened value is some other bit pattern that's in some way better for hardening purposes

... and our "is it unformed" detection then fails to detect that a hardened unformed value is in fact unformed.

It'd be nice if we could make that kind of bug impossible, by ensuring that the hardened unformed state and the non-hardened unformed state are somehow consistent with each other.

[chandlerc]

This is what the match_first impls for IsUnformed provide when using the UnformedInvalid and UnformedHarden interfaces. It ensures when the harden interface is implemented, it is included in the InUnformed implementation.

The only way to write this bug is to use the lower level UnformedInit and UnformedHardenInit interfaces, manually implementing both, and then manually implementing IsUnformed incorrectly.

I don't really see a way to preclude that, but it at least seems like the well lit path doesn't end up there?

The challenge with making the unformed and hardened states required to be consistent is if the value used in the non-hardened case is lower cost but potentially less secure. In that case you want the value to differ between the two -- that's the whole point. The place where this comes up are things like indices where zero is a good, cheap unformed value, but happens to be "valid" and risky from a security perspective and so hardening prefers to set some other value like INT_MIN. Not expecting this to be common at all, but wanted to leave that flexibility in the design.

[zygoloid]

Hm. There's something that's not working well for me in this description: we talk about an object having "an unformed state" / "its unformed state" / "the unformed state" rather than having a set of unformed states, which to my reading implies that the thing that UnformedHarden gives you must either be consistent with what UnformedInit gives you (on the subset of fields that UnformedInit initializes) or is not an unformed state.

I think we don't have the terminology quite right, particularly about whether a type has a singular unformed state or a set of unformed states. If we want UnformedHardenInit to provide an unformed state, but not necessarily one that's consistent with the representation that UnformedInit provides, then the latter is not providing "the unformed state", just one possible unformed state, which means that the impl of IsUnformed in terms of the UnformedInvalid state isn't necessarily right, as there may be other unformed states. But if instead we want there to be a singular unformed state, then the state that an uninitialized variable is initialized to is not necessarily an unformed state (it won't be one in a hardened build), making the terminology there confusing, along with the name IsUnformed.

Perhaps we could use different words for the set of possible representations that an uninitialized variable can be in, versus the state that UnformedInit puts the object into? That might help to clarify that IsUnformed detects the former, not the latter.

This is what the match_first impls for IsUnformed provide when using the UnformedInvalid and UnformedHarden interfaces. It ensures when the harden interface is implemented, it is included in the InUnformed implementation.

I don't think that is a complete solution. For example, if a type provides an UnformedInvalid impl and an UnformedHardenInit impl, and the latter doesn't produce a state that's compatible with the one that UnformedInvalid computes, then you would use the second impl from the match_first, which does the wrong thing for a hardened value. (I think I'd be fine with rejecting that set of impls if there's a good way to do so.)

Do we expect the "hardened" state to be global, or could it vary between (say) packages in the same program? Do we actually need two sets of interfaces, and an or in the impl of IsUnformed, or could we instead have a single UnformedInvalid interface that sometimes produces a hardened value based on the build configuration?

[zygoloid]

Would

impl as ImplicitAs(C) = C;

work? C is a compatible type that implements ImplicitAs(C).

[chandlerc]

Thanks so much for all the review!!!

I think I've gotten to most and maybe even all of the comments. PTAL!

[chandlerc]

Yeah, reworded.

[chandlerc]

My goal was to let it have a different, but compatible representation. Although that may not have much utility. They're still fields of T, and each type has to be compatible with fields of T. And you can't access the fields (or the types used) from here. Reads always go through MaybeUnformed(T) and that in turn through the non-hardening struct.

[chandlerc]

I think the flow sensitive section does restrict this as it restricts the operation set.

Currently, I think even the above would be rejected. I think it has to be: F((ref t as Core.MaybeUnformed(T)) unsafe as T) ... which seems ... suboptimal.

We could build a wrapper to do the explicit escape:

unsafe fn Escape[T:! type](bound ref obj: Core.MaybeUnformed(T)) -> ref T {
  return obj unsafe as T;
}

And then use it:

var t: T;
F(unsafe Escape(ref t));

But it's not clear this is a great experience either.

Is it too ad-hoc to suggest unsafe ref instead of ref in this proposal to do this? Basically, unsafe ref would turn off the flow sensitive restrictions on unformed objects operation usage.

I suppose the down side is that we don't use ref for the object parameter, so this would only support non-methods. Personally, that works for me because methods I feel like are better situated to instead use Core.MaybeUnformed(T) themselves. Thoughts?

[chandlerc]

Yeah, deleted this and the previous section. Not adding anything.

[chandlerc]

Tried to do a better job of spelling out what I meant here, PTAL.

[chandlerc]

I like the first one a bit more than the second, because we can't have a conversion to C while we're defining conversions to C...

Chatted a bit with @zygoloid about this live, and came up with the idea of explicitly extending the blanket impl when impl-ing the interface that produces the blanket impl. That seems like the case which we can make work (because we can use the explicit extension of the blanket impl to insist that we see it and everyone else sees it too), and ensure that our extension is coherent.

It does mean that we have yet another thing that makes negative constraints bad, but that seems OK.

I've added a description of this to the proposal, PTAL and let me know if this direction makes sense?

It raises some more open questions around final that I've added. Those at least seem more tactical questions we need to think through and less open-ended "how do we want this to work".

[danakj]

Few small things

[danakj]

Not flipping an approval bit - but I am happy with this when @zygoloid and @josh11b are.

[chandlerc]

Actually posting my replies instead of just pushing the commit and leaving them pending... =D PTAL!

[chandlerc]

This is what the match_first impls for IsUnformed provide when using the UnformedInvalid and UnformedHarden interfaces. It ensures when the harden interface is implemented, it is included in the InUnformed implementation.

The only way to write this bug is to use the lower level UnformedInit and UnformedHardenInit interfaces, manually implementing both, and then manually implementing IsUnformed incorrectly.

I don't really see a way to preclude that, but it at least seems like the well lit path doesn't end up there?

The challenge with making the unformed and hardened states required to be consistent is if the value used in the non-hardened case is lower cost but potentially less secure. In that case you want the value to differ between the two -- that's the whole point. The place where this comes up are things like indices where zero is a good, cheap unformed value, but happens to be "valid" and risky from a security perspective and so hardening prefers to set some other value like INT_MIN. Not expecting this to be common at all, but wanted to leave that flexibility in the design.

[josh11b]

Do you say that anywhere?

[josh11b]

It seems expensive to check that the result causes IsUnformed to return true every time this happens, but the invariants of the system rely on that.

[josh11b]

Fine with me. It seems to work with final, as you observed.

[zygoloid]

Hm. There's something that's not working well for me in this description: we talk about an object having "an unformed state" / "its unformed state" / "the unformed state" rather than having a set of unformed states, which to my reading implies that the thing that UnformedHarden gives you must either be consistent with what UnformedInit gives you (on the subset of fields that UnformedInit initializes) or is not an unformed state.

I think we don't have the terminology quite right, particularly about whether a type has a singular unformed state or a set of unformed states. If we want UnformedHardenInit to provide an unformed state, but not necessarily one that's consistent with the representation that UnformedInit provides, then the latter is not providing "the unformed state", just one possible unformed state, which means that the impl of IsUnformed in terms of the UnformedInvalid state isn't necessarily right, as there may be other unformed states. But if instead we want there to be a singular unformed state, then the state that an uninitialized variable is initialized to is not necessarily an unformed state (it won't be one in a hardened build), making the terminology there confusing, along with the name IsUnformed.

Perhaps we could use different words for the set of possible representations that an uninitialized variable can be in, versus the state that UnformedInit puts the object into? That might help to clarify that IsUnformed detects the former, not the latter.

This is what the match_first impls for IsUnformed provide when using the UnformedInvalid and UnformedHarden interfaces. It ensures when the harden interface is implemented, it is included in the InUnformed implementation.

I don't think that is a complete solution. For example, if a type provides an UnformedInvalid impl and an UnformedHardenInit impl, and the latter doesn't produce a state that's compatible with the one that UnformedInvalid computes, then you would use the second impl from the match_first, which does the wrong thing for a hardened value. (I think I'd be fine with rejecting that set of impls if there's a good way to do so.)

Do we expect the "hardened" state to be global, or could it vary between (say) packages in the same program? Do we actually need two sets of interfaces, and an or in the impl of IsUnformed, or could we instead have a single UnformedInvalid interface that sometimes produces a hardened value based on the build configuration?

[zygoloid]

I think it'd help to rename UnformedHarden to UnformedHardenInvalid to emphasize that it must produce an invalid state, like UnformedInvalid does.

[CarbonInfraBot]

[diff] _{reported by reviewdog 🐶}

Suggested change

	`extend impl` will end with a semicolon `;`, instead of a definition block in curly
	braces `{`...`}`, but acts as a definition of the members of the extended
	interface. This also allows
	the found _impl_ to be `final` because this precludes any changes to the aspects
	of the `impl` that were final. This allows adapters to extend which layer of
	these kinds of interface hierarchies they implement without breaking coherence:
	`extend impl` will end with a semicolon `;`, instead of a definition block in
	curly braces `{`...`}`, but acts as a definition of the members of the extended
	interface. This also allows the found _impl_ to be `final` because this
	precludes any changes to the aspects of the `impl` that were final. This allows
	adapters to extend which layer of these kinds of interface hierarchies they
	implement without breaking coherence:

[CarbonInfraBot]

[diff] _{reported by reviewdog 🐶}

Suggested change

	`IsUnformed` implementation (but do support unformed state) _must_ implement assignment and destruction with
	`Core.MaybeUnformed(T)`. When assignment or destruction are implemented with
	`Core.MaybeUnformed(T)`, they are called regardless of whether the object is in
	the unformed state. When assignment or destruction are implemented with `T`, the
	implementation will only call them if `IsUnformed` returns false and using the
	normal type. If the `IsUnformed` returns true in these cases, assignment will be
	replaced with initialization, and destruction will be skipped.
	`IsUnformed` implementation (but do support unformed state) _must_ implement
	assignment and destruction with `Core.MaybeUnformed(T)`. When assignment or
	destruction are implemented with `Core.MaybeUnformed(T)`, they are called
	regardless of whether the object is in the unformed state. When assignment or
	destruction are implemented with `T`, the implementation will only call them if
	`IsUnformed` returns false and using the normal type. If the `IsUnformed`
	returns true in these cases, assignment will be replaced with initialization,
	and destruction will be skipped.