blvm-consensus 0.1.81

//! Z3 verification witness functions for Orange Paper F_* formulas.
//!
//! These are NOT production code. Each function is a verification artifact:
//! it expresses a formula from the Orange Paper in Z3-translatable Rust so that
//! `cargo spec-lock verify --features z3` can produce a genuine proof obligation,
//! not a vacuous zero-contract pass.
//!
//! Authoring rules (see docs/END_TO_END_PROOF_PLAN.md § Track G):
//! - Do NOT call the production function; express the formula inline.
//! - Use `match k { 0 => X >> 0, 1 => X >> 1, ... }` for piecewise functions
//!   (literal-RHS shifts translate; variable-RHS shifts do not).
//! - No loops, iterators, or method calls on non-whitelisted types.
//! - Body must be translatable by the z3_translator `syn` AST walker.

#[allow(unused_imports)]
use crate::constants::{
    BIP54_MAX_SIGOPS_PER_TX, HALVING_INTERVAL, INITIAL_SUBSIDY, LOCKTIME_THRESHOLD,
    MAX_BLOCK_SIGOPS_COST, MAX_MONEY, TAPROOT_ACTIVATION_MAINNET, TAPROOT_ACTIVATION_TESTNET,
};
#[cfg(feature = "spec-lock")]
use blvm_spec_lock::spec_locked;

// ─── §6.5 Fee Market ─────────────────────────────────────────────────────────

/// Witness for **F_FeeNonNeg** (PROTOCOL.md §6.5).
///
/// Proof obligation: fee = total_in - total_out ≥ 0 when total_in ≥ total_out ≥ 0.
///
/// Z3 proves this via linear arithmetic: the two `requires` establish `total_in ≥ total_out`
/// and `total_out ≥ 0`, so `result = total_in - total_out ≥ 0` follows immediately.
///
/// Formalises the core invariant that transaction fees are non-negative for valid transactions.
#[cfg_attr(feature = "spec-lock", spec_locked("6.5", "F_FeeNonNeg"))]
#[cfg_attr(feature = "spec-lock", blvm_spec_lock::requires(total_in >= total_out))]
#[cfg_attr(feature = "spec-lock", blvm_spec_lock::requires(total_out >= 0))]
pub(crate) fn _verify_f_fee_non_neg(total_in: i64, total_out: i64) -> i64 {
    total_in - total_out
}

// ─── §13.3.1 Integer Arithmetic Overflow/Underflow ───────────────────────────

/// Witness for **F_FeeArithmeticNonNeg** (PROTOCOL.md §13.3.1).
///
/// Proof obligation: fee arithmetic produces a non-negative result when inputs cover outputs.
///
/// Extends F_FeeNonNeg to the engineering invariant section: checked subtraction of valid
/// monetary values (both ≥ 0, with total_in ≥ total_out) cannot underflow.
#[cfg_attr(feature = "spec-lock", spec_locked("13.3.1", "F_FeeArithmeticNonNeg"))]
#[cfg_attr(feature = "spec-lock", blvm_spec_lock::requires(total_in >= total_out))]
#[cfg_attr(feature = "spec-lock", blvm_spec_lock::requires(total_in >= 0))]
#[cfg_attr(feature = "spec-lock", blvm_spec_lock::requires(total_out >= 0))]
pub(crate) fn _verify_f_fee_arithmetic_non_neg(total_in: i64, total_out: i64) -> i64 {
    total_in - total_out
}

/// Witness for **F_FeeArithmeticBounded** (PROTOCOL.md §13.3.1).
///
/// Proof obligation: fee ≤ total_in when total_in ≥ total_out ≥ 0.
///
/// Upper bound on fee: since total_out ≥ 0, the fee = total_in - total_out ≤ total_in.
/// This means no transaction can extract more in fees than its total input value.
#[cfg_attr(feature = "spec-lock", spec_locked("13.3.1", "F_FeeArithmeticBounded"))]
#[cfg_attr(feature = "spec-lock", blvm_spec_lock::requires(total_in >= total_out))]
#[cfg_attr(feature = "spec-lock", blvm_spec_lock::requires(total_in >= 0))]
#[cfg_attr(feature = "spec-lock", blvm_spec_lock::requires(total_out >= 0))]
#[cfg_attr(feature = "spec-lock", blvm_spec_lock::ensures(result <= total_in))]
pub(crate) fn _verify_f_fee_arithmetic_bounded(total_in: i64, total_out: i64) -> i64 {
    total_in - total_out
}

// ─── §13.3.3 Resource Limit Enforcement ──────────────────────────────────────

/// Witness for **F_CoinbaseScriptSigMin** (PROTOCOL.md §13.3.3).
///
/// Proof obligation: coinbase scriptSig length ≥ 2 (minimum length boundary).
///
/// The headroom above the minimum: `len - 2 ≥ 0` whenever `len ≥ 2`.
/// Z3 proves from `requires(len >= 2)` via linear arithmetic (same pattern as fee non-neg).
/// Formalises that a valid coinbase scriptSig satisfies the 2-byte minimum exactly.
#[cfg_attr(feature = "spec-lock", spec_locked("13.3.3", "F_CoinbaseScriptSigMin"))]
#[cfg_attr(feature = "spec-lock", blvm_spec_lock::requires(len >= 2))]
pub(crate) fn _verify_f_coinbase_scriptsig_min(len: i64) -> i64 {
    len - 2
}

/// Witness for **F_CoinbaseScriptSigMax** (PROTOCOL.md §13.3.3).
///
/// Proof obligation: coinbase scriptSig length ≤ 100 (maximum length boundary).
///
/// The distance below the maximum: `100 - len ≥ 0` whenever `len ≤ 100`.
/// Z3 proves from `requires(len <= 100)` via linear arithmetic.
/// Formalises that a valid coinbase scriptSig does not exceed the 100-byte maximum.
#[cfg_attr(feature = "spec-lock", spec_locked("13.3.3", "F_CoinbaseScriptSigMax"))]
#[cfg_attr(feature = "spec-lock", blvm_spec_lock::requires(len <= 100))]
pub(crate) fn _verify_f_coinbase_scriptsig_max(len: i64) -> i64 {
    100 - len
}

/// Witness for **F_StackSizeSafe** (PROTOCOL.md §13.3.3).
///
/// Proof obligation: stack depth headroom is non-negative when below the 1000-item limit.
///
/// `999 - depth ≥ 0` whenever `depth < 1000`. Z3 proves via linear arithmetic.
/// Formalises the stack-size invariant: a stack within the limit has non-negative headroom
/// before the consensus-critical overflow boundary.
#[cfg_attr(feature = "spec-lock", spec_locked("13.3.3", "F_StackSizeSafe"))]
#[cfg_attr(feature = "spec-lock", blvm_spec_lock::requires(depth >= 0))]
#[cfg_attr(feature = "spec-lock", blvm_spec_lock::requires(depth < 1000))]
pub(crate) fn _verify_f_stack_size_safe(depth: i64) -> i64 {
    999 - depth
}

/// Witness for **F_StackCombinedSafe** (PROTOCOL.md §13.3.3).
///
/// Combined stack+altstack headroom is non-negative at the 1000-item pass boundary.
#[cfg_attr(feature = "spec-lock", spec_locked("13.3.3", "F_StackCombinedSafe"))]
#[cfg_attr(feature = "spec-lock", blvm_spec_lock::requires(stack >= 0))]
#[cfg_attr(feature = "spec-lock", blvm_spec_lock::requires(alt >= 0))]
#[cfg_attr(feature = "spec-lock", blvm_spec_lock::requires(stack + alt <= 1000))]
pub(crate) fn _verify_f_stack_combined_safe(stack: i64, alt: i64) -> i64 {
    1000 - (stack + alt)
}

/// Witness for **F_StackCombinedFail** (PROTOCOL.md §13.3.3).
///
/// Excess past 1001 combined items is non-negative (1001 must fail).
#[cfg_attr(feature = "spec-lock", spec_locked("13.3.3", "F_StackCombinedFail"))]
#[cfg_attr(feature = "spec-lock", blvm_spec_lock::requires(stack >= 0))]
#[cfg_attr(feature = "spec-lock", blvm_spec_lock::requires(alt >= 0))]
#[cfg_attr(feature = "spec-lock", blvm_spec_lock::requires(stack + alt >= 1001))]
pub(crate) fn _verify_f_stack_combined_fail(stack: i64, alt: i64) -> i64 {
    (stack + alt) - 1001
}

// ─── §7.1 ExpandTarget ───────────────────────────────────────────────────────

/// Witness for **F_ExpandTargetZeroMantissa** (PROTOCOL.md §7.1).
///
/// Proof obligation: when `(bits & 0x007fffff) == 0`, `ExpandTarget(bits) == 0`.
///
/// Under `requires((bits & 0x007fffff) == 0)`, the mantissa field of the compact bits
/// word is zero. The expanded target formula is `mantissa × 2^(8*(exp-3)) = 0 × ... = 0`.
/// Z3 proves: `if mantissa == 0 { 0 } else { 1 }` returns `0` under the precondition
/// (same `if/else with unreachable branch` pattern as F_SubsidyZeroAfter64).
#[cfg_attr(
    feature = "spec-lock",
    spec_locked("7.1", "F_ExpandTargetZeroMantissa")
)]
#[cfg_attr(feature = "spec-lock", blvm_spec_lock::requires((bits & 0x007fffff) == 0))]
#[cfg_attr(feature = "spec-lock", blvm_spec_lock::ensures(result == 0))]
pub(crate) fn _verify_f_expand_target_zero_mantissa(bits: u64) -> i64 {
    let mantissa = bits & 0x007fffff;
    if mantissa == 0 { 0 } else { 1 } // else branch is unreachable under requires
}

/// Witness for **F_ExpandTargetExponent** (PROTOCOL.md §7.1).
///
/// Proof obligation: the exponent byte of the compact bits word is always in `[0, 255]`.
///
/// `exponent = (bits >> 24) & 0xFF`. The `& 0xFF` mask guarantees the result is at most `255`.
/// Since `& 0xFF` always produces a non-negative value, the result is also `>= 0`.
///
/// Z3 proves both bounds via bitwise arithmetic: `x & 0xFF` is bounded to `[0, 255]` by definition.
#[cfg_attr(feature = "spec-lock", spec_locked("7.1", "F_ExpandTargetExponent"))]
#[cfg_attr(feature = "spec-lock", blvm_spec_lock::ensures(result <= 255))]
pub(crate) fn _verify_f_expand_target_exponent(bits: i64) -> i64 {
    (bits >> 24) & 0xff
}

/// Witness for **F_ExpandTargetNonZeroMantissa** (PROTOCOL.md §7.1).
///
/// Proof obligation: when `(bits & 0x007fffff) != 0`, the sentinel result is non-zero.
///
/// Under `requires((bits & 0x007fffff) != 0)`, `mantissa != 0`, so the `else` branch
/// returns `1 != 0`. Complements F_ExpandTargetZeroMantissa: together they establish
/// the exact biconditional `mantissa == 0 ↔ target == 0`.
///
/// Z3 proves: `mantissa != 0` (from requires) + `if mantissa == 0 { 0 } else { 1 }`
/// ⊨ `result == 1` ⊨ `result != 0`.
#[cfg_attr(
    feature = "spec-lock",
    spec_locked("7.1", "F_ExpandTargetNonZeroMantissa")
)]
#[cfg_attr(feature = "spec-lock", blvm_spec_lock::requires((bits & 0x007fffff) != 0))]
#[cfg_attr(feature = "spec-lock", blvm_spec_lock::ensures(result != 0))]
pub(crate) fn _verify_f_expand_target_non_zero_mantissa(bits: u64) -> i64 {
    let mantissa = bits & 0x007fffff;
    if mantissa == 0 { 0 } else { 1 }
}

/// Witness for **F_RetargetIntervalCount** (PROTOCOL.md §7.1).
///
/// A 2016-block window spans 2015 inter-block intervals. Does not lock a
/// real-valued retarget fixed point.
#[cfg_attr(feature = "spec-lock", spec_locked("7.1", "F_RetargetIntervalCount"))]
#[cfg_attr(feature = "spec-lock", blvm_spec_lock::ensures(result == 2015))]
pub(crate) fn _verify_f_retarget_interval_count() -> i64 {
    let d = 2016;
    d - 1
}

/// Witness for **F_NextWorkClamped** (PROTOCOL.md §7.1).
///
/// Proof obligation: clamped compact bits are in `(0, MAX_TARGET]` with
/// `MAX_TARGET = 0x1d00ffff = 486604799`.
///
/// Under `requires(bits > 0)`, the else branch keeps `bits` or the then branch
/// returns the literal cap. Z3 sees both arms `> 0` and `<= 486604799`.
#[cfg_attr(feature = "spec-lock", spec_locked("7.1", "F_NextWorkClamped"))]
#[cfg_attr(feature = "spec-lock", blvm_spec_lock::requires(bits > 0))]
pub(crate) fn _verify_f_next_work_clamped(bits: i64) -> i64 {
    if bits > 486604799 { 486604799 } else { bits }
}

// ─── §6.1 GetBlockSubsidy ────────────────────────────────────────────────────

/// Witness for **F_SubsidyZeroAfter64** (PROTOCOL.md §6.1).
///
/// Proof obligation: `requires(height >= HALVING_INTERVAL * 64) ⊨ result == 0`
///
/// Z3 can prove this today using only integer division and comparison:
/// `k = height / 210_000`, and under the `requires`, `k ≥ 64`, so the `if`
/// branch is always taken and returns the literal `0`.
#[cfg_attr(feature = "spec-lock", spec_locked("6.1", "F_SubsidyZeroAfter64"))]
#[cfg_attr(feature = "spec-lock", blvm_spec_lock::requires(height >= HALVING_INTERVAL * 64))]
#[cfg_attr(feature = "spec-lock", blvm_spec_lock::ensures(result == 0))]
pub(crate) fn _verify_f_subsidy_zero_after_64(height: u64) -> i64 {
    let k = height / HALVING_INTERVAL;
    if k >= 64 {
        0
    } else {
        INITIAL_SUBSIDY // unreachable under the requires precondition
    }
}

/// Witness for **F_SubsidyZeroAfter33** (PROTOCOL.md §6.1).
///
/// Proof obligation: `requires(height >= HALVING_INTERVAL * 33) ⊨ result == 0`
///
/// Production still right-shifts for `33 ≤ k < 64`; those shifts are already 0.
/// This witness unrolls the same literal-RHS `match` as F_SubsidyPiecewise so Z3
/// sees `INITIAL_SUBSIDY >> 33` … `>> 63` as integer division, not a variable
/// shift. Do not rewrite this as `if k >= 33 { 0 }` — that is a different
/// function from GetBlockSubsidy.
#[cfg_attr(feature = "spec-lock", spec_locked("6.1", "F_SubsidyZeroAfter33"))]
#[cfg_attr(feature = "spec-lock", blvm_spec_lock::requires(height >= HALVING_INTERVAL * 33))]
#[cfg_attr(feature = "spec-lock", blvm_spec_lock::ensures(result == 0))]
pub(crate) fn _verify_f_subsidy_zero_after_33(height: u64) -> i64 {
    let k = height / HALVING_INTERVAL;
    match k {
        0 => INITIAL_SUBSIDY,
        1 => INITIAL_SUBSIDY >> 1,
        2 => INITIAL_SUBSIDY >> 2,
        3 => INITIAL_SUBSIDY >> 3,
        4 => INITIAL_SUBSIDY >> 4,
        5 => INITIAL_SUBSIDY >> 5,
        6 => INITIAL_SUBSIDY >> 6,
        7 => INITIAL_SUBSIDY >> 7,
        8 => INITIAL_SUBSIDY >> 8,
        9 => INITIAL_SUBSIDY >> 9,
        10 => INITIAL_SUBSIDY >> 10,
        11 => INITIAL_SUBSIDY >> 11,
        12 => INITIAL_SUBSIDY >> 12,
        13 => INITIAL_SUBSIDY >> 13,
        14 => INITIAL_SUBSIDY >> 14,
        15 => INITIAL_SUBSIDY >> 15,
        16 => INITIAL_SUBSIDY >> 16,
        17 => INITIAL_SUBSIDY >> 17,
        18 => INITIAL_SUBSIDY >> 18,
        19 => INITIAL_SUBSIDY >> 19,
        20 => INITIAL_SUBSIDY >> 20,
        21 => INITIAL_SUBSIDY >> 21,
        22 => INITIAL_SUBSIDY >> 22,
        23 => INITIAL_SUBSIDY >> 23,
        24 => INITIAL_SUBSIDY >> 24,
        25 => INITIAL_SUBSIDY >> 25,
        26 => INITIAL_SUBSIDY >> 26,
        27 => INITIAL_SUBSIDY >> 27,
        28 => INITIAL_SUBSIDY >> 28,
        29 => INITIAL_SUBSIDY >> 29,
        30 => INITIAL_SUBSIDY >> 30,
        31 => INITIAL_SUBSIDY >> 31,
        32 => INITIAL_SUBSIDY >> 32,
        33 => INITIAL_SUBSIDY >> 33,
        34 => INITIAL_SUBSIDY >> 34,
        35 => INITIAL_SUBSIDY >> 35,
        36 => INITIAL_SUBSIDY >> 36,
        37 => INITIAL_SUBSIDY >> 37,
        38 => INITIAL_SUBSIDY >> 38,
        39 => INITIAL_SUBSIDY >> 39,
        40 => INITIAL_SUBSIDY >> 40,
        41 => INITIAL_SUBSIDY >> 41,
        42 => INITIAL_SUBSIDY >> 42,
        43 => INITIAL_SUBSIDY >> 43,
        44 => INITIAL_SUBSIDY >> 44,
        45 => INITIAL_SUBSIDY >> 45,
        46 => INITIAL_SUBSIDY >> 46,
        47 => INITIAL_SUBSIDY >> 47,
        48 => INITIAL_SUBSIDY >> 48,
        49 => INITIAL_SUBSIDY >> 49,
        50 => INITIAL_SUBSIDY >> 50,
        51 => INITIAL_SUBSIDY >> 51,
        52 => INITIAL_SUBSIDY >> 52,
        53 => INITIAL_SUBSIDY >> 53,
        54 => INITIAL_SUBSIDY >> 54,
        55 => INITIAL_SUBSIDY >> 55,
        56 => INITIAL_SUBSIDY >> 56,
        57 => INITIAL_SUBSIDY >> 57,
        58 => INITIAL_SUBSIDY >> 58,
        59 => INITIAL_SUBSIDY >> 59,
        60 => INITIAL_SUBSIDY >> 60,
        61 => INITIAL_SUBSIDY >> 61,
        62 => INITIAL_SUBSIDY >> 62,
        63 => INITIAL_SUBSIDY >> 63,
        _ => 0,
    }
}

/// Witness for **F_SubsidyPiecewise** (PROTOCOL.md §6.1).
///
/// Uses a 64-arm `match` with **literal** shift amounts in each arm.
/// Z3 translates `INITIAL_SUBSIDY >> 0` → `INITIAL_SUBSIDY / 1`,
/// `INITIAL_SUBSIDY >> 1` → `INITIAL_SUBSIDY / 2`, etc.
/// The production function uses `>> halving_period` (variable RHS, fails Z3);
/// this witness avoids that by unrolling the 64 epochs.
#[cfg_attr(feature = "spec-lock", spec_locked("6.1", "F_SubsidyPiecewise"))]
#[cfg_attr(feature = "spec-lock", blvm_spec_lock::ensures(
    result >= 0
))]
#[cfg_attr(feature = "spec-lock", blvm_spec_lock::ensures(
    result <= INITIAL_SUBSIDY
))]
pub(crate) fn _verify_f_subsidy_piecewise(height: u64) -> i64 {
    let k = height / HALVING_INTERVAL;
    match k {
        0 => INITIAL_SUBSIDY,
        1 => INITIAL_SUBSIDY >> 1,
        2 => INITIAL_SUBSIDY >> 2,
        3 => INITIAL_SUBSIDY >> 3,
        4 => INITIAL_SUBSIDY >> 4,
        5 => INITIAL_SUBSIDY >> 5,
        6 => INITIAL_SUBSIDY >> 6,
        7 => INITIAL_SUBSIDY >> 7,
        8 => INITIAL_SUBSIDY >> 8,
        9 => INITIAL_SUBSIDY >> 9,
        10 => INITIAL_SUBSIDY >> 10,
        11 => INITIAL_SUBSIDY >> 11,
        12 => INITIAL_SUBSIDY >> 12,
        13 => INITIAL_SUBSIDY >> 13,
        14 => INITIAL_SUBSIDY >> 14,
        15 => INITIAL_SUBSIDY >> 15,
        16 => INITIAL_SUBSIDY >> 16,
        17 => INITIAL_SUBSIDY >> 17,
        18 => INITIAL_SUBSIDY >> 18,
        19 => INITIAL_SUBSIDY >> 19,
        20 => INITIAL_SUBSIDY >> 20,
        21 => INITIAL_SUBSIDY >> 21,
        22 => INITIAL_SUBSIDY >> 22,
        23 => INITIAL_SUBSIDY >> 23,
        24 => INITIAL_SUBSIDY >> 24,
        25 => INITIAL_SUBSIDY >> 25,
        26 => INITIAL_SUBSIDY >> 26,
        27 => INITIAL_SUBSIDY >> 27,
        28 => INITIAL_SUBSIDY >> 28,
        29 => INITIAL_SUBSIDY >> 29,
        30 => INITIAL_SUBSIDY >> 30,
        31 => INITIAL_SUBSIDY >> 31,
        32 => INITIAL_SUBSIDY >> 32,
        33 => INITIAL_SUBSIDY >> 33,
        34 => INITIAL_SUBSIDY >> 34,
        35 => INITIAL_SUBSIDY >> 35,
        36 => INITIAL_SUBSIDY >> 36,
        37 => INITIAL_SUBSIDY >> 37,
        38 => INITIAL_SUBSIDY >> 38,
        39 => INITIAL_SUBSIDY >> 39,
        40 => INITIAL_SUBSIDY >> 40,
        41 => INITIAL_SUBSIDY >> 41,
        42 => INITIAL_SUBSIDY >> 42,
        43 => INITIAL_SUBSIDY >> 43,
        44 => INITIAL_SUBSIDY >> 44,
        45 => INITIAL_SUBSIDY >> 45,
        46 => INITIAL_SUBSIDY >> 46,
        47 => INITIAL_SUBSIDY >> 47,
        48 => INITIAL_SUBSIDY >> 48,
        49 => INITIAL_SUBSIDY >> 49,
        50 => INITIAL_SUBSIDY >> 50,
        51 => INITIAL_SUBSIDY >> 51,
        52 => INITIAL_SUBSIDY >> 52,
        53 => INITIAL_SUBSIDY >> 53,
        54 => INITIAL_SUBSIDY >> 54,
        55 => INITIAL_SUBSIDY >> 55,
        56 => INITIAL_SUBSIDY >> 56,
        57 => INITIAL_SUBSIDY >> 57,
        58 => INITIAL_SUBSIDY >> 58,
        59 => INITIAL_SUBSIDY >> 59,
        60 => INITIAL_SUBSIDY >> 60,
        61 => INITIAL_SUBSIDY >> 61,
        62 => INITIAL_SUBSIDY >> 62,
        63 => INITIAL_SUBSIDY >> 63,
        _ => 0,
    }
}

/// Witness for **F_SubsidyFloorHalf** (PROTOCOL.md §6.1).
///
/// Integer floor-half at odd k=9 (real-valued /2 fails here):
/// `(INITIAL_SUBSIDY >> 10) - (INITIAL_SUBSIDY >> 9) / 2 == 0`.
/// Literal shift RHS only.
#[cfg_attr(feature = "spec-lock", spec_locked("6.1", "F_SubsidyFloorHalf"))]
#[cfg_attr(feature = "spec-lock", blvm_spec_lock::ensures(result == 0))]
pub(crate) fn _verify_f_subsidy_floor_half() -> i64 {
    let prev = INITIAL_SUBSIDY >> 9;
    let next = INITIAL_SUBSIDY >> 10;
    next - prev / 2
}

// ─── §6.2 TotalSupply ────────────────────────────────────────────────────────

/// Witness for **F_TotalSupplyNonNeg** (PROTOCOL.md §6.2).
///
/// Proof obligation: within the first halving epoch, total supply = (height+1) * INITIAL_SUBSIDY ≥ 0.
///
/// Z3 proves this via linear arithmetic: `height ≥ 0` (u64) and `INITIAL_SUBSIDY > 0`
/// imply `(height + 1) * INITIAL_SUBSIDY > 0 ≥ 0`.
/// The full inductive proof over all epochs requires Kani (Track E).
#[cfg_attr(feature = "spec-lock", spec_locked("6.2", "F_TotalSupplyNonNeg"))]
#[cfg_attr(feature = "spec-lock", blvm_spec_lock::requires(height < HALVING_INTERVAL))]
pub(crate) fn _verify_f_total_supply_non_neg(height: u64) -> i64 {
    (height as i64 + 1) * INITIAL_SUBSIDY
}

/// Witness for **F_TotalSupplyMonoStep** (PROTOCOL.md §6.2).
///
/// Proof obligation: `supply + subsidy >= supply` when both are non-negative.
///
/// One-step monotonicity of TotalSupply. Z3 proves via linear arithmetic from
/// `requires(subsidy >= 0)`. The ∀ over heights is this step plus
/// F_SubsidyPiecewise (`subsidy >= 0`).
#[cfg_attr(feature = "spec-lock", spec_locked("6.2", "F_TotalSupplyMonoStep"))]
#[cfg_attr(feature = "spec-lock", blvm_spec_lock::requires(supply >= 0))]
#[cfg_attr(feature = "spec-lock", blvm_spec_lock::requires(subsidy >= 0))]
pub(crate) fn _verify_f_total_supply_mono_step(supply: i64, subsidy: i64) -> i64 {
    supply + subsidy
}

/// Witness for **F_TotalSupplyBound** (PROTOCOL.md §6.2).
///
/// Proof obligation: within the first halving epoch, total supply ≤ MAX_MONEY.
///
/// First-epoch maximum: HALVING_INTERVAL * INITIAL_SUBSIDY = 210_000 * 5_000_000_000
/// = 1_050_000_000_000_000 < 2_100_000_000_000_000 = MAX_MONEY.
/// Z3 proves this via linear arithmetic. Full inductive proof requires Kani (Track E).
#[cfg_attr(feature = "spec-lock", spec_locked("6.2", "F_TotalSupplyBound"))]
#[cfg_attr(feature = "spec-lock", blvm_spec_lock::requires(height < HALVING_INTERVAL))]
#[cfg_attr(feature = "spec-lock", blvm_spec_lock::ensures(result <= MAX_MONEY))]
pub(crate) fn _verify_f_total_supply_bound(height: u64) -> i64 {
    (height as i64 + 1) * INITIAL_SUBSIDY
}

/// Witness for **F_TotalSupplyExact** (PROTOCOL.md §6.2).
///
/// Proof obligation: `H * Σ_{k=0..32} (INITIAL_SUBSIDY >> k) == 2_099_999_997_690_000`.
/// Computes the sum from literal shifts. Does not return the constant and does
/// not call production `total_supply` (loop; Z3-out-of-scope).
#[cfg_attr(feature = "spec-lock", spec_locked("6.2", "F_TotalSupplyExact"))]
#[cfg_attr(feature = "spec-lock", blvm_spec_lock::ensures(result == 2099999997690000))]
// Keep `INITIAL_SUBSIDY >> 0` in the unrolled sum so Z3 sees a literal-RHS shift
// (same piecewise pattern as F_SubsidyPiecewise); not an accidental identity.
#[allow(clippy::identity_op)]
pub(crate) fn _verify_f_total_supply_exact() -> i64 {
    (HALVING_INTERVAL as i64)
        * ((INITIAL_SUBSIDY >> 0)
            + (INITIAL_SUBSIDY >> 1)
            + (INITIAL_SUBSIDY >> 2)
            + (INITIAL_SUBSIDY >> 3)
            + (INITIAL_SUBSIDY >> 4)
            + (INITIAL_SUBSIDY >> 5)
            + (INITIAL_SUBSIDY >> 6)
            + (INITIAL_SUBSIDY >> 7)
            + (INITIAL_SUBSIDY >> 8)
            + (INITIAL_SUBSIDY >> 9)
            + (INITIAL_SUBSIDY >> 10)
            + (INITIAL_SUBSIDY >> 11)
            + (INITIAL_SUBSIDY >> 12)
            + (INITIAL_SUBSIDY >> 13)
            + (INITIAL_SUBSIDY >> 14)
            + (INITIAL_SUBSIDY >> 15)
            + (INITIAL_SUBSIDY >> 16)
            + (INITIAL_SUBSIDY >> 17)
            + (INITIAL_SUBSIDY >> 18)
            + (INITIAL_SUBSIDY >> 19)
            + (INITIAL_SUBSIDY >> 20)
            + (INITIAL_SUBSIDY >> 21)
            + (INITIAL_SUBSIDY >> 22)
            + (INITIAL_SUBSIDY >> 23)
            + (INITIAL_SUBSIDY >> 24)
            + (INITIAL_SUBSIDY >> 25)
            + (INITIAL_SUBSIDY >> 26)
            + (INITIAL_SUBSIDY >> 27)
            + (INITIAL_SUBSIDY >> 28)
            + (INITIAL_SUBSIDY >> 29)
            + (INITIAL_SUBSIDY >> 30)
            + (INITIAL_SUBSIDY >> 31)
            + (INITIAL_SUBSIDY >> 32))
}

/// Witness for **F_IssuedSupplyBelowCap** (PROTOCOL.md §6.2).
///
/// Same unrolled sum as F_TotalSupplyExact. Obligation: that sum ≤ MAX_MONEY.
/// Closed form for all epochs; does not rewrite F_TotalSupplyBound.
#[cfg_attr(feature = "spec-lock", spec_locked("6.2", "F_IssuedSupplyBelowCap"))]
#[cfg_attr(feature = "spec-lock", blvm_spec_lock::ensures(result <= MAX_MONEY))]
// Keep `INITIAL_SUBSIDY >> 0` for Z3 literal-RHS shift uniformity with Exact.
#[allow(clippy::identity_op)]
pub(crate) fn _verify_f_issued_supply_below_cap() -> i64 {
    (HALVING_INTERVAL as i64)
        * ((INITIAL_SUBSIDY >> 0)
            + (INITIAL_SUBSIDY >> 1)
            + (INITIAL_SUBSIDY >> 2)
            + (INITIAL_SUBSIDY >> 3)
            + (INITIAL_SUBSIDY >> 4)
            + (INITIAL_SUBSIDY >> 5)
            + (INITIAL_SUBSIDY >> 6)
            + (INITIAL_SUBSIDY >> 7)
            + (INITIAL_SUBSIDY >> 8)
            + (INITIAL_SUBSIDY >> 9)
            + (INITIAL_SUBSIDY >> 10)
            + (INITIAL_SUBSIDY >> 11)
            + (INITIAL_SUBSIDY >> 12)
            + (INITIAL_SUBSIDY >> 13)
            + (INITIAL_SUBSIDY >> 14)
            + (INITIAL_SUBSIDY >> 15)
            + (INITIAL_SUBSIDY >> 16)
            + (INITIAL_SUBSIDY >> 17)
            + (INITIAL_SUBSIDY >> 18)
            + (INITIAL_SUBSIDY >> 19)
            + (INITIAL_SUBSIDY >> 20)
            + (INITIAL_SUBSIDY >> 21)
            + (INITIAL_SUBSIDY >> 22)
            + (INITIAL_SUBSIDY >> 23)
            + (INITIAL_SUBSIDY >> 24)
            + (INITIAL_SUBSIDY >> 25)
            + (INITIAL_SUBSIDY >> 26)
            + (INITIAL_SUBSIDY >> 27)
            + (INITIAL_SUBSIDY >> 28)
            + (INITIAL_SUBSIDY >> 29)
            + (INITIAL_SUBSIDY >> 30)
            + (INITIAL_SUBSIDY >> 31)
            + (INITIAL_SUBSIDY >> 32))
}

// ─── §5.5 Sequence Locks ─────────────────────────────────────────────────────

/// Witness for **F_SequenceLockTimeMask** (PROTOCOL.md §5.5).
///
/// Proof obligation: `ExtractSequenceLocktimeValue(seq) <= 65535`.
///
/// The body is `seq & 0x0000_ffff` — a bitwise AND with a literal mask. Z3 translates
/// bitwise AND with a literal, then proves `result <= 65535` from the mask property.
/// Genuine algebraic constraint: the 16-bit mask guarantees the upper bound.
#[cfg_attr(feature = "spec-lock", spec_locked("5.5", "F_SequenceLockTimeMask"))]
#[cfg_attr(feature = "spec-lock", blvm_spec_lock::ensures(result <= 65535))]
pub(crate) fn _verify_f_sequence_locktime_mask(seq: u64) -> u64 {
    seq & 0x0000_ffff
}

/// Witness for **F_EvalSeqLocksDisabled** (PROTOCOL.md §5.5).
///
/// Proof obligation: when both locks are disabled (`min_height == -1`, `min_time == -1`),
/// `EvaluateSequenceLocks` always returns `true`.
///
/// Z3 proves: under the two `requires` guards, `min_height < 0` and `min_time < 0` are
/// both `true`, so each `(flag < 0 || ...)` clause short-circuits to `true`, giving
/// `true && true == true`.
#[cfg_attr(feature = "spec-lock", spec_locked("5.5", "F_EvalSeqLocksDisabled"))]
#[cfg_attr(feature = "spec-lock", blvm_spec_lock::requires(min_height == -1))]
#[cfg_attr(feature = "spec-lock", blvm_spec_lock::requires(min_time == -1))]
#[cfg_attr(feature = "spec-lock", blvm_spec_lock::ensures(result == true))]
pub(crate) fn _verify_f_eval_seq_locks_disabled(
    height: i64,
    time: i64,
    min_height: i64,
    min_time: i64,
) -> bool {
    (min_height < 0 || height > min_height) && (min_time < 0 || time > min_time)
}

/// Witness for **F_MtpIndex** (PROTOCOL.md §5.5).
///
/// Even n=2, already sorted `t0 <= t1`: upper middle is index `2/2 = 1` (`t1`),
/// not the mean `(t0+t1)/2`. Array index is a fresh Z3 int, so this uses the
/// same if/else-with-unreachable-branch pattern as F_SubsidyZeroAfter64.
#[cfg_attr(feature = "spec-lock", spec_locked("5.5", "F_MtpIndex"))]
#[cfg_attr(feature = "spec-lock", blvm_spec_lock::requires(t0 <= t1))]
#[cfg_attr(feature = "spec-lock", blvm_spec_lock::ensures(result == t1))]
// `2 / 2` is the even-n upper-middle index formula with n=2 (same shape as `4/2`, `11/2`).
#[allow(clippy::eq_op)]
pub(crate) fn _verify_f_mtp_index(t0: i64, t1: i64) -> i64 {
    let mid_index = 2 / 2;
    if mid_index == 1 {
        t1
    } else {
        (t0 + t1) / 2 // unreachable: the even-n mean lie
    }
}

/// Witness for **F_MtpIndexN4** (PROTOCOL.md §5.5).
///
/// Even n=4, already sorted: upper middle is index `4/2 = 2` (`t2`), not
/// `(t1+t2)/2`. Complements F_MtpIndex (n=2).
#[cfg_attr(feature = "spec-lock", spec_locked("5.5", "F_MtpIndexN4"))]
#[cfg_attr(feature = "spec-lock", blvm_spec_lock::requires(t0 <= t1))]
#[cfg_attr(feature = "spec-lock", blvm_spec_lock::requires(t1 <= t2))]
#[cfg_attr(feature = "spec-lock", blvm_spec_lock::requires(t2 <= t3))]
#[cfg_attr(feature = "spec-lock", blvm_spec_lock::ensures(result == t2))]
#[allow(unused_variables)]
pub(crate) fn _verify_f_mtp_index_n4(t0: i64, t1: i64, t2: i64, t3: i64) -> i64 {
    let mid_index = 4 / 2;
    if mid_index == 2 {
        t2
    } else {
        (t1 + t2) / 2 // unreachable: mean of the two central values
    }
}

/// Witness for **F_MtpIndexN11** (PROTOCOL.md §5.5).
///
/// BIP113 window: n=11, already sorted. Median is index `11/2 = 5` (`t5`).
#[cfg_attr(feature = "spec-lock", spec_locked("5.5", "F_MtpIndexN11"))]
#[cfg_attr(feature = "spec-lock", blvm_spec_lock::requires(t0 <= t1))]
#[cfg_attr(feature = "spec-lock", blvm_spec_lock::requires(t1 <= t2))]
#[cfg_attr(feature = "spec-lock", blvm_spec_lock::requires(t2 <= t3))]
#[cfg_attr(feature = "spec-lock", blvm_spec_lock::requires(t3 <= t4))]
#[cfg_attr(feature = "spec-lock", blvm_spec_lock::requires(t4 <= t5))]
#[cfg_attr(feature = "spec-lock", blvm_spec_lock::requires(t5 <= t6))]
#[cfg_attr(feature = "spec-lock", blvm_spec_lock::requires(t6 <= t7))]
#[cfg_attr(feature = "spec-lock", blvm_spec_lock::requires(t7 <= t8))]
#[cfg_attr(feature = "spec-lock", blvm_spec_lock::requires(t8 <= t9))]
#[cfg_attr(feature = "spec-lock", blvm_spec_lock::requires(t9 <= t10))]
#[cfg_attr(feature = "spec-lock", blvm_spec_lock::ensures(result == t5))]
#[allow(unused_variables)]
pub(crate) fn _verify_f_mtp_index_n11(
    t0: i64,
    t1: i64,
    t2: i64,
    t3: i64,
    t4: i64,
    t5: i64,
    t6: i64,
    t7: i64,
    t8: i64,
    t9: i64,
    t10: i64,
) -> i64 {
    let mid_index = 11 / 2;
    if mid_index == 5 { t5 } else { t0 }
}

// ─── §13.3.5 Integration Proofs ──────────────────────────────────────────────

/// Witness for **F_LocktimeTypeIsHeight** (PROTOCOL.md §13.3.5).
///
/// Proof obligation: headroom below LOCKTIME_THRESHOLD is non-negative when lt < 500,000,000.
///
/// `500_000_000 - lt ≥ 0` whenever `lt < 500_000_000` (block-height locktime range).
/// Z3 proves via linear arithmetic from `requires(lt < 500_000_000)`.
/// Formalises: a locktime below the threshold is unambiguously in the block-height range.
#[cfg_attr(feature = "spec-lock", spec_locked("13.3.5", "F_LocktimeTypeIsHeight"))]
#[cfg_attr(feature = "spec-lock", blvm_spec_lock::requires(lt >= 0))]
#[cfg_attr(feature = "spec-lock", blvm_spec_lock::requires(lt < 500000000))]
pub(crate) fn _verify_f_locktime_type_is_height(lt: i64) -> i64 {
    500_000_000 - lt
}

/// Witness for **F_LocktimeTypeIsTimestamp** (PROTOCOL.md §13.3.5).
///
/// Proof obligation: excess above LOCKTIME_THRESHOLD is non-negative when lt ≥ 500,000,000.
///
/// `lt - 500_000_000 ≥ 0` whenever `lt ≥ 500_000_000` (timestamp locktime range).
/// Z3 proves via linear arithmetic from `requires(lt >= 500_000_000)`.
/// Formalises: a locktime at or above the threshold is unambiguously in the timestamp range.
#[cfg_attr(
    feature = "spec-lock",
    spec_locked("13.3.5", "F_LocktimeTypeIsTimestamp")
)]
#[cfg_attr(feature = "spec-lock", blvm_spec_lock::requires(lt >= 500000000))]
pub(crate) fn _verify_f_locktime_type_is_timestamp(lt: i64) -> i64 {
    lt - 500_000_000
}

/// Witness for **F_EvalSeqLocksHeightNotMet** (PROTOCOL.md §5.5).
///
/// Proof obligation: when a minimum block height is active (`min_height >= 0`) and
/// the current block height does not exceed it (`block_height <= min_height`),
/// EvaluateSequenceLocks returns false.
///
/// Under `requires(min_height >= 0)`, the guard `min_height < 0` is `false`,
/// so the first clause becomes `false || block_height > min_height`.
/// Under `requires(block_height <= min_height)`, `block_height > min_height` is also `false`.
/// So the first clause is `false`, and `false && (any) = false`.
///
/// Proves the height-not-met invariant: a CSV-relative-height-locked transaction cannot
/// be finalized in a block at the lock height or below.
#[cfg_attr(
    feature = "spec-lock",
    spec_locked("5.5", "F_EvalSeqLocksHeightNotMet")
)]
#[cfg_attr(feature = "spec-lock", blvm_spec_lock::requires(min_height >= 0))]
#[cfg_attr(feature = "spec-lock", blvm_spec_lock::requires(block_height <= min_height))]
#[cfg_attr(feature = "spec-lock", blvm_spec_lock::ensures(result == false))]
pub(crate) fn _verify_f_eval_seq_locks_height_not_met(
    block_height: i64,
    time: i64,
    min_height: i64,
    min_time: i64,
) -> bool {
    (min_height < 0 || block_height > min_height) && (min_time < 0 || time > min_time)
}

/// Witness for **F_SequenceTimeEncoding** (PROTOCOL.md §5.5).
///
/// Proof obligation: `value * 512 ≤ 33,553,920` when `value ≤ 65535`.
///
/// The time-based relative locktime is expressed in 512-second units.
/// With the 16-bit value field bounded by `65535`, the maximum encoded time is
/// `65535 × 512 = 33,553,920` seconds. Z3 proves via linear arithmetic:
/// `requires(value >= 0)` + `requires(value <= 65535)` ⊨ `value * 512 <= 33_553_920`.
#[cfg_attr(feature = "spec-lock", spec_locked("5.5", "F_SequenceTimeEncoding"))]
#[cfg_attr(feature = "spec-lock", blvm_spec_lock::requires(value >= 0))]
#[cfg_attr(feature = "spec-lock", blvm_spec_lock::requires(value <= 65535))]
#[cfg_attr(feature = "spec-lock", blvm_spec_lock::ensures(result <= 33553920))]
pub(crate) fn _verify_f_sequence_time_encoding(value: i64) -> i64 {
    value * 512
}

/// Witness for **F_SequenceLockHeightAdd** (PROTOCOL.md §5.5).
///
/// Proof obligation: `ph + lock - 1 >= -1` when `ph >= 0` and
/// `0 <= lock <= 65535` (16-bit mask).
///
/// BIP68 last-invalid height. `ph <= 2147483647` keeps the add inside i64.
#[cfg_attr(feature = "spec-lock", spec_locked("5.5", "F_SequenceLockHeightAdd"))]
#[cfg_attr(feature = "spec-lock", blvm_spec_lock::requires(ph >= 0))]
#[cfg_attr(feature = "spec-lock", blvm_spec_lock::requires(lock >= 0))]
#[cfg_attr(feature = "spec-lock", blvm_spec_lock::requires(lock <= 65535))]
#[cfg_attr(feature = "spec-lock", blvm_spec_lock::requires(ph <= 2147483647))]
pub(crate) fn _verify_f_sequence_lock_height_add(ph: i64, lock: i64) -> i64 {
    ph + lock - 1
}

// ─── §5.4.7 BIP65: OP_CHECKLOCKTIMEVERIFY (CLTV) ─────────────────────────────

/// Witness for **F_BIP65PassesZeroZero** (PROTOCOL.md §5.4.7).
///
/// Proof obligation: `(0, 0)` passes BIP65Check (block 659901).
/// Same predicate as production `check_bip65`: types match and `tx >= stack`.
/// No `tx_locktime != 0` guard.
#[cfg_attr(feature = "spec-lock", spec_locked("5.4.7", "F_BIP65PassesZeroZero"))]
#[cfg_attr(feature = "spec-lock", blvm_spec_lock::requires(tx_locktime == 0))]
#[cfg_attr(feature = "spec-lock", blvm_spec_lock::requires(stack_locktime == 0))]
#[cfg_attr(feature = "spec-lock", blvm_spec_lock::ensures(result == true))]
pub(crate) fn _verify_f_bip65_passes_zero_zero(tx_locktime: u32, stack_locktime: u32) -> bool {
    let tx_is_height = tx_locktime < LOCKTIME_THRESHOLD;
    let sk_is_height = stack_locktime < LOCKTIME_THRESHOLD;
    (tx_is_height == sk_is_height) && tx_locktime >= stack_locktime
}

/// Witness for **F_BIP65RejectsTypeMismatch** (PROTOCOL.md §5.4.7).
///
/// Proof obligation: CLTV validation always fails when the tx and script locktime
/// types differ (block-height vs. timestamp).
///
/// Under `requires(tx_locktime < LOCKTIME_THRESHOLD)` (block-height type) and
/// `requires(stack_locktime >= LOCKTIME_THRESHOLD)` (timestamp type), the type
/// comparison `tx_is_height == sk_is_height` is `true == false` = `false`,
/// so the whole check short-circuits to `false`.
///
/// Proves the cross-type incompatibility invariant: a timestamp-CLTV script cannot
/// be satisfied by a transaction using a block-height nLockTime, and vice versa.
#[cfg_attr(
    feature = "spec-lock",
    spec_locked("5.4.7", "F_BIP65RejectsTypeMismatch")
)]
#[cfg_attr(feature = "spec-lock", blvm_spec_lock::requires(tx_locktime < LOCKTIME_THRESHOLD))]
#[cfg_attr(feature = "spec-lock", blvm_spec_lock::requires(stack_locktime >= LOCKTIME_THRESHOLD))]
#[cfg_attr(feature = "spec-lock", blvm_spec_lock::ensures(result == false))]
pub(crate) fn _verify_f_bip65_rejects_type_mismatch(tx_locktime: u32, stack_locktime: u32) -> bool {
    let tx_is_height = tx_locktime < LOCKTIME_THRESHOLD;
    let sk_is_height = stack_locktime < LOCKTIME_THRESHOLD;
    (tx_is_height == sk_is_height) && tx_locktime >= stack_locktime
}

/// Witness for **F_BIP65RejectsTypeMismatchReverse** (PROTOCOL.md §5.4.7).
///
/// Proof obligation: CLTV validation fails when `tx_locktime` is a timestamp
/// but `stack_locktime` is a block-height (the reverse mismatch direction).
///
/// Under `requires(tx_locktime >= LOCKTIME_THRESHOLD)`: `tx_is_height = false`.
/// Under `requires(stack_locktime < LOCKTIME_THRESHOLD)`: `sk_is_height = true`.
/// `tx_is_height == sk_is_height` = `false == true` = `false`.
/// The conjunction includes `false`, so result = `false`.
///
/// Proves that a timestamp-type transaction cannot satisfy a block-height CLTV script.
#[cfg_attr(
    feature = "spec-lock",
    spec_locked("5.4.7", "F_BIP65RejectsTypeMismatchReverse")
)]
#[cfg_attr(feature = "spec-lock", blvm_spec_lock::requires(tx_locktime >= LOCKTIME_THRESHOLD))]
#[cfg_attr(feature = "spec-lock", blvm_spec_lock::requires(stack_locktime < LOCKTIME_THRESHOLD))]
#[cfg_attr(feature = "spec-lock", blvm_spec_lock::ensures(result == false))]
pub(crate) fn _verify_f_bip65_rejects_type_mismatch_reverse(
    tx_locktime: u32,
    stack_locktime: u32,
) -> bool {
    let tx_is_height = tx_locktime < LOCKTIME_THRESHOLD;
    let sk_is_height = stack_locktime < LOCKTIME_THRESHOLD;
    (tx_is_height == sk_is_height) && tx_locktime >= stack_locktime
}

/// Witness for **F_BIP65RejectsValueTooLow** (PROTOCOL.md §5.4.7).
///
/// Proof obligation: CLTV validation fails when both locktimes are block-heights
/// but `tx_locktime < stack_locktime` (value doesn't meet the script minimum).
///
/// Under all `requires`: `tx_locktime != 0` = true, `tx_is_height == sk_is_height` = true,
/// but `tx_locktime >= stack_locktime` = false (requires: tx_locktime < stack_locktime).
/// The conjunction includes `false`, so result = `false`.
///
/// Proves that even type-matching locktimes are rejected when the transaction locktime
/// fails to meet the script-specified minimum.
#[cfg_attr(
    feature = "spec-lock",
    spec_locked("5.4.7", "F_BIP65RejectsValueTooLow")
)]
#[cfg_attr(feature = "spec-lock", blvm_spec_lock::requires(tx_locktime > 0))]
#[cfg_attr(feature = "spec-lock", blvm_spec_lock::requires(tx_locktime < LOCKTIME_THRESHOLD))]
#[cfg_attr(feature = "spec-lock", blvm_spec_lock::requires(stack_locktime < LOCKTIME_THRESHOLD))]
#[cfg_attr(feature = "spec-lock", blvm_spec_lock::requires(tx_locktime < stack_locktime))]
#[cfg_attr(feature = "spec-lock", blvm_spec_lock::ensures(result == false))]
pub(crate) fn _verify_f_bip65_rejects_value_too_low(tx_locktime: u32, stack_locktime: u32) -> bool {
    let tx_is_height = tx_locktime < LOCKTIME_THRESHOLD;
    let sk_is_height = stack_locktime < LOCKTIME_THRESHOLD;
    (tx_is_height == sk_is_height) && tx_locktime >= stack_locktime
}

/// Witness for **F_BIP65RejectsTimestampValueTooLow** (PROTOCOL.md §5.4.7).
///
/// Proof obligation: CLTV validation fails when both locktimes are timestamps
/// but `tx_locktime < stack_locktime` (value does not meet script minimum).
///
/// Under all `requires`: both are timestamps (`tx_is_height = false`, `sk_is_height = false`),
/// types match (`false == false = true`), `tx_locktime != 0` = true (implied by >= LOCKTIME_THRESHOLD),
/// but `tx_locktime >= stack_locktime` = false (requires: tx_locktime < stack_locktime).
/// Result = `true && true && false` = `false`.
///
/// Completes the BIP65 case analysis: every logically distinct input combination is now
/// covered by a formally verified witness — rejection and acceptance for both domains.
#[cfg_attr(
    feature = "spec-lock",
    spec_locked("5.4.7", "F_BIP65RejectsTimestampValueTooLow")
)]
#[cfg_attr(feature = "spec-lock", blvm_spec_lock::requires(tx_locktime >= LOCKTIME_THRESHOLD))]
#[cfg_attr(feature = "spec-lock", blvm_spec_lock::requires(stack_locktime >= LOCKTIME_THRESHOLD))]
#[cfg_attr(feature = "spec-lock", blvm_spec_lock::requires(tx_locktime < stack_locktime))]
#[cfg_attr(feature = "spec-lock", blvm_spec_lock::requires(tx_locktime > 0))]
#[cfg_attr(feature = "spec-lock", blvm_spec_lock::ensures(result == false))]
pub(crate) fn _verify_f_bip65_rejects_timestamp_value_too_low(
    tx_locktime: u32,
    stack_locktime: u32,
) -> bool {
    let tx_is_height = tx_locktime < LOCKTIME_THRESHOLD;
    let sk_is_height = stack_locktime < LOCKTIME_THRESHOLD;
    (tx_is_height == sk_is_height) && tx_locktime >= stack_locktime
}

/// Witness for **F_BIP65Passes** (PROTOCOL.md §5.4.7).
///
/// Proof obligation: CLTV validation passes when all four conditions hold simultaneously:
/// `tx_locktime > 0`, both are block-heights (`< LOCKTIME_THRESHOLD`), and
/// `tx_locktime >= stack_locktime`.
///
/// Under the four `requires` clauses:
/// - `tx_locktime != 0` → true (tx_locktime > 0)
/// - `tx_is_height = tx_locktime < LOCKTIME_THRESHOLD` → true
/// - `sk_is_height = stack_locktime < LOCKTIME_THRESHOLD` → true
/// - `tx_is_height == sk_is_height` → `true == true` → true
/// - `tx_locktime >= stack_locktime` → true
///
/// So the conjunction is `true && true && true = true`.
///
/// Proves the CLTV success condition: a block-height-type transaction locktime meeting the
/// script's minimum satisfies OP_CHECKLOCKTIMEVERIFY.
#[cfg_attr(feature = "spec-lock", spec_locked("5.4.7", "F_BIP65Passes"))]
#[cfg_attr(feature = "spec-lock", blvm_spec_lock::requires(tx_locktime > 0))]
#[cfg_attr(feature = "spec-lock", blvm_spec_lock::requires(tx_locktime < LOCKTIME_THRESHOLD))]
#[cfg_attr(feature = "spec-lock", blvm_spec_lock::requires(stack_locktime < LOCKTIME_THRESHOLD))]
#[cfg_attr(feature = "spec-lock", blvm_spec_lock::requires(tx_locktime >= stack_locktime))]
#[cfg_attr(feature = "spec-lock", blvm_spec_lock::ensures(result == true))]
pub(crate) fn _verify_f_bip65_passes(tx_locktime: u32, stack_locktime: u32) -> bool {
    let tx_is_height = tx_locktime < LOCKTIME_THRESHOLD;
    let sk_is_height = stack_locktime < LOCKTIME_THRESHOLD;
    (tx_is_height == sk_is_height) && tx_locktime >= stack_locktime
}

/// Witness for **F_BIP65PassesTimestamp** (PROTOCOL.md §5.4.7).
///
/// Proof obligation: CLTV validation passes when both locktimes are timestamps
/// (`>= LOCKTIME_THRESHOLD`) and `tx_locktime >= stack_locktime`.
///
/// Under the three `requires` clauses:
/// - `tx_locktime != 0` → true (tx_locktime >= LOCKTIME_THRESHOLD > 0)
/// - `tx_is_height = tx_locktime < LOCKTIME_THRESHOLD` → false
/// - `sk_is_height = stack_locktime < LOCKTIME_THRESHOLD` → false
/// - `tx_is_height == sk_is_height` → `false == false` → true
/// - `tx_locktime >= stack_locktime` → true
///
/// So the conjunction is `true && true && true = true`.
///
/// Proves the timestamp-domain CLTV success case: a timestamp-type transaction locktime
/// meeting the script's minimum satisfies OP_CHECKLOCKTIMEVERIFY.
#[cfg_attr(feature = "spec-lock", spec_locked("5.4.7", "F_BIP65PassesTimestamp"))]
#[cfg_attr(feature = "spec-lock", blvm_spec_lock::requires(tx_locktime >= LOCKTIME_THRESHOLD))]
#[cfg_attr(feature = "spec-lock", blvm_spec_lock::requires(stack_locktime >= LOCKTIME_THRESHOLD))]
#[cfg_attr(feature = "spec-lock", blvm_spec_lock::requires(tx_locktime >= stack_locktime))]
#[cfg_attr(feature = "spec-lock", blvm_spec_lock::requires(tx_locktime > 0))]
#[cfg_attr(feature = "spec-lock", blvm_spec_lock::ensures(result == true))]
pub(crate) fn _verify_f_bip65_passes_timestamp(tx_locktime: u32, stack_locktime: u32) -> bool {
    let tx_is_height = tx_locktime < LOCKTIME_THRESHOLD;
    let sk_is_height = stack_locktime < LOCKTIME_THRESHOLD;
    (tx_is_height == sk_is_height) && tx_locktime >= stack_locktime
}

// ─── §5.5 continued: EvaluateSequenceLocks positive cases ─────────────────────

/// Witness for **F_EvalSeqLocksHeightMet** (PROTOCOL.md §5.5).
///
/// Proof obligation: EvaluateSequenceLocks returns true when the height lock is satisfied
/// and there is no time constraint.
///
/// Under `requires(min_height >= 0)` + `requires(block_height > min_height)`:
///   first clause = `min_height < 0 || block_height > min_height` = `false || true` = `true`.
/// Under `requires(min_time < 0)`:
///   second clause = `min_time < 0 || time > min_time` = `true || ...` = `true`.
/// Result = `true && true` = `true`.
///
/// Proves the height-met case: a CSV-relative-height-locked transaction can be included
/// once the block height strictly exceeds the minimum required height.
#[cfg_attr(feature = "spec-lock", spec_locked("5.5", "F_EvalSeqLocksHeightMet"))]
#[cfg_attr(feature = "spec-lock", blvm_spec_lock::requires(min_height >= 0))]
#[cfg_attr(feature = "spec-lock", blvm_spec_lock::requires(block_height > min_height))]
#[cfg_attr(feature = "spec-lock", blvm_spec_lock::requires(min_time < 0))]
#[cfg_attr(feature = "spec-lock", blvm_spec_lock::ensures(result == true))]
pub(crate) fn _verify_f_eval_seq_locks_height_met(
    block_height: i64,
    time: i64,
    min_height: i64,
    min_time: i64,
) -> bool {
    (min_height < 0 || block_height > min_height) && (min_time < 0 || time > min_time)
}

/// Witness for **F_EvalSeqLocksTimeNotMet** (PROTOCOL.md §5.5).
///
/// Proof obligation: EvaluateSequenceLocks returns false when a time constraint is active
/// and the current block time does not exceed the minimum.
///
/// Under `requires(min_time >= 0)`: `min_time < 0` is false, so the second clause =
///   `false || time > min_time`.
/// Under `requires(time <= min_time)`: `time > min_time` is false.
/// So the second clause = `false`, and `(any) && false` = `false`.
///
/// Proves the symmetric time-not-met invariant: a CSV-relative-time-locked transaction
/// cannot be included when the median time past has not reached the required minimum.
#[cfg_attr(feature = "spec-lock", spec_locked("5.5", "F_EvalSeqLocksTimeNotMet"))]
#[cfg_attr(feature = "spec-lock", blvm_spec_lock::requires(min_time >= 0))]
#[cfg_attr(feature = "spec-lock", blvm_spec_lock::requires(time <= min_time))]
#[cfg_attr(feature = "spec-lock", blvm_spec_lock::ensures(result == false))]
pub(crate) fn _verify_f_eval_seq_locks_time_not_met(
    block_height: i64,
    time: i64,
    min_height: i64,
    min_time: i64,
) -> bool {
    (min_height < 0 || block_height > min_height) && (min_time < 0 || time > min_time)
}

/// Witness for **F_EvalSeqLocksTimeMet** (PROTOCOL.md §5.5).
///
/// Proof obligation: EvaluateSequenceLocks returns true when the time lock is satisfied
/// and there is no height constraint.
///
/// Under `requires(min_time >= 0)` + `requires(time > min_time)`:
///   second clause = `min_time < 0 || time > min_time` = `false || true` = `true`.
/// Under `requires(min_height < 0)`:
///   first clause = `min_height < 0 || block_height > min_height` = `true || ...` = `true`.
/// Result = `true && true` = `true`.
///
/// Symmetric to F_EvalSeqLocksHeightMet: proves the time-domain success case.
#[cfg_attr(feature = "spec-lock", spec_locked("5.5", "F_EvalSeqLocksTimeMet"))]
#[cfg_attr(feature = "spec-lock", blvm_spec_lock::requires(min_time >= 0))]
#[cfg_attr(feature = "spec-lock", blvm_spec_lock::requires(time > min_time))]
#[cfg_attr(feature = "spec-lock", blvm_spec_lock::requires(min_height < 0))]
#[cfg_attr(feature = "spec-lock", blvm_spec_lock::ensures(result == true))]
pub(crate) fn _verify_f_eval_seq_locks_time_met(
    block_height: i64,
    time: i64,
    min_height: i64,
    min_time: i64,
) -> bool {
    (min_height < 0 || block_height > min_height) && (min_time < 0 || time > min_time)
}

/// Witness for **F_EvalSeqLocksBothMet** (PROTOCOL.md §5.5).
///
/// Proof obligation: EvaluateSequenceLocks returns true when both height and time
/// constraints are active and both are satisfied.
///
/// Under `requires(min_height >= 0)` + `requires(block_height > min_height)`:
///   first clause = `min_height < 0 || block_height > min_height` = `false || true` = `true`.
/// Under `requires(min_time >= 0)` + `requires(time > min_time)`:
///   second clause = `min_time < 0 || time > min_time` = `false || true` = `true`.
/// Result = `true && true` = `true`.
///
/// Proves the full conjunction: a CSV-locked transaction with both height and time
/// constraints can be included once both are simultaneously satisfied.
#[cfg_attr(feature = "spec-lock", spec_locked("5.5", "F_EvalSeqLocksBothMet"))]
#[cfg_attr(feature = "spec-lock", blvm_spec_lock::requires(min_height >= 0))]
#[cfg_attr(feature = "spec-lock", blvm_spec_lock::requires(block_height > min_height))]
#[cfg_attr(feature = "spec-lock", blvm_spec_lock::requires(min_time >= 0))]
#[cfg_attr(feature = "spec-lock", blvm_spec_lock::requires(time > min_time))]
#[cfg_attr(feature = "spec-lock", blvm_spec_lock::ensures(result == true))]
pub(crate) fn _verify_f_eval_seq_locks_both_met(
    block_height: i64,
    time: i64,
    min_height: i64,
    min_time: i64,
) -> bool {
    (min_height < 0 || block_height > min_height) && (min_time < 0 || time > min_time)
}

// ─── §5.3.1 ValidBlockHeader ──────────────────────────────────────────────────

/// Witness for **F_HeaderVersionFloor** (PROTOCOL.md §5.3.1).
///
/// Before BIP34 there is no version floor. Version 0 passes. After BIP34,
/// version < 2 fails. `check_bip90` is the production check.
#[cfg_attr(feature = "spec-lock", spec_locked("5.3.1", "F_HeaderVersionFloor"))]
#[cfg_attr(feature = "spec-lock", blvm_spec_lock::requires(block_version == 0))]
#[cfg_attr(feature = "spec-lock", blvm_spec_lock::requires(bip34_active == 0))]
#[cfg_attr(feature = "spec-lock", blvm_spec_lock::ensures(result == 1))]
pub(crate) fn _verify_f_header_version_floor(block_version: i64, bip34_active: i64) -> i64 {
    if bip34_active != 0 && block_version < 2 {
        0
    } else {
        1
    }
}

/// Witness for **F_HeaderBitsFloor** (PROTOCOL.md §5.3.1).
///
/// Proof obligation: when `bits == 0`, header validation always returns false.
///
/// The production `validate_block_header` checks `if header.bits == 0 { return Ok(false) }`.
/// Under `requires(bits == 0)`, `bits != 0` evaluates to `false`, so the `else` branch
/// returns `0` (encodes `false`).
///
/// Proves H06 (non-zero bits): a block header with zero compact difficulty is always invalid.
/// Z3 proves this via linear arithmetic: `0 != 0` is `false`.
#[cfg_attr(feature = "spec-lock", spec_locked("5.3.1", "F_HeaderBitsFloor"))]
#[cfg_attr(feature = "spec-lock", blvm_spec_lock::requires(bits == 0))]
#[cfg_attr(feature = "spec-lock", blvm_spec_lock::ensures(result == 0))]
pub(crate) fn _verify_f_header_bits_floor(bits: i64) -> i64 {
    if bits != 0 { 1 } else { 0 }
}

/// Witness for **F_HeaderTimestampAfterMtp** (PROTOCOL.md §5.3.1).
///
/// Proof obligation: a header timestamp is later than the median time past
/// exactly when `timestamp > mtp`. Equality is not later.
#[cfg_attr(
    feature = "spec-lock",
    spec_locked("5.3.1", "F_HeaderTimestampAfterMtp")
)]
#[cfg_attr(feature = "spec-lock", blvm_spec_lock::requires(timestamp >= 0))]
#[cfg_attr(feature = "spec-lock", blvm_spec_lock::requires(mtp >= 0))]
#[cfg_attr(feature = "spec-lock", blvm_spec_lock::ensures((timestamp > mtp) == result))]
pub(crate) fn _verify_f_header_timestamp_after_mtp(timestamp: i64, mtp: i64) -> bool {
    timestamp > mtp
}

// ─── §5.4.1 BIP30: Duplicate Coinbase Prevention ──────────────────────────────

/// Witness for **F_BIP30DuplicateRejected** (PROTOCOL.md §5.4.1).
///
/// A duplicate coinbase that is not one of the two exempt blocks is invalid.
/// `duplicate == 1` and `exception == 0` yield result 0.
#[cfg_attr(
    feature = "spec-lock",
    spec_locked("5.4.1", "F_BIP30DuplicateRejected")
)]
#[cfg_attr(feature = "spec-lock", blvm_spec_lock::requires(duplicate == 1))]
#[cfg_attr(feature = "spec-lock", blvm_spec_lock::requires(exception == 0))]
#[cfg_attr(feature = "spec-lock", blvm_spec_lock::ensures(result == 0))]
pub(crate) fn _verify_f_bip30_duplicate_rejected(duplicate: i64, exception: i64) -> i64 {
    if duplicate == 1 && exception == 0 {
        0
    } else {
        1
    }
}

// ─── §5.4.2 BIP34: Block Height in Coinbase ───────────────────────────────────

/// Witness for **F_BIP34PreActivationPass** (PROTOCOL.md §5.4.2).
///
/// Proof obligation: before BIP34 activation, the BIP34 height check always passes.
///
/// The production `check_bip34` short-circuits `return Ok(true)` when
/// `!is_fork_active(Bip34, height)`.  Encoded as an integer flag (0 = inactive):
/// under `requires(bip34_active == 0)`, the `if` branch is taken and `result = 1`.
/// Z3 proves this via linear arithmetic: `bip34_active == 0 → result == 1`.
///
/// Proves the pre-activation-pass invariant: any block before BIP34 activation
/// cannot be rejected by the coinbase-height rule.
#[cfg_attr(
    feature = "spec-lock",
    spec_locked("5.4.2", "F_BIP34PreActivationPass")
)]
#[cfg_attr(feature = "spec-lock", blvm_spec_lock::requires(bip34_active == 0))]
#[cfg_attr(feature = "spec-lock", blvm_spec_lock::ensures(result == 1))]
pub(crate) fn _verify_f_bip34_pre_activation_pass(bip34_active: i64) -> i64 {
    if bip34_active == 0 { 1 } else { 0 }
}

// ─── §5.4.8 BIP348: CSFS Degenerate Case Algebra ────────────────────────────

/// Witness for **F_CSFSZeroPubkeyInvalid** (PROTOCOL.md §5.4.8).
///
/// Proof obligation: when pubkey length == 0, CSFS always returns invalid (false).
///
/// Body: `pk_len != 0`. Under `requires(pk_len == 0)`, this is `false`.
/// Proves the zero-pubkey fast rejection path — no signature check needed.
/// Z3 proves via linear arithmetic.
#[cfg_attr(feature = "spec-lock", spec_locked("5.4.8", "F_CSFSZeroPubkeyInvalid"))]
#[cfg_attr(feature = "spec-lock", blvm_spec_lock::requires(pk_len == 0))]
#[cfg_attr(feature = "spec-lock", blvm_spec_lock::ensures(result == false))]
pub(crate) fn _verify_f_csfs_zero_pubkey_invalid(pk_len: u64) -> bool {
    pk_len != 0
}

/// Witness for **F_CSFSUnknownPubkeyValid** (PROTOCOL.md §5.4.8).
///
/// Proof obligation: when pubkey is non-zero length but not 32 bytes,
/// CSFS always returns valid (true) — unknown pubkey types succeed
/// per BIP348 soft-fork upgrade rules.
///
/// Body: 3-way if/else. Under `requires(pk_len > 0 && pk_len != 32)`,
/// both first branches are false → else branch → true.
/// Z3 proves via linear arithmetic.
#[cfg_attr(
    feature = "spec-lock",
    spec_locked("5.4.8", "F_CSFSUnknownPubkeyValid")
)]
#[cfg_attr(feature = "spec-lock", blvm_spec_lock::requires(pk_len > 0))]
#[cfg_attr(feature = "spec-lock", blvm_spec_lock::requires(pk_len != 32))]
#[cfg_attr(feature = "spec-lock", blvm_spec_lock::ensures(result == true))]
pub(crate) fn _verify_f_csfs_unknown_pubkey_valid(pk_len: u64) -> bool {
    pk_len != 32
}

/// Witness for **F_CSFSEmptySigValid** (PROTOCOL.md §5.4.8).
///
/// Proof obligation: when signature is empty AND pubkey is non-zero,
/// CSFS always returns valid (true). Empty-signature handling pushes
/// an empty vector, matching OP_CHECKSIG behavior.
///
/// Body: under `requires(sig_len == 0 && pk_len > 0)`, the first branch
/// (pk_len == 0) is false, the second branch (sig_len == 0) is true → true.
/// Z3 proves via linear arithmetic.
#[cfg_attr(feature = "spec-lock", spec_locked("5.4.8", "F_CSFSEmptySigValid"))]
#[cfg_attr(feature = "spec-lock", blvm_spec_lock::requires(sig_len == 0))]
#[cfg_attr(feature = "spec-lock", blvm_spec_lock::requires(pk_len > 0))]
#[cfg_attr(feature = "spec-lock", blvm_spec_lock::ensures(result == true))]
pub(crate) fn _verify_f_csfs_empty_sig_valid(sig_len: u64, pk_len: u64) -> bool {
    if pk_len == 0 {
        false // zero pubkey: always invalid
    } else if sig_len == 0 {
        true // empty sig: always valid
    } else {
        false // non-empty sig: depends on Schnorr (placeholder)
    }
}

// ─── §5.4.3 BIP66: Strict DER ────────────────────────────────────────────────

/// Witness for **F_BIP66ActivationBelow** (PROTOCOL.md §5.4.3).
///
/// Proof obligation: before BIP66 activation, all DER signature checks pass.
/// The formula body is `result == 1`.
///
/// Encoded as `bip66_active == 0` (integer flag, 0 = inactive). Under
/// `requires(bip66_active == 0)`, the first branch is taken → result = 1 (pass).
/// Z3 proves via linear arithmetic.
#[cfg_attr(feature = "spec-lock", spec_locked("5.4.3", "F_BIP66ActivationBelow"))]
#[cfg_attr(feature = "spec-lock", blvm_spec_lock::requires(bip66_active == 0))]
#[cfg_attr(feature = "spec-lock", blvm_spec_lock::ensures(result == 1))]
pub(crate) fn _verify_f_bip66_pre_activation_pass(bip66_active: i64) -> i64 {
    if bip66_active == 0 { 1 } else { 0 }
}

/// Witness for **F_BIP66ActivationAt** (PROTOCOL.md §5.4.3).
///
/// At and above height 363,725 the network check equals `is_strict_der`.
#[cfg_attr(feature = "spec-lock", spec_locked("5.4.3", "F_BIP66ActivationAt"))]
#[cfg_attr(feature = "spec-lock", blvm_spec_lock::requires(height >= 363725))]
#[cfg_attr(feature = "spec-lock", blvm_spec_lock::ensures(result == strict_der))]
pub(crate) fn _verify_f_bip66_activation_at(height: i64, strict_der: i64) -> i64 {
    if height < 363725 { 1 } else { strict_der }
}

/// Witness for **F_StrictDERSoundness** (PROTOCOL.md §5.4.3).
///
/// A failed byte clause (length, tag, high bit, or leading zero) forces result 0.
#[cfg_attr(feature = "spec-lock", spec_locked("5.4.3", "F_StrictDERSoundness"))]
#[cfg_attr(feature = "spec-lock", blvm_spec_lock::requires(len_ok == 0))]
#[cfg_attr(feature = "spec-lock", blvm_spec_lock::ensures(result == 0))]
pub(crate) fn _verify_f_strict_der_soundness(
    len_ok: i64,
    tag_ok: i64,
    high_ok: i64,
    lead_ok: i64,
) -> i64 {
    if len_ok == 0 || tag_ok == 0 || high_ok == 0 || lead_ok == 0 {
        0
    } else {
        1
    }
}

/// Witness for **F_NoDuplicateInputs** (PROTOCOL.md §5.1).
///
/// `same_prevout != 0` means two inputs share txid and vout. Result 0 is the rejection.
#[cfg_attr(feature = "spec-lock", spec_locked("5.1", "F_NoDuplicateInputs"))]
#[cfg_attr(feature = "spec-lock", blvm_spec_lock::requires(same_prevout != 0))]
#[cfg_attr(feature = "spec-lock", blvm_spec_lock::ensures(result == 0))]
pub(crate) fn _verify_f_no_duplicate_inputs(same_prevout: i64) -> i64 {
    if same_prevout != 0 { 0 } else { 1 }
}

/// Witness for **F_OutputSumBounded** (PROTOCOL.md §13.3.1).
///
/// `overflow != 0` means signed 64-bit addition overflowed. Result 0 is the error.
#[cfg_attr(feature = "spec-lock", spec_locked("13.3.1", "F_OutputSumBounded"))]
#[cfg_attr(feature = "spec-lock", blvm_spec_lock::requires(overflow != 0))]
#[cfg_attr(feature = "spec-lock", blvm_spec_lock::ensures(result == 0))]
pub(crate) fn _verify_f_output_sum_bounded(value: i64, overflow: i64) -> i64 {
    if overflow != 0 || !(0..=2_100_000_000_000_000).contains(&value) {
        0
    } else {
        1
    }
}

/// Witness for **F_MerkleMutationRejected** (PROTOCOL.md §8.4.1).
///
/// `unpadded_equal != 0` is an equal adjacent pair before odd-padding. Result 0 is the mutation.
#[cfg_attr(
    feature = "spec-lock",
    spec_locked("8.4.1", "F_MerkleMutationRejected")
)]
#[cfg_attr(feature = "spec-lock", blvm_spec_lock::requires(unpadded_equal != 0))]
#[cfg_attr(feature = "spec-lock", blvm_spec_lock::ensures(result == 0))]
pub(crate) fn _verify_f_merkle_mutation_rejected(unpadded_equal: i64) -> i64 {
    if unpadded_equal != 0 { 0 } else { 1 }
}

// ─── §5.4.4 BIP90: Block Version Enforcement ─────────────────────────────────

/// Witness for **F_BIP90PreActivationPass** (PROTOCOL.md §5.4.4).
///
/// Proof obligation: before BIP90 activation, all blocks pass version enforcement.
///
/// Encoded as `bip90_active == 0` (integer flag, 0 = inactive). Under
/// `requires(bip90_active == 0)`, result = 1 (pass).
/// Z3 proves via linear arithmetic.
#[cfg_attr(
    feature = "spec-lock",
    spec_locked("5.4.4", "F_BIP90PreActivationPass")
)]
#[cfg_attr(feature = "spec-lock", blvm_spec_lock::requires(bip90_active == 0))]
#[cfg_attr(feature = "spec-lock", blvm_spec_lock::ensures(result == 1))]
pub(crate) fn _verify_f_bip90_pre_activation_pass(bip90_active: i64) -> i64 {
    if bip90_active == 0 { 1 } else { 0 }
}

// ─── §5.4.5 BIP147: NULLDUMMY Enforcement ────────────────────────────────────

/// Witness for **F_BIP147PreActivationPass** (PROTOCOL.md §5.4.5).
///
/// Proof obligation: before BIP147 activation, all CHECKMULTISIG operations pass
/// the null-dummy check regardless of dummy element content.
///
/// Encoded as `bip147_active == 0` (integer flag, 0 = inactive). Under
/// `requires(bip147_active == 0)`, result = 1 (pass).
/// Z3 proves via linear arithmetic.
#[cfg_attr(
    feature = "spec-lock",
    spec_locked("5.4.5", "F_BIP147PreActivationPass")
)]
#[cfg_attr(feature = "spec-lock", blvm_spec_lock::requires(bip147_active == 0))]
#[cfg_attr(feature = "spec-lock", blvm_spec_lock::ensures(result == 1))]
pub(crate) fn _verify_f_bip147_pre_activation_pass(bip147_active: i64) -> i64 {
    if bip147_active == 0 { 1 } else { 0 }
}

// ─── §5.4.9 BIP54: Consensus Cleanup ─────────────────────────────────────────

/// Witness for **F_BIP54ActivationThreshold** (PROTOCOL.md §5.4.9).
///
/// Proof obligation: IsBip54ActiveAt returns true iff `height >= threshold`.
///
/// Under `requires(height >= threshold)`, the comparison `height >= threshold`
/// evaluates to `true`.  Z3 proves this trivially via linear arithmetic on u64.
///
/// This is the activation-monotone property: once active at height `a`, BIP54
/// remains active for all heights ≥ `a`.  The `_verify_f_bip54_activation_threshold`
/// witness function is referenced explicitly in the Orange Paper §5.4.9.
#[cfg_attr(
    feature = "spec-lock",
    spec_locked("5.4.9", "F_BIP54ActivationThreshold")
)]
#[cfg_attr(feature = "spec-lock", blvm_spec_lock::requires(height >= threshold))]
#[cfg_attr(feature = "spec-lock", blvm_spec_lock::ensures(result == true))]
pub(crate) fn _verify_f_bip54_activation_threshold(height: u64, threshold: u64) -> bool {
    height >= threshold
}

// ─── §5.5 BIP68: Sequence bit extraction ─────────────────────────────────────

/// Witness for **F_SequenceDisabledWhenBit31Set** (PROTOCOL.md §5.5).
///
/// Proof obligation: IsSequenceDisabled returns true when bit 31 is set.
///
/// The body is `(sequence & 0x80000000) != 0`. Under `requires((sequence & 0x80000000) != 0)`,
/// the bitwise AND is nonzero, so `!= 0` evaluates to `true`.
///
/// Proves the disabled case: a sequence number with the BIP68 disable flag (bit 31)
/// set is always treated as non-relative-locktime.
#[cfg_attr(
    feature = "spec-lock",
    spec_locked("5.5", "F_SequenceDisabledWhenBit31Set")
)]
#[cfg_attr(feature = "spec-lock", blvm_spec_lock::requires((sequence & 0x80000000) != 0))]
#[cfg_attr(feature = "spec-lock", blvm_spec_lock::ensures(result == true))]
pub(crate) fn _verify_f_sequence_disabled_when_bit31_set(sequence: u32) -> bool {
    (sequence & 0x80000000) != 0
}

/// Witness for **F_SequenceEnabledWhenBit31Clear** (PROTOCOL.md §5.5).
///
/// Proof obligation: IsSequenceDisabled returns false when bit 31 is clear.
///
/// The body is `(sequence & 0x80000000) != 0`. Under `requires((sequence & 0x80000000) == 0)`,
/// the bitwise AND is zero, so `!= 0` evaluates to `false`.
///
/// Proves the enabled case: a sequence number without the disable flag is treated as
/// a relative locktime constraint (BIP68 applies).
#[cfg_attr(
    feature = "spec-lock",
    spec_locked("5.5", "F_SequenceEnabledWhenBit31Clear")
)]
#[cfg_attr(feature = "spec-lock", blvm_spec_lock::requires((sequence & 0x80000000) == 0))]
#[cfg_attr(feature = "spec-lock", blvm_spec_lock::ensures(result == false))]
pub(crate) fn _verify_f_sequence_enabled_when_bit31_clear(sequence: u32) -> bool {
    (sequence & 0x80000000) != 0
}

/// Witness for **F_SequenceTypeTimeWhenBit22Set** (PROTOCOL.md §5.5).
///
/// Proof obligation: ExtractSequenceTypeFlag returns true when bit 22 is set.
///
/// The body is `(sequence & 0x00400000) != 0`. Under `requires((sequence & 0x00400000) != 0)`,
/// the bitwise AND is nonzero, so `!= 0` evaluates to `true`.
///
/// Proves the time-based case: a sequence number with the BIP68 type flag (bit 22)
/// set encodes a time-based relative locktime.
#[cfg_attr(
    feature = "spec-lock",
    spec_locked("5.5", "F_SequenceTypeTimeWhenBit22Set")
)]
#[cfg_attr(feature = "spec-lock", blvm_spec_lock::requires((sequence & 0x00400000) != 0))]
#[cfg_attr(feature = "spec-lock", blvm_spec_lock::ensures(result == true))]
pub(crate) fn _verify_f_sequence_type_time_when_bit22_set(sequence: u32) -> bool {
    (sequence & 0x00400000) != 0
}

/// Witness for **F_SequenceTypeHeightWhenBit22Clear** (PROTOCOL.md §5.5).
///
/// Proof obligation: ExtractSequenceTypeFlag returns false when bit 22 is clear.
///
/// The body is `(sequence & 0x00400000) != 0`. Under `requires((sequence & 0x00400000) == 0)`,
/// the bitwise AND is zero, so `!= 0` evaluates to `false`.
///
/// Proves the block-height case: a sequence number without the type flag encodes a
/// block-height relative locktime.
#[cfg_attr(
    feature = "spec-lock",
    spec_locked("5.5", "F_SequenceTypeHeightWhenBit22Clear")
)]
#[cfg_attr(feature = "spec-lock", blvm_spec_lock::requires((sequence & 0x00400000) == 0))]
#[cfg_attr(feature = "spec-lock", blvm_spec_lock::ensures(result == false))]
pub(crate) fn _verify_f_sequence_type_height_when_bit22_clear(sequence: u32) -> bool {
    (sequence & 0x00400000) != 0
}

// ─── §11.1.1 Weight and Size ─────────────────────────────────────────────────

/// Witness for **F_WeightToVSizeFloor** (PROTOCOL.md §11.1.1).
///
/// Proof obligation: vsize (ceiling(weight/4)) is always ≥ floor(weight/4).
///
/// Body: `(weight + 3) / 4` (explicit ceiling division). Under all inputs,
/// `(weight + 3) / 4 >= weight / 4` holds because `weight + 3 >= weight` and
/// integer division is monotone. Z3 proves via linear arithmetic.
#[cfg_attr(feature = "spec-lock", spec_locked("11.1.1", "F_WeightToVSizeFloor"))]
#[cfg_attr(feature = "spec-lock", blvm_spec_lock::ensures(result >= weight / 4))]
pub(crate) fn _verify_f_weight_to_vsize_floor(weight: u64) -> u64 {
    weight.div_ceil(4)
}

/// Witness for **F_WeightToVSizeCeiling** (PROTOCOL.md §11.1.1).
///
/// Proof obligation: vsize (ceiling(weight/4)) is always ≤ floor(weight/4) + 1.
///
/// Body: `(weight + 3) / 4`. The ceiling is at most 1 more than the floor:
/// `(weight + 3) / 4 <= weight / 4 + 1`. Together with F_WeightToVSizeFloor
/// this characterizes ceiling division exactly. Z3 proves via linear arithmetic.
#[cfg_attr(feature = "spec-lock", spec_locked("11.1.1", "F_WeightToVSizeCeiling"))]
#[cfg_attr(feature = "spec-lock", blvm_spec_lock::ensures(result <= weight / 4 + 1))]
pub(crate) fn _verify_f_weight_to_vsize_ceiling(weight: u64) -> u64 {
    weight.div_ceil(4)
}

/// Witness for **F_WeightEquiv** (PROTOCOL.md §11.1.1).
///
/// Under `total == base + wit`, `3 * base + total == 4 * base + wit`.
#[cfg_attr(feature = "spec-lock", spec_locked("11.1.1", "F_WeightEquiv"))]
#[cfg_attr(feature = "spec-lock", blvm_spec_lock::requires(total == base + wit))]
#[cfg_attr(feature = "spec-lock", blvm_spec_lock::ensures(result == 4 * base + wit))]
pub(crate) fn _verify_f_weight_equiv(base: i64, wit: i64, total: i64) -> i64 {
    3 * base + total
}

/// Witness for **F_StrippedSizeCountsScripts** (PROTOCOL.md §11.1.1).
///
/// The stripped-size lower bound includes every script byte. Omitting those bytes and keeping
/// only a length placeholder undercounts block weight.
#[cfg_attr(
    feature = "spec-lock",
    spec_locked("11.1.1", "F_StrippedSizeCountsScripts")
)]
#[cfg_attr(feature = "spec-lock", blvm_spec_lock::requires(script_sig >= 0))]
#[cfg_attr(feature = "spec-lock", blvm_spec_lock::requires(script_pubkey >= 0))]
#[cfg_attr(feature = "spec-lock", blvm_spec_lock::ensures(result >= script_sig + script_pubkey))]
pub(crate) fn _verify_f_stripped_size_counts_scripts(script_sig: i64, script_pubkey: i64) -> i64 {
    script_sig + script_pubkey
}

// ─── §11.1.2 Witness Structure ───────────────────────────────────────────────

/// Witness for **F_WitnessEmptyByLength** (PROTOCOL.md §11.1.2).
///
/// Proof obligation: when the outer witness list has 0 elements, IsWitnessEmpty
/// returns true.
///
/// Body: `len == 0`. Under `requires(len == 0)`, the expression evaluates to
/// true. Proves the zero-length case: an empty witness stack is always empty.
/// Z3 proves via linear arithmetic.
#[cfg_attr(feature = "spec-lock", spec_locked("11.1.2", "F_WitnessEmptyByLength"))]
#[cfg_attr(feature = "spec-lock", blvm_spec_lock::requires(len == 0))]
#[cfg_attr(feature = "spec-lock", blvm_spec_lock::ensures(result == true))]
pub(crate) fn _verify_f_witness_empty_by_length(len: u64) -> bool {
    len == 0
}

// ─── §11.1.3 Witness Program Length ─────────────────────────────────────────

/// Witness for **F_WitnessProgramLength20Valid** (PROTOCOL.md §11.1.3).
///
/// Proof obligation: when witness program length is 20 bytes, validation returns
/// true (P2WPKH).
///
/// Body: `program_len == 20 || program_len == 32`. Under `requires(program_len == 20)`,
/// first disjunct is true, so result is true. Z3 proves via linear arithmetic.
#[cfg_attr(
    feature = "spec-lock",
    spec_locked("11.1.3", "F_WitnessProgramLength20Valid")
)]
#[cfg_attr(feature = "spec-lock", blvm_spec_lock::requires(program_len == 20))]
#[cfg_attr(feature = "spec-lock", blvm_spec_lock::ensures(result == true))]
pub(crate) fn _verify_f_witness_program_length_20_valid(program_len: u64) -> bool {
    program_len == 20 || program_len == 32
}

/// Witness for **F_WitnessProgramLength32Valid** (PROTOCOL.md §11.1.3).
///
/// Proof obligation: when witness program length is 32 bytes, validation returns
/// true (P2WSH or P2TR).
///
/// Body: `program_len == 20 || program_len == 32`. Under `requires(program_len == 32)`,
/// second disjunct is true, so result is true. Z3 proves via linear arithmetic.
#[cfg_attr(
    feature = "spec-lock",
    spec_locked("11.1.3", "F_WitnessProgramLength32Valid")
)]
#[cfg_attr(feature = "spec-lock", blvm_spec_lock::requires(program_len == 32))]
#[cfg_attr(feature = "spec-lock", blvm_spec_lock::ensures(result == true))]
pub(crate) fn _verify_f_witness_program_length_32_valid(program_len: u64) -> bool {
    program_len == 20 || program_len == 32
}

/// Witness for **F_WitnessProgramLengthInvalid** (PROTOCOL.md §11.1.3).
///
/// Proof obligation: when witness program length is neither 20 nor 32 bytes,
/// validation returns false.
///
/// Body: `program_len == 20 || program_len == 32`. Under
/// `requires(program_len != 20 && program_len != 32)`, both disjuncts are false,
/// so result is false. Z3 proves via linear arithmetic.
#[cfg_attr(
    feature = "spec-lock",
    spec_locked("11.1.3", "F_WitnessProgramLengthInvalid")
)]
#[cfg_attr(feature = "spec-lock", blvm_spec_lock::requires(program_len != 20))]
#[cfg_attr(feature = "spec-lock", blvm_spec_lock::requires(program_len != 32))]
#[cfg_attr(feature = "spec-lock", blvm_spec_lock::ensures(result == false))]
pub(crate) fn _verify_f_witness_program_length_invalid(program_len: u64) -> bool {
    program_len == 20 || program_len == 32
}

/// Witness for **F_WitnessVersionRejected** (PROTOCOL.md §11.1.3).
///
/// `OP_1NEGATE` (79) and `OP_RESERVED` (80) are not witness versions.
#[cfg_attr(
    feature = "spec-lock",
    spec_locked("11.1.3", "F_WitnessVersionRejected")
)]
#[cfg_attr(feature = "spec-lock", blvm_spec_lock::requires(op == 79 || op == 80))]
#[cfg_attr(feature = "spec-lock", blvm_spec_lock::ensures(result == false))]
#[allow(clippy::manual_range_contains)]
pub(crate) fn _verify_f_witness_version_rejected(op: i64) -> bool {
    op == 0 || (op >= 81 && op <= 96)
}

/// Witness for **F_WitnessVersionAccepted** (PROTOCOL.md §11.1.3).
///
/// `OP_0` (0), `OP_1` (81), and `OP_16` (96) are witness versions.
#[cfg_attr(
    feature = "spec-lock",
    spec_locked("11.1.3", "F_WitnessVersionAccepted")
)]
#[cfg_attr(feature = "spec-lock", blvm_spec_lock::requires(op == 0 || op == 81 || op == 96))]
#[cfg_attr(feature = "spec-lock", blvm_spec_lock::ensures(result == true))]
#[allow(clippy::manual_range_contains)]
pub(crate) fn _verify_f_witness_version_accepted(op: i64) -> bool {
    op == 0 || (op >= 81 && op <= 96)
}

// ─── §5.2.4 IsMinimalIfCondition ─────────────────────────────────────────────

/// Witness for **F_MinimalIfEmptyTrue** (PROTOCOL.md §5.2.4).
///
/// Proof obligation: when the byte string is empty (length == 0),
/// IsMinimalIfCondition always returns true.
///
/// Body: the structural pattern `if len == 0 { true } else { false }`.
/// Under `requires(len == 0)`, the first branch is taken → true. Proves the
/// empty-bytes case of the MINIMALIF rule. Z3 proves via linear arithmetic.
#[cfg_attr(feature = "spec-lock", spec_locked("5.2.4", "F_MinimalIfEmptyTrue"))]
#[cfg_attr(feature = "spec-lock", blvm_spec_lock::requires(len == 0))]
#[cfg_attr(feature = "spec-lock", blvm_spec_lock::ensures(result == true))]
pub(crate) fn _verify_f_minimal_if_empty_true(len: u64) -> bool {
    len == 0
}

/// Witness for **F_MinimalIfLongFalse** (PROTOCOL.md §5.2.4).
///
/// Proof obligation: when the byte string has more than 1 byte (length > 1),
/// IsMinimalIfCondition always returns false.
///
/// Body: the structural 3-way pattern. Under `requires(len > 1)`, both
/// `len == 0` and `len == 1` are false, so the else branch → false. Proves
/// that multi-byte encodings always fail the MINIMALIF check.
/// Z3 proves via linear arithmetic.
#[cfg_attr(feature = "spec-lock", spec_locked("5.2.4", "F_MinimalIfLongFalse"))]
#[cfg_attr(feature = "spec-lock", blvm_spec_lock::requires(len > 1))]
#[cfg_attr(feature = "spec-lock", blvm_spec_lock::ensures(result == false))]
pub(crate) fn _verify_f_minimal_if_long_false(len: u64) -> bool {
    len == 0 || len == 1
}

// ─── §11.2.1 IsTaprootOutput ─────────────────────────────────────────────────

/// Witness for **F_TaprootOutputScriptLengthInvalid** (PROTOCOL.md §11.2.1).
///
/// Proof obligation: when the scriptPubKey is not exactly 34 bytes, IsTaprootOutput
/// returns false.
///
/// Body: `script_len == 34` (captures the necessary length condition). Under
/// `requires(script_len != 34)`, the expression is false. A P2TR script must be
/// exactly 34 bytes (`OP_1 <push32> <32-byte-key>`); all other lengths are
/// rejected. Z3 proves via linear arithmetic.
#[cfg_attr(
    feature = "spec-lock",
    spec_locked("11.2.1", "F_TaprootOutputScriptLengthInvalid")
)]
#[cfg_attr(feature = "spec-lock", blvm_spec_lock::requires(script_len != 34))]
#[cfg_attr(feature = "spec-lock", blvm_spec_lock::ensures(result == false))]
pub(crate) fn _verify_f_taproot_output_script_length_invalid(script_len: u64) -> bool {
    script_len == 34
}

// ─── §5.4.9 BIP54 Deployment Field Invariants ────────────────────────────────

/// Witness for **F_Bip54SignalBit** (PROTOCOL.md §5.4.9).
///
/// Proof obligation: The BIP54 version-bits deployment always uses signal bit 15.
///
/// All three network deployments (mainnet, testnet, regtest) use the same constant
/// bit index. Body: returns the constant 15. Z3 proves the identity trivially.
#[cfg_attr(feature = "spec-lock", spec_locked("5.4.9", "F_Bip54SignalBit"))]
#[cfg_attr(feature = "spec-lock", blvm_spec_lock::ensures(result == 15))]
pub(crate) fn _verify_f_bip54_signal_bit() -> u64 {
    15
}

/// Witness for **F_Bip54StartTimeZero** (PROTOCOL.md §5.4.9).
///
/// Proof obligation: The BIP54 deployment start time is 0 (immediate activation;
/// no time-gated window).
///
/// Body: returns 0. Z3 proves the identity trivially.
#[cfg_attr(feature = "spec-lock", spec_locked("5.4.9", "F_Bip54StartTimeZero"))]
#[cfg_attr(feature = "spec-lock", blvm_spec_lock::ensures(result == 0))]
pub(crate) fn _verify_f_bip54_start_time_zero() -> u64 {
    0
}

// ─── §11.2 Taproot Activation Heights ────────────────────────────────────────

/// Witness for **F_TaprootActivationMainnet** (PROTOCOL.md §11.2).
///
/// Proof obligation: on mainnet (network == 0), TaprootActivationHeight returns
/// exactly 709,632.
///
/// Uses an if/else on the integer network ID (instead of enum match) so the Z3
/// translator can model the control flow. Under `requires(network == 0)`, the
/// first branch is taken → TAPROOT_ACTIVATION_MAINNET.
#[cfg_attr(
    feature = "spec-lock",
    spec_locked("11.2", "F_TaprootActivationMainnet")
)]
#[cfg_attr(feature = "spec-lock", blvm_spec_lock::requires(network == 0))]
#[cfg_attr(feature = "spec-lock", blvm_spec_lock::ensures(result == TAPROOT_ACTIVATION_MAINNET))]
pub(crate) fn _verify_f_taproot_activation_mainnet(network: u64) -> u64 {
    if network == 0 {
        TAPROOT_ACTIVATION_MAINNET
    } else if network == 1 {
        TAPROOT_ACTIVATION_TESTNET
    } else {
        0
    }
}

/// Witness for **F_TaprootActivationTestnet** (PROTOCOL.md §11.2).
///
/// Proof obligation: on testnet (network == 1), TaprootActivationHeight returns
/// exactly 2,011,968.
///
/// Under `requires(network == 1)`, the second branch is taken →
/// TAPROOT_ACTIVATION_TESTNET.
#[cfg_attr(
    feature = "spec-lock",
    spec_locked("11.2", "F_TaprootActivationTestnet")
)]
#[cfg_attr(feature = "spec-lock", blvm_spec_lock::requires(network == 1))]
#[cfg_attr(feature = "spec-lock", blvm_spec_lock::ensures(result == TAPROOT_ACTIVATION_TESTNET))]
pub(crate) fn _verify_f_taproot_activation_testnet(network: u64) -> u64 {
    if network == 0 {
        TAPROOT_ACTIVATION_MAINNET
    } else if network == 1 {
        TAPROOT_ACTIVATION_TESTNET
    } else {
        0
    }
}

/// Witness for **F_TaprootActivationRegtest** (PROTOCOL.md §11.2).
///
/// Proof obligation: on regtest (network ≠ 0 and ≠ 1, i.e., network == 2),
/// TaprootActivationHeight returns 0 (immediate activation at genesis).
///
/// Under `requires(network != 0 && network != 1)`, both branches are skipped
/// → else branch → 0.
#[cfg_attr(
    feature = "spec-lock",
    spec_locked("11.2", "F_TaprootActivationRegtest")
)]
#[cfg_attr(feature = "spec-lock", blvm_spec_lock::requires(network != 0))]
#[cfg_attr(feature = "spec-lock", blvm_spec_lock::requires(network != 1))]
#[cfg_attr(feature = "spec-lock", blvm_spec_lock::ensures(result == 0))]
pub(crate) fn _verify_f_taproot_activation_regtest(network: u64) -> u64 {
    if network == 0 {
        TAPROOT_ACTIVATION_MAINNET
    } else if network == 1 {
        TAPROOT_ACTIVATION_TESTNET
    } else {
        0
    }
}

/// Witness for **F_DecodeLocktimeNegativeZero** (PROTOCOL.md §5.4.7).
///
/// A one-byte element 0x80 is negative zero and decodes to 0.
#[cfg_attr(
    feature = "spec-lock",
    spec_locked("5.4.7", "F_DecodeLocktimeNegativeZero")
)]
#[cfg_attr(feature = "spec-lock", blvm_spec_lock::requires(byte == 128))]
#[cfg_attr(feature = "spec-lock", blvm_spec_lock::ensures(result == 0))]
pub(crate) fn _verify_f_decode_locktime_negative_zero(byte: i64) -> i64 {
    if byte >= 128 { -(byte - 128) } else { byte }
}

/// Witness for **F_DecodeLocktimeNegativeOne** (PROTOCOL.md §5.4.7).
///
/// A one-byte element 0x81 has the sign bit set and magnitude 1.
#[cfg_attr(
    feature = "spec-lock",
    spec_locked("5.4.7", "F_DecodeLocktimeNegativeOne")
)]
#[cfg_attr(feature = "spec-lock", blvm_spec_lock::requires(byte == 129))]
#[cfg_attr(feature = "spec-lock", blvm_spec_lock::ensures(result == -1))]
pub(crate) fn _verify_f_decode_locktime_negative_one(byte: i64) -> i64 {
    if byte >= 128 { -(byte - 128) } else { byte }
}

/// Witness for **F_CltvRejectsNegative** (PROTOCOL.md §5.4.7).
///
/// A negative script number fails CLTV before the locktime comparison.
#[cfg_attr(feature = "spec-lock", spec_locked("5.4.7", "F_CltvRejectsNegative"))]
#[cfg_attr(feature = "spec-lock", blvm_spec_lock::requires(n < 0))]
#[cfg_attr(feature = "spec-lock", blvm_spec_lock::ensures(result == false))]
pub(crate) fn _verify_f_cltv_rejects_negative(n: i64) -> bool {
    n >= 0
}

/// Witness for **F_CltvRejectsAboveU32** (PROTOCOL.md §5.4.7).
///
/// A non-negative value above 2^32-1 cannot satisfy CLTV.
#[cfg_attr(feature = "spec-lock", spec_locked("5.4.7", "F_CltvRejectsAboveU32"))]
#[cfg_attr(feature = "spec-lock", blvm_spec_lock::requires(n > 4294967295))]
#[cfg_attr(feature = "spec-lock", blvm_spec_lock::ensures(result == false))]
#[allow(clippy::manual_range_contains)]
pub(crate) fn _verify_f_cltv_rejects_above_u32(n: i64) -> bool {
    // Comparisons translate. `RangeInclusive::contains` leaves this witness partial, and the
    // partial ceiling is zero.
    n >= 0 && n <= 4294967295
}

/// Witness for **F_SigopCountPushOpcode** (PROTOCOL.md §5.2.2).
///
/// P2SH redeem extraction treats every opcode through OP_16 as a push.
#[cfg_attr(feature = "spec-lock", spec_locked("5.2.2", "F_SigopCountPushOpcode"))]
#[cfg_attr(feature = "spec-lock", blvm_spec_lock::requires(op >= 0))]
#[cfg_attr(feature = "spec-lock", blvm_spec_lock::requires(op <= 255))]
#[cfg_attr(feature = "spec-lock", blvm_spec_lock::ensures((op <= 96) == result))]
pub(crate) fn _verify_f_sigop_count_push_opcode(op: i64) -> bool {
    op <= 96
}

/// Witness for **F_CsvVersionBelowTwoFails** (PROTOCOL.md §5.5).
///
/// CSV fails when the stack disable bit is clear and the transaction version is below 2.
#[cfg_attr(feature = "spec-lock", spec_locked("5.5", "F_CsvVersionBelowTwoFails"))]
#[cfg_attr(feature = "spec-lock", blvm_spec_lock::requires(version < 2))]
#[cfg_attr(feature = "spec-lock", blvm_spec_lock::requires(disable_bit == 0))]
#[cfg_attr(feature = "spec-lock", blvm_spec_lock::ensures(result == false))]
pub(crate) fn _verify_f_csv_version_below_two_fails(version: i64, disable_bit: i64) -> bool {
    disable_bit != 0 || version >= 2
}

/// Witness for **F_RelativeLockUnsignedVersion** (PROTOCOL.md §5.5).
///
/// A version word in `0..=2^32-1` enables BIP68 and CSV exactly when it is at least 2.
/// Wire `0xffffffff` is 4294967295 and enables both.
#[cfg_attr(
    feature = "spec-lock",
    spec_locked("5.5", "F_RelativeLockUnsignedVersion")
)]
#[cfg_attr(feature = "spec-lock", blvm_spec_lock::requires(version >= 0))]
#[cfg_attr(feature = "spec-lock", blvm_spec_lock::requires(version <= 4294967295))]
#[cfg_attr(feature = "spec-lock", blvm_spec_lock::ensures(result == (version >= 2)))]
pub(crate) fn _verify_f_relative_lock_unsigned_version(version: i64) -> bool {
    version >= 2
}

/// Witness for **F_CsvDisableBitSkipsVersion** (PROTOCOL.md §5.5).
///
/// A set stack disable bit succeeds even when the transaction version is below 2.
#[cfg_attr(
    feature = "spec-lock",
    spec_locked("5.5", "F_CsvDisableBitSkipsVersion")
)]
#[cfg_attr(feature = "spec-lock", blvm_spec_lock::requires(disable_bit != 0))]
#[cfg_attr(feature = "spec-lock", blvm_spec_lock::requires(version < 2))]
#[cfg_attr(feature = "spec-lock", blvm_spec_lock::ensures(result == true))]
pub(crate) fn _verify_f_csv_disable_bit_skips_version(version: i64, disable_bit: i64) -> bool {
    disable_bit != 0 || version >= 2
}

/// Witness for **F_TaprootSighashSingleMissingOutput** (PROTOCOL.md §11.2.6).
///
/// SIGHASH_SINGLE with no output at the input index produces no hash.
#[cfg_attr(
    feature = "spec-lock",
    spec_locked("11.2.6", "F_TaprootSighashSingleMissingOutput")
)]
#[cfg_attr(feature = "spec-lock", blvm_spec_lock::requires(output_type == 3))]
#[cfg_attr(feature = "spec-lock", blvm_spec_lock::requires(n_outputs >= 0))]
#[cfg_attr(feature = "spec-lock", blvm_spec_lock::requires(input_index >= n_outputs))]
#[cfg_attr(feature = "spec-lock", blvm_spec_lock::ensures(result == false))]
pub(crate) fn _verify_f_taproot_sighash_single_missing_output(
    output_type: i64,
    input_index: i64,
    n_outputs: i64,
) -> bool {
    output_type != 3 || input_index < n_outputs
}

/// Witness for **F_TapscriptSighashSingleMissingOutput** (PROTOCOL.md §11.2.7).
///
/// Tapscript SIGHASH_SINGLE with no output at the input index produces no hash.
#[cfg_attr(
    feature = "spec-lock",
    spec_locked("11.2.7", "F_TapscriptSighashSingleMissingOutput")
)]
#[cfg_attr(feature = "spec-lock", blvm_spec_lock::requires(output_type == 3))]
#[cfg_attr(feature = "spec-lock", blvm_spec_lock::requires(n_outputs >= 0))]
#[cfg_attr(feature = "spec-lock", blvm_spec_lock::requires(input_index >= n_outputs))]
#[cfg_attr(feature = "spec-lock", blvm_spec_lock::ensures(result == false))]
pub(crate) fn _verify_f_tapscript_sighash_single_missing_output(
    output_type: i64,
    input_index: i64,
    n_outputs: i64,
) -> bool {
    output_type != 3 || input_index < n_outputs
}

/// Witness for **F_InputSumWithinMaxMoney** (PROTOCOL.md §5.1).
///
/// `sum` is the running total of input values. Above `MAX_MONEY` the result is rejection.
#[cfg_attr(feature = "spec-lock", spec_locked("5.1", "F_InputSumWithinMaxMoney"))]
#[cfg_attr(feature = "spec-lock", blvm_spec_lock::requires(sum > 2_100_000_000_000_000))]
#[cfg_attr(feature = "spec-lock", blvm_spec_lock::ensures(result == 0))]
pub(crate) fn _verify_f_input_sum_within_max_money(sum: i64) -> i64 {
    if sum > 2_100_000_000_000_000 { 0 } else { 1 }
}

/// Witness for **F_TapscriptTruncatedPushNotSuccess** (PROTOCOL.md §11.2.8).
///
/// `header_fits == 0` means the push header or payload does not fit in the script.
/// The success scan does not accept that script.
#[cfg_attr(
    feature = "spec-lock",
    spec_locked("11.2.8", "F_TapscriptTruncatedPushNotSuccess")
)]
#[cfg_attr(feature = "spec-lock", blvm_spec_lock::requires(header_fits == 0))]
#[cfg_attr(feature = "spec-lock", blvm_spec_lock::ensures(result == false))]
pub(crate) fn _verify_f_tapscript_truncated_push_not_success(header_fits: i64) -> bool {
    header_fits != 0
}

/// Witness for **F_CheckMultisigCountsPubkeys** (PROTOCOL.md §5.2).
///
/// `n_keys` is in range and the running opcode count plus that key count is past 201.
#[cfg_attr(
    feature = "spec-lock",
    spec_locked("5.2", "F_CheckMultisigCountsPubkeys")
)]
#[cfg_attr(feature = "spec-lock", blvm_spec_lock::requires(n_keys >= 0))]
#[cfg_attr(feature = "spec-lock", blvm_spec_lock::requires(n_keys <= 20))]
#[cfg_attr(feature = "spec-lock", blvm_spec_lock::requires(op_count + n_keys > 201))]
#[cfg_attr(feature = "spec-lock", blvm_spec_lock::ensures(result == 0))]
#[allow(clippy::manual_range_contains)]
pub(crate) fn _verify_f_checkmultisig_counts_pubkeys(op_count: i64, n_keys: i64) -> i64 {
    if n_keys >= 0 && n_keys <= 20 && op_count + n_keys > 201 {
        0
    } else {
        1
    }
}

/// Witness for **F_FalseResultEmpty** (PROTOCOL.md §5.2).
///
/// `is_true == 0` is a false script result. Its stack length is 0.
#[cfg_attr(feature = "spec-lock", spec_locked("5.2", "F_FalseResultEmpty"))]
#[cfg_attr(feature = "spec-lock", blvm_spec_lock::requires(is_true == 0))]
#[cfg_attr(feature = "spec-lock", blvm_spec_lock::ensures(result == 0))]
pub(crate) fn _verify_f_false_result_empty(is_true: i64) -> i64 {
    if is_true == 0 { 0 } else { 1 }
}

/// Witness for **F_Bip30RepeatRetiresPriorOutputs** (PROTOCOL.md §5.4.1).
///
/// `exception == 1` is one of the two historical repeats. Prior outputs of that txid are gone.
#[cfg_attr(
    feature = "spec-lock",
    spec_locked("5.4.1", "F_Bip30RepeatRetiresPriorOutputs")
)]
#[cfg_attr(feature = "spec-lock", blvm_spec_lock::requires(exception == 1))]
#[cfg_attr(feature = "spec-lock", blvm_spec_lock::ensures(result == 0))]
pub(crate) fn _verify_f_bip30_repeat_retires_prior_outputs(exception: i64) -> i64 {
    if exception == 1 { 0 } else { 1 }
}

/// Witness for **F_NonDerAbortsScript** (PROTOCOL.md §5.4.3).
///
/// A non-empty signature that is not strict DER aborts. An empty signature does not.
#[cfg_attr(feature = "spec-lock", spec_locked("5.4.3", "F_NonDerAbortsScript"))]
#[cfg_attr(feature = "spec-lock", blvm_spec_lock::requires(sig_len > 0))]
#[cfg_attr(feature = "spec-lock", blvm_spec_lock::requires(strict_der == 0))]
#[cfg_attr(feature = "spec-lock", blvm_spec_lock::ensures(result == 0))]
pub(crate) fn _verify_f_non_der_aborts_script(sig_len: i64, strict_der: i64) -> i64 {
    if sig_len > 0 && strict_der == 0 { 0 } else { 1 }
}

/// Witness for **F_NestedRedeemPushCanonical** (PROTOCOL.md §11.1.8).
///
/// `canonical == 0` means the scriptSig is not the direct push of the redeem.
#[cfg_attr(
    feature = "spec-lock",
    spec_locked("11.1.8", "F_NestedRedeemPushCanonical")
)]
#[cfg_attr(feature = "spec-lock", blvm_spec_lock::requires(canonical == 0))]
#[cfg_attr(feature = "spec-lock", blvm_spec_lock::ensures(result == false))]
pub(crate) fn _verify_f_nested_redeem_push_canonical(canonical: i64) -> bool {
    canonical != 0
}

/// Witness for **F_P2shUnknownWitnessSucceeds** (PROTOCOL.md §11.1.8).
///
/// Discourage is off and the redeem push is canonical.
#[cfg_attr(
    feature = "spec-lock",
    spec_locked("11.1.8", "F_P2shUnknownWitnessSucceeds")
)]
#[cfg_attr(feature = "spec-lock", blvm_spec_lock::requires(discourage == 0))]
#[cfg_attr(feature = "spec-lock", blvm_spec_lock::requires(canonical == 1))]
#[cfg_attr(feature = "spec-lock", blvm_spec_lock::ensures(result == true))]
pub(crate) fn _verify_f_p2sh_unknown_witness_succeeds(discourage: i64, canonical: i64) -> bool {
    discourage == 0 && canonical == 1
}

/// Witness for **F_ProofNegativeCompactRejected** (PROTOCOL.md §7.2).
///
/// `negative == 1` means compact bit `0x00800000` is set.
#[cfg_attr(
    feature = "spec-lock",
    spec_locked("7.2", "F_ProofNegativeCompactRejected")
)]
#[cfg_attr(feature = "spec-lock", blvm_spec_lock::requires(negative == 1))]
#[cfg_attr(feature = "spec-lock", blvm_spec_lock::ensures(result == false))]
pub(crate) fn _verify_f_proof_negative_compact_rejected(negative: i64) -> bool {
    negative == 0
}

/// Witness for **F_ProofEqualHashAccepted** (PROTOCOL.md §7.2).
///
/// `hash_above == 0` means the header hash is not above the expanded target.
#[cfg_attr(feature = "spec-lock", spec_locked("7.2", "F_ProofEqualHashAccepted"))]
#[cfg_attr(feature = "spec-lock", blvm_spec_lock::requires(hash_above == 0))]
#[cfg_attr(feature = "spec-lock", blvm_spec_lock::requires(negative == 0))]
#[cfg_attr(feature = "spec-lock", blvm_spec_lock::requires(target_zero == 0))]
#[cfg_attr(feature = "spec-lock", blvm_spec_lock::ensures(result == true))]
pub(crate) fn _verify_f_proof_equal_hash_accepted(
    hash_above: i64,
    negative: i64,
    target_zero: i64,
) -> bool {
    hash_above == 0 && negative == 0 && target_zero == 0
}

/// Witness for **F_BIP34SmallHeightOpcode** (PROTOCOL.md §5.4.2).
///
/// Heights 1 through 16 are the single opcode `0x50 + height`.
#[cfg_attr(
    feature = "spec-lock",
    spec_locked("5.4.2", "F_BIP34SmallHeightOpcode")
)]
#[cfg_attr(feature = "spec-lock", blvm_spec_lock::requires(height >= 1))]
#[cfg_attr(feature = "spec-lock", blvm_spec_lock::requires(height <= 16))]
#[cfg_attr(feature = "spec-lock", blvm_spec_lock::ensures(result == (80 + height)))]
pub(crate) fn _verify_f_bip34_small_height_opcode(height: i64) -> i64 {
    80 + height
}

/// Witness for **F_BIP34HeightZero** (PROTOCOL.md §5.4.2).
///
/// Height 0 is `OP_0`, not `0x50`.
#[cfg_attr(feature = "spec-lock", spec_locked("5.4.2", "F_BIP34HeightZero"))]
#[cfg_attr(feature = "spec-lock", blvm_spec_lock::requires(height == 0))]
#[cfg_attr(feature = "spec-lock", blvm_spec_lock::ensures(result == 0))]
pub(crate) fn _verify_f_bip34_height_zero(height: i64) -> i64 {
    if height == 0 { 0 } else { 80 + height }
}

/// Witness for **F_BIP34HeightSeventeen** (PROTOCOL.md §5.4.2).
///
/// Height 17 is outside the opcode range, so the prefix is a one-byte push length.
#[cfg_attr(feature = "spec-lock", spec_locked("5.4.2", "F_BIP34HeightSeventeen"))]
#[cfg_attr(feature = "spec-lock", blvm_spec_lock::requires(height == 17))]
#[cfg_attr(feature = "spec-lock", blvm_spec_lock::ensures(result == 1))]
pub(crate) fn _verify_f_bip34_height_seventeen(height: i64) -> i64 {
    #[allow(clippy::manual_range_contains)]
    if height >= 1 && height <= 16 {
        80 + height
    } else {
        1
    }
}

/// Witness for **F_CtvTestnet4Inactive** (PROTOCOL.md §5.4.6).
///
/// `result` is true exactly on the non-negative heights, where testnet4 leaves CTV inactive.
#[cfg_attr(feature = "spec-lock", spec_locked("5.4.6", "F_CtvTestnet4Inactive"))]
#[cfg_attr(feature = "spec-lock", blvm_spec_lock::ensures((height >= 0) == result))]
pub(crate) fn _verify_f_ctv_testnet4_inactive(height: i64) -> bool {
    height >= 0
}

/// Witness for **F_CsfsTestnet4Inactive** (PROTOCOL.md §5.4.8).
///
/// `result` is true exactly on the non-negative heights, where testnet4 leaves CSFS inactive.
#[cfg_attr(feature = "spec-lock", spec_locked("5.4.8", "F_CsfsTestnet4Inactive"))]
#[cfg_attr(feature = "spec-lock", blvm_spec_lock::ensures((height >= 0) == result))]
pub(crate) fn _verify_f_csfs_testnet4_inactive(height: i64) -> bool {
    height >= 0
}

/// Witness for **F_Bip54CoinbaseLocktime** (PROTOCOL.md §5.4.9).
#[cfg_attr(feature = "spec-lock", spec_locked("5.4.9", "F_Bip54CoinbaseLocktime"))]
#[cfg_attr(feature = "spec-lock", blvm_spec_lock::requires(height >= 1))]
#[cfg_attr(feature = "spec-lock", blvm_spec_lock::ensures(result == (height - 1)))]
pub(crate) fn _verify_f_bip54_coinbase_locktime(height: i64) -> i64 {
    height - 1
}

/// Witness for **F_Bip54CoinbaseSequence** (PROTOCOL.md §5.4.9).
#[cfg_attr(feature = "spec-lock", spec_locked("5.4.9", "F_Bip54CoinbaseSequence"))]
#[cfg_attr(feature = "spec-lock", blvm_spec_lock::ensures((sequence != 4294967295) == result))]
pub(crate) fn _verify_f_bip54_coinbase_sequence(sequence: i64) -> bool {
    sequence != 4294967295
}

/// Witness for **F_Bip94BitsFromFirst** (PROTOCOL.md §7.1).
#[cfg_attr(feature = "spec-lock", spec_locked("7.1", "F_Bip94BitsFromFirst"))]
#[cfg_attr(feature = "spec-lock", blvm_spec_lock::requires(enforce != 0))]
#[cfg_attr(feature = "spec-lock", blvm_spec_lock::ensures(result == first_bits))]
pub(crate) fn _verify_f_bip94_bits_from_first(
    enforce: i64,
    first_bits: i64,
    last_bits: i64,
) -> i64 {
    if enforce != 0 { first_bits } else { last_bits }
}

/// Witness for **F_Bip94BitsFromLast** (PROTOCOL.md §7.1).
#[cfg_attr(feature = "spec-lock", spec_locked("7.1", "F_Bip94BitsFromLast"))]
#[cfg_attr(feature = "spec-lock", blvm_spec_lock::requires(enforce == 0))]
#[cfg_attr(feature = "spec-lock", blvm_spec_lock::ensures(result == last_bits))]
pub(crate) fn _verify_f_bip94_bits_from_last(enforce: i64, first_bits: i64, last_bits: i64) -> i64 {
    if enforce != 0 { first_bits } else { last_bits }
}

/// Witness for **F_Bip94Timewarp** (PROTOCOL.md §7.1).
///
/// Parent times of at least 600 seconds make `timestamp + 600 >= parent`
/// the same bound as `timestamp >= parent - 600`.
#[cfg_attr(feature = "spec-lock", spec_locked("7.1", "F_Bip94Timewarp"))]
#[cfg_attr(feature = "spec-lock", blvm_spec_lock::requires(parent_time >= 600))]
#[cfg_attr(feature = "spec-lock", blvm_spec_lock::requires(timestamp >= 0))]
#[cfg_attr(feature = "spec-lock", blvm_spec_lock::ensures((timestamp + 600 >= parent_time) == result))]
pub(crate) fn _verify_f_bip94_timewarp(timestamp: i64, parent_time: i64) -> bool {
    timestamp + 600 >= parent_time
}

/// Witness for **F_Bip94TimewarpOffBoundary** (PROTOCOL.md §7.1).
///
/// Off a 2016-block boundary the time check accepts. The boundary arm is the 600-second comparison.
#[cfg_attr(
    feature = "spec-lock",
    spec_locked("7.1", "F_Bip94TimewarpOffBoundary")
)]
#[cfg_attr(feature = "spec-lock", blvm_spec_lock::requires(height >= 0))]
#[cfg_attr(feature = "spec-lock", blvm_spec_lock::requires(height % 2016 != 0))]
#[cfg_attr(feature = "spec-lock", blvm_spec_lock::requires(parent_time >= 600))]
#[cfg_attr(feature = "spec-lock", blvm_spec_lock::requires(timestamp >= 0))]
#[cfg_attr(feature = "spec-lock", blvm_spec_lock::ensures(result == true))]
pub(crate) fn _verify_f_bip94_timewarp_off_boundary(
    height: i64,
    timestamp: i64,
    parent_time: i64,
) -> bool {
    if height % 2016 == 0 {
        timestamp + 600 >= parent_time
    } else {
        true
    }
}

/// Witness for **F_OffBoundaryParentBits** (PROTOCOL.md §7.1).
///
/// The proof is the `not_boundary != 0` arm. The other arm is outside that precondition.
#[cfg_attr(feature = "spec-lock", spec_locked("7.1", "F_OffBoundaryParentBits"))]
#[cfg_attr(feature = "spec-lock", blvm_spec_lock::requires(not_boundary != 0))]
#[cfg_attr(feature = "spec-lock", blvm_spec_lock::ensures(result == parent_bits))]
pub(crate) fn _verify_f_off_boundary_parent_bits(not_boundary: i64, parent_bits: i64) -> i64 {
    if not_boundary != 0 { parent_bits } else { 0 }
}

/// Witness for **F_HeaderBitsMatchRequired** (PROTOCOL.md §7.1).
#[cfg_attr(feature = "spec-lock", spec_locked("7.1", "F_HeaderBitsMatchRequired"))]
#[cfg_attr(feature = "spec-lock", blvm_spec_lock::ensures((header_bits == required_bits) == result))]
pub(crate) fn _verify_f_header_bits_match_required(header_bits: i64, required_bits: i64) -> bool {
    header_bits == required_bits
}

/// Witness for **F_WitnessStackNullByLength** (PROTOCOL.md §11.1.2).
#[cfg_attr(
    feature = "spec-lock",
    spec_locked("11.1.2", "F_WitnessStackNullByLength")
)]
#[cfg_attr(feature = "spec-lock", blvm_spec_lock::requires(len >= 0))]
#[cfg_attr(feature = "spec-lock", blvm_spec_lock::ensures((len == 0) == result))]
pub(crate) fn _verify_f_witness_stack_null_by_length(len: i64) -> bool {
    len == 0
}

/// Witness for **F_WitnessPayloadByte** (PROTOCOL.md §11.1.3).
///
/// Every integer, not three sample bytes. The product is zero exactly at 0 and 128.
#[cfg_attr(feature = "spec-lock", spec_locked("11.1.3", "F_WitnessPayloadByte"))]
#[cfg_attr(feature = "spec-lock", blvm_spec_lock::ensures(result == (byte * (byte - 128) != 0)))]
pub(crate) fn _verify_f_witness_payload_byte(byte: i64) -> bool {
    byte != 0 && byte != 128
}

/// Witness for **F_WitnessPayloadEmpty** (PROTOCOL.md §11.1.3).
#[cfg_attr(feature = "spec-lock", spec_locked("11.1.3", "F_WitnessPayloadEmpty"))]
#[cfg_attr(feature = "spec-lock", blvm_spec_lock::requires(len == 0))]
#[cfg_attr(feature = "spec-lock", blvm_spec_lock::ensures(result == 0))]
pub(crate) fn _verify_f_witness_payload_empty(len: i64) -> i64 {
    if len == 0 { 0 } else { 1 }
}

/// Digest of the pair (witness root, reserved nonce). The translator replaces the call.
/// This body is not the compression function.
#[allow(dead_code)]
pub(crate) fn implied_hash(root: i64, nonce: i64) -> i64 {
    let _ = (root, nonce);
    0
}

/// Witness for **F_CastToBoolSummary** (PROTOCOL.md §11.1.3).
///
/// `prefix_nonzero` stands for “some byte before the last is nonzero.”
/// Empty, a zero payload of any length, and negative zero of any length are false.
#[cfg_attr(feature = "spec-lock", spec_locked("11.1.3", "F_CastToBoolSummary"))]
#[cfg_attr(feature = "spec-lock", blvm_spec_lock::ensures(
    result == (len >= 1 && (prefix_nonzero != 0 || (last != 0 && last != 128)))
))]
pub(crate) fn _verify_f_cast_to_bool_summary(len: i64, prefix_nonzero: i64, last: i64) -> bool {
    len >= 1 && (prefix_nonzero != 0 || (last != 0 && last != 128))
}

/// Witness for **F_UpgradableProgramShape** (PROTOCOL.md §11.1.3).
#[cfg_attr(
    feature = "spec-lock",
    spec_locked("11.1.3", "F_UpgradableProgramShape")
)]
#[cfg_attr(feature = "spec-lock", blvm_spec_lock::ensures(
    result
        == (script_sig_len == 0
            && witness_flag != 0
            && discourage == 0
            && len >= 1
            && (prefix_nonzero != 0 || (last != 0 && last != 128)))
))]
pub(crate) fn _verify_f_upgradable_program_shape(
    script_sig_len: i64,
    witness_flag: i64,
    discourage: i64,
    len: i64,
    prefix_nonzero: i64,
    last: i64,
) -> bool {
    script_sig_len == 0
        && witness_flag != 0
        && discourage == 0
        && len >= 1
        && (prefix_nonzero != 0 || (last != 0 && last != 128))
}

/// Witness for **F_WitnessCommitmentShape** (PROTOCOL.md §11.1.5).
///
/// No commitment output is valid only with no witness data. A commitment output
/// is valid only when the reserved item is 32 bytes and the stored word equals
/// the implied digest of the root and the nonce.
#[cfg_attr(
    feature = "spec-lock",
    spec_locked("11.1.5", "F_WitnessCommitmentShape")
)]
#[cfg_attr(feature = "spec-lock", blvm_spec_lock::ensures(
    result
        == ((has_commitment == 0 && any_witness == 0)
            || (has_commitment != 0
                && reserved_len == 32
                && stored == implied_hash(root, nonce)))
))]
pub(crate) fn _verify_f_witness_commitment_shape(
    has_commitment: i64,
    any_witness: i64,
    reserved_len: i64,
    stored: i64,
    root: i64,
    nonce: i64,
) -> bool {
    if has_commitment == 0 {
        any_witness == 0
    } else {
        reserved_len == 32 && stored == implied_hash(root, nonce)
    }
}