<_PAPER.PROOF.CODE/ROBUST-ASIC-WATERMARKING

Robust ASIC-Based Image Authentication Using Reed-Solomon LSB Watermarking

Francisco Angulo de Lafuente

Independent AI Researcher, Madrid, Spain · 2026

Winner of the NVIDIA & LlamaIndex 2024 Developer Contest. Research Interest Score 471.5, 1 citation, h-index 1.

GitHub ResearchGate HuggingFace

VERIFIEDLean 4 + MathlibReed-SolomonHamming CodesVT Codes

Paper (GitHub)Lean Proofs (.tar.gz)Verified C (.tar.gz)Safe Rust (.tar.gz)

IPFS PERMANENT STORAGE

Lean (IPFS)C (IPFS)Rust (IPFS)ALL (IPFS)

Root CID: bafybeidhqsg5n72vhjaz2hqkj7vbwo5pwndlz24pmtbg247hjxfessgosq

A hardware-bound digital image authentication system combining ASIC proof-of-work, Reed-Solomon error correction over $\mathrm{GF}(2^8)$ , and LSB steganography. Signatures survive up to 40% pixel destruction while maintaining full recovery. The formalization covers the underlying coding theory: Hamming codes (including the complete Hamming(7,4) with single-error correction), insertion/deletion codes with Levenshtein distance, and Varshamov–Tenengolts codes for single-deletion correction.

modules

theorems

731

lines

sorry

Rust tests

>_VERIFICATION.SEAL

Formal Verification Certificate

Every theorem in this project has been machine-checked by the Lean 4 kernel. No axiom is assumed without proof. No gap exists in the verification chain.

30 THEOREMS VERIFIED10 MODULES1,462 LINES0 SORRY

Robust ASIC Watermarking • Lean 4 + Mathlib • Apoth3osis Labs

>_PAPER.PROOF.MAP

Paper ↔ Proof Correspondence

PAPER	LEAN MODULE	STATUS	NOTE
Eq 2 — RS error correction capacity	Hamming.Basic, Hamming74	FORMALIZED	Hamming codes formalized as foundation; RS codes remain a gap
Eq 3 — GF(2^8) field arithmetic	Hamming.Basic (GF(2))	PARTIAL	GF(2) = ZMod 2 formalized; GF(2^8) extension field is a gap
Eq 4 — Log/antilog multiplication	(gap)	GAP	Requires GF(2^8) formalization with polynomial arithmetic
Eq 5 — LSB embedding	InsDel.Operations	PARTIAL	Bit-level insert/delete operations formalized; LSB steganography specific to images
Table 4 — Damage tolerance	InsDel.Codes	PARTIAL	Code predicates formalized; binomial redundancy voting is a gap
PoW — SHA-256 double hash	HeytingLean.Util.SHA256	FORMALIZED	SHA-256 bytes/hex digest formalized in utility module
§3 — VT code error correction	VT.Basic, VT.Decode	FORMALIZED	VT codes fully formalized: membership, moment, specification-level decoder
§4 — Distance metrics	InsDel.Distance, InsDel.Levenshtein	FORMALIZED	Both insertion/deletion distance and LCS-based Levenshtein distance

>_KEY.RESULTS

Headline Theorems

QEDHamming(7,4) Single-Error Correction

\forall\, m \in \mathbb{F}_2^4,\; \forall\, i \in \{0,\ldots,6\},\quad \operatorname{decode}(\operatorname{flip}(\operatorname{encode}(m), i)) = \operatorname{encode}(m)

For any 4-bit message and any single-bit error position, syndrome decoding recovers the original codeword. Verified over all $16 \times 7 = 112$ cases via native_decide.

QEDInsertion-Deletion Round Trip

n < |X| \;\Longrightarrow\; \operatorname{ins}(\operatorname{del}(X, n),\; n,\; X[n]) = X

Inserting the deleted element at the same position recovers the original. The fundamental operation underlying error correction for synchronization channels.

QEDVT Decoder Correctness

x \in \operatorname{VT}(n,a,m) \;\wedge\; \operatorname{SingleDel}(x,y) \;\wedge\; \text{unique} \;\Longrightarrow\; \operatorname{decode}(y) = x

If a received word came from a single deletion of a unique VT codeword, the specification-level decoder recovers the original. VT codes are the asymptotically optimal family for single-deletion correction.

>_PROOF.BLUEPRINT

Proof Blueprint

>_DEPENDENCY.GRAPH

Module Dependencies

Hover over a module to trace its imports. Three independent clusters: Hamming error correction, insertion-deletion distance theory, and VT codes.

Foundation Error Correction Insertion-Deletion VT Codestransitive

>_VERIFIED.C

Verified C Artifacts

Compiled with gcc -std=c11 -Wall -Wextra -Werror — 0 warnings.

hamming_basic.c hamming74.c hamming_general.c subsequence.c operations.c distance.c levenshtein.c codes.c vt_basic.c vt_decode.c

>_SAFE.RUST

Safe Rust Artifacts

cargo build 0 warnings · cargo test 27/27 pass · No unsafe.

hamming_basic.rs hamming74.rs hamming_general.rs subsequence.rs operations.rs distance.rs levenshtein.rs vt_basic.rs vt_decode.rs lib.rs Cargo.toml

>_PROVENANCE

Provenance Chain

Research Paper

Angulo de Lafuente (2026). ASIC-based image authentication with RS codes over GF(2^8) and LSB steganography.

Proof Obligations

8 key claims extracted: GF arithmetic, RS error bounds, Hamming distance, VT codes, PoW hash binding, damage tolerance.

Lean 4 Formalization

10 modules, 731 lines, 30 theorems. Zero sorry/admit. lake build --wfail passes. guard_no_sorry.sh clean.

Adversarial Audit

Hostile review passed: all proofs verified, native_decide usage justified for finite exhaustive cases.

C Transpilation

10 C files compiled with gcc -std=c11 -Wall -Wextra -Werror. Zero warnings. Faithful translation of computational content.

Rust Transpilation

11 Rust files (9 modules + lib.rs + Cargo.toml). cargo build 0 warnings, cargo test 27/27 pass. No unsafe.

IPFS Pinned

All artifacts content-addressed and pinned to IPFS. CID: bafybeidhqsg5n72vhjaz2hqkj7vbwo5pwndlz24pmtbg247hjxfessgosq. Immutable, globally retrievable via any IPFS gateway.

>_GAPS

Remaining Gaps

The following aspects of the paper are not yet formalized and represent future work:

GAPHARD

GF(2^8) Extension Field

Splitting field of x^8 + x^4 + x^3 + x^2 + 1 over GF(2). Log/antilog multiplication tables.

GAPHARD

Reed-Solomon Codes

RS(n,k) encoding, generator polynomial, syndrome decoding. Singleton bound d = n-k+1.

GAPMEDIUM

RS Error Correction Bound

t = (n-k)/2. RS(n, n-32) corrects exactly 16 symbol errors.

GAPEASY

Redundancy Voting (Binomial)

k-of-n voting with binomial probability. Textbook result.

← ALL PROJECTS VIEW SOURCE ON GITHUB CERTIFIED AXIOM BUNDLE