[FEATURE] Audit authority, code quality and documentation in exsh #2
Labels
No labels
bug
ci
docs
duplicate
enhancement
help wanted
invalid
performance
phase-6
question
refactor
security
wontfix
No milestone
No project
No assignees
1 participant
Notifications
Due date
No due date set.
Dependencies
No dependencies set
Reference
erix/exsh#2
Loading…
Reference in a new issue
No description provided.
Delete branch "%!s()"
Deleting a branch is permanent. Although the deleted branch may continue to exist for a short time before it actually gets removed, it CANNOT be undone in most cases. Continue?
Problem and motivation
This issue tracks continuous Phase 6 audit closure for
exsh. Implement shell language, execution state and interactive behavior while treating arguments, environment and pathnames as data rather than grants.An initial inventory is not a security or documentation closure claim. Evidence must follow each changed boundary through final heads, with priority security, reliability, then performance.
Proposed behavior and scope
Caller-owned transport scratch — 15 September 2026
Move both full-capacity shell transport buffers into the authenticated caller-owned workspace: ordinary message I/O and the descriptor transaction's emergency cleanup. The current descriptor state is exclusively borrowed while a transaction lives, so the transaction can borrow its cleanup slice directly. No global scratch lookup, shared mutable cell, runtime lock or new capability is needed. Remove the unsafe static message accessor and the 32 KiB automatic cleanup array. Preserve the 64 KiB process stack and all current upper stack ceilings.
Group descriptor backing storage explicitly at startup, validate cleanup capacity and clean bytes before constructing effectful state, and keep the cleanup slice disjoint from ordinary transport, history and other arenas. A transaction temporarily borrows that slice, retires providers in the existing order, erases the full borrowed extent and returns the borrow; explicit restore and already-retired resolver paths retain their existing behavior. Failure and uncertain ownership must retain their existing fail-stop rules. Do not introduce shared aliases or fallback storage.
Coordinate target and image-builder layout version 22. Export the target transport-array size/alignment in the layout description, allocate both buffers in identical typed carve order, and reject old or mixed descriptors. Preserve caller resource policy and complete transport capacity; this is an ownership/layout change, not a smaller-message workaround. The frame inspector must eventually bind the full workspace reservation instead of requiring a now-removed stack array, while still rejecting unproved ordinary-source and direct/nested bounds.
Required evidence includes clean/short/dirty scratch, canary/erasure/reuse, early error, explicit restore, handoff, uncertain cleanup and existing shell regressions; exact target/producer layout agreement and old-version refusals; strict warning-denied Rust/helper matrices; actual optimized frame inspection; and relevant bounded runtime VMs before product acceptance. Keep the complete frame gate and full self-hosting criteria open until their own evidence exists.
Current inventory: 3 Cargo targets (1 bin, 1 lib, 1 test); manifests:
Cargo.toml. Include explicit and automatically discovered targets, supported features and target-specific configurations.Inventory every startup/runtime grant and authenticated peer, then success, denial, cancellation, failed transfer, restart and teardown. Trace callers and downstream providers so names, numeric identities and retained aliases never become implicit authority.
Initial target-root inventory found no direct/shared
missing_docspolicy attests/manifest_catalog.rs; verify and enforce it with meaningful rustdoc.Authority, security and reliability
Maintain a finding register with public finding references, exact revisions, invariants, reproduction, owners, regression tests and closure evidence. Publish only non-sensitive status here; suspected vulnerabilities follow SECURITY.md. Each dimension below needs its own result and rationale; an absent daemon or current Rust target is not a blanket exemption.
Acceptance criteria
missing_docsenforcement without blanket allowances or hidden-API escapes, warning-denied private-item rustdoc and an undocumented-public-API negative gate.cargo fmt --all -- --check, strict Clippy, unit/doctests and warning-denied builds/rustdoc for every owned crate/target under default and all valid feature, freestanding/host, SMP and profile combinations; test mutually exclusive combinations separately. Add focused VM regressions for runtime behavior and observe the older catalog and unit tests at the exact published heads.Alternatives and tradeoffs
Use cohesive local refactoring or a justified shared extraction only after identifying real common semantics and authority boundaries. Remove superseded paths after preserving maintained coverage. Profile before optimization; document unavoidable ABI/hardware limits and explicit quotas rather than weakening security for speed.
Workspace ownership checkpoint — 15 September 2026: Signed Exsh
b12e172e7b266842a8659104894f6821166165fbowns ordinary and emergency transport in distinct version-22 authenticated workspace slices. Descriptor startup rejects short or dirty cleanup storage before metadata effects; transactions exclusively reborrow the complete slice and erase it after emergency cleanup. The global UnsafeCell accessor and automatic 32 KiB cleanup array are removed. Larger valid caller slices retain their complete extent. Existing provider retirement, metadata rollback and uncertain-cleanup behavior remain enforced.All 961 Rust tests pass in each default/all-feature/production development/release configuration, with formatting, strict host/native Clippy, private rustdoc and eight native builds without warnings. Four added tests cover workspace disjointness, malformed backing, complete caller extent and consecutive cleanup reuse; existing cleanup controls now also check buffer canaries and erasure. All 73 warning-denied checker tests pass.
Both actual optimized native fallbacks measure 48 local bytes, compared with the retained prior 32,816-byte frames. Their full checker reports remain INCOMPLETE: runtime/all graphs contain 691/604 unresolved observations, and the old 32 KiB initial stack-reservation requirement still needs a workspace-specific evidence contract. Ordinary-source membership and direct-versus-nested early-drop bounds remain open. The 8/33/56 KiB upper limits and 64 KiB stack are unchanged; this measurement is not an all-path stack-safety claim.
Matching producer
38424571b76b36c1e631d99fd2c859fb32311eeaexports/consumes 96 capacity words plus 72 target layout words, reserves both transport arrays first and rejects old/mixed layouts. Packaging both actual optimized shell configurations under canonical dev/release policies derives 4,300,800 workspace bytes, with unchanged executable bytes and a separate 64 KiB stack. All 162 Integration helper commands and its strict 320/321-test Rust matrix pass, including four native builds. These are private artifact and host checks, not guest execution. The product catalog still selects the earlier shell; coordinated catalog adoption and matching runtime VMs remain required.Documentation
79cdd4c3694e800091b55c737fca04c7bdd3d071describes the ownership and compatibility contract. Its 45 tests and canonical checks pass. The full manual renders 2,375 pages without final warnings; all 433,713 word boxes are in bounds and changed page 2280 passes visual review. API snapshots are unchanged. Exsh CI 225/226 fails only the incomplete frame gate after 961 Rust and 73 checker tests; all four logs total 311,820 bytes with zero warnings. CI runtime/all graph observations are 662/587 and both fallbacks measure 48 bytes; these artifacts remain distinct from local images. Docs CI 883/884 passes with all four complete logs (762,212 bytes); reference passes converge with 35/1/0 warnings and zero final warnings. These component cohorts are fully classified. Integration CI 1637/1638 remains queued at its first observation. No full build within EriX or whole-codebase authority closure is claimed.Diagnostic guest evidence — 15 September 2026: The original serial editor/history, inherited-stream time and runtime-error probes pass on a newly built native image using Exsh
b12e172e7b266842a8659104894f6821166165fband the complete companion helper correction published as Integrationdb80a2c1dfc669bd724762d476f5f5c0da005ff6. All original timeout and exact output assertions are preserved; the image remains unchanged. This uses a separately recorded original-component catalog and explicitly identified helper delta, not an admitted product catalog. Full frame evidence remains INCOMPLETE, including workspace evidence, ordinary-source membership and direct-versus-nested bounds. The three probes do not establish either complete guest build generation. Build compatibility evidence: erix/integration#52.Packaged workspace evidence design — 15 September 2026: Replace the obsolete automatic-stack-scratch requirement with a separate mandatory workspace mapping domain. The checker will accept an explicitly selected pristine ELF and optional corresponding packaged ELF, capture both under its existing owner/budgets, and require the packaged artifact to retain the pristine entry and executable bytes. Missing packaged input remains incomplete. A complete mapping domain requires the unique version-22 read-only descriptor, unchanged target type layout and full transport capacity, exact descriptor/arena extent, two disjoint complete transport spans, unique writable/non-executable zero-fill arena ownership, and the unchanged separate 64 KiB stack. Overlapping section/load/page claims, stale or mixed layouts, executable changes and relocation writes into the descriptor must fail. No cache receipt or caller-supplied success flag substitutes for actual artifact bytes.
Local fallback stack accounting remains independent and retains its existing upper bound; register pushes or an old 32 KiB stack reservation cannot certify workspace storage. This mapping domain does not prove source-level borrowing/erasure, complete typed arena carving or every machine call path. Existing source tests and exact build identity retain those separate contracts. Ordinary-source membership, direct-versus-nested bounds and unproved indirect targets remain incomplete, and the full gate remains nonzero until every required domain is established. Add original positive/malformed/overlap/mismatch fixtures and replay the unchanged actual runtime/all artifacts and their existing dev/release packaging. No runtime code or stack budgets change in this checker slice.
Paired workspace mapping checkpoint — 15 September 2026:
Signed Exsh
f17670c7f0c3b6da4458deac534ba6210921550dadds paired pristine/packaged ELF workspace evidence under report schema 2. The checker captures both regular-file snapshots under its existing budgets and retains them when pair admission fails. It verifies the version-22 target descriptor, complete transport spans, exact arena extent, unique zero-fill arena/stack ownership and the unchanged separate 64 KiB stack. All mapped file bytes and permissions must match except tunable capacity words and the workspace owner's extent. Stale/mixed layouts, changed code/data, overlapping claims and relocation writes into descriptor/arena/stack bytes fail before the disassembler runs.The obsolete automatic-stack-scratch requirement and redundant prologue-reservation scan are removed. Local frame ceilings remain 8/33/56 KiB in their existing domains; a local stack frame cannot supply workspace evidence. Mapping success assumes the native loader preserves the declared mappings and does not prove source borrowing, erasure, complete typed carving, ordinary-source membership or direct-versus-nested bounds. Unproved indirect targets remain unresolved.
All 90 warning-denied checker tests pass, including 17 new independent mapping/CLI controls. Formatting, Markdown and canonical checks pass. Four exact retained runtime/all-feature artifacts with canonical dev/release packaging establish the mapping domain: workspace 4,300,800 bytes, two complete 32 KiB buffers, separate 64 KiB stack. Both local fallback frames are complete at 48 bytes. Full reports remain INCOMPLETE with 691/604 unresolved observations and the original source/direct-path gaps; no full frame pass is claimed.
Rust, Cargo and linker source bytes are unchanged from workspace checkpoint
b12e172e7b266842a8659104894f6821166165fb. Its 961-test strict matrices and eight native builds retain that source scope; the paired replays retain their original ELF hashes. The earlier three diagnostic guest probes also retain their original image/source identities and are not new runtime execution at this checker head. Exsh CI 227/228 fails the remaining full frame gate after all 961 Rust and 90 checker tests pass. All four logs are complete (311,713 bytes) with zero warnings. Both fallbacks are complete at 48 bytes; CI runtime/all graphs retain 662/587 unresolved observations. CI supplies no packaged counterpart, so its workspace mapping domain remains incomplete; the four local paired-artifact results retain their separate scope. The cohort is fully classified without accepting any missing proof. Matching Docs5d77dc2b82bf5439e58234d901e30f4565aaa81ais signed and pushed: all 45 tests, the complete warning-free 2,375-page render, 433,924 in-bounds word boxes, literal-option extraction and nine-page visual review pass. Docs CI 887/888 passes with all four complete classified logs (762,236 bytes). Both manual jobs pass 45 tests and converge with 35/1/0 reference warnings, leaving zero final warnings; both Markdown jobs pass. Its issue erix/docs#8 records the 24 repaired inline-option/delimiter cases and is closed after complete CI classification. Full frame proof, coherent product admission, realm work and both complete guest build generations remain open.CI packaged-input checkpoint — 15 September 2026:
Signed Exsh
453641cd19eaa7c85a8f6693363f8660c792ed73supplies packaged counterparts in CI. Its helper is pinned to original Integrationdb80a2c1dfc669bd724762d476f5f5c0da005ff6. The actual producer packages separate copies of each optimized runtime/all-feature ELF using both canonical dev/release policies. Packaging has a 60-second deadline, refuses existing outputs and stops the job on failure. Each pristine/packaged pair gets its own complete checker invocation; any unresolved required domain keeps a nonzero status.The exact changed workflow block was replayed against both retained native binaries. All four produced ELF hashes equal the previously independently validated production bytes, workspace mapping is complete, and pristine inputs remain unchanged. The full reports remain incomplete with 691/604 unresolved observations and unproved source/direct-path domains. YAML and shell syntax, 90 checker tests, formatting, Markdown, canonical and pinned dependency checks pass without warnings. Rust, linker and checker source bytes are unchanged, so their earlier strict validation retains its original source scope. Current Exsh CI 229/230 is fully classified: both runs pass 961 Rust and 90 checker tests and all four workspace-mapping domains, but fail the remaining full frame gate. All four complete logs total 314,746 bytes with zero warnings. Runtime/all graph observations remain 662/587 and fallback local frames remain 48 bytes. This resolves the missing packaged-input domain; source membership, non-returning/indirect targets and direct-versus-nested path proof remain open. No full frame proof, product admission or guest build is claimed.
RELRO target-admission design — 16 September 2026: retained exact runtime/all-feature artifacts contain 3,289/3,272 six-byte RIP-relative indirect call/tail instructions. Each candidate slot is inside declared RELRO and has one symbol-free relative relocation whose addend names an exact function entry. This is an inventory only; raw pointer bytes and section names do not establish target authority or immutability.
Extend the existing static checker with a narrow byte-checked RIP-relative call/tail rule. Share the complete supported dynamic relocation inventory with guarded tables; retain explicit addends, require one exact non-overlapping pointer relocation and reject code-changing writes. Validate complete RELRO ranges and page protection against original load intervals, including writable neighbours, file ownership and range overflow. Infer the target from the relocation expression in the same load-bias domain, never from an unrelocated or writable pointer word. The existing native loader contract must preserve final mappings and executable bytes. Record the slot, relocation and exact target in each admitted edge; apply the existing tail restoration and call-site depth rules.
Add original independent ELF/instruction controls for different stored words versus relocation addends, signed displacements, duplicate/overlapping writes, missing/partial RELRO, writable neighbours, malformed dynamic metadata, non-entry targets and unrestored tails. Replay both exact artifact pairs with unchanged resource and stack budgets. Register-indirect calls, unknown relocation forms, non-returning boundary semantics, ordinary source membership and direct-versus-nested routes remain incomplete until independently established. No whole frame, runtime authority, product catalog or guest-build acceptance follows from a smaller unresolved-site inventory.
Normative inputs are the x86-64 psABI relocation definitions and GNU RELRO program-header contract. Implementation and fixtures remain original EriX code. The Loaderd and Kernel permission checkpoints and maintained Integration diagnostic are prerequisites recorded in their linked work.
Protected relative-target checkpoint — 16 September 2026: signed Exsh
a26ecffb39b70abbf15fb300c5c8c703c6900c37admits exact six-byte RIP-relative calls and tails only after complete relative-relocation, file ownership, protected RELRO page and target-entry checks. It shares the relocation inventory with guarded tables and rejects overlapping or executable-byte writes. Independent controls cover malformed ranges, writable neighbours, different stored words, negative displacements, self-entry loops and tail restoration. All 102 checker tests and all six strict Rust feature/profile configurations pass (961 tests each), together with six native builds, host/native Clippy, formatting and private rustdoc. Runtime Rust, linker scripts and Cargo selections are unchanged.Replaying both unique original pristine/packaged artifact pairs preserves their hashes and all original stack/resource budgets. Runtime/all-feature reports retain 641/591 new call/tail proofs and reach 266/240 functions; unresolved observations fall from 691/604 to 271/232. Workspace mapping passes. Both full reports remain incomplete: unknown indirect control flow, non-returning semantics and source/direct-versus-nested boundaries remain separate obligations. These are partial static admission results, not a complete frame or authority proof.
Signed Docs
83b2d4a2dfc473bb8a99719f86fa1c3c33effa53explains the proof contract and its limits. All 45 documentation tests and canonical checks pass; the 2,377-page manual has 434,680 in-bounds word boxes, zero final warnings and a visually reviewed changed page. API snapshots are unchanged. The preceding Docs permission-observer checkpoint passes CI 893/894 with four complete logs (762,616 bytes) and zero final warnings. Exsh CI 231/232 is fully classified: all 961 Rust tests, 102 checker tests and all four workspace domains pass, with four complete logs totaling 314,760 bytes and zero warnings. Only the complete frame gate fails. Its separately selected CI artifacts report 273/230 unresolved observations; these do not replace the retained local artifact identities/counts. The preceding Docs CI result is recorded below. All 2,997 inventoried authored code files remain below 1,000 lines; semantic authority/documentation closure, product catalog adoption, runnable realms and both complete guest builds remain open.Non-returning control-flow design — 16 September 2026: the exact retained graph includes calls at function ends, including the native exit/fail-stop chain. The current ordinary-call model conservatively assumes fallthrough and reports a missing boundary. Callee names, Rust return types and absence of a decoded return are insufficient to remove that edge.
Refine the existing checked body interpretation with a monotone work queue. Establish a no-ordinary-return fact only for complete body evidence with no reachable ordinary return, no unresolved calls and no cross-function tail whose no-return fact is unproved. Initial facts arise from checked closed local loops or terminal traps. A call to an already proved exact target may suppress its fallthrough; the call edge, callee frame, stack depth and any protected-slot evidence remain present. Revisit only affected callers and record each proof's earlier dependencies. Mutual recursion without a grounded proof, malformed boundaries, unknown instructions, changing stack cycles and unresolved targets cannot bootstrap acceptance. Preserve original resource/stack budgets and the incomplete source/direct-versus-nested domains.
Add independent literal controls for terminal chains, direct and protected-slot calls, returning alternatives, tails, recursion, unknown targets, malformed decoding, cancellation and retained callee obligations. Replay the same exact artifact pairs and measure analysis work before claiming a performance improvement. This is a static ordinary-call model; it does not prove memory safety, exceptional control transfer, whole runtime authority or a full guest build.
Grounded return-flow checkpoint — 16 September 2026: signed Exsh
4bb35938b52c0e6b20c65ccb861af79871272cbederives no-ordinary-return facts from complete checked loop/trap bodies and earlier proved tail targets. Only these grounded exact callees suppress ordinary fallthrough. Calls retain target, depth and relocation evidence, and each fact preserves its original body evidence and earlier dependencies. Final reachability removes stale fallthrough descendants while keeping terminal callee obligations. Unknown calls, unsupported instructions, malformed boundaries and unproved tail cycles cannot establish facts.All 114 checker tests pass, including twelve new literal controls and a 1,200-function chain requiring at most two body visits per function. All six strict Rust feature/profile configurations pass 961 tests each, with six native builds, host/native Clippy, formatting and private rustdoc. Runtime Rust, linker scripts and Cargo selections are unchanged. The physical inventory now covers 2,999 authored code files, all below 1,000 lines.
The same retained original artifact pairs yield thirteen grounded facts each. Runtime/all-feature unresolved observations fall from 271/232 to 181/150; every function-end boundary error disappears under the stated ordinary-call model. The work queue performs 347/313 body evaluations for 266/240 discovered functions and retains 263/237 in the final reachable graph. This is an analysis-work count, not a claimed runtime speedup. Remaining observations are 140/111 unknown calls, 40/38 unknown branches and one unsupported instruction per mode. Both workspace mappings pass; whole frame and source domains remain incomplete with unchanged budgets. A separate proof audit verifies earlier dependencies and retained terminal callees.
Signed Docs
97ce65dcb8cef7232b50d53af90ff8673d623e05documents the refinement. All 45 tests and canonical checks pass, and the 2,377-page manual has 434,800 in-bounds word boxes, zero final warnings and a visually reviewed changed page. Exported API snapshots are unchanged. Exsh CI 233/234 is fully classified: 961 Rust tests, all 114 checker tests and four workspace mappings pass, while the full frame gate remains incomplete. All four logs total 314,776 bytes with zero warnings. Those separately selected CI artifacts retain 183/145 unresolved observations, distinct from the retained local pair counts. Matching Docs CI 897/898 passes with all four complete logs across the two terminal observations (762,600 bytes), 45 tests per manual job and zero final warnings. The preceding Docs target-contract checkpoint passes CI 895/896 with four complete logs totaling 762,636 bytes and zero final warnings. Full indirect/source proof, coherent catalog adoption, whole-codebase authority/documentation closure, runnable realms and both full guest-build generations remain open.Direction-flag stack grammar — 16 September 2026: after grounded return-flow refinement, each retained artifact has one unsupported
stdinmemmove. Extend the stack interpreter only for operand-free single-byteFD(std) andFC(cld). These alter the direction flag without writing the stack/frame pointer. Reject mismatched bytes, operands and prefixes. Preserve frame-pointer facts and ordinary stack joins; this does not prove string-operation memory safety or direction-flag restoration across calls. Add literal positive/negative controls and replay the unchanged original pairs. Unknown indirect edges and source-domain requirements remain incomplete.The implementation and fixtures are original. Normative instruction effects and encodings are in Intel's CLD instruction reference and STD instruction reference. Existing strict Rust/runtime evidence remains applicable only where original source bytes are unchanged; the changed checker receives new complete host tests and artifact replay.
Exact direction-flag checkpoint — 16 September 2026: signed Exsh
05eeb7bc0b1bf1e6fa781b26ee83a8896263a439admits operand-free single-byteFC/FDas stack-neutral direction-flag updates, preserving frame-pointer facts. Mismatched bytes, operands and prefixes refuse. Three original controls bring the full checker group to 117 passing tests, including a growing-stack negative case. Formatting, canonical documentation checks and the 2,999-file physical audit pass. The precise instruction contract is documented in Exsh; the existing manual's ordinary stack model remains applicable.Replaying the same exact artifact pairs now admits each
memmoveframe at eight local bytes and removes its one unsupported-instruction observation. Runtime/all-feature reports retain 180/149 unresolved observations, all unknown indirect calls or branches, with thirteen grounded no-return facts each. Original input hashes and budgets are unchanged; workspace mappings pass and full frame/source domains remain incomplete.Every Rust, Cargo, linker, build and workflow input is byte-identical to the preceding checkpoint's six strict 961-test configurations and six native builds. Those results are retained at their original identity; this checker-only follow-up claims no new Rust or guest execution. Matching Exsh CI 235/236 is fully classified: all 961 Rust tests, 117 checker tests and four workspace domains pass, while the full frame gate remains incomplete. All four complete logs total 314,740 bytes with zero warnings. Those CI artifact identities retain 182/144 unresolved observations, distinct from the local retained pairs. No whole authority, realm or full guest-build acceptance is added.
Measured parser checkpoint — 16 September 2026: signed Exsh
ffbe846cbcd0ab6ea12a476c2c84339f635ee50acompiles the three unchanged disassembly regexes once per input. It retains the exact grammar, instruction bytes, annotations and every disassembly deadline check. Three paired runtime host profiles against signed05eeb7bc0b1bf1e6fa781b26ee83a8896263a439reduce regex-cache lookups from 1,142,474 to 570,949; median profiled time falls from 5.088 to 4.214 seconds and complete wall time from 5.311 to 4.425 seconds. These measurements include profiler overhead and subprocess waiting. The 837,947 full matches, 189,680 splits and 375,664 disassembly deadline checks remain identical; they do not measure guest performance.All eight runtime/all-feature observations preserve their original nonzero checker exits and identical complete decision reports. Only checker-source identity and private snapshot path metadata differ. Workspace mappings pass and the same 180/149 unknown indirect observations keep full frame/source admission incomplete. All 117 checker tests, formatting, canonical documentation checks and the 2,999-file physical ceiling audit pass. Every Rust, Cargo, linker, build and workflow input remains byte-identical to the existing six strict 961-test configurations and six native builds; no new Rust or guest execution is claimed. The focused contract documents the measurement and limits; the unchanged manual's stack model remains applicable. Matching Exsh CI 237/238 is fully classified: all 961 Rust tests, 117 checker tests, Markdown and four workspace domains pass; both runs fail the still-incomplete full frame gate. All four complete logs total 314,754 bytes with zero warnings. These CI artifacts retain 182/144 unresolved observations, the same counts as preceding CI and distinct from the local retained artifact pairs. Whole authority, realms and both full guest-build generations remain open.
Register-target proof design — 16 September 2026: the current runtime/all-feature artifacts retain 180/149 unresolved indirect observations. Six/seven immediately adjacent protected-slot loads are only candidates: textual proximity does not prove every incoming path. Extend the existing finite stack CFG with register facts for all sixteen baseline x86-64 general registers. Entry values are unknown. Exact byte-checked 64-bit RIP-relative loads can acquire a target only from the existing complete immutable relocation/RELRO proof; exact 64-bit register copies carry that evidence. Immediate integers, names, mutable data and stored pointer words supply no target.
Join facts only when every incoming path has the same target value, retaining all contributing load sites and protected-slot proofs. Explicit and implicit writes invalidate each affected full-register family, including partial aliases. Unknown effects, system calls and ordinary calls clear facts; no callee-saved convention, returned function pointer or stack spill becomes an unproved preservation premise. Existing probe/dispatch macros conservatively discard register facts until their complete effects are represented. Unsupported instruction/control-flow cases remain incomplete under the existing trusted-decoder and ordinary-call model.
Revisit weakened joins and replace stale call/branch evidence; an earlier strong path cannot survive as the only proof after another predecessor loses its value. Exact register-call/tail bytes must agree with the selected register. Preserve call depth, tail restoration, grounded return dependencies, unknown branches and the full source/domain gates. The finite worklist and provenance sets use the caller's original deadlines with no invented iteration or origin-count ceiling.
Add independently authored positive, alias/implicit-clobber, bypass, disagreeing/equal-join, loop, stale-edge, call/syscall and source-receipt controls. Replay both original artifact pairs, measure analysis work, update the focused/manual contracts, and validate/sign/push before any adoption. This is original code derived from the Intel instruction reference; it imports no implementation code. Complete guest-image identity, source membership, authority and both full guest-build generations remain separate required work.
Protected register checkpoint — 16 September 2026: signed Exsh
da8b75c9063c52de2149f2a6c7ed170f720a6c62propagates exact full-width protected-slot loads and register copies through the reached CFG. Equal-target joins retain every load origin; unknown or conflicting predecessors, alias/implicit writes, calls/syscalls and unknown effects discard facts. Weakening a join replaces stale edge proof. Complete admitted probe/dispatch effects preserve only unwritten register values. Supported REX forms permit unused bits with byte/text agreement. There is no caller-input, saved-register, spill-word or immediate-address target premise.All 138 checker tests, formatting, canonical document checks and an independent original-byte/load/relocation and earlier no-return dependency audit pass. Retained runtime/all artifact pairs gain 16/18 register edges; the all-feature graph reaches one additional function. Remaining unresolved sites are 164/132, with thirteen grounded no-return facts per mode. Both workspace mappings pass. Full frame/source gates remain incomplete with actual exit 1 and unchanged 60/15-second and 64 MiB budgets. Every Rust/Cargo/linker/build/workflow byte is unchanged from six strict 961-test configurations and six native builds; no new Rust build or guest execution is claimed.
Profiling identified unnecessary effect parsing when all registers were unknown. Skipping those identity transfers and compiling fixed effect patterns once preserves every report decision, reducing runtime effect-parser calls from 34,901 to 1,334 and all-feature calls from 33,398 to 1,348. One before/after observation per identical pair measures 5.089 to 4.385 seconds and 4.997 to 4.358 seconds respectively, including observer overhead. These are bounded host work measurements, not a statistical timing guarantee or guest speedup.
Signed Docs
4f770bee4c6a4784b4fcce6ae606d1fc10b328dadocuments register provenance and limits. All 45 tests and the 2,377-page manual render pass, with 435,231 word boxes inside page bounds, no final warnings and visual review of the changed page. All 3,001 authored code files remain below 1,000 physical lines. Matching Exsh/Docs CI is pending. Complete source domains, authority closure, executable realms and both complete guest-build generations remain open.Path-derived table design — 16 September 2026: retained runtime/all artifacts still have 40/39 unresolved register jumps, including constant indices, byte loads, reused table bases and guards separated from dispatch. Adjacency and Rust enum conventions do not establish index bounds.
Extend the existing finite register state with distinct unsigned-range, RIP-relative base, signed-table-offset and checked local-target facts. These facts never substitute for protected function-call identity. Full-width constants, exact self-zeroing and zero-extending byte/word loads establish numeric bounds; checked copies preserve the appropriate width. Equal paths merge ranges conservatively and retain every original premise. Unknown predecessors, partial/implicit clobbers and calls/syscalls discard facts. Keep complete macro effects and stale-edge replacement.
A scaled signed table load requires a proved base and complete index interval, unique unchanged read-only byte ownership, supported relocation exclusion and every selected entry. Adding the original matching base creates only local branch targets; each must pass the current function/instruction-boundary and macro-interior checks. Preserve all table/base/index/load evidence. Support the baseline register fields and actual encoded displacement without fixed table-count or iteration caps. All work remains under the original deadlines and byte budgets. Unknown guard relationships remain unresolved until separate flag/branch refinement is implemented; do not infer callee preservation, enum validity, memory safety or caller values.
Validate literal constants, bounded loads, nonzero index ranges, every table arm, separated/reused bases, equal/conflicting/bypass/cycle predecessors, aliases and implicit writes, calls, malformed bytes, writable/relocated table data and target-boundary refusal. Replay the same artifact pairs with real statuses, profile work, update the manual and retain every source/frame gate. Full frame and coherent catalog adoption are still prerequisites to the complete confined guest-build demonstration.
Register checkpoint CI — 16 September 2026: Exsh
da8b75c9063c52de2149f2a6c7ed170f720a6c62is terminal in CI 239/240. Both runs pass 961 Rust tests, all 138 checker tests, strict warning-denied Rust checks and Markdown. All four paired workspace domains pass in each run. The required full-frame gate remains incomplete, with 168/131 unresolved observations on these CI artifacts, so both runs correctly fail overall. Four complete logs total 314,840 bytes and contain no compiler/lint warnings. These CI artifact observations remain distinct from the retained local pairs.Docs
4f770bee4c6a4784b4fcce6ae606d1fc10b328dapasses CI 901/902. Four complete logs total 762,604 bytes; each manual job passes 45 tests and renders 2,377 pages. Initial reference-resolution warnings clear during the normal three LaTeX passes; final renders have zero warnings. The full source/frame proof, coherent catalog adoption, authority closure and both complete confined guest-build generations remain open.Bounded table checkpoint — 16 September 2026: signed Exsh
efb542a3418badef951d01dff24eec88b8490aeetracks distinct unsigned bounds, original relative bases, signed table offsets and local targets. Exact constants, self-zeroing and zero extension establish numeric premises. Every selected immutable table byte, matching base addition and candidate instruction boundary must be proved before retaining any successor or branch evidence. Numeric/table values cannot authorize function calls. Joins preserve all alternatives and original premises; unknown predecessors and alias/implicit/call clobbers discard facts.All 157 checker tests pass, including complete 256/65,536-entry domains, nonzero and signed read windows, extended register fields, joins, bypasses, loops, width controls and immutable/boundary refusals. Original-byte function/table/base/index/addition audits, formatting, Markdown and canonical checks pass. Final original runtime/all pairs admit two table branches each and retain 164/132 unresolved obligations: two entry branches resolve, while two newly exposed guard-interior conflicts remain. Both workspace mappings and thirteen grounded no-return facts per mode are retained. Full frame/source status remains incomplete with actual exit 1 and unchanged budgets. Initial partial-set exploration is diagnostic negative evidence, not accepted coverage.
Profiling identified repeated compilation of fixed stack patterns. Compiling sixteen unchanged patterns once and sharing the existing padding pattern preserves all report decisions and matching operations. One baseline/optimized observation per original pair reduces runtime/all regex-cache lookups from 651,254/627,530 to 135,274/131,391. Profiled times are 5.994 to 5.445 and 5.756 to 5.179 seconds, including overhead and waiting. These measurements establish reduced host work, not a timing guarantee or guest speedup. The final source has a clarified module docstring and separately reconciled complete replay decisions.
Every Rust/Cargo/linker/build/workflow byte retains the existing strict matrix; no new Rust build or guest execution is claimed. Signed Docs
242b78c8f35aeaef879f819c670574a4c1d95c3fexplains complete read windows and target-set admission. All 45 tests and the 2,379-page render pass, with 435,421 word boxes inside page bounds, zero final warnings and visual review of both changed pages. All 3,003 authored code files remain below 1,000 physical lines. Matching CI is pending. Explicit flag/guard refinement, full source/frame proof, coherent catalog adoption, authority closure and both complete confined guest-build generations remain required.Bounded table CI — 16 September 2026: signed Exsh
efb542a3418badef951d01dff24eec88b8490aeeis terminal in CI 241/242. Both runs pass 961 Rust tests, all 157 checker tests, strict warning-denied Rust checks and Markdown. Each run completes all four paired workspace domains. The required full-frame gate remains incomplete with 168/131 unresolved observations on the CI artifacts, so both runs fail overall. Four complete logs total 315,234 bytes, with no compiler/lint warnings. No incomplete proof is treated as acceptance.Signed Docs
242b78c8f35aeaef879f819c670574a4c1d95c3fpasses CI 903/904. All four logs are complete (763,044 bytes); each manual job passes 45 tests and renders 2,379 pages. Initial reference warnings clear in the normal LaTeX passes; final renders have zero warnings. An expanded local source/config inventory additionally checks 685 files, bringing the combined physical ceiling audit to 3,688 files, all below 1,000 lines. Flag/guard refinement, source/frame closure, coherent catalog adoption, complete authority review and both full confined guest-build generations remain required.Comparison-derived branch design — 16 September 2026: replace the fixed-register guarded-table collapse with ordinary control-flow interpretation. Bind immediate/register CMP operands, widths and comparison sites to original bytes. Refine unsigned and equality successors only when complete tracked values fit the compared width: a 32-bit comparison does not zero upper register bits. Keep all comparison, producer and edge premises; reject malformed branch encodings before granting a refined edge.
A write to either compared register, relevant flag clobber, unknown effect, call, syscall or collapsed page probe discards the condition. Other proven flag-preserving effects may keep it. A join retains a condition only when every incoming path agrees on its semantics, unioning comparison origins. Contradictory intervals may prune an edge; unmodeled predicates keep both successors. Byte-sized enum conventions and caller or callee preservation assumptions provide no bounds.
Byte-checked full 32-bit memory MOV/LEA and defined arithmetic writes provide architectural unsigned ceilings. Exact modular immediate arithmetic may preserve narrower intervals where sound. Expanding backward joins widen only to a certified architectural producer ceiling and retain their source sites; a small 64-bit constant never establishes a 32-bit ceiling. Use original deadlines, with no fixed iteration or origin-count cap. Revisit weakened joins and discard stale branch evidence. Every complete immutable table target must pass function and instruction-boundary checks before any target is admitted.
Remove the superseded dispatch macro and report field after ordinary flow covers its actual semantics; retain the separately checked page-probe rule. Replace artificial guard-interior barriers with real bypass/width/flag tests, preserving all meaningful ownership, relocation, late-arm, restoration and loop controls. Validate exact original artifact pairs, profile actual status/work, update component/manual contracts, sign and push checkpoints, and follow their original CI handles. Full source membership, direct-versus-nested boundaries, realm authority and two complete guest-build generations remain required and unproved. Implementation is original, derived from retained Intel instruction specifications, with no external implementation code.
Ordinary comparison checkpoint — 16 September 2026: signed Exsh
4ed392bcc53cb46d0296cecbdd930c8be5cd7c28replaces the fixed-register table macro with byte-checked CMP/Jcc facts, live comparison lifetime, unsigned/equality edge refinement and sound producer-width widening. A 32-bit comparison never zeroes upper bits. Every complete immutable target set remains mandatory, and numeric/table values cannot authorize function calls. Unknown predecessors, relevant flag/subject writes and unmodeled effects discard conditions. The obsolete dispatch report field is removed.All 176 checker tests pass, including an independent exhaustive interval oracle, high-register dispatch, sign extension, bypasses, conflicting/unknown joins, stale proofs, complete table arms and large arithmetic loops. Independent original-byte audits check 354/321 comparison edges, eleven table branches per mode, protected function loads and thirteen earlier grounded no-return facts per mode. Original runtime/all pairs reach 271/246 functions and retain 158/126 unresolved observations, down from 164/132. Workspace domains pass; full frame/source status remains incomplete with actual exit 1 and unchanged budgets.
The audit also reproduces and fixes terminal-call discovery loss. A prior successor diagnostic no longer suppresses recomputation of a revisited call. Three independent controls retain grounded no-return, returning and unknown-target behavior. Original byte/range inspection corrects earlier descriptions of two guard-interior conflicts: these were fallthrough exactly at declared function ends. Padding remains outside those functions; callee names never supply no-return proof. Matching CI remains required before closing the defect.
Profiling identified repeated decoder-effect work. Sharing immutable effects only within one function-body analysis reduces runtime/all effect decoding from 72,668/69,784 to 34,499/32,576 and operand parsing from 75,637/72,547 to 37,468/35,339. Complete paired decisions remain identical. Final single paired profiled observations are 6.633 to 6.425 and 6.416 to 6.269 seconds, including overhead and waiting. The final baseline overlaps host test execution, and earlier pairs show timing variability; these diagnostic durations do not isolate a speedup. This establishes reduced host work, not a timing guarantee or guest speedup.
Every Rust/Cargo/linker/build/workflow byte retains the existing strict six-configuration 961-test matrix and six native builds. Formatting, Markdown and canonical checks pass. Signed Docs
d8fbc3a1f3696e02954b81f23511cee513ddfa8cpasses all 45 tests and complete 2,379-page rendering: 435,637 in-bounds word boxes, zero final warnings and two visually reviewed pages. The physical audit covers 3,005 authored code files below 1,000 lines. Matching CI is pending. Remaining indirect calls/branches, full source/direct-versus-nested proof, coherent catalog adoption, complete realm authority and both full confined guest-build generations remain required.Comparison checkpoint CI — 16 September 2026: Exsh CI 243 and 244 are terminal. All four complete logs total 314,904 bytes with no compiler/lint warnings. Strict Rust checks, 961 Rust tests, 176 checker tests, Markdown and all four workspace domains per run pass. The required full-frame gate remains failed with 163/126 unresolved observations on these CI artifacts; their identities are distinct from the original static replay pairs. No full frame or guest-build acceptance is claimed.
Docs CI 905 and 906 pass with all four complete logs (763,056 bytes), 45 tests and 2,379-page manuals. Both final renders have zero warnings after ordinary reference convergence. The terminal-call discovery controls pass in both Exsh runs, resolving the scoped defect in Exsh #6 while the complete emitted-proof defect stays open. The current physical audit covers 3,690 authored source/config files below 1,000 lines; semantic authority and complete private documentation closure remain required. Original unfinished Integration jobs continue under their existing handles.
Arithmetic-condition design — 16 September 2026: the remaining original branch contexts include a defined 32-bit DEC before a guard, a full-width CMP of an otherwise unknown value, and a SUB/borrow branch. Extend exact byte-checked INC/DEC register writes with modular bounds and architectural producer ceilings. Their flag effects must not preserve an earlier combined CF/ZF condition. Narrow partial writes and undefined-result operations gain no upper-bit proof.
A baseline GP value always fits the unsigned 64-bit architectural domain. A live, exact 64-bit CMP may therefore refine an otherwise unknown value without guessing caller contents or memory provenance. A narrow comparison still requires independent proof of the complete value's upper bits. Numeric refinement must preserve independently established function/base/table identities rather than erase them or confer a new function target. Where the current single fact cannot retain both kinds, keep the existing identity and conservatively forgo the additional stored interval; the branch report retains the numeric premises.
For exact immediate ADD/SUB, derive CF/ZF from the unchanged modular result and encoded immediate. If the modulus is M and constant is C, ADD carry means result < C; SUB borrow means result >= M-C; zero means result == 0. Partition these finite result intervals at the carry boundary and zero, apply the encoded unsigned/equality predicate, and conservatively hull surviving pieces. Preserve zero constants, wrap boundaries, all producer/edge origins and actual incoming bounds. This derivation avoids treating the overwritten destination as the original CMP operand. Joins must distinguish comparison, addition and subtraction semantics. Subject/flag writes, calls, unknown effects and page probes still discard the condition.
Use an independent exhaustive small-width arithmetic oracle, literal full-width controls, malformed/alias/call/width negatives, ordinary table arms, joins and large loops. Replay exact original artifact pairs, inspect newly reached obligations, profile actual work/status, update component/manual contracts and monitor signed CI. No callee-saved assumption, enum validity guess, spill authority or changed frame/resource budget is introduced. Full source/frame boundaries, coherent catalog adoption, actual realms and both complete confined guest-build generations remain required.
Arithmetic wrap precision — 16 September 2026: the first independent byte/subtract/borrow control correctly remains incomplete when the intermediate result is immediately hulled to the full 32-bit domain. Preserve exact modular result intervals in the live arithmetic condition before hulling ordinary register values. Derive those intervals from the original operand bounds and encoded immediate; a wrap can split a contiguous input interval into two pieces. Retain their original operand premises and union/normalize pieces at agreeing semantic joins. Intersect the live condition pieces with current bounds and the actual CF/ZF branch predicate before taking a conservative successor hull. A subject write still discards the complete condition, and unknown/incompatible incoming conditions cannot retain these pieces. The failing control and original result remain retained; no incomplete table or partial target set is accepted.
Arithmetic evidence checkpoint — 16 September 2026: signed Exsh
0cdaa8869545308c528f9cf5a2dc165cb286c6efand Docs07181c34b1a20150afe3380977ca5ba70c909b84are pushed onfeature/posix-compat. Immediate ADD/SUB now retains exact modular result pieces and derives unsigned/equality edges from carry/borrow and zero. Defined INC/DEC writes establish widths without preserving a stale combined flag condition. Full 64-bit comparisons may use the architectural numeric domain while keeping protected typed identities separate; narrow comparisons still require independent upper-bit proof. Known encoding/text contradictions remain explicit flow errors.All 191 checker tests pass, including independent exhaustive concrete arithmetic and modular-interval oracles, wraparound and authority-negative controls. Original runtime/all artifact pairs admit fifteen table branches each and reach 271/246 functions, with 156/124 unresolved observations. Both workspace mappings pass; actual full-frame exits remain 1 and full source/direct domains remain incomplete. Independent original-byte audits check arithmetic/conditional/table premises, 16/18 protected register edges and thirteen grounded no-return facts per pair.
Profiling identified repeated stack-neutral grammar evaluation. A cache scoped to one function reduces those evaluations from 95,643 to 43,169 for runtime and 92,608 to 41,053 for all features, with complete paired report decisions equal. Cached values include refusals and contain no path facts. Timing observations include observer overhead and do not isolate a statistical speedup or guest performance.
Formatting, Markdown, whitespace and all 45 Docs tests pass. The 2,379-page manual has 435,808 in-bounds word boxes, zero final warnings and visual review of the changed pages. The physical inventory covers 3,691 authored source/configuration files, all below 1,000 lines. Semantic authority and complete private rustdoc closure remain open. Rust/Cargo/linker/build/workflow bytes are unchanged from the retained strict matrix and classified CI 243/244; new Exsh CI 245/246 independently reruns those checks. Docs CI 907/908 also runs. Matching CI is pending, and no full confined guest build or coherent product-catalog adoption is claimed.
Test-import correction and CI classification — 16 September 2026: original Exsh CI 245/246 failed before the frame gate because the arithmetic test could not import its checker module. They attempted 177 tests: 176 passed and one module import failed. The preceding 961 Rust tests and strict build stages passed; all four complete logs total 309,708 bytes with zero compiler/lint warnings. The earlier local 191-test pass used an explicitly supplied PYTHONPATH and did not prove equivalence to the clean workflow. This regression is retained in Exsh #7.
Signed correction
12331e26f3bb7a25c0146c8b314eef46dd451099loads the repository's literal fixture setup before implementation imports in both affected modules. A new regression imports every checker test module in a fresh isolated interpreter; it reproduces both failures before correction and passes afterward. The exact clean workflow command now passes all 192 tests without PYTHONPATH. Formatting, Markdown and whitespace pass. Checker/runtime/Cargo/workflow bytes are unchanged, so the prior original-artifact and profiler evidence retains its exact scope. New CI 247/248 runs against the corrected source; issue #7 remains open pending matching CI.Docs CI 907/908 now passes with four complete logs totaling 763,024 bytes, all 45 tests and 2,379-page manuals. Both final renders have zero warnings after ordinary reference convergence. Full frame/source proof, coherent catalog adoption and complete confined guest builds remain outstanding.
Corrected arithmetic checkpoint CI — 16 September 2026: Exsh CI 247 and 248 at signed
12331e26f3bb7a25c0146c8b314eef46dd451099both pass all 192 checker tests, including the ten isolated module imports, and all 961 Rust tests. The preceding strict formatting/Clippy/documentation/build stages and Markdown pass. All four complete logs total 314,944 bytes with zero compiler/lint warning candidates. This confirms the scoped import correction in Exsh #7.Both runs reach and fail the required full-frame gate. All four workspace mappings per run pass, while the emitted CI pairs retain unresolved counts [161, 161, 124, 124]; these artifacts are distinct from the original static pairs' 156/124 observations. Full source/direct domains remain incomplete, and Exsh #4 remains open. The original import-failed runs 245/246 stay classified and are not relabeled as passing.
Docs CI 907/908 passes all 45 tests and 2,379-page manuals with zero final warnings; four complete logs total 763,024 bytes. Signed trees are clean, canonical issue/PR metadata remains applied, and the 3,691-file physical inventory remains below 1,000 lines per authored source/configuration file. Semantic authority and private documentation closure, coherent catalog adoption, runnable realms and both full confined guest build generations remain outstanding. Original unfinished Integration runs continue under their existing handles and budgets.
Instruction-derived call preservation design — 16 September 2026: repeated protected function values are currently lost across calls. The original ELF inventory includes ordinary memory helpers that never write the register holding the caller's function value; assuming the platform's saved-register convention is unnecessary for those cases. The next change will derive conditional-on-ordinary-return register preservation from each exact captured function body and earlier callee proofs.
A candidate register must be untouched by every decoded instruction in that function, including partial and implicit writes. RSP is excluded; restored spill words, entry values, source enum validity and the current kernel's ABI do not supply evidence. Full ordinary body/control-flow admission must succeed. Every reachable call or external tail must resolve and independently preserve that same register. Unknown effects, calls and syscalls supply no preservation. Proofs record original bodies/effects, exact callee dependencies and earlier fact identities; no function-name whitelist or guessed ABI mask is admitted.
Analyze captured functions as conditional contracts without making them reachable roots. Start with no callee preservation, derive grounded facts, and revisit actual potential dependents as facts grow. Candidate subscriptions are only work scheduling and cannot authorize an edge. Each function/register fact is established at most once; existing byte/deadline budgets replace any invented iteration or recursion limit. Recursive assumptions alone cannot seed facts. Actual graph reachability and ordinary no-return analysis remain separate obligations.
At a resolved call, retain only previously established typed facts in independently preserved registers; erase every other register and the live flag condition. Include exact preservation premises with the call and retain their transitive proof closure. Complete frame/source gates, original stack limits and native graph identity remain unchanged. Add independent untouched/clobbered/alias/implicit-write, unknown-call/syscall, tail/branch, recursive and loop-join controls, then replay/profile both original artifact pairs, update documentation, validate and monitor signed-source CI. This establishes a needed part of the call-boundary proof; saved/restored registers and all remaining frame/source/realm/build obligations still require their own evidence.
Grounded call-preservation checkpoint — 16 September 2026: signed Exsh
641ac2fc7c3fba3ab351f2863df7e35117b2732aand Docs7a7c3ff0095de8f008c9b534fd993554df37f976are pushed onfeature/posix-compat. Complete original bodies and earlier callee facts now prove never-written register families. Only existing typed values survive proved calls; live conditions clear. The separate stack-derived rbp fact follows the same rule. This corrects the reproduced stale-frame defect, which stays open pending matching CI. ABI conventions, spill restoration and current kernel behavior supply no preservation mask.All 213 clean-environment checker tests pass, including 21 new controls, eleven isolated module imports and a 1,200-function grounded dependency chain. All six strict Rust feature/profile configurations pass 961 tests each, with host/native Clippy, private rustdoc and six native builds; no warnings. Original runtime/all artifact pairs retain 65/72 protected register edges and 70/77 load origins, reducing unresolved observations from 156/124 to 107/70. Both workspace mappings pass; full source/frame/direct gates retain actual exit 1. Independent audits bind 7,795/7,503 used-contract instructions and complete earlier-proof closure to the original captured bytes.
Profiling identified unnecessary empty-state scans and rejected-body suffix work. Removing them preserves every paired report decision and reduces total profiled Python calls from 32,160,478 to 26,673,252 and from 30,880,221 to 25,402,446. Single paired timings include observer overhead; they do not establish statistical or guest performance. Original timer, byte and stack budgets remain unchanged.
All 45 Docs tests, formatting, Markdown and canonical checks pass. The 2,379-page manual has 436,058 in-bounds word boxes, zero final warnings and visual review of both changed pages. The physical audit covers 3,693 source/configuration files, all below 1,000 lines. Semantic authority/private-documentation closure, product adoption, complete source/frame admission, runnable realms and both full in-EriX build generations remain open. Automatic CI for both exact signed heads is being followed; local passes are not reported as CI acceptance.
Matching preservation CI — 16 September 2026: Exsh 249 and 250 are fully classified at
641ac2fc7c3fba3ab351f2863df7e35117b2732a. Both pass all 213 checker tests, including eleven isolated imports and the stale-frame controls, all 961 Rust tests and preceding strict host/native Clippy, rustdoc and native build stages. Markdown and all four workspace mappings per run pass. The remaining full frame gate fails as required; original CI artifact observations are 111, 111, 74, 74], [111, 111, 74, 74. All four complete logs total 314,995 bytes without warnings. The independently retained local pairs remain 107/70, with their own original identities.Docs 909 and 910 pass at
7a7c3ff0095de8f008c9b534fd993554df37f976. All four complete logs total 763,088 bytes; both manual jobs pass 45 tests and render 2,379 pages with zero final warnings after ordinary reference convergence. The corrected frame-pointer issue is closed on this matching evidence; the full source/frame issue remains open. No full confined build, runnable realm or coherent product-catalog adoption is established.Native artifact intake design — 16 September 2026:
The native producer already retains an unstripped Exsh original before capacity
installation and stripping. Extend the static checker to pair that original with
its explicitly selected packaged copy. Only the packaged input may lack an
ordinary symbol table; a present malformed table remains an error. Preserve the
complete mapped byte/permission comparison, with only the existing capacity and
zero-fill transformations admitted. Check allocated section ownership as well;
stripping is not permission to substitute code, relocation data or symbols.
Admit the native entry only when its original function bytes are exactly one
five-byte relative jump to the unique shell entry. Keep the shell entry's existing
frame limit and record the trampoline separately. Extend relocation inventory to
known eight-byte absolute/global-data/jump-slot writes with checked dynamic
symbol/string selectors. Record their footprints to exclude mutation of evidence,
but never infer local call targets from symbolic addends. Relative target proofs
still require one symbol-free relative relocation. Unknown relocation streams,
text mutation and malformed dynamic metadata fail closed. Needed-library names
never authorize file discovery or execution.
Validate with independent literal positive/malformed/authority-negative fixtures,
replay both original standalone pairs and the retained native pair under the
unchanged profiler/deadlines, and retain actual nonzero checker status. Complete
source membership, dynamic closure, full frame acceptance and guest self-hosting
remain open. No runtime or producer change is proposed by this intake design.
Native artifact intake checkpoint — 16 September 2026: signed Exsh
d67dcb963f1aa265b13dd0609a5f8488784b5822admits the retained original/stripped native pair with exact mapped bytes, allocated ownership and complete program contracts. Only absent packaged ordinary symbols are optional. The exact five-byte native entry jump preserves the shell's 8192-byte frame limit. Checked symbolic relocations contribute write footprints, never local targets or library-discovery authority. Code/dynamic metadata mutation, unknown streams, malformed names/links, resolver symbols and invalid relative prefixes refuse intake.All 231 checker controls (18 new) and 12 isolated test modules pass in a clean environment. All six strict Rust configurations pass 961 tests each, host/native Clippy, private rustdoc and six native builds without warnings; formatting and canonical checks pass. Both retained standalone pairs have exactly unchanged proof decisions (107/70 unresolved). The original native pair inventories 1,345 functions, reaches 220, proves workspace mapping and retains 299 unresolved observations, including 102 symbolic-target refusals. The shell entry has 6,864 partially accounted bytes; its incomplete paths do not establish an upper bound. Independent original-byte audit checks all 1,086,955 executable bytes, exactly 154 changed capacity bytes and 627 relative call-load proofs. Full source/frame/direct gates remain incomplete, actual checker exit 1.
Native original SHA-256
879579542895f2f3fbda38972ebaaaf55e05857ffc456342117624a9bc8d24a9and packaged SHA-256183a1a2f1f4192ffd0b9c123ca50d33af6c584940ca51b156198f8822b718febretain their original Exsh runtime selectionb12e172e7b266842a8659104894f6821166165fb. The native producer already retains the original; no duplicate artifact or producer mutation was required. Profiling all three original pairs takes 16.60/16.47/17.02 seconds including observer work under unchanged 60/15-second and 64 MiB budgets. These are individual static observations, not guest performance claims.Signed Docs
12c6d0a91e5e9c5f170d6d0aa7f050dd60e883efdocuments the contract. All 45 tests and a complete 2,381-page manual pass, with 436,247 in-bounds word boxes, zero final warnings and changed-page visual review. The physical inventory covers 3,695 source/configuration files, all below 1,000 lines; semantic authority/private documentation closure remains open. New Exsh CI 251/252 and Docs CI 911/912 are running at their exact signed heads. Complete source membership, native dependency closure, coherent catalog adoption, runnable realms and both full guest builds remain required.Matching native intake CI — 16 September 2026: Exsh 251 and 252 are fully classified at
d67dcb963f1aa265b13dd0609a5f8488784b5822. Both pass 231 checker tests, twelve isolated imports, 961 Rust tests and the strict preceding Clippy/rustdoc/native build stages. All four workspace mappings per run and Markdown pass. The required full frame gate remains incomplete; the CI artifact counts are 111/111/74/74 unresolved observations in each run. Four complete logs total 315,371 bytes, with zero warnings. Retained local standalone and native artifacts keep their own separate identities and 107/70/299 counts.Docs 911 and 912 pass at
12c6d0a91e5e9c5f170d6d0aa7f050dd60e883ef. Four complete logs total 763,452 bytes; each manual job passes 45 tests and renders 2,381 pages, with ordinary reference convergence followed by zero final warnings. No full source/frame proof, native dependency closure, runnable confined realm or full EriX-in-EriX build is established.A separate original-source relocation calculation defect is now reproduced and tracked with the canonical bug template in lib-dynlink #2. Its two host failures do not imply a guest regression. All 107 symbol-only relocations in the seven retained native artifacts have zero addends; the supported nonzero-field case still requires correction before broader native binding admission.
Native dependency and frame design — 16 September 2026:
Extend the existing artifact checker with an explicitly selected dependency input contract. Every original/packaged object pair, content digest and runtime-manifest input is supplied by the caller. Needed-library names only match that closed inventory; they never trigger filesystem searches, directory enumeration, environment lookup or network reads. Capture all selected bytes under the existing total/input/output budgets and bind them to the report. Source revision declarations are retained as provenance claims and must not masquerade as verified source-to-object membership.
For shared libraries, compare every program header, allocated section owner, executable byte and dynamic table between the retained original and packaged counterpart. Permit only the independently validated ELF section-table location/count/name-selector changes caused by stripping; these administrative exceptions do not apply to executable code or arbitrary mapped data. Keep the existing Exsh capacity/workspace transformation contract separate. Original ordinary function ranges remain mandatory even when packaged symbols are absent.
Use the exact runtime-manifest closure and artifact metadata to bind dependency names, package identities and content. Resolve relocation values using the native planner's S, S+A and B+A rules, preserving provider selection, missing/weak/duplicate handling, checked bases and target ownership. Protected call slots still need one complete non-overlapping relocation and verified final RELRO. A selected provider must identify one exact original executable function entry; unresolved, ambiguous, data, resolver and out-of-range targets remain refused. Function identities include the owning object, so identical relative addresses in different libraries cannot alias.
Compose those checked objects into the existing ordinary-call, return-flow, register-preservation and stack analysis. Library bodies acquire no exemption from instruction, byte, source-membership or frame gates. Retain the original entry/fallback domains and fail incomplete until all required paths and source classifications are proved. No relocated target code is executed and no runtime authority or capability is added.
Add literal positive, malformed, substitution, duplicate-name/provider, bad-symbol, changed-code/metadata, incomplete-closure and overlapping-address controls. Replay both retained standalone pairs and the full native closure with profiler evidence under the original resource budgets. Update the manual and component contracts, run strict repository validation, publish signed checkpoints and classify matching CI. Coherent catalog adoption, runnable realms and both complete guest builds remain separate required acceptance.
Closed native dependency intake — 16 September 2026: signed Exsh
9827896d1cb5ad834589045ee03390aec650df84adds an explicit JSON input contract for one runtime manifest and the exact original/packaged executable and library pairs. Complete file hashes, manifest records, package/feature identities and both needed-name inventories must agree. Only explicit host selectors authorize reads; runtime names and source paths remain data. Inputs share one aggregate byte budget and the original deadline. Library stripping permits only independently checked administrative header selectors, never executable-byte changes. All other mapped bytes, allocated owners, program fields and paired artifact metadata remain identical. Producer source revisions remain unverified claims.The retained native closure binds seven objects, 2,373 ordinary functions and 1,608 relocation records. Intake does not yet resolve symbolic providers or compose cross-library frames. All 259 checker controls (28 new) and 16 isolated modules pass; six strict Rust configurations pass 961 tests each, host/native Clippy, private rustdoc and six native builds with zero warnings. Formatting, Markdown and canonical checks pass. All three retained artifact replays preserve their previous frame decisions: 107/70/299 unresolved observations for standalone runtime/all/native. Full frame/source gates retain actual exit 1. Profiling records 0.181 seconds in native dependency intake and 23.17/25.51/24.59 seconds for the three complete profiled runs, within unchanged 60/15-second and 64 MiB budgets. Concurrent Rust validation changes host contention, so elapsed differences from earlier runs are not a speedup or regression claim.
Signed Docs
88537b23e1def210eeff40b7ef90fce92fe2009edocuments this contract. All 45 tests and the complete 2,383-page manual pass, with 436,642 in-bounds word boxes, zero final warnings and visual review of the changed page. An initial double-hyphen ligature was corrected and the full render revalidated. The physical census covers 3,704 source/configuration files, all below 1,000 lines; complete semantic authority and private documentation closure remain open. Exact-head Exsh CI 253/254 and Docs CI 915/916 are running. Symbol providers, ordered runtime binding, cross-object frame paths, source membership, coherent catalog adoption, runnable realms and both complete guest builds remain required.Matching closed dependency intake CI — 16 September 2026: Exsh 253 and 254, exact
9827896d1cb5ad834589045ee03390aec650df84, pass 259 checker controls, 16 isolated imports, 961 Rust tests and the strict preceding build/Clippy/rustdoc stages. All four workspace domains per run and Markdown pass. The required full frame gate remains incomplete, with 111/111/74/74 unresolved observations in each CI artifact set. Four complete logs total 315,052 bytes and contain zero warnings. Original local runtime/all/native replays retain separate input identities and 107/70/299 counts.Docs 915 and 916, exact
88537b23e1def210eeff40b7ef90fce92fe2009e, pass 45 tests and complete 2,383-page renders. Four complete logs total 763,918 bytes. Reference convergence is 35/1/0 warnings across the three TeX passes, with zero final warnings. Both cohorts are classified without rerunning jobs or changing their budgets. The seven-object native dependency inventory is now checked; symbolic providers, ordered runtime binding, cross-object frames and source membership remain incomplete. No runnable realm, coherent product adoption or complete in-EriX build is established.Ordered native symbol evidence — 17 September 2026: signed Exsh
469bf1f1b9d8301cf98a79d16c7c27660ecda2a1enforces root-first depth-first discovery order and positional DT_NEEDED agreement, indexes exact strong/weak providers and preserves object-qualified relative function identities. Duplicate strong definitions fail; missing weak symbols remain zero data. S-only relocations ignore addends, while S+A must retain an exact original executable entry. Names confer no file reads and no load bias is invented.All 276 checker tests, 17 isolated modules and six strict Rust configurations (961 tests each) pass, including host/native Clippy, rustdoc and six warning-free native builds. Independent original-byte inventory matches all 117 symbolic records: 112 exact function identities and five refused data targets. Provider indexing/reporting takes approximately 16 ms in the captured native profile. Original standalone runtime/all/native replays preserve 107/70/299 unresolved observations and actual exit 1 under unchanged budgets. This is conditional relative identity evidence only: load-base arithmetic, protected slots, cross-object calls/frames and source membership remain incomplete.
Signed Docs
24cefeb2dc6d3f163140d32f5fed5a7e1a768ebdupdates the manual contract. All 45 documentation tests pass; the complete 2,383-page render has 436,737 in-bounds word boxes, zero final warnings and visual review of pages 2284–2285. The physical audit covers 3,706 source/configuration files, all below 1,000 lines. No runtime Rust, dependency, linker or workflow inputs changed. New host/CLI controls cover the analyzer behavior; no new guest feature is asserted. Exsh CI 255/256 is terminal: unit/strict/workspace stages pass, and the required full-frame gate remains incomplete. Docs CI 917/918 passes. Acceptance remains 15/459 leaves, 3.48% weighted. Both full in-EriX builds and the complete semantic authority audit remain open.Ordered-provider automatic CI classification — 17 September 2026: Exsh 255/256 at
469bf1f1b9d8301cf98a79d16c7c27660ecda2a1passes 961 Rust tests, the combined 276-test checker suite, strict preceding stages and all four workspace domains per run. The required full-frame gate fails with 111/111/74/74 unresolved observations per run. Four complete logs total 315,035 bytes with zero warnings. The 17 separate module executions are local evidence; CI uses combined test discovery.Docs 917/918 at
24cefeb2dc6d3f163140d32f5fed5a7e1a768ebdpasses 45 tests and the complete 2,383-page manual. Four complete logs total 763,878 bytes. Reference-resolution passes produce 35/1/0 warnings; final output has zero warnings and no layout overflow. Original API snapshots remain unchanged. Both cohorts are fully classified, without restarting workflows or changing thresholds. Original Integration layout, quota and FAT32 failures remain open, including #58 in Integration. Acceptance remains 15/459 leaves, 3.48% weighted. Complete native source/frame proof, a runnable realm, the full semantic authority audit and both full in-EriX builds remain required.Protected cross-object frame evidence — 17 September 2026: signed Exsh
ac9646c84e432129a872737789a9be08f984b881composes the seven explicitly selected native objects using protected relative/symbolic slots and object-qualified function identities. Local control-flow offsets cannot alias a foreign function or transfer the root fallback role. Register facts, grounded preservation/no-return dependencies and route accounting retain the selected object. Every captured decode shares the original output/time budgets; a late failure rejects the invocation. Native reports use schema 3; standalone schema 2 and input schema 1 remain unchanged.All 299 checker tests and 20 separately executed module suites pass. Six strict Rust configurations pass 961 tests each, host/native Clippy, rustdoc and six warning-free native builds; formatting and Markdown checks pass. Original runtime/all replays retain 107/70 unresolved observations. The composed native graph reaches 275 functions with 111 unresolved observations; all three actual checker exits remain 1. Native slots assume successful checked linking and unchanged disjoint mappings. Actual load bases, complete source/frame acceptance and coherent runtime adoption remain open.
Profiling identified redundant root-only analysis in native mode. Removing it preserved every composed decision while one profile changed from 41.52 to 25.81 seconds and 64.37M to 39.61M calls. This host profile pair includes observer overhead and gives no general or guest timing guarantee. The final source replay also preserves every decision; three register-proof records now correctly identify symbolic load provenance.
Signed Docs
44cd6c4aa95bebfa08c99804fab0f1551f537ae1specifies the contract. All 45 documentation tests pass; the complete 2,383-page manual has 436,894 in-bounds word boxes, zero final warnings and visual review of the changed page. All 3,713 inventoried source/configuration files are below 1,000 lines. The broader documentation audit retains 108 unchanged older test definitions needing inline docstrings; current production and all new/modified definitions are documented. Runtime Rust, dependency, linker and workflow inputs are unchanged; added behavior has host and real CLI regressions, with no new guest runtime feature asserted. Original Exsh CI 257/258 passes unit/strict/workspace stages and retains the required full-frame failure; Docs CI 919/920 passes. Both cohorts are fully classified. Both full builds inside EriX and complete semantic authority acceptance remain open.Cross-object checkpoint CI classification — 17 September 2026: Exsh 257/258 at
ac9646c84e432129a872737789a9be08f984b881passes 961 Rust tests, the combined 299-test checker suite, strict preceding stages and four workspace domains per run. Combined discovery also checks isolated module imports; the 20 separate module-suite executions are additional local evidence. The required full-frame gate fails with 111/111/74/74 unresolved observations on the four original CI artifact selections. Four complete logs total 315,180 bytes with zero warnings. Those CI selections remain distinct from the retained seven-object native replay.Docs 919/920 at
44cd6c4aa95bebfa08c99804fab0f1551f537ae1passes 45 tests and the complete 2,383-page manual. Four complete logs total 763,906 bytes; reference-resolution passes have 35/1/0 warnings, with zero final warnings or layout overflow. Both automatic cohorts are fully classified without workflow restarts or threshold changes. Existing Integration layout, quota and FAT32 regressions remain open. Full native source/frame acceptance, coherent runtime adoption, the semantic authority audit and both full builds inside EriX remain required.Saved-value preservation design — 17 September 2026: extend ordinary-call contracts with function-local entry-value tokens and exact stack-relative slot identities. Tokens can prove equality with an existing incoming register value; they cannot create a function target. Full-width copies and checked saves/restores retain identity, while conflicting joins, partial writes, deallocation/reuse, unknown memory aliases and unsupported effects destroy it.
A separate grounded callee contract must establish that every reached write is confined below its incoming stack pointer before caller-owned saved slots survive that call. Callee registers still require their own preservation facts. Unknown stores, unknown calls and recursive premises supply no initial contract. Frame-relative addresses, write extents and control flow must come from original checked bytes, and all earlier dependencies remain in the receipt. Existing stack, time, byte, source-membership and full-acceptance gates stay unchanged.
The observed startup iterator also writes through unproved pointer aliases. Its push/pop shape alone is insufficient and must remain refused unless those effects are independently resolved. Controls will cover wrong restored registers, partial/overlapping writes, alternate paths, slot reuse, foreign callees and cyclic dependencies. This design advances the existing full-frame obligation without an ABI mask or new source/memory-safety assumption.
Saved-value preservation evidence — 17 September 2026: signed Exsh
8b6b93a329757ae7f106e235761912b58a67deffderives incoming-register equality through exact full-width copies and owned live stack slots. Original byte decoders bind register, width and address forms. Partial or unknown aliases, conflicting paths, deallocation and reuse invalidate saved facts. Entry tokens carry equality only; they never supply a pointer or call target. A separate earlier callee contract must prove private stack writes before caller slots survive a call. Checked signed bounds and finite dependency order prevent wrapped offsets and recursive assumptions from granting evidence.All 329 checker tests and 22 separately executed module suites pass. Six strict Rust configurations pass 961 tests each, host/native Clippy, rustdoc and six warning-free native builds; formatting and Markdown checks pass. Independent eager scheduling controls agree with both filtered worklist orders. Original runtime/all/native replays retain 107/70/111 unresolved observations and actual checker exit 1. The native graph still reaches 275 functions. The startup iterator's unknown pointer writes remain a refusal; complete source/frame and runtime acceptance remain open.
Two initial native profiles exhausted the original 60-second budget and produced empty reports; both failures are retained. Immutable decode caches, retirement of exhausted equality state, fact-sensitive wakeups and dependency-first scheduling brought the final native replay within the unchanged budget: 57.45 seconds wall time, 53.94 profiled seconds and 72.27M calls. All 2,373 bodies are inspected once. This bounds one retained host replay and makes no general speedup or guest timing claim. Report schemas and original source, stack, byte and time gates are unchanged.
Signed Docs
c3401e5f6bbc19a0ba695219ed551e29a29677edspecifies the contract. All 45 documentation tests pass; the complete 2,383-page manual has 436,968 in-bounds word boxes, zero final warnings and visual review of both changed continuation pages. All 3,717 inventoried source/configuration files are below 1,000 lines. The touched preservation tests now document 21 older methods; 87 unchanged older test definitions remain in the inline documentation audit. Current production and all new/modified definitions are documented. Runtime Rust, dependency, linker and workflow inputs are unchanged; no new guest runtime feature is asserted. Original Exsh CI 259/260 passes unit/strict/workspace stages and retains the required full-frame failure; Docs CI 921/922 passes. Both cohorts are fully classified. Both full builds inside EriX and complete semantic authority acceptance remain open.Caller-bound write requirements — 17 September 2026: the original iterator and its parser callees have complete ordinary frame shapes, but writes through incoming arguments prevent an unconditional saved-register contract. The original environment parser also contains a one-byte SETcc memory write; an implementation must bind that write extent to its actual encoding. Local caller instructions suggest stack-relative argument locations, but that arithmetic is not an all-path callsite proof.
The next implementation will represent formal entry-register plus checked displacement as an unmet write/nonalias requirement. Such a symbolic expression grants no pointer, read, write or target authority. Consumption must bind the requirement to original caller CFG facts, exact object/call identity and live stack ownership. Nested substitutions and every partial/overlapping write must retain the slot invalidation rules. Conflicting or missing arguments, wrapped arithmetic, unknown memory effects and ungrounded recursive dependencies must refuse. A conditional result may be used only at a call whose premises are proved; it cannot become an unconditional function mask. Full source membership and memory safety remain separate obligations.
Validation must include missing/contradictory bindings, overlapping and reused storage, nested callees, loop joins, recursive premises and encoded-width disagreement. Original artifact selections, profiler deadlines and source/frame gates remain unchanged. This is a design boundary, with no new preservation fact or acceptance claim.
Saved-value checkpoint CI classification — 17 September 2026: Exsh 259/260 at
8b6b93a329757ae7f106e235761912b58a67deffpasses 961 Rust tests, the combined 329-test checker suite, strict preceding stages and four workspace domains per run. Combined discovery checks isolated module imports; the 22 separate module-suite executions are additional local evidence. The required full-frame gate fails with 111/111/74/74 unresolved observations on its four original CI artifact selections. Four complete logs total 315,234 bytes with zero warnings. These CI selections remain distinct from the retained seven-object native replay.Docs 921/922 at
c3401e5f6bbc19a0ba695219ed551e29a29677edpasses 45 tests and the complete 2,383-page manual. Four complete logs total 763,958 bytes; reference-resolution passes have 35/1/0 warnings, with zero final warnings or layout overflow. Both automatic cohorts are fully classified without workflow restarts or threshold changes. Existing Integration layout, quota and FAT32 regressions remain open. Full native source/frame acceptance, coherent runtime adoption, the semantic authority audit and both full builds inside EriX remain required.Context feasibility design — 17 September 2026: exact caller instances currently repeat expensive interpretations of functions that cannot establish the requested bounded-effects contract. A separate scheduling analysis will test the most favorable preservation of existing ordinary GP facts. Its output must carry a distinct non-proof status and cannot enter preservation, return, target or route proof ledgers. It does not assume a calling convention or provide an actual callee mask.
Negative inference also requires compatible abstract fact domains. An independent control showed that retaining a pointer identity can prevent storing numeric bounds across comparisons, whereas its actual clobber can permit those bounds. A candidate with a nonnumeric consumer therefore defers to actual instance interpretation. Only a compatible candidate whose favorable retention still leaves an unresolved control edge or opaque kernel effect may reject a request. Real positive evidence must still come from complete original-body interpretation with grounded callee contracts, actual caller bindings and live storage intervals. Candidate analysis and propagation share the original deadline. Filtered/unfiltered controls must include a case where proved restoration removes an opaque branch, so scheduling does not erase a valid conditional proof. Full source/frame and self-hosting acceptance remain open.
Caller-bound stack preservation — 17 September 2026: signed Exsh
e7ba974e96ee77a41c6a861150da843d4c84c7d6binds formal GP arguments to independently proved live caller stack intervals. Exact callee write spans preserve return-address gaps and invalidate every overlapping save. Scoped masks never enter the unconditional function index; loaded words, unknown contents, released storage and recursive assumptions supply no binding. Byte-checked SETcc writes exactly one unknown byte.All 355 checker tests and 23 separately executed module suites pass. Six strict Rust configurations pass 961 tests each, host/native Clippy, private rustdoc and six warning-free native builds. Formatting, templates and Markdown pass. Original runtime/all/native replays retain 97/60/97 unresolved observations and actual exit 1. The native graph reaches 275 functions; the startup iterator now has caller-bound preservation for its exact live buffers. Complete source/frame and runtime acceptance remain open.
Profiling exposed repeated failed argument specializations. Mandatory opaque-prefix refusals, conservative GP demand and rejection-only control candidates avoid unnecessary interpretations without changing the original 60-second limit. Candidate records cannot become proofs, and incompatible fact kinds defer to actual interpretation: losing pointer identity can enable numeric refinement. Positive and negative controls compare filtered and eager behavior. Each CFG site has at most one pending visit and later changes still enqueue it without an iteration cap; every native proof decision agrees with the prior queue.
The final ordinary native replay takes 39.80 seconds. Complete tracing still exhausted the original deadline; failures and empty reports are retained. A separately identified selective profile measures only caller-context analysis: the complete invocation takes 56.59 seconds, with 26.92 profiled seconds in that scope. Instrumentation preserves the complete proof result. Different profiling scopes are not timing comparisons, and no guest performance claim is made. The replay selects 367 instances, evaluates 587 bodies, proves 190 and defers 51 candidate bodies for incompatible domains.
Signed Docs
fc3ee44748c20a3aa6f55bd85ac1913c707e5d4especifies these contracts. All 45 documentation tests pass. The complete 2,385-page manual has 437,275 in-bounds word boxes, zero final warnings and visual review of the changed pages. All 3,721 inventoried source/configuration files are below 1,000 lines. All new/modified definitions are documented; 87 unchanged older test definitions remain in the audit. Runtime Rust, dependencies, linker and workflow inputs are unchanged. Original Exsh CI 261/262 passes unit/strict/workspace stages and retains the required full-frame failure; Docs CI 923/924 passes. Both cohorts are fully classified. Complete semantic authority acceptance, coherent runtime adoption and both full builds inside EriX remain required.Next syscall-memory boundary — 17 September 2026: the caller-bound checkpoint resolves the initial iterator calls, but a later query-local-cap loop still lacks preserved target facts. Original native thunk bytes save GP values around SYSCALL; that alone cannot prove that kernel effects leave the saved slots intact. Ordinary frame completeness and a local syscall-number immediate are insufficient.
Keep the refusal until an explicit grounded kernel-memory effect contract or independently proved path exclusion exists. Any specialized syscall selector and arguments must come from actual caller CFG facts with exact native object identity and selected kernel/source/artifact evidence. Do not introduce a generic ABI mask, symbol-name exemption or unobserved kernel guarantee. Require negative controls for unknown/conflicting selectors, pointer-output overlap, nested calls and relevant interrupted return paths. Preserve original time, byte, stack and complete source/frame gates. This is a design requirement and diagnostic boundary, not an admitted proof or guest acceptance.
Caller-bound checkpoint CI classification — 17 September 2026: Exsh 261/262 at
e7ba974e96ee77a41c6a861150da843d4c84c7d6passes 961 Rust tests, the combined 355-test checker suite, strict preceding stages and four workspace domains per run. Combined discovery checks isolated module imports; the 23 separate module-suite executions are additional local evidence. The required full-frame gate fails with 101/101/64/64 unresolved observations on its four original CI artifact selections. Four complete logs total 315,210 bytes with zero warnings. These CI selections remain distinct from the retained seven-object native replay.Docs 923/924 at
fc3ee44748c20a3aa6f55bd85ac1913c707e5d4epasses 45 tests and the complete 2,385-page manual. Four complete logs total 764,350 bytes; reference-resolution passes have 35/1/0 warnings, with zero final warnings or layout overflow. Both automatic cohorts are fully classified without workflow restarts or threshold changes. Existing Integration layout, quota and FAT32 regressions remain open. Full native source/frame acceptance, coherent runtime adoption, the semantic authority audit and both full builds inside EriX remain required.Explicit query caller context — 17 September 2026: isolate query-local-cap dispatch in a documented module. Resolve the kernel-attributed current TCB record once, validate the requested slot against that same record, and pass its explicit CSpace identity to both capability and endpoint-kind lookup. A descriptive source slot or process ID must never select a different owner, and a missing caller must retain DENIED rather than use the bootstrap root fallback.
Share the pure checked window predicate with the existing current-caller checks. Preserve parameter/error precedence, result-register encoding, diagnostics and the register-only wire interface. Add focused controls for a private CSpace shadowing root slots, denied/missing callers, malformed parameters and metadata observations without capability mutation. Keep new definitions documented and split the almost-full dispatch source by responsibility.
This removes repeated ambient CSpace selection and makes the memory-effect audit smaller; it does not itself certify the retained older kernel ELF. Keep the original syscall preservation refusal until selected kernel/source/artifact evidence and the relevant memory effects are grounded. Validate strict kernel feature matrices, applicable native/runtime controls, documentation and original automatic CI before claiming acceptance.
Caller-local query checkpoint — 17 September 2026: signed Kernel
e15a045d7701030e58d9e59517406f8c79694ff8selects one attributed TCB record for checked-window validation and both explicit CSpace metadata reads. Four added host controls cover independent owners, root shadows, missing callers, malformed inputs and unchanged inventories. Query results retain the register-only wire contract and clear descriptive payloads on errors.Four strict development/release default/all-feature matrices pass 670/694 unit tests plus two external controls, with three existing ignores. Formatting, host/native Clippy, private rustdoc and thirteen native binaries pass without warnings. Original kernel CI 578/579 both pass; all four complete terminal logs contain no warnings.
The selected native image passes fifteen actual CPL3 queries with exact metadata, RSP, six saved-register and sixteen live-stack-word comparisons across three private owners, then all existing invocation custody/retirement checks. The separate lifetime/revocation scenario also passes all original markers. Both use one TCG CPU and unchanged 60-second deadlines. The first canary fixture failure is retained in kernel issue 16; the corrected fixture explicitly selects its owned stack before testing syscall preservation. This is finite selected-image evidence, not a generic kernel memory guarantee or full guest build.
The existing full source/frame refusals remain required. No syscall mask is admitted by this checkpoint; selected kernel/source/artifact effects must still be grounded at the actual callsite.
Tracking and rollout
Dependency adoption frame evidence — 15 September 2026
The unpublished dependency-alignment worktree based on
7f9552abf3507b464921361fb985853525aef12dpasses 957 tests in each default/all-feature and production development/release configuration, formatting, strict host/native Clippy, eight native builds, private rustdoc and 59 checker fixtures. Both actual optimized frame inspections still exit 1 with explicit incomplete source domains and 700/613 unresolved observations. Intake reports contain no top-level issues; the selected disassembler runs successfully. This agrees with the existing incomplete proof documented here and does not establish an overflow, stack safety or a passing complete CI gate. The frame limits and CI requirements remain unchanged. The dependency update is not published or accepted for product-image adoption. An earlier local quiet compile exceeded its inactivity deadline before tests; its cleaned-up failure remains retained, and the longer bounded continuation passed.feature/posix-compat; update linked WIP PRs after coherent signed checkpoints using canonical CONTRIBUTING.md messages.70521817b0c8d907e765b0d8ef8ed1eaa89f67ce; refresh component/dependency heads and their own CI evidence as implementation advances.Original terminal-accounting graph validation — 21 September 2026:
Signed 0d5d5ad9aff082ca75ec79dbc9c29d73f799d8ed adopts the original shared terminal-observation, exact-acknowledgement and final-CPU dependencies. Both development configurations pass 976 Rust tests; all four host/native Clippy, warning-denied host/native build, applicable doctest and private-rustdoc selections pass. All 355 checker controls pass. The shell implementation and release optimization/LTO policy are unchanged.
The new graph independently retains two release unit-test compilation failures:
cargo test --locked --offline --release --all-targetsstops at 126.117857 seconds andcargo test --locked --offline --all-features --release --all-targetsat 120.024146 seconds. Both reach the existing 120-second silence bound within the 600-second hard bound; the child exits on signal 15, the owner reports status 124, and cleanup succeeds. No release unit test executes. These are new original-graph observations in compiler regression 9, with all prior failures retained. The cause needs an actual compiler profile; no optimization, LTO or deadline setting was relaxed.Actual runtime and all-feature PIC artifacts are checked in both deployment profiles using the maintained frame configuration. All four reports return incomplete proof (exit 1), with 97 unresolved routes for runtime and 63 for all features. Workspace mapping passes separately. The original ELF and packaged artifact digests, selected tool/helper identities and failed reports remain retained. Frame regression 4 stays open. Original CI 275/276 is being observed without restart.
The WIP PR awards no complete runtime or self-hosting acceptance. Actual service CPU/profiler VMs, complete authority/source/effect/frame proof, native external Rust/LLVM/runtime rebuilding and both full EriX guest build generations remain required in Phase 6 completion.
Original terminal-graph CI classification — 21 September 2026:
Signed
0d5d5ad9aff082ca75ec79dbc9c29d73f799d8edreaches actual analysis in both original CI 275/276. Each passes 976 unit tests and 355 checker controls before the required frame gate fails. Each run retains four incomplete reports: 101 unresolved runtime observations in both profiles and 68 all-feature observations in both profiles. All four workspace mappings pass separately. These CI artifact observations differ from local 97/63 results and are not interchangeable proof.All four terminal logs are complete and hash-verified (319,902 bytes), with zero warnings. The disassembler intake correction reaches the real proof boundary; tool-selection issue 5 is resolved. Complete frame issue 4 and local release compiler issue 9 remain open. No workflow restart, bound change or conversion of incomplete evidence to a pass occurred.
[FEATURE] [P02.R17] Audit authority, code quality and documentation in exshto [FEATURE] Audit authority, code quality and documentation in exsh