Term Language

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

inductive Term : Type

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

• var: ℕ → Term
• zero: Term

  The constant 0

• negOne: Term

  The constant -1

• one: Term

  The constant 1

• and: Term → Term → Term

  Bitwise and

• or: Term → Term → Term

  Bitwise or

• xor: Term → Term → Term

  Bitwise xor

• not: Term → Term

  Bitwise complement

• ls: Bool → Term → Term

  Append a single bit the start (i.e., least-significant end) of the bitstream

• add: Term → Term → Term

  Addition

• sub: Term → Term → Term

  Subtraction

• neg: Term → Term

  Negation

• incr: Term → Term

  Increment (i.e., add one)

• decr: Term → Term

  Decrement (i.e., subtract one)

• repeatBit: Term → Term

  repeatBit is an operation that will repeat the infinitely repeat the least significant true bit of the input.

  That is repeatBit t is all-zeroes iff t is all-zeroes. Otherwise, there is some number k s.t. repeatBit t is all-ones after dropping the least significant k bits

def Term.eval (t : Term) (vars : ℕ → BitStream) : BitStream

Evaluate a term t to the BitStream it represents, given a value for the free variables in t.

Note that we don't keep track of how many free variable occur in t, so eval requires us to give a value for each possible variable.

Equations

• (Term.var n).eval vars = vars n
• Term.zero.eval vars = BitStream.zero
• Term.one.eval vars = BitStream.one
• Term.negOne.eval vars = BitStream.negOne
• (t₁.and t₂).eval vars = t₁.eval vars &&& t₂.eval vars
• (t₁.or t₂).eval vars = t₁.eval vars ||| t₂.eval vars
• (t₁.xor t₂).eval vars = t₁.eval vars ^^^ t₂.eval vars
• t_2.not.eval vars = ~~~t_2.eval vars
• (Term.ls b t_2).eval vars = BitStream.concat b (t_2.eval vars)
• (t₁.add t₂).eval vars = t₁.eval vars + t₂.eval vars
• (t₁.sub t₂).eval vars = t₁.eval vars - t₂.eval vars
• t_2.neg.eval vars = -t_2.eval vars
• t_2.incr.eval vars = (t_2.eval vars).incr
• t_2.decr.eval vars = (t_2.eval vars).decr
• t_2.repeatBit.eval vars = (t_2.eval vars).repeatBit

instance instAddTerm : Add Term

Equations

• instAddTerm = { add := Term.add }

instance instSubTerm : Sub Term

Equations

• instSubTerm = { sub := Term.sub }

instance instOneTerm : One Term

Equations

• instOneTerm = { one := Term.one }

instance instZeroTerm : Zero Term

Equations

• instZeroTerm = { zero := Term.zero }

instance instNegTerm : Neg Term

Equations

• instNegTerm = { neg := Term.neg }

def Term.arity : 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

• (Term.var n).arity = n + 1
• Term.zero.arity = 0
• Term.one.arity = 0
• 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_1.not.arity = t_1.arity
• (Term.ls b t_1).arity = t_1.arity
• (t₁.add t₂).arity = max t₁.arity t₂.arity
• (t₁.sub t₂).arity = max t₁.arity t₂.arity
• t_1.neg.arity = t_1.arity
• t_1.incr.arity = t_1.arity
• t_1.decr.arity = t_1.arity
• t_1.repeatBit.arity = t_1.arity

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

Evaluate a term t to the BitStream 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

• (Term.var n).evalFin vars_2 = vars_2 (Fin.last n)
• Term.zero.evalFin vars_2 = BitStream.zero
• Term.one.evalFin vars_2 = BitStream.one
• Term.negOne.evalFin vars_2 = BitStream.negOne
• (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
• (Term.ls b t_2).evalFin vars_2 = BitStream.concat b (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).incr
• t_2.decr.evalFin vars_2 = (t_2.evalFin vars_2).decr
• t_2.repeatBit.evalFin vars_2 = (t_2.evalFin vars_2).repeatBit