rustledger-core 0.20.1

//! Kani Proof Harnesses for rustledger-core
//!
//! These proofs verify that the Rust implementation maintains the same invariants
//! proven in the TLA+ specifications (see `spec/tla/`).
//!
//! # Relationship to TLA+ Specs
//!
//! | TLA+ Spec | Kani Proof | Property Verified |
//! |-----------|------------|-------------------|
//! | Conservation.tla | `proof_conservation_*` | `inventory + reduced = added` |
//! | FIFOCheck.tla | `proof_fifo_*` | FIFO selects oldest lot |
//! | DoubleEntry.tla | `proof_double_entry_*` | Transaction postings sum to zero |
//! | NONECorrect.tla | `proof_none_*` | shorting split exact; conservation across zero |
//!
//! # Why Both TLA+ and Kani?
//!
//! - **TLA+** verifies the *algorithm design* is correct
//! - **Kani** verifies the *Rust implementation* matches that design
//!
//! # Running Proofs
//!
//! ```bash
//! cd crates/rustledger-core
//! cargo kani --all-features
//! ```

#![cfg(kani)]

use rust_decimal::Decimal;

// ============================================================================
// CONSERVATION PROOFS (from Conservation.tla)
// ============================================================================
//
// TLA+ Invariant: inventory + totalReduced = totalAdded
//
// These proofs verify that units are never created from nothing or lost.

/// Proof: Conservation holds for add then reduce sequence.
///
/// Corresponds to Conservation.tla ConservationInvariant:
///   inventory + totalReduced = totalAdded
///
/// After adding X units and reducing Y units (where Y <= X),
/// the remaining inventory equals X - Y.
#[kani::proof]
#[kani::unwind(1)]
fn proof_conservation_add_reduce() {
    let added: i64 = kani::any();
    let reduced: i64 = kani::any();

    // Constrain to valid accounting scenario
    kani::assume(added > 0 && added < 100_000);
    kani::assume(reduced > 0 && reduced < 100_000);
    kani::assume(reduced <= added); // Can't reduce more than added

    let dec_added = Decimal::from(added);
    let dec_reduced = Decimal::from(reduced);

    // Simulate: start at 0, add, then reduce
    let inventory = Decimal::ZERO;
    let after_add = inventory + dec_added;
    let final_inventory = after_add - dec_reduced;

    // Conservation: inventory + reduced = added
    // Rearranged: inventory = added - reduced
    let expected = dec_added - dec_reduced;

    kani::assert(
        final_inventory == expected,
        "Conservation violated: inventory + reduced != added",
    );
}

/// Proof: Conservation holds for multiple add/reduce operations.
///
/// Simulates a more complex sequence: add A, add B, reduce C, reduce D.
/// Verifies: final_inventory = A + B - C - D
#[kani::proof]
#[kani::unwind(1)]
fn proof_conservation_multiple_operations() {
    let add1: i64 = kani::any();
    let add2: i64 = kani::any();
    let reduce1: i64 = kani::any();
    let reduce2: i64 = kani::any();

    kani::assume(add1 > 0 && add1 < 10_000);
    kani::assume(add2 > 0 && add2 < 10_000);
    kani::assume(reduce1 > 0 && reduce1 < 10_000);
    kani::assume(reduce2 > 0 && reduce2 < 10_000);

    let total_added = add1 + add2;
    let total_reduced = reduce1 + reduce2;
    kani::assume(total_reduced <= total_added);

    let mut inventory = Decimal::ZERO;
    inventory = inventory + Decimal::from(add1);
    inventory = inventory + Decimal::from(add2);
    inventory = inventory - Decimal::from(reduce1);
    inventory = inventory - Decimal::from(reduce2);

    // Conservation: inventory = added - reduced
    let expected = Decimal::from(total_added - total_reduced);

    kani::assert(
        inventory == expected,
        "Conservation violated in multi-op sequence",
    );
}

/// Proof: Full reduction returns to zero.
///
/// If we add X and then reduce X, inventory must be exactly zero.
/// This is a critical property for position closing.
#[kani::proof]
#[kani::unwind(1)]
fn proof_conservation_full_reduction_is_zero() {
    let units: i64 = kani::any();
    kani::assume(units > 0 && units < 1_000_000_000);

    let dec_units = Decimal::from(units);

    let inventory = Decimal::ZERO + dec_units - dec_units;

    kani::assert(
        inventory == Decimal::ZERO,
        "Full reduction must return to zero",
    );
}

// ============================================================================
// FIFO ORDERING PROOFS (from FIFOCheck.tla)
// ============================================================================
//
// TLA+ Invariant: FIFO must select the OLDEST lot (by insertion order)
//
// These proofs verify that FIFO booking selects lots in the correct order.

/// A simple lot representation for FIFO verification.
/// Models the [units, date] record from FIFOCheck.tla
struct SimpleLot {
    units: i64,
    /// Insertion order (lower = older)
    order: u8,
}

/// Proof: FIFO selects the first (oldest) lot.
///
/// Corresponds to FIFOCheck.tla FIFOSelectsOldest:
///   For all reductions, selected_date <= all other dates
///
/// With two lots, FIFO must select the one with lower insertion order.
#[kani::proof]
#[kani::unwind(1)]
fn proof_fifo_selects_oldest_of_two() {
    let lot1_units: i64 = kani::any();
    let lot2_units: i64 = kani::any();

    kani::assume(lot1_units > 0 && lot1_units < 1000);
    kani::assume(lot2_units > 0 && lot2_units < 1000);

    // Lot 1 was added first (order=0), Lot 2 added second (order=1)
    let lot1 = SimpleLot {
        units: lot1_units,
        order: 0,
    };
    let lot2 = SimpleLot {
        units: lot2_units,
        order: 1,
    };

    // FIFO: select the lot with minimum order (oldest)
    let selected = if lot1.order < lot2.order {
        &lot1
    } else {
        &lot2
    };

    // Verify FIFO selected the oldest
    kani::assert(selected.order == 0, "FIFO must select oldest lot (order=0)");
}

/// Proof: FIFO order is deterministic regardless of lot sizes.
///
/// Even if Lot 2 has more units than Lot 1, FIFO still selects Lot 1.
#[kani::proof]
#[kani::unwind(1)]
fn proof_fifo_ignores_lot_size() {
    let lot1_units: i64 = kani::any();
    let lot2_units: i64 = kani::any();

    kani::assume(lot1_units > 0 && lot1_units < 1000);
    kani::assume(lot2_units > lot1_units); // Lot 2 is bigger

    let lots = [(lot1_units, 0u8), (lot2_units, 1u8)]; // (units, order)

    // FIFO selection: find minimum order
    let selected_order = lots.iter().map(|(_, order)| *order).min().unwrap();

    kani::assert(
        selected_order == 0,
        "FIFO must select oldest lot regardless of size",
    );
}

// ============================================================================
// LIFO ORDERING PROOFS
// ============================================================================

/// Proof: LIFO selects the last (newest) lot.
///
/// Opposite of FIFO: selects highest insertion order.
#[kani::proof]
#[kani::unwind(1)]
fn proof_lifo_selects_newest() {
    let lot1_order: u8 = 0; // First added
    let lot2_order: u8 = 1; // Second added

    // LIFO: select the lot with maximum order (newest)
    let selected_order = if lot1_order > lot2_order {
        lot1_order
    } else {
        lot2_order
    };

    kani::assert(selected_order == 1, "LIFO must select newest lot (order=1)");
}

// ============================================================================
// HIFO ORDERING PROOFS
// ============================================================================

/// Proof: HIFO selects the highest cost lot.
///
/// Given lots with different costs, HIFO must select the one with highest cost.
#[kani::proof]
#[kani::unwind(1)]
fn proof_hifo_selects_highest_cost() {
    let cost1: i64 = kani::any();
    let cost2: i64 = kani::any();

    kani::assume(cost1 > 0 && cost1 < 100_000);
    kani::assume(cost2 > 0 && cost2 < 100_000);
    kani::assume(cost1 != cost2); // Different costs

    // HIFO: select maximum cost
    let selected_cost = if cost1 > cost2 { cost1 } else { cost2 };
    let max_cost = std::cmp::max(cost1, cost2);

    kani::assert(
        selected_cost == max_cost,
        "HIFO must select highest cost lot",
    );
}

// ============================================================================
// DOUBLE-ENTRY PROOFS (from DoubleEntry.tla)
// ============================================================================
//
// TLA+ Invariant: Every transaction balances (debits = credits)

/// Proof: Transaction with two postings must sum to zero.
///
/// Corresponds to DoubleEntry.tla TransactionsBalance:
///   For a transaction with debit D and credit C, D + (-C) = 0
#[kani::proof]
#[kani::unwind(1)]
fn proof_double_entry_two_postings() {
    let amount: i64 = kani::any();
    kani::assume(amount != 0 && amount != i64::MIN);
    kani::assume(amount.abs() < 1_000_000_000);

    let debit = Decimal::from(amount);
    let credit = Decimal::from(-amount); // Opposite sign

    let sum = debit + credit;

    kani::assert(
        sum == Decimal::ZERO,
        "Double-entry: debit + credit must equal zero",
    );
}

/// Proof: Transaction with multiple postings must sum to zero.
///
/// Simulates: Expense 100, Expense 50, Bank -150
/// Sum must be zero.
#[kani::proof]
#[kani::unwind(1)]
fn proof_double_entry_multiple_postings() {
    let posting1: i64 = kani::any();
    let posting2: i64 = kani::any();

    kani::assume(posting1 > 0 && posting1 < 100_000);
    kani::assume(posting2 > 0 && posting2 < 100_000);

    // posting3 is the balancing posting (negative sum of others)
    let posting3 = -(posting1 + posting2);

    let sum = Decimal::from(posting1) + Decimal::from(posting2) + Decimal::from(posting3);

    kani::assert(
        sum == Decimal::ZERO,
        "Double-entry: all postings must sum to zero",
    );
}

// ============================================================================
// DECIMAL ARITHMETIC PROOFS (foundational properties)
// ============================================================================
//
// These verify that rust_decimal maintains properties we rely on.

/// Proof: Decimal addition is commutative.
///
/// Required for: inventory calculations where order shouldn't matter.
#[kani::proof]
#[kani::unwind(1)]
fn proof_decimal_addition_commutative() {
    let a: i64 = kani::any();
    let b: i64 = kani::any();

    kani::assume(a != i64::MIN && b != i64::MIN);
    kani::assume(a.abs() < 1_000_000 && b.abs() < 1_000_000);

    let dec_a = Decimal::from(a);
    let dec_b = Decimal::from(b);

    kani::assert(
        dec_a + dec_b == dec_b + dec_a,
        "Addition must be commutative",
    );
}

/// Proof: Decimal negation is involutive.
///
/// Required for: sign flipping in reductions is reversible.
#[kani::proof]
#[kani::unwind(1)]
fn proof_decimal_negation_involutive() {
    let a: i64 = kani::any();
    kani::assume(a != i64::MIN);
    kani::assume(a.abs() < 1_000_000_000);

    let dec_a = Decimal::from(a);

    kani::assert(-(-dec_a) == dec_a, "Double negation must return original");
}

// ============================================================================
// NONE-SHORTING ARITHMETIC (from NONECorrect.tla, post-#1686 semantics)
// ============================================================================
//
// NONE booking lets a reduction cross zero: consume what is available, then
// append the remainder as a short (negative) position. These proofs pin the
// arithmetic of that split for ALL amounts in range, complementing the
// 396-behavior NONECorrect replay (which covers model-reachable states only).

/// Proof: the NONE over-reduction split is exact.
///
/// For any `available >= 0` and `requested > available`, consuming
/// `available` and shorting `requested - available` lands exactly at
/// `available - requested` — no units created or lost at the zero crossing.
#[kani::proof]
#[kani::unwind(1)]
fn proof_none_shorting_split_exact() {
    let available: i64 = kani::any();
    let requested: i64 = kani::any();
    kani::assume(available >= 0 && available < 100_000);
    kani::assume(requested > available && requested < 100_000);

    let consumed = Decimal::from(available);
    let shorted = Decimal::from(requested) - consumed;
    let balance = (consumed - consumed) - shorted;

    kani::assert(
        balance == Decimal::from(available - requested),
        "NONE shorting split lost units at the zero crossing",
    );
    kani::assert(balance < Decimal::ZERO, "over-reduction must short");
}

/// Proof: NONE conservation holds across the zero crossing.
///
/// The Conservation identity `balance + totalReduced = totalAdded` must
/// survive a reduction that takes the balance negative (the #1686 class:
/// shorting from a positive balance was rejected while shorting from zero
/// was allowed — the identity held on one path and not the other).
#[kani::proof]
#[kani::unwind(1)]
fn proof_none_conservation_across_zero() {
    let added: i64 = kani::any();
    let reduced: i64 = kani::any();
    kani::assume(added >= 0 && added < 100_000);
    kani::assume(reduced > added && reduced < 100_000); // crosses zero

    let balance = Decimal::from(added) - Decimal::from(reduced);

    kani::assert(
        balance + Decimal::from(reduced) == Decimal::from(added),
        "Conservation violated when shorting past zero",
    );
}

// ============================================================================
// SPIKE FINDING: proofs over the real `Inventory` are NOT tractable today
// ============================================================================
//
// A harness driving the actual `Inventory::reduce` (single simple position,
// two symbolic i64s, STRICT over-reduction must Err and leave the inventory
// untouched — the stutter obligation) was attempted with kani 0.67 /
// CBMC and did NOT verify within a 40-minute solo budget at #[kani::unwind(3)].
// The solver log shows path explosion in:
//
// 1. the currency interner — `size_of_val_raw::<ArcInner<str>>` paths from
//    `Currency::from`'s global interning;
// 2. `imbl::Vector`'s RRB-tree allocation machinery behind
//    `Inventory::positions`.
//
// Until Kani can stub the interner (fixed symbol) and bound imbl's small-
// vector fast path, implementation-level verification of the booking engine
// belongs to the TLA+ behavior-replay + proptest layers (which check the
// same stutter obligation on sampled and model-exhaustive inputs). The
// proofs in this file intentionally stay at the Decimal-arithmetic level,
// where CBMC verifies for ALL values in range within seconds.