Theory K_Gates

section ‹K-Gates›

theory K_Gates
  imports Encoding_Semantics
begin

text ‹The paper's placeholder variables @{text "K≥l"} (equations (9)/(10)) reify
  the clipped cost condition @{text "cost ≥ min{B, max{0, l}}"} with @{text "l ∈ ℤ"}.
  In the paper they are defined via the reification variables @{text "cost≥k"} from
  the encoding family (4)/(5); since the certificate format keeps circuit gates
  disjoint from the encoding's reification variables, we inline that composition:
  a K-gate reifies the clipped threshold ∗‹directly over the cost bits›.  The
  primed copy of such a gate (under @{const primed_circuit}) then constrains
  @{const PrimedCostBit} — exactly the paper's @{text "K'≥l"}.

  The paper proves its Lemmas 1 and 2 with the RED rule (empty witness).  RED with
  an empty witness concludes @{text C} from @{text "C ∪ {¬C} ⊨ C"}, i.e. from
  semantic implication — which is subsumed by the semantic @{thm cpr_derives.rup}
  rule of the formal system, so no additional proof rule is needed.›

subsection ‹Clipping arithmetic›

definition clip :: "nat ⇒ int ⇒ nat" where
  "clip B l ≡ min B (nat l)"

lemma clip_nonpos[simp]: "l ≤ 0 ⟹ clip B l = 0"
  by (simp add: clip_def)

lemma clip_ge_B[simp]: "l ≥ int B ⟹ clip B l = B"
  by (simp add: clip_def min_def nat_le_eq_zle)

lemma clip_in_range[simp]: "0 ≤ l ⟹ l ≤ int B ⟹ clip B l = nat l"
proof -
  assume "0 ≤ l" and "l ≤ int B"
  then have "nat l ≤ B" by simp
  then show ?thesis by (simp add: clip_def min_def)
qed

lemma clip_le_B: "clip B l ≤ B"
  by (simp add: clip_def)

lemma clip_mono:
  assumes "j ≤ j'"
  shows "clip B j ≤ clip B j'"
proof -
  have "nat j ≤ nat j'" using assms by (rule nat_mono)
  then show ?thesis unfolding clip_def by (intro min.mono) auto
qed

lemma nat_add_int_le: "nat (l + int m) ≤ nat l + m"
  by (cases "l ≥ 0") auto

lemma clip_add_le:
  "clip B (l + int m) ≤ clip B l + m"
proof (cases "nat l ≤ B")
  case True
  have "clip B (l + int m) ≤ nat (l + int m)" by (simp add: clip_def)
  also have "... ≤ nat l + m" by (rule nat_add_int_le)
  also have "... = clip B l + m" using True by (simp add: clip_def min_def)
  finally show ?thesis .
next
  case False
  have "clip B (l + int m) ≤ B" by (rule clip_le_B)
  also have "... ≤ clip B l + m" using False by (simp add: clip_def min_def)
  finally show ?thesis .
qed

subsection ‹K-gates and their semantics›

text ‹The gate triple for a K-gate with name literal @{text r}: it reifies
  @{text "Σ 2^i·cᵢ ≥ clip B l"} over the @{text "bits_needed B"}-bit cost block.
  All new cost bodies use this width so they stay aligned with the
  @{const encode_delta_cost} gates of the transition encoding.›

definition k_gate_body :: "nat ⇒ (nat × 'w pvar literal) list" where
  "k_gate_body B ≡ map (λi. (2^i, Pos (CostBit i))) [0..<bits_needed B]"

definition k_gate :: "'w pvar literal ⇒ nat ⇒ int ⇒
    'w pvar literal × (nat × 'w pvar literal) list × nat" where
  "k_gate r B l ≡ (r, k_gate_body B, clip B l)"

lemma k_gate_forces:
  assumes rho01: "∀x. rho x = 0 ∨ rho x = 1"
    and m: "models (reification r (k_gate_body B) (clip B l)) rho"
  shows "eval_lit r rho = 1 ⟷ bits_val (bits_needed B) CostBit rho ≥ clip B l"
  using cost_threshold_gate_forces[OF rho01 m[unfolded k_gate_body_def]] .

text ‹Lemma 1 of the paper, semantically: if the cost bits witness the larger
  clipped threshold @{text "clip B (j + k)"}, they witness the smaller one
  @{text "clip B j"}.  At the gate level: a true K-gate for @{text "j + k"}
  forces the K-gate for @{text j}.›

lemma k_gate_mono_semantic:
  assumes rho01: "∀x. rho x = 0 ∨ rho x = 1"
    and m_hi: "models (reification r_hi (k_gate_body B) (clip B (j + int k))) rho"
    and m_lo: "models (reification r_lo (k_gate_body B) (clip B j)) rho"
    and hi: "eval_lit r_hi rho = 1"
  shows "eval_lit r_lo rho = 1"
proof -
  have "bits_val (bits_needed B) CostBit rho ≥ clip B (j + int k)"
    using k_gate_forces[OF rho01 m_hi] hi by simp
  moreover have "clip B j ≤ clip B (j + int k)"
    by (rule clip_mono) simp
  ultimately have "bits_val (bits_needed B) CostBit rho ≥ clip B j"
    by simp
  then show ?thesis using k_gate_forces[OF rho01 m_lo] by simp
qed

text ‹Lemma 2 of the paper, semantically: from @{text "cost ≥ clip B l"} and
  @{text "Δc = m"} conclude @{text "cost' ≥ clip B (l + m)"}.  The primed K-gate
  body is the @{const PrimedCostBit} block, which is what @{const primed_circuit}
  produces from a K-gate.›

definition k_gate_body_primed :: "nat ⇒ (nat × 'w pvar literal) list" where
  "k_gate_body_primed B ≡ map (λi. (2^i, Pos (PrimedCostBit i))) [0..<bits_needed B]"

lemma k_gate_primed_forces:
  assumes rho01: "∀x. rho x = 0 ∨ rho x = 1"
    and m: "models (reification r (k_gate_body_primed B) (clip B l)) rho"
  shows "eval_lit r rho = 1 ⟷ bits_val (bits_needed B) PrimedCostBit rho ≥ clip B l"
  using cost_threshold_gate_forces[OF rho01 m[unfolded k_gate_body_primed_def]] .

lemma k_gate_step_semantic:
  assumes rho01: "∀x. rho x = 0 ∨ rho x = 1"
    and mK: "models (reification rK (k_gate_body B) (clip B l)) rho"
    and mK': "models (reification rK' (k_gate_body_primed B) (clip B (l + int m))) rho"
    and mD: "models (encode_delta_cost m (bits_needed B)) rho"
    and K1: "eval_lit rK rho = 1"
    and D1: "rho (ReifDeltaCost m) = 1"
  shows "eval_lit rK' rho = 1"
proof -
  let ?c = "bits_val (bits_needed B) CostBit rho"
  let ?c' = "bits_val (bits_needed B) PrimedCostBit rho"
  have c_ge: "?c ≥ clip B l"
    using k_gate_forces[OF rho01 mK] K1 by simp
  have c'_eq: "?c' = ?c + m"
    using encode_delta_cost_forces[OF rho01 mD] D1 by simp
  have "clip B (l + int m) ≤ clip B l + m"
    by (rule clip_add_le)
  also have "... ≤ ?c + m" using c_ge by simp
  also have "... = ?c'" using c'_eq by simp
  finally show ?thesis
    using k_gate_primed_forces[OF rho01 mK'] by simp
qed

text ‹Bit-level form of the premise @{text "cost ≥ clip B l"} as a PB constraint —
  used when a deduction-style hypothesis set assumes a clipped cost bound
  directly (the analogue of @{const cost_ge_constraint} for clipped thresholds).›

definition clip_cost_constraint :: "nat ⇒ int ⇒ 'w pconstraint" where
  "clip_cost_constraint B l ≡ (k_gate_body B, clip B l)"

lemma clip_cost_constraint_sat:
  assumes rho01: "∀x. rho x = 0 ∨ rho x = 1"
  shows "satisfies (clip_cost_constraint B l) rho
       ⟷ bits_val (bits_needed B) CostBit rho ≥ clip B l"
  by (simp add: clip_cost_constraint_def k_gate_body_def satisfies_def
      pb_sum_bits_val)

end