theorem Sparkle.Verification.Equivalence.SignalLemmas.val_add {dom : Core.Domain.DomainConfig} {n : Nat} (a b : Core.Signal.Signal dom (BitVec n)) (t : Nat) : (a + b).val t = a.val t + b.val t

theorem Sparkle.Verification.Equivalence.SignalLemmas.val_sub {dom : Core.Domain.DomainConfig} {n : Nat} (a b : Core.Signal.Signal dom (BitVec n)) (t : Nat) : (a - b).val t = a.val t - b.val t

theorem Sparkle.Verification.Equivalence.SignalLemmas.val_mul {dom : Core.Domain.DomainConfig} {n : Nat} (a b : Core.Signal.Signal dom (BitVec n)) (t : Nat) : (a * b).val t = a.val t * b.val t

theorem Sparkle.Verification.Equivalence.SignalLemmas.val_and {dom : Core.Domain.DomainConfig} {n : Nat} (a b : Core.Signal.Signal dom (BitVec n)) (t : Nat) : (a &&& b).val t = a.val t &&& b.val t

theorem Sparkle.Verification.Equivalence.SignalLemmas.val_or {dom : Core.Domain.DomainConfig} {n : Nat} (a b : Core.Signal.Signal dom (BitVec n)) (t : Nat) : (a ||| b).val t = a.val t ||| b.val t

theorem Sparkle.Verification.Equivalence.SignalLemmas.val_xor {dom : Core.Domain.DomainConfig} {n : Nat} (a b : Core.Signal.Signal dom (BitVec n)) (t : Nat) : (a ^^^ b).val t = a.val t ^^^ b.val t

theorem Sparkle.Verification.Equivalence.SignalLemmas.val_register_zero {dom : Core.Domain.DomainConfig} {α : Type} (init : α) (x : Core.Signal.Signal dom α) : (Core.Signal.Signal.register init x).val 0 = init

theorem Sparkle.Verification.Equivalence.SignalLemmas.val_register_succ {dom : Core.Domain.DomainConfig} {α : Type} (init : α) (x : Core.Signal.Signal dom α) (n : Nat) : (Core.Signal.Signal.register init x).val (n + 1) = x.val n

theorem Sparkle.Verification.Equivalence.SignalLemmas.val_pure {dom : Core.Domain.DomainConfig} {α : Type} (x : α) (t : Nat) : (Core.Signal.Signal.pure x).val t = x

theorem Sparkle.Verification.Equivalence.SignalLemmas.val_map {dom : Core.Domain.DomainConfig} {α β : Type} (f : α → β) (s : Core.Signal.Signal dom α) (t : Nat) : (Core.Signal.Signal.map f s).val t = f (s.val t)

theorem Sparkle.Verification.Equivalence.SignalLemmas.val_mux {dom : Core.Domain.DomainConfig} {α : Type} (c : Core.Signal.Signal dom Bool) (a b : Core.Signal.Signal dom α) (t : Nat) : (c.mux a b).val t = if c.val t = true then a.val t else b.val t

theorem Sparkle.Verification.Equivalence.SignalLemmas.val_beq {dom : Core.Domain.DomainConfig} {n : Nat} (a b : Core.Signal.Signal dom (BitVec n)) (t : Nat) : (a.beq b).val t = (a.val t == b.val t)

def Sparkle.Verification.Equivalence.verifyEqCmd : Lean.ParserDescr

#verify_eq f g — prove f = g via funext; unfold; bv_decide.

Equations

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

def Sparkle.Verification.Equivalence.elabVerifyEq : Lean.Elab.Command.CommandElab

Equations

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

def Sparkle.Verification.Equivalence.verifyEqAtCmd : Lean.ParserDescr

#verify_eq_at (cycles := N) (latency := L)? impl spec

Equations

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

def Sparkle.Verification.Equivalence.elabVerifyEqAt : Lean.Elab.Command.CommandElab

Equations

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

def Sparkle.Verification.Equivalence.elabVerifyEqAt.runVerifyEqAt (cyclesLit : Lean.TSyntax `num) (latency : Nat) (impl spec : Lean.Ident) : Lean.Elab.Command.CommandElabM Unit

Equations

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

def Sparkle.Verification.Equivalence.verifyEqGitCmd : Lean.ParserDescr

#verify_eq_git <commit-ref> <ident> — prove the current version of <ident> equivalent to the version at <commit-ref>.

Equations

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

def Sparkle.Verification.Equivalence.elabVerifyEqGit : Lean.Elab.Command.CommandElab

Equations

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

def Sparkle.Verification.Equivalence.elabVerifyEqGit.runVerifyEqGit (commitRef : String) (target : Lean.Ident) : Lean.Elab.Command.CommandElabM Unit

Equations

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