MemAlign-family read-soundness discharge (follow-on to #115, gated on MemAlignRom extraction)

[codygunton]

Summary

Follow-on to #115 (see its scope-amendment warning). #115 derives memory-bus read-soundness for
accesses served directly by the mutable Mem table. Accesses routed through the MemAlign family
(unaligned / sub-doubleword loads and stores) are classified and row-corresponded but their
read-soundness is not derived: they retain named structural residues. This issue tracks
discharging those residues so read-soundness covers all RV64IM memory accesses.

The named residues to consume (as of the #115 route-B line, tip 22c8ebcd)

• MemAlignLoadProviderRomValueFacts (ZiskFv/AirsClean/FullEnsemble/Balance/MemBusRowBridges.lean)
  — MemAlignRom-mediated width = ind_width, value_1 = 0, low-value range bounds needed to
  convert a structural provider row into the legacy SubdoublewordLoadProviderWitness.
• MemAlignCoreLookupFacts (ZiskFv/Compliance/SharedBundles.lean) — MemAlignByte /
  MemAlignReadByte core_every_row + RangeLookupWitness bundles (re-packaged from the legacy
  MemAlignWitness).
• ActiveMainMemAlignSelectedProveBranchPins (MemBusRowBridges.lean) — prove-branch selector
  pins for the general-MemAlign provider branch.
• The three per-load branch-exclusion residues in LoadBDirectMutableMemResidues
  (ZiskFv/Compliance/TraceLevelExport/BootSegmentMemorySeed.lean): no_marb / no_mab /
  no_memAlign — under Eliminate the RowTraceCoherence memory trace-coherence floor — follow-on to #76 #115's direct-Mem scope these exclude the MemAlign routes; this issue
  replaces exclusion with derivation.

Why this is genuinely blocked (two prerequisites)

1. MemAlignRom extraction. The ROM/value facts above exist as residues precisely because
   MemAlignRom is not extracted as a first-class Lean table (see the T4 note in
   SharedBundles.lean). Discharge requires extending tools/pil-extract + named-column wrappers
   • composed lookups — the Extend Aeneas extraction to cover ZisK table data + witness builders (reduce hand-modeled Lean) #108 axis. This issue should carry a blockedBy edge to that work.
2. A through-MemAlign timeline argument. MemAlign provider rows do not appear in
   activeMemReplayRowsOfTable / memReplayRows at all (verified in the Eliminate the RowTraceCoherence memory trace-coherence floor — follow-on to #76 #115 route-B review,
   PR #115 post-review: narrow Mem replay and MemAlign residues #239). Read-soundness for a MemAlign-routed access must thread value agreement
   Main pull → MemAlignByte/ReadByte byte assembly → the Mem table's aligned 8-byte reads → the
   accepted replay. No form of this argument exists yet; it is new proof work, not a port.

Acceptance

• The readSound_of_* seed endpoints cover traces containing MemAlign-routed accesses (the
  direct-scope classifier generalizes or gains a MemAlign constructor with derived obligations).
• The residues listed above are consumed by derivations (or demonstrably reduced), with the
  trust/trusted-base.md MemAlign entries updated in the same PR.
• No new ZiskFv.* project axioms; V1/V2/nix run .#test green.

Non-goals

Whole-channel BalancedChannels (#219); cross-segment memory (#103/#76); the Mem cross-row
Component.transition fidelity upgrade (separate #237 follow-on, gated on #226).

[codygunton]

Cross-thread note from the live-provider coverage audit (2026-07-19, full matrix on #279): the audit independently re-confirmed this issue's scope as the MemAlign-general gap — MemAlignLoadProviderRomValueFacts (Compliance/.../MemBusRowBridges.lean:1893-1916) premise-carries the MemAlignRom-derived width/value_1 = 0/value_0-range facts because MemAlignRom is not extracted as a first-class Lean table; additionally 9 cross-row continuity constraints are mirror-dormant and the 8 forward-rotated (+1 rowOffset) constraints are absent even from the extraction (extractor limitation to note when the S4 survey runs).

Coordination constraint for the architecture-refactor thread (PR stack #255+): the refactor must NOT attempt MemAlign-family legacy deletion before this issue lands — its Q2 gate cannot pass while the ROM facts are premise-carried. The two threads converge here; whichever runs first in Mem/MemAlign territory should check the other's STATUS (base checkout STATUS.md is the hub).