// ⚠️  UNAUDITED. EXPERIMENTAL. Use-at-own-risk for high-value flows.
//
// Aldabra escrow validator — v1 (Plutus V3 / Aiken v1.1.x)
//
// No third-party audit has been performed. Internal review only —
// see audits/2026-05-09-escrow-internal-audit.md for findings.
//
// Two-party agreement-with-veto escrow. See aiken-escrow/README.md
// for the state-machine summary.
//
// State machine:
//   Open ─(both sign Agree)─▶ Agreed{at} ─(lock elapsed, no veto)─▶ Settle (→ recipient)
//                                  │
//                                  └─(A or B fires Veto)──────────▶ Refund (per-contributor)
//   Open ─(open_deadline passed)──────────────────────────────────▶ Refund (per-contributor)
//
// Five redeemers: Deposit / Agree / Veto / Settle / Refund.

use aiken/collection/list
use aiken/collection/pairs
use aiken/crypto.{VerificationKeyHash}
use aiken/interval.{Finite}
use aiken/cbor
use cardano/address.{Address, VerificationKey}
use cardano/assets.{Value, add, flatten, merge, negate, quantity_of, zero}
use cardano/transaction.{
  Transaction, Output, OutputReference, InlineDatum, find_input,
}

// ----- types -----
//
// FlatValue mirrors Plutus's on-chain `Map PolicyId (Map AssetName Int)`
// using concrete `Pairs` since the cardano/assets `Value` type is opaque
// (datums require concrete types). Convert to/from `Value` at script
// boundaries via `assets.flatten` + manual reduction.

pub type AssetEntries = Pairs<ByteArray, Int>

pub type FlatValue = Pairs<ByteArray, AssetEntries>

pub type DepositEntry {
  contributor: VerificationKeyHash,
  value: FlatValue,
}

pub type EscrowState {
  Open
  Agreed { agreed_at_ms: Int }
}

pub type EscrowDatum {
  party_a: VerificationKeyHash,
  party_b: VerificationKeyHash,
  recipient: VerificationKeyHash,
  open_deadline_ms: Int,
  lock_period_ms: Int,
  state: EscrowState,
  deposits: List<DepositEntry>,
}

pub type EscrowRedeemer {
  Deposit { contributor: VerificationKeyHash }
  Agree
  Veto
  Settle
  Refund
}

// ----- helpers -----

fn signed_by(tx: Transaction, pkh: VerificationKeyHash) -> Bool {
  list.has(tx.extra_signatories, pkh)
}

fn pkh_to_base_address(pkh: VerificationKeyHash) -> Address {
  Address {
    payment_credential: VerificationKey(pkh),
    stake_credential: None,
  }
}

/// Convert opaque on-chain Value into FlatValue (Pairs form). Iterates
/// `assets.flatten` triples and groups by policy.
fn value_to_flat(v: Value) -> FlatValue {
  list.foldr(
    flatten(v),
    [],
    fn(triple, acc) {
      let (policy, name, qty) = triple
      // append (name, qty) under existing policy entry, else add new
      when pairs.get_first(acc, policy) is {
        Some(entries) -> {
          let updated = list.concat(entries, [Pair(name, qty)])
          insert_pair(acc, policy, updated)
        }
        None -> list.concat(acc, [Pair(policy, [Pair(name, qty)])])
      }
    },
  )
}

/// Functional update: replace `key`'s value in the Pairs (key must exist
/// per caller's check).
fn insert_pair(p: Pairs<ByteArray, AssetEntries>, key: ByteArray, value: AssetEntries) -> Pairs<ByteArray, AssetEntries> {
  list.map(
    p,
    fn(entry) {
      let Pair(k, v) = entry
      if k == key {
        Pair(k, value)
      } else {
        Pair(k, v)
      }
    },
  )
}

/// Find the unique continuing output back to `script_addr`. Returns
/// (datum, value) when exactly one such output exists.
fn find_continuing_output(
  outputs: List<Output>,
  script_addr: Address,
) -> Option<(EscrowDatum, Value)> {
  let candidates = list.filter(outputs, fn(o) { o.address == script_addr })
  when candidates is {
    [single] -> {
      when single.datum is {
        InlineDatum(d) -> {
          expect new_datum: EscrowDatum = d
          Some((new_datum, single.value))
        }
        _ -> None
      }
    }
    _ -> None
  }
}

/// True iff a >= b in every (policy, asset) component using opaque Value
/// arithmetic.
fn value_geq_value(a: Value, b: Value) -> Bool {
  list.all(
    flatten(b),
    fn(triple) {
      let (policy, name, qty) = triple
      quantity_of(a, policy, name) >= qty
    },
  )
}

/// True iff `paid` (a Value) >= `flat` (a FlatValue) per-component.
fn value_geq_flat(paid: Value, flat: FlatValue) -> Bool {
  list.all(
    flat,
    fn(policy_entry) {
      let Pair(policy, assets) = policy_entry
      list.all(
        assets,
        fn(asset_entry) {
          let Pair(name, qty) = asset_entry
          quantity_of(paid, policy, name) >= qty
        },
      )
    },
  )
}

/// Sum every entry across all deposits into a single on-chain `Value`.
/// Used by Veto / Refund-timeout to enforce the invariant
/// `sum(deposits.value) == in_value` — i.e., the escrow's tracked
/// deposits must account for every lovelace + token actually locked
/// at the script. Without this, an escrow opened with empty deposits
/// + non-zero locked value (or one griefed via a token send) lets the
/// driver pocket untracked funds via vacuous-true `refund_outputs_satisfy`.
/// HIGH-2 fix from 2026-05-09 internal audit.
fn deposits_to_value(deposits: List<DepositEntry>) -> Value {
  list.foldr(
    deposits,
    zero,
    fn(d, acc) {
      list.foldr(
        d.value,
        acc,
        fn(policy_entry, acc2) {
          let Pair(policy, assets_) = policy_entry
          list.foldr(
            assets_,
            acc2,
            fn(asset_entry, acc3) {
              let Pair(name, qty) = asset_entry
              add(acc3, policy, name, qty)
            },
          )
        },
      )
    },
  )
}

/// Component-wise equality on opaque `Value`. Cheaper than two-direction
/// `value_geq_value` because we can short-circuit on the first mismatch.
fn value_eq(a: Value, b: Value) -> Bool {
  value_geq_value(a, b) && value_geq_value(b, a)
}

/// For each Deposit entry, an output to that contributor's base address
/// must pay at least the entry's value.
fn refund_outputs_satisfy(
  tx_outputs: List<Output>,
  deposits: List<DepositEntry>,
) -> Bool {
  list.all(
    deposits,
    fn(d) {
      let target = pkh_to_base_address(d.contributor)
      let paid =
        list.foldr(
          tx_outputs,
          zero,
          fn(o, acc) {
            if o.address == target {
              merge(acc, o.value)
            } else {
              acc
            }
          },
        )
      value_geq_flat(paid, d.value)
    },
  )
}

fn tx_lower_ms(tx: Transaction) -> Option<Int> {
  when tx.validity_range.lower_bound.bound_type is {
    Finite(t) -> Some(t)
    _ -> None
  }
}

fn tx_upper_ms(tx: Transaction) -> Option<Int> {
  when tx.validity_range.upper_bound.bound_type is {
    Finite(t) -> Some(t)
    _ -> None
  }
}

/// Compute new deposits list = old with `net_added` (a FlatValue)
/// attributed to `contributor` (merge into existing entry if present,
/// else append).
fn expected_deposits_after(
  old: List<DepositEntry>,
  contributor: VerificationKeyHash,
  net_added: FlatValue,
) -> List<DepositEntry> {
  let has_entry = list.any(old, fn(d) { d.contributor == contributor })
  if has_entry {
    list.map(
      old,
      fn(d) {
        if d.contributor == contributor {
          DepositEntry { contributor: d.contributor, value: flat_merge(d.value, net_added) }
        } else {
          d
        }
      },
    )
  } else {
    list.concat(old, [DepositEntry { contributor, value: net_added }])
  }
}

/// Component-wise add of two FlatValues, preserving first-seen ordering.
fn flat_merge(a: FlatValue, b: FlatValue) -> FlatValue {
  list.foldr(
    b,
    a,
    fn(b_entry, acc) {
      let Pair(b_policy, b_assets) = b_entry
      when pairs.get_first(acc, b_policy) is {
        Some(a_assets) -> {
          let merged = merge_assets(a_assets, b_assets)
          insert_pair(acc, b_policy, merged)
        }
        None -> list.concat(acc, [Pair(b_policy, b_assets)])
      }
    },
  )
}

fn merge_assets(a: AssetEntries, b: AssetEntries) -> AssetEntries {
  list.foldr(
    b,
    a,
    fn(b_entry, acc) {
      let Pair(b_name, b_qty) = b_entry
      when pairs.get_first(acc, b_name) is {
        Some(a_qty) -> insert_asset(acc, b_name, a_qty + b_qty)
        None -> list.concat(acc, [Pair(b_name, b_qty)])
      }
    },
  )
}

fn insert_asset(p: AssetEntries, key: ByteArray, value: Int) -> AssetEntries {
  list.map(
    p,
    fn(entry) {
      let Pair(k, v) = entry
      if k == key {
        Pair(k, value)
      } else {
        Pair(k, v)
      }
    },
  )
}

// ----- validator -----

validator escrow {
  spend(
    datum: Option<EscrowDatum>,
    redeemer: EscrowRedeemer,
    own_ref: OutputReference,
    self: Transaction,
  ) {
    expect Some(d) = datum
    expect Some(in_) = find_input(self.inputs, own_ref)
    let in_value = in_.output.value
    let script_addr = in_.output.address

    when redeemer is {
      Deposit { contributor } -> {
        expect d.state == Open
        expect contributor == d.party_a || contributor == d.party_b
        expect signed_by(self, contributor)
        expect Some((new_d, new_value)) =
          find_continuing_output(self.outputs, script_addr)
        // HIGH-1 fix (2026-05-09 audit): without this, `net_added` from
        // `flatten(merge(new_value, negate(in_value)))` could carry
        // negative quantities and the depositor could DRAIN tokens
        // while writing a matching new_d.deposits with reduced values.
        // Forcing new_value ≥ in_value component-wise ensures every
        // net_added entry is non-negative.
        expect value_geq_value(new_value, in_value)
        // Datum unchanged except `deposits`
        expect new_d.party_a == d.party_a
        expect new_d.party_b == d.party_b
        expect new_d.recipient == d.recipient
        expect new_d.open_deadline_ms == d.open_deadline_ms
        expect new_d.lock_period_ms == d.lock_period_ms
        expect new_d.state == Open
        // Net added = new_value - in_value (in Value space)
        let net_added = value_to_flat(merge(new_value, negate(in_value)))
        // Deposits list updated correctly
        let expected = expected_deposits_after(d.deposits, contributor, net_added)
        cbor.serialise(expected) == cbor.serialise(new_d.deposits)
      }

      Agree -> {
        expect d.state == Open
        expect signed_by(self, d.party_a)
        expect signed_by(self, d.party_b)
        expect Some(upper) = tx_upper_ms(self)
        expect upper <= d.open_deadline_ms
        expect Some((new_d, new_value)) =
          find_continuing_output(self.outputs, script_addr)
        expect value_geq_value(new_value, in_value) && value_geq_value(in_value, new_value)
        expect new_d.party_a == d.party_a
        expect new_d.party_b == d.party_b
        expect new_d.recipient == d.recipient
        expect new_d.open_deadline_ms == d.open_deadline_ms
        expect new_d.lock_period_ms == d.lock_period_ms
        expect cbor.serialise(new_d.deposits) == cbor.serialise(d.deposits)
        new_d.state == Agreed { agreed_at_ms: upper }
      }

      Veto -> {
        expect Agreed { .. } = d.state
        expect signed_by(self, d.party_a) || signed_by(self, d.party_b)
        // HIGH-2 fix (2026-05-09 audit): without this, an escrow whose
        // deposits don't account for every lovelace at the script
        // (e.g. opened with `initial_contributor=None`, or griefed via
        // a token-send) lets the driver pocket untracked funds as
        // change because `refund_outputs_satisfy` is vacuously true on
        // empty / partial deposits. Enforcing equality forces the
        // tracked deposits to be the FULL accounting of locked value.
        expect value_eq(deposits_to_value(d.deposits), in_value)
        refund_outputs_satisfy(self.outputs, d.deposits)
      }

      Settle -> {
        expect Agreed { agreed_at_ms } = d.state
        expect Some(lower) = tx_lower_ms(self)
        expect lower > agreed_at_ms + d.lock_period_ms
        let recipient_addr = pkh_to_base_address(d.recipient)
        let paid =
          list.foldr(
            self.outputs,
            zero,
            fn(o, acc) {
              if o.address == recipient_addr {
                merge(acc, o.value)
              } else {
                acc
              }
            },
          )
        value_geq_value(paid, in_value)
      }

      Refund -> {
        expect d.state == Open
        expect Some(lower) = tx_lower_ms(self)
        expect lower > d.open_deadline_ms
        // HIGH-2 fix (2026-05-09 audit): same invariant as Veto —
        // deposits must account for full in_value, else driver
        // pockets untracked funds via vacuous refund_outputs_satisfy.
        expect value_eq(deposits_to_value(d.deposits), in_value)
        refund_outputs_satisfy(self.outputs, d.deposits)
      }
    }
  }

  else(_) {
    fail
  }
}

// ----- tests -----

test minimal_smoke() {
  // Smoke test: type-checks. End-to-end behavior is exercised by the
  // off-chain builder integration tests in `crates/aldabra-dao`.
  True
}