Residues within linear work space

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

Main results

• Cslib.TreeEval.Reader.addMod_inSpace, .mulMod_inSpace, .negMod_inSpace, .chi_inSpace, .unitInv_inSpace: the residue operations; unitInv p j computes (j + 1) ^ (p - 2) modulo p by repeated multiplication.

theorem Cslib.TreeEval.Reader.addMod_inSpace : Turing.MultiTapeTM.ComputableTidilyInSpace (fun (q : ℕ × ℕ × ℕ) => addMod q.1 q.2.1 q.2.2) Turing.MultiTapeTM.ComputableTidilyInSpace.encNat3 Turing.MultiTapeTM.encNat fun (q : ℕ × ℕ × ℕ) => (Turing.MultiTapeTM.ComputableTidilyInSpace.encNat3 q).length

The sum modulo p, from (p, a, b).

theorem Cslib.TreeEval.Reader.mulMod_inSpace : Turing.MultiTapeTM.ComputableTidilyInSpace (fun (q : ℕ × ℕ × ℕ) => mulMod q.1 q.2.1 q.2.2) Turing.MultiTapeTM.ComputableTidilyInSpace.encNat3 Turing.MultiTapeTM.encNat fun (q : ℕ × ℕ × ℕ) => (Turing.MultiTapeTM.ComputableTidilyInSpace.encNat3 q).length

The product modulo p, from (p, a, b).

theorem Cslib.TreeEval.Reader.negMod_inSpace : Turing.MultiTapeTM.ComputableTidilyInSpace (fun (q : ℕ × ℕ) => negMod q.1 q.2) (Turing.MultiTapeTM.encPair Turing.MultiTapeTM.encNat Turing.MultiTapeTM.encNat) Turing.MultiTapeTM.encNat fun (q : ℕ × ℕ) => ((Turing.MultiTapeTM.encPair Turing.MultiTapeTM.encNat Turing.MultiTapeTM.encNat) q).length

The negation modulo p, from (p, a).

theorem Cslib.TreeEval.Reader.chi_inSpace : Turing.MultiTapeTM.ComputableTidilyInSpace (fun (q : (ℕ × ℕ) × Bool) => chi q.1.1 q.2 q.1.2) (Turing.MultiTapeTM.encPair (Turing.MultiTapeTM.encPair Turing.MultiTapeTM.encNat Turing.MultiTapeTM.encNat) Turing.MultiTapeTM.encBool) Turing.MultiTapeTM.encNat fun (q : (ℕ × ℕ) × Bool) => ((Turing.MultiTapeTM.encPair (Turing.MultiTapeTM.encPair Turing.MultiTapeTM.encNat Turing.MultiTapeTM.encNat) Turing.MultiTapeTM.encBool) q).length

The residue of x or of 1 - x modulo p, from ((p, x), b).

theorem Cslib.TreeEval.Reader.powMod_le {p a k : ℕ} (hk : k ≤ p - 2) : powMod p a k ≤ p + 1

theorem Cslib.TreeEval.Reader.unitInv_inSpace : Turing.MultiTapeTM.ComputableTidilyInSpace (fun (q : ℕ × ℕ) => unitInv q.1 q.2) (Turing.MultiTapeTM.encPair Turing.MultiTapeTM.encNat Turing.MultiTapeTM.encNat) Turing.MultiTapeTM.encNat fun (q : ℕ × ℕ) => ((Turing.MultiTapeTM.encPair Turing.MultiTapeTM.encNat Turing.MultiTapeTM.encNat) q).length

The inverse of the unit of round j, unitInv p j from (p, j).