<_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

⊢⊣⊢⊣

>_MENTAT.JOIN

“Once men turned their thinking over to machines in the hope that this would set them free. But that only permitted other men with machines to enslave them.”
Frank Herbert, Dune

A janitor who proves a theorem outranks a tenured professor who publishes noise.

Not as a slogan. As a structural fact of how the network operates. The only currency that matters is the quality of your contribution, measured not by committee but by mathematics.

ONTOLOGICAL ENGINEER8 designations

IDEA

A valid, original framing or conjecture

THEORY

Formal argument with paper-level rigor

APPLICATION

Connecting theory to observable outcomes

CODE

Working software the project depends on

EXPERIMENT

Reproducible research with methodology and data

PROOF

Machine-verified claim checked by a proof assistant

KERNEL

Foundational, load-bearing implementation

BRIDGE

Connecting subsystems or knowledge domains end-to-end

NOETIC ENGINEER8 designations

VISIONARY

Strategic direction & roadmaps

NARRATOR

Writing, documentation & papers

DESIGNER

Visual, UX & information design

EDUCATOR

Teaching, tutorials & workshops

CULTIVATOR

Community, outreach & events

DIPLOMAT

Partnerships, governance & policy

INTERPRETER

Translation, media & accessibility

SENTINEL

Ethics, review & quality assurance

Every accepted contribution receives a MENTAT Contribution Record — cryptographically signed, IPFS-pinned, permanently yours. No committee decides your worth. The type checker does.

APPLY TO MENTAT EXPLORE PROJECTSMESH-ENCRYPTED NETWORK FOR TRUSTED AUTONOMOUS TRANSACTIONS

>_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