Separation logic, sort-erased

The whole theory lives here, the solver functions included: a separation-logic term's well-formedness depends on the heap a solver declared, not only on its operands.

The heap is declared, and everything hangs off that

Solver.declareSepHeap fixes the heap's location and data sorts, once per solver, and cvc5 checks nothing else against them: (pto 1 true) is built without complaint against a heap of Loc × Int and fails only at check-sat, reporting a type error about set.union — cvc5's internal encoding showing through.

So declareSepHeap answers a handle, and the two heap-dependent constructors hang off it:

• Heap.pto, which checks its operands against the sorts the handle carries;
• Heap.nil, which builds sep.nil at the heap's location sort rather than at any sort a caller might name.

The handle is indexed by the solver that produced it: two solvers of one scope may declare different heaps.

sepEmp, sepStar and sepWand mention no heap sort, so they need no handle. None of these operators is lifted over nullables.

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

Separating implication, the magic wand.

Equations

• lft.sepWand rgt = Cvc.runUnsafe✝ fun (tm : cvc5.TermManager) => tm.mkTerm cvc5.Kind.SEP_WAND #[lft, rgt]

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

sepStar over two or more terms.

Equations

• Cvc.Untyped.Term.sepStarN terms atLeastTwoElements = Cvc.runUnsafe✝ fun (tm : cvc5.TermManager) => tm.mkTerm cvc5.Kind.SEP_STAR terms

def Cvc.Untyped.Term.sepEmp [Ω] : Env Term

Holds exactly when the heap is empty.

Equations

• Cvc.Untyped.Term.sepEmp = Cvc.runUnsafe✝ fun (tm : cvc5.TermManager) => tm.mkSepEmp

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

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

Equations

• lft.sepStar rgt = Cvc.runUnsafe✝ fun (tm : cvc5.TermManager) => tm.mkTerm cvc5.Kind.SEP_STAR #[lft, rgt]

inductive Cvc.Untyped.View.Sep [Ω] : Type

Sep's operators, taken apart one level, sort-erased.

• sepEmp [Ω] : View.Sep

  Holds exactly when the heap is empty.

• sepStar [Ω] (kids : Kids) : View.Sep

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

  kids holds every operand, two or more.

• sepWand [Ω] (lft rgt : Term) : View.Sep

  Separating implication, the magic wand.

def Cvc.Untyped.View.Sep.of? [Ω] (viewed : Term) : Option View.Sep

Takes a term apart one level, if Sep owns its operator.

Equations

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

structure Cvc.Untyped.Solver.Heap [Ω] (solver : Solver) : Type

The heap of a solver, and the sorts it was declared at.

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

• loc : Srt

  Sort of the heap's locations.

• data : Srt

  Sort of the data a location points to.

def Cvc.Untyped.Solver.instBEqHeap.beq {inst✝ : Ω} {solver✝ : Solver} : solver✝.Heap → solver✝.Heap → Bool

Equations

• Cvc.Untyped.Solver.instBEqHeap.beq { loc := a, data := a_1 } { loc := b, data := b_1 } = (a == b && a_1 == b_1)
• Cvc.Untyped.Solver.instBEqHeap.beq x✝¹ x✝ = false

@[instance_reducible]

instance Cvc.Untyped.Solver.instBEqHeap {inst✝ : Ω} {solver✝ : Solver} : BEq solver✝.Heap

Equations

• Cvc.Untyped.Solver.instBEqHeap = { beq := Cvc.Untyped.Solver.instBEqHeap.beq }

def Cvc.Untyped.Solver.declareSepHeap [Ω] (s : Solver) (loc data : Srt) : 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 loc data = do Cvc.runUnsafe'✝ ((Cvc.Untyped.Solver.toUnsafe✝ s).declareSepHeap loc data) pure { loc := loc, data := data }

def Cvc.Untyped.Solver.Heap.sorts [Ω] {s : Solver} (h : s.Heap) : Srt × Srt

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

Equations

• h.sorts = (h.loc, h.data)

def Cvc.Untyped.Solver.Heap.nil [Ω] {s : Solver} (h : s.Heap) : Env Term

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

Equations

• h.nil = Cvc.runUnsafe✝ fun (tm : cvc5.TermManager) => tm.mkSepNil h.loc

def Cvc.Untyped.Solver.Heap.pto [Ω] {s : Solver} (h : s.Heap) (loc data : Term) : Env Term

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

The operands are checked against the sorts the heap was declared at, which cvc5 does not do until check-sat — and then reports as a set.union type error naming neither pto nor the heap.

Equations

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

Reading a heap back

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

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

Equations

• s.getValueSepHeap = liftM (Cvc.runUnsafe'✝ (Cvc.Untyped.Solver.toUnsafe✝ s).getValueSepHeap)

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

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

Equations

• s.getValueSepNil = liftM (Cvc.runUnsafe'✝ (Cvc.Untyped.Solver.toUnsafe✝ s).getValueSepNil)

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

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

Equations

• s.getValueSepHeap! = Cvc.Untyped.Solver.EnvSatT.toEnv✝ s.getValueSepHeap

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

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

Equations

• s.getValueSepNil! = Cvc.Untyped.Solver.EnvSatT.toEnv✝ s.getValueSepNil