What is checked

Each guarantee and build-time check is listed with its basis.

Sources and scope

This page reads NoGoals's built-in guarantee and gate definitions directly from the code at build time, keeping the list consistent with the implementation.

A build's report uses these definitions. It restates theorems proved by the site as claims about that site and records the results of the gates that ran. The verification page contains the evidence for this build.

The label on the right identifies each guarantee's scope. kernel applies to content routed through the verified renderer. chrome applies to the typed frame around every page. artifact applies to the files emitted by the build.

This build's verification pageVerification results for this site

Guarantees enforced by types

  • 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

Guarantees proved by theorems

  • 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

Security

This section lists escaping theorems and a typed delivery policy. Each entry states its basis.

  • 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

What is checked at build time

Gates run under --audit and check the candidate artifact and the data the site declared. The HTML gates read the emitted files through a parser. A site can add its own. If any gate fails, no files are copied to the output directory.

  • 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

Get started