docs(site): IA restructure — Diátaxis sidebar, split pages, new explainers#1909
Merged
Conversation
…iners
A 12-point information-architecture pass on the docs:
1. Re-order content/_meta.js so the newcomer path is linear:
Home → Introduction (Architecture / Trust Model) →
Tutorials → How-To Guides → Reference → Explanation → Project.
2. Move add-contract.mdx into guides/ and demote it to the second
guide ("Add a Contract") — stops the duplicate top-level entry.
3. Adopt a four-bucket Diátaxis sidebar via _meta.js separators
(Introduction, Tutorials, How-To, Reference, Explanation,
Project) so each existing page maps onto an obvious role.
4. examples.mdx becomes a pure sample gallery — the "How to
organize a contract" + "Authoring checklist" sections are no
longer duplicated here; the canonical home is /guides/add-contract.
5. New trust-model.mdx (Layer 1/2/3, what's verified, what's
trusted). index.mdx / compiler.mdx / verification.mdx no longer
restate the model; they link.
6. Split compiler.mdx (837 L) into:
• /compiler — CLI reference, audit artifacts, validated set.
• /compiler-architecture — pipeline narrative, design
decisions, SimpleStorage walkthrough.
7. New faq.mdx — "Why Lean / why an EDSL / what's verified vs
trusted / how does Verity compare to Certora & Halmos & K /
production-ready? / Solidity story". Answers were scattered
across research.mdx and core.mdx.
8. New architecture.mdx — one screen, EDSL → CompilationModel →
IR → Yul → EVM with a paragraph each, placed before the heavy
core/compiler references.
9. Move guides/verity-syntax-highlighting.mdx → /syntax-highlighting
(top-level under "Project"); it's docs-site tooling, not a
contract-authoring guide.
10. New glossary.mdx with canonical one-paragraph definitions for
CompilationModel, ContractState, ContractResult, Layer 1/2/3,
local_obligations, linked_externals, trust report, assumption
inventory, layout report, ECM, EDSL, the spec/invariant/impl/
proof shape, and differential/property tests.
11. Tighten core.mdx ↔ edsl-api-reference.mdx boundary: core
describes types + monad only and points at the EDSL API
reference for the primitive catalogue.
12. Split verification.mdx:
• /verification — theorem inventory per contract.
• /proof-techniques — guard modeling, full-unfolding,
arithmetic semantics, known limitations (merged with
research.mdx techniques + limitations).
Sitemap, internal links (/guides/first-contract → /first-contract,
/add-contract → /guides/add-contract), and the hero CTA all updated.
next.config.mjs adds 301 redirects for the three moved URLs so old
bookmarks and external links don't 404.
|
The latest updates on your projects. Learn more about Vercel for GitHub.
|
Contributor
| \n### CI Failure Hints\n\nFailed jobs: `checks`\n\nCopy-paste local triage:\n```bash\nmake check\nlake build\nFOUNDRY_PROFILE=difftest forge test -vv\n``` |
added 2 commits
May 19, 2026 12:46
The /research and /research/iterations pages were old LLM-authored
project logs that no longer reflect current state. Removed:
• content/research.mdx
• content/research/iterations.mdx
• content/research/_meta.js (folder now empty)
• '/research' link in components/VerityHero.tsx → swapped to /faq
• '/research' entries in content/_meta.js and app/sitemap.ts
• outdated Research listing in public/llms.txt → replaced with full
new-IA link list (architecture, trust-model, proof-techniques,
glossary, faq, etc.)
Across the docs site, cut ~3,000 lines of redundant detail without losing material content. Goal: every page narrates one idea, then links out for inventories and code. Lean files and the trust report are the source of truth, not docs prose. Tier A (high-confidence removals, no information loss): - verification.mdx: 425 → 41. Replace per-contract theorem name tables (1,400+ lines of bullets reachable from `Contracts/.../Proofs/`) with one summary table per category. - first-contract.mdx: 698 → 214. Drop the 150-line Foundry test paste (the scaffold generator emits it), the duplicate API table (now lives in /edsl-api-reference), manual mkdir lines, redundant troubleshooting (handled by /guides/debugging-proofs), and prose phases collapse into the same workflow. - guides/debugging-proofs.mdx: 787 → 203. Remove emoji prefixes, decorative affirmations, performance/tracing sections (rare), the induction patterns section, and the Quick Decision Tree (already in the Quick Reference table). Keep concrete real-proof examples. - compiler.mdx + compiler-architecture.mdx → compiler.mdx (209): Merge into one page. Drop the manual-IR vs declarative "33% shorter" comparison (gone), the generated-IR/Yul/bytecode dumps for SimpleStorage (obvious from the inputs), and Backend Profiles prose (now a single-line bullet). - guides/linking-libraries.mdx: 346 → 110. Drop the TL;DR duplicate, internal linker stage breakdown, and CLI ref duplication. Tier B (compression of catalogue-style content): - edsl-api-reference.mdx: 882 → 355. Cut per-primitive "Proof lemmas" bullets (consolidated into one paragraph that points to the two Stdlib automation modules), collapse 13 ERC4626 helpers into one template + table, compress Tuple/Stateless/Constants/Immutables/ Linked Externals sections. - core.mdx: 199 → 146. Spec-helper tables become prose by tier (atomic/mixed/composite/fine-grained) keyed by what each setter writes. - proof-techniques.mdx: 122 → 101. Known-limitations bullets fold into one paragraph; the per-bullet expansions added nothing. - getting-started.mdx: 144 → 117. Drop "Explore a proof" detour and the scaffold-file table (printed by the generator). - faq.mdx: 103 → 90. Production-readiness section compressed; the contract enumeration was a verification.mdx duplicate. - examples.mdx: 223 → 205. Drop pattern-progression bullet list (the section headings already are the progression). Tier C (strategic moves): - C1: Delete syntax-highlighting.mdx (contributor reference, not user docs). The grammar/theme note moves to docs-site/README.md where it belongs. - C2: Merge compiler-architecture into compiler (above). - Both deletions wired up via permanent redirects in next.config.mjs. Other: - Update llms.txt (drop compiler-architecture entry), sitemap.ts (drop both deleted routes), _meta.js (drop both sidebar entries). - Replace stale Th0rgal/verity GitHub links with lfglabs-dev/verity. - Drop the docs/VERIFICATION_STATUS.md citation from /verification — the per-contract page is now self-contained. Build: 18 indexed pages (was 20), 1980 words. All routes resolve.
…tractState, missing primitives After a deeper read of the source, several pages were lagging behind the code: - examples.mdx: add Vault (minimal ERC-4626) and ERC721 entries. Both are real verified contracts in Contracts/ but had no docs page. - verification.mdx: rebuild the per-contract table from actual theorem counts in Contracts/<Name>/Proofs/*.lean. Add Native column (IR/Yul lowering theorems), add Vault row, and replace the hard-coded Stdlib numbers with an actually-counted table. - core.mdx: ContractState had drifted — actually six persistent storage spaces plus transient storage, plus storageArray, plus full EVM context (blockNumber, chainId, blobBaseFee, selfBalance, calldata, memory). Doc now matches Verity/Core.lean. - edsl-api-reference.mdx: add getMappingAddr/setMappingAddr, getMappingUintAddr/setMappingUintAddr (used in ERC721), pushStorageArray/popStorageArray, Contract.tryCatch, addressToWord/wordToAddress conversion helpers. - faq.mdx: add a single Q on AI agents writing Verity proofs, linking to Th0rgal/verity-benchmark (30 tasks across six real-world protocols). Build: 18 indexed pages, 2071 words.
- edsl-api-reference: add a single subsection pointing at the larger macro surface (modifiers, packed storage structs, ADTs, newtypes, storage_namespace erc7201, MappingStruct/MappingStruct2) and where to find concrete shapes — the production-solidity-patterns guide already covers usage; Verity/Macro/Syntax.lean is the grammar source of truth. - llms.txt: rewrite as a self-contained briefing for AI agents. Pipeline diagram, accurate ContractState description (six storage spaces + transient + EVM context), the _meets_spec pattern, deny-flag inventory, the verity-benchmark reference, a tighter doc index ordered by Diátaxis category, and a "working effectively in this codebase" section that orients agents toward Contracts/<Name>/ as the source of truth. Build: 18 pages, 2081 indexed words.
…, faq, glossary Three pages still claimed "five storage spaces" (the pre-storageArray shape). After confirming Verity/Core.lean has six persistent spaces (storage, storageAddr, storageMap, storageMapUint, storageMap2, storageArray) plus transient storage, update: - architecture.mdx: source-layer description - faq.mdx: "why an EDSL" answer - glossary.mdx: ContractState entry (also adds the missing EVM context fields — selfBalance, blockNumber, chainId, blobBaseFee, calldata, memory — that the page omitted) Build: 18 pages.
The benchmark repo moved from Th0rgal/ to lfglabs-dev/ (Th0rgal still 301-redirects). Use the canonical URL in faq.mdx and llms.txt to keep agents on the live owner.
The ERC20 transfer walkthrough was teaching agents broken patterns. The EDSL has no whole-mapping read or function-shaped write — you use getMapping/setMapping per key, not getStorage on a mapping slot. The spec example also used a record-style ContractSpec that doesn't exist; real specs are Prop-valued predicates over (s s' : ContractState) named <op>_spec. Fixes: - Direct-mappings table: balances[a] → getMapping balances a, plus rows for getMapping2 (allowances), getMappingUintAddr (token owners), and the correct emitEvent shape with separated data/indexed lists. - Step B (function body): rewrite using msgSender / getMapping / setMapping / requireSomeUint / emitEvent matching what Contracts/SimpleToken actually does. - Step C (spec shape): replace fictional ContractSpec record with the real <op>_spec : s → s' → Prop convention and a concrete storageMapUnchangedExceptKeysAtSlot + sameStorageAddrContext shape. - Step D (proof): replace generic prose with a real _meets_spec theorem and a single-simp shape, plus working source links. - Update repo paths: Verity/Proofs/<Name>/Basic.lean was the old layout; current code lives in Contracts/<Name>/Proofs/Basic.lean. Build: 18 pages.
Three guides were missing description frontmatter (or any frontmatter at all), which makes their sidebar tooltips and OpenGraph cards unhelpful: solidity-to-verity, production-solidity-patterns, add-contract. All four guides plus the two reference guides now have title + description. Also fix the See-also list at the bottom of solidity-to-verity: "Compiler" → "Compiler & CLI", "Formal Verification" → "Verification Status" to match the current sidebar labels. Build: 18 pages, 2090 indexed words.
The section was '## Spec helpers (`Verity/Specs/Common.lean`)', which Nextra slugified to #spec-helpers-verityspecscommonlean. Internal links in first-contract.mdx and solidity-to-verity.mdx that pointed at /core#spec-helpers were silently broken. Move the file path mention into the body and rename the header to '## Spec helpers', so the anchor becomes the obvious #spec-helpers.
…o Contracts/CryptoHash/
The first five examples (SimpleStorage, Counter, SafeCounter, Owned, OwnedCounter) were written in the old \`def x : Contract Unit := do\` style, which still compiles but is no longer the canonical authoring surface. Update them to the verity_contract macro syntax that actually lives in Contracts/<Name>/<Name>.lean today. Owned also picks up its constructor and transferOwnership entrypoints — the old snippet only showed the helper. Build: 18 pages, 2092 indexed words.
…act syntax Same modernization as the earlier 5 examples: drop the old def...Contract Unit := do style in favor of the verity_contract macro that lives in Contracts/<Name>/ today. SimpleToken also picks up its constructor — the old snippet started mid-function. Build: 18 pages.
AXIOMS.md says 'None. Verity has zero project-level Lean axioms.'
after solidityMappingSlot_lt_evmModulus was eliminated by replacing
the FFI keccak256 with a kernel-computable engine. The trust-model
page was still describing 'a short list including the residual
keccak256 primitive and a small number of EVM-side primitives' as
Lean axioms — that conflates the axiom registry with ECM/trust-report
assumptions.
Rewrite the 'Axioms and assumptions' section to:
1. State the zero-axiom fact and explain how the last one was eliminated.
2. Clarify what *does* remain outside the proof envelope: ECM
assumption names (erc20_balanceOf_interface etc.), local_obligations
metadata, and 'not modeled' feature flags. These show up in the
trust report, not in AXIOMS.md.
3. List the deny-flags that let a build fail closed on each category.
Also fix the matching bullet in 'What is trusted' to point at the
real category (ECM assumptions in --trust-report) instead of axioms.
Build: 18 pages, 2099 indexed words.
The trust-model edit clarified that AXIOMS.md lists zero active project-level Lean axioms — the residual keccak/mapping-slot axiom was eliminated by the kernel-computable Keccak engine. faq.mdx and llms.txt still said 'axioms in AXIOMS.md' as if there were some; update both to state the zero-axiom fact and route the remaining trust to ECM interface assumptions surfaced by --trust-report. Build: 18 pages.
After grepping Compiler/MainDriver.lean for the actual flag handlers,
four flags I'd documented were correct but four more existed that
the docs didn't mention:
Already there: axiomatized-primitives, local-obligations,
linear-memory-mechanics, event-emission,
proxy-upgradeability, layout-incompatibility
Newly added: unchecked-dependencies, assumed-dependencies,
low-level-mechanics, runtime-introspection
Rewrite compiler.mdx's deny-flag list as a 10-row table mapping each
flag to what it actually fails closed on, and update llms.txt with
the full list so agents see the complete surface.
Build: 18 pages.
MainDriver.lean exposes --deny-unsafe alongside the per-category flags. It's the catch-all that trips on any of the documented categories at once — useful for ship-blocking gates.
![cursor[bot]](https://avatars.githubusercontent.com/in/1210556?s=60&v=4){kind=small}
There was a problem hiding this comment.
Cursor Bugbot has reviewed your changes and found 2 potential issues.
❌ Bugbot Autofix is OFF. To automatically fix reported issues with cloud agents, enable autofix in the Cursor dashboard.
Reviewed by Cursor Bugbot for commit 012bd52. Configure here.
The aggressive prune removed verbatim phrases that boundary-sync
scripts enforce across docs pages. make check failed on five of
them; this restores the phrases while keeping the prose tight and
updates two sync scripts whose paths went stale.
CI-enforced phrases restored:
Layer 2 boundary (check_layer2_boundary_sync.py)
- compiler.mdx: "Layer 2 boundary today" callout with the
generic whole-contract theorem, eliminated body-simulation
axiom, and dispatcher-bridge-as-hypothesis statements.
- index.mdx: Compiler/Proofs/IRGeneration/Contract.lean
reference in the trust callout.
- examples.mdx: same theorem reference in the intro.
- first-contract.mdx: the compiler-level CompilationModel→IR
result lives in IRGeneration/Contract.lean.
- verification.mdx: rename row to "Generic whole-contract
Layer 2 theorem".
- llms.txt: "Generic whole-contract theorem for the supported
fragment. 0 axioms."
Low-level call boundary (check_low_level_call_boundary_sync.py)
- edsl-api-reference.mdx + compiler.mdx: trust-boundary notes
for call/staticcall/delegatecall plus the proxy-upgradeability
callout for delegatecall.
Linear-memory boundary (check_linear_memory_boundary_sync.py)
- edsl-api-reference.mdx + compiler.mdx: linear-memory
partial-modeling note with --deny-linear-memory-mechanics.
Axiomatized-primitive boundary (check_axiomatized_primitive_boundary_sync.py)
- edsl-api-reference.mdx + compiler.mdx: keccak256 still
axiomatized note with --deny-axiomatized-primitives.
Struct-mapping surface (check_struct_mapping_surface_sync.py)
- compiler.mdx: structMember / setStructMember docs for
Morpho-style mapping(K => Struct) layouts.
Sync scripts updated for new IA:
- check_layer2_boundary_sync.py: move
DOCS_SITE_FIRST_CONTRACT from guides/first-contract.mdx to
first-contract.mdx (top-level after IA restructure); drop
DOCS_SITE_RESEARCH entirely (page deleted in the prune).
- check_struct_mapping_surface_sync.py: move ADD_CONTRACT path
to guides/add-contract.mdx.
make check now passes; docs build still green at 18 pages.
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
1 participant
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
Summary
A 12-point information-architecture pass on the docs. All 12 items from the audit are addressed in this single PR.
🚀 Live preview: built by Vercel from this branch.
What changes
1. Sidebar re-organised into Diátaxis groups (
_meta.jsonly)2. URL changes + redirects
/guides/first-contract/first-contract/add-contract/guides/add-contract/guides/verity-syntax-highlighting/syntax-highlightingAll three get HTTP 301 redirects via
next.config.mjs#redirects()so old bookmarks / external links don't 404.3. New pages (6)
architecture.mdx— one-screen map of EDSL → CompilationModel → IR → Yul → EVM.trust-model.mdx— Layer 1/2/3 framing, what's verified, what's trusted (the single canonical home;index.mdx/compiler.mdx/verification.mdxnow link instead of restating).compiler-architecture.mdx— pipeline narrative, design decisions, SimpleStorage walkthrough (split fromcompiler.mdx).proof-techniques.mdx— guard modeling, full-unfolding, arithmetic semantics, known limitations (split fromverification.mdx+ merged withresearch.mdx).faq.mdx— "Why Lean / why an EDSL / what's verified vs trusted / how does Verity compare to Certora & Halmos & K / production-ready? / Solidity story".glossary.mdx— canonical definitions for CompilationModel, ContractState, ContractResult, Layer 1/2/3, local_obligations, linked_externals, trust report, assumption inventory, layout report, ECM, etc.4. Slimmed pages
compiler.mdx: 837 L → ~100 L. Now: CLI usage, audit flags, validated contracts. Architecture/walkthrough lives in/compiler-architecture.verification.mdx: theorem inventory only. "Guard modeling", "Proof techniques", "Known limitations" moved to/proof-techniques.research.mdx: research log (evolution, iterations, design decisions, compiler-development milestones). Proof Techniques / Arithmetic Semantics / Known Limitations moved to/proof-techniques.examples.mdx: pure sample gallery. "How to organize a contract" / "Authoring checklist" content lives in/guides/add-contract.core.mdx: types + monad only. Storage / context / require primitives delegated to/edsl-api-reference.index.mdx: "Where the trust comes from" callout now links to/trust-modelinstead of restating it. ReadingList re-ordered for the new IA.Test plan
/,/architecture,/trust-model,/getting-started,/first-contract,/guides/add-contract,/examples,/core,/edsl-api-reference,/compiler,/verification,/glossary,/compiler-architecture,/proof-techniques,/research,/faq,/syntax-highlighting,/research/iterations)././guides/first-contract→/first-contract,/add-contract→/guides/add-contractin MDX prose, the hero CTA,public/llms.txt).next.config.mjs301 redirects in place for legacy URLs.app/sitemap.tswith the full new route set.Scope
Pure content +
_meta.js+next.config.mjs+sitemap.ts. No theme/CSS changes, no shiki theme changes, no component changes (besides theVerityHero.tsxhref update).Note
Low Risk
Low risk because changes are confined to documentation content, navigation metadata, and routing redirects/sitemap. Main risk is broken internal links or missing redirects causing 404s.
Overview
Docs IA overhaul. Reorganizes
content/_meta.jsinto Diátaxis-style sections (Introduction/Tutorials/How-To/Reference/Explanation), updates the homepage hero CTA, and refreshesapp/sitemap.tsto reflect the new route set.New/rewritten docs pages. Adds new pages including
architecture.mdx,first-contract.mdx,faq.mdx, andglossary.mdx, and significantly rewrites/slims key reference pages (compiler.mdx,core.mdx,edsl-api-reference.mdx,examples.mdx,guides/debugging-proofs.mdx) to match the new structure and cross-linking.Routing/link hygiene. Adds/updates legacy URL redirects in
next.config.mjs, updates various internal links (including repo URLs), and tweaks the docs API route comment/examples to match current pages.Reviewed by Cursor Bugbot for commit 1d86cd4. Bugbot is set up for automated code reviews on this repo. Configure here.