Term Language

This file defines the term language the decision procedure operates on, and the denotation of these terms into operations on bitstreams

inductive AutoStructs.Term : Type

A Term is an expression in the language our decision procedure operates on, it represent an infinite bitstream (with free variables)

• var: ℕ → AutoStructs.Term
• zero: AutoStructs.Term

  The constant 0

• negOne: AutoStructs.Term

  The constant -1

• one: AutoStructs.Term

  The constant 1

• and: AutoStructs.Term → AutoStructs.Term → AutoStructs.Term

  Bitwise and

• or: AutoStructs.Term → AutoStructs.Term → AutoStructs.Term

  Bitwise or

• xor: AutoStructs.Term → AutoStructs.Term → AutoStructs.Term

  Bitwise xor

• not: AutoStructs.Term → AutoStructs.Term

  Bitwise complement

• add: AutoStructs.Term → AutoStructs.Term → AutoStructs.Term

  Addition

• sub: AutoStructs.Term → AutoStructs.Term → AutoStructs.Term

  Subtraction

• neg: AutoStructs.Term → AutoStructs.Term

  Negation

• incr: AutoStructs.Term → AutoStructs.Term

  Increment (i.e., add one)

• decr: AutoStructs.Term → AutoStructs.Term

  Decrement (i.e., subtract one)

instance AutoStructs.instReprTerm : Repr AutoStructs.Term

Equations

• AutoStructs.instReprTerm = { reprPrec := AutoStructs.reprTerm✝ }

instance AutoStructs.instInhabitedTerm : Inhabited AutoStructs.Term

Equations

• AutoStructs.instInhabitedTerm = { default := AutoStructs.Term.zero }

instance AutoStructs.instAddTerm : Add AutoStructs.Term

Equations

• AutoStructs.instAddTerm = { add := AutoStructs.Term.add }

instance AutoStructs.instSubTerm : Sub AutoStructs.Term

Equations

• AutoStructs.instSubTerm = { sub := AutoStructs.Term.sub }

instance AutoStructs.instOneTerm : One AutoStructs.Term

Equations

• AutoStructs.instOneTerm = { one := AutoStructs.Term.one }

instance AutoStructs.instZeroTerm : Zero AutoStructs.Term

Equations

• AutoStructs.instZeroTerm = { zero := AutoStructs.Term.zero }

instance AutoStructs.instNegTerm : Neg AutoStructs.Term

Equations

• AutoStructs.instNegTerm = { neg := AutoStructs.Term.neg }

def AutoStructs.Term.arity : AutoStructs.Term → ℕ

t.arity is the max free variable id that occurs in the given term t, and thus is an upper bound on the number of free variables that occur in t.

Note that the upper bound is not perfect: a term like var 10 only has a single free variable, but its arity will be 11

Equations

• (AutoStructs.Term.var n).arity = n + 1
• AutoStructs.Term.zero.arity = 0
• AutoStructs.Term.one.arity = 0
• AutoStructs.Term.negOne.arity = 0
• (t₁.and t₂).arity = max t₁.arity t₂.arity
• (t₁.or t₂).arity = max t₁.arity t₂.arity
• (t₁.xor t₂).arity = max t₁.arity t₂.arity
• t.not.arity = t.arity
• (t₁.add t₂).arity = max t₁.arity t₂.arity
• (t₁.sub t₂).arity = max t₁.arity t₂.arity
• t.neg.arity = t.arity
• t.incr.arity = t.arity
• t.decr.arity = t.arity

def AutoStructs.Term.evalFin {w : ℕ} (t : AutoStructs.Term) (vars : Fin t.arity → BitVec w) : BitVec w

Evaluate a term t to the BitVec it represents.

This differs from Term.eval in that Term.evalFin uses Term.arity to determine the number of free variables that occur in the given term, and only require that many bitstream values to be given in vars.

Equations

• (AutoStructs.Term.var n).evalFin vars_2 = vars_2 (Fin.last n)
• AutoStructs.Term.zero.evalFin vars_2 = BitVec.zero w
• AutoStructs.Term.one.evalFin vars_2 = 1
• AutoStructs.Term.negOne.evalFin vars_2 = -1
• (t₁.and t₂).evalFin vars_2 = (t₁.evalFin fun (i : Fin t₁.arity) => vars_2 (Fin.castLE ⋯ i)) &&& t₂.evalFin fun (i : Fin t₂.arity) => vars_2 (Fin.castLE ⋯ i)
• (t₁.or t₂).evalFin vars_2 = (t₁.evalFin fun (i : Fin t₁.arity) => vars_2 (Fin.castLE ⋯ i)) ||| t₂.evalFin fun (i : Fin t₂.arity) => vars_2 (Fin.castLE ⋯ i)
• (t₁.xor t₂).evalFin vars_2 = (t₁.evalFin fun (i : Fin t₁.arity) => vars_2 (Fin.castLE ⋯ i)) ^^^ t₂.evalFin fun (i : Fin t₂.arity) => vars_2 (Fin.castLE ⋯ i)
• t_2.not.evalFin vars_2 = ~~~t_2.evalFin vars_2
• (t₁.add t₂).evalFin vars_2 = (t₁.evalFin fun (i : Fin t₁.arity) => vars_2 (Fin.castLE ⋯ i)) + t₂.evalFin fun (i : Fin t₂.arity) => vars_2 (Fin.castLE ⋯ i)
• (t₁.sub t₂).evalFin vars_2 = (t₁.evalFin fun (i : Fin t₁.arity) => vars_2 (Fin.castLE ⋯ i)) - t₂.evalFin fun (i : Fin t₂.arity) => vars_2 (Fin.castLE ⋯ i)
• t_2.neg.evalFin vars_2 = -t_2.evalFin vars_2
• t_2.incr.evalFin vars_2 = t_2.evalFin vars_2 + 1
• t_2.decr.evalFin vars_2 = t_2.evalFin vars_2 - 1

def AutoStructs.Term.evalNat {w : ℕ} (t : AutoStructs.Term) (vars : ℕ → BitVec w) : BitVec w

Equations

• (AutoStructs.Term.var n).evalNat vars = vars ↑(Fin.last n)
• AutoStructs.Term.zero.evalNat vars = BitVec.zero w
• AutoStructs.Term.one.evalNat vars = 1
• AutoStructs.Term.negOne.evalNat vars = -1
• (t₁.and t₂).evalNat vars = t₁.evalNat vars &&& t₂.evalNat vars
• (t₁.or t₂).evalNat vars = t₁.evalNat vars ||| t₂.evalNat vars
• (t₁.xor t₂).evalNat vars = t₁.evalNat vars ^^^ t₂.evalNat vars
• t_1.not.evalNat vars = ~~~t_1.evalNat vars
• (t₁.add t₂).evalNat vars = t₁.evalNat vars + t₂.evalNat vars
• (t₁.sub t₂).evalNat vars = t₁.evalNat vars - t₂.evalNat vars
• t_1.neg.evalNat vars = -t_1.evalNat vars
• t_1.incr.evalNat vars = t_1.evalNat vars + 1
• t_1.decr.evalNat vars = t_1.evalNat vars - 1

def AutoStructs.Term.evalFinStream (t : AutoStructs.Term) (vars : Fin t.arity → BitStream) : BitStream

Equations

• (AutoStructs.Term.var n).evalFinStream vars_2 = vars_2 (Fin.last n)
• AutoStructs.Term.zero.evalFinStream vars_2 = BitStream.zero
• AutoStructs.Term.one.evalFinStream vars_2 = BitStream.one
• AutoStructs.Term.negOne.evalFinStream vars_2 = BitStream.negOne
• (t₁.and t₂).evalFinStream vars_2 = (t₁.evalFinStream fun (i : Fin t₁.arity) => vars_2 (Fin.castLE ⋯ i)) &&& t₂.evalFinStream fun (i : Fin t₂.arity) => vars_2 (Fin.castLE ⋯ i)
• (t₁.or t₂).evalFinStream vars_2 = (t₁.evalFinStream fun (i : Fin t₁.arity) => vars_2 (Fin.castLE ⋯ i)) ||| t₂.evalFinStream fun (i : Fin t₂.arity) => vars_2 (Fin.castLE ⋯ i)
• (t₁.xor t₂).evalFinStream vars_2 = (t₁.evalFinStream fun (i : Fin t₁.arity) => vars_2 (Fin.castLE ⋯ i)) ^^^ t₂.evalFinStream fun (i : Fin t₂.arity) => vars_2 (Fin.castLE ⋯ i)
• t_2.not.evalFinStream vars_2 = ~~~t_2.evalFinStream vars_2
• (t₁.add t₂).evalFinStream vars_2 = (t₁.evalFinStream fun (i : Fin t₁.arity) => vars_2 (Fin.castLE ⋯ i)) + t₂.evalFinStream fun (i : Fin t₂.arity) => vars_2 (Fin.castLE ⋯ i)
• (t₁.sub t₂).evalFinStream vars_2 = (t₁.evalFinStream fun (i : Fin t₁.arity) => vars_2 (Fin.castLE ⋯ i)) - t₂.evalFinStream fun (i : Fin t₂.arity) => vars_2 (Fin.castLE ⋯ i)
• t_2.neg.evalFinStream vars_2 = -t_2.evalFinStream vars_2
• t_2.incr.evalFinStream vars_2 = (t_2.evalFinStream vars_2).incr
• t_2.decr.evalFinStream vars_2 = (t_2.evalFinStream vars_2).decr

inductive AutoStructs.RelationOrdering : Type

• lt: AutoStructs.RelationOrdering
• le: AutoStructs.RelationOrdering
• gt: AutoStructs.RelationOrdering
• ge: AutoStructs.RelationOrdering

instance AutoStructs.instReprRelationOrdering : Repr AutoStructs.RelationOrdering

Equations

• AutoStructs.instReprRelationOrdering = { reprPrec := AutoStructs.reprRelationOrdering✝ }

inductive AutoStructs.Relation : Type

• eq: AutoStructs.Relation
• signed: AutoStructs.RelationOrdering → AutoStructs.Relation
• unsigned: AutoStructs.RelationOrdering → AutoStructs.Relation

instance AutoStructs.instReprRelation : Repr AutoStructs.Relation

Equations

• AutoStructs.instReprRelation = { reprPrec := AutoStructs.reprRelation✝ }

def AutoStructs.evalRelation {w : ℕ} (rel : AutoStructs.Relation) (bv1 : BitVec w) (bv2 : BitVec w) : Bool

Equations

• AutoStructs.evalRelation AutoStructs.Relation.eq bv1 bv2 = decide (bv1 = bv2)
• AutoStructs.evalRelation (AutoStructs.Relation.signed AutoStructs.RelationOrdering.lt) bv1 bv2 = (bv2 >ₛ bv1)
• AutoStructs.evalRelation (AutoStructs.Relation.signed AutoStructs.RelationOrdering.le) bv1 bv2 = (bv2 ≥ₛ bv1)
• AutoStructs.evalRelation (AutoStructs.Relation.signed AutoStructs.RelationOrdering.gt) bv1 bv2 = (bv1 >ₛ bv2)
• AutoStructs.evalRelation (AutoStructs.Relation.signed AutoStructs.RelationOrdering.ge) bv1 bv2 = (bv1 ≥ₛ bv2)
• AutoStructs.evalRelation (AutoStructs.Relation.unsigned AutoStructs.RelationOrdering.lt) bv1 bv2 = (bv2 >ᵤ bv1)
• AutoStructs.evalRelation (AutoStructs.Relation.unsigned AutoStructs.RelationOrdering.le) bv1 bv2 = (bv2 ≥ᵤ bv1)
• AutoStructs.evalRelation (AutoStructs.Relation.unsigned AutoStructs.RelationOrdering.gt) bv1 bv2 = (bv1 >ᵤ bv2)
• AutoStructs.evalRelation (AutoStructs.Relation.unsigned AutoStructs.RelationOrdering.ge) bv1 bv2 = (bv1 ≥ᵤ bv2)

inductive AutoStructs.Binop : Type

• and: AutoStructs.Binop
• or: AutoStructs.Binop
• impl: AutoStructs.Binop
• equiv: AutoStructs.Binop

instance AutoStructs.instReprBinop : Repr AutoStructs.Binop

Equations

• AutoStructs.instReprBinop = { reprPrec := AutoStructs.reprBinop✝ }

def AutoStructs.evalBinop (op : AutoStructs.Binop) (b1 : Bool) (b2 : Bool) : Bool

Equations

• AutoStructs.evalBinop AutoStructs.Binop.and b1 b2 = (b1 && b2)
• AutoStructs.evalBinop AutoStructs.Binop.or b1 b2 = (b1 || b2)
• AutoStructs.evalBinop AutoStructs.Binop.impl b1 b2 = decide (b1 = true → b2 = true)
• AutoStructs.evalBinop AutoStructs.Binop.equiv b1 b2 = decide (b1 = true ↔ b2 = true)

def AutoStructs.evalBinop' (op : AutoStructs.Binop) (b1 : Prop) (b2 : Prop) : Prop

Equations

• AutoStructs.evalBinop' AutoStructs.Binop.and b1 b2 = (b1 ∧ b2)
• AutoStructs.evalBinop' AutoStructs.Binop.or b1 b2 = (b1 ∨ b2)
• AutoStructs.evalBinop' AutoStructs.Binop.impl b1 b2 = (b1 → b2)
• AutoStructs.evalBinop' AutoStructs.Binop.equiv b1 b2 = (b1 ↔ b2)

inductive AutoStructs.Unop : Type

• neg: AutoStructs.Unop

instance AutoStructs.instReprUnop : Repr AutoStructs.Unop

Equations

• AutoStructs.instReprUnop = { reprPrec := AutoStructs.reprUnop✝ }

inductive AutoStructs.Formula : Type

• atom: AutoStructs.Relation → AutoStructs.Term → AutoStructs.Term → AutoStructs.Formula
• msbSet: AutoStructs.Term → AutoStructs.Formula
• unop: AutoStructs.Unop → AutoStructs.Formula → AutoStructs.Formula
• binop: AutoStructs.Binop → AutoStructs.Formula → AutoStructs.Formula → AutoStructs.Formula

instance AutoStructs.instReprFormula : Repr AutoStructs.Formula

Equations

• AutoStructs.instReprFormula = { reprPrec := AutoStructs.reprFormula✝ }

instance AutoStructs.instInhabitedFormula : Inhabited AutoStructs.Formula

Equations

• AutoStructs.instInhabitedFormula = { default := AutoStructs.Formula.msbSet default }

def AutoStructs.Formula.arity : AutoStructs.Formula → ℕ

Equations

• (AutoStructs.Formula.atom a a_1 a_2).arity = max a_1.arity a_2.arity
• (AutoStructs.Formula.msbSet a).arity = a.arity
• (AutoStructs.Formula.unop a a_1).arity = a_1.arity
• (AutoStructs.Formula.binop a a_1 a_2).arity = max a_1.arity a_2.arity

def AutoStructs.Formula.sat {w : ℕ} (φ : AutoStructs.Formula) (ρ : Fin φ.arity → BitVec w) : Bool

Equations

• One or more equations did not get rendered due to their size.
• (AutoStructs.Formula.unop AutoStructs.Unop.neg φ_2).sat ρ_2 = !φ_2.sat ρ_2
• (AutoStructs.Formula.binop op φ1 φ2).sat ρ_2 = AutoStructs.evalBinop op (φ1.sat fun (n : Fin φ1.arity) => ρ_2 (Fin.castLE ⋯ n)) (φ2.sat fun (n : Fin φ2.arity) => ρ_2 (Fin.castLE ⋯ n))
• (AutoStructs.Formula.msbSet t).sat ρ_2 = (t.evalFin ρ_2).msb

def AutoStructs.Formula.sat' {w : ℕ} (φ : AutoStructs.Formula) (ρ : ℕ → BitVec w) : Prop

Equations

• (AutoStructs.Formula.atom rel t1 t2).sat' ρ = (AutoStructs.evalRelation rel (t1.evalNat ρ) (t2.evalNat ρ) = true)
• (AutoStructs.Formula.unop AutoStructs.Unop.neg φ_2).sat' ρ = ¬φ_2.sat' ρ
• (AutoStructs.Formula.binop op φ1 φ2).sat' ρ = AutoStructs.evalBinop' op (φ1.sat' ρ) (φ2.sat' ρ)
• (AutoStructs.Formula.msbSet t).sat' ρ = ((t.evalNat ρ).msb = true)

@[reducible, inline]

abbrev AutoStructs.envOfArray {w : ℕ} (a : Array (BitVec w)) : ℕ → BitVec w

Equations

• AutoStructs.envOfArray a n = a.getD n 0

@[reducible, inline]

abbrev AutoStructs.envOfList {w : ℕ} (a : List (BitVec w)) : ℕ → BitVec w

Equations

• AutoStructs.envOfList a n = a.getD n 0