Gate the facts docs/index.html and docs/index.md both state

CHANGELOG.md

@@ -6,6 +6,12 @@ The format is based on [Keep a Changelog](https://keepachangelog.com/en/1.1.0/).
 
 ## [Unreleased]
 
+### Fixed
+
+- **`scripts/check_site_assets.py` gates the facts `docs/index.html` and `docs/index.md` both state** ([#1154](https://github.com/aallan/vera/issues/1154)). The Markdown companion agents fetch via `rel="alternate"` and `llms.txt` is emitted by `build_index_md()` in `scripts/build_site.py`, which holds the landing page's substance as a hand-maintained f-string. The staleness check called that generator and compared the result against the committed file — the generator on both sides of the comparison — so a generator that missed an edit to the hand-designed HTML produced a committed asset stale in exactly the same way, and the gate passed. A v0.0.7-era benchmark section survived every intervening release that way.
+
+  `check_fact_coherence()` now extracts the load-bearing facts from each file independently and fails when they diverge: the VeraBench version and the Vera release it was measured against, the landing-page version badge, the problem/tier/model/provider counts, the headline perfect-Vera count, the nine-row results table (model name, tier and all three figures per row, plus each file's row count against its own stated model count), and the three editor names. An error names the fact, both values and both paths. A fact that cannot be located is itself a failure rather than a silent skip, so a reworded sentence cannot switch its own check off.
+
 ### Documentation
 
 - **The VeraBench section carries the v0.0.18 sweep** ([#1169](https://github.com/aallan/vera/pull/1169)), the first in which all 60 problems are graded — v0.0.17 took the gradeable set from 36 to 46 and v0.0.18 closed it. One problem is now worth 1.7 percentage points rather than 2.8. Six of the nine models solve every Vera problem, and Vera is highest or level with it for six of the nine. Measured against [Vera v0.1.8](https://github.com/aallan/vera/releases/tag/v0.1.8). The section also gains the reading the wider gradeable set supports: Python is dynamically typed and TypeScript is not, Vera sits with TypeScript and goes further, and sorting the three by how much they constrain the model rather than by how much of them it has read puts the two constraining languages ahead — TypeScript with training data behind it, Vera without.

CLAUDE.md

@@ -73,7 +73,7 @@ python scripts/check_doc_builtin_shadowing.py # Verify no doc example redefines
 python scripts/check_diagnostic_fields.py # Verify every diagnostic carries rationale + spec_ref (+ fix for errors; warnings exempt) or a # diag-fields-exempt reason — waives missing/unresolvable fields only, never a factually wrong spec_ref/error_code (#682)
 python scripts/check_explicit_encoding.py # Verify every text-mode open()/read_text()/write_text() passes explicit encoding='utf-8' (#645)
 python scripts/build_site.py          # Regenerate AI-readable site assets (llms.txt, etc.)
-python scripts/check_site_assets.py   # Verify site assets are up-to-date
+python scripts/check_site_assets.py   # Verify site assets are up-to-date + docs/index.html ↔ docs/index.md state coherent facts (#1154)
 python scripts/check_version_sync.py  # Verify version consistency
 python scripts/check_doc_counts.py    # Verify documentation counts match codebase
 python scripts/check_licenses.py      # Verify all package licenses are MIT-compatible

CONTRIBUTING.md

@@ -112,6 +112,8 @@ The **commit-stage** hooks (30, each gated to relevant files) include:
 
 If you modify documentation sources (SKILL.md, AGENTS.md, FAQ.md, `vera/errors.py`, `vera/grammar.lark`, or `docs/index.html`), the `site-assets` hook will regenerate `docs/` files via `scripts/build_site.py`. The CI also runs `scripts/check_site_assets.py` to verify freshness.
 
+`docs/index.md` is a special case: it is not derived from `docs/index.html` but written out by `build_index_md()` in `scripts/build_site.py`, so an edit to the landing page's substance has to be made in both places. `check_site_assets.py` compares the load-bearing facts across the pair — benchmark version strings, problem and model counts, the results table, the editor names — and fails when they diverge or when one of them can no longer be located.
+
 ### Pre-push hook: CHANGELOG enforcement
 
 A separate `pre-push` hook runs once before each `git push` (not per-commit — which would be too noisy on feature branches). It verifies that any PR touching a non-exempt top-level path adds a new entry to `CHANGELOG.md`. The same check also runs in CI, so pushes without the local hook installed are still caught before merge.

KNOWN_ISSUES.md

@@ -11,7 +11,6 @@ Defects in shipped compiler, runtime, or tooling behaviour — this table matche
 | Cross-module type-alias namespaces merge flatly in codegen (`setdefault` on bare name, first module wins), so two imported modules defining the same alias name with different targets corrupt one module's function signatures — check-clean (the checker is module-correct), then an invalid WASM module or wrong values at run time. The fix preserves per-module alias maps keyed by module path; the workaround is unique alias names across a program's module graph. | [#1111](https://github.com/aallan/vera/issues/1111) |
 | A codegen `[E602]` skip drops the function from the emitted module but leaves its callers' `call`/`return_call` in place, so a check- and verify-clean program whose skipped construct sits in a *called helper* fails at `run`/`compile` with a raw wasmtime `unknown func` error instead of a source-located diagnostic. Loud, not silent (never a wrong answer); the fix propagates the skip to callers or diagnoses the dropped callee at the call site. | [#1100](https://github.com/aallan/vera/issues/1100) |
 | `ch05_closure_nat_return` (a run-level conformance program in the pre-commit + CI gate) trapped **once** in a full `check_conformance.py` run (`unreachable` in `main` — the sentinel `assert` or a GC shadow-stack guard) and has not reproduced in ~960 attempts across isolated, parallel, eager-GC, and hash-seed-swept executions; the emitted WAT is deterministic and correct. Suspected rare runtime/GC/wasmtime interaction, tracked so a future intermittent CI red resolves here instead of starting fresh. | [#996](https://github.com/aallan/vera/issues/996) |
-| `docs/index.md` — the Markdown companion agents fetch via `rel="alternate"` instead of the landing page — is generated by `build_index_md()` in `scripts/build_site.py`, which mirrors `docs/index.html`'s substance as hand-maintained prose rather than deriving it. An edit to the HTML does not propagate, and `check_site_assets.py` cannot detect the drift: it regenerates from that same function and compares against the committed file, so a stale generator and a stale asset agree and the gate passes. Silent and unbounded — a v0.0.7-era benchmark section survived every intervening release until it was caught by hand. Fix options: derive the Markdown from the HTML, gate the load-bearing facts across the pair, or extract the shared substance to a data file both read. | [#1154](https://github.com/aallan/vera/issues/1154) |
 | A user `effect <BuiltinName> { … }` block overriding a built-in host effect (`IO` / `DB` / `Http` / …) — which spec §9.5.1 explicitly permits "for backward compatibility" — with an operation signature that diverges from the built-in passes **both `vera check` and `vera compile`** (exit 0, no diagnostic), yet emits structurally invalid WASM that traps at `run`. The override is checker-level only (§9.5.1 makes only the declared ops available); codegen ignores it and routes a qualified `Effect.op(...)` to the fixed-arity host import, so a divergent signature mismatches. Loud (a wasmtime validator error, never a wrong answer), reachable by an ordinary typo in the (optional-but-idiomatic) declaration; pre-existing and general, orthogonal to the #309 SQL-provenance gate. Fix: either validate an override's op signatures against the host ABI (reject divergence, keeping §9.5.1), or amend §9.5.1 to forbid the block outright (an E151-analogue, per design goal 3 — also closing the #309 shadow surface). | [#1149](https://github.com/aallan/vera/issues/1149) |
 
 ## Limitations

README.md

@@ -263,7 +263,7 @@ cp /path/to/vera/SKILL.md ~/.claude/skills/vera-language/SKILL.md
 
 ## Project status
 
-Vera is in **active development** at v0.1.8: 2,000+ commits, 204 releases, 8,568 tests, 95% code coverage, 169 conformance programs, 42 examples, and a 14-chapter specification. Known bugs and limitations are tracked in **[KNOWN_ISSUES.md](KNOWN_ISSUES.md)**. See **[HISTORY.md](HISTORY.md)** for how the compiler was built.
+Vera is in **active development** at v0.1.8: 2,000+ commits, 204 releases, 8,589 tests, 95% code coverage, 169 conformance programs, 42 examples, and a 14-chapter specification. Known bugs and limitations are tracked in **[KNOWN_ISSUES.md](KNOWN_ISSUES.md)**. See **[HISTORY.md](HISTORY.md)** for how the compiler was built.
 
 The reference compiler — parser, AST, type checker, contract verifier (Z3), WASM code generator, module system, browser runtime, and runtime contract insertion — is working. The language specification is in draft across [14 chapters](spec/).
 

ROADMAP.md

@@ -12,7 +12,7 @@ Ordering derives from the design principles ([DESIGN.md](DESIGN.md)): verificati
 
 ## Where we are
 
-8,568 tests, 169 conformance programs, 42 examples, 14 spec chapters.  [KNOWN_ISSUES.md](KNOWN_ISSUES.md) tracks the open bugs — burndown material rather than stage work — plus the *limitations* the stages below retire.
+8,589 tests, 169 conformance programs, 42 examples, 14 spec chapters.  [KNOWN_ISSUES.md](KNOWN_ISSUES.md) tracks the open bugs — burndown material rather than stage work — plus the *limitations* the stages below retire.
 
 ## Stage 19 — The verification completeness sprint
 

TESTING.md

@@ -6,7 +6,7 @@ This is the single source of truth for Vera's testing infrastructure, coverage d
 
 | Metric | Value |
 |--------|-------|
-| **Tests** | 8,568 across 131 files (~106,000 lines of test code; 8,452 passed + 26 stress, 90 skipped) |
+| **Tests** | 8,589 across 131 files (~106,000 lines of test code; 8,473 passed + 26 stress, 90 skipped) |
 | **Compiler code coverage** | 95% Python, 61% JavaScript — 91% combined (CI minimum: 80%) |
 | **Conformance programs** | 169 programs across 9 spec chapters, validating every language feature |
 | **Example programs** | 42, all validated through `vera check` + `vera verify` |
@@ -174,7 +174,7 @@ python scripts/check_wheel_availability.py           # pre-flight: every runtime
 | `test_html.py` | 4 | 167 | HTML landing page code samples: parse, check, verify (vera:skip-annotation aware, #538) |
 | `test_float64_fp.py` | 10 | 260 | #797 — `@Float64` contracts via Z3's IEEE-754 FloatingPoint sort: unsound relational / reflexive contracts (rounding at 2^53, `NaN`, `Inf`) flip from proved to violated/Tier-3, NaN-guarded contracts still verify at Tier 1, `==`/`!=` use IEEE `fpEQ`/`fpNEQ` (incl. `+0.0 == -0.0`), `%` matches codegen truncated remainder (not `fp.rem`; NaN-by-zero + large-magnitude edges), and `float_is_nan` / `float_is_infinite` / `nan()` / `infinity()` translate to FP predicates / constants. Also guards mixed `@Float64`/`@Int` ordering as a clean E142 (not a Z3 crash) |
 | `test_float64_builtins_807.py` | 81 | 491 | #807 — Tier-1 modeling of the modelable `@Float64` builtins. `float_clamp` modeled unconditionally as faithful WASM `f64.min(f64.max(v,lo),hi)` (the NaN-propagation soundness guard distinguishes it from a naive `z3.fpMin`/`fpMax`); `int_to_float` / `float_to_int` concrete-gated (symbolic args defer to Tier 3 — Z3's symbolic FP↔Real reasoning returns spurious counterexamples); `float_to_int` domain obligation (E529) for concrete NaN/Inf/out-of-range args. Verify-vs-run differentials confirm each model agrees with wasmtime bit-for-bit (±0, ±inf, NaN, ties, lo>hi, the 2^53 rounding boundary, i64 max, and the trap cases) |
-| `test_build_site.py` | 25 | 341 | Site-asset tooling — `_abs_links` rewriting (relative links, fenced-block immunity incl. inline backticks and tilde fences, http/https/fragment pass-through, Vera effect syntax not mis-parsed), `build_site` `<lastmod>` stability (preserve/refresh keyed on URL-structure change), `check_site_assets` sitemap staleness (missing / date-only-clean / structural-stale), and the #538 leak guard (vera:skip fence annotations stripped from generated `docs/SKILL.md` / `docs/llms-full.txt`, with a non-vacuous precondition that the source carries annotations) |
+| `test_build_site.py` | 46 | 698 | Site-asset tooling — `_abs_links` rewriting (relative links, fenced-block immunity incl. inline backticks and tilde fences, http/https/fragment pass-through, Vera effect syntax not mis-parsed), `build_site` `<lastmod>` stability (preserve/refresh keyed on URL-structure change), `check_site_assets` sitemap staleness (missing / date-only-clean / structural-stale), the #538 leak guard (vera:skip fence annotations stripped from generated `docs/SKILL.md` / `docs/llms-full.txt`, with a non-vacuous precondition that the source carries annotations), and the #1154 `check_fact_coherence` gate on `docs/index.html` ↔ `docs/index.md` (committed pair clean, then tmp_path-copy mutations for each drift class: a bumped percentage, version string, problem/model count, a removed/renamed table row, a changed tier, a dropped editor — plus extraction failure as gate failure for a restructured table, a deleted caveat, a missing editor claim, a missing file, and one file stating a fact two ways) |
 | `test_builtin_typevar_collision_970.py` | 61 | 811 | #970 a user `forall` type-var name colliding with a built-in generic's internal name (`T`/`E`/`A`/`B`/`K`/`U`/`V`): focused check/verify pins for the compound-argument shapes (`@Array<Option<T>>`, `@Result<Int, Option<E>>`, `@Map<K, Option<V>>`) plus a collide-vs-control differential battery over every generic-builtin family and contract/where-helper position.  Also pins marker-strip (the `#b` namespacing marker must never reach an E205/E202 diagnostic), a registry-consistency pin (every built-in ability-constraint `type_var` stays a member of its `forall_vars`), the dual completeness-gap pinned in both argument orders, a tier-split equality pin, and the #1069 leaked-placeholder message-rendering sweep (a stripped built-in var renders as `?`, not a bare letter, at every reachable actual-type slot: the mismatch sites plus the operator/index/interpolation family, `assert`/`assume`, `if` condition and branches, and the contract/refinement predicates — one parametrized row per converted render slot, with the provably-unreachable sites documented in the class docstring) |
 | `test_check_changelog_updated.py` | 68 | 712 | `check_changelog_updated.py` unit + end-to-end tests: file classification (incl. file-style exact-match vs directory-style prefix-match), CHANGELOG diff parsing with `[Unreleased]` section tracking, bare-heading rejection, and full-file context (regression test for bullets far below the heading), `Skip-changelog:` trailer detection, temp-repo integration covering substantive/exempt/label/trailer paths, and `GIT_*`-env hermeticity of the temp-repo fixtures (regression for the pre-commit-hook env leak) |
 | `test_release.py` | 47 | 566 | Release policy and registry verification (#481): strict project-name and version parsing/comparison, version-bump/TestPyPI/recovery planning, exact confirmation and immutable-tag guards, first-parent version-introduction discovery, package-change recovery refusal, non-empty CHANGELOG extraction, one-wheel/one-sdist SHA-256 manifests, malformed registry-response handling, missing/filename/hash propagation retries, exact filename/hash verification, and CLI dispatch/GitHub-output wiring.  An autouse fixture scrubs hook-exported `GIT_*` variables so the tmp-repo git calls (fixture helpers and `release.py`'s own) never resolve to the developer's repository when the suite runs inside a pre-commit hook. |
@@ -664,7 +664,7 @@ Twenty-two scripts in `scripts/` validate cross-cutting concerns beyond unit tes
 | `check_pypi_readme_examples.py` | All Vera code blocks in PYPI_README.md parse, check, and verify |
 | `check_examples_doc.py` | All Vera code blocks in EXAMPLES.md parse correctly |
 | `check_html_examples.py` | All Vera code blocks in docs/index.html pass parse + check + verify |
-| `check_site_assets.py` | Generated site assets under `docs/` are up-to-date |
+| `check_site_assets.py` | Generated site assets under `docs/` are up-to-date, and `docs/index.html` and `docs/index.md` state coherent facts (benchmark version, counts, results table, editor names) |
 | `check_version_sync.py` | `pyproject.toml`, `vera/__init__.py`, and the docs badge carry the same version |
 | `check_doc_counts.py` | Counts cited in the docs match the live codebase, KNOWN_ISSUES refactoring counts within ±10%, HISTORY version-row format |
 | `check_limitations_sync.py` | Limitation tables consistent across KNOWN_ISSUES.md, vera/README.md, spec chapters, SKILL.md, and LSP_SERVER.md |