Native verification of multiplication carry blocks #
Sixteen local words encode all carries in a short block. Its first and last carries must agree with the same global eight-word tuple used by every block. Native PLUS and exact shifts derive the local column equations; no multiplication relation occurs in the formula.
Main definitions #
Cslib.Logic.FO.Ordered.Multiplication.blockChecks: verify one carry block and its endpoints.
Main results #
Cslib.Logic.FO.Ordered.Multiplication.realize_blockChecks: exact block semantics.
References #
- N. Immerman, Descriptive Complexity, Theorem 1.17(1). This is the carry-table variant of the source's packed short sums.
noncomputable def Cslib.Logic.FO.Ordered.Multiplication.blockChecks (L : FirstOrder.Language) {α : Type u_1} (h e s x y z j : (language L).Term α) (g : Fin 8 → (language L).Term α) :
Check every local carry equation and match both ends with the global boundary words.
Instances For
theorem Cslib.Logic.FO.Ordered.Multiplication.realize_blockChecks {L : FirstOrder.Language} {n : ℕ} [Fact (2 ≤ n)] [L.Structure (Fin n)] {α : Type u_1} (h e s x y z j : (language L).Term α) (g : Fin 8 → (language L).Term α) (v : α → Fin n) (hs : ↑(FirstOrder.Language.Term.realize v s) = 2 ^ ↑(FirstOrder.Language.Term.realize v e)) (hcap : (↑(FirstOrder.Language.Term.realize v s) + 1) * ↑(FirstOrder.Language.Term.realize v s) < n) (hj : ↑(FirstOrder.Language.Term.realize v j) + ↑(FirstOrder.Language.Term.realize v s) < n) (hwidth : 2 ^ ↑(FirstOrder.Language.Term.realize v s) < n) (hspace : 16 * ↑(FirstOrder.Language.Term.realize v h) < n) :
(blockChecks L h e s x y z j g).Realize v ↔ ∃ (w : Fin 16 → Fin n),
have c := fun (t : ℕ) =>
BitString.readPackedField (↑(FirstOrder.Language.Term.realize v h)) (fun (r : Fin 16) => ↑(w r))
(t * ↑(FirstOrder.Language.Term.realize v s)) ↑(FirstOrder.Language.Term.realize v s);
c 0 = BitString.readPackedField (↑(FirstOrder.Language.Term.realize v h))
(fun (r : Fin 8) => ↑(FirstOrder.Language.Term.realize v (g r))) ↑(FirstOrder.Language.Term.realize v j)
↑(FirstOrder.Language.Term.realize v s) ∧ c ↑(FirstOrder.Language.Term.realize v s) = BitString.readPackedField (↑(FirstOrder.Language.Term.realize v h))
(fun (r : Fin 8) => ↑(FirstOrder.Language.Term.realize v (g r)))
(↑(FirstOrder.Language.Term.realize v j) + ↑(FirstOrder.Language.Term.realize v s))
↑(FirstOrder.Language.Term.realize v s) ∧ ∀ t < ↑(FirstOrder.Language.Term.realize v s),
c t + BitString.mulColumn (↑(FirstOrder.Language.Term.realize v x)) (↑(FirstOrder.Language.Term.realize v y))
(↑(FirstOrder.Language.Term.realize v j) + t) = ((↑(FirstOrder.Language.Term.realize v z)).testBit (↑(FirstOrder.Language.Term.realize v j) + t)).toNat + 2 * c (t + 1) ∧ c t + BitString.mulColumn (↑(FirstOrder.Language.Term.realize v x)) (↑(FirstOrder.Language.Term.realize v y))
(↑(FirstOrder.Language.Term.realize v j) + t) < n
The two decoded endpoints agree with the global words, and every interior step is exact.