Theory ProgramHyperproperties

section ‹Expressivity of Hyper Hoare Logic›

text ‹In this file, we define program hyperproperties (definition 8), and prove theorems 3 and 4.›

subsection ‹Program Hyperproperties›

theory ProgramHyperproperties
  imports Logic
begin

text ‹Definition 8›

type_synonym 'a hyperproperty = "('a × 'a) set ⇒ bool"
type_synonym ('pvar, 'pval) program_hyperproperty = "('pvar, 'pval) pstate hyperproperty"


definition set_of_traces where
  "set_of_traces C = { (σ, σ') |σ σ'. ⟨C, σ⟩ → σ' }"

definition hypersat :: "('pvar, 'pval) stmt ⇒ ('pvar, 'pval) program_hyperproperty ⇒ bool" where
  "hypersat C H ⟷ H (set_of_traces C)"

definition copy_p_state where
  "copy_p_state to_pvar to_lval σ x = to_lval (σ (to_pvar x))"

definition recover_p_state where
  "recover_p_state to_pval to_lvar l x = to_pval (l (to_lvar x))"

lemma injective_then_exists_inverse:
  assumes "injective to_lvar"
  shows "∃to_pvar. (∀x. to_pvar (to_lvar x) = x)"
proof -
  let ?to_pvar = "λy. SOME x. to_lvar x = y"
  have "⋀x. ?to_pvar (to_lvar x) = x"
    by (metis (mono_tags, lifting) assms injective_def someI)
  then show ?thesis
    by force
qed

lemma single_step_then_in_sem:
  assumes "single_sem C σ σ'"
      and "(l, σ) ∈ S"
    shows "(l, σ') ∈ sem C S"
  using assms(1) assms(2) in_sem by fastforce

lemma in_set_of_traces:
  "(σ, σ') ∈ set_of_traces C ⟷ ⟨C, σ⟩ → σ'"
  by (simp add: set_of_traces_def)


lemma in_set_of_traces_then_in_sem:
  assumes "(σ, σ') ∈ set_of_traces C"
      and "(l, σ) ∈ S"
    shows "(l, σ') ∈ sem C S"
  using in_set_of_traces assms single_step_then_in_sem by metis

lemma set_of_traces_same:
  assumes "⋀x. to_pvar (to_lvar x) = x"
      and "⋀x. to_pval (to_lval x) = x"
      and "S = {(copy_p_state to_pvar to_lval σ, σ) |σ. True}"
    shows "{(recover_p_state to_pval to_lvar l, σ') |l σ'. (l, σ') ∈ sem C S} = set_of_traces C"
(is "?A = ?B")
proof
  show "?A ⊆ ?B"
  proof (rule subsetPairI)
    fix σ σ' assume asm0: "(σ, σ') ∈ {(recover_p_state to_pval to_lvar l, σ') |l σ'. (l, σ') ∈ sem C S}"
    then obtain l where "σ = recover_p_state to_pval to_lvar l" "(l, σ') ∈ sem C S"
      by blast
    then obtain x where "(l, x) ∈ S" "⟨C, x⟩ → σ'"
      by (metis fst_conv in_sem snd_conv)
    then have "l = copy_p_state to_pvar to_lval x"
      using assms(3) by blast
    moreover have "σ = x"
    proof (rule ext)
      fix y show "σ y = x y"
        by (simp add: ‹σ = recover_p_state to_pval to_lvar l› assms(1) assms(2) calculation copy_p_state_def recover_p_state_def)
    qed
    ultimately show "(σ, σ') ∈ set_of_traces C"
      by (simp add: ‹⟨C, x⟩ → σ'› set_of_traces_def)
  qed
  show "?B ⊆ ?A"
  proof (rule subsetPairI)
    fix σ σ' assume asm0: "(σ, σ') ∈ set_of_traces C"
    let ?l = "copy_p_state to_pvar to_lval σ"
    have "(?l, σ) ∈ S"
      using assms(3) by blast
    then have "(?l, σ') ∈ sem C S"
      using asm0 in_set_of_traces_then_in_sem by blast
    moreover have "recover_p_state to_pval to_lvar ?l = σ"
    proof (rule ext)
      fix x show "recover_p_state to_pval to_lvar (copy_p_state to_pvar to_lval σ) x = σ x"
        by (simp add: assms(1) assms(2) copy_p_state_def recover_p_state_def)
    qed
    ultimately show "(σ, σ') ∈ {(recover_p_state to_pval to_lvar l, σ') |l σ'. (l, σ') ∈ sem C S}"
      by force
    qed
qed

text ‹Theorem 3›

theorem proving_hyperproperties:

  fixes to_lvar :: "'pvar ⇒ 'lvar"
  fixes to_lval :: "'pval ⇒ 'lval"

  assumes "injective to_lvar"
      and "injective to_lval"

    shows "∃P Q::('lvar, 'lval, 'pvar, 'pval) state hyperassertion. (∀C. hypersat C H ⟷ ⊨ {P} C {Q})"
proof -

  obtain to_pval :: "'lval ⇒ 'pval" where r1: "⋀x. to_pval (to_lval x) = x"
    using assms(2) injective_then_exists_inverse by blast

  obtain to_pvar :: "'lvar ⇒ 'pvar" where r2: "⋀x. to_pvar (to_lvar x) = x"
    using assms(1) injective_then_exists_inverse by blast

  let ?P = "λS. S = {(copy_p_state to_pvar to_lval σ, σ) |σ. True }"
  let ?Q = "λS. H { (recover_p_state to_pval to_lvar l, σ') |l σ'. (l, σ') ∈ S }"

  have "⋀C. hypersat C H ⟷ ⊨ {?P} C {?Q}"
  proof
    fix C
    assume "hypersat C H"
    show "⊨ {?P} C {?Q}"
    proof (rule hyper_hoare_tripleI)
      fix S assume "S = {(copy_p_state to_pvar to_lval σ, σ) |σ. True}"
      have "{(recover_p_state to_pval to_lvar l, σ') |l σ'. (l, σ') ∈ sem C S}
  = set_of_traces C"
        using ‹S = {(copy_p_state to_pvar to_lval σ, σ) |σ. True}› set_of_traces_same[of to_pvar to_lvar to_pval to_lval]
        r1 r2 by presburger
      then show "H {(recover_p_state to_pval to_lvar l, σ') |l σ'. (l, σ') ∈ sem C S}"
        using ‹hypersat C H› hypersat_def by metis
    qed
  next
    fix C
    let ?S = "{(copy_p_state to_pvar to_lval σ, σ) |σ. True }"
    assume "⊨ {?P} C {?Q}"
    then have "?Q (sem C ?S)"
      by (simp add: hyper_hoare_triple_def)
    moreover have "{(recover_p_state to_pval to_lvar l, σ') |l σ'. (l, σ') ∈ sem C ?S} = set_of_traces C"
      using r1 r2 set_of_traces_same[of to_pvar to_lvar to_pval to_lval]
      by presburger
    ultimately show "hypersat C H"
      by (simp add: hypersat_def)
  qed
  then show ?thesis 
    by auto
qed





text ‹Hypersafety, hyperliveness›

definition max_k where
  "max_k k S ⟷ finite S ∧ card S ≤ k"

definition hypersafety where
  "hypersafety P ⟷ (∀S. ¬ P S ⟶ (∀S'. S ⊆ S' ⟶ ¬ P S'))"

definition k_hypersafety where
  "k_hypersafety k P ⟷ (∀S. ¬ P S ⟶ (∃S'. S' ⊆ S ∧ max_k k S' ∧ (∀S''. S' ⊆ S'' ⟶ ¬ P S'')))"

definition hyperliveness where
  "hyperliveness P ⟷ (∀S. ∃S'. S ⊆ S' ∧ P S')"

lemma k_hypersafetyI:
  assumes "⋀S. ¬ P S ⟹ ∃S'. S' ⊆ S ∧ max_k k S' ∧ (∀S''. S' ⊆ S'' ⟶ ¬ P S'')"
  shows "k_hypersafety k P"
  by (simp add: assms k_hypersafety_def)


lemma hypersafetyI:
  assumes "⋀S S'. ¬ P S ⟹ S ⊆ S' ⟹ ¬ P S'"
  shows "hypersafety P"
  by (metis assms hypersafety_def)

lemma hyperlivenessI:
  assumes "⋀S. ∃S'. S ⊆ S' ∧ P S'"
  shows "hyperliveness P"
  using assms hyperliveness_def by blast

lemma k_hypersafe_is_hypersafe:
  assumes "k_hypersafety k P"
  shows "hypersafety P"
  by (metis (full_types) assms dual_order.trans hypersafety_def k_hypersafety_def)


lemma one_safety_equiv:
  assumes "sat H"
  shows "k_hypersafety 1 H ⟷ (∃P. ∀S. H S ⟷ (∀τ ∈ S. P τ))" (is "?A ⟷ ?B")
proof
  assume ?B
  then obtain P where asm0: "⋀S. H S ⟷ (∀τ ∈ S. P τ)"
    by auto
  show ?A
  proof (rule k_hypersafetyI)
    fix S
    assume asm1: "¬ H S"
    then obtain τ where "τ ∈ S" "¬ P τ"
      using asm0 by blast
    let ?S = "{τ}"
    have "?S ⊆ S ∧ max_k 1 ?S ∧ (∀S''. ?S ⊆ S'' ⟶ ¬ H S'')"
      using ‹¬ P τ› ‹τ ∈ S› asm0 max_k_def by fastforce
    then show "∃S'⊆S. max_k 1 S' ∧ (∀S''. S' ⊆ S'' ⟶ ¬ H S'')" by blast
  qed
next
  assume ?A
  let ?P = "λτ. H {τ}"
  have "⋀S. H S ⟷ (∀τ ∈ S. ?P τ)"
  proof
    fix S assume "H S"
    then show "∀τ ∈ S. ?P τ"
      using ‹k_hypersafety 1 H› hypersafety_def k_hypersafe_is_hypersafe by auto
  next
    fix S assume asm0: "∀τ ∈ S. ?P τ"
    show "H S"
    proof (rule ccontr)
      assume "¬ H S"
      then obtain S' where "S' ⊆ S ∧ max_k 1 S' ∧ (∀S''. S' ⊆ S'' ⟶ ¬ H S'')"
        by (metis ‹k_hypersafety 1 H› k_hypersafety_def)
      then show False
      proof (cases "S' = {}")
        case True
        then show ?thesis
          by (metis ‹S' ⊆ S ∧ max_k 1 S' ∧ (∀S''. S' ⊆ S'' ⟶ ¬ H S'')› assms empty_subsetI sat_def)
      next
        case False
        then obtain τ where "τ ∈ S'"
          by blast
        then have "card S' = 1"
          by (metis False One_nat_def Suc_leI ‹S' ⊆ S ∧ max_k 1 S' ∧ (∀S''. S' ⊆ S'' ⟶ ¬ H S'')› card_gt_0_iff le_antisym max_k_def)
        then have "S' = {τ}"
          using ‹τ ∈ S'› card_1_singletonE by auto
        then show ?thesis
          using ‹S' ⊆ S ∧ max_k 1 S' ∧ (∀S''. S' ⊆ S'' ⟶ ¬ H S'')› asm0 by fastforce
      qed
    qed
  qed
  then show ?B by blast
qed





definition hoarify where
  "hoarify P Q S ⟷ (∀p ∈ S. fst p ∈ P ⟶ snd p ∈ Q)"

lemma hoarify_hypersafety:
  "hypersafety (hoarify P Q)"
  by (metis (no_types, opaque_lifting) hoarify_def hypersafetyI subsetD)

theorem hypersafety_1_hoare_logic:
  "k_hypersafety 1 (hoarify P Q)"
proof (rule k_hypersafetyI)
  fix S assume "¬ hoarify P Q S"
  then obtain τ where "τ ∈ S" "fst τ ∈ P" "snd τ ∉ Q"      
    using hoarify_def by blast
  let ?S = "{τ}"
  have "?S ⊆ S ∧ max_k 1 ?S ∧ (∀S''. ?S ⊆ S'' ⟶ ¬ hoarify P Q S'')"
    by (metis Compl_iff One_nat_def ‹τ ∈ S› ‹fst τ ∈ P› ‹snd τ ∉ Q› card.empty card.insert compl_le_compl_iff empty_not_insert finite.intros(1) finite.intros(2) hoarify_def insert_absorb le_numeral_extra(4) max_k_def subset_Compl_singleton)
  then show "∃S'⊆S. max_k 1 S' ∧ (∀S''. S' ⊆ S'' ⟶ ¬ hoarify P Q S'')"
    by meson
qed

definition incorrectnessify where
  "incorrectnessify P Q S ⟷ (∀σ' ∈ Q. ∃σ ∈ P. (σ, σ') ∈ S)"

lemma incorrectnessify_liveness:
  assumes "P ≠ {}"
  shows "hyperliveness (incorrectnessify P Q)"
proof (rule hyperlivenessI)
  fix S
  obtain σ where asm0: "σ ∈ P"
    using assms by blast
  let ?S = "S ∪ {(σ, σ') |σ'. σ' ∈ Q}"
  have "incorrectnessify P Q ?S"
    using asm0 incorrectnessify_def by force
  then show "∃S'. S ⊆ S' ∧ incorrectnessify P Q S'"
    using sup.cobounded1 by blast
qed

definition real_incorrectnessify where
  "real_incorrectnessify P Q S ⟷ (∀σ ∈ P. ∃σ' ∈ Q. (σ, σ') ∈ S)"

lemma real_incorrectnessify_liveness:
  assumes "Q ≠ {}"
  shows "hyperliveness (real_incorrectnessify P Q)"
  by (metis UNIV_I assms equals0I hyperliveness_def real_incorrectnessify_def subsetI)











text ‹Verifying GNI›

definition gni_hyperassertion :: "'n ⇒ 'n ⇒ ('n ⇒ 'v) hyperassertion" where
  "gni_hyperassertion h l S ⟷ (∀σ ∈ S. ∀v. ∃σ' ∈ S. σ' h = v ∧ σ l = σ' l)"

definition semify where
  "semify Σ S = { (l, σ') |σ' σ l. (l, σ) ∈ S ∧ (σ, σ') ∈ Σ }"

definition hyperprop_hht where
  "hyperprop_hht P Q Σ ⟷ (∀S. P S ⟶ Q (semify Σ S))"

text ‹Theorem 4›
theorem any_hht_hyperprop:
  "⊨ {P} C {Q} ⟷ hypersat C (hyperprop_hht P Q)" (is "?A ⟷ ?B")
proof
  have "⋀S. semify (set_of_traces C) S = sem C S"
  proof -
    fix S
    have "⋀l σ'. (l, σ') ∈ sem C S ⟷ (l, σ') ∈ semify (set_of_traces C) S"
    proof -
      fix l σ'
      have "(l, σ') ∈ sem C S ⟷ (∃σ. (l, σ) ∈ S ∧ ⟨C, σ⟩ → σ')"
        by (simp add: in_sem)
      also have "... ⟷ (∃σ. (l, σ) ∈ S ∧ (σ, σ') ∈ set_of_traces C)"
        using set_of_traces_def by fastforce
      then show "(l, σ') ∈ sem C S ⟷ (l, σ') ∈ semify (set_of_traces C) S"
        by (simp add: calculation semify_def)
    qed
    then show "semify (set_of_traces C) S = sem C S"
      by auto
  qed
  show "?A ⟹ ?B"
    by (simp add: ‹⋀S. semify (set_of_traces C) S = sem C S› hyper_hoare_tripleE hyperprop_hht_def hypersat_def)
  show "?B ⟹ ?A"
    by (simp add: ‹⋀S. semify (set_of_traces C) S = sem C S› hyper_hoare_triple_def hyperprop_hht_def hypersat_def)
qed

end