Skip to content

README.md

Latest commit

 

History

History
305 lines (239 loc) · 11.6 KB

README.md

File metadata and controls

305 lines (239 loc) · 11.6 KB
Raw

A Constructive Proof of Rice's Theorem via Hilbert's Tenth Problem

Author: Jonathan Brossard (jonathan.brossard@moabi.com)
ORCID: 0009-0004-8031-1438

This repository contains the full source for the paper "A Constructive Proof of Rice's Theorem via Hilbert's Tenth Problem", including the mechanically verified Rocq formalization and a concrete C witness to the theorem.

Summary

Classical proofs of Rice's theorem invoke the law of excluded middle (LEM) twice: once via diagonalization, and once via the case split P(⊥) ∨ ¬P(⊥). This paper replaces both with a direct reduction from Hilbert's Tenth Problem (MRDP theorem), using a two-witness construction that is valid in intuitionistic logic without any classical reasoning.

The proof is mechanically verified by Rocq (Coq). The single axiom used is H10C_SAT_undec — the undecidability of H10C constraints, imported from coq-library-undecidability. Rice_Theorem and Halting_Problem are Closed under the global context.

Repository Contents

File Description
rice.tex LaTeX source (LMCS format, requires lmcs.cls)
rice.bib BibTeX bibliography (15 entries, DOIs included)
rice.v Rocq proof source — compile with coqc rice.v
lmcs.cls LMCS style file
alphaurl.bst BibTeX style for LMCS format
undecidable.c Concrete C witness to Rice's theorem
Makefile Build system
Dockerfile Reproducible build environment (Ubuntu 24.04)

Quick Start

With Docker (recommended — fully reproducible)

make docker         # build the image: installs all dependencies, verifies
                    # the Rocq proof, compiles rice.pdf, builds undecidable
make docker-run     # run the container and copy outputs to ./out/
make docker-rocq    # re-run the Rocq proof inside a fresh container
make docker-clean   # remove the image and ./out/

What each target does:

  • make docker — runs docker build. All build steps execute inside Ubuntu 24.04: apt installs, coqc rice.v (proof verified), pdflatex (PDF compiled), gcc (C witness built). A successful build guarantees all three artifacts are correct.
  • make docker-run — runs the container and copies rice.pdf, rice.vo, and undecidable to ./out/ on the host.
  • make docker-rocq — runs coqc rice.v in a fresh container instance, printing the Coq version and confirming the single axiom. Useful for demonstrating proof validity to a third party without relying on the cached build.
  • make docker-clean — removes the rice-constructive image and ./out/.

Output files after make docker-run:

out/rice.pdf        — paper, LMCS format
out/rice.vo         — compiled Rocq object (proof accepted)
out/undecidable     — C binary: concrete undecidable analysis target

Without Docker (Ubuntu/Debian)

Install dependencies:

sudo apt install coq texlive-latex-extra texlive-bibtex-extra \
                 texlive-fonts-recommended texlive-science libgmp-dev

Build:

make all        # PDF + Rocq proof + C binary
make pdf        # rice.pdf only
make rocq       # verify Rocq proof only
make c          # build undecidable only
make run        # build and run undecidable.c with example polynomials

Dependencies

Rocq (Coq)

  • Version: 8.18 or later (tested on 8.18 and 8.20)
  • Install: sudo apt install coq
  • Packages used: Arith List Bool Lia ZArith (all in the standard library)
  • No external libraries required

The proof uses only these tactics: intros, induction, destruct, rewrite, lia, apply, exact, injection, reflexivity, case_eq, simpl, pose proof. All have been stable since Coq 8.10.

GMP (GNU Multiple Precision)

  • Required for undecidable.c — provides unbounded integer arithmetic
  • Install: sudo apt install libgmp-dev
  • Why required: The Rocq proof reasons over infinite nat. The search counter n in run_search() uses GMP mpz_t as a correctness requirement: a fixed-width counter would exhaust its range in finite time, making the search trivially terminating and invalidating the formal claim. The polynomial evaluation also uses mpz_t to handle arbitrary integer coefficients and exponents without overflow. See the comment in undecidable.c and Remark 9.1 in the paper for the full rationale.

LaTeX

  • pdflatex (TeX Live 2023 or later)
  • bibtex
  • texlive-latex-extra (for listings, booktabs, enumitem)
  • texlive-bibtex-extra (for alphaurl.bst, required by LMCS format)
  • texlive-fonts-recommended

Makefile Targets

make all          build PDF + verify Rocq proofs + build C binary (default)
make pdf          build rice.pdf
make rocq         verify Rocq proofs
make c            build undecidable C binary
make run          build and run undecidable.c with example polynomials
make check        alias for rocq
make install      install all dependencies via apt
make axioms       print axioms used by the proof
make clean        remove auxiliary files + C binary (never touches source)
make distclean    clean + remove .pdf and .vo
make help         show status of all dependencies
make docker       build Docker image (fully reproducible)
make docker-run   build image and copy outputs to ./out/
make docker-rocq  run Rocq proof verification inside Docker
make docker-clean remove Docker image and ./out/

Proof Structure

The Rocq formalization in rice.v is organized as follows:

  1. Diophantine infrastructure — k-ary Cantor encoding, polynomial evaluation, check_solution, is_solvable, is_unsolvable
  2. Computation model — step-indexed programs (nat → nat → option nat), observational equivalence (obs_equiv)
  3. Search dynamics — find_sol with monotonicity lemmas (find_sol_step, find_sol_stable, find_sol_bound, find_sol_at_n, find_sol_unsolvable)
  4. Semantic properties — SemanticProperty record, NonTrivial record
  5. Two-witness construction — S_D definition, S_D_solvable_equiv, S_D_unsolvable_equiv
  6. H10C undecidability axiom — H10C_SAT_undec (the single external axiom, from coq-library-undecidability). Rice_Theorem and Halting_Problem are Closed under the global context.
  7. Main theorem — Rice_Theorem

Verifying the Proof

coqc rice.v

Exit code 0 means all goals are closed. To inspect the single axiom:

grep "Hypothesis\|Axiom" rice.v

Expected output:

  (* H10C_SAT_undec: sole external axiom, from coq-library-undecidability *)
  Axiom H10C_SAT_undec :

Cybersecurity Relevance

Rice's theorem is the formal foundation for why fully automatic semantic vulnerability detection is impossible in general. The constructive version strengthens this: the undecidability holds in intuitionistic logic, meaning it cannot be evaded by restricting the computational model. It is grounded in the undecidability of Diophantine arithmetic — the same reason no algorithm can decide integer solutions to polynomial equations.

For PSIRTs, vulnerability researchers, and tool vendors: this is the formal basis for why any claim of "complete" static analysis is false. Bounded analysis (as implemented in WCC) is not a limitation — it is the principled response to a provable ceiling.

Citation

@article{brossard2026rice,
  author  = {Jonathan Brossard},
  title   = {A Constructive Proof of {R}ice's Theorem
             via {H}ilbert's Tenth Problem},
  journal = {Logical Methods in Computer Science},
  year    = {2026},
  note    = {Submitted. Preprint: arXiv:2604.16477}
}

License

The Rocq proof (rice.v), LaTeX source (rice.tex, rice.bib), and C witness (undecidable.c) are released under CC BY 4.0.

lmcs.cls and alphaurl.bst are not authored by this repository and retain their respective licenses.

A Concrete Undecidable Analysis Target

The file undecidable.c is a single C program whose termination is provably undecidable by static analysis. It takes an arbitrary Diophantine polynomial as its sole argument and searches for a root in the naturals — a direct executable image of the S_D family from rice.v. Its undecidability is a consequence of Theorem Rice_Theorem.

Build and run

gcc -O2 -std=c17 undecidable.c -o undecidable -lgmp -lm

# Solvable polynomial — terminates immediately
./undecidable "x1^2 - x2^2 - x3^2 - 1"

# No solution in N — runs forever
./undecidable "x1^2 + 1"

How it works

The program parses a polynomial D(x1, ..., xk) from its command-line argument and searches N^k for a tuple with D = 0. It enumerates all tuples via iterated Cantor unpairing of a single unbounded counter n, evaluates D at each tuple using GMP exact arithmetic, and halts with a witness if and only if one is found. The search counter n uses GMP mpz_t as a correctness requirement: a fixed-width counter would make the search finite and invalidate the formal claim.

Before printing, the witness is re-verified by an independent evaluation of D — there is exactly one success path in the program, and it holds a genuine solution.

The input parser accepts polynomials in the form c * x1^e1 * x2^e2 ... + ... with integer coefficients. It is explicitly marked as untrusted in the source; the mathematical reduction begins from the internal polynomial representation consumed by the search core.

The formal claim

Theorem Rice_Theorem (in rice.v):
  No computable function can correctly decide, for all programs of this
  form, whether they terminate.

More precisely: termination of undecidable(D) is equivalent to solvability of D. Since solvability of arbitrary Diophantine equations is undecidable (MRDP theorem, mechanized in Rocq at https://github.com/uds-psl/coq-library-undecidability), termination of the program family is undecidable.

This is not a limitation of current tools. It is a theorem. Any static analyzer that claims to decide termination for all programs of this form either:

  • Is wrong on some input (by the Rice/MRDP argument), or
  • Runs forever on some inputs (which is not a decision procedure).

Connection to the Rocq proof

The C function run_search() in undecidable.c mirrors the Rocq definition:

Fixpoint find_sol (ar : nat) (p : Poly) (fuel : nat) : option nat

The Rocq proof constructs two programs S_D^0 and S_D^1 that call find_sol and behave differently depending on whether D is solvable. The C program is a concrete witness to this construction: it takes an arbitrary polynomial D and its behavior (halt vs. diverge) is determined entirely by the solvability of D. Any static analyzer deciding the semantic property "terminates" for this family would, by the proof's construction, decide Diophantine solvability — contradicting H10C_SAT_undec.

Why this matters for cybersecurity

Static analyzers used for vulnerability detection — SAST tools, taint analyzers, model checkers — all decide semantic properties of programs. Rice's theorem implies that any non-trivial semantic property has this undecidable structure. The programs above are not pathological adversarial inputs. They are straightforward integer loops. The undecidability is intrinsic to what static analysis asks, not to how the programs are written.

The constructive proof in rice.v strengthens this: the undecidability holds even in intuitionistic logic, meaning it cannot be evaded by restricting to weaker computational models. The obstacle is Diophantine arithmetic — present in any model expressive enough to run real programs.