NoGoals 検証レポート

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

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

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

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.

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

AssetId carries proof that asset exists with correct kind

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

Alt attributes require NonEmptyStr

Link text requires NonEmptyStr

External URLs must be https/http/data URIs

NoGoals.refine produces a verified SiteV 6 4 value at compile time

For all i, indexOf (slug i) (lang i) = some i — on this site's SiteV 6 4

Every page slug exists in both languages — NoGoals theorem on this site's SiteV

All 10 page and asset files in the NoGoals build plan have unique paths

No route path collides with any of the 4 asset paths

Every route in the verified site has a corresponding file in the build plan

All 4 asset paths are distinct (native_decide on the concrete list)

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

Staging security headers never weaken prod; stage only adds directives

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

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)

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

NoGoals.refine constructed a verified SiteV for all 6 (page × language) routes of this site's page SKELETON (slugs, languages, output paths — bodies are the trusted shell's): (slug,lang) round-trip, i18n completeness across both languages, unique output paths

All 6 route paths in the verified site are distinct

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.

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.

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

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.

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