Documentation

CatCryptCore.Tactics.SP

Strongest Postcondition Tactics #

This file provides tactics for strongest postcondition reasoning in pRHL, analogous to EasyCrypt's sp tactic.

Main tactics #

What EasyCrypt does #

EasyCrypt's sp processes the deterministic prefix of programs forwards, updating the precondition to reflect the operations consumed. It is the forward dual of wp.

How it maps to SPComp #

In our monadic setting, prefix consumption means decomposing set l v >>= k or get l >>= k at the HEAD of the program using rHoare_bind + sync rules. The precondition gets updated.

SPComp headSP transformation
pure v >>= kSubstitute v, precondition unchanged
set l v >>= kConsume set, precondition updated with heap set
get l >>= kConsume get, precondition gains knowledge of heap value
sample, failStop — non-deterministic

References #

SP Rules: Consuming Head Operations into Precondition #

source
theorem CatCrypt.Relational.rHoare_sp_ret {α β γ δ : Type} {Φ Φ' : RPre} {Ψ : RPost γ δ} {a : α} {b : β} {k₁ : α → Core.SPComp γ} {k₂ : β → Core.SPComp δ} (hpre : ∀ (h₁ h₂ : Core.Heap), Φ h₁ h₂ → Φ' h₁ h₂) (h : rHoare Φ' (k₁ a) (k₂ b) Ψ) :
rHoare Φ ((Core.SPComp.pure a).bind k₁) ((Core.SPComp.pure b).bind k₂) Ψ

SP for pure a >>= k at the head of both programs.

Both programs start with pure a >>= k₁ and pure b >>= k₂. Since pure a >>= k = k a, we reduce to k₁ a and k₂ b with the same precondition (possibly strengthened).

source
theorem CatCrypt.Relational.rHoare_sp_set {γ : Type u_1} {δ : Type u_2} {Φ : RPre} {Ψ : RPost γ δ} {l : Core.Location} {v : l.ty} {k₁ : Unit → Core.SPComp γ} {k₂ : Unit → Core.SPComp δ} (h : rHoare (fun (h₁ h₂ : Core.Heap) => Φ h₁ h₂) (k₁ ()) (k₂ ()) Ψ) :
rHoare (fun (h₁ h₂ : Core.Heap) => Φ (h₁.set l v) (h₂.set l v)) ((Core.SPComp.set l v).bind k₁) ((Core.SPComp.set l v).bind k₂) Ψ

SP for set l v >>= k at the head of both programs.

Both programs start with set l v >>= k. After consuming the set, the precondition is updated: instead of requiring Φ h₁ h₂, we require Φ (h₁.set l v) (h₂.set l v).

source
theorem CatCrypt.Relational.rHoare_sp_get {γ δ : Type} {Φ : RPre} {Ψ : RPost γ δ} {l : Core.Location} {k₁ : l.ty → Core.SPComp γ} {k₂ : l.ty → Core.SPComp δ} (h : ∀ (v : l.ty), rHoare (fun (h₁ h₂ : Core.Heap) => Φ h₁ h₂ ∧ h₁.get l = v ∧ h₂.get l = v) (k₁ v) (k₂ v) Ψ) :
rHoare (fun (h₁ h₂ : Core.Heap) => Φ h₁ h₂ ∧ h₁.get l = h₂.get l) ((Core.SPComp.get l).bind k₁) ((Core.SPComp.get l).bind k₂) Ψ

SP for get l >>= k at the head of both programs.

Both programs start with get l >>= k. After consuming the get, we universally quantify over the value read and add the knowledge that the heap value equals the read value.

Requires that the precondition implies both heaps agree at l.

SP Tactics #

source
def CatCrypt.Tactics.tacticSsprove_sp_step :
Lean.ParserDescr

ssprove_sp_step processes one deterministic operation at the head of both programs, updating the precondition.

It tries (in order):

  1. pure >>= k — substitute the value
  2. set l v >>= k — consume the set, update precondition
  3. get l >>= k — consume the get, add value knowledge
  4. One-sided put (left or right)
  5. One-sided get (left or right)
Equations
Instances For
    source
    def CatCrypt.Tactics.tacticSsprove_sp :
    Lean.ParserDescr

    ssprove_sp processes the deterministic prefix of both programs forwards, computing the strongest postcondition.

    It normalizes code first, then repeatedly peels off deterministic head operations (pure, set, get) from both sides, updating the precondition.

    The tactic stops at sample, fail, or any non-deterministic operation.

    Example:

    -- Before ssprove_sp:
-- rHoare Φ (do SPComp.set l v; sample Bool) (do SPComp.set l v; sample Bool) Ψ
-- After ssprove_sp:
-- rHoare (fun h₁ h₂ => Φ (h₁.set l v) (h₂.set l v)) (sample Bool) (sample Bool) Ψ
    Equations
    Instances For