Theory RelationalIncorrectness

theory RelationalIncorrectness
  imports "HOL-IMP.Big_Step"
begin

(* Author: Toby Murray *)

section "Under-Approximate Relational Judgement"

text ‹
  This is the relational analogue of OHearn's~cite"OHearn_19" and de Vries \& Koutavas'~cite"deVries_Koutavas_11"
  judgements.

  Note that in our case it doesn't really make sense to talk about ``erroneous'' states: the
  presence of an error can be seen only by the violation of a relation. Unlike O'Hearn, we cannot
  encode it directly into the semantics of our programs, without giving them a relational semantics.
  We use the standard big step semantics of IMP unchanged.
›

type_synonym rassn = "state  state  bool"

definition 
  ir_valid :: "rassn  com  com  rassn  bool"
  where
  "ir_valid P c c' Q  ( t t'. Q t t'  (s s'. P s s'  (c,s)  t  (c',s')  t'))"


section "Rules of the Logic"

definition
  flip :: "rassn  rassn"
  where
  "flip P  λs s'. P s' s"


inductive
  ir_hoare :: "rassn  com  com  rassn  bool"
  where
  ir_Skip: "(t t'. Q t t'  s'. P t s'  (c',s')  t') 
            ir_hoare P SKIP c' Q" |
  ir_If_True:   "ir_hoare (λs s'. P s s'  bval b s) c1 c' Q  
                 ir_hoare P (IF b THEN c1 ELSE c2) c' Q" |
  ir_If_False:   "ir_hoare (λs s'. P s s'  ¬ bval b s) c2 c' Q  
                  ir_hoare P (IF b THEN c1 ELSE c2) c' Q" |
  ir_Seq1: "ir_hoare P c c' Q  ir_hoare Q d SKIP R  ir_hoare P (Seq c d) c' R" |
  ir_Assign: "ir_hoare (λt t'.  v. P (t(x := v)) t'  (t x) = aval e (t(x := v))) SKIP c' Q 
              ir_hoare P (Assign x e) c' Q" |
  ir_While_False: "ir_hoare (λs s'. P s s'  ¬ bval b s) SKIP c' Q 
                  ir_hoare P (WHILE b DO c) c' Q" |
  ir_While_True: "ir_hoare (λs s'. P s s'  bval b s) (c;; WHILE b DO c) c' Q 
                  ir_hoare P (WHILE b DO c) c' Q" |
  ir_While_backwards_frontier: "(n. ir_hoare (λ s s'. P n s s'  bval b s) c SKIP (P (Suc n))) 
                                ir_hoare (λs s'. n. P n s s') (WHILE b DO c) c' Q 
                                ir_hoare (P 0) (WHILE b DO c) c' Q" |
  ir_conseq:      "ir_hoare P c c' Q  (s s'. P s s'  P' s s')  (s s'. Q' s s'  Q s s') 
                   ir_hoare P' c c' Q'" |
  ir_disj:        "ir_hoare P1 c c' Q1  ir_hoare P2 c c' Q2 
                   ir_hoare (λs s'. P1 s s'  P2 s s') c c' (λ t t'. Q1 t t'  Q2 t t')" |
  ir_sym: "ir_hoare (flip P) c c' (flip Q)  ir_hoare P c' c Q"

section "Simple Derived Rules"

lemma meh_simp[simp]: "(SKIP, s')  t' = (s' = t')"
  by auto


lemma ir_pre: "ir_hoare P c c' Q  (s s'. P s s'  P' s s')  
                  ir_hoare P' c c' Q"
  by(erule ir_conseq, blast+)

lemma ir_post: "ir_hoare P c c' Q  (s s'. Q' s s'  Q s s')  
                  ir_hoare P c c' Q'"
  by(erule ir_conseq, blast+)

section "Soundness"

lemma Skip_ir_valid[intro]:
  "(t t'. Q t t'  s'. P t s'  (c', s')  t')  ir_valid P SKIP c' Q"
  by(auto simp: ir_valid_def)

lemma sym_ir_valid[intro]:
  "ir_valid (flip P) c' c (flip Q)  ir_valid P c c' Q"
  by(fastforce simp: ir_valid_def flip_def)

lemma If_True_ir_valid[intro]:
  "ir_valid (λa c. P a c  bval b a) c1 c' Q 
   ir_valid P (IF b THEN c1 ELSE c2) c' Q"
  by(fastforce simp: ir_valid_def)

lemma If_False_ir_valid[intro]:
  "ir_valid (λa c. P a c  ¬ bval b a) c2 c' Q 
   ir_valid P (IF b THEN c1 ELSE c2) c' Q"
  by(fastforce simp: ir_valid_def)

lemma Seq1_ir_valid[intro]:
  "ir_valid P c c' Q  ir_valid Q d SKIP R  ir_valid P (c;; d) c' R"
  by(fastforce simp: ir_valid_def)

lemma Seq2_ir_valid[intro]:
  "ir_valid P c SKIP Q  ir_valid Q d c' R  ir_valid P (c;; d) c' R"
  by(fastforce simp: ir_valid_def)

lemma Seq_ir_valid[intro]:
  "ir_valid P c c' Q  ir_valid Q d d' R  ir_valid P (c;; d) (c';; d') R"
  by(fastforce simp: ir_valid_def)

lemma Assign_blah[intro]:
  "t x = aval e (t(x := v))
        (x ::= e, t(x := v))  t"
  using Assign 
  by (metis fun_upd_triv fun_upd_upd)

lemma Assign_ir_valid[intro]:
  "ir_valid (λt t'.  v. P (t(x := v)) t'  (t x) = aval e (t(x := v))) SKIP c' Q  ir_valid P (Assign x e) c' Q"
  by(fastforce simp: ir_valid_def)

lemma While_False_ir_valid[intro]:
  "ir_valid (λs s'. P s s'  ¬ bval b s) SKIP c' Q 
   ir_valid P (WHILE b DO c) c' Q"
  by(fastforce simp: ir_valid_def)

lemma While_True_ir_valid[intro]:
  "ir_valid (λs s'. P s s'  bval b s) (Seq c (WHILE b DO c)) c' Q 
   ir_valid P (WHILE b DO c) c' Q"
  by(clarsimp simp: ir_valid_def, blast)


lemma While_backwards_frontier_ir_valid':
  assumes asm: "n. t t'. P (k + Suc n) t t' 
                    (s. P (k + n) s t'  bval b s  (c, s)  t)"
  assumes last: "t t'. Q t t'  (s s'. (n. P (k + n) s s')  (WHILE b DO c, s)  t  (c', s')  t')"
  assumes post: "Q t t'"
  shows "s s'. P k s s'  (WHILE b DO c, s)  t  (c', s')  t'"
proof -
  from post last obtain s s' n where 
    "P (k + n) s s'" "(WHILE b DO c, s)  t" "(c', s')  t'"
    by blast
  with asm  show ?thesis
  proof(induction n arbitrary: k t t')
    case 0 
    then show ?case 
      by (metis WhileFalse WhileTrue add.right_neutral)
  next
    case (Suc n)
    from Suc
    obtain r r' where final_iteration: "P (Suc k) r r'" "(WHILE b DO c, r)  t" "(c', r')  t'"
      by (metis add_Suc_shift)
    from final_iteration(1) obtain q q' where
     "P k q r'  bval b q   (c, q)  r" 
      by (metis Nat.add_0_right Suc.prems(1) plus_1_eq_Suc semiring_normalization_rules(24))
    with final_iteration show ?case by blast
  qed
qed


lemma While_backwards_frontier_ir_valid[intro]:
  "(n. ir_valid (λ s s'. P n s s'  bval b s) c SKIP (P (Suc n))) 
   ir_valid (λs s'. n. P n s s') (WHILE b DO c) c' Q 
   ir_valid (P 0) (WHILE b DO c) c' Q"
  by(auto simp: meh_simp ir_valid_def intro: While_backwards_frontier_ir_valid')

lemma conseq_ir_valid:
  "ir_valid P c c' Q  (s s'. P s s'  P' s s')  (s s'. Q' s s'  Q s s') 
                  ir_valid P' c c' Q'"
  by(clarsimp simp: ir_valid_def, blast)

lemma disj_ir_valid[intro]:
  "ir_valid P1 c c' Q1  ir_valid P2 c c' Q2 
                  ir_valid (λs s'. P1 s s'  P2 s s') c c' (λ t t'. Q1 t t'  Q2 t t')"
  by(fastforce simp: ir_valid_def)


theorem soundness:
  "ir_hoare P c c' Q  ir_valid P c c' Q"
  apply(induction rule: ir_hoare.induct)
              apply(blast intro!: Skip_ir_valid)
  by (blast intro: conseq_ir_valid)+

section "Completeness"

lemma ir_Skip_Skip[intro]:
  "ir_hoare P SKIP SKIP P"
  by(rule ir_Skip, simp)

lemma ir_hoare_Skip_Skip[simp]:
  "ir_hoare P SKIP SKIP Q = (s s'. Q s s'  P s s')"
  using soundness ir_valid_def meh_simp ir_conseq ir_Skip by metis

lemma ir_valid_Seq1:
  "ir_valid P (c1;; c2) c' Q  ir_valid P c1 c' (λt t'. s s'. P s s'  (c1,s)  t  (c',s')  t'  (u. (c2,t)  u  Q u t'))"
  by(auto simp: ir_valid_def)

lemma ir_valid_Seq1':
  "ir_valid P (c1;; c2) c' Q  ir_valid (λt t'. s s'. P s s'  (c1,s)  t  (c',s')  t'  (u. (c2,t)  u  Q u t')) c2 SKIP Q"
  by(clarsimp simp: ir_valid_def, meson SeqE)

lemma ir_valid_track_history:
  "ir_valid P c c' Q 
   ir_valid P c c' (λt t'. Q s s'  (s s'. P s s'  (c,s)  t  (c',s')  t'))"
  by(auto simp: ir_valid_def)

lemma ir_valid_If:
  "ir_valid (λs s'. P s s') (IF b THEN c1 ELSE c2) c' Q 
   ir_valid (λs s'. P s s'  bval b s) c1 c' (λt t'. Q t t'  (s s'. P s s'  (c1,s)  t  (c',s')  t'  bval b s)) 
   ir_valid (λs s'. P s s'  ¬ bval b s) c2 c' (λt t'. Q t t'  (s s'. P s s'  (c2,s)  t  (c',s')  t'  ¬ bval b s))"
  by(clarsimp simp: ir_valid_def, blast)

text ‹
  Inspired by the 
  ``@{text "p(n) = {σ | you can get back from σ to some state in p by executing C backwards n times}"}''
  part of OHearn~cite"OHearn_19".
›
primrec get_back where
  "get_back P b c 0 = (λt t'. P t t')" |
  "get_back P b c (Suc n) = (λt t'. s. (c,s)  t  bval b s  get_back P b c n s t')"

(* Currently not used anywhere *)
lemma ir_valid_get_back:
  "ir_valid (get_back P b c (Suc k)) (WHILE b DO c) c' Q 
   ir_valid (get_back P b c k) (WHILE b DO c) c' Q"
proof(induct k)
  case 0
  then show ?case by(clarsimp simp: ir_valid_def, blast)
next
  case (Suc k)
  then show ?case  using  WhileTrue get_back.simps(2) ir_valid_def by smt 
qed

(* both this an the next one get used in the completeness proof *)
lemma ir_valid_While1:
  "ir_valid (get_back P b c k) (WHILE b DO c) c' Q 
   (ir_valid (λs s'. get_back P b c k s s'  bval b s) c SKIP (λt t'. get_back P b c (Suc k) t t'  (u u'. (WHILE b DO c,t)  u  (c',t')  u'  Q u u')))"
proof (subst ir_valid_def, clarsimp)
  fix t t' s u u'
  assume "ir_valid (get_back P b c k) (WHILE b DO c) c' Q" 
         "(WHILE b DO c, t)  u"
         "(c, s)  t" 
         "(c', t')  u'"
         "Q u u'"
         "bval b s"
         "get_back P b c k s t'"
  thus "s. get_back P b c k s t'  bval b s  (c, s)  t"
  proof(induction k arbitrary: t t' s u u')
    case 0
    then show ?case 
      by auto
  next
    case (Suc k)
    show ?case
      using Suc.prems(3) Suc.prems(6) Suc.prems(7) by blast
  qed
qed

lemma ir_valid_While3:
  "ir_valid (get_back P b c k) (WHILE b DO c) c' Q 
   (ir_valid (λs s'. get_back P b c k s s'  bval b s) c c' (λt t'. (s'. (c',s')  t'  get_back P b c (Suc k) t s'  (u. (WHILE b DO c,t)  u   Q u t'))))"
  apply(subst ir_valid_def, clarsimp)
proof -
  fix t t' s' s u
  assume "ir_valid (get_back P b c k) (WHILE b DO c) c' Q" 
         "(WHILE b DO c, t)  u"
         "(c, s)  t" 
         "(c', s')  t'"
         "Q u t'"
         "bval b s"
         "get_back P b c k s s'"
  thus "s s'. get_back P b c k s s'  bval b s  (c, s)  t  (c',s')  t'"
  proof(induction k arbitrary: t t' s' s u)
    case 0
    then show ?case 
      by auto
  next
    case (Suc k)
    show ?case
      using Suc.prems(3) Suc.prems(4) Suc.prems(6) Suc.prems(7) by blast
  qed
qed

(* not used anywhere *)
lemma ir_valid_While2:
   "ir_valid P (WHILE b DO c) c' Q 
   ir_valid (λs s'. P s s'  ¬ bval b s) SKIP c' (λt t'. Q t t'  (s'. (c',s')  t'  P t s'  ¬ bval b t))"  
  by(clarsimp simp: ir_valid_def, blast)

lemma assign_upd_blah:
  "(λa. if a = x1 then s x1 else (s(x1 := aval x2 s)) a) = s"
  by(rule ext, auto)

lemma Assign_complete:
  assumes v: "ir_valid P (x1 ::= x2) c' Q"
  assumes q: "Q t t'"
  shows  "s'. (v. P (t(x1 := v)) s'  t x1 = aval x2 (t(x1 := v)))  (c', s')  t'"
proof -
  from v and q obtain s s' where a: "P s s'  (x1 ::= x2,s)  t  (c',s')  t'"
    using ir_valid_def by smt
  hence "P (λa. if a = x1 then s x1 else (s(x1 := aval x2 s)) a) s'  aval x2 s = aval x2 (s(x1 := s x1))"
    using assign_upd_blah 
    by simp
  thus ?thesis 
    using assign_upd_blah a 
    by (metis AssignE fun_upd_same fun_upd_triv fun_upd_upd)
qed

lemmas ir_Skip_sym = ir_sym[OF ir_Skip, simplified flip_def]

theorem completeness:
  "ir_valid P c c' Q  ir_hoare P c c' Q"
proof(induct c arbitrary: P c' Q)
case SKIP
  show ?case 
    apply(rule ir_Skip)
    using SKIP by(fastforce simp: ir_valid_def)
next
  case (Assign x1 x2)
  show ?case
    apply(rule ir_Assign)
    apply(rule ir_Skip)
    using Assign_complete Assign by blast
next
  case (Seq c1 c2)
  have a: "ir_hoare P c1 c' (λt t'. s s'. P s s'  (c1, s)  t  (c', s')  t'  (u. (c2, t)  u  Q u t'))"
    using ir_valid_Seq1 Seq by blast
  show ?case 
    apply(rule ir_Seq1)
     apply (blast intro: a)
    apply(rule ir_Skip_sym)
    by(metis SeqE ir_valid_def Seq)
next
  case (If x1 c1 c2)
  have t: "ir_hoare (λs s'. P s s'  bval x1 s) c1 c'
      (λt t'. Q t t'  (s s'. P s s'  (c1, s)  t  (c', s')  t'  bval x1 s))" and
       f: " ir_hoare (λs s'. P s s'  ¬ bval x1 s) c2 c'
      (λt t'. Q t t'  (s s'. P s s'  (c2, s)  t  (c', s')  t'  ¬ bval x1 s))"
    using ir_valid_If If by blast+
  show ?case 
    (* consider both cases of the if via conseq, disj, then _True and _False *)
    apply(rule ir_conseq)
      apply(rule ir_disj)
       apply(rule ir_If_True,fastforce intro: t)
      apply(rule ir_If_False, fastforce intro: f)    
     apply blast
    by (smt IfE ir_valid_def If)
next
  case (While x1 c)
  have a: "n. ir_hoare (λs s'. get_back P x1 c n s s'  bval x1 s) c SKIP (get_back P x1 c (Suc n))"
    using ir_valid_While1  While
    by (smt get_back.simps(2) ir_valid_def meh_simp)
  have b: "ir_hoare (λs s'. P s s'  bval x1 s) c c'
                    (λt t'.  s'. (c', s')  t'  (s. (c, s)  t  bval x1 s  P s s')  
                    (u. (WHILE x1 DO c, t)  u  Q u t'))"
    using ir_valid_While3[where k=0,simplified] While by blast
  have gb: "t t'. Q t t'  (s'. (c', s')  t'  P t s'  ¬ bval x1 t) 
                    s'. ((n. get_back P x1 c n t s')  ¬ bval x1 t)  (c', s')  t'"
    by (meson get_back.simps(1))
  
  show ?case 
    (* use the frontier rule much as in OHearn POPL *)
    apply(rule ir_conseq)
      apply(rule_tac P="get_back P x1 c" in ir_While_backwards_frontier)
       apply(blast intro: a)
      (* consider both cases of the While via conseq, disj, then _True and _False *)
      apply(rule ir_conseq)
        apply(rule ir_disj)
         apply(rule_tac P="λs s'. n. get_back P x1 c n s s'" and Q="(λt t'. Q t t'  (s'. (c', s')  t'  P t s'  ¬ bval x1 t))" in ir_While_False)
         apply(rule ir_Skip, blast intro: gb)
        apply(rule ir_While_True)
        apply(rule ir_Seq1[OF b])
        apply(rule ir_Skip_sym)
        apply(fastforce)
       apply (metis get_back.simps(1))
      apply assumption
     apply simp
    by (metis While.prems WhileE ir_valid_def)
qed




section "A Decomposition Principle: Proofs via Under-Approximate Hoare Logic"

text ‹
  We show the under-approximate analogue holds for Beringer's~cite"Beringer_11" decomposition
  principle for over-approximate relational logic.
›


definition
  decomp :: "rassn  com  com  rassn  rassn" where
  "decomp P c c' Q  λt s'. s t'. P s s'  (c,s)  t  (c',s')  t'  Q t t'"


lemma ir_valid_decomp1:
  "ir_valid P c c' Q  ir_valid P c SKIP (decomp P c c' Q)  ir_valid (decomp P c c' Q) SKIP c' Q"
  by(fastforce simp: ir_valid_def meh_simp decomp_def)

lemma ir_valid_decomp2:
  "ir_valid P c SKIP R  ir_valid R SKIP c' Q  ir_valid P c c' Q"
  by(fastforce simp: ir_valid_def meh_simp decomp_def)

lemma ir_valid_decomp:
  "ir_valid P c c' Q = (ir_valid P c SKIP (decomp P c c' Q)  ir_valid (decomp P c c' Q) SKIP c' Q)"
  using ir_valid_decomp1 ir_valid_decomp2 by blast

text ‹
  Completeness with soundness means we can prove proof rules about @{term ir_hoare} in terms
  of @{term ir_valid}.
›

lemma ir_to_Skip:     
  "ir_hoare P c c' Q = (ir_hoare P c SKIP (decomp P c c' Q)  ir_hoare (decomp P c c' Q) SKIP c' Q)"
  using soundness completeness ir_valid_decomp 
  by meson

text ‹
  O'Hearn's under-approximate Hoare triple, for the ``ok'' case (since that is the only case we have)
  This is also likely the same as from the "Reverse Hoare Logic" paper (SEFM).
›
type_synonym assn = "state  bool"
definition
  ohearn :: "assn  com  assn  bool"
  where
  "ohearn P c Q  (t. Q t  (s. P s  (c,s)  t))"

lemma fold_ohearn1:
  "ir_valid P c SKIP Q = (t'. ohearn (λt. P t t') c (λt. Q t t'))"
  by(fastforce simp add: ir_valid_def ohearn_def)

lemma fold_ohearn2:
  "ir_valid P SKIP c' Q = (t. ohearn (P t) c' (Q t))"
  by(simp add: ir_valid_def ohearn_def)

theorem relational_via_hoare:
  "ir_hoare P c c' Q = ((t'. ohearn (λt. P t t') c (λt. decomp P c c' Q t t'))  (t. ohearn (decomp P c c' Q t) c' (Q t)))"
proof -
  have a: "P c c' Q. ir_hoare P c c' Q = ir_valid P c c' Q"
    using soundness completeness by auto
  show ?thesis
    using ir_to_Skip a fold_ohearn1 fold_ohearn2 by metis
qed

section "Deriving Proof Rules from Completeness"

text ‹
  Note that we can more easily derive proof rules sometimes by appealing to the
   corresponding properties of @{term ir_valid} than from the proof rules directly.

  We see more examples of this later on when we consider examples.
›

lemma ir_Seq2: 
  "ir_hoare P c SKIP Q  ir_hoare Q d c' R  ir_hoare P (Seq c d) c' R"
  using soundness completeness Seq2_ir_valid by metis

lemma ir_Seq: 
  "ir_hoare P c c' Q  ir_hoare Q d d' R  ir_hoare P (Seq c d) (Seq c' d') R"
  using soundness completeness Seq_ir_valid by metis

section "Examples"

subsection "Some Derived Proof Rules"

text ‹
First derive some proof rules -- here not by appealing to completeness but just using
the existing rules 
›

lemma ir_If_True_False:   
  "ir_hoare (λs s'. P s s'  bval b s  ¬ bval b' s') c1 c2' Q  
   ir_hoare P (IF b THEN c1 ELSE c2) (IF b' THEN c1' ELSE c2') Q"
  apply(rule ir_If_True)
  apply(rule ir_sym)
  apply(rule ir_If_False)
  apply(rule ir_sym)
  by(simp add: flip_def)


lemma ir_Assign_Assign:
  "ir_hoare P (x ::= e) (x' ::= e') (λt t'. v v'. P (t(x := v)) (t'(x' := v'))  t x = aval e (t(x := v))  t' x' = aval e' (t'(x' := v')))"
  apply(rule ir_Assign)
  apply(rule ir_sym)
  apply(rule ir_Assign)
  by(simp add: flip_def, auto)

subsection "prog1"

text ‹
  A tiny insecure program. Note that we only need to reason on one path through this program to
  detect that it is insecure. 
›

abbreviation low_eq :: rassn where "low_eq s s'  s ''low'' = s' ''low''"
abbreviation low_neq :: rassn where "low_neq s s'  ¬ low_eq s s'"
definition prog1 :: com where
  "prog1  (IF (Less (N 0) (V ''x'')) THEN (Assign ''low'' (N 1)) ELSE (Assign ''low'' (N 0)))"

text ‹
  We prove that @{term prog1} is definitely insecure. To do that, we need to find some non-empty
  post-relation that implies insecurity. The following property encodes the idea that the 
  post-relation is non-empty, i.e. represents a feasible pair of execution paths.
›
definition
  nontrivial :: "rassn  bool"
  where
  "nontrivial Q  (t t'. Q t t')"

text ‹
  Note the property we prove here explicitly encodes the fact that the postcondition can be anything
  that implies insecurity, i.e. implies @{term low_neq}. In particular we should not necessarily
  expect it to cover the entirely of all states that satisfy @{term low_neq}. 

  Also note that we also have to prove that the postcondition is non-trivial. This is necessary to 
  make sure that the violation we find is not an infeasible path.
›
lemma prog1:
  "Q. ir_hoare low_eq prog1 prog1 Q  (s s'. Q s s'  low_neq s s')  nontrivial Q"
  apply(rule exI)
  apply(rule conjI)
   apply(simp add: prog1_def)
   apply(rule ir_If_True_False)
   apply(rule ir_Assign_Assign)
  apply(rule conjI)
   apply auto[1]
  apply(clarsimp simp: nontrivial_def)
  apply(rule_tac x="λv. 1" in exI)
  apply simp
  apply(rule_tac x="λv. 0" in exI)
  by auto

subsection "More Derived Proof Rules for Examples"

definition BEq :: "aexp  aexp  bexp" where
  "BEq a b  And (Less a (Plus b (N 1))) (Less b (Plus a (N 1)))"


lemma BEq_aval[simp]: 
  "bval (BEq a b) s = ((aval a s) = (aval b s))"
  by(auto simp add: BEq_def)

lemma ir_If_True_True:
  "ir_hoare (λs s'. P s s'  bval b s  bval b' s') c1 c1' Q1 
   ir_hoare P (IF b THEN c1 ELSE c2) (IF b' THEN c1' ELSE c2') (λt t'. Q1 t t')"
  by(simp add: ir_If_True ir_sym flip_def)

lemma ir_If_False_False:
  "ir_hoare (λs s'. P s s'  ¬ bval b s  ¬ bval b' s') c2 c2' Q2 
   ir_hoare P (IF b THEN c1 ELSE c2) (IF b' THEN c1' ELSE c2') (λt t'. Q2 t t')"
  by(simp add: ir_If_False ir_sym flip_def)

lemma ir_If':
  "ir_hoare (λs s'. P s s'  bval b s  bval b' s') c1 c1' Q1 
   ir_hoare (λs s'. P s s'  ¬ bval b s  ¬ bval b' s') c2 c2' Q2 
   ir_hoare P (IF b THEN c1 ELSE c2) (IF b' THEN c1' ELSE c2') (λt t'. Q1 t t'  Q2 t t')"
  apply(rule ir_pre)
   apply(rule ir_disj)
    apply(rule ir_If_True_True)
    apply assumption
   apply(rule ir_If_False_False)
   apply assumption
  apply blast
  done

lemma ir_While_triv:
  "ir_hoare (λs s'. P s s'  ¬ bval b s  ¬ bval b' s') SKIP SKIP Q2 
   ir_hoare P (WHILE b DO c) (WHILE b' DO c') (λs s'. (Q2 s s'))"
  by(simp add: ir_While_False ir_sym flip_def)

lemma ir_While':
  "ir_hoare (λs s'. P s s'  bval b s  bval b' s') (c;;WHILE b DO c) (c';;WHILE b' DO c') Q1 
   ir_hoare (λs s'. P s s'  ¬ bval b s  ¬ bval b' s') SKIP SKIP Q2 
   ir_hoare P (WHILE b DO c) (WHILE b' DO c') (λs s'. (Q1 s s'  Q2 s s'))"
  apply(rule ir_pre)
   apply(rule ir_disj)
     apply(rule ir_While_True)
     apply(rule ir_sym)
     apply(simp add: flip_def)
     apply(rule ir_While_True)
     apply(rule ir_sym)
    apply(simp add: flip_def)
   apply(rule ir_While_triv)
   apply assumption
  apply simp
  done 

subsection "client0"   

definition low_eq_strong where
  "low_eq_strong s s'  (s ''high''  s' ''high'')  low_eq s s'"

lemma low_eq_strong_upd[simp]:
  "var  ''high''  var  ''low''  low_eq_strong(s(var := v)) (s'(var := v')) = low_eq_strong s s'"
  by(auto simp: low_eq_strong_def)

text ‹
  A variation on client0 from O'Hearn~cite"OHearn_19": how to reason about loops via a single unfolding
›
definition client0 :: com where
  "client0  (Assign ''x'' (N 0);;
              (While (Less (N 0) (V ''n''))
                     ((Assign ''x'' (Plus (V ''x'') (V ''n'')));;
                      (Assign ''n'' (V ''nondet''))));;
              (If (BEq (V ''x'') (N 2000000)) (Assign ''low'' (V ''high'')) SKIP))"



lemma client0:
  "Q. ir_hoare low_eq client0 client0 Q  (s s'. Q s s'  low_neq s s')  nontrivial Q"
  apply(rule exI, rule conjI, simp add: client0_def)
   apply(rule_tac P=low_eq_strong in ir_pre)  
   apply(rule ir_Seq)
    apply(rule ir_Seq)
      apply(rule ir_Assign_Assign)
     apply clarsimp

    apply(rule ir_While')
      apply clarsimp

      apply(rule ir_Seq)
       apply(rule ir_Seq)
        apply(rule ir_Assign_Assign)
       apply(rule ir_Assign_Assign)
      apply clarsimp

      apply(rule ir_While_triv)
      apply clarsimp
      apply assumption

     apply clarsimp
     apply assumption


    apply(rule ir_If_True_True)
    apply(rule ir_Assign_Assign)
   apply(fastforce simp: low_eq_strong_def)
  apply(rule conjI)
   apply(clarsimp simp: low_eq_strong_def split: if_splits)

  (* ugh having to manually do constraint solving here... *)
  apply(clarsimp simp: low_eq_strong_def nontrivial_def)
  apply(rule_tac x="λv. if v = ''x'' then 2000000 else if v = ''high'' then 1 else if v = ''n'' then -1 else if v = ''nondet'' then -1 else if v = ''low'' then 1 else undefined" in exI)
  apply(rule_tac x="λv. if v = ''x'' then 2000000 else if v = ''high'' then 0 else if v = ''n'' then -1 else if v = ''nondet'' then -1 else if v = ''low'' then 0 else undefined" in exI)
  apply clarsimp
  done

(* Not needed? *)
lemma ir_While_backwards:
  "(n. ir_hoare (λ s s'. P n s s'  bval b s) c SKIP (P (Suc n))) 
                       ir_hoare (λs s'. n. P n s s'  ¬ bval b s) SKIP c' Q 
                       ir_hoare (P 0) (WHILE b DO c) c' Q"
  apply(rule ir_While_backwards_frontier)
   apply assumption
  apply(rule ir_While_False)
  apply auto
  done

subsection "Derive a variant of the backwards variant rule"

text ‹Here we appeal to completeness again to derive this rule from the corresponding
        property about @{term ir_valid}.›

subsection "A variant of the frontier rule"

text ‹
  Agin we derive this rule by appealing to completeness and the corresponding property of
  @{term ir_valid}

lemma While_backwards_frontier_both_ir_valid':
  assumes asm: "n. t t'. P (k + Suc n) t t' 
                    (s s'. P (k + n) s s'  bval b s  bval b' s'  (c, s)  t  (c', s')  t')"
  assumes last: "t t'. Q t t'  (s s'. (n. P (k + n) s s')  (WHILE b DO c, s)  t  (WHILE b' DO c', s')  t')"
  assumes post: "Q t t'"
  shows "s s'. P k s s'  (WHILE b DO c, s)  t  (WHILE b' DO c', s')  t'"
proof -
  from post last obtain s s' n where 
    "P (k + n) s s'" "(WHILE b DO c, s)  t" "(WHILE b' DO c', s')  t'"
    by blast
  with asm  show ?thesis
  proof(induction n arbitrary: k t t')
    case 0 
    then show ?case 
      by (metis WhileFalse WhileTrue add.right_neutral)
  next
    case (Suc n)
    from Suc
    obtain r r' where final_iteration: "P (Suc k) r r'" "(WHILE b DO c, r)  t" "(WHILE b' DO c', r')  t'"
      by (metis add_Suc_shift)
    from final_iteration(1) obtain q q' where
     "P k q q'  bval b q  bval b' q'  (c, q)  r  (c', q')  r'" 
      by (metis Nat.add_0_right Suc.prems(1) plus_1_eq_Suc semiring_normalization_rules(24))
    with final_iteration show ?case by blast
  qed
qed

lemma While_backwards_frontier_both_ir_valid[intro]:
  "(n. ir_valid (λ s s'. P n s s'  bval b s  bval b' s') c c' (P (Suc n))) 
   ir_valid (λs s'. n. P n s s') (WHILE b DO c) (WHILE b' DO c') Q 
   ir_valid (P 0) (WHILE b DO c) (WHILE b' DO c') (λs s'. Q s s')"
  by(auto simp: ir_valid_def intro: While_backwards_frontier_both_ir_valid')

lemma ir_While_backwards_frontier_both:
  "n. ir_hoare (λs s'. P n s s'  bval b s  bval b' s') c c' (P (Suc n));
   ir_hoare (λs s'. n. P n s s') (WHILE b DO c) (WHILE b' DO c') Q
    ir_hoare (P 0) (WHILE b DO c) (WHILE b' DO c') (λs s'. Q s s')"
  using soundness completeness While_backwards_frontier_both_ir_valid by auto

text ‹
  The following rule then follows easily as a special case
›
lemma ir_While_backwards_both:
  "(n. ir_hoare (λ s s'. P n s s'  bval b s  bval b' s') c c' (P (Suc n))) 
                       ir_hoare (P 0) (WHILE b DO c) (WHILE b' DO c') (λs s'. n. P n s s'  ¬ bval b s  ¬ bval b' s')"
  apply(rule ir_While_backwards_frontier_both)
   apply blast
  by(simp add: ir_While_False ir_sym flip_def)


subsection "client1"


text ‹
  An example roughly equivalent to cient1 from O'Hearn~cite"OHearn_19"0 

  In particular we use the backwards variant rule to reason about the loop.
›
definition client1 :: com where
  "client1  (Assign ''x'' (N 0);;
              (While (Less (V ''x'') (V ''n''))
                     ((Assign ''x'' (Plus (V ''x'') (N 1)))));;
              (If (BEq (V ''x'') (N 2000000)) (Assign ''low'' (V ''high'')) SKIP))"


lemma client1:
  "Q. ir_hoare low_eq client1 client1 Q  (s s'. Q s s'  low_neq s s')  nontrivial Q"
  apply(rule exI, rule conjI, simp add: client1_def)
   apply(rule_tac P=low_eq_strong in ir_pre)  
   apply(rule ir_Seq)
    apply(rule ir_Seq)
      apply(rule ir_Assign_Assign)
     apply clarsimp

  apply(rule ir_pre)
      apply(rule ir_While_backwards_both[where P="λn s s'. low_eq_strong s s'  s ''x'' = int n  s' ''x'' = int n  int n  s ''n''  int n  s' ''n''"])
      apply(rule ir_post)
       apply(rule ir_Assign_Assign)
      apply clarsimp
  
     apply clarsimp

    apply(rule ir_If_True_True)
    apply(rule ir_Assign_Assign)
   apply(fastforce simp: low_eq_strong_def)
  apply(rule conjI)
   apply(clarsimp simp: low_eq_strong_def split: if_splits)

  apply clarsimp
  (* ugh having to manually do constraint solving here... *)
  apply(clarsimp simp: low_eq_strong_def nontrivial_def)
  apply(rule_tac x="λv. if v = ''x'' then 2000000 else if v = ''high'' then 1 else if v = ''n'' then 2000000 else if v = ''nondet'' then -1 else if v = ''low'' then 1 else undefined" in exI)
  apply(rule_tac x="λv. if v = ''x'' then 2000000 else if v = ''high'' then 0 else if v = ''n'' then 2000000 else if v = ''nondet'' then -1 else if v = ''low'' then 0 else undefined" in exI)
  apply clarsimp
  done


subsection "client2"

text ‹
  An example akin to client2 from O'Hearn~cite"OHearn_19". 

  Note that this example is carefully written to show use of the frontier rule first to
  reason up to the broken loop iteration, and then we unfold the loop at that point to
  reason about the broken iteration, and then use the plain backwards variant rule to
  reason over the remainder of the loop.
›
definition client2 :: com where
  "client2  (Assign ''x'' (N 0);;
              (While (Less (V ''x'') (N 4000000))
                     ((Assign ''x'' (Plus (V ''x'') (N 1)));;
                       (If (BEq (V ''x'') (N 2000000)) (Assign ''low'' (V ''high'')) SKIP))
                       )
              )"

lemma client2:
  "Q. ir_hoare low_eq client2 client2 Q  (s s'. Q s s'  low_neq s s')  nontrivial Q"
  apply(rule exI, rule conjI, simp add: client2_def)
   apply(rule_tac P=low_eq_strong in ir_pre)  
   apply(rule ir_Seq)
     apply(rule ir_Assign_Assign)
    apply clarsimp

  apply(rule ir_pre)
     apply(rule ir_While_backwards_frontier_both[where P="λn s s'. low_eq_strong s s'  s ''x'' = int n  s' ''x'' = int n  s ''x''  0  s ''x''  2000000 - 1  s' ''x''  0  s' ''x''  2000000 - 1"])
      apply(rule ir_Seq)
       apply(rule ir_Assign_Assign)
  apply clarsimp
      apply(rule ir_post)
       apply(rule ir_If')
        apply(rule ir_Assign_Assign)
       apply(rule ir_Skip_Skip)
      apply clarsimp

     apply clarsimp
     apply(rule ir_While')
      apply clarsimp
      apply(rule ir_Seq)
       apply(rule ir_Seq)
       apply(rule ir_Assign_Assign)
      apply(rule ir_If_True_True)
      apply(rule ir_Assign_Assign)
     apply clarsimp

  apply(rule ir_pre)
     apply(rule ir_While_backwards_both[where P="λn s s'.  s ''x'' = 2000000 + int n  s' ''x'' = 2000000 + int n  s ''x''  2000000  s ''x''  4000000  s' ''x''  2000000  s' ''x''  4000000  s ''low'' = s ''high''  s' ''low'' = s' ''high''  s ''high''  s' ''high''"])


     apply(rule ir_Seq)
      apply(rule ir_Assign_Assign)
      apply(rule ir_If_False_False)
       apply fastforce
      apply (fastforce simp: low_eq_strong_def)
     apply fastforce
    apply(fastforce simp: low_eq_strong_def)
   apply(fastforce simp: low_eq_strong_def)

  apply(rule conjI)
   apply(clarsimp simp: low_eq_strong_def split: if_splits)

  apply clarsimp
  (* ugh having to manually do constraint solving here... *)
  apply(clarsimp simp: low_eq_strong_def nontrivial_def)
  apply(rule_tac x="λv. if v = ''x'' then 4000000 else if v = ''high'' then 1 else if v = ''n'' then 2000000 else if v = ''nondet'' then -1 else if v = ''low'' then 1 else undefined" in exI)
  apply(rule_tac x="λv. if v = ''x'' then 4000000 else if v = ''high'' then 0 else if v = ''n'' then 2000000 else if v = ''nondet'' then -1 else if v = ''low'' then 0 else undefined" in exI)
  apply clarsimp
  done

end