adic-lean-proof-replay
ADIC R-SOUND Replay Verification
This repository contains a reproducible Lean 4 proof artifact for ADIC replay verification.
It shows, in a mechanically checked form, that when an ADIC replay certificate is accepted by the verifier, the corresponding semantic-validity condition follows.
In the ADIC architecture, this provides the formal core for preserving accountability after deployment.
Conceptual flow of ADIC replay verification
Note: In this repository, ADIC denotes the audit/verifier architecture studied in the accompanying paper; it is unrelated to p-adic numbers.
The main Lean file is:
ADIC_RSound_Replay.lean
Scope
This repository formalizes the Lean-side replay soundness structure for ADIC.
In particular, it covers the connection between:
certificate rows
spec rows
replay verification
semantic validity
acceptance soundness
The goal is not to verify an entire deployed software system, but to provide a mechanically checked formal core for the replay verification argument used in ADIC.
DAG representation note
The DAG layer in this repository is formalized as a replay-oriented row-list lowering layer. The compiler-correctness lemmas establish correspondence between DAG-level syntax and the compiled replay-row representation used by the verifier.
Accordingly, the DAG results should be read as row-list lowering correctness / replay representation correspondence, not as a full general-purpose compiler correctness theorem for arbitrary deployed software.
Main theorem direction
At a high level, the file establishes that if an ADIC certificate is accepted by the replay verifier, then the corresponding semantic validity condition follows.
This supports the ADIC idea that audit acceptance should not be a loose runtime judgment, but a reproducible verification result.
Reproducibility
This repository is a reproducible Lean/Lake artifact.
The Lean version is fixed by lean-toolchain, and Mathlib is pinned through lake-manifest.json.
A fresh clone should verify with:
git clone https://github.com/GhostDriftTheory/adic-lean-proof-replay.git
cd adic-lean-proof-replay
lake exe cache get
lake build
Successful verification means that lake build completes without errors.
Repository structure
ADIC_RSound_Replay.lean Main Lean formalization
lean-toolchain Lean toolchain pin
lakefile.lean Lake project file
lake-manifest.json Lake dependency lock file generated by `lake update`
.github/workflows/ci.yml GitHub Actions verification workflow
README.md Repository description
Verification evidence
The primary verification evidence is:
fresh clone -> lake exe cache get -> lake build
The GitHub Actions workflow runs the same Lean/Lake verification on every push and pull request.
Screenshots may be kept as supplementary evidence, but they are not the reproducibility mechanism.
Paper-to-Lean correspondence
The accompanying paper contains a full Lean correspondence table. The key identifiers can be checked directly in:
ADIC_RSound_Replay.lean
Representative grep targets are:
| Paper statement | Lean identifier(s) |
|---|---|
| Galois insertion | gc_alpha_gamma, alpha_gamma_strict |
| Truth preservation of tau | tau_preserves, tau_truth |
| FDIV/CDIV witness bounds | fdiv_bound, cdiv_bound |
| R-SOUND for addition/subtraction | rsound_add, rsound_sub |
| R-SOUND for multiplication | rsound_mul, rsound_mul_closed |
| R-SOUND for inverse | rsound_inv, rsound_inv_closed |
| R-SOUND for square root | rsound_sqrt, rsound_sqrt_closed |
| R-SOUND for ReLU | rsound_relu |
| Replay verifier soundness | verifierBool_sound, verifierBool_sound_unique |
| DAG replay soundness | verifierDAGBool_direct_sound, dagCert_end_to_end_sound |
| Structural cost bound | verifierBoolStructuralCost_eq_size, replayVerifierStructuralCost_linear |
Related paper and archival record
Preprint: Verifier Closure for Fixed-Core Interval Programs: A Certified Replay Architecture in Lean4
Archival DOI:
10.5281/zenodo.19808324