Theory Mask_Equations

subsubsection ‹Equations for masking relations›

theory Mask_Equations
  imports "../Register_Machine/MachineMasking" Equation_Setup "../Diophantine/Binary_And"

abbrevs mb = "≼"

begin

context rm_eq_fixes
begin

  text ‹Equation 4.15›  
  definition register_mask :: "bool" where
    "register_mask ≡ ∀l < n. r l ≼ d"
  
  text ‹Equation 4.17›
  definition zero_indicator_mask :: "bool" where
    "zero_indicator_mask ≡ ∀l < n. z l ≼ e"

  text ‹Equation 4.20›
  definition zero_indicator_0_or_1 :: "bool" where
    "zero_indicator_0_or_1 ≡ ∀l<n. 2^c * z l = (r l + d) && f"
  
  definition mask_equations :: "bool" where 
    "mask_equations ≡ register_mask ∧ zero_indicator_mask ∧ zero_indicator_0_or_1"

end

context register_machine
begin

lemma register_mask_dioph:
  fixes d r
  assumes "n = length r"
  defines "DR ≡ (NARY (λl. rm_eq_fixes.register_mask n (l!0) (shift l 1)) ([d] @ r))"
  shows "is_dioph_rel DR"
proof -
  define DS where "DS ≡ [∀<n] (λi. ((r!i) [≼] d))"

  have "eval DS a = eval DR a" for a
  proof -
    have "eval DR a = rm_eq_fixes.register_mask n (peval d a) (list_eval r a)"
      unfolding DR_def by (auto simp add: shift_def list_eval_def)
    also have "... = (∀l < n. (peval (r!l) a) ≼ peval d a)"
      using rm_eq_fixes.register_mask_def ‹n = length r› rm_eq_fixes_def 
            local.register_machine_axioms by (auto simp: list_eval_def)
    finally show ?thesis
      unfolding DS_def defs by simp
  qed

  moreover have "is_dioph_rel DS"
    unfolding DS_def by (auto simp add: dioph)

  ultimately show ?thesis
    by (simp add: is_dioph_rel_def)
qed

lemma zero_indicator_mask_dioph:
  fixes e z
  assumes "n = length z"
  defines "DR ≡ (NARY (λl. rm_eq_fixes.zero_indicator_mask n (l!0) (shift l 1)) ([e] @ z))"
  shows "is_dioph_rel DR"
proof -
  define DS where "DS ≡ [∀<n] (λi. ((z!i) [≼] e))"

  have "eval DS a = eval DR a" for a
  proof -
    have "eval DR a = rm_eq_fixes.zero_indicator_mask n (peval e a) (list_eval z a)"
      unfolding DR_def by (auto simp add: shift_def list_eval_def)
    also have "... = (∀l < n. (peval (z!l) a) ≼ peval e a)"
      using rm_eq_fixes.zero_indicator_mask_def ‹n = length z› 
      rm_eq_fixes_def local.register_machine_axioms by (auto simp: list_eval_def)
    finally show ?thesis
      unfolding DS_def defs by simp
  qed

  moreover have "is_dioph_rel DS"
    unfolding DS_def by (auto simp add: dioph)

  ultimately show ?thesis
    by (simp add: is_dioph_rel_def)
qed

lemma zero_indicator_0_or_1_dioph:
  fixes c d f r z
  assumes "n = length r" and "n = length z"
  defines "DR ≡ LARY (λll. rm_eq_fixes.zero_indicator_0_or_1 n (ll!0!0) (ll!0!1) (ll!0!2)
                             (nth (ll!1)) (nth (ll!2))) [[c, d, f], r, z]"
  shows "is_dioph_rel DR"
proof -
  let ?N = 2
  define c' d' f' r' z' where pushed_def: "c' = push_param c ?N" "d' = push_param d ?N"
                                "f' = push_param f ?N" "r' = map (λx. push_param x ?N) r"
                                "z' = map (λx. push_param x ?N) z"
  define DS where "DS ≡ [∀<n] (λi. ([∃2] [Param 0 = (Const 2) ^ c'] 
                                        [∧] [Param 1 = (r'!i) [+] d' && f']
                                        [∧] Param 0 [*] (z'!i) [=] Param 1))"

  have "eval DS a = eval DR a" for a
  proof -
    have "eval DR a = rm_eq_fixes.zero_indicator_0_or_1 n (peval c a) (peval d a) (peval f a)
                        (list_eval r a) (list_eval z a)"
      unfolding DR_def defs by (auto simp add: assms shift_def list_eval_def)
    also have "... = (∀l < n. 2^(peval c a) * (peval (z!l) a)
                              = (peval (r!l) a + peval d a) && peval f a)"
      using rm_eq_fixes.zero_indicator_0_or_1_def ‹n = length r› using assms
      rm_eq_fixes_def local.register_machine_axioms by (auto simp: list_eval_def)
    finally show ?thesis
      unfolding DS_def defs pushed_def using push_push apply (auto)
      subgoal for k
        apply (rule exI[of _ "[2^peval c a, peval (r!k) a + peval d a && peval f a]"])
        apply (auto simp: push_list_def assms(1-2))
        by (metis assms(1) assms(2) length_Cons list.size(3) nth_map numeral_2_eq_2)
      subgoal
        using assms by auto
      done
  qed

  moreover have "is_dioph_rel DS"
    unfolding DS_def by (auto simp add: dioph)

  ultimately show ?thesis
    by (simp add: is_dioph_rel_def)
qed


definition mask_equations_relation (‹[MASK] _ _ _ _ _ _›) where
  "[MASK] c d e f r z ≡ LARY (λll. rm_eq_fixes.mask_equations n 
                              (ll!0!0) (ll!0!1) (ll!0!2) (ll!0!3) (nth (ll!1)) (nth (ll!2)))
                              [[c, d, e, f], r, z]"

lemma mask_equations_relation_dioph:
  fixes c d e f r z
  assumes "n = length r" and "n = length z"
  defines "DR ≡ [MASK] c d e f r z"
  shows "is_dioph_rel DR"
proof -
  define DS where "DS ≡ NARY (λl. rm_eq_fixes.register_mask n (l!0) (shift l 1)) ([d] @ r)
  [∧] NARY (λl. rm_eq_fixes.zero_indicator_mask n (l!0) (shift l 1)) ([e] @ z)
  [∧] LARY (λll. rm_eq_fixes.zero_indicator_0_or_1 n (ll!0!0) (ll!0!1) (ll!0!2)
                             (nth (ll!1)) (nth (ll!2))) [[c, d, f], r, z]"

  have "eval DS a = eval DR a" for a
    using DS_def DR_def mask_equations_relation_def rm_eq_fixes.mask_equations_def
    rm_eq_fixes_def local.register_machine_axioms by (simp add: defs shift_def)
    
  moreover have "is_dioph_rel DS"
    unfolding DS_def using assms dioph
    using register_mask_dioph zero_indicator_mask_dioph zero_indicator_0_or_1_dioph
    by (metis (no_types, lifting))

  ultimately show ?thesis
    by (simp add: is_dioph_rel_def)
qed

end

end