Mapping a Lean 4 Computer Vision Library

computervision is a small Lean 4 library written by Kim Lien Vu (@vukimlien4706-cpu) at Hanoi University of Science and Technology. It has RGB and YCbCr colour types, full-range BT.601 conversion in both directions, a simple array-backed image type, and an EMVA 1288-style sensor characterisation module that turns pairs of dark and illuminated frames into gain, read noise, saturation capacity, SNR and dynamic range. The README calls it the author’s first Lean project.

I did not write any of that code. My contribution was documentation: an architecture atlas made of one overview diagram and twelve focused Mermaid views, each rendered as light and dark PNGs, plus the script and theme files to re-render them. The author merged it upstream as pull request #1 on 23 September 2026. This post covers what an atlas is, how I chose the views, and what the review view found when I wrote down what the code actually does.

Status: research. The library is a learning project with a console demo. It has no assertion tests or formal proofs, and neither the library nor the atlas claims EMVA 1288 compliance.

What I mean by an architecture atlas

A single architecture diagram either leaves things out or turns into a wall of boxes. An atlas is a set of diagrams with one overview and several focused views. Each view answers one question and links back to the same named boundary nodes, so you can move between them without getting lost. I hold it to four rules:

• It describes the code as it is. No planned features, no “should”. The README of the atlas says the diagrams “describe implementation behavior, not verified EMVA standards compliance.”
• Every declaration appears somewhere. If a function or type exists in tracked source, at least one view shows it.
• Arrows mean one thing per style. Solid arrows are imports, calls or data flow, as labelled. Dotted arrows are configuration, type relationships or review caveats.
• No cross-page wires. When a node shows up in two views, it keeps the same name in both, so a reader can match them by eye.

For a 411-line library (61 lines in Basic.lean, 53 in Image.lean, 257 in EMVA1288.lean, 40 in Main.lean), thirteen diagrams can look like too many. But each view stays small enough to read at normal zoom, and together they cover every declaration. A newcomer can follow one question at a time. A reviewer can check each diagram against a single file.

The overview

The overview fits on one page. It shows the two entry points (the console demo and any library caller), the umbrella module Computervision.lean, the three library layers with their import direction, the sensor-analysis data flow, and a box stating the scope: a pure in-memory library plus a console demo, with no acquisition, codecs, GUI or persistence.

The scope box carries more weight than it looks. Anyone who reads “EMVA 1288” in a project description could assume it talks to cameras. It does not. The caller supplies four Image Float values in digital numbers and a saturation level, and everything else happens in memory.

How I chose the twelve views

I picked views by asking which questions a new reader would have, in the order they would have them, and then checked that the views between them covered every declaration in the source. The resulting list, from docs/architecture/README.md:

Some things I chose deliberately:

• EMVA1288.lean gets four views. It is the largest file and holds the domain logic. Orchestration (06), low-level statistics (07), spatial metrics (08) and derived metrics (09) fit four different reading tasks.
• Formulas are written into the boxes. Views 04 and 09 put the actual expression in each node, for example dynamicRange = saturationCap_e / sensitivityThreshold_e, so a reader can check the diagram against the source line by line.
• The demo gets its own view. Main.lean mixes elaboration-time #eval commands with a runtime main. View 11 separates the two, which matters for the review findings below.
• The last view is a review. It lists current behaviour and limits only, not proposed features. The title says so: “current behavior, not proposed features.”

Here is the source behind three of those boxes:

-- Computervision/EMVA1288.lean
/-- Absolute sensitivity threshold (signal at SNR = 1) in electrons (e⁻) -/
def sensitivityThreshold_e (p : SensorParams) : Float :=
  p.readNoise_e + 0.5

/-- Dynamic Range (linear): saturation capacity / absolute sensitivity threshold -/
def dynamicRange (p : SensorParams) : Float :=
  p.saturationCap_e / (sensitivityThreshold_e p)

/-- Dynamic Range in dB -/
def dynamicRangeDb (p : SensorParams) : Float :=
  20.0 * Float.log10 (dynamicRange p)

The diagram adds one note that is easy to miss in the code. readNoise_DN takes the square root of the raw dark variance, which includes quantisation noise. characterizeFromPairs, on the other hand, subtracts the 1/12 DN² quantisation term before computing read noise in electrons. Both behaviours may be intended. The diagram just puts them next to each other.

How the atlas is built

Each view is a plain-text .mmd file in docs/architecture/; the overview is ARCHITECTURE.mmd in the repository root. A short PowerShell script runs the Mermaid CLI over every source twice, once with a light theme and once with a dark theme, at 2x pixel density:

# docs/architecture/render.ps1
foreach ($source in $sources) {
    foreach ($mode in @('light', 'dark')) {
        $stem = [System.IO.Path]::Combine([System.IO.Path]::GetDirectoryName($source), [System.IO.Path]::GetFileNameWithoutExtension($source))
        $output = if ($source -eq $sources[0] -and $mode -eq 'light') { "$stem.png" } else { "$stem.$mode.png" }
        $background = if ($mode -eq 'dark') { '#0b1220' } else { '#ffffff' }
        & $MermaidCli -i $source -o $output -s 2 -w 1800 -b $background -p $browserConfig -c (Join-Path $PSScriptRoot "$mode.json")

The colours, fonts and spacing live in light.json and dark.json. I used matching high-contrast palettes so text, edges and node fills stay readable in either GitHub theme. The rendered PNGs are committed next to the sources, so readers never need the toolchain. Anyone who edits a diagram can re-render with Node.js, @mermaid-js/mermaid-cli and a Chromium browser. The script never modifies any Lean code.

The whole contribution is commit 13f9ac0: 44 files, 461 lines added and one removed. Most of it is diagram source, PNG renders, the atlas README, the script and the two theme files. The only change to the author’s existing files was a short README paragraph linking to the atlas. That paragraph also includes the sentence “it does not establish EMVA 1288 standards compliance,” which I added deliberately. I wrote the atlas with help from Claude Code, and the commit records that with a co-author line. I reviewed every view against the source before submitting it.

What the review view found

View 12 is the part I would keep even if I dropped every other diagram. Each node on the left is a real declaration. Each node on the right is a caveat about how that declaration currently behaves, connected by a dotted “caveat” edge. None of these are bug reports or requests. They describe the boundaries a caller has to respect.

Image shape is unchecked

Image is a structure with width, height and a pixels array, and nothing in the type ties the array length to width * height. The statistics functions compare pixel counts, not dimensions, so two arrays of the same length but different shapes are accepted together. In practice that only matters if a caller builds images by hand. Image.ofFn always produces a consistent one.

Invalid pairs become a (0, 0) sentinel

-- Computervision/EMVA1288.lean
def emvaTemporalStats (imgA imgB : Image Float) : Float × Float :=
  let n := imgA.pixels.size
  if n == 0 || n != imgB.pixels.size then
    (0.0, 0.0)

characterizeFromPairs rejects the result only when the illuminated-minus-dark mean or variance is not positive. It does not check for the sentinel itself. So a valid illuminated pair combined with a mismatched dark pair can still produce sensor parameters, computed as if the dark frame were zero.

Float domain is unguarded

Every field of SensorParams is a plain Float. Nothing enforces a positive gain or finite values. conversionFactor divides by gainK, and the dB functions call Float.log10 on values that could be zero or negative if a caller builds parameters by hand. Variance uses the sum-of-squares formula, which can lose precision through cancellation, and temporal variance has no non-negative clamp. In Lean these cases give IEEE results such as infinity or NaN, not errors.

Spatial metrics may include temporal noise

DSNU and PRNU are computed from the averaged pairs directly, without subtracting the remaining temporal noise variance. The diagram notes that the computed spatial variation may include temporal noise. I left it to the reader to compare that with the standard. The atlas describes the implementation and does not judge whether it complies.

The demo shows output but checks nothing

Main.lean has four #eval commands and a main function. The sensor report it prints comes from hard-coded values, not from runEMVA1288Analysis:

-- Main.lean
-- 1. Pixel round-trip test (pure red):
#eval FloatConv.rgb8ToYCbCr8 ⟨255, 0, 0⟩
-- Output: { y := 76, cb := 85, cr := 255 }

The expected output is in a comment, so nothing fails if the result changes. Tracked source has no theorem, lemma or assertion test. View 12 says “No dedicated assertion tests or formal proofs in tracked source” and “Comments showing expected results are not executable checks.”

Truncation is worth a test of its own: clampToUInt8 converts with x.toUInt64.toUInt8, which truncates instead of rounding (view 12 notes this too). An assertion on the round-trip values would catch any drift automatically, and a comment cannot.

On “formal verification”

The author archived the project on Zenodo. Version v1.0.3 is DOI 10.5281/zenodo.22908982, credited to Vu, Kim Lien, and the README badge points to the concept DOI 10.5281/zenodo.22885537 for all versions. The archive is titled “Computervision: Formal Verification in Lean 4.” Lean is a theorem prover, so that framing makes sense as the project’s direction. But the source at the commit I examined has no proofs, so the atlas describes executable definitions and their runtime behaviour. Neither the atlas nor this post claims anything has been formally verified.

That is the main thing I would argue for when documenting someone else’s code. The atlas should state the scope precisely enough that nobody reading it comes away believing more than the code supports. If proofs are added later, a “proven properties” view would be easy to add next to the review view.

Why document a small library at all

Small projects get read by students, reviewers, and people deciding whether to build on them, and those readers rarely have time to trace every function. With a dozen diagrams, each matched to a single file, someone can understand the project in minutes and check the details when they need to. The review view also gives the maintainer a list of known limits to work from without anyone opening issues.

I do this same kind of work when helping teams take an existing idea or codebase and work out what it really does before deciding what to build next. That is the starting point of our Idea to Solution service.

Limitations

• The library is a learning project. The README describes it as the author’s first Lean project. It has a console demo and no test suite.
• No proofs or assertion tests. Tracked source has no theorem or lemma declarations and no assertion-based tests. CI runs leanprover/lean-action on push and pull request with no custom test steps, so in practice it confirms the project builds. I did not look up individual CI run results.
• No EMVA 1288 compliance claim. The implementation follows the EMVA 1288 measurement model as described in its own doc comments. The README states the atlas “does not establish EMVA 1288 standards compliance.”
• I did not build or run the Lean code. There is no Lean toolchain on the machine I used to write this. The truncation observation above comes from recomputing the formula in Python.
• The atlas is a snapshot. It matches the source as of commit 13f9ac0. Later code changes would need the matching .mmd files updated and re-rendered by hand, and nothing in CI checks that diagrams and code still agree.
• Rendering needs local tools. The render script expects PowerShell, Node.js, Mermaid CLI and a Chromium path. It has not been wired into CI.

Resources

• vukimlien4706-cpu/computervision (upstream, primary) – MIT License – commit 4bf740d. The atlas is commit 13f9ac0, merged as PR #1.
• CompleteTech-LLC-AI-Research/computervision (our fork, used to prepare the pull request) – source-available on GitHub, no LICENSE file in the fork at its current head – commit cc16cc9, two commits behind upstream.

The computervision library (Basic.lean, Image.lean, EMVA1288.lean, Main.lean) was written by Kim Lien Vu (@vukimlien4706-cpu), Hanoi University of Science and Technology. CompleteTech’s contribution is the architecture atlas documentation only. The project’s MIT license, added by the author after the merge, lists “Hanoi University of Science and Technology, CompleteTech LLC” as copyright holders.