# initialization as a two-state automaton
## state space
the object has exactly two states:
* `u` (unprepared)
* `p` (prepared)

no other state is semantically relevant.
## semantic vs representation state
semantic state is defined only by successful transitions and external resource ownership.

representation state is the concrete byte contents of the object.

the automaton constrains semantic state only.
## state definition
state is determined by successful transitions:
* before any successful `init` -> `u`
* after a successful `init` and before `uninit` -> `p`
* after `uninit` -> `u`

failed `init` attempts are not transitions.
## transitions
### init
`u` -> `p`

obligations:
* acquire all required external resources
* authoritatively write all runtime-relevant state
* establish all runtime invariants

obligations on failure:
* leave the object owning no external resources
* ensure another `init` call on the same object is valid

init is total on `u`.
### uninit
`p` -> `u`

obligations:
* release all external resources owned by the object

non-obligations:
* no requirement to zero fields
* no requirement to restore configuration templates
* no requirement to repair non-owning internal references

uninit is total on `p`.
## forbidden transitions
* `p` -> `p` via `init`
* `u` -> `u` via `uninit`
* calling `uninit` before a successful `init`
* any transition that leaves external resources owned in `u`

## invariants
* `p` implies all runtime invariants hold
* `u` implies no external resources are owned
* no external resource survives a transition to `u`
* representation state in `u` is unconstrained except that `init` is permitted

## atomicity invariant
`init` is atomic with respect to semantic state at function return:
* upon return, the object is either in `u` or `p`
* partial resource acquisition during execution is permitted
* on failure return, no external resources remain owned

## reinitialization guarantee
because:
* `init` is total on `u`
* `uninit` returns `p` -> `u`
* failed `init` leaves the object in `u`

the sequence:
```
`u` -> init -> `p` -> uninit -> `u` -> init -> ...
```
is always valid.
## minimal correctness criterion
the automaton is correct if and only if:
* all external resource ownership is confined to `p`
* failed `init` leaves the object in `u` and permits another `init`
* `init` and `uninit` are mutual inverses on semantic state

# Addendum
Any external resource whose ownership would characterize the `p` state (being a property of it) should, from the moment of acquisition, be represented in the object. No such direct ownership may be staged or duplicated in locals for later publication.

On failure return from `init`, the implementation performs only the releases necessary to ensure that the object owns no external resources. It performs no additional representation writes for restoration, normalization, or repair.

`init` is defined to operate correctly on any representation satisfying the `u` invariant, independent of its byte contents. The sole semantic requirement on failure is therefore: no external resources remain owned.