Add proof source visualization atlas by achamayou · Pull Request #67 · microsoft/merklecpp

Amaury Chamayou (achamayou) · 2026-08-05T10:31:53Z

Summary

add an interactive atlas for tile-backed inclusion and consistency proofs;
build the model from the public API only: no library changes, no instrumentation, no parallel proof implementation;
locate each returned proof element in the node map by its SHA-256 digest, so proof roles are discovered rather than predicted;
ask the tile source and the frontier source separately, so each node's provenance and any overlap between them is observed, not inferred from the flush boundary;
draw both trees of a consistency proof, including the old tree's own fold, so it is visible which returned hashes rebuild the old root and which extend it to the new one;
define all 11 scenarios as strict ordered name: value files in tools/proof-viz/scenarios/;
export a versioned strict data.json and load it without executable globals;
match the PyData documentation palette in saved/system light and dark modes;
build, validate, and package the self-contained atlas into the documentation Pages artifact with make_viz.sh.

Base

This PR targets main directly. The tile-backed proof APIs exercised by the atlas landed in #54; #55 remains separate.

How the model is built

Nothing about proof structure is reimplemented. For each scenario the harness:

writes full tiles with TileWriter, and flushes an in-memory Tree to the same boundary;
lays out the RFC 6962 decomposition of the tree, which is shape only;
asks TileHashSource and MemoryHashSource individually for each perfect range. A node answered by both is a genuine overlap, and the two answers are cross-checked for equality;
folds the remaining ranges — exactly the ones the engine has to recombine — with merkle::sha256;
fetches the proof through ProofEngine::inclusion_proof / consistency_proof_from_indices and looks up each element's digest to find its node and its position in proof order.

Because the digests are SHA-256, step 5 is exact, so the atlas needs no access to the engine's internals and cannot drift from them. Inclusion proofs are additionally compared byte-for-byte against Tree::path(), consistency proofs are checked with ProofEngine::verify_consistency(), and both drawn roots are checked against Tree::past_root().

Consistency proofs relate two sizes

consistency_proof_from_indices(a, b) is consistency_proof(a + 1, b + 1), and SUBPROOF takes only the two sizes. The selected leaf indices name those sizes and appear in none of the five proofs, so the scenes lead with old tree / new tree sizes and mark the leaves only as where each tree ends.

The smaller tree has a right spine of its own — the ranges a verifier folds proof elements into to recover the old root — and those ranges are absent from the larger tree unless its size is an aligned power of two. Both decompositions are merged into one node map, and each range records its parent in both trees. Where those parents differ, the old tree's edge is drawn, which is precisely its fold:

scene	old	new	returned hashes	rebuild the old root
`consistency-boundary`	256	300	1	0, the old root is already a node of the new tree
`consistency-frontier-only`	48	150	5	2
`consistency-tiled-history`	128	400	2	0, as above
`consistency-arbitrary-crossing`	92	288	8	4
`consistency-frontier-pair`	270	494	9	4

The two single-digit proofs are the degenerate case, not missing data: when the old size is an aligned power of two, SUBPROOF returns immediately and verifying is one sha256 of the old root and the remainder.

Build and view

tools/proof-viz/make_viz.sh
python3 -m http.server 4173 --directory tools/proof-viz

Open http://localhost:4173/. CI calls the same script with doc/build/proof-viz as its output directory.

The generated site contains index.html, styles.css, app.js, and data.json. The JSON document has schemaVersion 5, tileWidth, a flags legend, and a list of scenarios. Nodes are parallel columns — lo, hi, height, parent, parentFirst, flags — plus proof as node ids in proof order, firstRoot / secondRoot, and tiles as the [level, index] pairs that reached disk. Ranking is by height above the leaves rather than depth below the root, so every leaf shares a baseline in an unbalanced tree.

Validation

11 scenarios, 7,916 nodes, 67 proof elements, 12 tile files, and a 156 KB data.json;
every proof element is found in the node map by digest, so a drifted model fails the build rather than drawing the wrong thing;
both roots of every consistency proof match past_root(), and every inclusion proof matches Tree::path() byte-for-byte;
proof sizes agree with an independent RFC 6962 SUBPROOF implementation;
make_viz.sh validates shell/JavaScript syntax and the strict scenario file shape: exact key order, no stray whitespace or control characters, no extra lines, and name matching the file name, each rejection checked against a deliberately malformed file;
generated data.json and build outputs remain ignored.

Add HashSourceT (abstract subtree-root resolver), TileHashSourceT (resolves from full tiles, with an LRU tile cache), ProofEngineT (inclusion/consistency proofs and their verifiers, built on mth_range), MemoryHashSourceT (resolves from a resident in-memory tree), and CombinedHashSourceT (memory first, falling back to tiles). Add the sole essential core change: TreeT::subtree_root(), a read-only, non-hashing accessor that lets proofs be served from the resident tree, plus the <limits> include it needs. No other merklecpp.h changes. Add tiles_proofs tests, cross-checking tile-derived inclusion and consistency proofs against merkle::TreeT as the oracle across a range of sizes, including tile-boundary crossings. Move the memory-only subtree_root proof coverage and the ProofEngineProbe hostile-arithmetic edge cases here from tree coverage, since they exercise the proof engine and core accessor rather than TiledTree lifecycle. Add tiles_level2 for end-to-end coverage of the level-2 tile path. Introduce the LONG_TESTS CMake option, gate tiles_level2 behind it, and enable it in CI (and CodeQL) so long-running tile coverage runs on pull requests. Document the compatibility statement, the optional core accessor, and the HashSource/ProofEngineT API and algorithms in the design doc. Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com>

Use the current default tree hash function for public proof aliases, reject index conversions that cannot be represented safely, and align the design and level-2 coverage notes with the rebased implementation. Co-authored-by: Copilot App <223556219+Copilot@users.noreply.github.com> Copilot-Session: c504572c-322f-4950-8682-edf4a7fd2c5b

Co-authored-by: eddyashton <6000239+eddyashton@users.noreply.github.com>

Copilot

Pull request overview

Adds a self-contained “proof visualization atlas” under tools/proof-viz/ that generates a strict data.json trace from real tile/memory proof resolution, and ships a static HTML/CSS/JS viewer as part of the documentation build artifact.

Changes:

Introduces a C++ harness (proof_viz.cpp) + scenario files to generate and validate traced inclusion/consistency proof resolution attempts.
Adds a static frontend (index.html, styles.css, app.js) that renders the atlas (tile/frontier/computed nodes, routes, and resolver attempts) from data.json.
Extends the docs workflow to build and package the atlas into the Pages artifact, and links to it from the Sphinx docs landing page.

Reviewed changes

Copilot reviewed 19 out of 19 changed files in this pull request and generated 3 comments.

Show a summary per file

File	Description
tools/proof-viz/styles.css	Theme + layout styling for the atlas (light/dark, responsive, print).
tools/proof-viz/scenarios/tile-to-frontier.scenario	Defines an inclusion scenario crossing from tile-backed history to frontier.
tools/proof-viz/scenarios/next-frontier.scenario	Defines an inclusion scenario starting at the first post-tile frontier leaf.
tools/proof-viz/scenarios/near-boundary.scenario	Defines an inclusion scenario just before a tile completion boundary.
tools/proof-viz/scenarios/frontier-to-tile.scenario	Defines an inclusion scenario that needs a tile lookup late in the proof.
tools/proof-viz/scenarios/frontier-only.scenario	Defines an inclusion scenario entirely within the resident frontier.
tools/proof-viz/scenarios/consistency-tiled-history.scenario	Defines a consistency scenario fully satisfiable from tiled history.
tools/proof-viz/scenarios/consistency-frontier-pair.scenario	Defines a consistency scenario with both checkpoints beyond the first tile.
tools/proof-viz/scenarios/consistency-frontier-only.scenario	Defines a consistency scenario entirely before tiling begins.
tools/proof-viz/scenarios/consistency-boundary.scenario	Defines a consistency scenario spanning the flush boundary.
tools/proof-viz/scenarios/consistency-arbitrary-crossing.scenario	Defines a consistency scenario with an arbitrary A/B pair crossing tile/frontier.
tools/proof-viz/scenarios/boundary-overlap.scenario	Defines an inclusion scenario at the exact two-tile boundary (overlap case).
tools/proof-viz/proof_viz.cpp	Generates scenarios, traces `HashSource::subtree_root` attempts, verifies proofs, and writes the `data.json` contract.
tools/proof-viz/make_viz.sh	Builds the generator, produces `data.json`, validates JS + JSON shape, and copies site assets to output.
tools/proof-viz/index.html	Static page structure and controls for the atlas UI.
tools/proof-viz/app.js	Frontend renderer: loads `data.json`, builds node maps, draws canvases, and wires UI toggles/filters.
tools/proof-viz/.gitignore	Ignores generated `data.json` in the source directory.
doc/index.rst	Adds a docs entry linking to the generated `proof-viz/` site.
.github/workflows/build-docs.yml	Runs on PRs and builds the proof visualization into `doc/build/proof-viz` before uploading the Pages artifact.

💡 Add Copilot custom instructions for smarter, more guided reviews. Learn how to get started.

Co-authored-by: Copilot Autofix powered by AI <175728472+Copilot@users.noreply.github.com>

Max (maxtropets) · 2026-08-11T12:06:37Z

I've hit a blind approve, because I sort of hope the visualization is correct, although there's no breakdown/tests to make sure of that.

Code style makes me sad. I think with time we may develop a sort of general (repo-agnostic) LLM-skills, so the code looks consistent, at least across a single project. I'm not going to bikeshed here tho, this feature clearly isn't worth it.

Amaury Chamayou (achamayou) · 2026-08-11T12:39:23Z

I've hit a blind approve, because I sort of hope the visualization is correct, although there's no breakdown/tests to make sure of that.

We don't have tests for other visualisation tools we have either. Since this is purely for documentation, and not a release artifact, I think that's ok.

Code style makes me sad. I think with time we may develop a sort of general (repo-agnostic) LLM-skills, so the code looks consistent, at least across a single project. I'm not going to bikeshed here tho, this feature clearly isn't worth it.

It would be helpful if you could point to concrete inconsistencies. There's no visualisation tooling in this repository, and I don't think proof_viz.cpp is particularly inconsistent with the way testcases are written in this repo. I agree we want consistent code, hence why I did a round of fixing and hooked up clang-tidy in #33, but further improvements are obviously welcome.

Co-authored-by: Copilot App <223556219+Copilot@users.noreply.github.com>

Max (maxtropets) · 2026-08-11T12:57:21Z

hooked up clang-tidy

I'm very suspicious about it passing with default-uninitialized struct members, for instance

Amaury Chamayou (achamayou) · 2026-08-11T13:10:01Z

hooked up clang-tidy

I'm very suspicious about it passing with default-uninitialized struct members, for instance

https://github.com/microsoft/merklecpp/blob/main/.clang-tidy#L29
https://github.com/microsoft/merklecpp/blob/main/.clang-tidy#L36

Having said that, proof_viz.cpp is not checked because it is not built by CMake.

Co-authored-by: Copilot App <223556219+Copilot@users.noreply.github.com>

The visualization model reimplemented library internals: mark_inclusion mirrored the inclusion_proof descent, mark_consistency was a verbatim copy of the private subproof, and each node's source was inferred from the flush boundary rather than observed. Ask the tile and frontier sources separately instead of only through the CombinedHashSource that hides which one answered, so a node's source and the tile/frontier overlap are recorded rather than guessed, and cross-check that both stores agree where they overlap. Fetch proofs through the public API and find each element's node by its digest, which is exact for SHA-256, replacing both marking functions and the proof-size assertion that stood in for real correlation. Emit the node map as parallel columns with one flag bitmask per node, plus the proof as node ids in proof order and the full tiles that reached disk. The generated data.json drops from 822KB to 127KB. No library changes: shape, proof positions, endpoints, source labels and overlap all match the previous output exactly. Co-authored-by: Copilot App <223556219+Copilot@users.noreply.github.com> Copilot-Session: e274c92e-afa1-48a2-b9ac-ca3a1ace6b6c

A consistency proof reconciles two trees, but the atlas only ever drew the larger one. The smaller tree has a right spine of its own -- the ranges a verifier folds proof elements into to recover the first root -- and those ranges are absent from the larger tree unless its size is an aligned power of two. Three of the five consistency scenes were missing it, including the first root itself, so the picture never showed how one root reaches the other. It looked complete only where m was 128 or 256 and the spine coincided with real nodes. Merge both decompositions into one node map and record which trees each range belongs to. The split point depends only on the range, so a shared range has the same children in both trees and is stored once. Ranges that exist solely in the first tree are drawn as individual nodes, since they carry no edges in this map, and both roots are checked against past_root. Rank nodes by height above the leaves rather than depth below the root so that every leaf shares a baseline; the decomposition is unbalanced, and a ragged range reaches its leaves in fewer splits than a perfect one, which left subtrees floating. Drop the interior ranges that no store answers and no proof names: right-hand scaffolding that exists only because the tree size is not a power of two. Trim the scenario parser to the constraints the model depends on and check the strict file shape in make_viz.sh instead. Co-authored-by: Copilot App <223556219+Copilot@users.noreply.github.com> Copilot-Session: e274c92e-afa1-48a2-b9ac-ca3a1ace6b6c

Computed was a browsable category only while the ragged interior ranges were drawn. Every node that survives pruning and carries no store answer is now also a proof element or a root, so the swatch never stood on its own. Drop it and describe the ringed first-tree spine in the slot it frees; the colour stays for those few nodes and the tooltip still names them. The near-boundary takeaway described the assembling ranges that pruning removed. Say what the scene shows instead: seven resident ranges of doubling size and one tiled sibling, which is the proof it returns. Co-authored-by: Copilot App <223556219+Copilot@users.noreply.github.com> Copilot-Session: e274c92e-afa1-48a2-b9ac-ca3a1ace6b6c

Pruning the ranges no store answers took out the whole right spine of an unbalanced tree, and re-pointing their children at the nearest surviving ancestor collapsed that side onto the root: near-boundary drew nine edges into its root, one per proof element plus the target, in place of the fold that actually combines them. Those ranges are where the halves are joined, so they cannot be removed without losing the structure. Every leaf is answered by a store, or its digest could not be computed at all, so no subtree is ever empty of nodes worth drawing and the pruning could never have removed anything else. Drop it rather than keep a pass that provably does nothing. Draw a range that no store answers and no proof names smaller instead. It stays on the page as the join it is, without competing with the hashes someone actually holds. Co-authored-by: Copilot App <223556219+Copilot@users.noreply.github.com> Copilot-Session: e274c92e-afa1-48a2-b9ac-ca3a1ace6b6c

A consistency proof exists to turn one root into another, but neither root was marked, so the scene where the old tree is exactly the left subtree of the new one looked broken: SUBPROOF returns immediately there and the proof is a single hash, which read as missing nodes rather than as the degenerate case it is. Ring both roots and label them, so the one step that checks them, sha256 of the old root and that hash, is visible on the canvas. The takeaway for that scene described several frontier hashes and a recursion that does not happen when the old tree lands on the split point. Say what the proof is instead. Co-authored-by: Copilot App <223556219+Copilot@users.noreply.github.com> Copilot-Session: e274c92e-afa1-48a2-b9ac-ca3a1ace6b6c

Marking the two roots said what a consistency proof relates but not how. The proof elements that rebuild the old root are a subset of the ones that rebuild the new root, and which subset was nowhere on the page. Record each range's parent in the first tree as well as the second. The split point depends only on the range, so both trees give a range the same children, but they combine it with a different sibling wherever the trees disagree, and that difference is the fold. Draw the first tree's edge only where it differs, since elsewhere the edge is already there. In the crossing scene this draws six edges: four proof elements feeding three joins up to the old root, out of the eight elements the proof returns. Where the old size is an aligned power of two the old root is already a node of the new tree, nothing diverges, and no extra edge is drawn. Co-authored-by: Copilot App <223556219+Copilot@users.noreply.github.com> Copilot-Session: e274c92e-afa1-48a2-b9ac-ca3a1ace6b6c

The scenes called this leaf-to-leaf consistency and led with an earlier and a later leaf, which reads as a claim about those two leaves. It is not one: consistency_proof_from_indices(a, b) is consistency_proof(a + 1, b + 1), SUBPROOF takes only the two sizes, and neither selected leaf appears in any of the five proofs. Lead with the sizes instead, and say what the marked leaves are: where each tree ends, which is how the scenario file names a size. The A and B markers stay, since the boundary they draw is real. Co-authored-by: Copilot App <223556219+Copilot@users.noreply.github.com> Copilot-Session: e274c92e-afa1-48a2-b9ac-ca3a1ace6b6c

The map from range to node id is scratch space for building the two decompositions, not part of a scenario, so it lived past its use in every scenario that had already been written out. Pass it instead, and name the fields being set so a member added later cannot silently land in the wrong slot. Fold the old tree's edges into the tree edge toggle. They were drawn unconditionally, so turning edges off left them behind. Generated output is byte-identical. Co-authored-by: Copilot App <223556219+Copilot@users.noreply.github.com> Copilot-Session: e274c92e-afa1-48a2-b9ac-ca3a1ace6b6c

Amaury Chamayou (achamayou) and others added 14 commits July 25, 2026 21:39

Parallelize CI builds and release tests

96a6a31

Address proof generation review feedback

9d669bf

Use standard CMake parallelism variables

791ddb0

Adopt standard CMake test configuration

ebfa8d8

Address large-tree and proof review feedback

0d16668

Tighten proof roll-up and documentation

18355a2

Clarify subtree root result and effects

6a9e58a

Co-authored-by: eddyashton <6000239+eddyashton@users.noreply.github.com>

Consolidate proof subtree reduction

741fb70

Add proof source visualization atlas

42e3ca7

Visualize consistency between arbitrary leaves

8b87555

Simplify proof atlas scenario model

74c94e7

Publish proof visualization on GitHub Pages

f3560a1

Amaury Chamayou (achamayou) marked this pull request as ready for review August 6, 2026 20:52

Amaury Chamayou (achamayou) requested a review from a team as a code owner August 6, 2026 20:52

Amaury Chamayou (achamayou) added 5 commits August 7, 2026 13:12

Generate proof atlas in documentation CI

6b8e7d9

Use full viewport for proof atlas

b395e7d

Refine proof atlas data and styling

47030a4

Extract proof atlas scenarios

2a1640b

Format proof atlas generator

447d11b

Amaury Chamayou (achamayou) changed the base branch from achamayou/tiles-proofs to main August 7, 2026 14:50

Amaury Chamayou (achamayou) and others added 2 commits August 7, 2026 15:57

Merge branch 'main' into achamayou/proof-viz

80c2983

Simplify proof atlas presentation

d662622

Copilot AI lite review requested due to automatic review settings August 7, 2026 15:22

Copilot started reviewing on behalf of Amaury Chamayou (achamayou) August 7, 2026 15:23 View session

Copilot AI reviewed Aug 7, 2026

View reviewed changes

Comment thread tools/proof-viz/proof_viz.cpp

Comment thread tools/proof-viz/index.html Outdated

Comment thread tools/proof-viz/make_viz.sh Outdated

Apply suggestions from code review

6d30474

Co-authored-by: Copilot Autofix powered by AI <175728472+Copilot@users.noreply.github.com>

Max (maxtropets) reviewed Aug 11, 2026

View reviewed changes

Comment thread tools/proof-viz/make_viz.sh Outdated

Max (maxtropets) reviewed Aug 11, 2026

View reviewed changes

Comment thread tools/proof-viz/proof_viz.cpp Outdated

Max (maxtropets) reviewed Aug 11, 2026

View reviewed changes

Comment thread tools/proof-viz/.gitignore

Amaury Chamayou (achamayou) and others added 3 commits August 11, 2026 13:52

Simplify proof visualization build

8a59a74

Co-authored-by: Copilot App <223556219+Copilot@users.noreply.github.com>

Use native sizes in proof visualization

57dd249

Co-authored-by: Copilot App <223556219+Copilot@users.noreply.github.com>

Merge branch 'main' into achamayou/proof-viz

cd092b2

Amaury Chamayou (achamayou) and others added 9 commits August 11, 2026 15:33

Generate proof visualization model in C++

90e2172

Co-authored-by: Copilot App <223556219+Copilot@users.noreply.github.com>

Navigation Menu

Uh oh!

Add proof source visualization atlas - #67

Add proof source visualization atlas#67
Amaury Chamayou (achamayou) wants to merge 34 commits into
microsoft:mainfrom
achamayou:achamayou/proof-viz

Amaury Chamayou (achamayou) commented Aug 5, 2026 •

edited

Loading

Uh oh!

Copilot AI left a comment

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Max (maxtropets) commented Aug 11, 2026

Uh oh!

Amaury Chamayou (achamayou) commented Aug 11, 2026

Uh oh!

Max (maxtropets) commented Aug 11, 2026

Uh oh!

Amaury Chamayou (achamayou) commented Aug 11, 2026

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

4 participants

Uh oh!

Conversation

Amaury Chamayou (achamayou) commented Aug 5, 2026 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Summary

Base

How the model is built

Consistency proofs relate two sizes

Build and view

Validation

Uh oh!

Copilot AI left a comment

Choose a reason for hiding this comment

Pull request overview

Reviewed changes

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Max (maxtropets) commented Aug 11, 2026

Uh oh!

Amaury Chamayou (achamayou) commented Aug 11, 2026

Uh oh!

Max (maxtropets) commented Aug 11, 2026

Uh oh!

Amaury Chamayou (achamayou) commented Aug 11, 2026

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

4 participants

Amaury Chamayou (achamayou) commented Aug 5, 2026 •

edited

Loading