何を検査するか

一覧の出典と保証の対象範囲

このビルドの検証ページこのサイトの検証結果

型による保証

• Bilingual completeness for editorial content

  artifact

  Every L leaf carries both JA and EN — enforced structurally by the L type; a page cannot ship with one language missing

  NoGoals.DSL.L (record with both ja and en fields)

• Dates are valid ISO calendar dates

  artifact

  Every article and page date is an `IsoDate`; the `IsoDate.lit` literal is parsed during elaboration, so a malformed date is a compile error

  NoGoals.Verify.IsoDate.lit (elaboration-checked literal)

• Output paths cannot escape the root

  artifact

  Every page path is derived from a Route whose slug is a list of validated [a-z0-9-] segments, and every asset path from validated [a-z0-9._-] segments that are never `.` or `..`; a name that could escape the output root or collide across case is unrepresentable — a compile error at the literal

  Segment / Slug / AssetPath types + Route.outputPath

• Route closure: every internal href resolves to an emitted page (IR vocabulary)

  kernel

  In the kernel IR, link targets are Fin nP (unrepresentable otherwise); rendered_link_resolves proves the emitted href, resolved as a browser and the host resolve it from any source page, is a file in the build plan. Body links of the shipped site are covered separately by the artifact-level link gate.

  Fin nP + rendered_link_resolves

• Fragment closure: a link's #anchor is an id the target declares (IR vocabulary)

  kernel

  A link's anchor is a member of the target page's anchor schema (AnchorIn); anchors_sound + body_ids_emitted prove the target's rendered tree carries that id

  AnchorIn subtype + rendered_fragment_declared

• No missing assets (IR vocabulary)

  kernel

  AssetId carries proof that asset exists with correct kind

  AssetId type witness

• No asset type confusion (IR vocabulary)

  kernel

  Cannot use JS file as image - kind is part of type

  AssetId n k A

• No empty alt text (IR vocabulary)

  kernel

  Alt attributes require NonEmptyStr

  NonEmptyStr type

• No empty link labels (IR vocabulary)

  kernel

  Link text requires NonEmptyStr

  NonEmptyStr type

• Safe external URLs only (IR vocabulary)

  kernel

  External URLs must be https/http/data URIs

  Url.Safe ADT

定理による保証

• Slug/index round-trip (IR)

  kernel

  indexOf (slug i) (lang i) = some i for all pages of a refined SiteV

  roundTrip₁ theorem

• i18n completeness (IR)

  kernel

  Every slug exists in every language, for a refined SiteV (the language set is closed: ja, en)

  i18nComplete theorem

• No file collisions (IR plan)

  kernel

  All output paths of a refined SiteV's build plan are unique - no overwrites

  unique_paths theorem

• Pages/assets path disjoint (IR)

  kernel

  Page paths never collide with asset paths in a refined SiteV

  disjointAssets theorem

• Build covers all content (IR plan)

  kernel

  Every page and asset of a refined SiteV appears in its build plan

  coverage theorem

• Asset path injectivity (IR)

  kernel

  Different assets have different paths

  Assets.path_injective

• Sitemap covers every route

  artifact

  Every route of an indexed page (page × language) is the loc of an entry that is a member of the generated sitemap, and the sitemap has exactly one entry per such route — no page dropped, none invented

  sitemap_covers + sitemap_entry_count theorems

• Stage headers ⊇ prod headers

  artifact

  Staging security headers never weaken prod; stage only adds directives

  stage_headers_superset_prod theorem

• Robots/sitemap URL consistent

  artifact

  Prod robots.txt Sitemap URL matches sitemap base URL — no drift

  prod_robots_sitemap_consistent theorem

• Canonical, hreflang and sitemap from one route set

  artifact

  The <head> canonical link, the <head> hreflang alternates, the sitemap alternates and the switcher are all Route.href of the same route set through one alternatesFor function: the JA and EN entries of a slug carry the identical alternate set (hreflang_symmetric) and every set names ja, en and x-default (alternates_complete)

  hreflang_symmetric + alternates_complete theorems

• Language switcher symmetric

  chrome

  The switcher offers a language iff the twin page's switcher offers the way back — a page you can switch into can always switch out

  switcher_symmetric theorem

セキュリティ

• Escaping correct where applied (typed tree)

  chrome

  Text and attribute content routed through the typed tree renderer is escaped; htmlEscape_no_specials proves the output contains no < > " ' for ANY input. Raw slot content is NOT covered by this theorem — each raw node is a named trust obligation checked by the runtime validators.

  htmlEscape_no_specials theorem

• CSP forbids inline styles and scripts (typed policy)

  artifact

  The typed HeadersPolicy ships style-src 'self' and script-src without 'unsafe-inline'; the emitted _headers file is rendered from it. Whether the emitted PAGES honor the policy is the CSP audit gate's claim, reported separately from its actual run.

  typed HeadersPolicy

• XML injection impossible (sitemap/feeds)

  artifact

  xmlEscape is the charwise htmlEscape; xmlEscape_no_specials proves sitemap and feed text/attribute content contains no < > " ' for ANY input

  xmlEscape_no_specials theorem

• Chrome structure well-formed (slots trusted)

  chrome

  Every content page is one typed HTML tree: kernel chrome (head, nav, hero, footer) around the site's typed slots; chrome_tree_wellFormed proves the chrome adds no imbalance whenever the slot trees are well-formed, and render_wf_mod promotes that to the rendered bytes modulo the listed raw slots — the fragment grammar plus void/normal tag classes, not HTML element semantics (html-validate remains the authority for those). The report pages use their own constructors and are checked well-formed (no raw node) before they are written.

  chrome_tree_wellFormed + render_wf_mod theorems

• Well-formed markup (kernel renderer)

  kernel

  The kernel renderer factors through a typed HTML tree; render_wf proves every raw-free tree renders to properly nested tags whose text and attribute values cannot open or close an element, with void elements never given children — balanced markup is a grammar theorem, not a validator's opinion

  render_wf grammar theorem

ビルド時に検査すること

• External link liveness

  artifact

  Every external URL the site embeds answers a liveness check (same-origin redirects followed)

  gate.external

• HTML validity (every emitted page)

  artifact

  html-validate (pinned) runs over every emitted HTML file, including the verification pages

  gate.html-validate

• Parser facts available

  artifact

  A browser-grade parser (parse5, pinned) produced facts for every emitted HTML file; the gates below read them

  gate.html-facts

• CSP ↔ content consistency

  artifact

  Every HTML-declared resource use on every page is allowed by the typed production CSP; inline script/style, event handlers and unmodelled elements fail

  gate.csp

• Internal reference closure

  artifact

  Every internal href/src/srcset/poster/action on every page resolves (browser + host semantics) to an emitted file or a declared endpoint, and every fragment to an id the target declares

  gate.links

• SEO coherence

  artifact

  Every route page's canonical link, hreflang alternates, og:url and og:locale equal the values its route predicts

  gate.seo

• Metadata completeness

  artifact

  Every route page declares its document language, one title, one non-empty description, og:title/description/type, and og:locale:alternate for the other languages

  gate.metadata

• No CJK leaks on English pages

  artifact

  Japanese text on EN pages only where deliberately allowed (visible text and human-facing attributes)

  gate.i18n-cjk

• CSS contract

  artifact

  Every class on every page is styled or a declared semantic hook

  gate.css-contract

• No double-escaped entities

  artifact

  No double escaping in any page's visible text: an entity that was escaped twice shows up as literal entity text

  gate.escaping

• Click-path reachability

  artifact

  Every page is reachable from a declared root (pages declared redirect-reached and the not-found pages aside)

  gate.reachability

• Stylesheet asset reality

  artifact

  Every url(/assets/…) reference in the declared stylesheets exists in the candidate artifact

  gate.assets

• News invariants

  artifact

  Articles sorted newest-first; none future-dated vs the wall clock

  gate.news

• Feed entries are emitted routes

  artifact

  Every Atom entry route is a route this build emitted

  gate.feeds

• Permalink permanence

  artifact

  Every previously published URL obligation is live or typed-redirected; `_redirects` is rendered from the same map

  gate.permalinks

はじめる