Separation logic, typed

A solver's heap is declared once, at the Lean types of its locations and data. The two constructors that depend on it hang off the handle declareSepHeap answers, so a location or a datum of the wrong type does not compile:

let h ← s.declareSepHeap Int Int
s.assert (← h.pto x y)     -- `x y : Term Int`
let n ← h.nil              -- `n : Term Int`

sepEmp, sepStar and sepWand need no heap. getValueSepHeap and getValueSepNil describe the model's heap as formulas.

def Cvc.Typed.Term.sepStar [Ω] (lft rgt : Term Bool) : Env (Term Bool)

Separating conjunction: the heap splits in two, one part satisfying each side.

Equations

• lft.sepStar rgt = Cvc.Untyped.Term.sepStar lft rgt

def Cvc.Typed.Term.sepStarN [Ω] (terms : Terms Bool) (atLeastTwoElements : 2 ≤ Array.size terms := by (try grind) <;> fail "failed to prove term array has at least two elements") : Env (Term Bool)

sepStar over two or more terms.

Equations

• Cvc.Typed.Term.sepStarN terms atLeastTwoElements = Cvc.Untyped.Term.sepStarN terms atLeastTwoElements

def Cvc.Typed.Term.sepWand [Ω] (lft rgt : Term Bool) : Env (Term Bool)

Separating implication, the magic wand.

Equations

• lft.sepWand rgt = Cvc.Untyped.Term.sepWand lft rgt

def Cvc.Typed.Term.sepEmp [Ω] : Env (Term Bool)

Holds exactly when the heap is empty.

Equations

• Cvc.Typed.Term.sepEmp = Cvc.Untyped.Term.sepEmp

inductive Cvc.Typed.View.Sep [Ω] : Typ → Type

Sep's operators, taken apart one level, indexed by the sort each produces.

• bool [Ω] : OnBool → View.Sep Typ.bool

  An operator with a result of sort Bool.

inductive Cvc.Typed.View.Sep.OnBool [Ω] : Type

Sep's operators with a result of sort Bool.

• sepEmp [Ω] : OnBool

  Holds exactly when the heap is empty.

• sepStar [Ω] (kids : Kids Bool) : OnBool

  Separating conjunction: the heap splits in two, one part satisfying each side.

  kids holds every operand, two or more.

• sepWand [Ω] (lft rgt : Term Bool) : OnBool

  Separating implication, the magic wand.

def Cvc.Typed.View.Sep.of [Ω] (τ : Typ) (t : Term τ.Denote) : Env (Option (View.Sep τ))

Takes a term apart one level, at its sort, if Sep owns its operator and the term's sort fits it.

Equations

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

structure Cvc.Typed.Solver.Heap [Ω] (solver : Solver) (α β : Type) : Type

The heap of a solver, at the Lean types of its locations and its data.

Produced by declareSepHeap, and the only way to Heap.pto or Heap.nil.

• untyped : Cvc.Untyped.Solver.Heap solver

def Cvc.Typed.Solver.Heap.toUntyped [Ω] {α β : Type} {solver : Solver} (h : solver.Heap α β) : Untyped.Solver.Heap solver

The sort-erased heap it wraps, which carries α and β as Srts; free.

Equations

• h.toUntyped = Cvc.Typed.Solver.Heap.untyped✝ h

@[reducible, inline]

abbrev Cvc.Typed.Solver.Heap.erase [Ω] {α β : Type} {solver : Solver} (h : solver.Heap α β) : Untyped.Solver.Heap solver

The sort-erased heap it wraps, which carries α and β as Srts; free.

Equations

• h.erase = h.toUntyped

def Cvc.Untyped.Solver.Heap.toTypedAs [Ω] (α β : Type) [ToTyp α] [ToTyp β] {solver : Typed.Solver} (h : Heap solver) : Env (solver.Heap α β)

Types a sort-erased heap at locations α and data β, checking its two sorts against theirs.

toTyped infers α and β from the expected type; typeCheckAs and typeCheck are the same two functions under the names that say what they do.

Equations

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

def Cvc.Untyped.Solver.Heap.toTyped [Ω] {α β : Type} [ToTyp α] [ToTyp β] {solver : Typed.Solver} (h : Heap solver) : Env (solver.Heap α β)

Types a sort-erased heap at locations α and data β, checking its two sorts against theirs.

toTyped infers α and β from the expected type; typeCheckAs and typeCheck are the same two functions under the names that say what they do.

Equations

• h.toTyped = Cvc.Untyped.Solver.Heap.toTypedAs α β h

@[reducible, inline]

abbrev Cvc.Untyped.Solver.Heap.typeCheckAs [Ω] (α β : Type) [ToTyp α] [ToTyp β] {solver : Typed.Solver} (h : Heap solver) : Env (solver.Heap α β)

Types a sort-erased heap at locations α and data β, checking its two sorts against theirs.

toTyped infers α and β from the expected type; typeCheckAs and typeCheck are the same two functions under the names that say what they do.

Equations

• @Cvc.Untyped.Solver.Heap.typeCheckAs = @Cvc.Untyped.Solver.Heap.toTypedAs

@[reducible, inline]

abbrev Cvc.Untyped.Solver.Heap.typeCheck [Ω] {α β : Type} [ToTyp α] [ToTyp β] {solver : Typed.Solver} (h : Heap solver) : Env (solver.Heap α β)

Types a sort-erased heap at locations α and data β, checking its two sorts against theirs.

toTyped infers α and β from the expected type; typeCheckAs and typeCheck are the same two functions under the names that say what they do.

Equations

• @Cvc.Untyped.Solver.Heap.typeCheck = @Cvc.Untyped.Solver.Heap.toTyped

def Cvc.Typed.Solver.declareSepHeap [Ω] (s : Solver) (α β : Type) [ToTyp α] [ToTyp β] : Env (s.Heap α β)

Declares the heap's location and data sorts, and answers the handle they are reached through.

cvc5 allows this once per solver, and rejects a second call even at the same sorts. It has to come before any separation-logic constraint: asserting one against an undeclared heap is an error.

Equations

• s.declareSepHeap α β = do let loc ← Cvc.Srt.of α let data ← Cvc.Srt.of β let __do_lift ← Cvc.Untyped.Solver.declareSepHeap s loc data pure { untyped := __do_lift }

def Cvc.Typed.Solver.Heap.sorts {α β : Type} [Ω] {s : Solver} (h : s.Heap α β) : Srt × Srt

The location sort and the data sort, in that order.

Equations

• h.sorts = (Cvc.Typed.Solver.Heap.untyped✝ h).sorts

def Cvc.Typed.Solver.Heap.nil {α β : Type} [Ω] {s : Solver} (h : s.Heap α β) : Env (Term α)

sep.nil, the null location, at the heap's location sort.

Equations

• h.nil = (Cvc.Typed.Solver.Heap.untyped✝ h).nil

def Cvc.Typed.Solver.Heap.pto {α β : Type} [Ω] {s : Solver} (h : s.Heap α β) (loc : Term α) (data : Term β) : Env (Term Bool)

The points-to constraint: loc points to data in a heap holding nothing else.

The operands are the heap's own indices, so the mismatch the sort-erased version has to check is not expressible here.

Equations

• h.pto loc data = (Cvc.Typed.Solver.Heap.untyped✝ h).pto loc.erase data.erase

Reading a heap back

Both answer a formula describing the model's heap rather than a value, so both are Term Bool whatever the heap's types.

def Cvc.Typed.Solver.getValueSepHeap [Ω] (s : Solver) : s.EnvSat (Term Bool)

A formula describing the model's heap, such as (pto (as @Loc_1 Loc) 0); not a value.

Equations

• s.getValueSepHeap = Cvc.Untyped.Solver.getValueSepHeap s

def Cvc.Typed.Solver.getValueSepNil [Ω] (s : Solver) : s.EnvSat (Term Bool)

A formula giving sep.nil in the model, such as (= (as sep.nil Loc) (as @Loc_0 Loc)).

Equations

• s.getValueSepNil = Cvc.Untyped.Solver.getValueSepNil s

def Cvc.Typed.Solver.getValueSepHeap! [Ω] (s : Solver) : Env (Term Bool)

getValueSepHeap in Env, not checked to follow a sat answer.

Equations

• s.getValueSepHeap! = Cvc.Untyped.Solver.getValueSepHeap! s

def Cvc.Typed.Solver.getValueSepNil! [Ω] (s : Solver) : Env (Term Bool)

getValueSepNil in Env, not checked to follow a sat answer.

Equations

• s.getValueSepNil! = Cvc.Untyped.Solver.getValueSepNil! s