Add Verity syntax highlighting to docs

[Th0rgal]

Summary

• tighten the Verity TextMate grammar around actual Verity DSL scopes: contract sections, typed externals, reusable modifiers, with modifier clauses, nonreentrant(...), effectful calls, ABI projections, field access, event names, and custom errors
• add the LFGLabs Cream Shiki theme so Verity docs use a warm light code palette with semantic colors instead of generic Lean/GitHub highlighting
• add subtle Verity-only code-block styling for declaration, guard, external-call, and event lines
• add a dedicated docs page with the syntax-highlighting definition of done and an Unlink-style preview snippet
• strengthen npm run check:highlighting with an Unlink-shaped sample and 25 required Verity-specific scopes

Definition of Done

• Verity snippets are rendered with verity, not generic lean, when they show contract DSL code
• contract structure is visually explicit: verity_contract, section headers, linked_externals, typed external declarations, modifier, and function headers each receive distinct scopes
• Solidity-like control surfaces are easy to scan: with onlyRelayer, nonreentrant(...), forEach, requireError, tryExternalCall, abiEncode, and emit are all highlighted by semantic role
• domain-level signals stand out without changing source text: field access such as txn.proof, typed external returns such as Circuit, event names, and custom errors such as PoolCircuitNotRegistered() receive dedicated scopes
• code blocks use a warm light theme with subtle scope bands for guards, external calls, events, and declaration lines
• the scope contract is checked by npm run check:highlighting

Validation

• npm run check:highlighting
• npm run build
• rendered /guides/verity-syntax-highlighting locally with next start and captured a screenshot to inspect the actual code-block rendering

Notes

• This is docs/reporting tooling only. It does not touch Verity compiler, macro, proof, or trusted runtime semantics.
• The docs build uses next build --webpack because Next 16 Turbopack requires serializable MDX loader options, while custom Shiki highlighter hooks are functions.

[cursor]

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 c88dfcb. Configure here.}

[cursor]

Dead ternary produces identical empty arrays both branches

Low Severity

The expression ...((options.themes ?? options.theme) ? [] : []) is a no-op since both the truthy and falsy branches evaluate to []. The ternary always spreads an empty array regardless of whether options.themes or options.theme exist. This looks like either an incomplete implementation (perhaps meant to forward options.themes) or leftover logic that was never cleaned up.

 

^{Reviewed by Cursor Bugbot for commit c88dfcb. Configure here.}

[cursor]

Grammar match pattern shadows begin/end block pattern

Low Severity

The simple match pattern on line 130 includes linked_externals in its alternation, so it always matches that keyword first. This prevents the begin/end block pattern on line 134 from ever activating. The block was designed to scope the entire linked_externals section with specialized inner patterns and the theme color #53616a, but it's dead code because TextMate grammars try patterns in array order and stop at the first match.

Additional Locations (1)

• docs-site/syntaxes/verity.tmLanguage.json#L133-L172

 

^{Reviewed by Cursor Bugbot for commit c88dfcb. Configure here.}