Preserving complete frontend output

Later native programs may allocate beyond the frontend's endpoint. Its exact descriptor and payload interpretation survives a frame on the concrete allocated prefix.

Main results

• Output.frame: preserve all descriptors and compact payloads below the frontend endpoint.

This memory-frame bridge is original and reuses the existing output and block predicates.

theorem Cslib.Algorithms.WordRAM.ThreeSum.Frontend.Output.frame {l : Layout} {U : ℕ} {rs : List (ℕ × ℕ)} {before after : ℕ → ℕ} (h : Output l U rs before) (hcard : rs.length ≤ l.n) (hp : ∀ p < l.endpoint, after p = before p) : Output l U rs after

A frame on the frontend allocation preserves every descriptor and actual payload word.