Register operations within linear work space

The register operations of Cslib.TreeEval.Reader are tidily computable within work space linear in the lengths of their encoded arguments.

Main results

• Cslib.TreeEval.Reader.get_inSpace, .set_inSpace: selecting and replacing a register.
• Cslib.TreeEval.Reader.scale_inSpace: multiplying a register by a residue.
• Cslib.TreeEval.Reader.subtractSums_inSpace: subtracting a multiple of the sums of a pass.

@[reducible, inline]

abbrev Cslib.TreeEval.Reader.encReg : Fin 3 ↪ List Bool

The encoding of register indices.

theorem Cslib.TreeEval.Reader.get_inSpace {α : Type} {encIn : α ↪ List Bool} {Bs : α → ℕ} {R : α → Regs} {t : α → Fin 3} (hR : Turing.MultiTapeTM.ComputableTidilyInSpace R encIn encRegs Bs) (ht : Turing.MultiTapeTM.ComputableTidilyInSpace t encIn encReg Bs) : Turing.MultiTapeTM.ComputableTidilyInSpace (fun (x : α) => (R x).get (t x)) encIn (Turing.MultiTapeTM.encList Turing.MultiTapeTM.encNat) Bs

Selecting a register, given the registers and the index within a budget.

theorem Cslib.TreeEval.Reader.set_inSpace {α : Type} {encIn : α ↪ List Bool} {Bs : α → ℕ} {R : α → Regs} {t : α → Fin 3} {l : α → List ℕ} (hR : Turing.MultiTapeTM.ComputableTidilyInSpace R encIn encRegs Bs) (ht : Turing.MultiTapeTM.ComputableTidilyInSpace t encIn encReg Bs) (hl : Turing.MultiTapeTM.ComputableTidilyInSpace l encIn (Turing.MultiTapeTM.encList Turing.MultiTapeTM.encNat) Bs) : Turing.MultiTapeTM.ComputableTidilyInSpace (fun (x : α) => (R x).set (t x) (l x)) encIn encRegs Bs

Replacing a register.

theorem Cslib.TreeEval.Reader.scale_inSpace {α : Type} {encIn : α ↪ List Bool} {Bs p a : α → ℕ} {R : α → Regs} {r : α → Fin 3} (hp : Turing.MultiTapeTM.ComputableTidilyInSpace p encIn Turing.MultiTapeTM.encNat Bs) (ha : Turing.MultiTapeTM.ComputableTidilyInSpace a encIn Turing.MultiTapeTM.encNat Bs) (hR : Turing.MultiTapeTM.ComputableTidilyInSpace R encIn encRegs Bs) (hr : Turing.MultiTapeTM.ComputableTidilyInSpace r encIn encReg Bs) (hin : Turing.MultiTapeTM.BigOLe (fun (x : α) => (encIn x).length) Bs) (hB : Turing.MultiTapeTM.BigOLe (fun (x : α) => ((R x).get (r x)).length * ((Turing.MultiTapeTM.encNat (p x)).length + (Turing.MultiTapeTM.encNat (a x)).length)) Bs) : Turing.MultiTapeTM.ComputableTidilyInSpace (fun (x : α) => Regs.scale (p x) (r x) (a x) (R x)) encIn encRegs Bs

Multiplying a register by a residue, within a budget that covers the register with every entry as long as the prime and the factor together.

theorem Cslib.TreeEval.Reader.modifyAt_inSpace {α : Type} {encIn : α ↪ List Bool} {Bs : α → ℕ} {l : α → List ℕ} {i p c : α → ℕ} (hl : Turing.MultiTapeTM.ComputableTidilyInSpace l encIn (Turing.MultiTapeTM.encList Turing.MultiTapeTM.encNat) Bs) (hi : Turing.MultiTapeTM.ComputableTidilyInSpace i encIn Turing.MultiTapeTM.encNat Bs) (hp : Turing.MultiTapeTM.ComputableTidilyInSpace p encIn Turing.MultiTapeTM.encNat Bs) (hc : Turing.MultiTapeTM.ComputableTidilyInSpace c encIn Turing.MultiTapeTM.encNat Bs) : Turing.MultiTapeTM.ComputableTidilyInSpace (fun (x : α) => modifyAt (l x) (i x) (addMod (p x) (c x))) encIn (Turing.MultiTapeTM.encList Turing.MultiTapeTM.encNat) Bs

Changing one entry by adding a residue, modifyAt l i (addMod p c).

theorem Cslib.TreeEval.Reader.subtractSums_inSpace {α : Type} {encIn : α ↪ List Bool} {Bs p c : α → ℕ} {t : α → Fin 3} {acc : α → List ℕ} {R : α → Regs} (hp : Turing.MultiTapeTM.ComputableTidilyInSpace p encIn Turing.MultiTapeTM.encNat Bs) (hc : Turing.MultiTapeTM.ComputableTidilyInSpace c encIn Turing.MultiTapeTM.encNat Bs) (ht : Turing.MultiTapeTM.ComputableTidilyInSpace t encIn encReg Bs) (hacc : Turing.MultiTapeTM.ComputableTidilyInSpace acc encIn (Turing.MultiTapeTM.encList Turing.MultiTapeTM.encNat) Bs) (hR : Turing.MultiTapeTM.ComputableTidilyInSpace R encIn encRegs Bs) (hB : Turing.MultiTapeTM.BigOLe (fun (x : α) => ((R x).get (t x)).length * ((Turing.MultiTapeTM.encNat (p x)).length + 1)) Bs) : Turing.MultiTapeTM.ComputableTidilyInSpace (fun (x : α) => subtractSums (p x) (c x) (t x) (acc x) (R x)) encIn encRegs Bs

Subtracting c times the sums of a pass from a register, within a budget that covers the register with every entry as long as the prime.

theorem Cslib.TreeEval.Reader.mapEqOne_inSpace : Turing.MultiTapeTM.ComputableTidilyInSpace (fun (l : List ℕ) => List.map (fun (x : ℕ) => x == 1) l) (Turing.MultiTapeTM.encList Turing.MultiTapeTM.encNat) Turing.MultiTapeTM.encBits fun (l : List ℕ) => 64 * (((Turing.MultiTapeTM.encList Turing.MultiTapeTM.encNat) l).length + 1)

The bits of a register, l.map (· == 1), encoded as themselves.