fix: docs accuracy — broken paths, missing fields, wrong counts

[Th0rgal]

Summary

• Fix linking-libraries.mdx: all examples used non-existent libs/ directory — a developer following the Quick Start would fail at step 1
• Fix core.mdx: ContractState shown with 7 fields but actual has 11 — missing storageMapUint, storageMap2, knownAddresses, events
• Fix verification.mdx: Stdlib count was 64 but manifest has 69 — MappingAutomation.lean (7 theorems) was added but never reflected in docs
• Fix add-contract.mdx: scaffold count said "6 files" but creates 7; proof path pointed to re-export shim instead of actual proof directory

Details

linking-libraries.mdx (highest impact)

Every command in the TL;DR, Quick Start, Debugging, and CLI Reference sections used paths like libs/MyHash.yul or libs/Poseidon.yul. This directory does not exist in the repo. The actual convention is examples/external-libs/ (where PoseidonT3.yul and PoseidonT4.yul live). Changed all occurrences to use the real path, including adding mkdir -p examples/external-libs in the TL;DR.

core.mdx

The ContractState struct was shown with 7 fields but the actual Core.lean (lines 37-48) has 11 fields. The 4 missing fields are critical for understanding the EDSL:

• storageMapUint — uint256-keyed mappings
• storageMap2 — double mappings (e.g., allowances[owner][spender])
• knownAddresses — tracked address sets for conservation proofs
• events — append-only event log

verification.mdx

The Stdlib section said "64 theorems (Math 25, Automation 39)" but the manifest has 69 Stdlib entries. The 5 additional theorems come from MappingAutomation.lean which was added after the docs were written. Updated to "69 theorems (Math 25, Automation 39, MappingAutomation 7; 2 shared)".

add-contract.mdx

• "6 scaffold files" → "7 scaffold files" (the Verity/Specs/<Name>/Proofs.lean re-export shim was omitted from the count)
• Step 3 said "Prove correctness in Verity/Specs/<Name>/Proofs.lean" — that file is a re-export shim, not where you write proofs. Fixed to point to Verity/Proofs/<Name>/Basic.lean and Correctness.lean

Test plan

• check_doc_counts.py passes locally
• Docs site builds (Vercel preview)
• CI passes (no Lean/Solidity changes)

🤖 Generated with Claude Code

---

Note

Low Risk
Documentation-only changes correcting file counts, paths, and type/state descriptions; low risk aside from potentially breaking reader workflows if any path was still wrong.

Overview
Fixes several docs inconsistencies so tutorials match the repo:

Updates add-contract.mdx to reflect 7 generated scaffold files and clarifies that Verity/Specs/<Name>/Proofs.lean is a re-export shim, with proofs written under Verity/Proofs/<Name>/.

Corrects core.mdx’s ContractState definition to include the missing storage mapping variants plus knownAddresses and events, and updates the surrounding explanation accordingly. The linking guide switches all examples from the non-existent libs/ directory to examples/external-libs/ (including adding mkdir -p), and verification.mdx updates the Stdlib theorem count to include MappingAutomation.

^{Written by Cursor Bugbot for commit ed7dcb6. This will update automatically on new commits. Configure here.}

[vercel]

The latest updates on your projects. Learn more about Vercel for GitHub.

Project	Deployment	Actions	Updated (UTC)
dumbcontracts	Ready	Preview, Comment	Feb 17, 2026 5:25pm