Documentation

Strata.DL.SMT.Term

Based on Cedar's Term language. (https://github.com/cedar-policy/cedar-spec/blob/main/cedar-lean/Cedar/SymCC/Term.lean) This file defines the Term language, a strongly and simply typed IR. The Term language has a straightforward translation to SMTLib. It is designed to reduce the semantic gap between Strata and SMTLib, and to faciliate proofs of soundness and completeness of the symbolic evaluator. Additionally, it allows us to generate different SMT encodings for different solvers (e.g., CVC5's theory of finite sets vs Z3's theory of Arrays).

Terms should not be created directly using Term constructors. Instead, they should be created using the factory functions defined in Factory.lean. The factory functions check the types of their arguments, perform optimizations, and ensure that applying them to well-formed terms results in well-formed terms.

See TermType.lean and Op.lean for definition of Term types and operators.

inductive Strata.SMT.TermPrim :

bool : Bool → TermPrim
int : Int → TermPrim
real : Decimal → TermPrim
bitvec {n : Nat} : BitVec n → TermPrim
string : String → TermPrim

Instances For

instance Strata.SMT.instReprTermPrim :

Equations

Strata.SMT.instReprTermPrim = { reprPrec := Strata.SMT.instReprTermPrim.repr }

def Strata.SMT.instReprTermPrim.repr :

TermPrim → Nat → Std.Format

Equations

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

Instances For

def Strata.SMT.instInhabitedTermPrim.default :

Equations

Strata.SMT.instInhabitedTermPrim.default = Strata.SMT.TermPrim.bool default

Instances For

instance Strata.SMT.instInhabitedTermPrim :

Inhabited TermPrim

Equations

Strata.SMT.instInhabitedTermPrim = { default := Strata.SMT.instInhabitedTermPrim.default }

def Strata.SMT.instDecidableEqTermPrim.decEq (x✝ x✝¹ : TermPrim) :

Decidable (x✝ = x✝¹)

Equations

One or more equations did not get rendered due to their size.
Strata.SMT.instDecidableEqTermPrim.decEq (Strata.SMT.TermPrim.bool a) (Strata.SMT.TermPrim.bool b) = if h : a = b then h ▸ isTrue ⋯ else isFalse ⋯
Strata.SMT.instDecidableEqTermPrim.decEq (Strata.SMT.TermPrim.bool a) (Strata.SMT.TermPrim.int a_1) = isFalse ⋯
Strata.SMT.instDecidableEqTermPrim.decEq (Strata.SMT.TermPrim.bool a) (Strata.SMT.TermPrim.real a_1) = isFalse ⋯
Strata.SMT.instDecidableEqTermPrim.decEq (Strata.SMT.TermPrim.bool a) (Strata.SMT.TermPrim.bitvec a_1) = isFalse ⋯
Strata.SMT.instDecidableEqTermPrim.decEq (Strata.SMT.TermPrim.bool a) (Strata.SMT.TermPrim.string a_1) = isFalse ⋯
Strata.SMT.instDecidableEqTermPrim.decEq (Strata.SMT.TermPrim.int a) (Strata.SMT.TermPrim.bool a_1) = isFalse ⋯
Strata.SMT.instDecidableEqTermPrim.decEq (Strata.SMT.TermPrim.int a) (Strata.SMT.TermPrim.int b) = if h : a = b then h ▸ isTrue ⋯ else isFalse ⋯
Strata.SMT.instDecidableEqTermPrim.decEq (Strata.SMT.TermPrim.int a) (Strata.SMT.TermPrim.real a_1) = isFalse ⋯
Strata.SMT.instDecidableEqTermPrim.decEq (Strata.SMT.TermPrim.int a) (Strata.SMT.TermPrim.bitvec a_1) = isFalse ⋯
Strata.SMT.instDecidableEqTermPrim.decEq (Strata.SMT.TermPrim.int a) (Strata.SMT.TermPrim.string a_1) = isFalse ⋯
Strata.SMT.instDecidableEqTermPrim.decEq (Strata.SMT.TermPrim.real a) (Strata.SMT.TermPrim.bool a_1) = isFalse ⋯
Strata.SMT.instDecidableEqTermPrim.decEq (Strata.SMT.TermPrim.real a) (Strata.SMT.TermPrim.int a_1) = isFalse ⋯
Strata.SMT.instDecidableEqTermPrim.decEq (Strata.SMT.TermPrim.real a) (Strata.SMT.TermPrim.real b) = if h : a = b then h ▸ isTrue ⋯ else isFalse ⋯
Strata.SMT.instDecidableEqTermPrim.decEq (Strata.SMT.TermPrim.real a) (Strata.SMT.TermPrim.bitvec a_1) = isFalse ⋯
Strata.SMT.instDecidableEqTermPrim.decEq (Strata.SMT.TermPrim.real a) (Strata.SMT.TermPrim.string a_1) = isFalse ⋯
Strata.SMT.instDecidableEqTermPrim.decEq (Strata.SMT.TermPrim.bitvec a) (Strata.SMT.TermPrim.bool a_1) = isFalse ⋯
Strata.SMT.instDecidableEqTermPrim.decEq (Strata.SMT.TermPrim.bitvec a) (Strata.SMT.TermPrim.int a_1) = isFalse ⋯
Strata.SMT.instDecidableEqTermPrim.decEq (Strata.SMT.TermPrim.bitvec a) (Strata.SMT.TermPrim.real a_1) = isFalse ⋯
Strata.SMT.instDecidableEqTermPrim.decEq (Strata.SMT.TermPrim.bitvec a) (Strata.SMT.TermPrim.string a_1) = isFalse ⋯
Strata.SMT.instDecidableEqTermPrim.decEq (Strata.SMT.TermPrim.string a) (Strata.SMT.TermPrim.bool a_1) = isFalse ⋯
Strata.SMT.instDecidableEqTermPrim.decEq (Strata.SMT.TermPrim.string a) (Strata.SMT.TermPrim.int a_1) = isFalse ⋯
Strata.SMT.instDecidableEqTermPrim.decEq (Strata.SMT.TermPrim.string a) (Strata.SMT.TermPrim.real a_1) = isFalse ⋯
Strata.SMT.instDecidableEqTermPrim.decEq (Strata.SMT.TermPrim.string a) (Strata.SMT.TermPrim.bitvec a_1) = isFalse ⋯
Strata.SMT.instDecidableEqTermPrim.decEq (Strata.SMT.TermPrim.string a) (Strata.SMT.TermPrim.string b) = if h : a = b then h ▸ isTrue ⋯ else isFalse ⋯

Instances For

instance Strata.SMT.instDecidableEqTermPrim :

DecidableEq TermPrim

Equations

Strata.SMT.instDecidableEqTermPrim = Strata.SMT.instDecidableEqTermPrim.decEq

def Strata.SMT.TermPrim.mkName :

TermPrim → String

Equations

(Strata.SMT.TermPrim.bool a).mkName = "bool"
(Strata.SMT.TermPrim.int a).mkName = "int"
(Strata.SMT.TermPrim.real a).mkName = "real"
(Strata.SMT.TermPrim.bitvec a_1).mkName = "bitvec"
(Strata.SMT.TermPrim.string a).mkName = "string"

Instances For

def Strata.SMT.TermPrim.lt :

TermPrim → TermPrim → Bool

Equations

(Strata.SMT.TermPrim.bool b₁).lt (Strata.SMT.TermPrim.bool b₂) = decide (b₁ < b₂)
(Strata.SMT.TermPrim.int i₁).lt (Strata.SMT.TermPrim.int i₂) = decide (i₁ < i₂)
(Strata.SMT.TermPrim.real r₁).lt (Strata.SMT.TermPrim.real r₂) = decide (r₁.toRat < r₂.toRat)
(Strata.SMT.TermPrim.bitvec bv₁).lt (Strata.SMT.TermPrim.bitvec bv₂) = (decide (n₁ < n₂) || decide (n₁ = n₂) && decide (bv₁.toNat < bv₂.toNat))
(Strata.SMT.TermPrim.string s₁).lt (Strata.SMT.TermPrim.string s₂) = decide (s₁ < s₂)
x✝¹.lt x✝ = decide (x✝¹.mkName < x✝.mkName)

Instances For

instance Strata.SMT.instLTTermPrim :

Equations

Strata.SMT.instLTTermPrim = { lt := fun (x y : Strata.SMT.TermPrim) => x.lt y = true }

instance Strata.SMT.TermPrim.decLt (x y : TermPrim) :

Decidable (x < y)

Equations

x.decLt y = if h : x.lt y = true then isTrue h else isFalse h

inductive Strata.SMT.QuantifierKind :

all : QuantifierKind
exist : QuantifierKind

Instances For

instance Strata.SMT.instReprQuantifierKind :

Repr QuantifierKind

Equations

Strata.SMT.instReprQuantifierKind = { reprPrec := Strata.SMT.instReprQuantifierKind.repr }

def Strata.SMT.instReprQuantifierKind.repr :

QuantifierKind → Nat → Std.Format

Equations

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

Instances For

instance Strata.SMT.instDecidableEqQuantifierKind :

DecidableEq QuantifierKind

Equations

Strata.SMT.instDecidableEqQuantifierKind x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

instance Strata.SMT.instHashableQuantifierKind :

Hashable QuantifierKind

Equations

Strata.SMT.instHashableQuantifierKind = { hash := Strata.SMT.instHashableQuantifierKind.hash }

def Strata.SMT.instHashableQuantifierKind.hash :

QuantifierKind → UInt64

Equations

Instances For

inductive Strata.SMT.Term :

prim : TermPrim → Term
var : TermVar → Term
none : TermType → Term
some : Term → Term
app : Op → (args : List Term) → (retTy : TermType) → Term
quant : QuantifierKind → (args : List TermVar) → (tr body : Term) → Term

Instances For

partial def Strata.SMT.instReprTerm.repr :

Term → Nat → Std.Format

instance Strata.SMT.instReprTerm :

Equations

Strata.SMT.instReprTerm = { reprPrec := Strata.SMT.instReprTerm.repr }

instance Strata.SMT.instInhabitedTerm :

Equations

Strata.SMT.instInhabitedTerm = { default := Strata.SMT.instInhabitedTerm.default }

def Strata.SMT.instInhabitedTerm.default :

Equations

Strata.SMT.instInhabitedTerm.default = Strata.SMT.Term.prim default

Instances For

def Strata.SMT.Term.isVar (t : Term) :

Equations

(Strata.SMT.Term.var a).isVar = true
t.isVar = false

Instances For

def Strata.SMT.Term.hasDecEq (t t' : Term) :

Decidable (t = t')

Equations

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

Instances For

def Strata.SMT.Term.hasListDec (ts₁ ts₂ : List Term) :

Decidable (ts₁ = ts₂)

Equations

One or more equations did not get rendered due to their size.
Strata.SMT.Term.hasListDec [] [] = isTrue Strata.SMT.Term.hasDecEq._proof_54
Strata.SMT.Term.hasListDec (head :: tail) [] = isFalse ⋯
Strata.SMT.Term.hasListDec [] (head :: tail) = isFalse ⋯

Instances For

instance Strata.SMT.instDecidableEqTerm :

DecidableEq Term

Equations

Strata.SMT.instDecidableEqTerm = Strata.SMT.Term.hasDecEq

def Strata.SMT.hashTerm (t : Term) :

Equations

Strata.SMT.hashTerm (Strata.SMT.Term.prim a) = 2
Strata.SMT.hashTerm (Strata.SMT.Term.var a) = 3
Strata.SMT.hashTerm (Strata.SMT.Term.none a) = 5
Strata.SMT.hashTerm a.some = 7
Strata.SMT.hashTerm (Strata.SMT.Term.app a a_1 a_2) = 11 * hash a * hash a_2
Strata.SMT.hashTerm (Strata.SMT.Term.quant a a_1 a_2 a_3) = 13 * hash a * hash a_1

Instances For

instance Strata.SMT.instHashableTerm :

Equations

Strata.SMT.instHashableTerm = { hash := Strata.SMT.hashTerm }

def Strata.SMT.Term.mkName :

Term → String

Equations

(Strata.SMT.Term.prim a).mkName = "prim"
(Strata.SMT.Term.var a).mkName = "var"
(Strata.SMT.Term.none a).mkName = "none"
a.some.mkName = "some"
(Strata.SMT.Term.app a args retTy).mkName = "app"
(Strata.SMT.Term.quant Strata.SMT.QuantifierKind.all args tr body).mkName = "all"
(Strata.SMT.Term.quant Strata.SMT.QuantifierKind.exist args tr body).mkName = "exists"

Instances For

@[irreducible]

def Strata.SMT.Term.lt :

Term → Term → Bool

Equations

One or more equations did not get rendered due to their size.
(Strata.SMT.Term.prim p₁).lt (Strata.SMT.Term.prim p₂) = decide (p₁ < p₂)
(Strata.SMT.Term.var v₁).lt (Strata.SMT.Term.var v₂) = decide (v₁ < v₂)
(Strata.SMT.Term.none ty₁).lt (Strata.SMT.Term.none ty₂) = decide (ty₁ < ty₂)
t₁.some.lt t₂.some = t₁.lt t₂
x✝¹.lt x✝ = decide (x✝¹.mkName < x✝.mkName)

Instances For

@[irreducible]

def Strata.SMT.Term.ltList :

List Term → List Term → Bool

Equations

Strata.SMT.Term.ltList [] [] = false
Strata.SMT.Term.ltList [] (head :: tail) = true
Strata.SMT.Term.ltList (head :: tail) [] = false
Strata.SMT.Term.ltList (t₁ :: ts₁) (t₂ :: ts₂) = (t₁.lt t₂ || decide (t₁ = t₂) && Strata.SMT.Term.ltList ts₁ ts₂)

Instances For

instance Strata.SMT.instLTTerm :

Equations

Strata.SMT.instLTTerm = { lt := fun (x y : Strata.SMT.Term) => x.lt y = true }

instance Strata.SMT.Term.decLt (x y : Term) :

Decidable (x < y)

Equations

x.decLt y = if h : x.lt y = true then isTrue h else isFalse h

@[reducible, inline]

abbrev Strata.SMT.Term.bool (b : Bool) :

Equations

Strata.SMT.Term.bool b = Strata.SMT.Term.prim (Strata.SMT.TermPrim.bool b)

Instances For

@[reducible, inline]

abbrev Strata.SMT.Term.int (i : Int) :

Equations

Strata.SMT.Term.int i = Strata.SMT.Term.prim (Strata.SMT.TermPrim.int i)

Instances For

@[reducible, inline]

abbrev Strata.SMT.Term.real (r : Decimal) :

Equations

Strata.SMT.Term.real r = Strata.SMT.Term.prim (Strata.SMT.TermPrim.real r)

Instances For

@[reducible, inline]

abbrev Strata.SMT.Term.bitvec {n : Nat} (bv : BitVec n) :

Equations

Strata.SMT.Term.bitvec bv = Strata.SMT.Term.prim (Strata.SMT.TermPrim.bitvec bv)

Instances For

@[reducible, inline]

abbrev Strata.SMT.Term.string (s : String) :

Equations

Strata.SMT.Term.string s = Strata.SMT.Term.prim (Strata.SMT.TermPrim.string s)

Instances For

def Strata.SMT.TermPrim.typeOf :

TermPrim → TermType

Equations

Instances For

def Strata.SMT.Term.typeOf :

Term → TermType

Equations

(Strata.SMT.Term.prim a).typeOf = a.typeOf
(Strata.SMT.Term.var a).typeOf = a.ty
(Strata.SMT.Term.none a).typeOf = a.option
a.some.typeOf = a.typeOf.option
(Strata.SMT.Term.app a a_1 a_2).typeOf = a_2
(Strata.SMT.Term.quant a a_1 a_2 a_3).typeOf = Strata.SMT.TermType.bool

Instances For

def Strata.SMT.Term.isLiteral :

Equations

(Strata.SMT.Term.prim a).isLiteral = true
(Strata.SMT.Term.none a).isLiteral = true
t.some.isLiteral = t.isLiteral
x✝.isLiteral = false

Instances For

instance Strata.SMT.instCoeBoolTerm :

Equations

Strata.SMT.instCoeBoolTerm = { coe := fun (b : Bool) => Strata.SMT.Term.prim (Strata.SMT.TermPrim.bool b) }

instance Strata.SMT.instCoeIntTerm :

Equations

Strata.SMT.instCoeIntTerm = { coe := fun (i : Int) => Strata.SMT.Term.prim (Strata.SMT.TermPrim.int i) }

instance Strata.SMT.instCoeInt64Term :

Equations

Strata.SMT.instCoeInt64Term = { coe := fun (i : Int64) => Strata.SMT.Term.prim (Strata.SMT.TermPrim.bitvec i.toBitVec) }

instance Strata.SMT.instCoeOutBitVecTerm {n : Nat} :

CoeOut (BitVec n) Term

Equations

Strata.SMT.instCoeOutBitVecTerm = { coe := fun (b : BitVec n) => Strata.SMT.Term.prim (Strata.SMT.TermPrim.bitvec b) }

instance Strata.SMT.instCoeStringTerm :

Coe String Term

Equations

Strata.SMT.instCoeStringTerm = { coe := fun (s : String) => Strata.SMT.Term.prim (Strata.SMT.TermPrim.string s) }

instance Strata.SMT.instCoeTermVarTerm :

Coe TermVar Term

Equations

Strata.SMT.instCoeTermVarTerm = { coe := fun (v : Strata.SMT.TermVar) => Strata.SMT.Term.var v }