logicaffeine_proof/
linalg_certify.rs

1//! Kernel-certified linear algebra: turn an exact solve into a KERNEL-CHECKED PROOF TERM.
2//!
3//! [`crate::linalg`] solves `A·x = b` exactly over ℚ and re-checks the residual. This module goes
4//! one level deeper: it emits, for each row, an honest kernel proof term of type `Eq Int lhsᵢ rhsᵢ`,
5//! where the row identity `Σⱼ Aᵢⱼ·xⱼ = bᵢ` has been cleared of denominators to an INTEGER identity
6//!
7//! ```text
8//! bdᵢ · (Σⱼ Anᵢⱼ · Xnⱼ)  =  Da_i · Dx · bnᵢ
9//! ```
10//!
11//! and proven by the ring-axiom oracle [`crate::arith::prove_int_eq`], then RE-CHECKED by the
12//! kernel's own `infer_type`. This is the same trust path the kernel's Gödel/Chaitin theorems ride:
13//! the oracle is untrusted search, the kernel is the judge. A false identity is unprovable (the
14//! oracle returns `None`) and a forged proof fails the type-check — fail-closed. The current arith
15//! oracle is i64-wide, so systems whose cleared integers exceed i64 return `None` (an honest limit,
16//! not a wrong answer; a BigInt oracle would lift it).
17
18use crate::linalg;
19use logicaffeine_base::Rational;
20use logicaffeine_kernel::{
21    infer_type, normalize, prelude::StandardLibrary, Context, Literal, Term,
22};
23
24fn global(s: &str) -> Term {
25    Term::Global(s.to_string())
26}
27fn app(f: Term, x: Term) -> Term {
28    Term::App(Box::new(f), Box::new(x))
29}
30fn app2(f: Term, x: Term, y: Term) -> Term {
31    app(app(f, x), y)
32}
33fn lit(n: i64) -> Term {
34    Term::Lit(Literal::Int(n))
35}
36fn add(a: Term, b: Term) -> Term {
37    app2(global("add"), a, b)
38}
39fn mul(a: Term, b: Term) -> Term {
40    app2(global("mul"), a, b)
41}
42/// The proposition `Eq Int l r`.
43fn eq_int(l: Term, r: Term) -> Term {
44    app(app(app(global("Eq"), global("Int")), l), r)
45}
46
47/// A kernel context of its own carrying the ring/field/order axioms the oracle proves against: a
48/// copy-on-write clone of the standard library's one registration.
49pub fn ring_context() -> Context {
50    StandardLibrary::context().clone()
51}
52
53fn gcd(a: i128, b: i128) -> i128 {
54    let (mut a, mut b) = (a.abs(), b.abs());
55    while b != 0 {
56        let t = a % b;
57        a = b;
58        b = t;
59    }
60    a
61}
62fn lcm(a: i128, b: i128) -> Option<i128> {
63    if a == 0 || b == 0 {
64        return Some(0);
65    }
66    let g = gcd(a, b);
67    (a / g).checked_mul(b).map(|v| v.abs())
68}
69fn fit(v: i128) -> Option<i64> {
70    if (i64::MIN as i128..=i64::MAX as i128).contains(&v) {
71        Some(v as i64)
72    } else {
73        None
74    }
75}
76/// (numerator, denominator) of a rational as i128, or None if either exceeds i64 (oracle width).
77fn nd(r: &Rational) -> Option<(i128, i128)> {
78    Some((
79        r.numerator().to_i64()? as i128,
80        r.denominator().to_i64()? as i128,
81    ))
82}
83
84/// Scale a rational vector to integers: `vₖ · D` where `D = lcm` of the denominators. Returns the
85/// integer vector and `D`, or `None` past i64.
86fn clear_vec(v: &[Rational]) -> Option<(Vec<i128>, i128)> {
87    let nds: Vec<(i128, i128)> = v.iter().map(nd).collect::<Option<_>>()?;
88    let mut d: i128 = 1;
89    for &(_, den) in &nds {
90        d = lcm(d, den)?;
91    }
92    let ints: Vec<i128> = nds
93        .iter()
94        .map(|&(num, den)| num.checked_mul(d / den))
95        .collect::<Option<_>>()?;
96    Some((ints, d))
97}
98
99/// Prove the dot-product identity `Σₖ psₖ·qsₖ = r` as ONE kernel-checked term (type
100/// `Eq Int lhs rhs`). Clears denominators to `rd·Σₖ (Pnₖ·Qnₖ) = Dp·Dq·rn` — structure preserved —
101/// proves it with the untrusted oracle, then RE-CHECKS with the kernel. `None` if false or past i64.
102/// This one identity underlies every certificate below: a solve is a row·x = b, a factorization
103/// entry is Lrow·Ucol = (PA)ᵢⱼ, an inverse entry is Arow·(A⁻¹col) = Iᵢⱼ.
104pub fn prove_dot(ctx: &Context, ps: &[Rational], qs: &[Rational], r: &Rational) -> Option<Term> {
105    let k = ps.len();
106    if k == 0 || qs.len() != k {
107        return None;
108    }
109    let (pn, dp) = clear_vec(ps)?;
110    let (qn, dq) = clear_vec(qs)?;
111    let (rn, rd) = nd(r)?;
112    let mut sum = mul(lit(fit(pn[0])?), lit(fit(qn[0])?));
113    for i in 1..k {
114        sum = add(sum, mul(lit(fit(pn[i])?), lit(fit(qn[i])?)));
115    }
116    let lhs = mul(lit(fit(rd)?), sum);
117    let rhs = lit(fit(dp.checked_mul(dq)?.checked_mul(rn)?)?);
118    // untrusted oracle search → kernel re-check that the type is exactly this proposition.
119    let proof = crate::arith::prove_int_eq(ctx, &lhs, &rhs)?;
120    let ty = infer_type(ctx, &proof).ok()?;
121    if normalize(ctx, &ty) != normalize(ctx, &eq_int(lhs, rhs)) {
122        return None;
123    }
124    Some(proof)
125}
126
127/// Prove `r ≠ 0` in the kernel by EXHIBITING its inverse: a kernel-checked proof of `r·(1/r) = 1`.
128/// A value with a multiplicative inverse is nonzero, so this certifies nonsingularity when applied to
129/// a determinant. `None` iff `r == 0` — correctly unprovable, since `0` has no inverse.
130pub fn prove_nonzero(ctx: &Context, r: &Rational) -> Option<Term> {
131    let inv = r.recip()?; // r == 0 → None (the claim `0 ≠ 0` is false)
132    prove_dot(
133        ctx,
134        std::slice::from_ref(r),
135        std::slice::from_ref(&inv),
136        &Rational::one(),
137    )
138}
139
140/// Prove `A·x = b` for a GIVEN candidate `x`, one kernel-checked proof term per row (each is the
141/// row dot-product identity `Aᵢ·x = bᵢ`). `None` if any row is false (fail-closed) or past i64.
142pub fn prove_solution(
143    ctx: &Context,
144    a: &[Vec<Rational>],
145    x: &[Rational],
146    b: &[Rational],
147) -> Option<Vec<Term>> {
148    let n = a.len();
149    if n == 0 || a.iter().any(|r| r.len() != n) || x.len() != n || b.len() != n {
150        return None;
151    }
152    (0..n).map(|i| prove_dot(ctx, &a[i], x, &b[i])).collect()
153}
154
155/// Factor `A` and PROVE the factorization in the kernel: every entry of `P·A = L·U` is a dot-product
156/// proof `Lᵢ·Uⱼ = (PA)ᵢⱼ`. Returns the exact factorization and an n×n grid of kernel-checked terms.
157pub fn prove_lu(ctx: &Context, a: &[Vec<Rational>]) -> Option<(linalg::Lu, Vec<Vec<Term>>)> {
158    let f = linalg::lu(a)?;
159    let n = a.len();
160    let pa: Vec<Vec<Rational>> = f.perm.iter().map(|&i| a[i].clone()).collect();
161    let ucols = linalg::transpose(&f.u); // ucols[j] = column j of U
162    let mut proofs = Vec::with_capacity(n);
163    for i in 0..n {
164        let mut row = Vec::with_capacity(n);
165        for j in 0..n {
166            row.push(prove_dot(ctx, &f.l[i], &ucols[j], &pa[i][j])?);
167        }
168        proofs.push(row);
169    }
170    Some((f, proofs))
171}
172
173/// Invert `A` and PROVE it in the kernel: every entry of `A·A⁻¹ = I` is a dot-product proof
174/// `Aᵢ·(A⁻¹)ⱼ = Iᵢⱼ` (the off-diagonal `= 0` identities are proven too). `None` iff singular / past i64.
175pub fn prove_inverse(
176    ctx: &Context,
177    a: &[Vec<Rational>],
178) -> Option<(Vec<Vec<Rational>>, Vec<Vec<Term>>)> {
179    let ainv = linalg::inverse(a)?;
180    let n = a.len();
181    let id = linalg::identity(n);
182    let invcols = linalg::transpose(&ainv); // invcols[j] = column j of A⁻¹
183    let mut proofs = Vec::with_capacity(n);
184    for i in 0..n {
185        let mut row = Vec::with_capacity(n);
186        for j in 0..n {
187            row.push(prove_dot(ctx, &a[i], &invcols[j], &id[i][j])?);
188        }
189        proofs.push(row);
190    }
191    Some((ainv, proofs))
192}
193
194/// The complete certificate that a linear system `A·x = b` has a UNIQUE exact solution: the exact
195/// `x`, a kernel proof of `Aᵢ·x = bᵢ` for every row, and a kernel proof that `det A ≠ 0` (so the
196/// solution is unique, not merely one of many). Every term is re-checked by the kernel. This is the
197/// full "prove, not just run" object for a linear system. `None` iff singular or past the i64 width.
198pub struct SystemCert {
199    pub x: Vec<Rational>,
200    pub solve_proofs: Vec<Term>,
201    pub det: Rational,
202    pub nonsingular_proof: Term,
203}
204
205/// Solve and produce the complete unique-solution certificate.
206pub fn certify_system(ctx: &Context, a: &[Vec<Rational>], b: &[Rational]) -> Option<SystemCert> {
207    let x = linalg::solve(a, b)?;
208    let solve_proofs = prove_solution(ctx, a, &x, b)?;
209    let det = linalg::det(a);
210    let nonsingular_proof = prove_nonzero(ctx, &det)?;
211    Some(SystemCert {
212        x,
213        solve_proofs,
214        det,
215        nonsingular_proof,
216    })
217}
218
219/// Solve `A·x = b` exactly and hand back the exact `x` together with a kernel-checked proof that it
220/// solves the system (one proof term per row). `None` iff singular or beyond the i64 oracle width.
221pub fn prove_solve(
222    ctx: &Context,
223    a: &[Vec<Rational>],
224    b: &[Rational],
225) -> Option<(Vec<Rational>, Vec<Term>)> {
226    let x = linalg::solve(a, b)?;
227    let proofs = prove_solution(ctx, a, &x, b)?;
228    Some((x, proofs))
229}
230
231#[cfg(test)]
232#[path = "../../logicaffeine_tests/unit/logicaffeine_proof/linalg_certify/tests.rs"]
233mod tests;
logicaffeine_proof/linalg_certify.rs

logicaffeine_proof/
linalg_certify.rs
