hax_compoly_horner_evaluation_PoC

Author: klausnat

README_CompPoly_Horner.md

@@ -0,0 +1,173 @@
+# Horner algorithm verification (WIP) using CompPoly
+
+This folder documents an ongoing experiment toward an end-to-end verification workflow:
+
+**Rust implementation → hax extraction → CompPoly specification → Lean proofs**
+
+This repository follows a “one repo, multiple PoCs” approach. The Horner PoC currently lives in:
+- rust/horner_eval_rs/ — Rust implementation to be extracted with hax
+- lean-compoly/ — Lean project intended to host CompPoly specs and (eventually) proofs for the extracted code
+
+Status note: this work is **in progress**. At the moment, the hax-extracted Horner code does not compile in the same Lean project as CompPoly due to Lean toolchain version pinning across libraries. The primary success so far is that we raised issues and coordinated with maintainers, who agreed on a unified Lean version. Once the upgrades land, the pipeline should become feasible without splitting projects.
+
+
+## Horner Evaluation
+
+Many zk proof systems (including Plonky3-based stacks) rely heavily on polynomial arithmetic. A minimal but representative component is **univariate polynomial evaluation**.
+
+Given coefficients [c0, c1, c2, …], Horner’s method computes:
+p(x)=c0+x(c1+x(c2+… ))
+
+We aim to verify that the Rust implementation of Horner evaluation corresponds to a mathematical specification expressed using **CompPoly**.
+
+**Reference (algorithmic origin)**
+
+We use Plonky3-recursion as the [Plonky3-recursion](https://github.com/Plonky3/Plonky3-recursion/blob/d3ccaf73d5f707b4a2018ac65ece55d329fee934/recursion/src/pcs/fri/verifier.rs#L98).
+
+
+```Rust
+fn evaluate_polynomial<EF: Field>(
+    builder: &mut CircuitBuilder<EF>,
+    coefficients: &[Target],
+    point: Target,
+) -> Target {
+    let mut result = coefficients[coefficients.len() - 1];
+    for &coeff in coefficients.iter().rev().skip(1) {
+        result = builder.mul(result, point);
+        result = builder.add(result, coeff);
+    }
+    result
+}
+```
+
+This is Horner evaluation, but implemented over a circuit builder abstraction. For a first PoC we extract a simpler arithmetic-only version.
+
+## Rust side (implementation + extraction target)
+
+**Create an extraction-friendly Rust crate**
+
+```bash
+cd zkvm-merkle-lean-verified/rust
+cargo new --lib horner_eval_rs
+cd horner_eval_rs
+cargo add --target 'cfg(hax)' --git https://github.com/hacspec/hax hax-lib
+
+```
+
+**Extraction-friendly Horner implementation**
+
+Because the hax Lean backend is still evolving (and iterator support is limited), we avoid Rust iterators and write the loop using while. This keeps the algorithm identical but reduces extraction complexity.
+
+```Rust
+pub fn horner_eval_i64(coeffs: &[i64], x: i64) -> i64 {
+    // p(x) = a0 + a1*x + ... + an*x^n
+    // Horner: (((an*x + a_{n-1})*x + ...)*x + a0)
+    if coeffs.is_empty() {
+        return 0;
+    }
+
+    let mut i = coeffs.len();
+    let mut acc = coeffs[i - 1];
+
+    while i > 1 {
+        i -= 1;
+        acc = acc * x + coeffs[i - 1];
+    }
+    acc
+}
+
+#[cfg(test)]
+mod tests {
+    use super::*;
+
+    #[test]
+    fn horner_basic() {
+        // p(x) = 3 + 2x + x^2, x=10 => 3 + 20 + 100 = 123
+        let coeffs = [3i64, 2i64, 1i64];
+        assert_eq!(horner_eval_i64(&coeffs, 10), 123);
+    }
+
+    #[test]
+    fn empty_is_zero() {
+        let coeffs: [i64; 0] = [];
+        assert_eq!(horner_eval_i64(&coeffs, 7), 0);
+    }
+}
+```
+
+**Run hax extraction**
+
+We extract to:
+- lean-compoly/CompPolyEval/Extracted/Horner_eval_rs.lean
+
+For convenience we added a script:
+- scripts/extract_horner_to_compoly.sh
+
+## Lean side (CompPoly specification)
+
+We created a separate Lean project:
+
+- lean-compoly/
+
+and added CompPoly as a dependency.
+
+**Specification module**
+
+We added:
+
+- lean-compoly/CompPolyEval/Spec.lean
+
+This defines a univariate polynomial model (one variable) over ℤ using CompPoly:
+
+- P := CPoly.CMvPolynomial 1 ℤ
+- X0 as the variable X in one dimension
+- polyOfCoeffs : List ℤ → P building the polynomial from coefficients
+- evalAt : ℤ → P → ℤ using CPoly.CMvPolynomial.eval
+
+This enables a clean mathematical statement of Horner correctness in Lean once the extracted code can be compiled in the same environment.
+
+## Proof plan (WIP)
+
+A direct equivalence proof between the extracted Rust function and the CompPoly spec over ℤ will require:
+
+- Panic/exception freedom (or bounds assumptions) for the extracted i64 code, since the hax Lean model uses RustM and overflow-aware operators.
+- A semantic bridge from machine integers (i64) to mathematical integers (ℤ), typically under bounds that rule out overflow.
+- The main functional correctness theorem: extracted Horner evaluation equals evalAt of polyOfCoeffs.
+
+## Current bottleneck: Lean toolchain version mismatch
+
+At the time of writing, the blocker for a single-project end-to-end pipeline is Lean version pinning across libraries:
+
+- hax Lean prelude was pinned to a single Lean version and is sensitive to Lean changes.
+- CompPoly and ArkLib were pinned to different Lean versions.
+
+This prevented compiling the hax-extracted Horner module in the same Lean project as CompPoly.
+
+### Coordination outcome (major progress)
+
+As a result of issues raised during this work, maintainers of hax, CompPoly, and ArkLib agreed to converge on a unified Lean toolchain version:
+
+**Lean 4.26.0**
+
+Once these upgrades land, we expect the end-to-end pipeline:
+
+**Rust → hax → CompPoly spec → proofs**
+
+to become feasible without splitting across incompatible Lean versions.
+
+Reference discussion: hax issue [#1873](https://github.com/cryspen/hax/issues/1873)
+
+## Artifacts in this repository
+
+- rust/horner_eval_rs/ — Rust Horner implementation (tests pass)
+- scripts/extract_horner_to_compoly.sh — extraction helper
+- lean-compoly/CompPolyEval/Spec.lean — CompPoly-based specification (typechecks)
+- lean-compoly/CompPolyEval/Extracted/Horner_eval_rs.lean — hax-extracted Lean code (generated; compilation depends on toolchain alignment)
+
+## Next steps
+
+- Update dependencies once hax/CompPoly/ArkLib are on Lean 4.26.0.
+- Compile extracted Horner code and write the first proof obligations:
+    - panic-freedom / bounds,
+    - correctness w.r.t. CompPoly eval.
+- Add additional normalization lemmas/tactics (simp/grind sets) as needed to support proof automation for Horner and future polynomial components.

lean-compoly/.gitignore

@@ -0,0 +1 @@
+/.lake

lean-compoly/CompPolyEval.lean

@@ -0,0 +1,4 @@
+-- This module serves as the root of the `CompPolyEval` library.
+-- Import modules here that should be built as part of the library.
+import CompPolyEval.Basic
+import CompPolyEval.HornerProof

lean-compoly/CompPolyEval/Basic.lean

@@ -0,0 +1,19 @@
+import CompPoly.Multivariate.CMvPolynomial
+import CompPoly.Multivariate.MvPolyEquiv
+import CompPoly.Multivariate.Lawful
+
+namespace CompPolyEval
+
+abbrev P := CPoly.CMvPolynomial 1 ℤ
+
+-- constant polynomial 3 in 1 variable ring
+def pConst : P := (CPoly.Lawful.C (n := 1) (R := ℤ) 3)
+
+-- X_0 lives in 1-variable ring, and Lawful.X 0 has type Lawful 1 ℤ
+def X0 : P := (CPoly.Lawful.X 0)
+
+def p : P := pConst + (CPoly.Lawful.C (n := 1) (R := ℤ) 2) * X0
+
+#check p
+
+end CompPolyEval

lean-compoly/CompPolyEval/Extracted/Horner_eval_rs.lean

@@ -0,0 +1,39 @@
+
+-- Experimental lean backend for Hax
+-- The Hax prelude library can be found in hax/proof-libs/lean
+import Hax
+import Std.Tactic.Do
+import Std.Do.Triple
+import Std.Tactic.Do.Syntax
+open Std.Do
+open Std.Tactic
+
+set_option mvcgen.warning false
+set_option linter.unusedVariables false
+
+def Horner_eval_rs.horner_eval_i64
+  (coeffs : (RustSlice i64))
+  (x : i64)
+  : RustM i64
+  := do
+  if (← (Core.Slice.Impl.is_empty i64 coeffs)) then
+    (pure (0 : i64))
+  else
+    let i : usize ← (Core.Slice.Impl.len i64 coeffs);
+    let acc : i64 ← coeffs[(← (i -? (1 : usize)))]_?;
+    let ⟨acc, i⟩ ←
+      (Rust_primitives.Hax.while_loop
+        (fun ⟨acc, i⟩ => (do (pure true) : RustM Bool))
+        (fun ⟨acc, i⟩ => (do
+          (Rust_primitives.Hax.Machine_int.gt i (1 : usize)) : RustM Bool))
+        (fun ⟨acc, i⟩ => (do
+          (Rust_primitives.Hax.Int.from_machine (0 : u32)) : RustM
+          Hax_lib.Int.Int))
+        (Rust_primitives.Hax.Tuple2.mk acc i)
+        (fun ⟨acc, i⟩ => (do
+          let i : usize ← (i -? (1 : usize));
+          let acc : i64 ←
+            ((← (acc *? x)) +? (← coeffs[(← (i -? (1 : usize)))]_?));
+          (pure (Rust_primitives.Hax.Tuple2.mk acc i)) : RustM
+          (Rust_primitives.Hax.Tuple2 i64 usize))));
+    (pure acc)

lean-compoly/CompPolyEval/HornerProof.lean

@@ -0,0 +1,4 @@
+import CompPolyEval.Extracted.Horner_eval_rs
+
+-- Sanity: check the extracted name exists
+#check Horner_eval_rs.horner_eval_i64

lean-compoly/CompPolyEval/Spec.lean

@@ -0,0 +1,18 @@
+import CompPoly.Multivariate.CMvPolynomial
+import CompPoly.Multivariate.Lawful
+
+namespace CompPolyEval
+
+abbrev P := CPoly.CMvPolynomial 1 ℤ
+
+def x0 : Fin 1 := ⟨0, by decide⟩
+def X0 : P := CPoly.Lawful.X 0
+
+def evalAt (x : ℤ) (p : P) : ℤ :=
+  CPoly.CMvPolynomial.eval (R := ℤ) (n := 1) (fun (_ : Fin 1) => x) p
+
+def polyOfCoeffs : List ℤ → P
+| []      => (CPoly.Lawful.C (n := 1) (R := ℤ) 0)
+| c :: cs => (CPoly.Lawful.C (n := 1) (R := ℤ) c) + X0 * polyOfCoeffs cs
+
+end CompPolyEval

lean-compoly/Main.lean

@@ -0,0 +1,4 @@
+import CompPolyEval.Basic
+
+def main : IO Unit :=
+  IO.println "CompPolyEval build ok"