Relational Assertions

This file defines relational preconditions and postconditions for pRHL.

Main definitions

• RPre - Relational precondition (predicate on heap pairs)
• RPost α β - Relational postcondition (predicate on (result, heap) pairs)
• eqPre - Equality precondition
• eqPost - Equality postcondition

Notation

• ⟨1⟩ - Access left component
• ⟨2⟩ - Access right component

Basic types

@[reducible, inline]

abbrev CatCrypt.Relational.RPre : Type

Relational precondition: predicate on pairs of heaps

Equations

• CatCrypt.Relational.RPre = (CatCrypt.Core.Heap → CatCrypt.Core.Heap → Prop)

@[reducible, inline]

abbrev CatCrypt.Relational.RPost (α : Type u_1) (β : Type u_2) : Type (max u_1 u_2)

Relational postcondition: predicate on pairs of (result, heap)

Equations

• CatCrypt.Relational.RPost α β = (α → CatCrypt.Core.Heap → β → CatCrypt.Core.Heap → Prop)

structure CatCrypt.Relational.RSpec (α : Type u_1) (β : Type u_2) : Type (max u_1 u_2)

Relational specification

• pre : RPre
• post : RPost α β

Standard preconditions

def CatCrypt.Relational.eqPre : RPre

Equality precondition: heaps must be equal

Equations

• CatCrypt.Relational.eqPre h₁ h₂ = (h₁ = h₂)

theorem CatCrypt.Relational.eqPre_eq (h₁ h₂ : Core.Heap) : eqPre h₁ h₂ = (h₁ = h₂)

Grind normalization for eqPre

def CatCrypt.Relational.truePre : RPre

True precondition: always holds

Equations

• CatCrypt.Relational.truePre x✝¹ x✝ = True

theorem CatCrypt.Relational.truePre_eq (h₁ h₂ : Core.Heap) : truePre h₁ h₂ = True

def CatCrypt.Relational.falsePre : RPre

False precondition: never holds

Equations

• CatCrypt.Relational.falsePre x✝¹ x✝ = False

theorem CatCrypt.Relational.falsePre_eq (h₁ h₂ : Core.Heap) : falsePre h₁ h₂ = False

Standard postconditions

def CatCrypt.Relational.eqPost {α : Type u_1} : RPost α α

Equality postcondition: results and heaps must be equal

Equations

• CatCrypt.Relational.eqPost a₁ h₁ a₂ h₂ = (a₁ = a₂ ∧ h₁ = h₂)

theorem CatCrypt.Relational.eqPost_eq {α : Type u_1} (a₁ a₂ : α) (h₁ h₂ : Core.Heap) : eqPost a₁ h₁ a₂ h₂ = (a₁ = a₂ ∧ h₁ = h₂)

Grind normalization for eqPost

def CatCrypt.Relational.truePost {α : Type u_1} {β : Type u_2} : RPost α β

True postcondition: always holds

Equations

• CatCrypt.Relational.truePost x✝³ x✝² x✝¹ x✝ = True

theorem CatCrypt.Relational.truePost_eq {α : Type u_1} {β : Type u_2} (a₁ : α) (h₁ : Core.Heap) (a₂ : β) (h₂ : Core.Heap) : truePost a₁ h₁ a₂ h₂ = True

Combinators

def CatCrypt.Relational.andPre (P Q : RPre) : RPre

Conjunction of preconditions

Equations

• (P ⋀ Q) h₁ h₂ = (P h₁ h₂ ∧ Q h₁ h₂)

def CatCrypt.Relational.«term_⋀_» : Lean.TrailingParserDescr

Equations

• One or more equations did not get rendered due to their size.

def CatCrypt.Relational.orPre (P Q : RPre) : RPre

Disjunction of preconditions

Equations

• (P ⋁ Q) h₁ h₂ = (P h₁ h₂ ∨ Q h₁ h₂)

def CatCrypt.Relational.«term_⋁_» : Lean.TrailingParserDescr

Equations

• One or more equations did not get rendered due to their size.

def CatCrypt.Relational.implPre (P Q : RPre) : RPre

Implication of preconditions

Equations

• (P ⟹ Q) h₁ h₂ = (P h₁ h₂ → Q h₁ h₂)

def CatCrypt.Relational.«term_⟹_» : Lean.TrailingParserDescr

Equations

• One or more equations did not get rendered due to their size.

def CatCrypt.Relational.andPost {α : Type u_1} {β : Type u_2} (P Q : RPost α β) : RPost α β

Conjunction of postconditions

Equations

• CatCrypt.Relational.andPost P Q a₁ h₁ a₂ h₂ = (P a₁ h₁ a₂ h₂ ∧ Q a₁ h₁ a₂ h₂)

EasyCrypt-style ⟨1⟩/⟨2⟩ accessors

def CatCrypt.Relational.lhs {γ : Type u_3} (f : Core.Heap → γ) : Core.Heap → Core.Heap → γ

Access left heap in relational assertion

Equations

• f⟨1⟩ h₁ x✝ = f h₁

def CatCrypt.Relational.rhs {γ : Type u_3} (f : Core.Heap → γ) : Core.Heap → Core.Heap → γ

Access right heap in relational assertion

Equations

• f⟨2⟩ x✝ h₂ = f h₂

def CatCrypt.Relational.«term_⟨1⟩» : Lean.TrailingParserDescr

Equations

• CatCrypt.Relational.«term_⟨1⟩» = Lean.ParserDescr.trailingNode `CatCrypt.Relational.«term_⟨1⟩» 1024 0 (Lean.ParserDescr.symbol "⟨1⟩")

def CatCrypt.Relational.«term_⟨2⟩» : Lean.TrailingParserDescr

Equations

• CatCrypt.Relational.«term_⟨2⟩» = Lean.ParserDescr.trailingNode `CatCrypt.Relational.«term_⟨2⟩» 1024 0 (Lean.ParserDescr.symbol "⟨2⟩")

Location-based assertions

def CatCrypt.Relational.leftHas (l : Core.Location) (v : l.ty) : RPre

Left heap has value v at location l

Equations

• CatCrypt.Relational.leftHas l v h₁ x✝ = (h₁.get l = v)

theorem CatCrypt.Relational.leftHas_eq (l : Core.Location) (v : l.ty) (h₁ h₂ : Core.Heap) : leftHas l v h₁ h₂ = (h₁.get l = v)

def CatCrypt.Relational.rightHas (l : Core.Location) (v : l.ty) : RPre

Right heap has value v at location l

Equations

• CatCrypt.Relational.rightHas l v x✝ h₂ = (h₂.get l = v)

theorem CatCrypt.Relational.rightHas_eq (l : Core.Location) (v : l.ty) (h₁ h₂ : Core.Heap) : rightHas l v h₁ h₂ = (h₂.get l = v)

Lemmas

@[simp]

theorem CatCrypt.Relational.eqPre_iff (h₁ h₂ : Core.Heap) : eqPre h₁ h₂ ↔ h₁ = h₂

@[simp]

theorem CatCrypt.Relational.truePre_iff (h₁ h₂ : Core.Heap) : truePre h₁ h₂ ↔ True

@[simp]

theorem CatCrypt.Relational.eqPost_iff {α : Type u_1} (a₁ : α) (h₁ : Core.Heap) (a₂ : α) (h₂ : Core.Heap) : eqPost a₁ h₁ a₂ h₂ ↔ a₁ = a₂ ∧ h₁ = h₂

theorem CatCrypt.Relational.andPre_iff (P Q : RPre) (h₁ h₂ : Core.Heap) : (P ⋀ Q) h₁ h₂ ↔ P h₁ h₂ ∧ Q h₁ h₂