Soundness of Hoare Logic

module Chapter.Imp.HoareLogicSoundness where

Imports

open import Library.Bool
open import Library.Nat
open import Library.Nat.Properties
open import Library.Logic
open import Library.Logic.Laws
open import Library.Equality
open import Library.Equality.Reasoning

open import Chapter.Imp.AexpBexp
open import Chapter.Imp.BigStep
open import Chapter.Imp.HoareLogic

Formalizing the partial correctness criterion into a definition, we say that the triple [ P ] c [ Q ] is valid if for all s, t ∈ State whenever P holds of s and ⦅ c , s ⦆ converges to t, Q holds of t. Formally, we define the following predicate:

|=_ : Triple -> Set
|= [ P ] c [ Q ] = ∀ {s t} -> P s -> ⦅ c , s ⦆ ⇒ t -> Q t

Hoare Logic is intended to provide a tool to establish when a triple is valid. To ensure that this is the case, we show that the system is sound i.e. that only valid triples are derivable. This is the content of theorem-Hoare-sound claiming the implication

                ∀ {P c Q} ->  |- [ P ] c [ Q ]  ->  |= [ P ] c [ Q ]

The strategy to prove the theorem is first to show that all instances of axioms H-Skip and H-Loc are valid triples, which is immediate. Then the actual task in the proof is to show that the remaining rules infer valid triples from valid ones instantiating the respective premises. All in all, this is a proof by structural induction on the derivation of |- [ P ] c [ Q ].

Going through the proof, we realise that the thesis is an easy consequence of the induction hypotheses in all cases but in case of rule H-While, which deserves a more careful inspection. In Hoare system the rule is written:

                              {P ∧ b} c {P}
                        -------------------------
                        {P} WHILE b DO c {P ∧ ¬ b}

where P is the loop invariant, which is assumed to hold before executing the command WHILE b DO c and to be preserved by the execution of the body c whenever the condition of the guard b is true. From such hypotheses and the hypothesis that the execution of WHILE b DO c terminates, the rule infers that the post-condition of this loop is P ∧ ¬ b, where ¬ b expresses the fact that for a WHILE command to terminate the guard must be eventually false.

In our system the above rule is encoded by

       H-While : ∀ {P b c}
               -> |- [ (λ s -> P s ∧ bval b s == true) ] c [ P ]
               ---------------------------------------------------------------
               -> |- [ P ] (WHILE b DO c) [ (λ s -> P s ∧ bval b s == false) ]

To simplify the proof of the theorem, we begin with two lemmas stating respectively that under the hypothesis that [ (λ s -> P s ∧ bval b s == true) ] c [ P ] is valid, the assertion P is a loop invariant for WHILE b DO c and that if its execution terminates in a state t then bval b t == false.

lemma-Hoare-inv : ∀ {P : Assn} {s b c t} ->
                  (∀{s' t'} -> (P s' ∧ bval b s' == true) ->
                               ⦅ c , s' ⦆ ⇒ t'
                               -> P t') ->
                  P s ->
                  ⦅ WHILE b DO c , s ⦆ ⇒ t ->
                  P t
                  
lemma-Hoare-inv {P} {s} {b} {c} {.s} hyp1 hyp2 (WhileFalse x) = hyp2
lemma-Hoare-inv {P} {s} {b} {c} {t} hyp1 hyp2
           (WhileTrue {.c} {.b} {.s} {s'} {s''} x hyp3 hyp4) = claim2 
     where
       claim1 = hyp1 {s} {s'} (hyp2 , x) hyp3               
       claim2 = lemma-Hoare-inv {P} {s'} {b} {c} {t}
                                  (hyp1 {_} {_}) claim1 hyp4

lemma-Hoare-loop-exit : ∀ {b c s t}
             -> ⦅ WHILE b DO c , s ⦆ ⇒ t -> bval b t == false 

lemma-Hoare-loop-exit (WhileFalse x) = x
lemma-Hoare-loop-exit (WhileTrue x hyp1 hyp2) =
                                  lemma-Hoare-loop-exit hyp2

Technically we observe the usage of implicit arguments in the proof of lemma-Hoare-inv and in particular of dot patterns Implicit arguments are necessary to distinguish the states s', s'' from s: indeed the formers are automatically generated by Agda when splitting the hypothesis ⦅ WHILE b DO c , s ⦆ ⇒ s'' of the inductive case into ⦅ c , s ⦆ ⇒ s' and ⦅ WHILE b DO c , s' ⦆ ⇒ s'', so that without passing the implicit arguments to WhileTrue they are not in scope and hence inaccessible.

Dot patterns are constraints used by Agda to enforce the same binding of several occurrences of a variable in a non linear pattern: for example the variable {.c} has to be bound to the same command as the previous variable {c}. For explanations about dot patterns see Function Definitions - Dot patterns in Agda documentation.

We are eventually in place to prove theorem-Hoare-sound which is a corollary of lemma-Hoare-sound that establishes the same thesis but in a more explicit form, which allows the access to those implicit parameters which are essential in the proof of the theorem.

lemma-Hoare-sound : ∀ {P c Q s t} ->
             |- [ P ] c [ Q ] -> 
             P s -> 
             ⦅ c , s ⦆ ⇒ t -> 
             Q t

To facilitate the understanding of the proof we intersperse the cases with some comments drown from the interactive construction of the proof itself. As a first step in the proof we write

                 lemma-Hoare-sound hyp1 hyp2 hyp3 = ?

and then we hit C-c C-c twice splitting hyp1 : |- [ P ] c [ Q ] and hyp3 : ⦅ c , s ⦆ ⇒ t.

lemma-Hoare-sound H-Skip hyp2 Skip = hyp2

lemma-Hoare-sound H-Loc hyp2 Loc = hyp2

In cases of H-Skip and H-Loc the hypothesis hyp2 in the left-hand sides has the types P s and Q (s [ x ::= aval a s ]) respectively. These are the same as the types of the respective right-hand sides, hence they are both authomatically obtained typing C-c C-a while putting the cursor in the holes.

lemma-Hoare-sound (H-Comp hyp1 hyp4) hyp2 (Comp hyp3 hyp5) = IH2
      where
         IH1 = lemma-Hoare-sound hyp1 hyp2 hyp3
         IH2 = lemma-Hoare-sound hyp4 IH1 hyp5

In case of H-Comp, typing

      lemma-Hoare-sound (H-Comp hyp1 hyp4) hyp2 (Comp hyp3 hyp5) = ?

and then hitting C-c C-, with the cursor in the hole we obtain from Agda the reply (omitting parameters that are not in scope):

      Goal: Q t
      ———————————————————————————————————————————————————————
      hyp5 : ⦅ c₂ , s₂ ⦆ ⇒ t
      hyp3 : ⦅ c₁ , s ⦆ ⇒ s₂
      hyp2 : P s
      hyp4 : |- [ Q₁ ] c₂ [ Q ]
      hyp1 : |- [ P ] c₁ [ Q₁ ]

The induction hypothesis lemma-Hoare-sound hyp1 is a proof of |= [ P ] c₁ [ Q₁ ] that is applied to hyp2 : P s and to hyp3 : ⦅ c₁ , s ⦆ ⇒ s₂ yielding a proof IH1 : Q₁ s₂. On the other hand the induction hypothesis lemma-Hoare-sound hyp4 is a proof of |= [ Q₁ ] c₂ [ Q ], that when applied to IH1 : Q₁ s₂ and hyp5 : ⦅ c₂ , s₂ ⦆ ⇒ t returns a proof of Q t which is the goal.

lemma-Hoare-sound (H-If hyp1 hyp4) hyp2 (IfTrue x hyp3) = thesis
      where

        IH = lemma-Hoare-sound hyp1
        thesis = IH (hyp2 , x) hyp3

lemma-Hoare-sound (H-If hyp1 hyp4) hyp2 (IfFalse y hyp3) = thesis
      where

        IH = lemma-Hoare-sound hyp4
        thesis = IH (hyp2 , y) hyp3

Case H-If is split into two subcases according to the value of b from the command IF b THEN c₁ ELSE c₂ in the third hypothesis. By asking Agda about the context by means of C-c C-, we get

      Goal: Q t
      ——————————————————————————————————————————————————————
      hyp3 : ⦅ c₁ , s ⦆ ⇒ t
      x    : bval b s == true
      hyp2 : P s
      hyp4 : |- [ (λ s₁ -> P s₁ ∧ bval b s₁ == false) ] c₂ [ Q ]
      hyp1 : |- [ (λ s₁ -> P s₁ ∧ bval b s₁ == true) ] c₁ [ Q ]

In case of (IfTrue x hyp3) : ⦅ IF b THEN c₁ ELSE c₂ , s ⦆ ⇒ t the induction hypothesis IH = lemma-Hoare-sound hyp1 : |= [ (λ s₁ -> P s₁ ∧ bval b s₁ == true) ] c₁ [ Q ] is applied to (hyp2 , x) : P s ∧ bval b s == true and to hyp3 : ⦅ c₁ , s ⦆ ⇒ t yielding a proof thesis : Q t as desired.

The case (IfFalse y hyp3) : ⦅ IF b THEN c₁ ELSE c₂ , s ⦆ ⇒ t, where hyp3 : ⦅ c₂ , s ⦆ ⇒ t and y : bval b s == false is similar, using the induction hypothesis IH = lemma-Hoare-sound hyp4.

lemma-Hoare-sound {P} {_} {_} {s} {t}
                  (H-While {_} {b} hyp1) hyp2 hyp3 = Pt , b-false
      where

        Pt : P t
        Pt = lemma-Hoare-inv (lemma-Hoare-sound hyp1 ) hyp2 hyp3 

        b-false : bval b t == false
        b-false = lemma-Hoare-loop-exit hyp3

Case H-While is the most interesting one. Starting with

      lemma-Hoare-sound {P} {_} {_} {s} {t}
              (H-While {.P} {b} hyp1) hyp2 hyp3 = ?

and typing C-c C-l and then C-c C-, with the cursor in the hole we get the context:

      Goal: P t ∧ bval b t == false
      ———————————————————————————————————————————————————————
      hyp3 : ⦅ WHILE b DO c , s ⦆ ⇒ t
      hyp2 : P s
      hyp1 : |- [ (λ s₁ -> P s₁ ∧ bval b s₁ == true) ] c [ P ]

Since the goal is a conjunction, putting the cursor in the hole and typing C-c C-r to refine Agda’s guess about the filling of the hole, we get a pair of holes {!!} , {!!}; in the first hole it is expected a proof of P t, which is called Pt in the above proof, and in the second hole a proof of bval b == false is required, which is called b-false.

Now, by passing the induction hypothesis lemma-Hoare-sound hyp1 : |= [ (λ s₁ -> P s₁ ∧ bval b s₁ == true) ] c [ P ] to the lemma lemma-Hoare-inv and then the result to hyp2 and to hyp3 we get a proof of the fact that P is an invariant of the command WHILE b DO c, hence it holds for the final state t whenever ⦅ WHILE b DO c , s ⦆ ⇒ t; therefore we have established that P t holds as required.

On the other hand applying lemma-Hoare-loop-exit to hyp3 : ⦅ WHILE b DO c , s ⦆ ⇒ t we obtain a proof b-false : bval b t == false which ends the proof of this case.

lemma-Hoare-sound {_} {_} {_} {s} {t}
                               (H-Conseq x hyp1 y) hyp2 hyp3 = ths
      where

        P₁s = x s hyp2
        IH  = lemma-Hoare-sound hyp1
        Q₁t = IH P₁s hyp3
        ths = y t Q₁t

In the case H-Conseq we have the context:

      Goal: Q t
      ————————————————————————————————————————————————————
      hyp3 : ⦅ c , s ⦆ ⇒ t
      hyp2 : P s
      y    : (s₁ : State) -> Q₁ s₁ -> Q s₁
      hyp1 : |- [ P₁ ] c [ Q₁ ]
      x    : (s₁ : State) -> P s₁ -> P₁ s₁

Then the induction hypothesis lemma-Hoare-sound hyp1 : |= [ P₁ ] c [ Q₁ ] can be easily combined with P₁s = x s hyp2 : P₁ s and Q₁t = IH P₁s hyp3 : Q₁ t establishing the thesis ths = y t Q₁t : Q t as desired.

Eventually we conclude:

theorem-Hoare-sound : ∀ {P c Q} ->
                    |- [ P ] c [ Q ] -> |= [ P ] c [ Q ] 

theorem-Hoare-sound hyp = lemma-Hoare-sound hyp

Remark. The functions theorem-Hoare-sound and lemma-Hoare-sound have different definitions, even if when applied to hyp yield the same value. The reason is that these functions are extensionally equivalent, that is they yield the same values for the same arguments. However the extensionality principle is not part of the Agda logic, rather it is just compatible with it and must be postulated for use in proofs.