fix: correct stale docs, wrong test commands, and inaccurate API surface

[Th0rgal]

Summary

Fixes multiple documentation inaccuracies that would cause developers to fail when following the guides:

• core.mdx: ContractState struct was missing 4 fields (storageMapUint, storageMap2, knownAddresses, events) and the storage operations table was incomplete (missing getMappingUint/setMappingUint, getMapping2/setMapping2, emitEvent, and context accessors)
• compiler.mdx: allSpecs was shown as List (ContractSpec × List Nat) (tuple with manual selectors) but the actual code is List ContractSpec — selectors are computed automatically by computeSelectors
• getting-started.mdx: Incorrectly claimed forge test works for property tests without FOUNDRY_PROFILE=difftest. All property tests use deployYul() → vm.ffi() → solc, which requires FFI enabled
• first-contract.mdx: Test commands missing FOUNDRY_PROFILE=difftest, which would fail on first use
• examples.mdx: File layout section was stale (missing Proofs/<Name>/Basic.lean and Correctness.lean); ReentrancyExample code had unbalanced parenthesis
• test/README.md: Claimed forge test runs "unit + property tests" but property tests require FFI; fixed all commands to include FOUNDRY_PROFILE=difftest

Verification

Each fix was verified against the actual codebase:

• ContractState fields checked against Verity/Core.lean:37-48
• allSpecs type checked against Compiler/Specs.lean:453
• All Property*.t.sol files confirmed to import YulTestBase (which uses vm.ffi)
• foundry.toml confirms ffi = false in default profile, ffi = true in difftest

Test plan

• Docs site builds successfully
• No Lean code was modified — existing proofs and CI unaffected
• Verify the docs site renders correctly at verity.thomasm.ar

🤖 Generated with Claude Code

---

Note

Low Risk
Docs-only changes that correct API descriptions and required Foundry commands; no runtime or proof logic is modified.

Overview
Updates documentation to match the current codebase and prevent broken setup steps. The compiler docs now show allSpecs : List ContractSpec and clarify that function selectors are computed automatically during compilation.

Core docs are corrected to include the full ContractState surface (additional mapping types, address tracking, and event log) and to document the missing storage/event operations. Guides and test docs are updated to consistently run Foundry with FOUNDRY_PROFILE=difftest (and explain the vm.ffi() requirement), and examples.mdx is refreshed for the new proofs layout plus a small syntax fix in the ReentrancyExample snippet.

^{Written by Cursor Bugbot for commit c66405b. 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 4:28pm

[Th0rgal]

Closing — all changes in this PR have been merged via later PRs:

• compiler.mdx allSpecs fix → merged in fix: stale docs, wrong allSpecs example, and CI sorry filter #279
• core.mdx ContractState fields → merged in fix: docs accuracy — broken paths, missing fields, wrong counts #280
• getting-started.mdx difftest fix → merged in fix: repro command missing difftest profile + docs friction points #277
• first-contract.mdx difftest fix → merged in fix: repro command missing difftest profile + docs friction points #277
• examples.mdx file layout fix → included in rebased fix: make SpecInterpreter stubs fail-safe and add fuel-based API #276
• test/README.md test commands → included in rebased fix: make SpecInterpreter stubs fail-safe and add fuel-based API #276