Add Verity syntax highlighting to docs

docs-site/app/layout.tsx

@@ -2,6 +2,7 @@ import { Layout, Navbar } from 'nextra-theme-docs'
 import { Head } from 'nextra/components'
 import { getPageMap } from 'nextra/page-map'
 import 'nextra-theme-docs/style.css'
+import './verity-code.css'
 
 export const metadata = {
   title: {

docs-site/app/verity-code.css

@@ -0,0 +1,41 @@
+figure[data-rehype-pretty-code-figure] pre[data-language="verity"] {
+  background:
+    linear-gradient(90deg, rgba(123, 63, 50, 0.06), transparent 22rem),
+    #fffaf1 !important;
+  border: 1px solid #eadcca;
+  box-shadow: 0 1px 0 rgba(255, 255, 255, 0.72) inset;
+}
+
+figure[data-rehype-pretty-code-figure] pre[data-language="verity"] code {
+  line-height: 1.62;
+}
+
+figure[data-rehype-pretty-code-figure] pre[data-language="verity"] code > span {
+  position: relative;
+}
+
+figure[data-rehype-pretty-code-figure] pre[data-language="verity"] code > span::before {
+  content: "";
+  position: absolute;
+  inset-block: 0;
+  left: 1.35rem;
+  border-left: 1px solid rgba(139, 118, 99, 0.13);
+  pointer-events: none;
+}
+
+figure[data-rehype-pretty-code-figure] pre[data-language="verity"] code > span:has(> span[style*="#7b3f32" i]:first-child),
+figure[data-rehype-pretty-code-figure] pre[data-language="verity"] code > span:has(> span[style*="#875c24" i]) {
+  background: linear-gradient(90deg, rgba(234, 220, 202, 0.7), rgba(234, 220, 202, 0));
+}
+
+figure[data-rehype-pretty-code-figure] pre[data-language="verity"] code > span:has(> span[style*="#a34537" i]) {
+  background: linear-gradient(90deg, rgba(163, 69, 55, 0.08), rgba(163, 69, 55, 0));
+}
+
+figure[data-rehype-pretty-code-figure] pre[data-language="verity"] code > span:has(> span[style*="#285f91" i]) {
+  background: linear-gradient(90deg, rgba(40, 95, 145, 0.07), rgba(40, 95, 145, 0));
+}
+
+figure[data-rehype-pretty-code-figure] pre[data-language="verity"] code > span:has(> span[style*="#3f7456" i]) {
+  background: linear-gradient(90deg, rgba(63, 116, 86, 0.08), rgba(63, 116, 86, 0));
+}

docs-site/content/compiler.mdx

@@ -55,7 +55,7 @@ Roadmap, milestones, and progress updates live in `docs-site/content/research.md
 ## Example: SimpleStorage
 
 ### EDSL Implementation
-```lean
+```verity
 -- Verity/Examples/SimpleStorage.lean
 def storedData : StorageSlot Uint256 := ⟨0⟩
 
@@ -67,7 +67,7 @@ def retrieve : Contract Uint256 := do
 ```
 
 ### Declarative Specification
-```lean
+```verity
 -- Compiler/Specs.lean
 def simpleStorageSpec : CompilationModel := {
   name := "SimpleStorage"
@@ -217,7 +217,7 @@ forge create SimpleStorage --from 0x... --private-key ...
 ## Features
 
 ### Automatic Storage Slot Inference ✅
-```lean
+```verity
 fields := [
   { name := "owner", ty := FieldType.address },     -- slot 0
   { name := "balances", ty := FieldType.mappingTyped (.simple .address) },  -- slot 1
@@ -228,7 +228,7 @@ fields := [
 No manual slot management needed. Compiler assigns slots based on field order.
 
 ### Constructor Parameters ✅
-```lean
+```verity
 constructor := some {
   params := [{ name := "initialOwner", ty := ParamType.address }]
   body := [
@@ -363,22 +363,22 @@ Members can carry packed bit metadata, so common `uint128`-style packed subfield
 | `internalCall "f" args` | Call internal function (statement) | `internal_f(args...)` |
 
 **Example**, combining multiple features:
-```lean
+```verity
 -- Balance check with require
 Stmt.require (Expr.ge (Expr.mapping "balances" Expr.caller) (Expr.param "amount")) "Insufficient",
 Stmt.setMapping "balances" Expr.caller
   (Expr.sub (Expr.mapping "balances" Expr.caller) (Expr.param "amount")),
 Stmt.stop
 ```
 
-```lean
+```verity
 -- If/else branching
 Stmt.ite (Expr.eq Expr.caller (Expr.storage "owner"))
   [Stmt.setStorage "paused" (Expr.literal 1), Stmt.stop]
   [Stmt.stop]  -- non-owner: no-op
 ```
 
-```lean
+```verity
 -- Bounded loop over array
 Stmt.forEach "i" (Expr.arrayLength "recipients")
   [Stmt.setMapping "balances" (Expr.arrayElement "recipients" (Expr.localVar "i"))
@@ -441,7 +441,7 @@ lake exe verity-compiler-patched --backend-profile solidity-parity
 
 Conditional logic for contract functions:
 
-```lean
+```verity
 -- Simple if (no else)
 Stmt.ite (Expr.eq Expr.caller (Expr.storage "owner"))
   [Stmt.setStorage "paused" (Expr.literal 1)]
@@ -468,7 +468,7 @@ Compiles to a block-scoped condition variable to avoid re-evaluation after state
 
 Iterate over array parameters or fixed counts:
 
-```lean
+```verity
 -- Iterate over a dynamic array
 Stmt.forEach "i" (Expr.arrayLength "recipients")
   [Stmt.setMapping "balances"
@@ -500,7 +500,7 @@ let (lhs, rhs) ← helperPair arg
 
 Those source forms lower to `Stmt.internalCall`, `Stmt.internalCallAssign`, or `Expr.internalCall` in the compilation model.
 
-```lean
+```verity
 def mySpec : CompilationModel := {
   name := "MyContract"
   fields := [{ name := "balances", ty := FieldType.mappingTyped (.simple .address) }]
@@ -531,7 +531,7 @@ def mySpec : CompilationModel := {
 ```
 
 Internal functions that return values use `__ret` assignment instead of EVM `RETURN`:
-```lean
+```verity
 -- Internal function returning a value
 { name := "getBalance"
   params := [{ name := "addr", ty := ParamType.address }]
@@ -548,7 +548,7 @@ Stmt.letVar "bal" (Expr.internalCall "getBalance" [Expr.caller])
 
 Emit EVM events for standards compliance (ERC20 Transfer/Approval, etc.):
 
-```lean
+```verity
 def tokenSpec : CompilationModel := {
   name := "Token"
   fields := [{ name := "balances", ty := FieldType.mappingTyped (.simple .address) }]
@@ -582,7 +582,7 @@ Event topic0 is computed from the event signature (e.g., `keccak256("Transfer(ad
 
 For ERC20 allowances and similar patterns requiring `mapping(address => mapping(address => uint256))`:
 
-```lean
+```verity
 fields := [
   { name := "allowances", ty := FieldType.mappingTyped (MappingType.nested .address .address) }
 ]
@@ -600,7 +600,7 @@ Storage layout: `keccak256(spender . keccak256(owner . slot))`; matches Solidity
 
 For mappings keyed by numeric values instead of addresses:
 
-```lean
+```verity
 fields := [
   { name := "data", ty := FieldType.mappingTyped (MappingType.simple .uint256) }
 ]
@@ -616,7 +616,7 @@ Stmt.setMappingUint "data" (Expr.param "tokenId") (Expr.param "value")
 
 Dynamic arrays, fixed arrays, and bytes parameters for batch operations:
 
-```lean
+```verity
 -- Dynamic array parameter
 { name := "recipients", ty := ParamType.array ParamType.address }
 
@@ -660,7 +660,7 @@ FOUNDRY_PROFILE=difftest forge test
 ### Add New Contract
 
 1. **Add a macro contract declaration** in `Contracts/<Name>/<Name>.lean`:
-```lean
+```verity
 verity_contract MyContract where
   storage
     value : Uint256 := slot 0
@@ -765,7 +765,7 @@ private def ownedContract : IRContract :=
 ```
 
 **After** (declarative spec):
-```lean
+```verity
 def ownedSpec : CompilationModel := {
   name := "Owned"
   fields := [

docs-site/content/core.mdx

@@ -9,7 +9,7 @@ The core is intentionally small. It provides types for contract state, storage o
 
 ## Types
 
-```lean
+```verity
 abbrev Address := String
 abbrev Uint256 := Verity.Core.Uint256
 
@@ -25,7 +25,7 @@ structure StorageSlot (α : Type) where
 
 ## ContractState
 
-```lean
+```verity
 structure ContractState where
   storage : Nat → Uint256                         -- Uint256 storage
   storageAddr : Nat → Address                      -- Address storage
@@ -64,7 +64,7 @@ abbrev Contract (α : Type) := ContractState → ContractResult α
 
 A contract is a function from state to result. The custom `bind` short-circuits on revert:
 
-```lean
+```verity
 def bind (ma : Contract α) (f : α → Contract β) : Contract β :=
   fun s => match ma s with
   | ContractResult.success a s' => f a s'
@@ -87,7 +87,7 @@ Five pairs of get/set functions, one per storage type:
 
 All follow the same pattern — read from or write to the corresponding `ContractState` field:
 
-```lean
+```verity
 def getStorage (s : StorageSlot Uint256) : Contract Uint256 :=
   fun state => ContractResult.success (state.storage s.slot) state
 
@@ -99,7 +99,7 @@ def setStorage (s : StorageSlot Uint256) (value : Uint256) : Contract Unit :=
 
 Mapping operations take key arguments:
 
-```lean
+```verity
 -- Address-keyed mapping (e.g., balances[owner])
 let bal ← getMapping balances owner
 setMapping balances owner newBal
@@ -119,7 +119,7 @@ setMapping2 allowances owner spender newAllow
 
 Read-only functions for accessing transaction context:
 
-```lean
+```verity
 let sender ← msgSender           -- Transaction sender address
 let self ← contractAddress        -- This contract's address
 let value ← msgValue             -- ETH value sent with call
@@ -130,15 +130,15 @@ These return values from `ContractState` without modifying state.
 
 ## Event emission
 
-```lean
+```verity
 emitEvent "Transfer" [amount] [senderBal, recipientBal]
 ```
 
 `emitEvent name args indexedArgs` appends to the `events` log. The `indexedArgs` parameter is optional (defaults to `[]`).
 
 ## Require guard
 
-```lean
+```verity
 def require (condition : Bool) (message : String) : Contract Unit :=
   fun s => if condition
            then ContractResult.success () s
@@ -151,7 +151,7 @@ Returns `success` when the condition holds, `revert` with the message when it do
 
 Every storage operation, context accessor, and event function has a full-result `@[simp]` lemma:
 
-```lean
+```verity
 -- Full-result form (preferred for new proofs):
 @[simp] theorem getStorage_run (s : StorageSlot Uint256) (state : ContractState) :
   (getStorage s).run state = ContractResult.success (state.storage s.slot) state := rfl
@@ -173,7 +173,7 @@ A plain `StateM ContractState α` monad cannot model `require` failures — proo
 
 The `StorageSlot α` type parameter prevents mixing storage types:
 
-```lean
+```verity
 def owner : StorageSlot Address := ⟨0⟩
 def count : StorageSlot Uint256 := ⟨1⟩
 def balances : StorageSlot (Address → Uint256) := ⟨2⟩