structure AutoStructs.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 : FinEnum 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 AutoStructs.FSM.State {arity : Type} (p : AutoStructs.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 AutoStructs.FSM.nextBit {arity : Type} (p : AutoStructs.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 AutoStructs.FSM.carry {arity : Type} (p : AutoStructs.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 AutoStructs.FSM.eval {arity : Type} (p : AutoStructs.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 AutoStructs.FSM.eval' {arity : Type} (p : AutoStructs.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 AutoStructs.FSM.changeInitCarry {arity : Type} (p : AutoStructs.FSM arity) (c : p.α → Bool) : AutoStructs.FSM arity

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

Equations

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

theorem AutoStructs.FSM.carry_changeInitCarry_succ {arity : Type} (p : AutoStructs.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 AutoStructs.FSM.eval_changeInitCarry_succ {arity : Type} (p : AutoStructs.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 AutoStructs.FSM.eval_eq_carry {arity : Type} (p : AutoStructs.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 AutoStructs.FSM.eval_eq_eval' {arity : Type} (p : AutoStructs.FSM arity) {x : arity → BitStream} : p.eval x = p.eval' x

def AutoStructs.FSM.changeVars {arity : Type} (p : AutoStructs.FSM arity) {arity2 : Type} (changeVars : arity → arity2) : AutoStructs.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 = AutoStructs.FSM.mk p.α p.initCarry fun (a : Option p.α) => (p.nextBitCirc a).map (Sum.map id changeVars)

def AutoStructs.FSM.compose {arity : Type} (p : AutoStructs.FSM arity) [FinEnum arity] [DecidableEq arity] (new_arity : Type) (q_arity : arity → Type) (vars : (a : arity) → q_arity a → new_arity) (q : (a : arity) → AutoStructs.FSM (q_arity a)) : AutoStructs.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 AutoStructs.FSM.carry_compose {arity : Type} (p : AutoStructs.FSM arity) [FinEnum arity] [DecidableEq arity] (new_arity : Type) (q_arity : arity → Type) (vars : (a : arity) → q_arity a → new_arity) (q : (a : arity) → AutoStructs.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 AutoStructs.FSM.eval_compose {arity : Type} (p : AutoStructs.FSM arity) [FinEnum arity] [DecidableEq arity] (new_arity : Type) (q_arity : arity → Type) (vars : (a : arity) → q_arity a → new_arity) (q : (a : arity) → AutoStructs.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 AutoStructs.FSM.and : AutoStructs.FSM Bool

Equations

• AutoStructs.FSM.and = AutoStructs.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 AutoStructs.FSM.eval_and (x : Bool → BitStream) : AutoStructs.FSM.and.eval x = x true &&& x false

def AutoStructs.FSM.or : AutoStructs.FSM Bool

Equations

• AutoStructs.FSM.or = AutoStructs.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 AutoStructs.FSM.eval_or (x : Bool → BitStream) : AutoStructs.FSM.or.eval x = x true ||| x false

def AutoStructs.FSM.xor : AutoStructs.FSM Bool

Equations

• AutoStructs.FSM.xor = AutoStructs.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 AutoStructs.FSM.eval_xor (x : Bool → BitStream) : AutoStructs.FSM.xor.eval x = x true ^^^ x false

def AutoStructs.FSM.add : AutoStructs.FSM Bool

Equations

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

theorem AutoStructs.FSM.carry_add_succ (x : Bool → BitStream) (n : ℕ) : AutoStructs.FSM.add.carry x (n + 1) = fun (x_1 : AutoStructs.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 AutoStructs.FSM.carry_zero {arity : Type} (p : AutoStructs.FSM arity) (x : arity → BitStream) : p.carry x 0 = p.initCarry

@[simp]

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

@[simp]

theorem AutoStructs.FSM.eval_add (x : Bool → BitStream) : AutoStructs.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 AutoStructs.FSM.sub : AutoStructs.FSM Bool

Equations

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

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

@[simp]

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

def AutoStructs.FSM.neg : AutoStructs.FSM Unit

Equations

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

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

@[simp]

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

def AutoStructs.FSM.not : AutoStructs.FSM Unit

Equations

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

@[simp]

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

def AutoStructs.FSM.zero : AutoStructs.FSM (Fin 0)

Equations

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

@[simp]

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

def AutoStructs.FSM.one : AutoStructs.FSM (Fin 0)

Equations

• AutoStructs.FSM.one = AutoStructs.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 AutoStructs.FSM.carry_one (x : Fin 0 → BitStream) (n : ℕ) : AutoStructs.FSM.one.carry x (n + 1) = fun (x : AutoStructs.FSM.one.α) => false

@[simp]

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

def AutoStructs.FSM.negOne : AutoStructs.FSM (Fin 0)

Equations

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

@[simp]

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

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

Equations

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

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

@[simp]

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

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

Equations

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

@[simp]

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

def AutoStructs.FSM.incr : AutoStructs.FSM Unit

Equations

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

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

@[simp]

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

def AutoStructs.FSM.decr : AutoStructs.FSM Unit

Equations

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

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

@[simp]

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

theorem AutoStructs.FSM.evalAux_eq_zero_of_set {arity : Type} (p : AutoStructs.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 AutoStructs.FSM.eval_eq_zero_of_set {arity : Type} (p : AutoStructs.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 AutoStructs.FSM.repeatBit : AutoStructs.FSM Unit

Equations

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

@[simp]

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

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

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

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

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

Equations

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

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

Equations

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

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

Equations

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

@[simp]

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

@[simp]

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

instance AutoStructs.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 AutoStructs.termEvalEqFSM (t : AutoStructs.Term) : AutoStructs.FSMSolution t

Equations

• AutoStructs.termEvalEqFSM (AutoStructs.Term.var n) = { toFSM := AutoStructs.FSM.var n, good := ⋯ }
• AutoStructs.termEvalEqFSM AutoStructs.Term.zero = { toFSM := AutoStructs.FSM.zero, good := AutoStructs.termEvalEqFSM.proof_15 }
• AutoStructs.termEvalEqFSM AutoStructs.Term.one = { toFSM := AutoStructs.FSM.one, good := AutoStructs.termEvalEqFSM.proof_16 }
• AutoStructs.termEvalEqFSM AutoStructs.Term.negOne = { toFSM := AutoStructs.FSM.negOne, good := AutoStructs.termEvalEqFSM.proof_17 }
• AutoStructs.termEvalEqFSM (t₁.and t₂) = { toFSM := AutoStructs.composeBinary AutoStructs.FSM.and (AutoStructs.termEvalEqFSM t₁) (AutoStructs.termEvalEqFSM t₂), good := ⋯ }
• AutoStructs.termEvalEqFSM (t₁.or t₂) = { toFSM := AutoStructs.composeBinary AutoStructs.FSM.or (AutoStructs.termEvalEqFSM t₁) (AutoStructs.termEvalEqFSM t₂), good := ⋯ }
• AutoStructs.termEvalEqFSM (t₁.xor t₂) = { toFSM := AutoStructs.composeBinary AutoStructs.FSM.xor (AutoStructs.termEvalEqFSM t₁) (AutoStructs.termEvalEqFSM t₂), good := ⋯ }
• AutoStructs.termEvalEqFSM t.not = { toFSM := id (AutoStructs.composeUnary AutoStructs.FSM.not (AutoStructs.termEvalEqFSM t)), good := ⋯ }
• AutoStructs.termEvalEqFSM (t₁.add t₂) = { toFSM := AutoStructs.composeBinary AutoStructs.FSM.add (AutoStructs.termEvalEqFSM t₁) (AutoStructs.termEvalEqFSM t₂), good := ⋯ }
• AutoStructs.termEvalEqFSM (t₁.sub t₂) = { toFSM := AutoStructs.composeBinary AutoStructs.FSM.sub (AutoStructs.termEvalEqFSM t₁) (AutoStructs.termEvalEqFSM t₂), good := ⋯ }
• AutoStructs.termEvalEqFSM t.neg = { toFSM := id (AutoStructs.composeUnary AutoStructs.FSM.neg (AutoStructs.termEvalEqFSM t)), good := ⋯ }
• AutoStructs.termEvalEqFSM t.incr = { toFSM := id (AutoStructs.composeUnary AutoStructs.FSM.incr (AutoStructs.termEvalEqFSM t)), good := ⋯ }
• AutoStructs.termEvalEqFSM t.decr = { toFSM := id (AutoStructs.composeUnary AutoStructs.FSM.decr (AutoStructs.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 AutoStructs.and : AutoStructs.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 AutoStructs.or : AutoStructs.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 AutoStructs.Result : Type

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

instance AutoStructs.instReprResult : Repr AutoStructs.Result

Equations

• AutoStructs.instReprResult = { reprPrec := AutoStructs.reprResult✝ }

instance AutoStructs.instDecidableEqResult : DecidableEq AutoStructs.Result

Equations

• AutoStructs.instDecidableEqResult = AutoStructs.decEqResult✝

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

Equations

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

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

@[irreducible]

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

Equations

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

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

Equations

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

@[irreducible]

theorem AutoStructs.decideIfZerosAux_correct {arity : Type} [DecidableEq arity] (p : AutoStructs.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) : AutoStructs.decideIfZerosAux p c = true ↔ ∀ (n : ℕ) (x : arity → BitStream), p.eval x n = false

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

inductive AutoStructs.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 : AutoStructs.Term) → AutoStructs.Predicate (max t1.arity t2.arity)
• and: {n m : ℕ} → AutoStructs.Predicate n → AutoStructs.Predicate m → AutoStructs.Predicate (max n m)
• or: {n m : ℕ} → AutoStructs.Predicate n → AutoStructs.Predicate m → AutoStructs.Predicate (max n m)