darcsweb - Log

The gen/ directory is not tracked in darcs; it is produced by
`make -C verified extract`, which Setup.hs' preBuild hook already
runs during `stack build` using the pinned Rocq 9.0.0 installed in
the build stage.  COPY gen/ gen/ therefore failed on fresh hosts
(no directory in the build context) and risked shipping stale
host-side extractions when it did succeed.

Security:
- getRepoTree now rejects non-empty subpaths that fail isSafeSubPath,
  closing a path-disclosure that exposed _darcs/ via the tree UI.
- Tree/blob breadcrumbs HTML-escape labels and percent-encode hrefs
  so a directory name containing HTML or URL-structural characters
  can no longer inject markup or break out of the URL.
- serveClone enforces a strict two-segment allowlist
  (hashed_inventory, inventories/_, patches/_, pristine.hashed/_,
  optional packs/basic.tar.gz + packs/patches.tar.gz) instead of
  serving every file that passed isSafeSubPath.
- readRepoDescription and getRepoBlob use strict ByteString +
  explicit UTF-8 validation under try; a NUL-byte sniff keeps binary
  files from being escaped character by character.
- All request-time canonicalizePath calls go through a new
  safeCanonicalize helper that degrades IO errors to 404 instead of
  leaking framework 500s.
- parsePortPure rejects empty, whitespace, hex, and non-digit port
  strings, replacing the partial Text.Read.read on startup.

Performance:
- getRepoPatch hash-filters before rendering diffs; a missing hash no
  longer walks and renders the entire patch history.
- getRepoSummary replaces listRepos + getRepoPatches + getRepoTags
  with a single readPatches pass. Count and tag positions come from
  cheap PatchInfo; extractPatchListing only runs on rows actually
  displayed.
- Native Text implementation of esc replaces the HtmlPure.esc String
  bridge. Equivalence against the Coq-extracted spec is pinned by
  QuickCheck with a biased generator over escaped characters.
- Tree/blob breadcrumb build is now O(depth) (threaded Text prefix)
  instead of O(depth^2) (acc ++ [p]).

UX / mobile-first:
- renderPage emits semantic <header>/<main>/<footer> landmarks plus a
  favicon <link>. Empty breadcrumb <nav> is skipped on index and 404.
- Index page has a visible <h1> site title.
- repoNavBar is a <nav aria-label="Repository sections"> with
  aria-current="page" on the active tab.
- Full-log entries are <article class="log-entry">.
- Tree-icon cells carry aria-hidden="true".

Tests:
- New Properties.Config covers parsePortPure's accepted/rejected set.
- Properties.Clone pins the two-segment clone allowlist and rejects
  nested paths (patches/a/b, inventories/a/b, pristine.hashed/a/b).
- Properties.Html pins the native esc equivalence vs HtmlPure.esc
  with a biased generator, plus example-based tests for the
  breadcrumb escape + percent-encode contracts (including the empty
  blob-breadcrumb degenerate case).

Reviews under reviews/ record the pre- and post-change findings from
three Codex + three Claude agents (first pass) and four Codex + four
Claude agents (post-change), plus the reconciliation document that
the user-visible fixes were derived from.

Security-critical pure functions (HTML escaping, path validation,
trailing slash normalization) are reimplemented in Gallina, formally
proven correct, and extracted to Haskell. Remaining pure functions
are covered by QuickCheck properties. Rocq extraction runs
automatically on stack build, proofs and QuickCheck on stack test.

So no one can access file, he is not allowed to.