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 26 49 value at compile time

Static pages are a closed enumeration (PageId); PageId.all is complete and Data.pages is built from it, so a link to an unregistered page is unrepresentable

People are a closed enumeration generated from the canonical data (PersonId); the lookup is total, so a leadership card cannot name someone who does not exist

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

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

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

No route path collides with any of the 49 asset paths

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

All 49 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 26 (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 26 route paths in the verified site are distinct

None of 8 retired brand/pseudonym/backstage patterns appear in any of the 26 rendered page bodies

Every divisionId on a news article or person record (8 refs) names one of the 5 declared divisions

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