//! Pure decision policy for the video capabilities — no crypto, no I/O.
//!
//! The ad decision and the spend accounting are ordinary integer algorithms;
//! the receipt layer that signs their output is not. Keeping the two apart
//! matters for the same reason `byte-exact-conformance` exists: a module with a
//! minimal dependency closure can be handed to a model checker, and the claims
//! this layer makes are exactly the ones worth checking.
//!
//! `wai.video.ssai` states that **an overspent receipt fails verification**. That
//! property has two halves. The receipt half — `verify()` recomputing the billable spend
//! and rejecting it over the grant's ceiling — is enforced there. The half that
//! lives here is stronger and earlier: [`decide`] never *proposes* a fill that
//! exceeds the funds, the avail duration, or the slot count it was given. The
//! harnesses below prove that, rather than sampling it.

/// A candidate ad in the decision pod.
#[derive(Clone, Debug, PartialEq, Eq)]
pub struct AdCandidate {
    pub ad_id: String,
    /// Identity of the creative bytes — bound into the impression so a swapped
    /// creative breaks the receipt.
    pub creative_hash: [u8; 32],
    pub duration_ms: u64,
    /// Price charged if this ad is served, in minor-currency micro-units. The
    /// same unit as the grant's `funds_ceiling`.
    pub price_micros: u64,
}

/// One filled slot in the avail: the selected ad and the completion its beacons
/// confirmed. `quartiles_reached`: `0` = never rendered, `1` = started (the
/// billable impression, IAB), `2..=5` = 25/50/75/100%.
#[derive(Clone, Debug, PartialEq, Eq)]
pub struct Impression {
    pub slot: u64,
    pub ad_id: String,
    pub creative_hash: [u8; 32],
    pub duration_ms: u64,
    pub price_micros: u64,
    pub quartiles_reached: u8,
}

impl Impression {
    /// An impression is billable once the ad has begun to render (IAB): the
    /// creative reached at least its start beacon.
    pub fn is_billable(&self) -> bool {
        self.quartiles_reached >= 1
    }
}

/// Deterministic decision: fill up to `avail_slots` of a `avail_duration_ms`
/// break from `candidates`, never exceeding `funds_remaining_micros`.
///
/// Greedy by price descending, ties broken by `ad_id` ascending — a pure
/// function of its inputs, so an auditor reproduces the fill exactly. Each
/// selected ad must fit the remaining avail time and the remaining funds. Slots
/// are returned as [`Impression`]s with `quartiles_reached = 0`; the caller
/// raises each as its beacons arrive, then seals.
pub fn decide(
    candidates: &[AdCandidate],
    avail_slots: u64,
    avail_duration_ms: u64,
    funds_remaining_micros: u64,
) -> Vec<Impression> {
    let mut order: Vec<&AdCandidate> = candidates.iter().collect();
    order.sort_by(|a, b| b.price_micros.cmp(&a.price_micros).then(a.ad_id.cmp(&b.ad_id)));
    let mut out = Vec::new();
    let (mut time_left, mut funds_left) = (avail_duration_ms, funds_remaining_micros);
    for c in order {
        if out.len() as u64 >= avail_slots {
            break;
        }
        if c.duration_ms <= time_left && c.price_micros <= funds_left {
            out.push(Impression {
                slot: out.len() as u64,
                ad_id: c.ad_id.clone(),
                creative_hash: c.creative_hash,
                duration_ms: c.duration_ms,
                price_micros: c.price_micros,
                quartiles_reached: 0,
            });
            time_left -= c.duration_ms;
            funds_left -= c.price_micros;
        }
    }
    out
}

/// Σ price over billable impressions — the one definition of spend, used by both
/// `seal` and `verify` so they cannot disagree.
pub(crate) fn billable_spend(impressions: &[Impression]) -> u64 {
    impressions.iter().filter(|i| i.is_billable()).map(|i| i.price_micros).sum()
}

// ─────────────────────────────────────────────────────────────────────
// Kani proof harnesses — "overspend cannot be signed", at its root
// ─────────────────────────────────────────────────────────────────────

// ATTEMPTED AND NOT ACHIEVED — recorded so it is not silently retried.
//
// The natural theorem here is that `decide` never proposes a fill exceeding the
// funds, the avail duration, or the slot count. It does not close under this
// checker:
//
//   - 3 candidates, all fields symbolic .......... CBMC timed out at 600s
//   - 2 candidates, all fields symbolic .......... CBMC timed out at 900s
//   - 2 candidates, durations concrete (funds
//     limit isolated) ............................ CBMC timed out at 600s
//
// The cost is not the budget arithmetic, which is trivial. `decide` sorts by
// `ad_id: String`, so the model has to carry `memcmp` plus the
// `Vec`/`raw_vec`/`Layout`/`handle_alloc_error` machinery; the plumbing around
// the logic is what explodes. Kani could stub that away, and the proof would
// then be about the stub — the "stand-in closing a goal nothing decided"
// failure this codebase has already been bitten by. Not worth a green tick.
//
// So the funds limit remains **test-backed, not proof-backed**: see
// `wai_video_ssai::tests::overspend_cannot_be_signed`, which exercises it on a
// concrete pod. Closing it properly needs either a decision path that does not
// sort on a heap-allocated key, or a deductive verifier (Creusot/Verus) rather
// than a bounded model checker.

/// Everything [`decide`] returns starts unbilled, so a fill cannot be mistaken
/// for delivery: spend is zero until beacons raise the quartiles.
#[cfg(kani)]
#[kani::proof]
#[kani::unwind(8)]
#[kani::solver(kissat)]
fn kani_a_fresh_decision_bills_nothing() {
    let bounded = || -> u64 {
        let v: u64 = kani::any();
        kani::assume(v < (1u64 << 30));
        v
    };
    let pod = [AdCandidate {
        ad_id: "a".to_string(),
        creative_hash: [0u8; 32],
        duration_ms: bounded(),
        price_micros: bounded(),
    }];
    let out = decide(&pod, 1, bounded(), bounded());
    kani::assert(billable_spend(&out) == 0, "a decision bills nothing before its beacons arrive");
}
