The cvc5 types for terms, sorts, solvers, etc. are all related to a notion of (term) manager responsible for allocating and indexing terms and sorts. These types cannot interact and will produce a runtime error if they do not agree on their manager.
Ω
This API abstracts away the term manager completely and enforces manager-consistency statically using a type-class called Ω. Virtually all types in this library have an implicit Ω argument that can be thought of as representing a specific term manager. On the sort type for instance:
#check Srt
An instance costs nothing at runtime, and you cannot build one yourself: running an environment provides it, as described below.
The current scope: an instance stands for one term manager.
Only Env.run and its variants make one, so a sort, term or solver cannot leave the run it was
made in, nor meet one made in another run, nested runs included.
Ω is tied to cvc.lean's environment monad Env: Env α, or more precisely @Env inst α where (inst : Ω), corresponds to code that uses a specific term manager to produce a value of type α.
Cvc5's term manager handles term/sort perfect sharingMarginal noteAlso known as hash-consing: building the same term twice produces the same (reference to the same) term, meaning physical (reference) equality is structural equality..
The first problem Ω and Env solve is that manipulating a value v tied to manager m after m has been freed is unsafe as freeing m frees v, so v should only live as long as m is alive. So most features in this library produce an Env _ output.
Second, as mentioned above, values tied to different managers should never interact as that would cause a runtime error. By encoding a specific term manager through an Ω-value, cvc.lean can type-check that sorts/terms/solvers/etc. are compatible by making sure they agree on their Ω-value.
For example, the function building an array-sort makes sure the index and element sorts agree on their manager, and keeps track of the manager associated to the resulting sort by having all of them agree on their Ω.
Most functions in this library are in the Env monad, built on top of the EnvT monad transformer.
#check EnvT
Be careful that, in practice, EnvT works on monads that lift BaseIO so that it can call the cvc5 C++ API.Marginal noteAlso for maintaining its state efficiently as a mutable reference. Env is simply EnvT BaseIO.
The only way to run Env-code is through its run-like functions. The simplest one is Env.run and produces a BaseIO (Res α) where Res is Except specialized to cvc.lean's Error type.
#check Env.run
Notice that this function quantifies the Ω-instance inst for code. This guarantees that whatever α is, it cannot mention inst in any way, so it is not possible for code to return, say, an Srt-value as it would require inst to escape its scope.Marginal noteThis design is heavily inspired by Lean's ST/ST.Ref.
Now, to manipulate Env or virtually any type from cvc.lean we need to have an Ω-instance in scope. We could have [Ω] as an argument of all our definitions, but it is often easier to have it as a variable.
variable [Ω]
We can now forget about Ω completely and write a few Srt-using Env functions:Marginal noteThe only time you should be reminded of Ω is when you are doing something memory-unsafe such as mixing terms/sorts/solvers.
def mkArrayBoolTo (srt : Srt) : Env Srt := do
srt.arrayFrom (← Srt.bool)
def codeInEnv : Env Unit := do
let real ← Srt.real
let array ← mkArrayBoolTo real
println! "array sort := {array}"
Next we can use Env.run to actually run this code.
def test1 : IO Unit := do
match ← Env.run codeInEnv with
| .ok () => println! "success"
| .error e => println! "an error occurred:\n{e}"
#eval test1
Running with Env.runIO lifts cvc.lean's errors to IO and makes this simple test much more straightforward.
#eval Env.runIO codeInEnv
Using a cvc.lean type after its manager has been freed is rejected due to the quantification of the Ω instance. While this guarantees no use-after-free, the error message is a regular lean type-error and its meaning is pretty obscure.
def mkSort : Env Srt := Srt.int
#eval do
let sortWithDeadTermManager ← Env.runIO mkSort
println! "dangling pointer: {sortWithDeadTermManager}"
The note closing the message comes from Lean and can be ignored: every sort error of this kind carries it.
Using a sort in an environment different from its native one is also a type error.
def mkBoolSort : Env Srt := Srt.bool
#eval Env.runIO do
-- let's call `ω` the current environment
let int ← Srt.int
Env.runIO do
-- we're now in a different environment `ω'`
let bool ← mkBoolSort
let array ← int.arrayTo bool