Finite-field elements

The Lean type denoting a value of SMT sort (_ FiniteField size), held as the integer representing it. cvc5 answers in the symmetric representation, so an element of GF(5) comes back in [-2, 2] rather than [0, 4]: 3 reads back as -2.

Converting an element to a term and back is done by Cvc.Untyped.Theory.FiniteField and Cvc.Typed.Theory.FiniteField.

structure Cvc.FiniteField (size : Nat) : Type

An element of a finite field of size size, held as an integer representing it.

Any integer congruent to it modulo size represents the same element, but equality, order and hashing compare the integers: ⟨6⟩ : FiniteField 7 and ⟨-1⟩ are the same element yet not equal. Values read from cvc5 come in its symmetric representation, 6 reading back as -1.

• repr : Int

  Element representation.

@[instance_reducible]

instance Cvc.instDecidableEqFiniteField {size✝ : Nat} : DecidableEq (FiniteField size✝)

Equations

• Cvc.instDecidableEqFiniteField = Cvc.instDecidableEqFiniteField.decEq

def Cvc.instDecidableEqFiniteField.decEq {size✝ : Nat} (x✝ x✝¹ : FiniteField size✝) : Decidable (x✝ = x✝¹)

Equations

• Cvc.instDecidableEqFiniteField.decEq { repr := a } { repr := b } = if h : a = b then h ▸ isTrue ⋯ else isFalse ⋯

def Cvc.instHashableFiniteField.hash {size✝ : Nat} : FiniteField size✝ → UInt64

Equations

• Cvc.instHashableFiniteField.hash { repr := a } = mixHash 0 (hash a)

@[instance_reducible]

instance Cvc.instHashableFiniteField {size✝ : Nat} : Hashable (FiniteField size✝)

Equations

• Cvc.instHashableFiniteField = { hash := Cvc.instHashableFiniteField.hash }

def Cvc.instOrdFiniteField.ord {size✝ : Nat} : FiniteField size✝ → FiniteField size✝ → Ordering

Equations

• Cvc.instOrdFiniteField.ord { repr := a } { repr := b } = (compare a b).then Ordering.eq

@[instance_reducible]

instance Cvc.instOrdFiniteField {size✝ : Nat} : Ord (FiniteField size✝)

Equations

• Cvc.instOrdFiniteField = { compare := Cvc.instOrdFiniteField.ord }

@[instance_reducible]

instance Cvc.FiniteField.instToTyp {size : Nat} : ToTyp (FiniteField size)

Equations

• Cvc.FiniteField.instToTyp = { typ := Cvc.Typ.finiteField size }

structure Cvc.FiniteField.Erased : Type

Erased version of FiniteField.

• size : Nat

  The field's size.

• get : FiniteField self.size

  The actual finite field element.

def Cvc.FiniteField.erase {size : Nat} (elem : FiniteField size) : Erased

Erases a finite-field-element's size.

Equations

• elem.erase = { size := size, get := elem }

def Cvc.FiniteField.toString {size : Nat} (ff : FiniteField size) : String

String representation.

Equations

• ff.toString = toString ff.repr

@[instance_reducible]

instance Cvc.FiniteField.instToString {size : Nat} : ToString (FiniteField size)

Equations

• Cvc.FiniteField.instToString = { toString := Cvc.FiniteField.toString }

def Cvc.FiniteField.Erased.toString (elem : Erased) : String

String representation.

Equations

• elem.toString = elem.get.toString

@[instance_reducible]

instance Cvc.FiniteField.Erased.instToString : ToString Erased

Equations

• Cvc.FiniteField.Erased.instToString = { toString := Cvc.FiniteField.Erased.toString }