[thotypous]

An independently authored x86-64 loop writes six 64-bit stack elements, then reads both 32-bit words of the final element. The unpatched output declares only five elements and returns unrelated, uninitialized scalar locals. Reading the first two words as well selects a 32-bit layout and loses the wide hint's byte extent; reading only the first element's upper word can discard the array layout altogether.

• Forward unit-stride numeric branch constraints through an immediate zero-extension to the existing conditional-read equations. This preserves a narrow loop counter's bound at its wider phi input without restricting operations that also execute on the exit path; wrapped predicates retain both branch outcomes on reachable values.
• Retain a fixed integer subword view inside an open integer array's existing minimum extent. It must fit entirely within one element; locked types, pointers, floats, aggregates, and accesses beyond that extent remain boundaries.
• Apply the same compatibility rule when the partial view overlaps the first element, instead of conceding the indexed storage to a scalar blob.
• When a different integer element width wins at the same base, translate the absorbed index bound through bytes, rounding up to preserve coverage.
• Keep the existing type preference and frame-capacity policy. This does not infer the source declaration's exact array length or add variable-stack allocation recovery.
• Removed two synthetic tests that required the indexed storage to split or lose mapped bytes; the replacement coverage checks shared storage, adjacent-object boundaries, and executable behavior.
• Emit checked, byte-order-aware integer transfers for scalar views into local stack byte arrays, retaining their declarations without invalid artificial C members or wider aliasing casts. Global byte-array transfers remain opt-in.
• Replace three zero-loop output-spelling assertions with an independently authored native regression. It verifies every byte of both records at each call, checks call order, and clobbers the first record's family field so the second record must use the value saved before the loops.

The executable regression uses four authored native functions: tail-word reads, first-and-tail-word reads, a first-cell interior read, and an already-wide predicate control. It compares the generated C with both the original machine code and independent unsigned arithmetic, including wrapping and sign-bit boundaries. It uses the existing integer-view compiler contract (-fno-strict-aliasing, -fwrapv) and enables undefined-behavior sanitization.

Focused local verification:

• Eight existing indexed_stack_stores tests and the new zero-loop regression passed in focused runs. The wide-word round trip covers 2,000 inputs per authored function with GCC/Clang at -O0/-O2; the zero-loop case uses the same compiler matrix and validates both complete 64-byte records.
• cargo test -p kuna-decomp --lib rangeutil::tests: 19 passed, including both outcomes of wrapped, nonwrapped, full, and empty predicates.
• cargo test -p kuna-decomp --lib varmap::tests: 62 passed, including locked storage and adjacent-object boundaries.
• The guard-range, array-extent, array-cover-width, and stack-store-guard stages: 31 assertions passed.
• python3 tools/check_spec.py --strict: passed.
• stack_object_lifetimes::partial_writes_control_flow_and_unknown_memory_effects_match_native: passed unchanged, including strict-aliasing compilation of the local byte-array case that failed the initial CI run.
• mapped_array_c::mapped_byte_accesses_compile_and_preserve_bytes: passed, retaining the global opt-in and byte-transfer behavior.

The full workspace and corpus suites are left to CI.