structure FSM (arity : Type) : Type 1

FSM n represents a function BitStream → ⋯ → BitStream → BitStream, where n is the number of BitStream arguments, as a finite state machine.

• α : Type

  The arity of the (finite) type α determines how many bits the internal carry state of this FSM has

• i : Fintype self.α
• dec_eq : DecidableEq self.α
• initCarry : self.α → Bool

  initCarry is the value of the initial internal carry state. It maps each α to a bit, thus it is morally a bitvector where the width is the arity of α

• nextBitCirc : Option self.α → Circuit (self.α ⊕ arity)

  nextBitCirc is a family of Boolean circuits, which may refer to the current input bits and the current state bits as free variables in the circuit.

  nextBitCirc none computes the current output bit. nextBitCirc (some a), computes the one bit of the new state that corresponds to a : α.

@[reducible, inline]

abbrev FSM.State {arity : Type} (p : FSM arity) : Type

The state of FSM p is given by a function from p.α to Bool.

Note that p.α is assumed to be a finite type, so p.State is morally a finite bitvector whose width is given by the arity of p.α

Equations

• p.State = (p.α → Bool)

def FSM.nextBit {arity : Type} (p : FSM arity) : p.State → (arity → Bool) → p.State × Bool

p.nextBit state in computes both the next state bits and the output bit, where state are the current state bits, and in are the current input bits.

Equations

• p.nextBit carry inputBits = (fun (a : p.α) => (p.nextBitCirc (some a)).eval (Sum.elim carry inputBits), (p.nextBitCirc none).eval (Sum.elim carry inputBits))

def FSM.carry {arity : Type} (p : FSM arity) (x : arity → BitStream) : ℕ → p.State

p.carry in i computes the internal carry state at step i, given input streams in

Equations

• p.carry x 0 = p.initCarry
• p.carry x n.succ = (p.nextBit (p.carry x n) fun (i : arity) => x i n).1

def FSM.eval {arity : Type} (p : FSM arity) (x : arity → BitStream) : BitStream

eval p morally gives the function BitStream → ... → BitStream represented by FSM p

Equations

• p.eval x n = (p.nextBit (p.carry x n) fun (i : arity) => x i n).2

def FSM.eval' {arity : Type} (p : FSM arity) (x : arity → BitStream) : BitStream

eval' is an alternative definition of eval

Equations

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

def FSM.changeInitCarry {arity : Type} (p : FSM arity) (c : p.α → Bool) : FSM arity

p.changeInitCarry c yields an FSM with c as the initial state

Equations

• p.changeInitCarry c = FSM.mk p.α c p.nextBitCirc

theorem FSM.carry_changeInitCarry_succ {arity : Type} (p : FSM arity) (c : p.α → Bool) (x : arity → BitStream) (n : ℕ) : (p.changeInitCarry c).carry x (n + 1) = (p.changeInitCarry (p.nextBit c fun (a : arity) => x a 0).1).carry (fun (a : arity) (i : ℕ) => x a (i + 1)) n

theorem FSM.eval_changeInitCarry_succ {arity : Type} (p : FSM arity) (c : p.α → Bool) (x : arity → BitStream) (n : ℕ) : (p.changeInitCarry c).eval x (n + 1) = (p.changeInitCarry (p.nextBit c fun (a : arity) => x a 0).1).eval (fun (a : arity) (i : ℕ) => x a (i + 1)) n

theorem FSM.eval_eq_carry {arity : Type} (p : FSM arity) (x : arity → BitStream) (n : ℕ) : p.eval x n = (p.nextBit (p.carry x n) fun (i : arity) => x i n).2

unfolds the definition of eval

theorem FSM.eval_eq_eval' {arity : Type} (p : FSM arity) {x : arity → BitStream} : p.eval x = p.eval' x

def FSM.changeVars {arity : Type} (p : FSM arity) {arity2 : Type} (changeVars : arity → arity2) : FSM arity2

p.changeVars f changes the arity of an FSM. The function f determines how the new input bits map to the input expected by p

Equations

• p.changeVars changeVars = FSM.mk p.α p.initCarry fun (a : Option p.α) => (p.nextBitCirc a).map (Sum.map id changeVars)

def FSM.compose {arity : Type} (p : FSM arity) [Fintype arity] [DecidableEq arity] (new_arity : Type) (q_arity : arity → Type) (vars : (a : arity) → q_arity a → new_arity) (q : (a : arity) → FSM (q_arity a)) : FSM new_arity

Given an FSM p of arity n, a family of n FSMs qᵢ of posibly different arities mᵢ, and given yet another arity m such that mᵢ ≤ m for all i, we can compose p with qᵢ yielding a single FSM of arity m, such that each FSM qᵢ computes the ith bit that is fed to the FSM p.

Equations

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

theorem FSM.carry_compose {arity : Type} (p : FSM arity) [Fintype arity] [DecidableEq arity] (new_arity : Type) (q_arity : arity → Type) (vars : (a : arity) → q_arity a → new_arity) (q : (a : arity) → FSM (q_arity a)) (x : new_arity → BitStream) (n : ℕ) : (p.compose new_arity q_arity vars q).carry x n = let z := p.carry (fun (a : arity) => (q a).eval fun (i : q_arity a) => x (vars a i)) n; Sum.elim z fun (a : (a : arity) × (q a).α) => (q a.fst).carry (fun (t : q_arity a.fst) => x (vars a.fst t)) n a.snd

theorem FSM.eval_compose {arity : Type} (p : FSM arity) [Fintype arity] [DecidableEq arity] (new_arity : Type) (q_arity : arity → Type) (vars : (a : arity) → q_arity a → new_arity) (q : (a : arity) → FSM (q_arity a)) (x : new_arity → BitStream) : (p.compose new_arity q_arity vars q).eval x = p.eval fun (a : arity) => (q a).eval fun (i : q_arity a) => x (vars a i)

Evaluating a composed fsm is equivalent to composing the evaluations of the constituent FSMs

def FSM.and : FSM Bool

Equations

• FSM.and = FSM.mk Empty Empty.elim fun (a : Option Empty) => a.elim ((Circuit.var true (Sum.inr true)).and (Circuit.var true (Sum.inr false))) Empty.elim

@[simp]

theorem FSM.eval_and (x : Bool → BitStream) : FSM.and.eval x = x true &&& x false

def FSM.or : FSM Bool

Equations

• FSM.or = FSM.mk Empty Empty.elim fun (a : Option Empty) => a.elim ((Circuit.var true (Sum.inr true)).or (Circuit.var true (Sum.inr false))) Empty.elim

@[simp]

theorem FSM.eval_or (x : Bool → BitStream) : FSM.or.eval x = x true ||| x false

def FSM.xor : FSM Bool

Equations

• FSM.xor = FSM.mk Empty Empty.elim fun (a : Option Empty) => a.elim ((Circuit.var true (Sum.inr true)).xor (Circuit.var true (Sum.inr false))) Empty.elim

@[simp]

theorem FSM.eval_xor (x : Bool → BitStream) : FSM.xor.eval x = x true ^^^ x false

def FSM.add : FSM Bool

Equations

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

theorem FSM.carry_add_succ (x : Bool → BitStream) (n : ℕ) : FSM.add.carry x (n + 1) = fun (x_1 : FSM.add.α) => ((x true).addAux (x false) n).2

The internal carry state of the add FSM agrees with the carry bit of addition as implemented on bitstreams

@[simp]

theorem FSM.carry_zero {arity : Type} (p : FSM arity) (x : arity → BitStream) : p.carry x 0 = p.initCarry

@[simp]

theorem FSM.initCarry_add : FSM.add.initCarry = fun (x : FSM.add.α) => false

@[simp]

theorem FSM.eval_add (x : Bool → BitStream) : FSM.add.eval x = x true + x false

We don't really need subtraction or negation FSMs, given that we can reduce both those operations to just addition and bitwise complement

def FSM.sub : FSM Bool

Equations

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

theorem FSM.carry_sub (x : Bool → BitStream) (n : ℕ) : FSM.sub.carry x (n + 1) = fun (x_1 : FSM.sub.α) => ((x true).subAux (x false) n).2

@[simp]

theorem FSM.eval_sub (x : Bool → BitStream) : FSM.sub.eval x = x true - x false

def FSM.neg : FSM Unit

Equations

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

theorem FSM.carry_neg (x : Unit → BitStream) (n : ℕ) : FSM.neg.carry x (n + 1) = fun (x_1 : FSM.neg.α) => ((x ()).negAux n).2

@[simp]

theorem FSM.eval_neg (x : Unit → BitStream) : FSM.neg.eval x = -x ()

def FSM.not : FSM Unit

Equations

• FSM.not = FSM.mk Empty Empty.elim fun (x : Option Empty) => Circuit.var false (Sum.inr ())

@[simp]

theorem FSM.eval_not (x : Unit → BitStream) : FSM.not.eval x = ~~~x ()

def FSM.zero : FSM (Fin 0)

Equations

• FSM.zero = FSM.mk Empty Empty.elim fun (x : Option Empty) => Circuit.fals

@[simp]

theorem FSM.eval_zero (x : Fin 0 → BitStream) : FSM.zero.eval x = BitStream.zero

def FSM.one : FSM (Fin 0)

Equations

• FSM.one = FSM.mk Unit (fun (x : Unit) => true) fun (a : Option Unit) => match a with | some PUnit.unit => Circuit.fals | none => Circuit.var true (Sum.inl ())

@[simp]

theorem FSM.carry_one (x : Fin 0 → BitStream) (n : ℕ) : FSM.one.carry x (n + 1) = fun (x : FSM.one.α) => false

@[simp]

theorem FSM.eval_one (x : Fin 0 → BitStream) : FSM.one.eval x = BitStream.one

def FSM.negOne : FSM (Fin 0)

Equations

• FSM.negOne = FSM.mk Empty Empty.elim fun (x : Option Empty) => Circuit.tru

@[simp]

theorem FSM.eval_negOne (x : Fin 0 → BitStream) : FSM.negOne.eval x = BitStream.negOne

def FSM.ls (b : Bool) : FSM Unit

Equations

• FSM.ls b = FSM.mk Unit (fun (x : Unit) => b) fun (x : Option Unit) => match x with | none => Circuit.var true (Sum.inl ()) | some PUnit.unit => Circuit.var true (Sum.inr ())

theorem FSM.carry_ls (b : Bool) (x : Unit → BitStream) (n : ℕ) : (FSM.ls b).carry x (n + 1) = fun (x_1 : (FSM.ls b).α) => x () n

@[simp]

theorem FSM.eval_ls (b : Bool) (x : Unit → BitStream) : (FSM.ls b).eval x = BitStream.concat b (x ())

def FSM.var (n : ℕ) : FSM (Fin (n + 1))

Equations

• FSM.var n = FSM.mk Empty Empty.elim fun (x : Option Empty) => Circuit.var true (Sum.inr (Fin.last n))

@[simp]

theorem FSM.eval_var (n : ℕ) (x : Fin (n + 1) → BitStream) : (FSM.var n).eval x = x (Fin.last n)

def FSM.incr : FSM Unit

Equations

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

theorem FSM.carry_incr (x : Unit → BitStream) (n : ℕ) : FSM.incr.carry x (n + 1) = fun (x_1 : FSM.incr.α) => ((x ()).incrAux n).2

@[simp]

theorem FSM.eval_incr (x : Unit → BitStream) : FSM.incr.eval x = (x ()).incr

def FSM.decr : FSM Unit

Equations

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

theorem FSM.carry_decr (x : Unit → BitStream) (n : ℕ) : FSM.decr.carry x (n + 1) = fun (x_1 : FSM.decr.α) => ((x ()).decrAux n).2

@[simp]

theorem FSM.eval_decr (x : Unit → BitStream) : FSM.decr.eval x = (x ()).decr

theorem FSM.evalAux_eq_zero_of_set {arity : Type} (p : FSM arity) (R : Set (p.α → Bool)) (hR : ∀ (x : arity → Bool) (s : p.State), (p.nextBit s x).1 ∈ R → s ∈ R) (hi : p.initCarry ∉ R) (hr1 : ∀ (x : arity → Bool) (s : p.State), (p.nextBit s x).2 = true → s ∈ R) (x : arity → BitStream) (n : ℕ) : p.eval x n = false ∧ p.carry x n ∉ R

theorem FSM.eval_eq_zero_of_set {arity : Type} (p : FSM arity) (R : Set (p.α → Bool)) (hR : ∀ (x : arity → Bool) (s : p.State), (p.nextBit s x).1 ∈ R → s ∈ R) (hi : p.initCarry ∉ R) (hr1 : ∀ (x : arity → Bool) (s : p.State), (p.nextBit s x).2 = true → s ∈ R) : p.eval = fun (x : arity → BitStream) (x : ℕ) => false

def FSM.repeatBit : FSM Unit

Equations

• FSM.repeatBit = FSM.mk Unit (fun (x : Unit) => false) fun (x : Option Unit) => (Circuit.var true (Sum.inl ())).or (Circuit.var true (Sum.inr ()))

@[simp]

theorem FSM.eval_repeatBit {x : Unit → BitStream} : FSM.repeatBit.eval x = (x ()).repeatBit

structure FSMSolution (t : Term) extends FSM : Type 1

• α : Type
• i : Fintype self.α
• dec_eq : DecidableEq self.α
• initCarry : self.α → Bool
• nextBitCirc : Option self.α → Circuit (self.α ⊕ Fin t.arity)
• good : t.evalFin = self.eval

theorem FSMSolution.good {t : Term} (self : FSMSolution t) : t.evalFin = self.eval

def composeUnary (p : FSM Unit) {t : Term} (q : FSMSolution t) : FSM (Fin t.arity)

Equations

• composeUnary p q = p.compose (Fin t.arity) (fun (x : Unit) => Fin t.arity) (fun (x : Unit) => id) fun (x : Unit) => q.toFSM

def composeBinary (p : FSM Bool) {t₁ : Term} {t₂ : Term} (q₁ : FSMSolution t₁) (q₂ : FSMSolution t₂) : FSM (Fin (max t₁.arity t₂.arity))

Equations

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

def composeBinary' (p : FSM Bool) {n : ℕ} {m : ℕ} (q₁ : FSM (Fin n)) (q₂ : FSM (Fin m)) : FSM (Fin (max n m))

Equations

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

@[simp]

theorem composeUnary_eval (p : FSM Unit) {t : Term} (q : FSMSolution t) (x : Fin t.arity → BitStream) : (composeUnary p q).eval x = p.eval fun (x_1 : Unit) => t.evalFin x

@[simp]

theorem composeBinary_eval (p : FSM Bool) {t₁ : Term} {t₂ : Term} (q₁ : FSMSolution t₁) (q₂ : FSMSolution t₂) (x : Fin (max t₁.arity t₂.arity) → BitStream) : (composeBinary p q₁ q₂).eval x = p.eval fun (b : Bool) => bif b then t₁.evalFin fun (i : Fin t₁.arity) => x (Fin.castLE ⋯ i) else t₂.evalFin fun (i : Fin t₂.arity) => x (Fin.castLE ⋯ i)

instance instFintypeCond_sSA {α : Type} {β : Type} [Fintype α] [Fintype β] (b : Bool) : Fintype (bif b then α else β)

Equations

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

def termEvalEqFSM (t : Term) : FSMSolution t

Equations

• termEvalEqFSM (Term.var n) = { toFSM := FSM.var n, good := ⋯ }
• termEvalEqFSM Term.zero = { toFSM := FSM.zero, good := termEvalEqFSM.proof_17 }
• termEvalEqFSM Term.one = { toFSM := FSM.one, good := termEvalEqFSM.proof_18 }
• termEvalEqFSM Term.negOne = { toFSM := FSM.negOne, good := termEvalEqFSM.proof_19 }
• termEvalEqFSM (t₁.and t₂) = { toFSM := composeBinary FSM.and (termEvalEqFSM t₁) (termEvalEqFSM t₂), good := ⋯ }
• termEvalEqFSM (t₁.or t₂) = { toFSM := composeBinary FSM.or (termEvalEqFSM t₁) (termEvalEqFSM t₂), good := ⋯ }
• termEvalEqFSM (t₁.xor t₂) = { toFSM := composeBinary FSM.xor (termEvalEqFSM t₁) (termEvalEqFSM t₂), good := ⋯ }
• termEvalEqFSM (Term.ls b t) = { toFSM := id (composeUnary (FSM.ls b) (termEvalEqFSM t)), good := ⋯ }
• termEvalEqFSM t.not = { toFSM := id (composeUnary FSM.not (termEvalEqFSM t)), good := ⋯ }
• termEvalEqFSM (t₁.add t₂) = { toFSM := composeBinary FSM.add (termEvalEqFSM t₁) (termEvalEqFSM t₂), good := ⋯ }
• termEvalEqFSM (t₁.sub t₂) = { toFSM := composeBinary FSM.sub (termEvalEqFSM t₁) (termEvalEqFSM t₂), good := ⋯ }
• termEvalEqFSM t.neg = { toFSM := id (composeUnary FSM.neg (termEvalEqFSM t)), good := ⋯ }
• termEvalEqFSM t.incr = { toFSM := id (composeUnary FSM.incr (termEvalEqFSM t)), good := ⋯ }
• termEvalEqFSM t.decr = { toFSM := id (composeUnary FSM.decr (termEvalEqFSM t)), good := ⋯ }
• termEvalEqFSM t.repeatBit = { toFSM := id (composeUnary FSM.repeatBit (termEvalEqFSM t)), good := ⋯ }

FSM that implement bitwise-and. Since we use 0 as the good state, we keep the invariant that if both inputs are good and our state is 0, then we produce a 0. If not, we produce an infinite sequence of 1.

def and : FSM Bool

Equations

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

FSM that implement bitwise-or. Since we use 0 as the good state, we keep the invariant that if either inputs is 0 then our state is 0. If not, we produce a 1.

def or : FSM Bool

Equations

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

FSM that implement logical not. we keep the invariant that if the input ever fails and becomes a 1, then we produce a 0. IF not, we produce an infinite sequence of 1.

EDIT: Aha, this doesn't work! We need NFA to DFA here (as the presburger book does), where we must produce an infinite sequence of0 iff the input can ever become a 1. But here, since we phrase things directly in terms of producing sequences, it's a bit less clear what we should do :)

• Alternatively, we need to be able to decide eventually always zero.
• Alternatively, we push negations inside, and decide ⬝ ≠ ⬝ and ⬝ ≰ ⬝.

inductive Result : Type

• falseAfter: ℕ → Result
• trueFor: ℕ → Result
• trueForall: Result

instance instReprResult : Repr Result

Equations

• instReprResult = { reprPrec := reprResult✝ }

instance instDecidableEqResult : DecidableEq Result

Equations

• instDecidableEqResult = decEqResult✝

def card_compl {α : Type} [Fintype α] [DecidableEq α] (c : Circuit α) : ℕ

Equations

• card_compl c = (Finset.filter (fun (a : α → Bool) => c.eval a = false) Finset.univ).card

theorem decideIfZeroAux_wf {α : Type} [Fintype α] [DecidableEq α] {c : Circuit α} {c' : Circuit α} (h : ¬c' ≤ c) : card_compl (c' ||| c) < card_compl c

@[irreducible]

def decideIfZerosAux {arity : Type} [DecidableEq arity] (p : FSM arity) (c : Circuit p.α) : Bool

Equations

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

def decideIfZeros {arity : Type} [DecidableEq arity] (p : FSM arity) : Bool

Equations

• decideIfZeros p = decideIfZerosAux p (p.nextBitCirc none).fst

@[irreducible]

theorem decideIfZerosAux_correct {arity : Type} [DecidableEq arity] (p : FSM arity) (c : Circuit p.α) (hc : ∀ (s : p.α → Bool), c.eval s = true → ∃ (m : ℕ) (y : arity → BitStream), (p.changeInitCarry s).eval y m = true) (hc₂ : ∀ (x : arity → Bool) (s : p.α → Bool), (p.nextBit s x).2 = true → c.eval s = true) : decideIfZerosAux p c = true ↔ ∀ (n : ℕ) (x : arity → BitStream), p.eval x n = false

theorem decideIfZeros_correct {arity : Type} [DecidableEq arity] (p : FSM arity) : decideIfZeros p = true ↔ ∀ (n : ℕ) (x : arity → BitStream), p.eval x n = false

inductive Predicate : ℕ → Type

The fragment of predicate logic that we support in bv_automata. Currently, we support equality, conjunction, disjunction, and negation. This can be expanded to also support arithmetic constraints such as unsigned-less-than.

• eq: (t1 t2 : Term) → Predicate (max t1.arity t2.arity)
• and: {n m : ℕ} → Predicate n → Predicate m → Predicate (max n m)
• or: {n m : ℕ} → Predicate n → Predicate m → Predicate (max n m)

def Predicate.denote {α : ℕ} : Predicate α → Prop

denote a reflected predicate into a `prop.

Equations

• (Predicate.eq t1 t2).denote = (t1.eval = t2.eval)
• (p.and q).denote = (p.denote ∧ q.denote)
• (p.or q).denote = (p.denote ∨ q.denote)

def Predicate.toFSM {k : ℕ} : Predicate k → FSM (Fin k)

Convert a predicate into a proposition

Equations

• (Predicate.eq t1 t2).toFSM = (termEvalEqFSM (t1.xor t2).repeatBit).toFSM
• (p.and q).toFSM = composeBinary' FSM.and p.toFSM q.toFSM
• (p.or q).toFSM = composeBinary' FSM.or p.toFSM q.toFSM

theorem Predicate.toFsm_correct {k : ℕ} (p : Predicate k) : decideIfZeros p.toFSM = true ↔ p.denote