A selected x86-64 option record is 32 bytes: name at 0, has_arg at 8, flag at 16 and val at 24. Padding is not interpreted.

Logical witnesses for one call family. Argument pointers include their exact capabilities; subsequent calls may permute only the tail. No bound on string contents is imposed beyond C termination.

Physical cells are references supplied by startup/linking. The four values alone do NOT establish initialization of glibc's private parser. Reads, writes and release ownership are separate authorities.

Canonical signed C int, stored/returned as its unsigned W bits.

Writable aligned int cell with an independently specified value.

Optional out-int: null is absence, not a writable null span.

Pointer slots, including the exact null sentinel. Each native byte is canonical independently of the aggregate pointer load; consumers can reconstruct exact byte pieces after argv permutation.

argv0 is fixed; GNU permutation moves whole tail pointers, never merely their address bits. argc=0 admits just the sentinel.

Argument strings are borrowed, readable C strings.

A writable argv vector and one capability-exact permitted ordering.

All records and names are readable; optional flag writes require their own authority. A null name terminates the table.

The five actual argument words, independent of any result.

Caller admission includes the entire sentinel-terminated table and every optional writable flag/index, even on an unknown option.

Public exposed state is coherent with memory. A separate rep premise certifies initialized continuation or reset optind=0, including GNU ordering/environment and any interior nextchar borrow.

A pointer borrow into any argv string, including its NUL, retains the original capability. Empty --greeting= is therefore admitted.

Null or an argv borrow, never a fresh owned allocation.

Spans protected against all writes, including private/errno roots. Separation is about storage, not restrictions on argument bytes.

Optional writable output span.

Exposed writable cells, distinct from private parser roots.

Caller-owned outputs remain separate from parser-private spans.

No character-buffer writes are authorized by parsing.

The separate output pieces do not overlap. This intentionally excludes aliased flag/index/state outputs, whose last-write behavior is not specified here; it excludes no Hello argument contents.

The argv slots and strings supply borrowed capabilities for optarg and permutation, but do not delegate private ownership.

Disjoint protected bytes and write spans. Representation must also keep private release rights exclusive of all caller objects.

Private releases name live heap objects and exclude every caller capability-bearing input/output object, not merely its byte span.

Normal outcomes preserve protected bytes AND shadow entries.

Physical public cell identities never change across a call.

Private projection capabilities come from explicitly enumerated private pointers or new objects, NOT complete pointer slots inside caches, which may contain a caller's optarg/nextchar borrow.

Private authority can only descend from old private authority or born objects. In particular storing optarg never makes its argv object a parser root or an owned allocation eligible for release.

Drop GNU's leading ordering marker, then the error marker.

First occurrence of a short option selects its argument mode. Native char is signed on this target; high bytes are sign-extended.

Mode zero has no optarg, mode one needs a nonnull argv borrow, and mode two permits either. No ownership is transferred.

Abstract result classification. Long success reports its table index and writes its flag, or returns val when the flag is absent. A required argument always yields a nonnull readable argv borrow. Errors and end-of-options have null optarg. Scanning order is left abstract; this relation promises no termination or exact diagnostics.

GNU diagnostics are stderr acceptance only; the caller-owned errno cell may change even when no diagnostic is emitted.

Ready admission does not equate reset with arbitrary writable state. Private ownership/liveness and noninterference belong to rep.

Logical prefix endpoints use an in-progress representation, not completed parser state at arbitrary native cutpoints. Resource ends inherit only this prefix relation, not the normal postcondition.

Normal completion restores represented option state and all input borrows for positive argc. The argc=0 early return exports private optarg/optopt, not necessarily their old public values or a borrow into this empty argv. optind is in range; opterr is unchanged. optopt is deliberately not overconstrained on successful paths.

Exact W/P/P/P/P arguments and W result, even when discarded.

Trusted family over a projection of the existing libc world. The supplied stable relation must preserve effective locale names, text, codec and epoch and the one shutdown/stdout inventory. requests accounts for diagnostic/private allocations; there is no promise of purity, ordinary malloc NULL, or native adequacy.

The exact capability of a borrowed optarg is never replaced by a stronger Obj capability having the same address.

Permutation preserves argv's full pointer inventory.

Every option result is a normal W return, never an exit request.

Required arguments cannot be a null optarg, even for empty strings.

The post exposes exactly the ordinary pointer-load protocol main uses: address bytes together with the original capability in aux.