This file contains the hoare rules from the paper of lundberg et al. Those rules are being defined and proved. By proving these rules, we archive

1. showing the correctness of the rules themselves
2. verifying the compatibility of the constructed machine model and the hoare logic from lundberg et al.

The assumptions of Hoare's rules used here differ in some respects from those in lundberg et al. This is because conditions such as $L_W \cap L_B = \emptyset$ are preconditions from the judgement of \mathcal{L}_{AS}. These statements must be valid in order for the conditions for applying the assumptions to be met.

TODO: prove of S_LOOP

theorem BL_SUBSET (code : Code) (P Q : Assertion) (l : UInt64) (L_w L_b L : Set UInt64) : L_w ∩ L_b = ∅ → code ⦃P⦄ l ↦ ⟨L_w | L_b⟩⦃Q⦄ → code ⦃P⦄ l ↦ ⟨L_w | L_b \ L⟩⦃Q⦄

Allows to weaken the Hoare triple by removing a set L from L_B without any restrictions

theorem BL_TO_WL (code : Code) (P Q : Assertion) (l : UInt64) (L_w L_b L : Set UInt64) : L ⊆ L_b → L_w ∩ L_b = ∅ → L_w ≠ ∅ → code ⦃P⦄ l ↦ ⟨L_w | L_b⟩⦃Q⦄ → code ⦃P⦄ l ↦ ⟨L_w ∪ L | L_b \ L⟩⦃Q⦄

Allows to weaken the Hoare triple by moving a set L it to L_W without restrictions.

theorem WL_TO_BL (c : Code) (P Q : Assertion) (l : UInt64) (L_w L_b L : Set UInt64) : L ⊂ L_w → (∀ (s : MState), Q s → s.pc ∉ L) → L_w ∩ L_b = ∅ → L_w ≠ ∅ → c ⦃P⦄ l ↦ ⟨L_w | L_b⟩⦃Q⦄ → c ⦃P⦄ l ↦ ⟨L_w \ L | L_b ∪ L⟩⦃Q⦄

This rule can be used to transfer the set L from L_W to L_B. However, this requires that the postcondition Q does not cause the PC to point to a line from L.

theorem S_SEQ {L_b'' : Set UInt64} (P R Q : Assertion) (c : Code) (l : UInt64) (L_w L_b L_w' L_b' : Set UInt64) : L_w ∩ L_b = ∅ → L_w ≠ ∅ → L_w' ∩ L_b' = ∅ → L_w' ⊆ L_b ∧ L_w ∩ L_w' = ∅ → c ⦃P⦄ l ↦ ⟨L_w | L_b⟩⦃R⦄ → (∀ l' ∈ L_w, c ⦃R⦄ l' ↦ ⟨L_w' | L_b'⟩⦃Q⦄) → L_b'' = L_b ∩ L_b' → c ⦃P⦄ l ↦ ⟨L_w' | L_b''⟩⦃Q⦄

Enables the merge of two Hoare-triples into one, given that the postcondition of the first triple is equal to the precondition of the second triple.

This rule lets you apply S_SEQ with any form of L_{B''} but asks for a proof of L_{B''} = L_B ∩ L_{B'}

theorem S_SEQ' (P R Q : Assertion) (c : Code) (l : UInt64) (L_w L_b L_w' L_b' : Set UInt64) : L_w ∩ L_b = ∅ → L_w ≠ ∅ → L_w' ∩ L_b' = ∅ → L_w' ⊆ L_b ∧ L_w ∩ L_w' = ∅ → c ⦃P⦄ l ↦ ⟨L_w | L_b⟩⦃R⦄ → (∀ l' ∈ L_w, c ⦃R⦄ l' ↦ ⟨L_w' | L_b'⟩⦃Q⦄) → c ⦃P⦄ l ↦ ⟨L_w' | L_b ∩ L_b'⟩⦃Q⦄

Enables the merge of two Hoare-triples into one, given that the postcondition of the first triple is equal to the precondition of the second triple.

theorem PRE_STR (c : Code) (P1 P2 Q : Assertion) (L_w L_b : Set UInt64) (l : UInt64) : (∀ (s : MState), s.code = c → s.pc = l ∧ P2 s → P1 s) → c ⦃P1⦄ l ↦ ⟨L_w | L_b⟩⦃Q⦄ → c ⦃P2⦄ l ↦ ⟨L_w | L_b⟩⦃Q⦄

Allows to strenghten the precondition of a given Hoare-triple

theorem POST_WEAK (c : Code) (P Q1 Q2 : Assertion) (L_w L_b : Set UInt64) (l : UInt64) : (∀ (s : MState), s.code = c → s.pc ∈ L_w ∧ Q1 s → Q2 s) → c ⦃P⦄ l ↦ ⟨L_w | L_b⟩⦃Q1⦄ → c ⦃P⦄ l ↦ ⟨L_w | L_b⟩⦃Q2⦄

Allows to weaken the postcondition of a given Hoare-triple

theorem S_COND (c : Code) (P C Q : Assertion) (l : UInt64) (L_w L_b : Set UInt64) : c ⦃P.And C⦄ l ↦ ⟨L_w | L_b⟩⦃Q⦄ → c ⦃P.And C.Not⦄ l ↦ ⟨L_w | L_b⟩⦃Q⦄ → c ⦃P⦄ l ↦ ⟨L_w | L_b⟩⦃Q⦄

In this rule, a condition C is evaluated and, depending on whether it is fulfilled or not, either the command chain S_1 or S_2$ is executed.

theorem S_LOOP {α : Type} [Preorder α] [WellFoundedLT α] (Q C I : Assertion) (code : Code) (l : UInt64) (L_w L_b : Set UInt64) (V : MState → α) : l ∉ L_w → l ∉ L_b → (∀ (x : α), code ⦃C st✝ ∧ I st✝ ∧ V st✝ = x⦄ l ↦ ⟨{l} ∪ L_w | L_b⟩⦃V st✝ < x ∧ I st✝ ∧ ⸨pc⸩ = l⦄) → code ⦃¬C st✝¹ ∧ I st✝¹⦄ l ↦ ⟨L_w | L_b⟩⦃Q⦄ → code ⦃I⦄ l ↦ ⟨L_w | L_b⟩⦃Q⦄

A rule to verify the formal correctness of a loop. Requires:

• A Condition C

• An Invariant I

• A Variant V

  High-level proof idea of S_LOOP

  • Define C v := “for any state s at l with invariant I and variant V s = v, we can reach some s' satisfying Q via weak with the original L_w/L_b.”
  • Prove C v by well-founded induction on v.
    • If C s (the loop condition) holds, use the given loop-body triple at variant v to get a next state s' back at l with strictly smaller variant (V s' < v) and still I. Then apply induction hypothesis to V s' to get a final state s'' satisfying Q. Finally, compose the two runs to build weak s s'' ... (this is where we stitch step counts and the “no earlier hit” condition).
    • If ¬C s, use the given exit triple to get Q directly.
  • Apply C (V s) to your original starting state s.