# K1141–K1179 local evidence reconciliation

This contract records the existing bounded spawn and process-rights interfaces
for the 32 local plan entries that remained `PLANNED` after their eight guest
gates were recorded. It does not change those guest results or claim a product
release. The audit must verify every referenced source and test-log hash and
confirm the named positive and negative tests actually executed. Reusing a
recorded result is reported as reconciliation, with zero new test executions.

## K1141–K1160: embedded image, arguments, entry and unwind

The detailed local ownership and transition contract remains in
`os-spawn-transaction/CONTRACT.md`. Its statement that guest integration was
pending describes the host model at the time it was written; the separately
dated K1145, K1150, K1155 and K1160 acceptance reports record later guest runs.

The kernel supplies immutable initialized bytes and a trusted extent through
the unsafe `TrustedImage::from_kernel` constructor. A private `Recipe` validates
the bounded ELF and private stack before PID/resource acquisition. A truncated
header or an extent longer than the supplied bytes is rejected without
publication. The unsafe boundary requires genuine kernel-owned bytes; a user
argument cannot establish their provenance.

Arguments and environment each contain at most four strings, at most 64 bytes
per string and at most 256 bytes in total including terminators. The private
stack plan retains copied bytes and in-range pointers with 16-byte-aligned SP.
Embedded NUL, a 257-byte total or an invalid entry is refused before publication.
The prepared entry requires RX code, RW user stack, an unmapped guard and an
EL0 register description. These checks do not independently authorize ERET.

The private nonclone ticket and resource bag retain the root, pages, handle
table and thread owners through prepare, publish, terminate and reap. A Before
failure rolls back the acquired bag; root detach and TLBI precede release.
An After failure retains custody and quarantines; Drop does not release owners.
The frozen module's typed errors and state transitions remain authoritative.

The bound tests are `os_spawn_transaction_{image,argv,entry,unwind}_{positive,negative}`
in the four archived preflights. Their host observations are modeled; the
separate guest reports bind the corresponding kernel recipe and physical runs.

## K1161–K1165: principal assignment

`Registry<P,N>` owns the association from a kernel-supplied process identity to
a private `Principal`. `bind_kernel` returns a distinct nonzero principal;
duplicate process, full table and counter exhaustion return `Duplicate`, `Full`
or `Exhausted` before changing state. Lookup of an absent process returns
`Unknown`. `request_user_change` never constructs an identity from its argument
and returns `Access` for a registered process. `retire_kernel` removes the
binding. Kernel adapters must supply the genuine process identity.

## K1166–K1170: explicit handle inheritance

`HandleSet<P,M>` owns private grants. The kernel issues a `Handle` for a
registered owner and a typed `Capability`. Inheritance requires distinct live
parent/child identities, a matching actual parent record and an explicitly
inheritable `ReadOnlyFile`. The returned child handle belongs to the child and
cannot be forwarded again. A kernel-device grant, wrong parent, absent grant,
full table or exhausted counter is refused without a partial grant. Closing an
owner removes that owner's grants. This probe capability is not a general VFS
file handle.

## K1171–K1175: inspection rights

`InspectSet<P,M>` owns permits binding an observer to one distinct live target.
`inspect_metadata` returns the supplied live record's `MapMetadata` only after
both identities and the permit's observer/target bindings are checked. Unknown
bindings return `Unknown`; mismatched target returns `Access`. Even a valid
metadata permit cannot authorize `read_foreign_map`, which returns `Access`.
Closing an observer removes its permits. Kernel adapters supply the metadata
from the same live process record they identify as the target.

## K1176–K1180: resource limits

`QuotaSet<P,N>` owns each registered process's `Budget {pages,threads,handles}`.
Adoption validates nonzero thread usage and `used <= limit`. `try_reserve`
checks all three additions before assigning the new usage once. Overflow is
`Exhausted`; a plus-one limit violation is `Limit`; missing ownership is
`Unknown`. Rejected operations preserve the complete quota snapshot.
`release_kernel` removes the quota and returns its recorded usage; it does not
itself free physical pages or handles.

The rights and ABI preflights each contain named positive and negative tests,
regression output and AArch64 no_std compilation. The guest adapters and their
scoped physical evidence remain in the separate K1165–K1180 reports. No new VM
run, general VFS guarantee, physical-hardware result or product acceptance is
created by reconciling these local entries.