v0.10.0: análise/prova/teste das críticas de engenharia Qwen3.8 lote 3 (r-35) — divisão SRP dos monólitos jepa/pensamento/moe/python em 26 submódulos (API estável via re-exports; 'Amdahl de compilação' refutada por experimento controlado, builds frios neutros), checkpoints atômicos SHA-256 puro FIPS 180-4 + fsync + rename + manifesto (CP-1..CP-3; correções da proposta: sem destruir estado anterior, manifesto com barreira, sem bincode/unwrap), TemperaturaInversa T-V3 (fronteira tipada da convexidade N-2; alegação compile-time corrigida), trait CamadaKhtst+CamadaHomeostatica (premissa do controlador refutada no fonte; Vec<Var>; adaptador MoeComPapel bit-a-bit), CLI Typer 75 (fachada aditiva com resume verificado por hash) — 123/123 cargo, 107/107 gates, treino real Wikipédia PT-BR com checkpoints íntegros
06e4b6f verified | //! 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]. | |
| 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`). | |
| 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. ∎ | |
| 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 | |
| } | |
| } | |
| mod testes_tipos { | |
| use super::*; | |
| /// T-V1a — `novo` recusa valores fora do domínio (fronteira única). | |
| 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]. | |
| 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]. | |
| 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). | |
| 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). | |
| 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. | |
| 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). | |
| fn tv3c_de_gamma_concorda() { | |
| let a = TemperaturaInversa::nova(2.0).unwrap(); | |
| let b = TemperaturaInversa::de_gamma(0.5).unwrap(); | |
| assert_eq!(a, b); | |
| } | |
| } | |