Theory PaperResults

theory PaperResults
  imports Loops SyntacticAssertions Compositionality TotalLogic ExamplesCompositionality
begin

section ‹Summary of the Results from the Paper›

text ‹This file contains the formal results mentioned the paper. It is organized in the same order
and with the same structure as the paper.
▪ You can use the panel "Sidekick" on the right to see and navigate the structure of the file, via sections and subsections.
▪ You can ctrl+click on terms to jump to their definition.
▪ After jumping to another location, you can come back to the previous location by clicking the
  green left arrow, on the right side of the menu above.›



subsection ‹3: Hyper Hoare Logic›

subsubsection ‹3.1: Language and Semantics›

text ‹The programming language is defined in the file Language.thy:
▪ The type of program state (definition 1) is \<^typ>‹('pvar, 'pval) pstate›
  (<-- you can ctrl+click on the name ‹pstate› above to jump to its definition).
▪ Program commands (definition 1) are defined via the type \<^typ>‹('var, 'val) stmt›.
▪ The big-step semantics (figure 9) is defined as \<^const>‹single_sem›. We also use the notation \<^term>‹⟨C, σ⟩ → σ'›.›

subsubsection ‹3.2: Hyper-Triples, Formally›

text ‹
▪ Extended states (definition 2) are defined as \<^typ>‹('lvar, 'lval, 'pvar, 'pval) state› (file Language.thy).
▪ Hyper-assertions (definition 3) are defined as \<^typ>‹('lvar, 'lval, 'pvar, 'pval) state hyperassertion› (file Logic.thy).
▪ The extended semantics (definition 4) is defined as \<^const>‹sem›  (file Language.thy).
▪ Lemma 1 is shown and proven below.
▪ Hyper-triples (definition 5) are defined as \<^const>‹hyper_hoare_triple› (file Logic.thy).
  We also use the notation \<^term>‹⊨ {P} C {Q}›.›

lemma lemma1:
  "sem C (S1 ∪ S2) = sem C S1 ∪ sem C S2"
  "S ⊆ S' ⟹ sem C S ⊆ sem C S'"
  "sem C (⋃x. f x) = (⋃x. sem C (f x))"
  "sem Skip S = S"
  "sem (C1;; C2) S = sem C2 (sem C1 S)"
  "sem (If C1 C2) S = sem C1 S ∪ sem C2 S"
  "sem (While C) S = (⋃n. iterate_sem n C S)"
  using sem_if sem_seq sem_union sem_skip sem_union_general sem_monotonic sem_while by metis+

subsubsection ‹3.3: Core Rules›

text ‹The core rules (from figure 2) are defined in the file Logic.thy as \<^const>‹syntactic_HHT›.
We also use the notation \<^term>‹⊢ {P} C {Q}›. Operators ‹⊗› (definition 6) and ‹⨂› (definition 7)
are defined as \<^const>‹join› and \<^const>‹natural_partition›, respectively.›

subsubsection ‹3.4: Soundness and Completeness›

text ‹Theorem 1: Soundness›
theorem thm1_soundness:
  assumes "⊢ {P} C {Q}"
  shows "⊨ {P} C {Q}"
  using assms soundness by auto

text ‹Theorem 2: Completeness›
theorem thm2_completeness:
  assumes "⊨ {P} C {Q}"
  shows "⊢ {P} C {Q}"
  using assms completeness by auto

subsubsection ‹3.5: Expressivity of Hyper-Triples›

text ‹Program hyperproperties (definition 8) are defined in the file ProgramHyperproperties as
the type \<^typ>‹('pvar, 'pval) program_hyperproperty›, which is syntactic sugar for the type
\<^typ>‹(('pvar, 'pval) pstate × ('pvar, 'pval) pstate) set ⇒ bool›. As written in the paper (after the definition),
this type is equivalent to the type \<^typ>‹((('pvar, 'pval) pstate × ('pvar, 'pval) pstate) set) set›.
The satisfiability of program hyperproperties is defined via the function \<^const>‹hypersat›.›

text ‹Theorem 3: Expressing hyperproperties as hyper-triples›
theorem thm3_expressing_hyperproperties_as_hyper_triples:
  fixes to_lvar :: "'pvar ⇒ 'lvar"
  fixes to_lval :: "'pval ⇒ 'lval"
  fixes H :: "('pvar, 'pval) program_hyperproperty"
  assumes "injective to_lvar" ―‹The cardinality of \<^typ>‹'lvar› is at least the cardinality of \<^typ>‹'pvar›.›
      and "injective to_lval" ―‹The cardinality of \<^typ>‹'lval› is at least the cardinality of \<^typ>‹'pval›.›
    shows "∃P Q::('lvar, 'lval, 'pvar, 'pval) state hyperassertion. (∀C. hypersat C H ⟷ ⊨ {P} C {Q})"
  using assms proving_hyperproperties
  by blast

text ‹Theorem 4: Expressing hyper-triples as hyperproperties›
theorem thm4_expressing_hyper_triples_as_hyperproperties:
  "⊨ {P} C {Q} ⟷ hypersat C (hyperprop_hht P Q)"
  by (simp add: any_hht_hyperprop)

text ‹Theorem 5: Disproving hyper-triples›
theorem thm5_disproving_triples:
  "¬ ⊨ {P} C {Q} ⟷ (∃P'. sat P' ∧ entails P' P ∧ ⊨ {P'} C {λS. ¬ Q S})"
  using disproving_triple by auto




subsection ‹4: Syntactic Rules›

subsubsection ‹4.1: Syntactic Hyper-Assertions›

text ‹Syntactic hyper-expressions and hyper-assertions (definition 9) are defined in the file
SyntacticAssertions.thy as \<^typ>‹'val exp› and \<^typ>‹'val assertion› respectively, where 'val is the
type of both logical and program values. Note that we use de Bruijn indices (i.e, natural numbers)
for states and variables bound by quantifiers.›

subsubsection ‹4.2: Syntactic Rules for Deterministic and Non-Deterministic Assignments.›

text ‹We prove semantic versions of the syntactic rules from subsection 4 (figure 3).
We use \<^const>‹interp_assert› to convert a syntactic hyper-assertion into a semantic one, because
our hyper-triples require semantic hyper-assertions. Similarly, we use \<^const>‹interp_pexp› to convert
a syntactic program expression into a semantic one.
\<^term>‹transform_assign x e P› and \<^term>‹transform_havoc x P› correspond to ‹A⇧e⇩x› and ‹H⇩x› from definition 10.›

text ‹Rule AssignS from figure 3›
proposition AssignS:
  "⊢ { interp_assert (transform_assign x e P) } Assign x (interp_pexp e) {interp_assert P}"
  using completeness rule_assign_syntactic by blast

text ‹Rule HavocS from figure 3›
proposition HavocS:
  "⊢ { interp_assert (transform_havoc x P) } Havoc x {interp_assert P}"
  using completeness rule_havoc_syntactic by blast

subsubsection ‹4.3: Syntactic Rules for Assume Statements›

text ‹\<^const>‹transform_assume› corresponds to ‹Π⇩b› (definition 11).›

text ‹Rule AssumeS from figure 3›
proposition AssumeS:
  "⊢ { interp_assert (transform_assume (pbexp_to_assertion 0 b) P) } Assume (interp_pbexp b) {interp_assert P}"
  using completeness rule_assume_syntactic by blast

text ‹As before, we use \<^const>‹interp_pbexp› to convert the syntactic program Boolean expression b into
a semantic one. Similarly, \<^term>‹pbexp_to_assertion 0 b› converts the syntactic program Boolean expression
p into a syntactic hyper-assertion. The number 0 is a de Bruijn index, which corresponds to the closest
quantified state. For example, the hyper-assertion ‹∀<φ>. φ(a)=φ(b) ∧ (∃<φ'>. φ(x) ≽ φ'(y))› would
be written as ‹∀. 0(a)=0(b) ∧ (∃. 1(x) ≽ 0(y))› with de Bruijn indices. Thus, one can think of
‹pbexp_to_assertion 0 b› as ‹b(φ)›, where ‹φ› is simply the innermost quantified state.›




subsection ‹5: Proof Principles for Loops›

text ‹We show in the following our proof rules for loops, presented in figure 5.›

text ‹Rule WhileDesugared from figure 5›
theorem while_desugared:
  assumes "⋀n. ⊢ {I n} Assume b;; C {I (Suc n)}"
      and "⊢ { natural_partition I } Assume (lnot b) { Q }"
    shows "⊢ {I 0} while_cond b C { Q }"
  by (metis completeness soundness assms(1) assms(2) seq_rule while_cond_def while_rule)

text ‹This result uses the following constructs:
▪ \<^term>‹natural_partition I› corresponds to the ‹⨂› operator from definition 7.
▪ \<^term>‹lnot b› negates b.
▪ \<^term>‹while_cond b C› is defined as \<^term>‹While (Assume b;; C);; Assume (lnot b)›.›

text ‹Rule WhileSync from figure 5 (presented in subsubsection 5.1)›
lemma WhileSync:
  assumes "entails I (low_exp b)"
      and "⊢ {conj I (holds_forall b)} C {I}"
    shows "⊢ {conj I (low_exp b)} while_cond b C {conj (disj I emp) (holds_forall (lnot b))}"
  using WhileSync_simpler entail_conj completeness soundness assms(1) assms(2) entails_refl 
  consequence_rule[of "conj I (holds_forall b)" "conj I (holds_forall b)" I "conj I (low_exp b)"] by blast

text ‹This result uses the following constructs:
▪ \<^term>‹conj A B› corresponds to the hyper-assertion ‹A ∧ B›.
▪ \<^term>‹holds_forall b› corresponds to ‹box(b)›.
▪ \<^term>‹low_exp b› corresponds to ‹low(b)›.
▪ \<^term>‹disj A B› corresponds to the hyper-assertion ‹A ∨ B›.
▪ \<^term>‹emp› checks whether the set of states is empty.›

text ‹Rule IfSync from figure 5 (presented in subsubsection 5.1)›
theorem IfSync:
  assumes "entails P (low_exp b)"
      and "⊢ {conj P (holds_forall b)} C1 {Q}"
      and "⊢ {conj P (holds_forall (lnot b))} C2 {Q}"
    shows "⊢ {P} if_then_else b C1 C2 {Q}"
  using completeness soundness consequence_rule[of _ "conj P (low_exp b)" Q] assms(1) entail_conj entails_refl assms if_synchronized by metis

text ‹This result uses the following construct:
▪ \<^term>‹if_then_else b C1 C2› is syntactic sugar for \<^term>‹If (Assume b;; C1) (Assume (lnot b);; C2)›.›

text ‹Rule ‹While-∀*∃*› from figure 5 (presented in subsubsection 5.2)›
theorem while_forall_exists:
  assumes "⊢ {I} if_then b C {I}"
      and "⊢ {I} Assume (lnot b) {interp_assert Q}"
      and "no_forall_state_after_existential Q"
    shows "⊢ {I} while_cond b C {interp_assert Q}"
  using consequence_rule[of I I "conj (interp_assert Q) (holds_forall (lnot b))" "interp_assert Q"]
  using completeness soundness while_forall_exists_simpler assms entail_conj_weaken entails_refl by metis

text ‹This result uses the following constructs:
▪ \<^term>‹if_then b C› is syntactic sugar for \<^term>‹If (Assume b;; C) (Assume (lnot b))›.
▪ \<^term>‹no_forall_state_after_existential Q› holds iff there is no universal state quantifier ‹∀⟨_⟩› after any ‹∃› in Q.›

text ‹Rule ‹While-∃› from figure 5 (presented in subsubsection 5.3)›
theorem while_loop_exists:
  assumes  "⋀v. ⊢ { (λS. ∃φ∈S. e (snd φ) = v ∧ b (snd φ) ∧ P φ S) } if_then b C { (λS. ∃φ∈S. lt (e (snd φ)) v ∧ P φ S) }"
      and "⋀φ. ⊢ { P φ } while_cond b C { Q φ }"
      and "wfP lt"
    shows "⊢ { (λS. ∃φ∈S. P φ S) } while_cond b C { (λS. ∃φ∈S. Q φ S)}"
  using completeness soundness exists_terminates_loop assms by blast

text ‹\<^term>‹wfP lt› in this result ensures that the binary operator ‹lt› is well-founded.
‹e› is a function of a program state, which must decrease after each iteration.›




subsection ‹Appendix A: Technical Definitions Omitted from the Paper›

text ‹The big-step semantics (figure 9) is defined as \<^const>‹single_sem›. We also use the notation \<^term>‹⟨C, σ⟩ → σ'›.
The following definitions are formalized in the file SyntacticAssertions.thy:
▪ Evaluation of hyper-expressions (definition 12): \<^const>‹interp_exp›.
▪ Satisfiability of hyper-assertions (definition 12): \<^const>‹sat_assertion›.
▪ Syntactic transformation for deterministic assignments (definition 13): \<^const>‹transform_assign›.
▪ Syntactic transformation for non-deterministic assignments (definition 14): \<^const>‹transform_havoc›.
▪ Syntactic transformation for assume statements. (definition 15): \<^const>‹transform_assume›.›



subsection ‹Appendix C: Expressing Judgments of Hoare Logics as Hyper-Triples›

subsubsection ‹Appendix C.1: Overapproximate Hoare Logics›

text ‹The following judgments are defined in the file Expressivity.thy as follows:
▪ Definition 16 (Hoare Logic): \<^term>‹HL P C Q›.
▪ Definition 17 (Cartesian Hoare Logic): \<^term>‹CHL P C Q›.›

text ‹Proposition 1: HL triples express hyperproperties›
proposition prop_1_HL_expresses_hyperproperties:
  "∃H. (∀C. hypersat C H ⟷ HL P C Q)"
  using HL_expresses_hyperproperties by blast

text ‹Proposition 2: Expressing HL in Hyper Hoare Logic›
proposition prop_2_expressing_HL_in_HHL:
  "HL P C Q ⟷ (hyper_hoare_triple (over_approx P) C (over_approx Q))"
  using encoding_HL by auto

text ‹Proposition 3: CHL triples express hyperproperties›
proposition prop_3_CHL_is_hyperproperty:
  "hypersat C (CHL_hyperprop P Q) ⟷ CHL P C Q"
  using CHL_hyperproperty by fast

text ‹Proposition 4: Expressing CHL in Hyper Hoare Logic›
proposition prop_4_encoding_CHL_in_HHL:
  assumes "not_free_var_of P x"
      and "not_free_var_of Q x"
      and "injective from_nat"
    shows "CHL P C Q ⟷ ⊨ {encode_CHL from_nat x P} C {encode_CHL from_nat x Q}"
  using encoding_CHL assms by fast

text ‹The function ‹from_nat› gives us a way to encode numbers from 1 to k as logical values.
Moreover, note that we represent k-tuples implicitly, as mappings of type \<^typ>‹'a ⇒ 'b›: When the type
‹'a› has k elements, a function of type \<^typ>‹'a ⇒ 'b› corresponds to a k-tuple of elements of type 'b.
This representation is more convenient to work with, and more general, since it also captures infinite sequences.›

subsubsection ‹Appendix C.2: Underapproximate Hoare Logics›

text ‹The following judgments are defined in the file Expressivity.thy as follows:
▪ Definition 18 (Incorrectness Logic): \<^term>‹IL P C Q›.
▪ Definition 19 (k-Incorrectness Logic): \<^term>‹RIL P C Q›.
▪ Definition 20 (Forward Underapproximation): \<^term>‹FU P C Q›.
▪ Definition 21 (k-Forward Underapproximation): \<^term>‹RFU P C Q›.›

text ‹RIL is the old name of k-IL, and RFU is the old name of k-FU.›

text ‹Proposition 5: IL triples express hyperproperties›
proposition prop_5_IL_hyperproperties:
  "IL P C Q ⟷ IL_hyperprop P Q (set_of_traces C)"
  using IL_expresses_hyperproperties by fast

text ‹Proposition 6: Expressing IL in Hyper Hoare Logic›
proposition prop_6_expressing_IL_in_HHL:
  "IL P C Q ⟷ (hyper_hoare_triple (under_approx P) C (under_approx Q))"
  using encoding_IL by fast

text ‹Proposition 7: k-IL triples express hyperproperties›
proposition prop_7_kIL_hyperproperties:
  "hypersat C (RIL_hyperprop P Q) ⟷ RIL P C Q"
  using RIL_expresses_hyperproperties by fast

text ‹Proposition 8: Expressing k-IL in Hyper Hoare Logic›
proposition prop_8_expressing_kIL_in_HHL:
  fixes x :: "'lvar"
  assumes "⋀l l' σ. (λi. (l i, σ i)) ∈ P ⟷ (λi. (l' i, σ i)) ∈ P"  (* P does not depend on logical variables *)
      and "injective (indexify :: (('a ⇒ ('pvar ⇒ 'pval)) ⇒ 'lval))" (* |lval| ≥ |PStates^k| *)
      and "c ≠ x"
      and "injective from_nat"
      and "not_free_var_of (P :: ('a ⇒ ('lvar ⇒ 'lval) × ('pvar ⇒ 'pval)) set) x ∧ not_free_var_of P c"
      and "not_free_var_of Q x ∧ not_free_var_of Q c"
    shows "RIL P C Q ⟷ ⊨ {pre_insec from_nat x c P} C {post_insec from_nat x c Q}"
  using assms(1) assms(2) assms(3) assms(4) assms(5) assms(6) by (rule encoding_RIL)

proposition FU_hyperproperties:
  "hypersat C (hyperprop_FU P Q) ⟷ FU P C Q"
  by (rule FU_expresses_hyperproperties)

text ‹Proposition 9: Expressing FU in Hyper Hoare Logic›
proposition prop_9_expressing_FU_in_HHL:
  "FU P C Q ⟷ ⊨ {encode_FU P} C {encode_FU Q}"
  by (rule encoding_FU)

text ‹Proposition 10: k-FU triples express hyperproperties›
proposition prop_10_kFU_expresses_hyperproperties:
  "hypersat C (RFU_hyperprop P Q) ⟷ RFU P C Q"
  by (rule RFU_captures_hyperproperties)

text ‹Proposition 11: Expressing k-FU in Hyper Hoare Logic›
proposition prop_11_encode_kFU_in_HHL:
  assumes "not_free_var_of P x"
      and "not_free_var_of Q x"
      and "injective from_nat"
    shows "RFU P C Q ⟷ ⊨ {encode_RFU from_nat x P} C {encode_RFU from_nat x Q}"
  using assms
  by (rule encode_RFU)

subsubsection ‹Appendix C.3: Beyond Over- and Underapproximation›

text ‹The following judgment is defined in the file Expressivity.thy as follows:
▪ Definition 22 (k-Universal Existential): \<^term>‹RUE P C Q›.
Note that RUE is the old name of k-UE.›

text ‹Proposition 12: k-UE triples express hyperproperties›
proposition prop_12_kUE_expresses_hyperproperty:
  "RUE P C Q ⟷ hypersat C (hyperprop_RUE P Q)"
  by (rule RUE_express_hyperproperties)

text ‹Proposition 13: Expressing k-UE in Hyper Hoare Logic›
proposition prop_13_expressing_kUE_in_HHL:
  assumes "injective fn ∧ injective fn1 ∧ injective fn2"
      and "t ≠ x"
      and "injective (fn :: nat ⇒ 'a)"
      and "injective fn1"
      and "injective fn2"
      and "not_in_free_vars_double {x, t} P"
      and "not_in_free_vars_double {x, t} Q"
  shows "RUE P C Q ⟷ ⊨ {encode_RUE_1 fn fn1 fn2 x t P} C {encode_RUE_2 fn fn1 fn2 x t Q}"
  using assms by (rule encoding_RUE)


text ‹Example 3›
proposition proving_refinement:
  fixes P :: "(('lvar ⇒ 'lval) × ('pvar ⇒ 'pval)) set ⇒ bool"
    and t :: 'pvar
  assumes "(one :: 'pval) ≠ two" ―‹We assume two distinct program values ‹one› and ‹two›, to represent 1 and 2.›
      and "P = (λS. card S = 1)"
      and "Q = (λS. ∀φ∈S. snd φ t = two ⟶ (fst φ, (snd φ)(t := one)) ∈ S)"
      and "not_free_var_stmt t C1"
      and "not_free_var_stmt t C2"
  shows "refinement C2 C1 ⟷
  ⊨ { P } If (Seq (Assign t (λ_. one)) C1) (Seq (Assign t (λ_. two)) C2) { Q }"
proof -
  have "refinement C2 C1 ⟷ ⊨ { P } If (Seq (Assign t (λ_. two)) C2) (Seq (Assign t (λ_. one)) C1) { Q }"
    using encoding_refinement[of two one P Q t C2 C1] assms by blast
  then show ?thesis using rewrite_if_commute by blast
qed




subsection ‹Appendix D: Compositionality›

subsubsection ‹Appendix D.1: Compositionality Rules›

text ‹In the following, we show the rules from figure 11, in the order in which they appear.›

proposition rule_Linking:
  assumes "⋀φ1 (φ2 :: ('a, 'b, 'c, 'd) state). fst φ1 = fst φ2 ∧ ( ⊢ { (in_set φ1 :: (('a, 'b, 'c, 'd) state) hyperassertion) } C { in_set φ2 } )
  ⟹ ( ⊢ { (P φ1 :: (('a, 'b, 'c, 'd) state) hyperassertion) } C { Q φ2 } )"
  shows "⊢ { ((λS. ∀φ1 ∈ S. P φ1 S) :: (('a, 'b, 'c, 'd) state) hyperassertion) } C { (λS. ∀φ2 ∈ S. Q φ2 S) }"
  using assms soundness completeness rule_linking by blast

proposition rule_And:
  assumes "⊢ {P} C {Q}"
      and "⊢ {P'} C {Q'}"
    shows "⊢ {conj P P'} C {conj Q Q'}"
  using assms soundness completeness rule_And by metis

proposition rule_Or:
  assumes "⊢ {P} C {Q}"
      and "⊢ {P'} C {Q'}"
    shows "⊢ {disj P P'} C {disj Q Q'}"
  using assms soundness completeness rule_Or by metis

proposition rule_FrameSafe:
  assumes "wr C ∩ fv F = {}"
      and "wf_assertion F"
      and "no_exists_state F"
    shows "⊢ {interp_assert F} C {interp_assert F}"
  using safe_frame_rule_syntactic assms completeness by metis

proposition rule_Forall:
  assumes "⋀x. ⊢ {P x} C {Q x}"
  shows "⊢ {forall P} C {forall Q}"
  using assms soundness completeness rule_Forall by metis

proposition rule_IndexedUnion:
  assumes "⋀x. ⊢ {P x} C {Q x}"
  shows "⊢ {general_join P} C {general_join Q}"
  using assms soundness completeness rule_IndexedUnion by metis

proposition rule_Union:
  assumes "⊢ {P} C {Q}"
      and "⊢ {P'} C {Q'}"
    shows "⊢ {join P P'} C {join Q Q'}"
  using assms soundness completeness rule_Union by metis

proposition rule_BigUnion:
  fixes P :: "((('a ⇒ 'b) × ('c ⇒ 'd)) set ⇒ bool)"
  assumes "⊢  {P} C {Q}"
  shows "⊢ {general_union P} C {general_union Q}"
  using assms soundness completeness rule_BigUnion by blast

proposition rule_Specialize:
  assumes "⊢ {interp_assert P} C {interp_assert Q}"
      and "indep_of_set b"
      and "wf_assertion_aux 0 1 b"
      and "wr C ∩ fv b = {}"
    shows "⊢ { interp_assert (transform_assume b P) } C { interp_assert (transform_assume b Q) }"
  using filter_rule_syntactic assms soundness completeness by blast

text ‹In the following, \<^term>‹entails_with_updates vars P P'› and \<^term>‹invariant_on_updates vars Q›
respectively correspond to the notions of entailments modulo logical variables and invariance with
respect to logical updates, as described in definition 23.›

proposition rule_LUpdate:
  assumes "⊢ {P'} C {Q}"
      and "entails_with_updates vars P P'"
      and "invariant_on_updates vars Q"
    shows "⊢ {P} C {Q}"
  using assms soundness completeness rule_LUpdate by blast

proposition rule_LUpdateSyntactic:
  assumes "⊢ { (λS. P S ∧ e_recorded_in_t e t S) } C { Q }"
      and "not_fv_hyper t P"
      and "not_fv_hyper t Q"
    shows "⊢ { P } C { Q }"
  using LUpdateS soundness completeness assms by fast

proposition rule_AtMost:
  assumes "⊢ {P} C {Q}"
  shows "⊢ {has_superset P} C {has_superset Q}"
  using assms soundness completeness rule_AtMost by blast

(* derived from join *)
proposition rule_AtLeast:
  assumes "⊢ {P} C {Q}"
  shows "⊢ {has_subset P} C {has_subset Q}"
  using assms soundness completeness rule_AtLeast by blast

proposition rule_True:
  "⊢ {P} C {λ_. True}"
  using rule_True completeness by blast

proposition rule_False:
  "⊢ { (λ_. False) } C {Q}"
  using rule_False completeness by blast

proposition rule_Empty:
  "⊢ { (λS. S = {}) } C { (λS. S = {}) }"
  using completeness rule_Empty by blast


subsubsection ‹Appendix D.2: Examples›

text ‹Example shown in figure 12. To see the actual proof, ctrl+click on @{thm composing_monotonicity_and_minimum}.›
proposition fig_12_composing_monotonicity_and_minimum:
  fixes P :: "((('a ⇒ 'b) × ('c ⇒ 'd)) set ⇒ bool)"
  fixes i :: 'a
  fixes x y :: 'c
  fixes leq :: "'d ⇒ 'd ⇒ bool"
  fixes one two :: 'b
  assumes "⊢ { P } C1 { has_minimum x leq }"
      and "⊢ { is_monotonic i x one two leq } C2 { is_monotonic i y one two leq }"
      and "⊢ { (is_singleton :: ((('a ⇒ 'b) × ('c ⇒ 'd)) set ⇒ bool)) } C2 { is_singleton }"
      and "one ≠ two" ―‹We use distinct logical values ‹one› and ‹two› to represent 1 and 2.›
      and "⋀x. leq x x" ―‹We assume that ‹leq› is a partial order, and thus that it satisfies reflexivity.›
    shows "⊢ { P } C1 ;; C2 { has_minimum y leq }"
  using assms soundness completeness composing_monotonicity_and_minimum by metis

text ‹Example shown in figure 13. To see the actual proof, ctrl+click on @{thm composing_GNI_with_SNI}.›
proposition fig_13_composing_GNI_with_SNI:
  fixes h :: 'lvar
  fixes l :: 'pvar
  assumes "⊢ { (low l :: (('lvar, 'lval, 'pvar, 'pval) state) hyperassertion) } C2 { low l }"
      and "⊢ { (not_empty :: (('lvar, 'lval, 'pvar, 'pval) state) hyperassertion) } C2 { not_empty }"
      and "⊢ { (low l :: (('lvar, 'lval, 'pvar, 'pval) state) hyperassertion) } C1 { lGNI l h }"
    shows "⊢ { (low l :: (('lvar, 'lval, 'pvar, 'pval) state) hyperassertion) } C1;; C2 { lGNI l h }"
  using assms soundness completeness composing_GNI_with_SNI by metis





subsection ‹Appendix E: Termination-Based Reasoning›

text ‹Terminating hyper-triples (definition 24) are defined as \<^const>‹total_hyper_triple›, and usually
written \<^term>‹⊨TERM {P} C {Q}›.›

theorem rule_Frame:
  assumes "⊨TERM {P} C {Q}"
      and "wr C ∩ fv F = {}"
      and "wf_assertion F"
    shows "⊨TERM {conj P (interp_assert F)} C {conj Q (interp_assert F)}"
  by (simp add: assms(1) assms(2) assms(3) frame_rule_syntactic)

theorem rule_WhileSyncTerm:
  assumes "⊨TERM {conj I (λS. ∀φ∈S. b (snd φ) ∧ fst φ t = e (snd φ))} C {conj (conj I (low_exp b)) (e_smaller_than_t e t lt)}"
      and "wfP lt"
      and "not_fv_hyper t I"
    shows "⊨TERM {conj I (low_exp b)} while_cond b C {conj I (holds_forall (lnot b))}"
  by (meson WhileSyncTot assms(1) assms(2) assms(3))




subsection ‹Appendix H: Synchronous Reasoning over Different Branches›

text ‹Proposition 14: Synchronous if rule›
proposition prop_14_synchronized_if_rule:
  assumes "⊨ {P} C1 {P1}"
      and "⊨ {P} C2 {P2}"
      and "⊨ {combine from_nat x P1 P2} C {combine from_nat x R1 R2}"
      and "⊨ {R1} C1' {Q1}"
      and "⊨ {R2} C2' {Q2}"
      and "not_free_var_hyper x P1"
      and "not_free_var_hyper x P2"
      and "from_nat 1 ≠ from_nat 2" ―‹We can represent 1 and 2 as distinct logical values.›
      and "not_free_var_hyper x R1"
      and "not_free_var_hyper x R2"
    shows "⊨ {P} If (Seq C1 (Seq C C1')) (Seq C2 (Seq C C2')) {join Q1 Q2}"
  using if_sync_rule assms by meson



end