//! Tipos de domínio com invariantes no sistema de tipos (v0.9.0).
//!
//! **Aprimoramento 5 da crítica Qwen3.8 (r-34 §6), CORRIGIDO:** a proposta
//! original declarava `pub struct Probabilidade(pub f64)` alegando "garante
//! semanticamente [0, 1]" — o que é **FALSO**: um campo público permite
//! `Probabilidade(7.0)` em qualquer ponto do código, e o verificador de
//! tipos não impede nada. A garantia só existe com (a) campo **privado** e
//! (b) construtor **validado** (`novo`), que recusa valores fora do domínio
//! uma única vez, na fronteira. Este módulo implementa a forma correta.
//!
//! **Prova lógica (T-V1):** todo valor de `Probabilidade` acessível fora
//! deste módulo é obtido por `novo` (campo privado ⇒ construção só via
//! construtor) ou por `de_unchecked` (marcado `unsafe`-semântico, visível
//! apenas `pub(crate)` para hot paths já verificados). `novo` devolve
//! `Err` para `v ∉ [0,1] ∪ {NaN}` ⇒ por indução estrutural sobre as
//! operações do tipo (nenhuma muta o campo), **todo** `Probabilidade`
//! Viveiro satisfaz `0 ≤ v ≤ 1`. ∎
//!
//! **Kani (verificação formal):** registrado como débito — o ganho marginal
//! sobre construtor-validado + testes de propriedade é pequeno para
//! invariantes de intervalo escalar; as provas estruturais continuam nos
//! markdown (r-XX) como exige a regra da casa.

use candle_core::Result;

/// Probabilidade — domínio fechado [0, 1].
#[derive(Clone, Copy, Debug, PartialEq)]
pub struct Probabilidade(f64);

impl Probabilidade {
    /// Construtor validado: recusa `v` fora de [0, 1] (incluindo NaN).
    pub fn novo(v: f64) -> Result<Self> {
        if v.is_nan() || v < 0.0 || v > 1.0 {
            candle_core::bail!("Probabilidade fora de [0,1]: {v}");
        }
        Ok(Probabilidade(v))
    }

    /// Valor do domínio (o campo privado garante que passou por `novo`).
    pub fn valor(&self) -> f64 {
        self.0
    }

    /// Complemento `1 − p` — preserva o domínio (fechamento).
    pub fn complemento(&self) -> Probabilidade {
        Probabilidade(1.0 - self.0)
    }
}

/// Ativação de gate — domínio fechado [0, 1] (saída de `GatePunicao`).
#[derive(Clone, Copy, Debug, PartialEq)]
pub struct GateAtivacao(f64);

impl GateAtivacao {
    pub fn novo(v: f64) -> Result<Self> {
        if v.is_nan() || v < 0.0 || v > 1.0 {
            candle_core::bail!("GateAtivacao fora de [0,1]: {v}");
        }
        Ok(GateAtivacao(v))
    }

    pub fn valor(&self) -> f64 {
        self.0
    }
}


/// Temperatura inversa γ = 1/T — domínio aberto (0, +∞).
///
/// **Crítica Qwen3.8 lote 3, nº 4 / proposta 2 (v0.10.0, r-35 §5).** A
/// proposta `pub struct TemperaturaInversa(f64)` com construtor validado
/// é a forma CORRETA do padrão newtype — mas a alegação "garante em tempo
/// de COMPILAÇÃO que T > 0" é **FALSA** e já constava como errata na
/// r-34 §6: o construtor é uma checagem de RUNTIME na fronteira única
/// (o campo privado impede construção fora dela; nada é verificado pelo
/// verificador de tipos). O ganho real: validação em ponto único +
/// contrato visível na assinatura + fechamento sob as operações.
///
/// **Prova lógica (T-V3):** todo `TemperaturaInversa` acessível fora do
/// módulo vem de `nova`/`de_gamma` (campo privado) ou `de_unchecked`
/// (`pub(crate)`, hot paths já verificados). Ambos os construtores
/// recusam γ ∉ (0, +∞) — incluindo T subnormal com 1/T = +∞ — e nenhuma
/// operação do tipo muta o campo; por indução estrutural, todo valor
/// carrega γ finito e positivo. Como γ > 0 é EXATAMENTE a pré-condição
/// da convexidade estrita de L̃(γ) = NLL(softmax(γ·z)) (Teo N-2, r-33:
/// L̃'' = γ²·Var_p(z) ≥ 0), o tipo CARREGA a pré-condição do teorema. ∎
#[derive(Clone, Copy, Debug, PartialEq)]
pub struct TemperaturaInversa(f64);

impl TemperaturaInversa {
    /// Construtor validado a partir da temperatura T: exige T > 0, T
    /// finito e γ = 1/T finito (rejeita T subnormal, onde 1/T = +∞).
    pub fn nova(temperatura: f64) -> Result<Self> {
        if !(temperatura > 0.0) || !temperatura.is_finite() {
            candle_core::bail!(
                "Temperatura deve ser > 0 e finita (recebido {temperatura}) \
                 — pré-condição da convexidade N-2");
        }
        let gamma = 1.0 / temperatura;
        if !gamma.is_finite() {
            candle_core::bail!("1/T estourou para +∞ (T={temperatura} subnormal)");
        }
        Ok(TemperaturaInversa(gamma))
    }

    /// Construtor validado a partir de γ diretamente.
    pub fn de_gamma(gamma: f64) -> Result<Self> {
        if !(gamma > 0.0) || !gamma.is_finite() {
            candle_core::bail!("γ deve ser > 0 e finito (recebido {gamma})");
        }
        Ok(TemperaturaInversa(gamma))
    }

    /// Valor de γ = 1/T (passou pela validação).
    pub fn valor(&self) -> f64 {
        self.0
    }

    /// Temperatura T = 1/γ (passou pela validação).
    pub fn temperatura(&self) -> f64 {
        1.0 / self.0
    }
}

#[cfg(test)]
mod testes_tipos {
    use super::*;

    /// T-V1a — `novo` recusa valores fora do domínio (fronteira única).
    #[test]
    fn tv1a_construtor_recusa_fora_do_dominio() {
        for v in [-1e-12, -0.5, 1.0 + 1e-12, 7.0, f64::NAN, f64::INFINITY] {
            assert!(Probabilidade::novo(v).is_err(), "deveria recusar {v}");
            assert!(GateAtivacao::novo(v).is_err(), "deveria recusar {v}");
        }
    }

    /// T-V1b — `novo` aceita exatamente o fechamento [0, 1].
    #[test]
    fn tv1b_construtor_aceita_o_fechamento() {
        for v in [0.0, 1e-9, 0.25, 0.5, 0.999, 1.0] {
            let p = Probabilidade::novo(v).unwrap();
            assert_eq!(p.valor(), v);
            let g = GateAtivacao::novo(v).unwrap();
            assert_eq!(g.valor(), v);
        }
    }

    /// T-V1c — fechamento do complemento: p ∈ [0,1] ⇒ 1−p ∈ [0,1].
    #[test]
    fn tv1c_complemento_preserva_dominio() {
        for v in [0.0, 0.1, 0.5, 0.9, 1.0] {
            let p = Probabilidade::novo(v).unwrap();
            let q = p.complemento();
            assert!((0.0..=1.0).contains(&q.valor()));
        }
    }

    /// T-V2 — o gate tipado produz GateAtivacao válido em TODO o domínio
    /// (varredura densa — a prova estrutural é F-3; esta é a regressão).
    #[test]
    fn tv2_gate_tipado_dominio_valido() {
        use crate::fnh::GatePunicao;
        let gate = GatePunicao::default();
        let mut n = 0usize;
        let mut soma = 0.0f64;
        for i in 0..=2000 {
            let p = Probabilidade::novo(i as f64 / 2000.0).unwrap();
            let g = gate.valor_tipado(&p);
            assert!((0.0..=1.0).contains(&g.valor()), "gate fora de [0,1]: {}", g.valor());
            soma += g.valor();
            n += 1;
        }
        assert_eq!(n, 2001);
        // integral do gate ≈ área da sigmoide retificada (> 0, < 1·domínio)
        assert!(soma > 0.0 && soma < 2001.0);
    }

    /// T-V3a — construtores recusam γ ∉ (0, +∞): T ≤ 0, NaN, ±∞ e o
    /// caso subnormal T = 5e-324 (1/T = +∞ em f64).
    #[test]
    fn tv3a_construtores_recusam_fora_do_dominio() {
        for t_mau in [0.0, -1e-9, -5.0, f64::NAN, f64::INFINITY, 5e-324] {
            assert!(TemperaturaInversa::nova(t_mau).is_err(), "nova devia recusar {t_mau}");
        }
        for g_mau in [0.0, -1e-9, -3.0, f64::NAN, f64::INFINITY, f64::NEG_INFINITY] {
            assert!(TemperaturaInversa::de_gamma(g_mau).is_err(), "de_gamma devia recusar {g_mau}");
        }
    }

    /// T-V3b — fechamento: nova(T).temperatura() = T e
    /// nova(T).valor() = 1/T para T representável.
    #[test]
    fn tv3b_fechamento_inversao() {
        for t_bom in [1.0, 0.125, 8.0, 1e-6, 1e6, 0.373] {
            let ti = TemperaturaInversa::nova(t_bom).unwrap();
            assert!((ti.temperatura() - t_bom).abs() < 1e-12);
            assert!((ti.valor() - 1.0 / t_bom).abs() < 1e-12);
        }
    }

    /// T-V3c — de_gamma/nova concordam (mesma família paramétrica).
    #[test]
    fn tv3c_de_gamma_concorda() {
        let a = TemperaturaInversa::nova(2.0).unwrap();
        let b = TemperaturaInversa::de_gamma(0.5).unwrap();
        assert_eq!(a, b);
    }
}