///|
/// Severity assigned to a failed waveform assertion.
pub enum AssertionSeverity {
  Info
  Warning
  Error
  Fatal
} derive(Debug, Eq)

///|
/// Kinds of temporal and value assertions supported by the engine.
pub enum AssertionKind {
  KnownValue
  StableInterval
  MinimumPulse
  MinimumGap
  UnsignedRange
  OneHot
  ResponseWithin
  NoActivity
  Monotonic
} derive(Debug, Eq)

///|
/// A serializable assertion definition.
pub struct WaveformAssertion {
  name : String
  kind : AssertionKind
  signal_id : String
  companion_id : String?
  start : Int64
  end : Int64
  limit : Int64
  lower : Int64
  upper : Int64
  severity : AssertionSeverity
  message : String
} derive(Debug, Eq)

///|
/// One assertion failure with an exact time range.
pub struct AssertionViolation {
  name : String
  kind : AssertionKind
  signal_id : String
  time : Int64
  end_time : Int64
  severity : AssertionSeverity
  observed : String
  expected : String
  message : String
} derive(Debug, Eq)

///|
/// Aggregate result for a set of assertions.
pub struct AssertionSummary {
  total : Int
  passed : Int
  failed : Int
  fatal : Int
  violations : Array[AssertionViolation]
} derive(Debug)

///|
/// Return all assertion severities for report configuration.
pub fn assertion_severity_catalog() -> Array[AssertionSeverity] {
  [Info, Warning, Error, Fatal]
}

///|
/// Return all assertion kinds for configuration UIs.
pub fn assertion_kind_catalog() -> Array[AssertionKind] {
  [
    KnownValue,
    StableInterval,
    MinimumPulse,
    MinimumGap,
    UnsignedRange,
    OneHot,
    ResponseWithin,
    NoActivity,
    Monotonic,
  ]
}

///|
/// Create a known-value assertion.
pub fn assert_known(
  name : String,
  signal_id : String,
  start : Int64,
  end : Int64,
  severity : AssertionSeverity,
) -> WaveformAssertion {
  base_assertion(name, KnownValue, signal_id, start, end, severity)
}

///|
/// Create a stability assertion over an inclusive time range.
pub fn assert_stable(
  name : String,
  signal_id : String,
  start : Int64,
  end : Int64,
  severity : AssertionSeverity,
) -> WaveformAssertion {
  base_assertion(name, StableInterval, signal_id, start, end, severity)
}

///|
/// Create a minimum pulse-width assertion for a scalar signal.
pub fn assert_minimum_pulse(
  name : String,
  signal_id : String,
  width : Int64,
  severity : AssertionSeverity,
) -> WaveformAssertion {
  {
    ..base_assertion(name, MinimumPulse, signal_id, 0L, 0L, severity),
    limit: Int64::max(1L, width),
  }
}

///|
/// Create a minimum gap assertion between consecutive scalar transitions.
pub fn assert_minimum_gap(
  name : String,
  signal_id : String,
  gap : Int64,
  severity : AssertionSeverity,
) -> WaveformAssertion {
  {
    ..base_assertion(name, MinimumGap, signal_id, 0L, 0L, severity),
    limit: Int64::max(1L, gap),
  }
}

///|
/// Create an unsigned integer range assertion.
pub fn assert_unsigned_range(
  name : String,
  signal_id : String,
  lower : Int64,
  upper : Int64,
  severity : AssertionSeverity,
) -> WaveformAssertion {
  {
    ..base_assertion(name, UnsignedRange, signal_id, 0L, 0L, severity),
    lower,
    upper: Int64::max(lower, upper),
  }
}

///|
/// Create a one-hot assertion for a vector signal.
pub fn assert_one_hot(
  name : String,
  signal_id : String,
  severity : AssertionSeverity,
) -> WaveformAssertion {
  base_assertion(name, OneHot, signal_id, 0L, 0L, severity)
}

///|
/// Create a request/response latency assertion.
pub fn assert_response_within(
  name : String,
  request_id : String,
  response_id : String,
  limit : Int64,
  severity : AssertionSeverity,
) -> WaveformAssertion {
  {
    ..base_assertion(name, ResponseWithin, request_id, 0L, 0L, severity),
    companion_id: Some(response_id),
    limit: Int64::max(0L, limit),
  }
}

///|
/// Create an idle-window assertion.
pub fn assert_no_activity(
  name : String,
  signal_id : String,
  start : Int64,
  end : Int64,
  severity : AssertionSeverity,
) -> WaveformAssertion {
  base_assertion(name, NoActivity, signal_id, start, end, severity)
}

///|
/// Create a monotonic unsigned-value assertion.
pub fn assert_monotonic(
  name : String,
  signal_id : String,
  severity : AssertionSeverity,
) -> WaveformAssertion {
  base_assertion(name, Monotonic, signal_id, 0L, 0L, severity)
}

///|
/// Run one assertion against a trace.
pub fn run_assertion(
  trace : Trace,
  assertion : WaveformAssertion,
) -> Array[AssertionViolation] {
  match assertion.kind {
    KnownValue => check_known_value(trace, assertion)
    StableInterval => check_stable_interval(trace, assertion)
    MinimumPulse => check_minimum_pulse(trace, assertion)
    MinimumGap => check_minimum_gap(trace, assertion)
    UnsignedRange => check_unsigned_range(trace, assertion)
    OneHot => check_one_hot(trace, assertion)
    ResponseWithin => check_response_within(trace, assertion)
    NoActivity => check_no_activity(trace, assertion)
    Monotonic => check_monotonic(trace, assertion)
  }
}

///|
/// Run a suite in declaration order and preserve all failures.
pub fn run_assertion_suite(
  trace : Trace,
  assertions : Array[WaveformAssertion],
) -> AssertionSummary {
  let violations : Array[AssertionViolation] = []
  let mut passed = 0
  for assertion in assertions {
    let current = run_assertion(trace, assertion)
    if current.length() == 0 {
      passed += 1
    } else {
      for violation in current {
        violations.push(violation)
      }
    }
  }
  let fatal = violations.count_if(fn(item) { item.severity == Fatal })
  {
    total: assertions.length(),
    passed,
    failed: assertions.length() - passed,
    fatal,
    violations,
  }
}

///|
/// Return whether every assertion passed.
pub fn AssertionSummary::is_success(self : AssertionSummary) -> Bool {
  self.failed == 0
}

///|
/// Return whether the suite contains a fatal violation.
pub fn AssertionSummary::has_fatal(self : AssertionSummary) -> Bool {
  self.fatal > 0
}

///|
/// Return a deterministic text report.
pub fn AssertionSummary::to_text(self : AssertionSummary) -> String {
  let rows : Array[String] = [
    "assertions=" + self.total.to_string(),
    "passed=" + self.passed.to_string(),
    "failed=" + self.failed.to_string(),
    "fatal=" + self.fatal.to_string(),
  ]
  for item in self.violations {
    rows.push(
      "violation=" +
      item.name +
      " signal=" +
      item.signal_id +
      " time=" +
      item.time.to_string() +
      " end=" +
      item.end_time.to_string() +
      " severity=" +
      assertion_severity_name(item.severity) +
      " observed=" +
      item.observed +
      " expected=" +
      item.expected,
    )
  }
  rows.join("\n")
}

///|
/// Return failures as CSV suitable for CI artifacts.
pub fn AssertionSummary::to_csv(self : AssertionSummary) -> String {
  let rows : Array[String] = [
    "name,kind,signal,time,end_time,severity,observed,expected,message",
  ]
  for item in self.violations {
    rows.push(
      csv_cell(item.name) +
      "," +
      assertion_kind_name(item.kind) +
      "," +
      csv_cell(item.signal_id) +
      "," +
      item.time.to_string() +
      "," +
      item.end_time.to_string() +
      "," +
      assertion_severity_name(item.severity) +
      "," +
      csv_cell(item.observed) +
      "," +
      csv_cell(item.expected) +
      "," +
      csv_cell(item.message),
    )
  }
  rows.join("\n")
}

///|
/// Return failures as JSON.
pub fn AssertionSummary::to_json(self : AssertionSummary) -> String {
  let body = self.violations
    .map(fn(item) {
      "{\"name\":\"" +
      csv_cell(item.name) +
      "\",\"kind\":\"" +
      assertion_kind_name(item.kind) +
      "\",\"signal\":\"" +
      csv_cell(item.signal_id) +
      "\",\"time\":" +
      item.time.to_string() +
      ",\"end_time\":" +
      item.end_time.to_string() +
      ",\"severity\":\"" +
      assertion_severity_name(item.severity) +
      "\",\"observed\":\"" +
      csv_cell(item.observed) +
      "\",\"expected\":\"" +
      csv_cell(item.expected) +
      "\",\"message\":\"" +
      csv_cell(item.message) +
      "\"}"
    })
    .join(",")
  "{\"total\":" +
  self.total.to_string() +
  ",\"passed\":" +
  self.passed.to_string() +
  ",\"failed\":" +
  self.failed.to_string() +
  ",\"fatal\":" +
  self.fatal.to_string() +
  ",\"success\":" +
  self.is_success().to_string() +
  ",\"violations\":[" +
  body +
  "]}"
}

///|
/// Return the canonical severity name.
pub fn assertion_severity_name(value : AssertionSeverity) -> String {
  match value {
    Info => "info"
    Warning => "warning"
    Error => "error"
    Fatal => "fatal"
  }
}

///|
/// Return the canonical assertion kind name.
pub fn assertion_kind_name(value : AssertionKind) -> String {
  match value {
    KnownValue => "known-value"
    StableInterval => "stable-interval"
    MinimumPulse => "minimum-pulse"
    MinimumGap => "minimum-gap"
    UnsignedRange => "unsigned-range"
    OneHot => "one-hot"
    ResponseWithin => "response-within"
    NoActivity => "no-activity"
    Monotonic => "monotonic"
  }
}

///|
/// Check that every observed value is known in a time range.
fn check_known_value(
  trace : Trace,
  assertion : WaveformAssertion,
) -> Array[AssertionViolation] {
  let violations : Array[AssertionViolation] = []
  for change in trace.changes {
    if change.id != assertion.signal_id ||
      !in_assertion_range(change.time, assertion) {
      continue
    }
    if change.value.is_unknown() {
      violations.push(
        make_violation(
          assertion,
          change.time,
          change.time,
          change.value.display(),
          "known",
          "unknown value observed",
        ),
      )
    }
  }
  violations
}

///|
/// Check that a signal keeps one value over the requested interval.
fn check_stable_interval(
  trace : Trace,
  assertion : WaveformAssertion,
) -> Array[AssertionViolation] {
  let violations : Array[AssertionViolation] = []
  let changes = trace.changes.filter(fn(change) {
    change.id == assertion.signal_id &&
    in_assertion_range(change.time, assertion)
  })
  if changes.length() > 1 {
    let baseline = changes[0].value
    for change in changes[1:] {
      if !values_equal(baseline, change.value, true) {
        violations.push(
          make_violation(
            assertion,
            changes[0].time,
            change.time,
            change.value.display(),
            baseline.display(),
            "value changed in stable interval",
          ),
        )
      }
    }
  }
  violations
}

///|
/// Check every scalar value interval against a minimum width.
fn check_minimum_pulse(
  trace : Trace,
  assertion : WaveformAssertion,
) -> Array[AssertionViolation] {
  let violations : Array[AssertionViolation] = []
  let changes = trace.changes.filter(fn(change) {
    change.id == assertion.signal_id
  })
  for index in 0.. Array[AssertionViolation] {
  let violations : Array[AssertionViolation] = []
  let changes = trace.changes.filter(fn(change) {
    change.id == assertion.signal_id
  })
  for index in 1.. Array[AssertionViolation] {
  let violations : Array[AssertionViolation] = []
  for change in trace.changes {
    if change.id != assertion.signal_id {
      continue
    }
    match change.value.to_int() {
      Some(value) if value < assertion.lower || value > assertion.upper =>
        violations.push(
          make_violation(
            assertion,
            change.time,
            change.time,
            value.to_string(),
            assertion.lower.to_string() + ".." + assertion.upper.to_string(),
            "unsigned value is outside range",
          ),
        )
      _ => ()
    }
  }
  violations
}

///|
/// Check that a vector contains at most one logical one at every sample.
fn check_one_hot(
  trace : Trace,
  assertion : WaveformAssertion,
) -> Array[AssertionViolation] {
  let violations : Array[AssertionViolation] = []
  for change in trace.changes {
    if change.id != assertion.signal_id {
      continue
    }
    match change.value {
      Vector(bits) => {
        let ones = bits.to_array().count_if(fn(bit) { bit == '1' })
        if ones > 1 {
          violations.push(
            make_violation(
              assertion,
              change.time,
              change.time,
              bits,
              "at most one 1",
              "one-hot constraint violated",
            ),
          )
        }
      }
      _ => ()
    }
  }
  violations
}

///|
/// Check that every rising request has a response before its deadline.
fn check_response_within(
  trace : Trace,
  assertion : WaveformAssertion,
) -> Array[AssertionViolation] {
  let violations : Array[AssertionViolation] = []
  match assertion.companion_id {
    Some(response_id) => {
      let requests = rising_times(trace, assertion.signal_id)
      let responses = rising_times(trace, response_id)
      for request in requests {
        let found = responses.any(fn(response) {
          response >= request && response - request <= assertion.limit
        })
        if !found {
          violations.push(
            make_violation(
              assertion,
              request,
              request + assertion.limit,
              "missing",
              "response within " + assertion.limit.to_string(),
              "response deadline exceeded",
            ),
          )
        }
      }
    }
    None => ()
  }
  violations
}

///|
/// Check that no changes occur in an idle interval.
fn check_no_activity(
  trace : Trace,
  assertion : WaveformAssertion,
) -> Array[AssertionViolation] {
  trace.changes
  .filter(fn(change) {
    change.id == assertion.signal_id &&
    in_assertion_range(change.time, assertion)
  })
  .map(fn(change) {
    make_violation(
      assertion,
      change.time,
      change.time,
      change.value.display(),
      "no change",
      "activity observed in idle interval",
    )
  })
}

///|
/// Check that known unsigned samples never decrease.
fn check_monotonic(
  trace : Trace,
  assertion : WaveformAssertion,
) -> Array[AssertionViolation] {
  let violations : Array[AssertionViolation] = []
  let mut previous : (Int64, Int64)? = None
  for change in trace.changes {
    if change.id != assertion.signal_id {
      continue
    }
    match change.value.to_int() {
      Some(current) =>
        match previous {
          Some((time, value)) if current < value =>
            violations.push(
              make_violation(
                assertion,
                time,
                change.time,
                current.to_string(),
                ">=" + value.to_string(),
                "monotonic value decreased",
              ),
            )
          _ => ()
        }
      None => ()
    }
    match change.value.to_int() {
      Some(value) => previous = Some((change.time, value))
      None => ()
    }
  }
  violations
}

///|
/// Create a base assertion with neutral numeric parameters.
fn base_assertion(
  name : String,
  kind : AssertionKind,
  signal_id : String,
  start : Int64,
  end : Int64,
  severity : AssertionSeverity,
) -> WaveformAssertion {
  {
    name,
    kind,
    signal_id,
    companion_id: None,
    start,
    end,
    limit: 0L,
    lower: 0L,
    upper: 0L,
    severity,
    message: name,
  }
}

///|
/// Return whether a timestamp is inside a rule's optional range.
fn in_assertion_range(time : Int64, assertion : WaveformAssertion) -> Bool {
  (assertion.start == 0L && assertion.end == 0L) ||
  (
    time >= Int64::min(assertion.start, assertion.end) &&
    time <= Int64::max(assertion.start, assertion.end)
  )
}

///|
/// Create a normalized violation record.
fn make_violation(
  assertion : WaveformAssertion,
  time : Int64,
  end_time : Int64,
  observed : String,
  expected : String,
  message : String,
) -> AssertionViolation {
  {
    name: assertion.name,
    kind: assertion.kind,
    signal_id: assertion.signal_id,
    time,
    end_time,
    severity: assertion.severity,
    observed,
    expected,
    message,
  }
}

///|
/// Return rising edge timestamps for one scalar signal.
fn rising_times(trace : Trace, signal_id : String) -> Array[Int64] {
  edges(trace, signal_id)
  .filter(fn(item) { item.kind == Rising })
  .map(fn(item) { item.time })
}