Width-independent native program prefixes

An execution that halts at one width identifies every successful prefix at a larger width when the program does not read physical width. These rules apply to both complete native frontends and programs that compose them.

Main results

• Code.readsWidth_rename: register renaming does not change width observation.
• Runs.prefix_at_smaller_width: wider prefixes agree with an admitted smaller-width execution.

These determinism and representation lemmas are original.

theorem Cslib.WordRAM.Code.readsWidth_rename {B : Basis} {r r' : ℕ} (f : Fin r → Fin r') (c : Code B r) : (rename f c).ReadsWidth ↔ c.ReadsWidth

Register renaming never changes whether a structured program observes physical width.

theorem Cslib.WordRAM.Runs.prefix_at_smaller_width {B : Basis} {w w' r : ℕ} {p : Program B r} (hp : ¬p.ReadsWidth) (hw : w ≤ w') {s t : State r} {k v total : ℕ} (hwide : Runs w' p s t k) (hlow : Executes w p s v total) : Runs w p s t k

Every wider prefix is the same smaller-width prefix if that smaller execution halts.

theorem Cslib.WordRAM.Op.eval_mem_above {B : Basis} {r w a : ℕ} {o : Op B r} {x y : Data r} (h : eval w o x = some y) (hx : Data.Bounded w x) (ha : 2 ^ w ≤ a) : y.mem a = x.mem a

A native instruction cannot write memory above the admitted address-word universe.

theorem Cslib.WordRAM.Next.mem_above {B : Basis} {r w a : ℕ} {p : Program B r} {s t : State r} (h : Next w p s t) (hs : Data.Bounded w s.data) (ha : 2 ^ w ≤ a) : t.data.mem a = s.data.mem a

A complete native step preserves memory beyond the admitted address-word universe.

theorem Cslib.WordRAM.Runs.mem_above {B : Basis} {r w a : ℕ} {p : Program B r} {s t : State r} {n : ℕ} (h : Runs w p s t n) (hs : Data.Bounded w s.data) (ha : 2 ^ w ≤ a) : t.data.mem a = s.data.mem a

A native run preserves every cell above its admitted address-word universe.