Core Linear Temporal Logic Operators

These operators form the foundation of LTL for hardware verification. All operators work on Signal d Bool predicates.

def Sparkle.Verification.Temporal.always {d : Core.Domain.DomainConfig} (P : Core.Signal.Signal d Bool) : Prop

always P - Property P holds at ALL future time steps.

Semantics: ∀ t, P.atTime t = true

Example:

theorem counter_never_exceeds_max :
  always (counter.map (· < 256))

Equations

• Sparkle.Verification.Temporal.always P = ∀ (t : Nat), P.atTime t = true

def Sparkle.Verification.Temporal.eventually {d : Core.Domain.DomainConfig} (P : Core.Signal.Signal d Bool) : Prop

eventually P - Property P holds at SOME future time step.

Semantics: ∃ t, P.atTime t = true

Example:

theorem done_flag_set :
  eventually (done.map (· == true))

Equations

• Sparkle.Verification.Temporal.eventually P = ∃ (t : Nat), P.atTime t = true

def Sparkle.Verification.Temporal.next {d : Core.Domain.DomainConfig} (n : Nat) (P : Core.Signal.Signal d Bool) : Prop

next n P - Property P holds exactly n cycles in the future.

Semantics: ∀ t, P.atTime (t + n) = true

Example:

theorem pipeline_latency :
  next 3 (output.map (· == expected))

Equations

• Sparkle.Verification.Temporal.next n P = ∀ (t : Nat), P.atTime (t + n) = true

def Sparkle.Verification.Temporal.Until {d : Core.Domain.DomainConfig} (P Q : Core.Signal.Signal d Bool) : Prop

Until P Q - Property P holds until Q becomes true.

Semantics: ∃ t, Q.atTime t = true ∧ (∀ t' < t, P.atTime t' = true)

Example:

theorem busy_until_done :
  Until (busy.map id) (done.map id)

Equations

• Sparkle.Verification.Temporal.Until P Q = ∃ (t : Nat), Q.atTime t = true ∧ ∀ (t' : Nat), t' < t → P.atTime t' = true

Derived Temporal Operators

These are convenience operators defined in terms of the core LTL operators.

def Sparkle.Verification.Temporal.implies {d : Core.Domain.DomainConfig} (P Q : Core.Signal.Signal d Bool) : Prop

implies P Q - Temporal implication: whenever P holds, Q also holds.

Semantics: ∀ t, P.atTime t = true → Q.atTime t = true

Equations

• Sparkle.Verification.Temporal.implies P Q = ∀ (t : Nat), P.atTime t = true → Q.atTime t = true

def Sparkle.Verification.Temporal.release {d : Core.Domain.DomainConfig} (P Q : Core.Signal.Signal d Bool) : Prop

release P Q - Dual of until: Q holds until and including when P holds.

Semantics: ∀ t, (Q.atTime t = true) ∨ (∃ t' ≤ t, P.atTime t' = true ∧ ∀ t'' < t', Q.atTime t'' = true)

Equations

• Sparkle.Verification.Temporal.release P Q = ∀ (t : Nat), Q.atTime t = true ∨ ∃ (t' : Nat), t' ≤ t ∧ P.atTime t' = true ∧ ∀ (t'' : Nat), t'' < t' → Q.atTime t'' = true

def Sparkle.Verification.Temporal.WeakUntil {d : Core.Domain.DomainConfig} (P Q : Core.Signal.Signal d Bool) : Prop

WeakUntil P Q - Like Until, but P can hold forever if Q never becomes true.

Semantics: (∃ t, Q.atTime t ∧ ∀ t' < t, P.atTime t') ∨ (∀ t, P.atTime t)

Equations

• Sparkle.Verification.Temporal.WeakUntil P Q = ((∃ (t : Nat), Q.atTime t = true ∧ ∀ (t' : Nat), t' < t → P.atTime t' = true) ∨ ∀ (t : Nat), P.atTime t = true)

Optimization-Enabling Operators

These operators specifically enable cycle-skipping optimizations when proven. They express stability properties that allow the simulator to skip evaluations.

def Sparkle.Verification.Temporal.stableFor {d : Core.Domain.DomainConfig} {α : Type} [BEq α] (s : Core.Signal.Signal d α) (v : α) (n : Nat) : Prop

stableFor s v n - Signal s maintains value v for exactly n cycles.

This is the KEY property that enables cycle skipping optimization. When proven, the simulator can skip n-1 evaluation cycles.

Example:

theorem reset_stable :
  stableFor counter 0 10  -- Counter stays 0 for 10 cycles

Equations

• Sparkle.Verification.Temporal.stableFor s v n = ∀ (t : Nat), t < n → (s.atTime t == v) = true

def Sparkle.Verification.Temporal.stableWhile {d : Core.Domain.DomainConfig} {α : Type} [BEq α] (s : Core.Signal.Signal d α) (cond : Core.Signal.Signal d Bool) : Prop

stableWhile s cond - Signal s remains constant while condition holds.

Example:

theorem idle_stable :
  stableWhile state (isIdle.map id)

Equations

• Sparkle.Verification.Temporal.stableWhile s cond = ∀ (t : Nat), cond.atTime t = true → cond.atTime (t + 1) = true ∧ (s.atTime (t + 1) == s.atTime t) = true

def Sparkle.Verification.Temporal.monotonic {d : Core.Domain.DomainConfig} (s : Core.Signal.Signal d Nat) : Prop

monotonic s - Signal s is monotonically increasing.

Useful for counters and timers. While not enabling cycle skipping, helps prove other temporal properties.

Equations

• Sparkle.Verification.Temporal.monotonic s = ∀ (t : Nat), s.atTime t ≤ s.atTime (t + 1)

Temporal Induction Principles

Helper lemmas and tactics for proving temporal properties.

theorem Sparkle.Verification.Temporal.always_induction {d : Core.Domain.DomainConfig} (P : Core.Signal.Signal d Bool) : P.atTime 0 = true → (∀ (t : Nat), P.atTime t = true → P.atTime (t + 1) = true) → always P

Induction principle for always: To prove ∀ t, P(t), prove P(0) and P(t) → P(t+1).

theorem Sparkle.Verification.Temporal.stableFor_induction {d : Core.Domain.DomainConfig} {α : Type} [BEq α] (s : Core.Signal.Signal d α) (v : α) (n : Nat) : (s.atTime 0 == v) = true → (∀ (t : Nat), t < n → (s.atTime t == v) = true → (s.atTime (t + 1) == v) = true) → stableFor s v (n + 1)

Induction principle for stableFor: To prove signal stays stable for n cycles, prove base case and preservation.

Note: This is a placeholder theorem for future proof development.

theorem Sparkle.Verification.Temporal.always_implies {d : Core.Domain.DomainConfig} (P Q : Core.Signal.Signal d Bool) : always P → implies P Q → always Q

Composition lemma: If P always holds and P implies Q, then Q always holds.

theorem Sparkle.Verification.Temporal.always_implies_eventually {d : Core.Domain.DomainConfig} (P : Core.Signal.Signal d Bool) : always P → eventually P

Eventually is weaker than always: if P always holds, it eventually holds.

Temporal Oracle Interface (Future Work)

This interface will be used by an optimized simulator to enable cycle skipping. Currently a placeholder for future implementation.

structure Sparkle.Verification.Temporal.TemporalOracle (d : Core.Domain.DomainConfig) : Type 1

Temporal Oracle: Queries proven temporal properties to enable cycle skipping.

The oracle checks if a signal has a proven stability property and returns how many cycles can be safely skipped.

• canSkip (α : Type) [BEq α] : Core.Signal.Signal d α → α → Option Nat

  Query if we can skip cycles for a given signal property

• soundness {α : Type} [BEq α] (s : Core.Signal.Signal d α) (v : α) (n : Nat) : self.canSkip α s v = some n → stableFor s v n

  Proof that canSkip is sound: if it returns n, the signal is stable for n cycles

def Sparkle.Verification.Temporal.emptyOracle {d : Core.Domain.DomainConfig} : TemporalOracle d

Empty oracle: no optimizations available. This is the default for standard simulation.

Equations

• Sparkle.Verification.Temporal.emptyOracle = { canSkip := fun (x : Type) [BEq x] (x_1 : Sparkle.Core.Signal.Signal d x) (x_2 : x) => none, soundness := ⋯ }

Notation and Helpers

Convenient notation for temporal formulas.

def Sparkle.Verification.Temporal.«term◯_» : Lean.ParserDescr

Equations

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

def Sparkle.Verification.Temporal.«term□_» : Lean.ParserDescr

Equations

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

def Sparkle.Verification.Temporal.«term◇_» : Lean.ParserDescr

Equations

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

def Sparkle.Verification.Temporal.term_U_ : Lean.TrailingParserDescr

Equations

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

def Sparkle.Verification.Temporal.term_R_ : Lean.TrailingParserDescr

Equations

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

def Sparkle.Verification.Temporal.«term_⟹_» : Lean.TrailingParserDescr

Equations

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

def Sparkle.Verification.Temporal.satisfiesAt {d : Core.Domain.DomainConfig} (P : Core.Signal.Signal d Bool) (t : Nat) : Bool

Check if a signal satisfies a property at a specific time.

Equations

• Sparkle.Verification.Temporal.satisfiesAt P t = P.atTime t

def Sparkle.Verification.Temporal.satisfiesFor {d : Core.Domain.DomainConfig} (P : Core.Signal.Signal d Bool) (n : Nat) : Prop

Check if a signal satisfies a property for a duration.

Equations

• Sparkle.Verification.Temporal.satisfiesFor P n = ∀ (t : Nat), t < n → P.atTime t = true

Examples and Documentation

See Examples/TemporalLogicExample.md for comprehensive usage examples.