Theory MachineEquations

section ‹Arithmetization of Register Machines›

subsection ‹A first definition of the arithmetizing equations›

theory MachineEquations
  imports MultipleStepRegister MultipleStepState MachineMasking
begin
 
definition mask_equations :: "nat ⇒ (register ⇒ nat) ⇒ (register ⇒ nat)
                              ⇒ nat ⇒ nat ⇒ nat ⇒ nat ⇒ bool" (* 4.15, 4.17 and 4.20 *)
  where "(mask_equations n r z c d e f) = ((∀l<n. (r l) ≼ d)
                                           ∧ (∀l<n. (z l) ≼ e)
                                           ∧ (∀l<n. 2^c * (z l) = (r l + d) && f))"

(* REGISTER EQUATIONS *)
definition reg_equations :: "program ⇒ (register ⇒ nat) ⇒ (register ⇒ nat) ⇒ (state ⇒ nat)
                             ⇒  nat ⇒ nat ⇒ nat ⇒ nat ⇒ bool" where
  "(reg_equations p r z s b a n q) = (
    ― ‹4.22› (∀l>0. l < n ⟶ r l =     b*r l + b*∑R+ p l (λk. s k) - b*∑R- p l (λk. s k && z l))
  ∧ ― ‹4.23› (      r 0 = a + b*r 0 + b*∑R+ p 0 (λk. s k) - b*∑R- p 0 (λk. s k && z 0))
  ∧ (∀l<n. r l < b ^ q)) ― ‹Extra equation not in Matiyasevich's book.
                                      Needed to show that all registers are empty at time q›"

(* STATE EQUATIONS -- todo from here on *)
definition state_equations :: "program ⇒ (state ⇒ nat) ⇒ (register ⇒ nat) ⇒ 
                              nat ⇒ nat ⇒ nat ⇒ nat ⇒ bool" where
  "state_equations p s z b e q m = (
― ‹4.24› (∀d>0. d≤m ⟶ s d =     b*∑S+ p d (λk. s k) + b*∑S- p d (λk. s k && z (modifies (p!k)))
                                                 + b*∑S0 p d (λk. s k && (e - z (modifies (p!k)))))
     ∧ ― ‹4.25› (       s 0 = 1 + b*∑S+ p 0 (λk. s k) + b*∑S- p 0 (λk. s k && z (modifies (p!k)))
                                                 + b*∑S0 p 0 (λk. s k && (e - z (modifies (p!k)))))
     ∧ ― ‹4.27› (s m = b^q)
     ∧ (∀k≤m. s k ≼ e) ∧  (∀k<m. s k < b ^ q) ― ‹these equations are not from the book›
     ∧ (∀M≤m. (∑k≤M. s k) ≼ e) ― ‹this equation is added, too› )"

(* The following two equations do not appear in Matiyasevich's book, this duplicated definition
   (note that they are also included just above) is, for now, only a reminder. *)
definition state_unique_equations :: "program ⇒ (state⇒nat) ⇒ nat ⇒ nat ⇒bool" where
  "state_unique_equations p s m e = ((∑k=0..m. s k) ≼ e ∧ (∀k≤m. s k ≼ e))"


(* RM CONSTANTS FOR DEFINITION AND CLARIFY OF EQUATIONS *)
definition rm_constants :: "nat ⇒ nat ⇒ nat ⇒ nat ⇒ nat ⇒ nat ⇒ nat ⇒ bool" where
  "rm_constants q c b d e f a = (
       ― ‹4.14› (b = B c)
     ∧ ― ‹4.16› (d = D q c b)
     ∧ ― ‹4.18› (e = E q b) ― ‹4.19 left out (compare book)›
     ∧ ― ‹4.21› (f = F q c b)
     ∧ ― ‹extra equation not in the book› c > 0
     ∧ ― ‹4.26› (a < 2^c) ∧ (q>0))"

definition rm_equations_old :: "program ⇒ nat ⇒ nat ⇒ nat ⇒ bool" where
  "rm_equations_old p q a n = (
    ∃ b c d e f :: nat.
    ∃ r z :: register ⇒ nat.
    ∃ s :: state ⇒ nat.
     mask_equations n r z c d e f
     ∧ reg_equations p r z s b a n q 
     ∧ state_equations p s z b e q (length p - 1)
     ∧ rm_constants q c b d e f a)"

end