Shared getopt storage is not thread-local. Only the selected errno cell is the current thread's TLS binding. All native identities are disjoint from Hello's own image and the copied launch arguments.

Public optarg cell.

Public optind cell.

Public opterr cell.

Public optopt cell.

The selected thread's errno cell.

Public stdout pointer cell.

Public stderr pointer cell.

Public full invocation-name cell, handed to main.

Public short invocation-name cell, handed to main.

The synthetic stdout FILE object.

The synthetic stderr FILE object.

Borrowed initial C-locale name.

The launch's empty environment vector.

Only the actual public data imports extend Hello's symbol map.

Hello's own symbols together with its public libc data imports.

The two launch strings and their copied writable vector.

The copied argv vector's object identity.

The actual getopt arguments for this fixed launch.

Exact private inventory, not merely membership of the parser root. Argv is deliberately absent: it is the program-owned output.

Environment storage the parser may inspect on initialization.

Fixed identities and exact private parser inventory.

A completed exact-option scan. The private continuation is decoded from memory, not named by an independent ghost phase. Bounds permit both the selected return and a subsequent end-of-options control.

Ordinary coherent cutpoints for this launch only. Running resource prefixes do not inherit this disjunction. Errno is sampled through getopt_state_at; it is not frozen across locale or output calls.

Positive argument/input facts are essential here: getopt_step existentially quantifies a transition without requiring an invoke. A false argument guard must never admit a spurious return code.

The physical native component has no ghost heap, returned code or call-restoration law. FILE/native realization is still the libc trust boundary; these are the concrete model's coherent views.

Private identities exclude caller memory pieces, including life pieces. This main-stage interpretation owns neither FILE lives nor errno bytes. Callback acquisition is a distinct later operation.

One composite interpretation. Current ghost names observe the same payload as physical locale/parser/FILE readiness. Native pools must stay apart from the program, but getopt's public argv writes are intentionally not classified as private roots.

The initial ghost token rules out the finished cutpoint by its public optind, exposing the actual decoded fresh private storage.

This is the selection implication main_to_version consumes. It applies to every transition witness, not only to admitted invokes.

One joint model image extends, rather than replaces, the actual linked initializer. Its private parser starts zero-initialized; public optopt starts at '?' independently of that private copy.

Program-owned launch regions, outside the linked image.

Keep the linked initializer below the native/launch allocation band.

Address, width and integer value for each nonzero startup store.

Capabilities written by the six nonnull pointer stores.

The single physical entry image; scalar folds avoid expanding memory records underneath symbolic addresses during certificate checking.

Initial C-locale observation and its private name storage.

Public initial values and the private parser's exact authorities.

Structural stdout representation with no pending bytes.

Structural stderr representation with no pending bytes.

One shared payload, errno cell and authoritative shutdown inventory.

Outside startup writes, the seed's byte is preserved.