///|
fn evidence_leaf(sequence : Int, event_hash : Int, state_hash : Int) -> Int {
  fingerprint_text("leaf|\{sequence}|\{event_hash}|\{state_hash}")
}

///|
fn evidence_parent(left : Int, right : Int) -> Int {
  fingerprint_text("node|\{left}|\{right}")
}

///|
fn empty_evidence_root() -> Int {
  fingerprint_text("replay-evidence-empty")
}

///|
fn build_next_level(current : Array[Int]) -> Array[Int] {
  let next : Array[Int] = []
  for index = 0; index < current.length(); index = index + 2 {
    let right = if index + 1 < current.length() {
      current[index + 1]
    } else {
      current[index]
    }
    next.push(evidence_parent(current[index], right))
  }
  next
}

///|
/// Builds a deterministic commitment over every event and resulting state.
///
/// The journal chain, replay boundary, state evidence length, and tail anchor
/// must all agree. Invalid or partial reports return `None`.
pub fn[P, S] build_replay_evidence(
  journal : Journal[P],
  report : ReplayReport[S],
  payload_fingerprint : (P) -> String,
) -> ReplayEvidenceTree? {
  match journal.validate(payload_fingerprint) {
    Invalid(_) => return None
    Valid(_, _) => ()
  }
  if report.status != Completed ||
    report.initial_sequence != 0 ||
    report.final_sequence != journal.length() ||
    report.applied_events != journal.length() ||
    report.journal_tail_hash != journal.tail_hash() ||
    report.state_hashes.length() != journal.length() + 1 {
    return None
  }
  if journal.length() == 0 {
    return Some({ event_count: 0, root: empty_evidence_root(), levels: [] })
  }
  let leaves : Array[Int] = []
  for index = 0; index < journal.length(); index = index + 1 {
    let event = match journal.get(index) {
      Some(value) => value
      None => abort("validated journal index disappeared")
    }
    leaves.push(
      evidence_leaf(event.sequence, event.hash, report.state_hashes[index + 1]),
    )
  }
  let levels : Array[Array[Int]] = [leaves]
  let mut current = leaves
  while current.length() > 1 {
    current = build_next_level(current)
    levels.push(current)
  }
  Some({ event_count: journal.length(), root: current[0], levels })
}

///|
/// Creates an inclusion proof for a one-based event sequence.
pub fn[P, S] replay_inclusion_proof(
  journal : Journal[P],
  report : ReplayReport[S],
  tree : ReplayEvidenceTree,
  sequence : Int,
) -> ReplayInclusionProof? {
  if sequence < 1 ||
    sequence > tree.event_count ||
    tree.levels.length() == 0 ||
    report.state_hashes.length() <= sequence {
    return None
  }
  let event = match journal.get(sequence - 1) {
    Some(value) => value
    None => return None
  }
  let state_hash = report.state_hashes[sequence]
  let leaf_hash = evidence_leaf(sequence, event.hash, state_hash)
  if tree.levels[0][sequence - 1] != leaf_hash {
    return None
  }
  let siblings : Array[Int] = []
  let sibling_on_left : Array[Bool] = []
  let mut index = sequence - 1
  for level_index = 0
      level_index < tree.levels.length() - 1
      level_index = level_index + 1 {
    let level = tree.levels[level_index]
    if index % 2 == 0 {
      let sibling = if index + 1 < level.length() {
        level[index + 1]
      } else {
        level[index]
      }
      siblings.push(sibling)
      sibling_on_left.push(false)
    } else {
      siblings.push(level[index - 1])
      sibling_on_left.push(true)
    }
    index = index / 2
  }
  Some({
    sequence,
    event_hash: event.hash,
    state_hash,
    leaf_hash,
    siblings,
    sibling_on_left,
    root: tree.root,
  })
}

///|
/// Verifies a portable inclusion proof without the full journal or state list.
pub fn verify_replay_inclusion(proof : ReplayInclusionProof) -> Bool {
  if proof.sequence < 1 ||
    proof.siblings.length() != proof.sibling_on_left.length() ||
    proof.leaf_hash !=
    evidence_leaf(proof.sequence, proof.event_hash, proof.state_hash) {
    return false
  }
  let mut current = proof.leaf_hash
  for index = 0; index < proof.siblings.length(); index = index + 1 {
    current = if proof.sibling_on_left[index] {
      evidence_parent(proof.siblings[index], current)
    } else {
      evidence_parent(current, proof.siblings[index])
    }
  }
  current == proof.root
}

///|
/// Locates the first differing one-based transition.
///
/// Equal-length trees are searched by descending only into the first unequal
/// subtree. A length mismatch returns the first missing transition boundary.
pub fn first_evidence_divergence(
  left : ReplayEvidenceTree,
  right : ReplayEvidenceTree,
) -> Int? {
  if left.event_count == right.event_count && left.root == right.root {
    return None
  }
  let common = if left.event_count < right.event_count {
    left.event_count
  } else {
    right.event_count
  }
  if left.event_count != right.event_count {
    for index = 0; index < common; index = index + 1 {
      if left.levels[0][index] != right.levels[0][index] {
        return Some(index + 1)
      }
    }
    return Some(common + 1)
  }
  if left.event_count == 0 {
    return None
  }
  let mut level_index = left.levels.length() - 1
  let mut node_index = 0
  while level_index > 0 {
    let child_level = level_index - 1
    let left_child = node_index * 2
    if left.levels[child_level][left_child] !=
      right.levels[child_level][left_child] {
      node_index = left_child
    } else {
      node_index = left_child + 1
    }
    level_index = child_level
  }
  Some(node_index + 1)
}