Documentation

CatCryptCore.Tactics.Restore

Invariant Restoration Tactics #

This file provides tactics for restoring invariants after put (write) operations.

Background #

After a put operation in a relational proof, the precondition may become "broken" - the rules rHoare_put_l and rHoare_put_r produce goals where the precondition is wrapped in set_lhs or set_rhs.

In the Lean formulation:

These tactics help "unwrap" the set operations when we can show that the invariant is preserved by the write.

Main tactics #

References #

Consequence-based Restoration #

An alternative approach is to use the consequence rule directly. When set_lhs l v pre h₀ h₁ holds (i.e., pre (h₀.set l v) h₁), we can establish pre' h₀ h₁ for some weaker precondition pre' if we can show that pre' is implied by pre on the modified heap.

source
theorem CatCrypt.Relational.set_lhs_conseq {pre pre' : RPre} {l : Core.Location} {v : l.ty} (h : ∀ (h₀ h₁ : Core.Heap), pre (h₀.set l v) h₁ → pre' h₀ h₁) (h₀ h₁ : Core.Heap) :
Invariant.set_lhs l v pre h₀ h₁ → pre' h₀ h₁

Weaken a set_lhs precondition using consequence. If we have set_lhs l v pre and can derive pre' from pre (_.set l v) _, then we can use pre' instead.

source
theorem CatCrypt.Relational.set_rhs_conseq {pre pre' : RPre} {l : Core.Location} {v : l.ty} (h : ∀ (h₀ h₁ : Core.Heap), pre h₀ (h₁.set l v) → pre' h₀ h₁) (h₀ h₁ : Core.Heap) :
Invariant.set_rhs l v pre h₀ h₁ → pre' h₀ h₁

Weaken a set_rhs precondition using consequence.

source
theorem CatCrypt.Relational.rHoare_restore_lhs_conseq {α : Type u_1} {β : Type u_2} {l : Core.Location} {v : l.ty} {pre pre' : RPre} {post : RPost α β} {c₁ : Core.SPComp α} {c₂ : Core.SPComp β} (hweaken : ∀ (h₀ h₁ : Core.Heap), pre (h₀.set l v) h₁ → pre' h₀ h₁) (hrh : rHoare pre' c₁ c₂ post) :
rHoare (Invariant.set_lhs l v pre) c₁ c₂ post

Restore with consequence: the most general form. Apply the consequence rule to weaken from set_lhs pre to pre'.

source
theorem CatCrypt.Relational.rHoare_restore_rhs_conseq {α : Type u_1} {β : Type u_2} {l : Core.Location} {v : l.ty} {pre pre' : RPre} {post : RPost α β} {c₁ : Core.SPComp α} {c₂ : Core.SPComp β} (hweaken : ∀ (h₀ h₁ : Core.Heap), pre h₀ (h₁.set l v) → pre' h₀ h₁) (hrh : rHoare pre' c₁ c₂ post) :
rHoare (Invariant.set_rhs l v pre) c₁ c₂ post

Restore with consequence for right side.

Tactics #

source
def CatCrypt.Tactics.tacticSsprove_restore_pre :
Lean.ParserDescr

ssprove_restore_pre restores the precondition after put operations.

After a put operation, the precondition is wrapped in set_lhs or set_rhs. This tactic applies the appropriate consequence-based restoration rule.

Example:

-- Goal: rHoare (set_lhs l v pre) c₁ c₂ post
-- After ssprove_restore_pre:
-- Goal 1: ∀ h₀ h₁, pre (h₀.set l v) h₁ → pre' h₀ h₁
-- Goal 2: rHoare pre' c₁ c₂ post
Equations
Instances For
    source
    def CatCrypt.Tactics.tacticSsprove_restore_mem :
    Lean.ParserDescr

    ssprove_restore_mem restores the precondition including remembered values.

    This is an alias for ssprove_restore_pre in the current implementation.

    Equations
    Instances For
      source
      def CatCrypt.Tactics.tacticSsprove_restore_inv :
      Lean.ParserDescr

      ssprove_restore_inv is an automation tactic that tries various restoration strategies and attempts to discharge preservation side conditions automatically.

      Equations
      Instances For