Disjoint ordinary-host register banks

Main results

• preprocessing_injective, host_injective, controller_injective: actual bank embeddings.
• extend_controller, extend_host_controller, extend_preprocessing_controller: register readback and frames used by the complete controller.

These finite bank proofs are original.

theorem Cslib.Algorithms.WordRAM.ThreeSum.Decision.preprocessing_injective (r : ℕ) : Function.Injective (preprocessingRegisters r)

Preprocessing occupies its original first 128 registers.

theorem Cslib.Algorithms.WordRAM.ThreeSum.Decision.host_injective (r : ℕ) : Function.Injective (hostRegisters r)

The host/callee bank retains every original register separately.

theorem Cslib.Algorithms.WordRAM.ThreeSum.Decision.controller_injective (r : ℕ) : Function.Injective (controllerRegisters r)

The outer controls occupy sixteen distinct registers after both callees.

theorem Cslib.Algorithms.WordRAM.ThreeSum.Decision.controller_ne_host {r : ℕ} (i : Fin 16) (j : Fin (64 + (r + 7))) : controllerRegisters r i ≠ hostRegisters r j

No outer control aliases a host or solver register.

theorem Cslib.Algorithms.WordRAM.ThreeSum.Decision.extend_controller {r : ℕ} (a : WordRAM.Data 16) (x : WordRAM.Data (registerCount r)) (i : Fin 16) : (WordRAM.Data.extend (controllerRegisters r) a x).regs (controllerRegisters r i) = a.regs i

Read an embedded controller result.

theorem Cslib.Algorithms.WordRAM.ThreeSum.Decision.extend_host_controller {r : ℕ} (a : WordRAM.Data (64 + (r + 7))) (x : WordRAM.Data (registerCount r)) (i : Fin 16) : (WordRAM.Data.extend (hostRegisters r) a x).regs (controllerRegisters r i) = x.regs (controllerRegisters r i)

A host call cannot overwrite any outer control.

theorem Cslib.Algorithms.WordRAM.ThreeSum.Decision.extend_preprocessing_controller {r : ℕ} (a : WordRAM.Data 128) (x : WordRAM.Data (registerCount r)) (i : Fin 16) : (WordRAM.Data.extend (preprocessingRegisters r) a x).regs (controllerRegisters r i) = x.regs (controllerRegisters r i)

Preprocessing cannot overwrite the saved length or outer controls.

theorem Cslib.Algorithms.WordRAM.ThreeSum.Decision.extend_controller_preprocessing {r : ℕ} (a : WordRAM.Data 16) (x : WordRAM.Data (registerCount r)) (i : Fin 128) : (WordRAM.Data.extend (controllerRegisters r) a x).regs (preprocessingRegisters r i) = x.regs (preprocessingRegisters r i)

Reading the preprocessing bank after a controller-only operation sees the old registers.