Native frontend descriptor loads

The controller executes all six memory reads and the fuel copy. The semantic entry is obtained from the existing frontend output relation, including empty compact arrays.

Main results

• loadRoot_exec: exact native descriptor loading, charged execution and memory/register frame.

These representation and native execution proofs are original.

theorem Cslib.Algorithms.WordRAM.ThreeSum.ChanHe.Preprocessing.loadRoot_preserves (i : Fin 128) : ↑i < 64 ∨ 71 ≤ ↑i → i ≠ address → WordRAM.Code.Preserves i loadRoot

A descriptor load changes only the seven current-record slots and its address scratch.

theorem Cslib.Algorithms.WordRAM.ThreeSum.ChanHe.Preprocessing.loadRoot_exec {w U f t : ℕ} {l : Frontend.Layout} {rs : List (ℕ × ℕ)} (x : WordRAM.Data 128) (hx : WordRAM.Data.Bounded w x) (ht : t < l.count) (hc : x.regs current = t) (hd : x.regs descriptors = l.descriptors) (hf : x.regs levels = f) (hs : x.regs stride = 6) (ho : x.regs one = 1) (hfit : WordRAM.Fits w (l.descriptors + 6 * t + 5)) (houtput : Frontend.Output l U rs x.mem) : ∃ (y : WordRAM.Data 128), WordRAM.Exec w loadRoot x y 14 ∧ (entry l U f rs t).Loaded y ∧ y.mem = x.mem ∧ ∀ (i : Fin 128), ↑i < 64 ∨ 71 ≤ ↑i → i ≠ address → y.regs i = x.regs i

Execute all descriptor arithmetic, six native memory reads and the runtime fuel copy.